feat(core-logic): add level expressions, modify type checker

src/core-logic/level.ml

@@ -0,0 +1,138 @@
+open Types_
+
+type view = level_view =
+  | L_zero
+  | L_succ of level
+  | L_var of string  (** variable *)
+  | L_max of level * level  (** max *)
+  | L_imax of level * level  (** impredicative max. *)
+
+and t = level = { l_view: level_view; mutable l_id: int }
+
+let[@inline] view (self : t) : view = self.l_view
+let[@inline] equal (a : t) (b : t) : bool = a == b
+let[@inline] hash (a : t) : int = Hash.int a.l_id
+let[@inline] compare a b : int = compare a.l_id b.l_id
+
+(* hashconsing *)
+module H_cons = Hashcons.Make (struct
+  type nonrec t = t
+
+  let equal (a : t) (b : t) : bool =
+    a == b
+    ||
+    match view a, view 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 hash a : int =
+    match view a with
+    | L_zero -> Hash.int 1
+    | L_succ a -> Hash.combine2 2 (hash a)
+    | L_var v -> Hash.combine2 3 (Hash.string v)
+    | L_max (a, b) -> Hash.combine3 10 (hash a) (hash b)
+    | L_imax (a, b) -> Hash.combine3 20 (hash a) (hash b)
+
+  let set_id self i =
+    assert (self.l_id = -1);
+    self.l_id <- i
+end)
+
+let as_offset (self : t) : t * int =
+  let rec loop n l =
+    match view 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 view 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
+
+type store = { h_cons: H_cons.t }
+
+module Store = struct
+  type t = store
+
+  let create () : store = { h_cons = H_cons.create ~size:64 () }
+end
+
+let make_ (self : store) (l_view : view) : t =
+  let lvl = { l_view; l_id = -1 } in
+  H_cons.hashcons self.h_cons lvl
+
+let zero self : t = make_ self L_zero
+let succ self t : t = make_ self (L_succ t)
+let one self = succ self @@ zero self
+let var self n : t = make_ self (L_var n)
+
+let rec max self a b : t =
+  if equal a b then
+    a
+  else (
+    match view a, view b with
+    | L_succ a', L_succ b' -> succ self (max self a' b')
+    | L_zero, _ -> b
+    | _, L_zero -> a
+    | _ ->
+      let a, b =
+        if compare a b > 0 then
+          b, a
+        else
+          a, b
+      in
+      make_ self (L_max (a, b))
+  )
+
+let rec imax self a b : t =
+  if equal a b then
+    a
+  else (
+    match view a, view b with
+    | _, L_zero -> zero self (* imax(_, 0) = 0 *)
+    | L_succ a', L_succ b' -> succ self (imax self a' b')
+    | L_zero, _ -> b
+    | _ -> make_ self (L_imax (a, b))
+  )
+
+let of_int self i : t =
+  assert (i >= 0);
+  let rec loop i =
+    if i = 0 then
+      zero self
+    else
+      succ self @@ loop (i - 1)
+  in
+  loop i
+
+let[@inline] is_zero l =
+  match view l with
+  | L_zero -> true
+  | _ -> false
+
+let is_one l =
+  match view 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)

src/core-logic/level.mli

