small improvement

src/core-logic/term.ml

@@ -441,24 +441,29 @@ module Make_ = struct
     else
       aux e 0
 
-  let compute_ty_ ~make (view : view) : term =
+  let compute_ty_ 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_const c ->
       let ty = Const.ty c in
+      Store.check_e_uid store 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;
       (* 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;
       let ty_f = ty f in
       let ty_a = ty a in
       (match ty_f.view with
@@ -478,6 +483,8 @@ module Make_ = struct
     | 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
       make (E_type u)
 
@@ -499,7 +506,7 @@ module Make_ = struct
         let get_ty () = make_ store (E_type (i + 1)) in
         e.ty <- T_ty_delayed get_ty
       | _ ->
-        let ty = compute_ty_ ~make:(make_ store) view in
+        let ty = compute_ty_ store ~make:(make_ store) view in
         e.ty <- T_ty ty);
       let has_fvars = compute_has_fvars_ e in
       e2.flags <-
@@ -571,28 +578,42 @@ module Make_ = struct
     else
       loop 0 e0
 
-  let abs_on_ (store : store) (v : var) (e : term) : term =
+  module DB = struct
-    Store.check_e_uid store v.v_ty;
+    let subst_db0 store e ~by : t = db_0_replace_ ~make:(make_ store) e ~by
-    Store.check_e_uid store e;
+
-    if not (is_closed v.v_ty) then
+    let shift store t ~by : t =
-      Error.errorf "cannot abstract on variable@ with non closed type %a"
+      assert (by >= 0);
-        pp_debug v.v_ty;
+      db_shift_ ~make:(make_ store) t by
-    let db0 = bvar store (Bvar.make 0 v.v_ty) in
+
-    let body = db_shift_ ~make:(make_ store) e 1 in
+    let lam_db ?(var_name = "") store ~var_ty bod : term =
-    subst_ ~make:(make_ store) ~recursive:false body
+      make_ store (E_lam (var_name, var_ty, bod))
-      { m = Var_.Map.singleton v db0 }
+
+    let pi_db ?(var_name = "") store ~var_ty bod : term =
+      make_ store (E_pi (var_name, var_ty, bod))
+
+    let abs_on (store : store) (v : var) (e : term) : term =
+      Store.check_e_uid store v.v_ty;
+      Store.check_e_uid store e;
+      if not (is_closed v.v_ty) then
+        Error.errorf "cannot abstract on variable@ with non closed type %a"
+          pp_debug v.v_ty;
+      let db0 = bvar store (Bvar.make 0 v.v_ty) in
+      let body = db_shift_ ~make:(make_ store) e 1 in
+      subst_ ~make:(make_ store) ~recursive:false body
+        { m = Var_.Map.singleton v db0 }
+  end
 
   let lam store v bod : term =
-    let bod' = abs_on_ store v bod in
+    let bod' = DB.abs_on store v bod in
-    make_ store (E_lam (Var.name v, Var.ty v, bod'))
+    DB.lam_db ~var_name:(Var.name v) store ~var_ty:(Var.ty v) bod'
 
   let pi store v bod : term =
-    let bod' = abs_on_ store v bod in
+    let bod' = DB.abs_on store v bod in
-    make_ store (E_pi (Var.name v, Var.ty v, bod'))
+    DB.pi_db ~var_name:(Var.name v) store ~var_ty:(Var.ty v) bod'
 
   let arrow store a b : term =
-    let b' = db_shift_ ~make:(make_ store) b 1 in
+    let b' = DB.shift store b ~by:1 in
-    make_ store (E_pi ("", a, b'))
+    DB.pi_db store ~var_ty:a b'
 
   let arrow_l store args ret = List.fold_right (arrow store) args ret
 
@@ -617,7 +638,7 @@ module Make_ = struct
     | E_lam (name, ty, bod) ->
       let name = pick_name_ name bod in
       let v = Var.make name ty in
-      let bod' = db_0_replace_ bod ~make:(make_ store) ~by:(var store v) in
+      let bod' = DB.subst_db0 store bod ~by:(var store v) in
       Some (v, bod')
     | _ -> None
 

src/core-logic/term.mli

@@ -80,7 +80,8 @@ val type_ : store -> t
 val type_of_univ : store -> int -> t
 val var : store -> var -> t
 val var_str : store -> string -> ty:t -> t
-val const : store -> Const.t -> t
+val bvar : store -> bvar -> t
+val const : store -> const -> t
 val app : store -> t -> t -> t
 val app_l : store -> t -> t list -> t
 val lam : store -> var -> t -> t
@@ -90,6 +91,38 @@ val arrow_l : store -> t list -> t -> t
 val open_lambda : store -> t -> (var * t) option
 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. *)
+
+  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. *)
+
+  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.
+
+      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 : 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).
+
+    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.
+
+      For example, [abs_on store x (\y. x+y)] is [\y. _[1] y].
+  *)
+end
+
 (**/**)
 
 module Internal_ : sig

unittest/core-logic/t1.expected

@@ -19,3 +19,6 @@ p2: p2
   type: (tau -> (tau -> Bool))
 t2: = ((tau -> (tau -> Bool))) ((\x:tau. (\y:tau. p2 x[1] y[0]))) (= tau)
   type: Bool
+f_vec: vec
+  type: (Type -> (nat -> Type))
+  type of type: Type(1)

unittest/core-logic/t1.ml

@@ -97,3 +97,18 @@ let t2 =
 let () =
   Fmt.printf "@[<v2>t2: %a@ type: %a@]@." Term.pp_debug t2 Term.pp_debug
     (Term.ty t2)
+
+(* a bit of dependent types *)
+
+let nat = Term.const store @@ Str_const.make "nat" ~ty:type_
+
+let f_vec =
+  let v_A = Var.make "A" type_ in
+  let v_n = Var.make "n" nat in
+  Term.const store
+  @@ Str_const.make "vec" ~ty:Term.(pi store v_A @@ pi store v_n @@ type_ store)
+
+let () =
+  Fmt.printf "@[<v2>f_vec: %a@ type: %a@ type of type: %a@]@." Term.pp_debug
+    f_vec Term.pp_debug (Term.ty f_vec) Term.pp_debug
+    (Term.ty @@ Term.ty f_vec)