wip: feat(leancheck): parse universe commands

src/leancheck/leancheck.ml

@@ -14,10 +14,10 @@ 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_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_ind (n, _) -> Fmt.fprintf out "#ind %s" n
+    | O_ind (n, _) -> Fmt.fprintf out "(#ind %s)" n
 
   let dummy : t = O_name ""
 end
@@ -27,13 +27,18 @@ 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 }
+  let create () : t =
+    let obj = Vec.create () in
+    Vec.push obj Obj.dummy;
+    { obj }
 
   (** 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] get (self : t) (i : int) : obj =
+    try Vec.get self.obj i
+    with _ -> Error.errorf "cannot access object at index %d" i
 
   let[@inline] set (self : t) (i : int) o : unit =
     ensure_size self i;
@@ -57,6 +62,11 @@ module Idx = struct
     match get self i with
     | O_term t -> t
     | _o -> Error.errorf "expected a term at %d, got %a" i Obj.pp _o
+
+  let dump out (self : t) : unit =
+    Fmt.fprintf out "(@[idx %a@])"
+      (Fmt.iter ~sep:(Fmt.return "@ ") Obj.pp)
+      (Vec.to_iter self.obj)
 end
 
 (** Join two names with "." *)
@@ -66,25 +76,51 @@ let name_join a b =
   else
     a ^ "." ^ b
 
-let process_files (files : string list) : unit =
+let process_files ~max_err (files : string list) : unit =
   let start = Mtime_clock.now () in
   let st = T.Store.create ~size:1024 () in
+  let lvl_st = T.Store.lvl_store st in
+
   Log.debugf 1 (fun k ->
       k "(@[process-files %a@])" Fmt.Dump.(list string) files);
 
   let n_lines = ref 0 in
 
+  (* get a level. 0 means level 0. *)
+  let get_level idx i =
+    if i = 0 then
+      Level.zero lvl_st
+    else
+      Idx.get_level idx i
+  in
+
   let proc_file (file : string) : unit =
     let@ ic = CCIO.with_in file in
     let idx = Idx.create () in
 
-    Parse.parse (`In ic)
+    Parse.parse ~max_errors:max_err (`In ic)
       (module struct
         let line _ = incr n_lines
-        let ns ~at i s = Idx.set_name idx at (name_join (Idx.get_name idx i) s)
 
-        let ni ~at i n =
+        let ns ~at i s : unit =
+          Idx.set_name idx at (name_join (Idx.get_name idx i) s)
+
+        let ni ~at i n : unit =
           Idx.set_name idx at (name_join (Idx.get_name idx i) (string_of_int n))
+
+        let us ~at i : unit =
+          Idx.set_level idx at (Level.succ lvl_st @@ get_level idx i)
+
+        let um ~at i j : unit =
+          Idx.set_level idx at
+            (Level.max lvl_st (get_level idx i) (get_level idx j))
+
+        let uim ~at i j : unit =
+          Idx.set_level idx at
+            (Level.imax lvl_st (get_level idx i) (get_level idx j))
+
+        let up ~at i : unit =
+          Idx.set_level idx at (Level.var lvl_st @@ Idx.get_name idx i)
       end)
   in
 
@@ -100,10 +136,14 @@ let process_files (files : string list) : unit =
 
 let () =
   let files = ref [] in
+  let max_err = ref max_int in
   let opts =
     [
       "--debug", Arg.Int Log.set_debug, " set debug level";
       "-d", Arg.Int Log.set_debug, " like --debug";
+      ( "--max-err",
+        Arg.Set_int max_err,
+        " maximum number of errors before bailing out" );
     ]
     |> Arg.align
   in
@@ -111,4 +151,4 @@ let () =
   Arg.parse opts (CCList.Ref.push files) "leancheck file+";
   if !files = [] then failwith "provide at least one file";
 
-  process_files (List.rev !files)
+  process_files ~max_err:!max_err (List.rev !files)

src/leancheck/parse.ml

@@ -33,10 +33,26 @@ let in_of_input (i : input) : (module IN) =
       let next_line () = try Some (input_line ic) with End_of_file -> None
     end)
 
-let parse (input : input) (cb : callback) : unit =
+module Lex = struct
+  type token = I of int | S of string
+
+  let lex_line (s : string) : token list =
+    let l = String.split_on_char ' ' s in
+    List.map
+      (fun s ->
+        match int_of_string_opt s with
+        | None -> S s
+        | Some i -> I i)
+      l
+end
+
+let parse ?(max_errors = max_int) (input : input) (cb : callback) : unit =
   let (module CB) = cb in
   let (module IN) = in_of_input input in
 
+  let n_line = ref 0 in
+  let n_errors = ref 0 in
+
   let rec loop () =
     match IN.next_line () with
     | None -> ()
@@ -44,8 +60,23 @@ let parse (input : input) (cb : callback) : unit =
       Log.debugf 50 (fun k -> k "(leancheck.parse-line %S)" line);
       CB.line line;
 
-      (* TODO: cb *)
-      loop ()
+      (try
+         let open Lex in
+         match Lex.lex_line line with
+         | [ I at; S "#NS"; I i; S name ] -> CB.ns ~at i name
+         | [ I at; S "#NI"; I i; I j ] -> CB.ni ~at i j
+         | [ I at; S "#US"; I i ] -> CB.us ~at i
+         | [ 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
+         | _ -> ()
+       with e ->
+         incr n_errors;
+         Fmt.eprintf "error on line %d:@.%s@." !n_line (Printexc.to_string e));
+
+      incr n_line;
+
+      if !n_errors < max_errors then loop ()
   in
 
   loop ()

src/leancheck/parse.mli

@@ -3,4 +3,4 @@ module type CALLBACK = Parse_intf.CALLBACK
 type callback = (module CALLBACK)
 type input = [ `String of string | `In of in_channel ]
 
-val parse : input -> callback -> unit
+val parse : ?max_errors:int -> input -> callback -> unit

src/leancheck/parse_intf.ml

@@ -2,4 +2,8 @@ module type CALLBACK = sig
   val line : string -> 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
 end