feat: add sidekick.cic_lib with non-hashconsed terms

this should be lighter and closer to Lean's proof format,
where terms don't carry their type, and DB indices are not typed
except from the context.

src/ciclib/bvar.ml

@@ -0,0 +1,9 @@
+open Types_
+
+type t = bvar = { bv_idx: int }
+
+let equal (v1 : t) v2 = v1.bv_idx = v2.bv_idx
+let hash v = H.combine2 10 (H.int v.bv_idx)
+let pp out v = Fmt.fprintf out "bv[%d]" v.bv_idx
+let[@inline] idx self = self.bv_idx
+let make i : t = { bv_idx = i }

src/ciclib/bvar.mli

@@ -0,0 +1,10 @@
+(** Bound variable *)
+
+open Types_
+
+type t = bvar = { bv_idx: int }
+
+include EQ_HASH_PRINT with type t := t
+
+val make : int -> t
+val idx : t -> int

src/ciclib/const.ml

@@ -0,0 +1,8 @@
+open Types_
+
+type t = const = { c_name: string; c_ty: term }
+
+let[@inline] name self = self.c_name
+let[@inline] ty self = self.c_ty
+let pp out (a : t) = Fmt.string out a.c_name
+let make c_name ~ty:c_ty : t = { c_name; c_ty }

src/ciclib/const.mli

@@ -0,0 +1,13 @@
+(** Constants.
+
+  Constants are logical symbols, defined by the user thanks to an open type *)
+
+open Types_
+
+type t = const
+
+val name : t -> string
+val make : string -> ty:term -> t
+val ty : t -> term
+
+include PRINT with type t := t

src/ciclib/dune

@@ -0,0 +1,7 @@
+(library
+ (name sidekick_cic_lib)
+ (public_name sidekick.cic-lib)
+ (synopsis "CiC checker, for the Lean logic")
+ (private_modules types_)
+ (flags :standard -w +32 -open Sidekick_sigs -open Sidekick_util)
+ (libraries containers iter sidekick.sigs sidekick.util))

src/ciclib/level.ml

