🚧 🦆 Inductive Types

cooltt.opam

@@ -18,6 +18,7 @@ depends: [
   "menhir" {>= "20180703"}
   "uuseg" {>= "12.0.0"}
   "uutf" {>= "1.0.2"}
+  "alcotest" {>= "1.5.0"} {with-test}
   "odoc" {with-doc}
   "bantorra"
   "yuujinchou"

src/core/Conversion.ml

@@ -96,6 +96,13 @@ let rec equate_tp (tp0 : D.tp) (tp1 : D.tp) =
     let* fib1 = lift_cmp @@ inst_tp_clo fam1 x in
     equate_tp fib0 fib1
   | D.Signature sign1, D.Signature sign2 -> equate_sign sign1 sign2
+  | D.Desc, D.Desc ->
+    ret ()
+  | D.Ctx, D.Ctx ->
+    ret ()
+  | D.Tm (ctx0, desc0), D.Tm (ctx1, desc1) ->
+    let* () = equate_con D.Ctx ctx0 ctx1 in
+    equate_con D.Desc desc0 desc1
   | D.Sub (tp0, phi0, clo0), D.Sub (tp1, phi1, clo1) ->
     let* () = equate_tp tp0 tp1 in
     let* () = equate_cof phi0 phi1 in
@@ -144,7 +151,7 @@ and equate_sign sign0 sign1 =
 
 and equate_stable_code univ code0 code1 =
   match code0, code1 with
-  | `Nat, `Nat | `Circle, `Circle | `Univ, `Univ -> ret ()
+  | `Nat, `Nat | `Circle, `Circle | `Univ, `Univ | `Desc, `Desc | `Ctx, `Ctx -> ret ()
   | `Pi (base0, fam0), `Pi (base1, fam1)
   | `Sg (base0, fam0), `Sg (base1, fam1) ->
     let* _ = equate_con univ base0 base1 in
@@ -179,6 +186,9 @@ and equate_stable_code univ code0 code1 =
 
   | `Signature sign0, `Signature sign1 ->
     equate_sign_code univ sign0 sign1
+  | `Tm (ctx0, desc0), `Tm (ctx1, desc1) ->
+    let* () = equate_con D.Ctx ctx0 ctx1 in
+    equate_con D.Desc desc0 desc1
   | code0, code1 ->
     conv_err @@ ExpectedConEq (univ, D.StableCode code0, D.StableCode code1)
 
@@ -228,6 +238,47 @@ and equate_con tp con0 con1 =
     equate_con fib snd0 snd1
   | D.Signature sign, _, _ ->
     equate_struct sign con0 con1
+  | _, D.DescEnd, D.DescEnd ->
+    ret ()
+  | _, D.DescArg (a0, desc0), D.DescArg (a1, desc1) ->
+    let* () = equate_con D.Univ a0 a1 in
+    let* famtp =
+      lift_cmp @@
+      Sem.splice_tp @@
+      Splice.con a0 @@ fun arg ->
+      Splice.term @@ TB.pi (TB.el arg) (fun _ -> TB.desc)
+    in
+    equate_con famtp desc0 desc1
+  | _, D.DescRec desc0, DescRec desc1 ->
+    equate_con D.Desc desc0 desc1
+  | _, D.CtxNil, D.CtxNil ->
+    ret ()
+  | _, D.CtxSnoc (ctx0, ident0, desc0), D.CtxSnoc (ctx1, ident1, desc1) when Ident.equal ident0 ident1 ->
+    let* () = equate_con D.Ctx ctx0 ctx1 in
+    equate_con D.Desc desc0 desc1
+  | _, D.TmVar x, D.TmVar y when Ident.equal x y ->
+    ret ()
+  | D.Tm (ctx, _), D.TmAppArg (base0, fam0, fn0, arg0), D.TmAppArg (base1, fam1, fn1, arg1) ->
+    let* () = equate_con D.Univ base0 base1 in
+    let* basetp =
+      lift_cmp @@
+      Sem.splice_tp @@
+      Splice.con base0 @@ fun base0 ->
+      Splice.term @@ TB.el base0
+    in
+    let* famtp =
+      lift_cmp @@
+      Sem.splice_tp @@
+      Splice.con base0 @@ fun base0 ->
+      Splice.term @@ TB.pi (TB.el base0) (fun _ -> TB.desc)
+    in
+    let* () = equate_con famtp fam0 fam1 in
+    let* () = equate_con (D.Tm (ctx, D.DescArg (base0, fam0))) fn0 fn1 in
+    equate_con basetp arg0 arg1
+  | D.Tm (ctx, _) ,D.TmAppRec (desc0, fn0, arg0), D.TmAppRec (desc1, fn1, arg1) ->
+    let* () = equate_con D.Desc desc0 desc1 in
+    let* () = equate_con (D.Tm (ctx, D.DescRec desc0)) fn0 fn1 in
+    equate_con (D.Tm (ctx, D.DescEnd)) arg0 arg1
   | D.Sub (tp, _phi, _), _, _ ->
     let* out0 = lift_cmp @@ do_sub_out con0 in
     let* out1 = lift_cmp @@ do_sub_out con1 in

src/core/Domain.ml

@@ -102,7 +102,12 @@ struct
     | KAp (_, con) -> Format.fprintf fmt "ap[%a]" pp_con con
     | KFst -> Format.fprintf fmt "fst"
     | KSnd -> Format.fprintf fmt "snd"
-    | KProj lbl -> Format.fprintf fmt "proj[%a]" Ident.pp_user lbl
+    | KProj lbl -> Format.fprintf fmt "proj[%a]" Ident.pp lbl
+    | KDescMethod (ctx, mot) ->
+      Format.fprintf fmt
+        "desc/method[%a, %a]" 
+        pp_con ctx
+        pp_con mot
     | KNatElim _ -> Format.fprintf fmt "<nat-elim>"
     | KCircleElim _ -> Format.fprintf fmt "<circle-elim>"
     | KElOut -> Uuseg_string.pp_utf_8 fmt "⭝ₑₗ"
@@ -156,7 +161,27 @@ struct
       Format.fprintf fmt "pair[%a,%a]" pp_con con0 pp_con con1
     | Struct fields ->
       Format.fprintf fmt "struct[%a]"
-        (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp_user lbl pp_con tp)) fields
+        (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp lbl pp_con tp)) fields
+    | DescEnd ->
+      Format.fprintf fmt "desc-end"
+    | DescArg (arg, desc) ->
+      Format.fprintf fmt "desc-arg[%a, %a]" pp_con arg pp_con desc
+    | DescRec desc ->
+      Format.fprintf fmt "desc-rec[%a]" pp_con desc
+    | CtxNil ->
+      Format.fprintf fmt "ctx-nil"
+    | CtxSnoc(ctx, ident, desc) ->
+      Format.fprintf fmt "ctx-snoc[%a, %a, %a]" pp_con ctx Ident.pp ident pp_con desc
+    | ElemHere (ctx, desc) ->
+      Format.fprintf fmt "elem-here[%a, %a]" pp_con ctx pp_con desc
+    | ElemThere (ctx, desc0, desc1, elem) ->
+      Format.fprintf fmt "elem-here[%a, %a, %a, %a]" pp_con ctx pp_con desc0 pp_con desc1 pp_con elem
+    | TmVar v ->
+      Format.fprintf fmt "tm-var[%a]" Ident.pp v
+    | TmAppArg (base, fam, f, a) ->
+      Format.fprintf fmt "tm-app-arg[%a, %a, %a, %a]" pp_con base pp_con fam pp_con f pp_con a
+    | TmAppRec (desc, f, a) ->
+      Format.fprintf fmt "tm-app-rec[%a, %a, %a]" pp_con desc pp_con f pp_con a
     | Prf ->
       Format.fprintf fmt "*"
     | Cof (Cof.Join phis) ->
