From 75e42072f4ebe59ed9d817b463065816e8c95945 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 1 Mar 2023 22:37:04 -0500
Subject: [PATCH] wip: feat(leancheck): store intermediate objects of the proof

---
 src/leancheck/leancheck.ml  | 72 +++++++++++++++++++++++++++++++++++--
 src/leancheck/parse_intf.ml |  4 +--
 2 files changed, 72 insertions(+), 4 deletions(-)

diff --git a/src/leancheck/leancheck.ml b/src/leancheck/leancheck.ml
index bb6449f6..e575094e 100644
--- a/src/leancheck/leancheck.ml
+++ b/src/leancheck/leancheck.ml
@@ -1,7 +1,71 @@
 module T = Sidekick_core_logic.Term
+module Level = Sidekick_core_logic.Level
 
 let ( let@ ) = ( @@ )
 
+type obj =
+  | O_level of Level.t
+  | O_name of string
+  | O_term of T.t
+  | O_ind of string * T.t
+
+(** Intermediate objects in a proof *)
+module Obj = struct
+  type t = obj
+
+  let pp out = function
+    | O_level lvl -> Level.pp out lvl
+    | O_name n -> Fmt.fprintf out "#name %S" n
+    | O_term t -> T.pp_debug out t
+    | O_ind (n, _) -> Fmt.fprintf out "#ind %s" n
+
+  let dummy : t = O_name ""
+end
+
+(** Map indexes to objects *)
+module Idx = struct
+  type t = { obj: obj Vec.t }
+
+  (* create. The slot 0 is already filled with name "" *)
+  let create () : t = { obj = Vec.make 1 Obj.dummy }
+
+  (** ensure that index [n] is valid *)
+  let ensure_size (self : t) (n : int) : unit =
+    if n >= Vec.size self.obj then Vec.ensure_size self.obj ~elt:Obj.dummy n
+
+  let[@inline] get (self : t) (i : int) : obj = Vec.get self.obj i
+
+  let[@inline] set (self : t) (i : int) o : unit =
+    ensure_size self i;
+    Vec.set self.obj i o
+
+  let[@inline] set_name self i n : unit = set self i (O_name n)
+  let[@inline] set_level self i l : unit = set self i (O_level l)
+  let[@inline] set_term self i t : unit = set self i (O_term t)
+
+  let get_name self i : string =
+    match get self i with
+    | O_name s -> s
+    | _o -> Error.errorf "expected a name at %d, got %a" i Obj.pp _o
+
+  let get_level self i : Level.t =
+    match get self i with
+    | O_level l -> l
+    | _o -> Error.errorf "expected a level at %d, got %a" i Obj.pp _o
+
+  let get_term self i : T.t =
+    match get self i with
+    | O_term t -> t
+    | _o -> Error.errorf "expected a term at %d, got %a" i Obj.pp _o
+end
+
+(** Join two names with "." *)
+let name_join a b =
+  if a = "" then
+    b
+  else
+    a ^ "." ^ b
+
 let process_files (files : string list) : unit =
   let start = Mtime_clock.now () in
   let st = T.Store.create ~size:1024 () in
@@ -12,11 +76,15 @@ let process_files (files : string list) : unit =
 
   let proc_file (file : string) : unit =
     let@ ic = CCIO.with_in file in
+    let idx = Idx.create () in
+
     Parse.parse (`In ic)
       (module struct
         let line _ = incr n_lines
-        let ns _ _ = ()
-        let ni _ _ = ()
+        let ns ~at i s = Idx.set_name idx at (name_join (Idx.get_name idx i) s)
+
+        let ni ~at i n =
+          Idx.set_name idx at (name_join (Idx.get_name idx i) (string_of_int n))
       end)
   in
 
diff --git a/src/leancheck/parse_intf.ml b/src/leancheck/parse_intf.ml
index 71d7d009..a98036d7 100644
--- a/src/leancheck/parse_intf.ml
+++ b/src/leancheck/parse_intf.ml
@@ -1,5 +1,5 @@
 module type CALLBACK = sig
   val line : string -> unit
-  val ns : int -> string -> unit
-  val ni : int -> int -> unit
+  val ns : at:int -> int -> string -> unit
+  val ni : at:int -> int -> int -> unit
 end