update leancheck+format

src/leancheck/lean_elab.ml

@@ -0,0 +1,26 @@
+module T = Sidekick_cic_lib.Term
+module C = Sidekick_cic_lib.Const
+
+let binder_to_cic : Lean_term.binder -> T.binder = function
+  | Lean_term.BD -> T.BD
+  | Lean_term.BI -> T.BI
+  | Lean_term.BS -> T.BS
+  | Lean_term.BC -> T.BC
+
+(* ctx: list of elaborated types for BVar 0, 1, ... (innermost first) *)
+let rec elab ~(ctx : T.t list) (lt : Lean_term.t) : T.t =
+  match lt with
+  | Lean_term.Sort l -> T.type_of_univ l
+  | Lean_term.BVar i -> T.bvar_i i
+  | Lean_term.Const (n, ls) -> T.const (C.make n) ls
+  | Lean_term.App (f, a) -> T.app (elab ~ctx f) (elab ~ctx a)
+  | Lean_term.Lam (b, n, ty, body) ->
+    let ty' = elab ~ctx ty in
+    let body' = elab ~ctx:(ty' :: ctx) body in
+    T.lam (binder_to_cic b) n ~var_ty:ty' body'
+  | Lean_term.Pi (b, n, ty, body) ->
+    let ty' = elab ~ctx ty in
+    let body' = elab ~ctx:(ty' :: ctx) body in
+    T.pi (binder_to_cic b) n ~var_ty:ty' body'
+
+let elab_top lt = elab ~ctx:[] lt

src/leancheck/lean_elab.mli

@@ -0,0 +1,4 @@
+val elab :
+  ctx:Sidekick_cic_lib.Term.t list -> Lean_term.t -> Sidekick_cic_lib.Term.t
+
+val elab_top : Lean_term.t -> Sidekick_cic_lib.Term.t

src/leancheck/lean_term.ml

@@ -0,0 +1,25 @@
+module Level = Sidekick_cic_lib.Level
+
+type binder = BD | BI | BS | BC
+
+type t =
+  | Sort of Level.t
+  | BVar of int (* de Bruijn index only, no type *)
+  | Const of string * Level.t list
+  | App of t * t
+  | Lam of binder * string * t * t (* binder, name, var_ty, body *)
+  | Pi of binder * string * t * t
+
+let dummy = Sort Level.one
+
+let rec pp out = function
+  | Sort l -> Fmt.fprintf out "Sort(%a)" Level.pp l
+  | BVar i -> Fmt.fprintf out "BVar(%d)" i
+  | Const (n, []) -> Fmt.string out n
+  | Const (n, ls) ->
+    Fmt.fprintf out "(%s %a)" n (Fmt.list ~sep:(Fmt.return " ") Level.pp) ls
+  | App (f, a) -> Fmt.fprintf out "(%a %a)" pp f pp a
+  | Lam (_, n, ty, body) ->
+    Fmt.fprintf out "(fun (%s : %a). %a)" n pp ty pp body
+  | Pi (_, n, ty, body) ->
+    Fmt.fprintf out "(forall (%s : %a). %a)" n pp ty pp body

src/leancheck/lean_term.mli

@@ -0,0 +1,14 @@
+module Level = Sidekick_cic_lib.Level
+
+type binder = BD | BI | BS | BC
+
+type t =
+  | Sort of Level.t
+  | BVar of int
+  | Const of string * Level.t list
+  | App of t * t
+  | Lam of binder * string * t * t
+  | Pi of binder * string * t * t
+
+val dummy : t
+val pp : t Fmt.printer

src/leancheck/leancheck.ml

@@ -7,7 +7,11 @@ let ( let@ ) = ( @@ )
 
 (** Map indexes to objects *)
 module Idx = struct
-  type t = { names: string Vec.t; levels: Level.t Vec.t; terms: T.t Vec.t }
+  type t = {
+    names: string Vec.t;
+    levels: Level.t Vec.t;
+    terms: Lean_term.t Vec.t;
+  }
 
   (* create. The slot 0 is already filled with name "" *)
   let create () : t =
@@ -31,10 +35,10 @@ module Idx = struct
     | exception _ -> Error.errorf "invalid name at %d" i
 
   let set_term self i t : unit =
-    ensure_size self.terms ~dummy:T.type_ (i + 1);
+    ensure_size self.terms ~dummy:Lean_term.dummy (i + 1);
     Vec.set self.terms i t
 
-  let get_term self i : T.t =
+  let get_term self i : Lean_term.t =
     match Vec.get self.terms i with
     | s -> s
     | exception _ -> Error.errorf "invalid term at %d" i
@@ -54,7 +58,7 @@ module Idx = struct
       "(@[idx {@ names: [@[%a@]],@ terms: [@[%a@]],@ levels: [@[%a@]]}@])"
       (Fmt.iter ~sep:(Fmt.return ";@ ") (pp_with_idx Fmt.Dump.string))
       (Vec.to_iter self.names |> Iter.zip_i)
