gitignore

.gitignore

@@ -18,3 +18,4 @@ perf.*
 *.gz
 .git-blame-ignore-revs
 *.json
+*.tmp

.ocamlformat

@@ -1,4 +1,4 @@
-version = 0.26.2
+version = 0.27.0
 profile=conventional
 margin=80
 if-then-else=k-r

Makefile

@@ -30,6 +30,12 @@ test:
 test-promote:
 	@dune runtest $(OPTS) --force --no-buffer --auto-promote
 
+format:
+	@dune build @fmt --auto-promote
+
+format-check:
+	@dune build @fmt --quiet
+
 TESTOPTS ?= -j $(J) -c tests/benchpress.sexp --progress
 TESTTOOL=benchpress
 DATE=$(shell date +%FT%H:%M)

src/ciclib/const.mli

@@ -1,6 +1,6 @@
 (** Constants.
 
-  Constants are logical symbols, defined by the user thanks to an open type *)
+    Constants are logical symbols, defined by the user thanks to an open type *)
 
 open Types_
 

src/ciclib/level.mli

@@ -39,16 +39,15 @@ val subst : subst -> t -> t
 
 (** {2 Judgements}
 
-    These are little proofs of some symbolic properties of levels, even
-    those which contain variables. *)
+    These are little proofs of some symbolic properties of levels, even those
+    which contain variables. *)
 
 val judge_leq : t -> t -> bool
-(** [judge_leq st l1 l2] is [true] if [l1] is proven to be lower
-    or equal to [l2] *)
+(** [judge_leq st l1 l2] is [true] if [l1] is proven to be lower or equal to
+    [l2] *)
 
 val judge_eq : t -> t -> bool
-(** [judge_eq st l1 l2] is [true] iff [judge_leq l1 l2]
-    and [judge_leq l2 l1] *)
+(** [judge_eq st l1 l2] is [true] iff [judge_leq l1 l2] and [judge_leq l2 l1] *)
 
 val judge_is_zero : t -> bool
 (** [judge_is_zero st l] is [true] iff [l <= 0] holds *)

src/ciclib/term.ml

@@ -190,9 +190,9 @@ let db_shift_ (e : term) (n : int) =
         map_shallow e ~f:(fun inbind u ->
             loop u
               (if inbind then
-                k + 1
-              else
-                k))
+                 k + 1
+               else
+                 k))
     )
   in
   assert (n >= 0);
@@ -225,9 +225,9 @@ let db_replace_ e (env : t list) : term =
         map_shallow e ~f:(fun inb u ->
             aux u
               (if inb then
-                k + 1
-              else
-                k))
+                 k + 1
+               else
+                 k))
     )
   in
   if is_closed e then

src/ciclib/term.mli

@@ -1,11 +1,11 @@
 (** Core logic terms.
 
-  The core terms are expressions in the calculus of constructions,
-  with no universe polymorphism nor cumulativity. It should be fast, with hashconsing;
-  and simple enough (no inductives, no universe trickery).
+    The core terms are expressions in the calculus of constructions, with no
+    universe polymorphism nor cumulativity. It should be fast, with hashconsing;
+    and simple enough (no inductives, no universe trickery).
 
-  It is intended to be the foundation for user-level terms and types and formulas.
-*)
+    It is intended to be the foundation for user-level terms and types and
+    formulas. *)
 
 open Types_
 
@@ -41,9 +41,9 @@ val as_type : t -> Level.t option
 val as_type_exn : t -> Level.t
 
 val iter_shallow : f:(bool -> t -> unit) -> t -> unit