@@ -0,0 +1,174 @@
+open Types_
+
+type t = level =
+  | L_zero
+  | L_succ of level
+  | L_var of string  (** variable *)
+  | L_max of level * level  (** max *)
+  | L_imax of level * level  (** impredicative max. *)
+
+let rec equal (a : t) (b : t) : bool =
+  match a, b with
+  | L_zero, L_zero -> true
+  | L_succ a, L_succ b -> equal a b
+  | L_var a, L_var b -> String.equal a b
+  | L_imax (a1, a2), L_imax (b1, b2) | L_max (a1, a2), L_max (b1, b2) ->
+    equal a1 b1 && equal a2 b2
+  | (L_zero | L_succ _ | L_var _ | L_max _ | L_imax _), _ -> false
+
+let as_offset (self : t) : t * int =
+  let rec loop n l =
+    match l with
+    | L_succ a -> loop (n + 1) a
+    | _ -> l, n
+  in
+  loop 0 self
+
+let rec pp out (self : t) : unit =
+  let lvl, offset = as_offset self in
+  let pp_offset out () = if offset > 0 then Fmt.fprintf out " + %d" offset in
+  match lvl with
+  | L_zero -> Fmt.int out offset
+  | L_succ _ -> assert false
+  | L_var v -> Fmt.fprintf out "%s%a" v pp_offset ()
+  | L_max (a, b) -> Fmt.fprintf out "max(%a, %a)%a" pp a pp b pp_offset ()
+  | L_imax (a, b) -> Fmt.fprintf out "imax(%a, %a)%a" pp a pp b pp_offset ()
+
+let to_string = Fmt.to_string pp
+
+let rec is_ground (l : t) : bool =
+  match l with
+  | L_zero -> true
+  | L_succ a -> is_ground a
+  | L_var _ -> false
+  | L_max (a, b) | L_imax (a, b) -> is_ground a && is_ground b
+
+let zero : t = L_zero
+let[@inline] succ t : t = L_succ t
+let[@inline] one = succ zero
+let[@inline] var n : t = L_var n
+
+let rec max a b : t =
+  if equal a b then
+    a
+  else (
+    match a, b with
+    | L_succ a', L_succ b' -> succ (max a' b')
+    | L_zero, _ -> b
+    | _, L_zero -> a
+    | _ ->
+      (* normalize wrt commutativity *)
+      let a, b =
+        if compare a b > 0 then
+          b, a
+        else
+          a, b
+      in
+      L_max (a, b)
+  )
+
+let rec imax a b : t =
+  if equal a b then
+    a
+  else (
+    match a, b with
+    | _, L_zero -> zero (* imax(_, 0) = 0 *)
+    | L_succ a', L_succ b' -> succ (imax a' b')
+    | _, L_succ _ -> max a b (* imax(, S_) is just max *)
+    | L_zero, _ -> b
+    | _ -> L_imax (a, b)
+  )
+
+let of_int i : t =
+  assert (i >= 0);
+  let rec loop i =
+    if i = 0 then
+      zero
+    else
+      succ @@ loop (i - 1)
+  in
+  loop i
+
+let[@inline] is_zero l =
+  match l with
+  | L_zero -> true
+  | _ -> false
+
+(** [subst_v store lvl v u] replaces [v] with [u] in [lvl] *)
+let subst_v (lvl : t) (v : string) (u : t) =
+  let rec loop lvl : t =
+    if is_ground lvl then
+      lvl
+    else (
+      match lvl with
+      | L_var v' when v = v' -> u
+      | L_var _ -> lvl
+      | L_zero -> assert false
+      | L_succ a -> succ (loop a)
+      | L_max (a, b) -> max (loop a) (loop b)
+      | L_imax (a, b) -> imax (loop a) (loop b)
+    )
+  in
+  loop lvl
+
+let is_one l =
+  match l with
+  | L_succ a -> is_zero a
+  | _ -> false
+
+let as_int self : _ option =
+  let lvl, offset = as_offset self in
+  if is_zero lvl then
+    Some offset
+  else
+    None
+
+let is_int self : bool = Option.is_some (as_int self)
+
+let judge_leq l1 l2 : bool =
+  (* [l <= l' + n] *)
+  let rec prove (l : t) (l' : t) n : bool =
+    (* replace [v] as [0] and [succ v], prove in both cases *)
+    let split_on_var (v : string) =
+      (let v' = zero in
+       prove (subst_v l v v') (subst_v l' v v') n)
+      &&
+      let v' = succ (var v) in
+      prove (subst_v l v v') (subst_v l' v v') n
+    in
+
+    match l, l' with
+    | _ when equal l l' && n >= 0 -> true
+    | L_zero, L_zero -> n >= 0
+    | L_zero, _ when n >= 0 -> true
+    | _, L_zero when n < 0 -> false
+    | L_var v, L_var v' -> String.equal v v' && n >= 0
+    | L_var _, L_zero -> false (* can instantiate var high enough to refute *)
+    | L_zero, L_var _ -> n >= 0
+    | L_succ l, _ -> prove l l' (n - 1)
+    | _, L_succ l' -> prove l l' (n + 1)
+    | _, L_max (l1, l2) -> prove l l1 n || prove l l2 n
+    | L_max (l1, l2), _ -> prove l1 l' n && prove l2 l' n
+    | L_imax (_, L_var v), _ | _, L_imax (_, L_var v) ->
+      (* imax containing var? split *)
+      split_on_var v
+    | L_imax (l1, L_imax (l2, l3)), _ ->
+      prove (max (imax l1 l3) (imax l2 l3)) l' n
+    | _, L_imax (l1, L_imax (l2, l3)) ->
+      prove l (max (imax l1 l3) (imax l2 l3)) n
+    | L_imax (l1, L_max (l2, l3)), _ ->
+      prove (max (imax l1 l2) (imax l1 l3)) l' n
+    | _, L_imax (l1, L_max (l2, l3)) ->
+      prove l (max (imax l1 l2) (imax l1 l3)) n
+    | L_imax (_, (L_zero | L_succ _)), _ | _, L_imax (_, (L_zero | L_succ _)) ->
+      assert false (* smart cstor makes this impossible *)
+  in
+
+  equal l1 l2
+  ||
+  let l2, n = as_offset l2 in
+  prove l1 l2 n
+
+let judge_eq l1 l2 : bool = equal l1 l2 || (judge_leq l1 l2 && judge_leq l2 l1)
+let judge_is_zero l : bool = judge_leq l zero
+let judge_is_nonzero l : bool = judge_leq one l

src/ciclib/level.mli

@@ -0,0 +1,49 @@
+open Types_
+
+type t = level =
+  | L_zero
+  | L_succ of level
+  | L_var of string  (** variable *)
+  | L_max of level * level  (** max *)
+  | L_imax of level * level  (** impredicative max. *)
+
+include Sidekick_sigs.PRINT with type t := t
+
+val to_string : t -> string
+
+val as_offset : t -> t * int
+(** [as_offset lvl] returns a pair [lvl' + n]. *)
+
+val zero : t
+val one : t
+val var : string -> t
+val succ : t -> t
+val of_int : int -> t
+val max : t -> t -> t
+val imax : t -> t -> t
+
+(** {2 helpers} *)
+
+val is_zero : t -> bool
+val is_one : t -> bool
+val is_int : t -> bool
+val as_int : t -> int option
+
+(** {2 Judgements}
+
+    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] *)
+
+val judge_eq : t -> t -> bool
+(** [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 *)
+
+val judge_is_nonzero : t -> bool
+(** [judge_is_nonzero st l] is [true] iff [1 <= l] holds *)

src/ciclib/sidekick_cic_lib.ml

@@ -0,0 +1,4 @@
+module Term = Term
+module Bvar = Bvar
+module Const = Const
+module Level = Level

src/ciclib/term.ml

@@ -0,0 +1,241 @@
+open Types_
+
+type bvar = Bvar.t
+type nonrec term = term
+
+type view = term_view =
+  | E_type of level
+  | E_bound_var of bvar
+  | E_const of const
+  | E_app of term * term
+  | E_lam of term * term
+  | E_pi of term * term
+
+type t = term
+
+(* mask to access the store id *)
+let[@inline] view (e : term) : view = e.view
+let[@inline] db_depth e = e.flags
+let[@inline] is_closed e : bool = db_depth e == 0
+
+(* open an application *)
+let[@inline] unfold_app (e : term) : term * term list =
+  let[@unroll 1] rec aux acc e =
+    match e.view with
+    | E_app (f, a) -> aux (a :: acc) f
+    | _ -> e, acc
+  in
+  aux [] e
+
+let[@inline] is_const e =
+  match e.view with
+  | E_const _ -> true
+  | _ -> false
+
+let[@inline] is_app e =
+  match e.view with
+  | E_app _ -> true
+  | _ -> false
+
+let[@inline] is_pi e =
+  match e.view with
+  | E_pi _ -> true
+  | _ -> false
+
+let as_type e : level option =
+  match e.view with
+  | E_type l -> Some l
+  | _ -> None
+
+(* debug printer *)
+let expr_pp_with_ ~max_depth out (e : term) : unit =
+  let rec loop k ~depth names out e =
+    let pp' = loop k ~depth:(depth + 1) names in
+    match e.view with
+    | E_type lvl when Level.is_one lvl -> Fmt.string out "Type"
+    | E_type lvl -> Fmt.fprintf out "Type.{%a}" Level.pp lvl
+    | E_bound_var v ->
+      let idx = v.bv_idx in
+      (match CCList.nth_opt names idx with
+      | Some n when n <> "" -> Fmt.fprintf out "%s[%d]" n idx
+      | _ -> Fmt.fprintf out "_[%d]" idx)
+    | E_const c -> Const.pp out c
+    | (E_app _ | E_lam _) when depth > max_depth -> Fmt.fprintf out "@<1>…"
+    | E_app _ ->
+      let f, args = unfold_app e in
+      Fmt.fprintf out "(%a@ %a)" pp' f (Util.pp_list pp') args
+    | E_lam (_ty, bod) ->
+      Fmt.fprintf out "(@[\\_:@[%a@].@ %a@])" pp' _ty
+        (loop (k + 1) ~depth:(depth + 1) ("" :: names))
+        bod
+    | E_pi (ty_arg, bod) ->
+      Fmt.fprintf out "(@[Pi _:@[%a@].@ %a@])" pp' ty_arg
+        (loop (k + 1) ~depth:(depth + 1) ("" :: names))
+        bod
+  in
+  Fmt.fprintf out "@[%a@]" (loop 0 ~depth:0 []) e
+
+let pp_debug = expr_pp_with_ ~max_depth:max_int
+
+let as_type_exn e : level =
+  match e.view with
+  | E_type l -> l
+  | _ -> Error.errorf "Term.as_type_exn: `%a` is not a type" pp_debug e
+
+let iter_shallow ~f (e : term) : unit =
+  match e.view with
+  | E_type _ -> ()
+  | _ ->
+    (match e.view with
+    | E_const _ -> ()
+    | E_type _ -> assert false
+    | E_bound_var _ -> ()
+    | E_app (hd, a) ->
+      f false hd;
+      f false a
+    | E_lam (tyv, bod) | E_pi (tyv, bod) ->
+      f false tyv;
+      f true bod)
+
+let[@inline] is_type e =
+  match e.view with
+  | E_type _ -> true
+  | _ -> false
+
+exception E_exit
+
+let exists_shallow ~f e : bool =
+  try
+    iter_shallow e ~f:(fun b x -> if f b x then raise_notrace E_exit);
+    false
+  with E_exit -> true
+
+let for_all_shallow ~f e : bool =
+  try
+    iter_shallow e ~f:(fun b x -> if not (f b x) then raise_notrace E_exit);
+    true
+  with E_exit -> false
+
+let compute_db_depth_ e : int =
+  if is_type e then
+    0
+  else (
+    let d =
+      match view e with
+      | E_type _ | E_const _ -> 0
+      | E_bound_var v -> v.bv_idx + 1
+      | E_app (a, b) -> max (db_depth a) (db_depth b)
+      | E_lam (ty, bod) | E_pi (ty, bod) ->
+        max (db_depth ty) (max 0 (db_depth bod - 1))
+    in
+    d
+  )
+
+let make_ view : term =
+  let e = { view; flags = 0 } in
+  let flags = compute_db_depth_ e in
+  e.flags <- flags;
+  e
+
+let map_shallow ~f (e : term) : term =
+  match view e with
+  | E_type _ | E_const _ | E_bound_var _ -> e
+  | E_app (hd, a) ->
+    let hd' = f false hd in
+    let a' = f false a in
+    if a == a' && hd == hd' then
+      e
+    else
+      make_ (E_app (f false hd, f false a))
+  | E_lam (tyv, bod) ->
+    let tyv' = f false tyv in
+    let bod' = f true bod in
+    if tyv == tyv' && bod == bod' then
+      e
+    else
+      make_ (E_lam (tyv', bod'))
+  | E_pi (tyv, bod) ->
+    let tyv' = f false tyv in
+    let bod' = f true bod in
+    if tyv == tyv' && bod == bod' then
+      e
+    else
+      make_ (E_pi (tyv', bod'))
+
+(* shift open bound variables of [e] by [n] *)
+let db_shift_ ~make (e : term) (n : int) =
+  let rec loop e k : term =
+    if is_closed e then
+      e
+    else if is_type e then
+      e
+    else (
+      match view e with
+      | E_bound_var bv ->
+        if bv.bv_idx >= k then
+          make (E_bound_var (Bvar.make (bv.bv_idx + n)))
+        else
+          e
+      | _ ->
+        map_shallow e ~f:(fun inbind u ->
+            loop u
+              (if inbind then
+                k + 1
+              else
+                k))
+    )
+  in
+  assert (n >= 0);
+  if n = 0 || is_closed e then
+    e
+  else
+    loop e 0
+
+(* replace DB0 in [e] with [u] *)
+let db_0_replace_ ~make e ~by:u : term =
+  (* recurse in subterm [e], under [k] intermediate binders (so any
+     bound variable under k is bound by them) *)
+  let rec aux e k : term =
+    if is_type e then
+      e
+    else if db_depth e < k then
+      e
+    else (
+      match view e with
+      | E_const _ -> e
+      | E_bound_var bv when bv.bv_idx = k ->
+        (* replace [bv] with [u], and shift [u] to account for the
+           [k] intermediate binders we traversed to get to [bv] *)
+        db_shift_ ~make u k
+      | _ ->
+        map_shallow e ~f:(fun inb u ->
+            aux u
+              (if inb then
+                k + 1
+              else
+                k))
+    )
+  in
+  if is_closed e then
+    e
+  else
+    aux e 0
+
+let type_of_univ lvl : term = make_ (E_type lvl)
+let type_of_univ_int i : term = type_of_univ (Level.of_int i)
+let type_ : term = type_of_univ Level.one
+let bvar v : term = make_ (E_bound_var v)
+let bvar_i i : term = make_ (E_bound_var (Bvar.make i))
+let const c : term = make_ (E_const c)
+let app f a = make_ (E_app (f, a))
+let app_l f l = List.fold_left app f l
+let lam ~var_ty bod : term = make_ (E_lam (var_ty, bod))
+let pi ~var_ty bod : term = make_ (E_pi (var_ty, bod))
+
+module DB = struct
+  let subst_db0 e ~by : t = db_0_replace_ ~make:make_ e ~by
+
+  let shift t ~by : t =
+    assert (by >= 0);
+    db_shift_ ~make:make_ t by
+end

src/ciclib/term.mli

@@ -0,0 +1,86 @@
+(** 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).
+
+  It is intended to be the foundation for user-level terms and types and formulas.
+*)
+
+open Types_
+
+type bvar = Bvar.t
+type nonrec term = term
+
+type t = term
+(** A term, in the calculus of constructions *)
+
+(** View.
+
+    A view is the shape of the root node of a term. *)
+type view = term_view =
+  | E_type of level
+  | E_bound_var of bvar
+  | E_const of const
+  | E_app of t * t
+  | E_lam of t * t
+  | E_pi of t * t
+
+val pp_debug : t Fmt.printer
+
+(** {2 Utils} *)
+
+val view : t -> view
+val unfold_app : t -> t * t list
+val is_app : t -> bool
+val is_const : t -> bool
+val is_pi : t -> bool
+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. *)
+
+val map_shallow : f:(bool -> t -> t) -> t -> t
+val exists_shallow : f:(bool -> t -> bool) -> t -> bool
+val for_all_shallow : f:(bool -> t -> bool) -> t -> bool
+
+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) *)
+
+(** {2 Creation} *)
+
+val type_ : t
+val type_of_univ : level -> t
+val type_of_univ_int : int -> t
+val bvar : bvar -> t
+val bvar_i : int -> t
+val const : const -> t
+val app : t -> t -> t
+val app_l : t -> t list -> t
+val lam : var_ty:t -> t -> t
+val pi : var_ty:t -> 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.
+
+      For example, with [t] being [_[0] = (\x. _[2] _[1] x[0])],
+      [subst_db0 store t ~by:"hello"] is ["hello" = (\x. _[2] "hello" x[0])].
+  *)
+
+  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).
+
+      For example, with term [t] being [\x. _[1] _[2] x[0]],
+      [shift t ~by:5] is [\x. _[6] _[7] x[0]]. *)
+end