-      (Fmt.iter ~sep:(Fmt.return ";@ ") (pp_with_idx T.pp_debug))
+      (Fmt.iter ~sep:(Fmt.return ";@ ") (pp_with_idx Lean_term.pp))
       (Vec.to_iter self.terms |> Iter.zip_i)
       (Fmt.iter ~sep:(Fmt.return ";@ ") Level.pp)
       (Vec.to_iter self.levels)
@@ -68,13 +72,13 @@ let name_join a b =
     a ^ "." ^ b
 
 let binder_of_string = function
-  | "#BD" -> T.BD
-  | "#BI" -> T.BI
-  | "#BS" -> T.BS
-  | "#BC" -> T.BC
+  | "#BD" -> Lean_term.BD
+  | "#BI" -> Lean_term.BI
+  | "#BS" -> Lean_term.BS
+  | "#BC" -> Lean_term.BC
   | s -> failwith (Printf.sprintf "invalid binder: %S" s)
 
-let process_files ~max_err (files : string list) : unit =
+let process_files ~max_err ~quiet (files : string list) : unit =
   let start = Mtime_clock.now () in
 
   Log.debugf 1 (fun k ->
@@ -116,38 +120,45 @@ 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 ev ~at i : unit = Idx.set_term idx at (Lean_term.BVar i)
 
         let ea ~at i j : unit =
-          Idx.set_term idx at (T.app (Idx.get_term idx i) (Idx.get_term idx j))
+          Idx.set_term idx at
+            (Lean_term.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)
+          Idx.set_term idx at (Lean_term.Const (name, args))
 
         let es ~at i : unit =
-          Idx.set_term idx at (T.type_of_univ (Idx.get_level idx i))
+          Idx.set_term idx at (Lean_term.Sort (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))
+            (Lean_term.Lam
+               ( binder_of_string b,
+                 Idx.get_name idx n,
+                 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))
+            (Lean_term.Pi
+               ( binder_of_string b,
+                 Idx.get_name idx n,
+                 Idx.get_term idx i,
+                 Idx.get_term idx j ))
 
         let ind ~n_params ~nidx ~tyidx ~intros ~univ_params : unit =
           let name = Idx.get_name idx nidx in
-          let ty = Idx.get_term idx tyidx in
+          let ty = Lean_elab.elab_top (Idx.get_term idx tyidx) in
           let cstors =
             List.map
               (fun (i, j) ->
                 {
                   Inductive.c_name = Idx.get_name idx i;
-                  c_ty = Idx.get_term idx j;
+                  c_ty = Lean_elab.elab_top (Idx.get_term idx j);
                 })
               intros
           in
@@ -157,12 +168,18 @@ let process_files ~max_err (files : string list) : unit =
 
           let spec = { Inductive.name; ty; n_params; univ_params; cstors } in
 
-          Fmt.eprintf "@[<2>@{<Green>Ind@}@ %a@]@." Inductive.pp_spec spec;
-          (* TODO: register to the conversion relation *)
-          Fmt.eprintf "is valid: %B@." (Inductive.is_valid spec);
+          if not quiet then (
+            Fmt.eprintf "@[<2>@{<Green>Ind@}@ %a@]@." Inductive.pp_spec spec;
+            (* TODO: register to the conversion relation *)
+            Fmt.eprintf "is valid: %B@." (Inductive.is_valid spec)
+          );
           ()
 
-        let after_line () = Fmt.eprintf "%a@." Idx.dump idx
+        let after_line () =
+          if quiet then (
+            if !n_lines mod 1000 = 0 then Fmt.eprintf "\rlines: %d%!" !n_lines
+          ) else
+            Fmt.eprintf "%a@." Idx.dump idx
       end)
   in
 
@@ -179,6 +196,7 @@ let process_files ~max_err (files : string list) : unit =
 let () =
   let files = ref [] in
   let max_err = ref max_int in
+  let quiet = ref false in
   let opts =
     [
       "--debug", Arg.Int Log.set_debug, " set debug level";
@@ -192,6 +210,10 @@ let () =
       ( "-nc",
         Arg.Unit (fun () -> CCFormat.set_color_default false),
         " disable colors" );
+      ( "-q",
+        Arg.Set quiet,
+        " quiet: suppress verbose output, show progress every 1000 lines" );
+      "--quiet", Arg.Set quiet, " like -q";
     ]
     |> Arg.align
   in
@@ -199,4 +221,4 @@ let () =
   Arg.parse opts (CCList.Ref.push files) "leancheck file+";
   if !files = [] then failwith "provide at least one file";
 
-  process_files ~max_err:!max_err (List.rev !files)
+  process_files ~max_err:!max_err ~quiet:!quiet (List.rev !files)