@@ -203,7 +228,7 @@ struct
 
   and pp_sign fmt =
     function
-    | Field (ident, tp, clo) -> Format.fprintf fmt "sig/field[%a,%a,%a]" Ident.pp_user ident pp_tp tp pp_sign_clo clo
+    | Field (ident, tp, clo) -> Format.fprintf fmt "sig/field[%a,%a,%a]" Ident.pp ident pp_tp tp pp_sign_clo clo
     | Empty -> Format.fprintf fmt "sig/empty"
 
   and pp_tp fmt =
@@ -222,6 +247,14 @@ struct
       Format.fprintf fmt "<cof>"
     | TpDim ->
       Format.fprintf fmt "<dim>"
+    | Desc ->
+      Format.fprintf fmt "<desc>"
+    | Ctx ->
+      Format.fprintf fmt "<ctx>"
+    | Elem (ctx, desc) ->
+      Format.fprintf fmt "elem[%a, %a]" pp_con ctx pp_con desc
+    | Tm (ctx, desc) ->
+      Format.fprintf fmt "tm[%a, %a]" pp_con ctx pp_con desc
     | Univ ->
       Format.fprintf fmt "<univ>"
     | Nat ->
@@ -247,6 +280,10 @@ struct
     | `Pi _ -> Format.fprintf fmt "<code-pi>"
     | `Sg _ -> Format.fprintf fmt "<code-sg>"
     | `Signature _ -> Format.fprintf fmt "<code-sig>"
+    | `Desc -> Format.fprintf fmt "<desc>"
+    | `Ctx -> Format.fprintf fmt "<ctx>"
+    | `Elem (ctx, desc) -> Format.fprintf fmt "elem[%a, %a]" pp_con ctx pp_con desc
+    | `Tm (ctx, desc) -> Format.fprintf fmt "ctx[%a, %a]" pp_con ctx pp_con desc
     | `Nat -> Format.fprintf fmt "<code-nat>"
     | `Circle -> Format.fprintf fmt "<code-circle>"
     | `Univ -> Format.fprintf fmt "<code-univ>"