src/ciclib/types_.ml

@@ -0,0 +1,25 @@
+module H = CCHash
+
+(** A level expression *)
+type level =
+  | L_zero
+  | L_succ of level
+  | L_var of string  (** variable *)
+  | L_max of level * level  (** max *)
+  | L_imax of level * level  (** impredicative max. *)
+
+type term_view =
+  | E_type of level
+  | E_bound_var of bvar
+  | E_const of const
+  | E_app of term * term
+  | E_lam of term * term
+  | E_pi of term * term
+
+and bvar = { bv_idx: int }
+and const = { c_name: string; c_ty: term }
+
+and term = {
+  view: term_view;
+  mutable flags: int;  (** contains: [highest DB var | 1:has free vars] *)
+}

src/leancheck/dune

@@ -1,4 +1,4 @@
 (executable
  (name leancheck)
  (flags :standard -w +32 -open Sidekick_sigs -open Sidekick_util)
- (libraries containers sidekick.core-logic sidekick.util mtime mtime.clock.os))
+ (libraries containers sidekick.cic-lib sidekick.util mtime mtime.clock.os))

src/leancheck/leancheck.ml

@@ -1,5 +1,5 @@
-module T = Sidekick_core_logic.Term
-module Level = Sidekick_core_logic.Level
+module T = Sidekick_cic_lib.Term
+module Level = Sidekick_cic_lib.Level
 
 let ( let@ ) = ( @@ )
 
@@ -78,8 +78,6 @@ let name_join a b =
 
 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);
@@ -89,7 +87,7 @@ let process_files ~max_err (files : string list) : unit =
   (* get a level. 0 means level 0. *)
   let get_level idx i =
     if i = 0 then
-      Level.zero lvl_st
+      Level.zero
     else
       Idx.get_level idx i
   in
@@ -109,18 +107,16 @@ let process_files ~max_err (files : string list) : 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)
+          Idx.set_level idx at (Level.succ @@ 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))
+          Idx.set_level idx at (Level.max (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))
+          Idx.set_level idx at (Level.imax (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)
+          Idx.set_level idx at (Level.var @@ Idx.get_name idx i)
       end)
   in