@@ -0,0 +1,41 @@
+open Types_
+
+type view = level_view =
+  | 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 t = level
+
+include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
+
+val to_string : t -> string
+
+val as_offset : t -> t * int
+(** [as_offset lvl] returns a pair [lvl' + n]. *)
+
+(** Hashconsing store *)
+module Store : sig
+  type t
+
+  val create : unit -> t
+end
+
+type store = Store.t
+
+val zero : store -> t
+val one : store -> t
+val var : store -> string -> t
+val succ : store -> t -> t
+val of_int : store -> int -> t
+val max : store -> t -> t -> t
+val imax : store -> 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

src/core-logic/sidekick_core_logic.ml

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

src/core-logic/term.ml

@@ -5,7 +5,7 @@ type bvar = Bvar.t
 type nonrec term = term
 
 type view = term_view =
-  | E_type of int
+  | E_type of level
   | E_var of var
   | E_bound_var of bvar
   | E_const of const
@@ -70,13 +70,23 @@ let[@inline] is_pi e =
   | E_pi _ -> true
   | _ -> false
 
+let as_type e : level option =
+  match e.view with
+  | E_type l -> Some l
+  | _ -> None
+
+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
+
 (* debug printer *)
 let expr_pp_with_ ~pp_ids ~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 0 -> Fmt.string out "Type"
-    | E_type i -> Fmt.fprintf out "Type(%d)" i
+    | E_type lvl when Level.is_one lvl -> Fmt.string out "Type"
+    | E_type lvl -> Fmt.fprintf out "Type.{%a}" Level.pp lvl
     | E_var v -> Fmt.string out v.v_name
     (* | E_var v -> Fmt.fprintf out "(@[%s : %a@])" v.v_name pp v.v_ty *)
     | E_bound_var v ->
@@ -103,15 +113,16 @@ let expr_pp_with_ ~pp_ids ~max_depth out (e : term) : unit =
       Fmt.fprintf out "(@[\\%s:@[%a@].@ %a@])" n pp' _ty
         (loop (k + 1) ~depth:(depth + 1) (n :: names))
         bod
-    | E_pi (_, ty, bod) when is_closed bod ->
+    | E_pi (_, ty_arg, bod)
+      when is_closed bod && Level.is_int (as_type_exn @@ ty ty_arg) ->
       (* actually just an arrow *)
       Fmt.fprintf out "(@[%a@ -> %a@])"
         (loop k ~depth:(depth + 1) names)
-        ty
+        ty_arg
         (loop (k + 1) ~depth:(depth + 1) ("" :: names))
         bod
-    | E_pi ("", _ty, bod) ->
-      Fmt.fprintf out "(@[Pi _:@[%a@].@ %a@])" pp' _ty
+    | E_pi ("", ty_arg, bod) ->
+      Fmt.fprintf out "(@[Pi _:@[%a@].@ %a@])" pp' ty_arg
         (loop (k + 1) ~depth:(depth + 1) ("" :: names))
         bod
     | E_pi (n, _ty, bod) ->
@@ -164,7 +175,7 @@ module Hcons = Hashcons.Make (struct
 
   let hash e : int =
     match e.view with
-    | E_type i -> H.combine2 10 (H.int i)
+    | E_type i -> H.combine2 10 (Level.hash i)
     | E_const c -> H.combine2 20 (Const.hash c)
     | E_var v -> H.combine2 30 (Var.hash v)
     | E_bound_var v -> H.combine2 40 (Bvar.hash v)
@@ -180,18 +191,22 @@ module Hcons = Hashcons.Make (struct
 end)
 
 module Store = struct
-  type t = { (* unique ID for this store *)
-             s_uid: int; s_exprs: Hcons.t }
+  type t = {
+    s_uid: int;  (** unique ID for this store *)
+    s_exprs: Hcons.t;
+    s_lvl_store: Level.store;
+  }
 
   (* TODO: use atomic? CCAtomic? *)
   let n = ref 0
-  let size self = Hcons.size self.s_exprs
+  let[@inline] size self = Hcons.size self.s_exprs
+  let[@inline] lvl_store self = self.s_lvl_store
 
-  let create ?(size = 256) () : t =
+  let create ?(level_store = Level.Store.create ()) ?(size = 256) () : t =
     (* store id, modulo 2^5 *)
     let s_uid = !n land store_id_mask in
     incr n;
-    { s_uid; s_exprs = Hcons.create ~size () }
+    { s_uid; s_exprs = Hcons.create ~size (); s_lvl_store = level_store }
 
   (* check that [e] belongs in this store *)
   let[@inline] check_e_uid (self : t) (e : term) =
@@ -353,14 +368,15 @@ module Make_ = struct
         has_fvars f || has_fvars acc0 || List.exists has_fvars args
       | E_lam (_, ty, bod) | E_pi (_, ty, bod) -> has_fvars ty || has_fvars bod
 
-  let universe_ (e : term) : int =
+  let universe_ (e : term) : level =
     match e.view with
     | E_type i -> i
     | _ -> assert false
 
-  let[@inline] universe_of_ty_ (e : term) : int =
+  (** Universe of the type of [e] *)
+  let universe_of_ty_ (self : store) (e : term) : level =
     match e.view with
-    | E_type i -> i + 1
+    | E_type lvl -> Level.succ self.s_lvl_store lvl
     | _ -> universe_ (ty e)
 
   module T_int_tbl = CCHashtbl.Make (struct
@@ -438,34 +454,39 @@ module Make_ = struct
     else
       aux e 0
 
-  let compute_ty_ store ~make (view : view) : term =
+  (* TODO: have beta-reduction here; level checking; and pluggable reduction
+     rules (in the store) so we can reduce quotients and recursors *)
+
+  (** compute the type of [view]. *)
+  let compute_ty_ (self : store) ~make (view : view) : term =
     match view with
     | E_var v -> Var.ty v
     | E_bound_var v -> Bvar.ty v
-    | E_type i -> make (E_type (i + 1))
+    | E_type lvl -> make (E_type (Level.succ self.s_lvl_store lvl))
     | E_const c ->
       let ty = Const.ty c in
-      Store.check_e_uid store ty;
+      Store.check_e_uid self ty;
       if not (is_closed ty) then
         Error.errorf "const %a@ cannot have a non-closed type like %a" Const.pp
           c pp_debug ty;
       ty
     | E_lam (name, ty_v, bod) ->
-      Store.check_e_uid store ty_v;
-      Store.check_e_uid store bod;
+      Store.check_e_uid self ty_v;
+      Store.check_e_uid self bod;
       (* type of [\x:tau. bod] is [pi x:tau. typeof(bod)] *)
       let ty_bod = ty bod in
       make (E_pi (name, ty_v, ty_bod))
     | E_app (f, a) ->
       (* type of [f a], where [a:tau] and [f: Pi x:tau. ty_bod_f],
          is [ty_bod_f[x := a]] *)
-      Store.check_e_uid store f;
-      Store.check_e_uid store a;
+      Store.check_e_uid self f;
+      Store.check_e_uid self a;
       let ty_f = ty f in
       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
           Error.errorf
             "@[<2>cannot @[apply `%a`@]@ @[to `%a`@],@ expected argument type: \
@@ -480,9 +501,9 @@ module Make_ = struct
           pp_debug f pp_debug a pp_debug ty_f)
     | E_app_fold { args = []; _ } -> assert false
     | E_app_fold { f; args = a0 :: other_args as args; acc0 } ->
-      Store.check_e_uid store f;
-      Store.check_e_uid store acc0;
-      List.iter (Store.check_e_uid store) args;
+      Store.check_e_uid self f;
+      Store.check_e_uid self acc0;
+      List.iter (Store.check_e_uid self) args;
       let ty_result = ty acc0 in
       let ty_a0 = ty a0 in
       (* check that all arguments have the same type *)
@@ -503,32 +524,34 @@ module Make_ = struct
           pp_debug app1 pp_debug (ty app1) pp_debug ty_result;
       ty_result
     | E_pi (_, ty, bod) ->
-      (* TODO: check the actual triplets for COC *)
       (*Fmt.printf "pi %a %a@." pp_debug ty pp_debug bod;*)
-      Store.check_e_uid store ty;
-      Store.check_e_uid store bod;
-      let u = max (universe_of_ty_ ty) (universe_of_ty_ bod) in
+      Store.check_e_uid self ty;
+      Store.check_e_uid self bod;
+      let u =
+        Level.imax self.s_lvl_store (universe_of_ty_ self ty)
+          (universe_of_ty_ self bod)
+      in
       make (E_type u)
 
   let ty_assert_false_ () = assert false
 
   (* hashconsing + computing metadata + computing type (for new terms) *)
-  let rec make_ (store : store) view : term =
+  let rec make_ (self : store) view : term =
     let e = { view; ty = T_ty_delayed ty_assert_false_; id = -1; flags = 0 } in
-    let e2 = Hcons.hashcons store.s_exprs e in
+    let e2 = Hcons.hashcons self.s_exprs e in
     if e == e2 then (
       (* new term, compute metadata *)
-      assert (store.s_uid land store_id_mask == store.s_uid);
+      assert (self.s_uid land store_id_mask == self.s_uid);
 
       (* first, compute type *)
       (match e.view with
-      | E_type i ->
+      | E_type lvl ->
         (* cannot force type now, as it's an infinite tower of types.
            Instead we will produce the type on demand. *)
-        let get_ty () = make_ store (E_type (i + 1)) in
+        let get_ty () = make_ self (E_type (Level.succ self.s_lvl_store lvl)) in
         e.ty <- T_ty_delayed get_ty
       | _ ->
-        let ty = compute_ty_ store ~make:(make_ store) view in
+        let ty = compute_ty_ self ~make:(make_ self) view in
         e.ty <- T_ty ty);
       let has_fvars = compute_has_fvars_ e in
       e2.flags <-
@@ -537,13 +560,17 @@ module Make_ = struct
               1 lsl store_id_bits
             else
               0)
-        lor store.s_uid;
-      Store.check_e_uid store e2
+        lor self.s_uid;
+      Store.check_e_uid self e2
     );
     e2
 
-  let type_of_univ store i : term = make_ store (E_type i)
-  let type_ store : term = type_of_univ store 0
+  let type_of_univ store lvl : term = make_ store (E_type lvl)
+
+  let type_of_univ_int store i : term =
+    type_of_univ store (Level.of_int store.s_lvl_store i)
+
+  let type_ store : term = type_of_univ store (Level.one store.s_lvl_store)
   let var store v : term = make_ store (E_var v)
   let var_str store name ~ty : term = var store (Var.make name ty)
   let bvar store v : term = make_ store (E_bound_var v)

src/core-logic/term.mli

@@ -27,7 +27,7 @@ type store
 
     A view is the shape of the root node of a term. *)
 type view = term_view =
-  | E_type of int
+  | E_type of level
   | E_var of var
   | E_bound_var of bvar
   | E_const of const
@@ -57,6 +57,8 @@ 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_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.
@@ -114,12 +116,14 @@ val ty : t -> t
 module Store : sig
   type t = store
 
-  val create : ?size:int -> unit -> t
+  val create : ?level_store:Level.store -> ?size:int -> unit -> t
   val size : t -> int
+  val lvl_store : t -> Level.store
 end
 
 val type_ : store -> t
-val type_of_univ : store -> int -> t
+val type_of_univ : store -> level -> t
+val type_of_univ_int : store -> int -> t
 val var : store -> var -> t
 val var_str : store -> string -> ty:t -> t
 val bvar : store -> bvar -> t

src/core-logic/types_.ml

@@ -2,8 +2,19 @@ module H = CCHash
 
 type const_view = ..
 
+(** View of a level expression. *)
+type level_view =
+  | L_zero
+  | L_succ of level
+  | L_var of string  (** variable *)
+  | L_max of level * level  (** max *)
+  | L_imax of level * level  (** impredicative max. *)
+
+and level = { l_view: level_view; mutable l_id: int }
+(** A level expression *)
+
 type term_view =
-  | E_type of int
+  | E_type of level
   | E_var of var
   | E_bound_var of bvar
   | E_const of const