details for leancheck

src/leancheck/dune

@@ -1,4 +1,4 @@
 (executable
  (name leancheck)
  (flags :standard -w +32 -open Sidekick_sigs -open Sidekick_util)
- (libraries containers sidekick.core-logic sidekick.util))
+ (libraries containers sidekick.core-logic sidekick.util mtime mtime.clock.os))

src/leancheck/leancheck.ml

@@ -3,20 +3,31 @@ module T = Sidekick_core_logic.Term
 let ( let@ ) = ( @@ )
 
 let process_files (files : string list) : unit =
+  let start = Mtime_clock.now () in
   let st = T.Store.create ~size:1024 () in
   Log.debugf 1 (fun k ->
       k "(@[process-files %a@])" Fmt.Dump.(list string) files);
 
+  let n_lines = ref 0 in
+
   let proc_file (file : string) : unit =
     let@ ic = CCIO.with_in file in
     Parse.parse (`In ic)
       (module struct
+        let line _ = incr n_lines
         let ns _ _ = ()
         let ni _ _ = ()
       end)
   in
 
   List.iter proc_file files;
+
+  let elapsed =
+    (Mtime.span (Mtime_clock.now ()) start |> Mtime.Span.to_float_ns) /. 1e9
+  in
+  Log.debugf 1 (fun k ->
+      k "number of lines processed: %d in %.4fs (%.2f/s)" !n_lines elapsed
+        (float !n_lines /. elapsed));
   ()
 
 let () =

src/leancheck/parse.ml

@@ -41,7 +41,8 @@ let parse (input : input) (cb : callback) : unit =
     match IN.next_line () with
     | None -> ()
     | Some line ->
-      Printf.eprintf "line %S\n" line;
+      Log.debugf 50 (fun k -> k "(leancheck.parse-line %S)" line);
+      CB.line line;
 
       (* TODO: cb *)
       loop ()

src/leancheck/parse_intf.ml

@@ -1,4 +1,5 @@
 module type CALLBACK = sig
+  val line : string -> unit
   val ns : int -> string -> unit
   val ni : int -> int -> unit
 end