-(** [iter_shallow f e] iterates on immediate subterms of [e],
-    calling [f trdb e'] for each subterm [e'], with [trdb = true] iff
-    [e'] is directly under a binder. *)
+(** [iter_shallow f e] iterates on immediate subterms of [e], calling
+    [f trdb e'] for each subterm [e'], with [trdb = true] iff [e'] is directly
+    under a binder. *)
 
 val map_shallow : f:(bool -> t -> t) -> t -> t
 val exists_shallow : f:(bool -> t -> bool) -> t -> bool
@@ -53,8 +53,8 @@ val is_type : t -> bool
 (** [is_type t] is true iff [view t] is [Type _] *)
 
 val is_closed : t -> bool
-(** Is the term closed (all bound variables are paired with a binder)?
- time: O(1) *)
+(** Is the term closed (all bound variables are paired with a binder)? time:
+    O(1) *)
 
 (** {2 Creation} *)
 
@@ -75,8 +75,8 @@ val subst_level : Level.subst -> t -> t
 (** De bruijn indices *)
 module DB : sig
   val subst_db0 : t -> by:t -> t
-  (** [subst_db0 store t ~by] replaces bound variable 0 in [t] with
-      the term [by]. This is useful, for example, to implement beta-reduction.
+  (** [subst_db0 store t ~by] replaces bound variable 0 in [t] with the term
+      [by]. This is useful, for example, to implement beta-reduction.
 
       For example, with [t] being [_[0] = (\x. _[2] _[1] x[0])],
       [subst_db0 store t ~by:"hello"] is ["hello" = (\x. _[2] "hello" x[0])]. *)
@@ -84,9 +84,9 @@ module DB : sig
   val subst_db_l : t -> t list -> t
 
   val shift : t -> by:int -> t
-  (** [shift t ~by] shifts all bound variables in [t] that are not
-      closed on, by amount [by] (which must be >= 0).
+  (** [shift t ~by] shifts all bound variables in [t] that are not closed on, by
+      amount [by] (which must be >= 0).
 
-      For example, with term [t] being [\x. _[1] _[2] x[0]],
-      [shift t ~by:5] is [\x. _[6] _[7] x[0]]. *)
+      For example, with term [t] being [\x. _[1] _[2] x[0]], [shift t ~by:5] is
+      [\x. _[6] _[7] x[0]]. *)
 end

src/core-logic/const.ml

@@ -26,5 +26,4 @@ let pp out (a : t) = a.c_ops.pp out a.c_view
 let ser ~ser_t (self : t) = self.c_ops.ser ser_t self.c_view
 let make c_view c_ops ~ty:c_ty : t = { c_view; c_ops; c_ty }
 
-type decoders =
-  (string * Ops.t * (term Ser_decode.t -> view Ser_decode.t)) list
+type decoders = (string * Ops.t * (term Ser_decode.t -> view Ser_decode.t)) list

src/core-logic/const.mli

@@ -1,6 +1,6 @@
 (** Constants.
 
-  Constants are logical symbols, defined by the user thanks to an open type *)
+    Constants are logical symbols, defined by the user thanks to an open type *)
 
 open Types_
 
@@ -24,10 +24,8 @@ val make : view -> Ops.t -> ty:term -> t
 val ser : ser_t:(term -> Ser_value.t) -> t -> string * Ser_value.t
 val ty : t -> term
 
-type decoders =
-  (string * Ops.t * (term Ser_decode.t -> view Ser_decode.t)) list
-(** Decoders for constants: given a term store, return a list
-    of supported tags, and for each tag, a decoder for constants
-    that have this particular tag. *)
+type decoders = (string * Ops.t * (term Ser_decode.t -> view Ser_decode.t)) list
+(** Decoders for constants: given a term store, return a list of supported tags,
+    and for each tag, a decoder for constants that have this particular tag. *)
 
 include EQ_HASH_PRINT with type t := t

src/core-logic/level.mli

@@ -42,16 +42,15 @@ val as_int : t -> int option
 
 (** {2 Judgements}
 
-    These are little proofs of some symbolic properties of levels, even
-    those which contain variables. *)
+    These are little proofs of some symbolic properties of levels, even those
+    which contain variables. *)
 
 val judge_leq : store -> t -> t -> bool
-(** [judge_leq st l1 l2] is [true] if [l1] is proven to be lower
-    or equal to [l2] *)
+(** [judge_leq st l1 l2] is [true] if [l1] is proven to be lower or equal to
+    [l2] *)
 
 val judge_eq : store -> t -> t -> bool
-(** [judge_eq st l1 l2] is [true] iff [judge_leq l1 l2]
-    and [judge_leq l2 l1] *)
+(** [judge_eq st l1 l2] is [true] iff [judge_leq l1 l2] and [judge_leq l2 l1] *)
 
 val judge_is_zero : store -> t -> bool
 (** [judge_is_zero st l] is [true] iff [l <= 0] holds *)

src/core-logic/reduce.ml

@@ -0,0 +1,85 @@
+open Types_
+module T = Term
+
+(* Pair-keyed table for def_eq cache *)
+module T2_tbl = CCHashtbl.Make (struct
+  type t = term * term
+
+  let equal (a1, b1) (a2, b2) = T.equal a1 a2 && T.equal b1 b2
+  let hash (a, b) = CCHash.combine3 91 (T.hash a) (T.hash b)
+end)
+
+(** Weak head normal form. Beta-reduces at the head until stuck. Memoised via
+    [cache]. *)
+let whnf ?(cache = T.Tbl.create 16) store e =
+  let rec loop e =
+    match T.Tbl.find_opt cache e with
+    | Some v -> v
+    | None ->
+      let v = step e in
+      T.Tbl.add cache e v;
+      v
+  and step e =
+    match T.view e with
+    | E_app (f, a) ->
+      let f' = loop f in
+      (match T.view f' with
+      | E_lam (_, _, body) -> loop (T.DB.subst_db0 store body ~by:a)
+      | _ ->
+        if f == f' then
+          e
+        else
+          T.app store f' a)
+    | _ -> e
+  in
+  loop e
+
+(** Definitional equality: WHNF both sides, then compare structurally. Uses
+    [Level.judge_eq] for universe levels. Memoised via pair cache to handle
+    sharing in DAGs. *)
+let def_eq store e1 e2 =
+  let whnf_cache = T.Tbl.create 16 in
+  let eq_cache : bool T2_tbl.t = T2_tbl.create 16 in
+  let whnf = whnf ~cache:whnf_cache store in
+
+  let rec go e1 e2 =
+    if T.equal e1 e2 then
+      true
+    else (
+      (* canonical order to halve cache size *)
+      let key =
+        if T.compare e1 e2 <= 0 then
+          e1, e2
+        else
+          e2, e1
+      in
+      match T2_tbl.find_opt eq_cache key with
+      | Some b -> b
+      | None ->
+        (* assume true while recursing (for coinductive guard on open terms) *)
+        T2_tbl.add eq_cache key true;
+        let r = check e1 e2 in
+        T2_tbl.replace eq_cache key r;
+        r
+    )
+  and check e1 e2 =
+    let e1 = whnf e1 in
+    let e2 = whnf e2 in
+    if T.equal e1 e2 then
+      true
+    else (
+      match T.view e1, T.view e2 with
+      | E_type l1, E_type l2 -> Level.judge_eq (T.Store.lvl_store store) l1 l2
+      | E_var v1, E_var v2 -> Var.equal v1 v2
+      | E_const c1, E_const c2 -> Const.equal c1 c2
+      | E_bound_var b1, E_bound_var b2 -> Bvar.equal b1 b2
+      | E_app (f1, a1), E_app (f2, a2) -> go f1 f2 && go a1 a2
+      | E_lam (_, ty1, b1), E_lam (_, ty2, b2) -> go ty1 ty2 && go b1 b2
+      | E_pi (_, ty1, b1), E_pi (_, ty2, b2) -> go ty1 ty2 && go b1 b2
+      | _ -> false
+    )
+  in
+  go e1 e2
+
+(* Install into the kernel *)
+let () = T.Internal_.def_eq_ref := def_eq

src/core-logic/reduce.mli

@@ -0,0 +1,13 @@
+val whnf : ?cache:Term.t Term.Tbl.t -> Term.store -> Term.t -> Term.t
+(** [whnf store e] reduces [e] to weak head normal form by beta-reducing at the
+    head until stuck. The optional [cache] is a memoisation table; pass the same
+    table across calls to amortise work over a DAG. *)
+
+val def_eq : Term.store -> Term.t -> Term.t -> bool
+(** [def_eq store a b] is true iff [a] and [b] are definitionally equal: both
+    sides are reduced to WHNF and then compared structurally, using
+    [Level.judge_eq] for universe levels. Results are memoised internally on the
+    shared DAG structure.
+
+    Note: this is installed as the kernel's equality check
+    ([Term.Internal_.def_eq_ref]) when this module is loaded. *)

src/core-logic/sidekick_core_logic.ml

@@ -6,6 +6,7 @@ module Subst = Subst
 module T_builtins = T_builtins
 module Store = Term.Store
 module Level = Level
+module Reduce = Reduce
 
 (* TODO: move to separate library? *)
 module Str_const = Str_const

src/core-logic/str_const.mli

@@ -1,7 +1,6 @@
 (** Basic string constants.
 
-   These constants are a string name, coupled with a type.
-*)
+    These constants are a string name, coupled with a type. *)
 
 open Types_
 

src/core-logic/t_builtins.mli

@@ -27,12 +27,12 @@ val is_eq : t -> bool
 val is_bool : t -> bool
 
 val abs : store -> t -> bool * t
-(** [abs t] returns an "absolute value" for the term, along with the
-    sign of [t].
+(** [abs t] returns an "absolute value" for the term, along with the sign of
+    [t].
 
-    The idea is that we want to turn [not a] into [(false, a)],
-    or [(a != b)] into [(false, a=b)]. For terms without a negation this
-    should return [(true, t)]. *)
+    The idea is that we want to turn [not a] into [(false, a)], or [(a != b)]
+    into [(false, a=b)]. For terms without a negation this should return
+    [(true, t)]. *)
 
 val as_bool_val : t -> bool option
 

src/core-logic/term.ml

@@ -404,9 +404,9 @@ module Make_ = struct
           map_shallow_ e ~make ~f:(fun inbind u ->
               loop u
                 (if inbind then
-                  k + 1
-                else
-                  k))
+                   k + 1
+                 else
+                   k))
       )
     in
     assert (n >= 0);
