From cd07d6924b26e84d61237b55ebee06422bba6656 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 28 Feb 2023 23:38:04 -0500
Subject: [PATCH] details for leancheck

---
 src/leancheck/dune          |  2 +-
 src/leancheck/leancheck.ml  | 11 +++++++++++
 src/leancheck/parse.ml      |  3 ++-
 src/leancheck/parse_intf.ml |  1 +
 4 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/leancheck/dune b/src/leancheck/dune
index afc5a15c..d50097e9 100644
--- a/src/leancheck/dune
+++ b/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))
diff --git a/src/leancheck/leancheck.ml b/src/leancheck/leancheck.ml
index 75baceb7..bb6449f6 100644
--- a/src/leancheck/leancheck.ml
+++ b/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 () =
diff --git a/src/leancheck/parse.ml b/src/leancheck/parse.ml
index 27b94520..5f80a4e8 100644
--- a/src/leancheck/parse.ml
+++ b/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 ()
diff --git a/src/leancheck/parse_intf.ml b/src/leancheck/parse_intf.ml
index 8cde17b2..71d7d009 100644
--- a/src/leancheck/parse_intf.ml
+++ b/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