Tracing for OCaml

Author: wimmers

ML/Checker.ml

@@ -352,11 +352,11 @@ let check_and_verify2 p m ignore_k max_steps inv trans prog query bounds pred s
     in let t = Sys.time() -. t
     in let _ = println("Internal time for precondition check + actual checking: " ^ string_of_float t)
     and _ = println("")
-    (* and _ = if !debug_level >= 1 then
+    and _ = if !debug_level >= 1 then
       let
         _ = println("# explored states: " ^ string_of_int(Tracing.get_count ()))
         and _ = println("")
-      in () else (); *)
+      in () else ();
   in
     print_result result
 

library/Tracing.thy

@@ -17,12 +17,25 @@ end = struct
   fun count_up () = (counter := !counter + 1);
   fun get_count () = !counter;
 end
+\<close> and (OCaml)
+\<open>
+module Tracing : sig
+  val count_up : unit -> unit
+  val get_count : unit -> int
+end = struct
+  let counter = ref 0
+  let count_up () = (counter := !counter + 1)
+  let get_count () = !counter
+end
 \<close>
 
 code_reserved SML Tracing
 
+code_reserved OCaml Tracing
+
 code_printing
   constant write_msg \<rightharpoonup> (SML) "(fn x => Tracing.count'_up ()) _"
+       and            (OCaml) "(fun x -> Tracing.count'_up ()) _"
 
 definition trace where
   "trace m x = (let a = write_msg m in x)"