@@ -441,9 +441,9 @@ module Make_ = struct
                map_shallow_ e ~make ~f:(fun inb u ->
                    aux u
                      (if inb then
-                       k + 1
-                     else
-                       k))
+                        k + 1
+                      else
+                        k))
              in
              T_int_tbl.add cache_ (e, k) r;
              r)
@@ -454,8 +454,11 @@ module Make_ = struct
     else
       aux e 0
 
-  (* TODO: have beta-reduction here; level checking; and pluggable reduction
-     rules (in the store) so we can reduce quotients and recursors *)
+  (* Definitional equality: installed by Reduce, defaults to syntactic equality *)
+  let def_eq_ref : (store -> term -> term -> bool) ref =
+    ref (fun _ a b -> equal a b)
+
+  (* TODO: pluggable reduction rules (in the store) for quotients and recursors *)
 
   (** compute the type of [view]. *)
   let compute_ty_ (self : store) ~make (view : view) : term =
@@ -485,9 +488,8 @@ module Make_ = struct
       let ty_a = ty a in
       (match ty_f.view with
       | E_pi (_, ty_arg_f, ty_bod_f) ->
-        (* check that the expected type matches *)
-        (* FIXME: replace [equal] with definitional equality *)
-        if not (equal ty_arg_f ty_a) then
+        (* check that the expected type matches, using definitional equality *)
+        if not (!def_eq_ref self ty_arg_f ty_a) then
           Error.errorf
             "@[<2>cannot @[apply `%a`@]@ @[to `%a`@],@ expected argument type: \
              `%a`@ @[actual: `%a`@]@]"
@@ -608,9 +610,9 @@ module Make_ = struct
         map_shallow_ e ~make ~f:(fun inb u ->
             loop
               (if inb then
-                k + 1
-              else
-                k)
+                 k + 1
+               else
+                 k)
               u)
       | Some u ->
         let u = db_shift_ ~make u k in
