feat(leancheck): handle term constructors

src/leancheck/leancheck.ml

@@ -1,4 +1,5 @@
 module T = Sidekick_cic_lib.Term
+module Const = Sidekick_cic_lib.Const
 module Level = Sidekick_cic_lib.Level
 
 let ( let@ ) = ( @@ )
@@ -16,7 +17,7 @@ module Obj = struct
   let pp out = function
     | O_level lvl -> Fmt.fprintf out "(#lvl %a)" Level.pp lvl
     | O_name n -> Fmt.fprintf out "(#name %S)" n
-    | O_term t -> T.pp_debug out t
+    | O_term t -> Fmt.fprintf out "(@[#term %a@])" T.pp_debug t
     | O_ind (n, _) -> Fmt.fprintf out "(#ind %s)" n
 
   let dummy : t = O_name ""
@@ -24,49 +25,56 @@ end
 
 (** Map indexes to objects *)
 module Idx = struct
-  type t = { obj: obj Vec.t }
+  type t = { names: string Vec.t; levels: Level.t Vec.t; terms: T.t Vec.t }
 
   (* create. The slot 0 is already filled with name "" *)
   let create () : t =
-    let obj = Vec.create () in
+    let names = Vec.create () in
-    Vec.push obj Obj.dummy;
+    Vec.push names "";
-    { obj }
+    let levels = Vec.create () in
+    let terms = Vec.create () in
+    { names; levels; terms }
 
   (** ensure that index [n] is valid *)
-  let ensure_size (self : t) (n : int) : unit =
+  let ensure_size (v : _ Vec.t) ~dummy (n : int) : unit =
-    if n >= Vec.size self.obj then Vec.ensure_size self.obj ~elt:Obj.dummy n
+    if n >= Vec.size v then Vec.ensure_size v ~elt:dummy n
 
-  let[@inline] get (self : t) (i : int) : obj =
+  let set_name self i n : unit =
-    try Vec.get self.obj i
+    ensure_size self.names ~dummy:"" (i + 1);
-    with _ -> Error.errorf "cannot access object at index %d" i
+    Vec.set self.names i n
-
-  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
+    match Vec.get self.names i with
-    | O_name s -> s
+    | s -> s
-    | _o -> Error.errorf "expected a name at %d, got %a" i Obj.pp _o
+    | exception _ -> Error.errorf "invalid name at %d" i
 
-  let get_level self i : Level.t =
+  let set_term self i t : unit =
-    match get self i with
+    ensure_size self.terms ~dummy:T.type_ (i + 1);
-    | O_level l -> l
+    Vec.set self.terms i t
-    | _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
+    match Vec.get self.terms i with
-    | O_term t -> t
+    | s -> s
-    | _o -> Error.errorf "expected a term at %d, got %a" i Obj.pp _o
+    | exception _ -> Error.errorf "invalid term at %d" i
+
+  let set_level self i l : unit =
+    ensure_size self.levels ~dummy:Level.zero (i + 1);
+    Vec.set self.levels i l
+
+  let get_level self i : Level.t =
+    match Vec.get self.levels i with
+    | s -> s
+    | exception _ -> Error.errorf "invalid level at %d" i
 
   let dump out (self : t) : unit =
-    Fmt.fprintf out "(@[idx %a@])"
+    Fmt.fprintf out
-      (Fmt.iter ~sep:(Fmt.return "@ ") Obj.pp)
+      "(@[idx {@ names: [@[%a@]],@ terms: [@[%a@]],@ levels: [@[%a@]]}@])"
-      (Vec.to_iter self.obj)
+      (Fmt.iter ~sep:(Fmt.return "@ ") Fmt.Dump.string)
+      (Vec.to_iter self.names)
+      (Fmt.iter ~sep:(Fmt.return "@ ") T.pp_debug)
+      (Vec.to_iter self.terms)
+      (Fmt.iter ~sep:(Fmt.return "@ ") Level.pp)
+      (Vec.to_iter self.levels)
 end
 
 (** Join two names with "." *)
@@ -76,6 +84,13 @@ let name_join a b =
   else
     a ^ "." ^ b
 