src/core/Domain.mli

@@ -22,13 +22,13 @@ module Make : functor (Symbol : Symbol.S) -> sig
 
   val fst : con
   val snd : con
-  val proj : Ident.user -> con
+  val proj : Ident.t -> con
   val el_out : con
 
   val tm_abort : con
   val tp_abort : tp
 
-  val sign_lbls : sign -> Ident.user list
+  val sign_lbls : sign -> Ident.t list
 
   (** {1 Pretty-printers }
 

src/core/DomainData.ml

@@ -17,9 +17,21 @@ struct
     | `Sg of 'a * 'a
     (** Dependent sum type *)
 
-    | `Signature of (Ident.user * 'a) list
+    | `Signature of (Ident.t * 'a) list
     (** First-Class Record types *)
 
+    | `Desc
+    (** Descriptions *)
+
+    | `Ctx
+    (** Contexts of Descriptions *)
+
+    | `Elem of 'a * 'a
+    (** A proof that [A ∈ Γ] *)
+
+    | `Tm of 'a * 'a
+    (** Terms in the language of inductive types. *)
+
     | `Ext of int * 'a * [`Global of 'a] * 'a
     (** Extension type *)
 
@@ -68,7 +80,35 @@ struct
     | Base
     | Loop of dim
     | Pair of con * con
-    | Struct of (Ident.user * con) list
+    | Struct of (Ident.t * con) list
+
+    (** Descriptions. These can be thought of as the types of a simple type theory. *)
+    | DescEnd
+    (** Something of sort [□] *)
+    | DescArg of con * con
+    (** A dependent function type [(x : A) → B x], where [A] comes from the outer type theory. *)
+    | DescRec of con
+    (** A non-dependent function type [□ → B]. *)
+
+    (** Contexts of descriptions. *)
+    | CtxNil
+    | CtxSnoc of con * Ident.t * con
+
+    (** Proofs that [A ∈ Γ] *)
+    | ElemHere of con * con
+    (** [∀ Γ A → A ∈ (Γ, A) ] *)
+    | ElemThere of con * con * con * con
+    (** [∀ Γ A B → A ∈ Γ → A ∈ (Γ, B) ] *)
+
+    (** Formal expressions involving elements of a context. We can think of these as embedded terms
+        from the simple type theory of inductive types. *)
+    | TmVar of Ident.t
+    (** A variable from the context [Γ] *)
+    | TmAppArg of con * con * con * con
+    (** Application to a dependent function type [(x : A) → B x], where [A] comes from the outer type theory. *)
+    | TmAppRec of con * con * con
+    (** Application to a function type [□ → B]  *)
+
     | SubIn of con
 
     | ElIn of con
@@ -108,12 +148,16 @@ struct
     | Pi of tp * Ident.t * tp_clo
     | Sg of tp * Ident.t * tp_clo
     | Signature of sign
+    | Desc
+    | Ctx
+    | Elem of con * con
+    | Tm of con * con
     | Nat
     | Circle
     | TpLockedPrf of cof
 
   and sign =
-    | Field of Ident.user * tp * S.sign clo
+    | Field of Ident.t * tp * S.sign clo
     | Empty
 
   (** A head is a variable (e.g. {!constructor:Global}, {!constructor:Var}), or it is some kind of unstable elimination form ({!constructor:Coe}, {!constructor:UnstableCut}). The geometry of {!type:cut}, {!type:hd}, {!type:unstable_frm} enables a very direct way to re-reduce a complex cut to whnf by following the unstable nodes to the root. *)
@@ -135,7 +179,8 @@ struct
     | KAp of tp * con
     | KFst
     | KSnd
-    | KProj of Ident.user
+    | KProj of Ident.t
+    | KDescMethod of con * con
     | KNatElim of con * con * con
     | KCircleElim of con * con * con
 

src/core/Ident.ml

@@ -1,22 +1,14 @@
 type t = [`Anon | `User of string list | `Machine of string]
-type 'a some = 'a constraint 'a = [< t ]
-type user = [ `User of string list ]
-
-let user parts = `User parts
 
 let qual_to_string =
   function
   | [] -> "(root)"
   | parts -> String.concat "." parts
 
-let pp_user fmt =
-  function
-  | `User parts -> Uuseg_string.pp_utf_8 fmt (qual_to_string parts)
-
 let pp fmt =
   function
   | `Anon -> Format.fprintf fmt "<anon>"
-  | `User _ as u -> pp_user fmt u
+  | `User parts -> Uuseg_string.pp_utf_8 fmt (qual_to_string parts)
   | `Machine str -> Uuseg_string.pp_utf_8 fmt str
 
 let to_string =
@@ -31,11 +23,7 @@ let to_string_opt =
   | `Machine nm -> Some nm
   | `Anon -> None
 
-let user_to_string_opt =
-  function
-  | `User [] -> None
-  | `User parts -> Some (String.concat "." parts)
-
 let equal i0 i1 =
   match (i0, i1) with
   | `User p0, `User p1 -> List.equal String.equal p0 p1
+  | _, _ -> false

src/core/Ident.mli

@@ -1,16 +1,9 @@
 open Basis
 
 type t = [`Anon | `User of string list | `Machine of string]
-type 'a some = 'a constraint 'a = [< t ]
-type user = [ `User of string list ]
-
-val user : string list -> t
 
 val pp : t Pp.printer
-val pp_user : user Pp.printer
 val to_string : t -> string
 val to_string_opt : t -> string option
 
-val user_to_string_opt : user -> string option
-
-val equal : user -> user -> bool
+val equal : t -> t -> bool