@@ -718,4 +720,6 @@ module Internal_ = struct
 
   let subst_ store ~recursive t subst =
     subst_ ~make:(make_ store) ~recursive t subst
+
+  let def_eq_ref = def_eq_ref
 end

src/core-logic/term.mli

@@ -1,11 +1,11 @@
 (** Core logic terms.
 
-  The core terms are expressions in the calculus of constructions,
-  with no universe polymorphism nor cumulativity. It should be fast, with hashconsing;
-  and simple enough (no inductives, no universe trickery).
+    The core terms are expressions in the calculus of constructions, with no
+    universe polymorphism nor cumulativity. It should be fast, with hashconsing;
+    and simple enough (no inductives, no universe trickery).
 
-  It is intended to be the foundation for user-level terms and types and formulas.
-*)
+    It is intended to be the foundation for user-level terms and types and
+    formulas. *)
 
 open Types_
 
@@ -19,9 +19,9 @@ type t = term
 type store
 (** The store for terms.
 
-    The store is responsible for allocating unique IDs to terms, and
-    enforcing their hashconsing (so that syntactic equality is just a pointer
-    comparison). *)
+    The store is responsible for allocating unique IDs to terms, and enforcing
+    their hashconsing (so that syntactic equality is just a pointer comparison).
+*)
 
 (** View.
 
@@ -61,31 +61,30 @@ val as_type : t -> Level.t option
 val as_type_exn : t -> Level.t
 
 val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:(t -> unit) -> t -> unit
-(** [iter_dag t ~f] calls [f] once on each subterm of [t], [t] included.
-        It must {b not} traverse [t] as a tree, but rather as a
-        perfectly shared DAG.
+(** [iter_dag t ~f] calls [f] once on each subterm of [t], [t] included. It must
+    {b not} traverse [t] as a tree, but rather as a perfectly shared DAG.
 
-        For example, in:
-        {[
-          let x = 2 in
-          let y = f x x in
-          let z = g y x in
-          z = z
-        ]}
+    For example, in:
+    {[
+      let x = 2 in
+      let y = f x x in
+      let z = g y x in
+      z = z
+    ]}
 
-        the DAG has the following nodes:
+    the DAG has the following nodes:
 
-        {[ n1: 2
-           n2: f n1 n1
-           n3: g n2 n1
-           n4: = n3 n3
-         ]}
-    *)
+    {[
+      n1: 2
+      n2: f n1 n1
+      n3: g n2 n1
+      n4: = n3 n3
+    ]} *)
 
 val iter_shallow : f:(bool -> t -> unit) -> t -> unit
-(** [iter_shallow f e] iterates on immediate subterms of [e],
-  calling [f trdb e'] for each subterm [e'], with [trdb = true] iff
-  [e'] is directly under a binder. *)
+(** [iter_shallow f e] iterates on immediate subterms of [e], calling
+    [f trdb e'] for each subterm [e'], with [trdb = true] iff [e'] is directly
+    under a binder. *)
 
 val map_shallow : store -> f:(bool -> t -> t) -> t -> t
 val exists_shallow : f:(bool -> t -> bool) -> t -> bool
@@ -101,12 +100,11 @@ val is_a_type : t -> bool
 (** [is_a_type t] is true if [is_ty (ty t)] *)
 
 val is_closed : t -> bool
-(** Is the term closed (all bound variables are paired with a binder)?
- time: O(1) *)
+(** Is the term closed (all bound variables are paired with a binder)? time:
+    O(1) *)
 
 val has_fvars : t -> bool
-(** Does the term contain free variables?
-  time: O(1)  *)
+(** Does the term contain free variables? time: O(1) *)
 
 val ty : t -> t
 (** Return the type of this term. *)
@@ -142,33 +140,33 @@ val open_lambda_exn : store -> t -> var * t
 (** De bruijn indices *)
 module DB : sig
   val lam_db : ?var_name:string -> store -> var_ty:t -> t -> t
-  (** [lam_db store ~var_ty bod] is [\ _:var_ty. bod]. Not DB shifting is done. *)
+  (** [lam_db store ~var_ty bod] is [\ _:var_ty. bod]. Not DB shifting is done.
+  *)
 
   val pi_db : ?var_name:string -> store -> var_ty:t -> t -> t
-  (** [pi_db store ~var_ty bod] is [pi _:var_ty. bod]. Not DB shifting is done. *)
+  (** [pi_db store ~var_ty bod] is [pi _:var_ty. bod]. Not DB shifting is done.
+  *)
 
   val subst_db0 : store -> t -> by:t -> t
-  (** [subst_db0 store t ~by] replaces bound variable 0 in [t] with
-      the term [by]. This is useful, for example, to implement beta-reduction.
+  (** [subst_db0 store t ~by] replaces bound variable 0 in [t] with the term
+      [by]. This is useful, for example, to implement beta-reduction.
 
       For example, with [t] being [_[0] = (\x. _[2] _[1] x[0])],
-      [subst_db0 store t ~by:"hello"] is ["hello" = (\x. _[2] "hello" x[0])].
-  *)
+      [subst_db0 store t ~by:"hello"] is ["hello" = (\x. _[2] "hello" x[0])]. *)
 
   val shift : store -> t -> by:int -> t
-  (** [shift store t ~by] shifts all bound variables in [t] that are not
-    closed on, by amount [by] (which must be >= 0).
+  (** [shift store t ~by] shifts all bound variables in [t] that are not closed
+      on, by amount [by] (which must be >= 0).
 
-    For example, with term [t] being [\x. _[1] _[2] x[0]],
-    [shift store t ~by:5] is [\x. _[6] _[7] x[0]]. *)
+      For example, with term [t] being [\x. _[1] _[2] x[0]],
+      [shift store t ~by:5] is [\x. _[6] _[7] x[0]]. *)
 
   val abs_on : store -> var -> t -> t
-  (** [abs_on store v t] is the term [t[v := _[0]]]. It replaces [v] with
-      the bound variable with the same type as [v], and the DB index 0,
-      and takes care of shifting if [v] occurs under binders.
+  (** [abs_on store v t] is the term [t[v := _[0]]]. It replaces [v] with the
+      bound variable with the same type as [v], and the DB index 0, and takes
+      care of shifting if [v] occurs under binders.
 
-      For example, [abs_on store x (\y. x+y)] is [\y. _[1] y].
-  *)
+      For example, [abs_on store x (\y. x+y)] is [\y. _[1] y]. *)
 end
 
 (**/**)
@@ -186,6 +184,10 @@ module Internal_ : sig
     t ->
     f:(recurse:(t -> t) -> t -> t option) ->
     t
+
+  val def_eq_ref : (store -> t -> t -> bool) ref
+  (** Definitional equality hook. Defaults to syntactic equality. Overwritten by
+      [Reduce] at init time. *)
 end
 
 (**/**)

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,26 @@ 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 def ~nidx ~tyidx ~validx ~univ_params : unit =
+          let name = Idx.get_name idx nidx in
+          let _ty = Lean_elab.elab_top (Idx.get_term idx tyidx) in
+          let _val = Lean_elab.elab_top (Idx.get_term idx validx) in
+          let _univ_params = List.map (Idx.get_name idx) univ_params in
+          if not quiet then
+            Fmt.eprintf "@[<2>@{<Blue>Def@}@ %s@]@." name
+
+        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 +204,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 +218,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 +229,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)

src/leancheck/parse.ml

@@ -100,6 +100,15 @@ let parse ?(max_errors = max_int) (input : input) (cb : callback) : unit =
                l
            in
            CB.ind ~n_params ~nidx ~tyidx ~intros ~univ_params
+         | S "#DEF" :: I nidx :: I tyidx :: I validx :: tl ->
+           let univ_params =
+             List.map
+               (function
+                 | I i -> i
+                 | _ -> failwith "invalid param")
+               tl
+           in
+           CB.def ~nidx ~tyidx ~validx ~univ_params
          | _ ->
            incr n_errors;
            Fmt.eprintf "@{<Yellow>warn@}: unhandled line %d: %s@." !n_line line

src/leancheck/parse_intf.ml

@@ -21,4 +21,7 @@ module type CALLBACK = sig
     intros:(int * int) list ->
     univ_params:int list ->
     unit
+
+  val def :
+    nidx:int -> tyidx:int -> validx:int -> univ_params:int list -> unit
 end