+let binder_of_string = function
+  | "#BD" -> T.BD
+  | "#BI" -> T.BI
+  | "#BS" -> T.BS
+  | "#BC" -> T.BC
+  | s -> failwith (Printf.sprintf "invalid binder: %S" s)
+
 let process_files ~max_err (files : string list) : unit =
   let start = Mtime_clock.now () in
 
@@ -117,6 +132,31 @@ let process_files ~max_err (files : string list) : unit =
 
         let up ~at i : unit =
           Idx.set_level idx at (Level.var @@ Idx.get_name idx i)
+
+        let ev ~at i : unit = Idx.set_term idx at (T.bvar_i i)
+
+        let ea ~at i j : unit =
+          Idx.set_term idx at (T.app (Idx.get_term idx i) (Idx.get_term idx j))
+
+        let ec ~at i_name i_args : unit =
+          let name = Idx.get_name idx i_name in
+          let args = List.map (Idx.get_level idx) i_args in
+          Idx.set_term idx at (T.const (Const.make name) args)
+
+        let es ~at i : unit =
+          Idx.set_term idx at (T.type_of_univ (Idx.get_level idx i))
+
+        let el ~at b n i j : unit =
+          Idx.set_term idx at
+            (T.lam (binder_of_string b) (Idx.get_name idx n)
+               ~var_ty:(Idx.get_term idx i) (Idx.get_term idx j))
+
+        let ep ~at b n i j : unit =
+          Idx.set_term idx at
+            (T.pi (binder_of_string b) (Idx.get_name idx n)
+               ~var_ty:(Idx.get_term idx i) (Idx.get_term idx j))
+
+        let after_line () = Fmt.eprintf "%a@." Idx.dump idx
       end)
   in
 

src/leancheck/parse.ml

@@ -57,7 +57,7 @@ let parse ?(max_errors = max_int) (input : input) (cb : callback) : unit =
     match IN.next_line () with
     | None -> ()
     | Some line ->
-      Log.debugf 50 (fun k -> k "(leancheck.parse-line %S)" line);
+      Log.debugf 50 (fun k -> k "(leancheck.parse-line[%d] %S)" !n_line line);
       CB.line line;
 
       (try
@@ -69,12 +69,29 @@ let parse ?(max_errors = max_int) (input : input) (cb : callback) : unit =
          | [ I at; S "#UM"; I i; I j ] -> CB.um ~at i j
          | [ I at; S "#UIM"; I i; I j ] -> CB.uim ~at i j
          | [ I at; S "#UP"; I i ] -> CB.up ~at i
-         | _ -> ()
+         | [ I at; S "#EV"; I i ] -> CB.ev ~at i
+         | [ I at; S "#EA"; I i; I j ] -> CB.ea ~at i j
+         | I at :: S "#EC" :: I i :: args ->
+           let args =
+             List.map
+               (function
+                 | I i -> i
+                 | _ -> failwith "argument must be an int")
+               args
+           in
+           CB.ec ~at i args
+         | [ I at; S "#ES"; I i ] -> CB.es ~at i
+         | [ I at; S "#EL"; S b; I n; I i; I j ] -> CB.el ~at b n i j
+         | [ I at; S "#EP"; S b; I n; I i; I j ] -> CB.ep ~at b n i j
+         | _ ->
+           incr n_errors;
+           Fmt.eprintf "warn: unhandled line %d: %s@." !n_line line
        with e ->
          incr n_errors;
          Fmt.eprintf "error on line %d:@.%s@." !n_line (Printexc.to_string e));
 
       incr n_line;
+      CB.after_line ();
 
       if !n_errors < max_errors then loop ()
   in

src/leancheck/parse_intf.ml

@@ -1,9 +1,16 @@
 module type CALLBACK = sig
   val line : string -> unit
+  val after_line : unit -> unit
   val ns : at:int -> int -> string -> unit
   val ni : at:int -> int -> int -> unit
   val us : at:int -> int -> unit
   val um : at:int -> int -> int -> unit
   val uim : at:int -> int -> int -> unit
   val up : at:int -> int -> unit
+  val ev : at:int -> int -> unit
+  val ea : at:int -> int -> int -> unit
+  val ec : at:int -> int -> int list -> unit
+  val es : at:int -> int -> unit
+  val el : at:int -> string -> int -> int -> int -> unit
+  val ep : at:int -> string -> int -> int -> int -> unit
 end