Theory PromelaStatistics

theory PromelaStatistics
imports 
  CAVA_Base.CAVA_Base
begin

code_printing
  code_module PromelaStatistics ⇀ (SML) ‹
    structure PromelaStatistics = struct
      val active = Unsynchronized.ref false
      val parseTime = Unsynchronized.ref Time.zeroTime
      val time = Unsynchronized.ref Time.zeroTime

      fun is_active () = !active

      fun start () = (
            active := true; 
            if !parseTime = Time.zeroTime then () else parseTime := Time.- (Time.now (), !parseTime);
            time := Time.now ())
      fun start_parse () = (active := true; parseTime := Time.now())
      fun stop_timer () = (time := Time.- (Time.now (), !time))

      fun to_string () = let
        val t = Time.toMilliseconds (!time)
        val pt = Time.toMilliseconds (!parseTime)
      in
        (if pt = 0 then "" else 
        "Parsing time : " ^ IntInf.toString pt ^ "ms\n")
      ^ "Building time: " ^ IntInf.toString t ^ "ms\n"
      end
        
      val _ = Statistics.register_stat ("Promela",is_active,to_string)
    end
›
code_reserved SML PromelaStatistics

ML_val ‹@{code hd}›

consts 
  start :: "unit ⇒ unit"
  start_parse :: "unit ⇒ unit"
  stop_timer :: "unit ⇒ unit"

code_printing
  constant start ⇀ (SML) "PromelaStatistics.start"
| constant start_parse ⇀ (SML) "PromelaStatistics.start'_parse"
| constant stop_timer ⇀ (SML) "PromelaStatistics.stop'_timer"

hide_const (open) start start_parse stop_timer

end