🔭 First-Class Telescopes

cooltt-lib

@@ -0,0 +1 @@
+{ "format": "1.0.0" }

src/core/Conversion.ml

@@ -21,7 +21,6 @@ struct
     | ExpectedTypeEq of D.tp * D.tp
     | ExpectedConEq of D.tp * D.con * D.con
     | ExpectedFrmEq of D.frm * D.frm
-    | ExpectedSignEq of D.sign * D.sign
     | SpineLengthMismatch of D.frm list * D.frm list
     | HeadMismatch of D.hd * D.hd
 
@@ -38,8 +37,6 @@ struct
       Format.fprintf fmt "Expected %a = %a : %a" D.pp_con con0 D.pp_con con1 D.pp_tp tp
     | ExpectedFrmEq (frm0, frm1) ->
       Format.fprintf fmt "Expected %a = %a" D.pp_frame frm0 D.pp_frame frm1
-    | ExpectedSignEq (sign0, sign1) ->
-      Format.fprintf fmt "Expected %a = %a sig" D.pp_sign sign0 D.pp_sign sign1
     | SpineLengthMismatch (sp0, sp1) ->
       Format.fprintf fmt "Spine length mismatch between %a and %a" D.pp_spine sp0 D.pp_spine sp1
     | HeadMismatch (hd0, hd1) ->
@@ -95,7 +92,9 @@ let rec equate_tp (tp0 : D.tp) (tp1 : D.tp) =
     let* fib0 = lift_cmp @@ inst_tp_clo fam0 x in
     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.Symbol, D.Symbol -> ret ()
+  | D.Telescope, D.Telescope -> ret ()
+  | D.Signature tele0, D.Signature tele1 -> equate_con D.Telescope tele0 tele1
   | D.Sub (tp0, phi0, clo0), D.Sub (tp1, phi1, clo1) ->
     let* () = equate_tp tp0 tp1 in
     let* () = equate_cof phi0 phi1 in
@@ -131,20 +130,9 @@ let rec equate_tp (tp0 : D.tp) (tp1 : D.tp) =
   | _ ->
     conv_err @@ ExpectedTypeEq (tp0, tp1)
 
-and equate_sign sign0 sign1 =
-  match sign0, sign1 with
-  | D.Field (lbl0, tp0, clo0), D.Field (lbl1, tp1, clo1) when Ident.equal lbl0 lbl1 ->
-    let* () = equate_tp tp0 tp1 in
-    bind_var_ tp0 @@ fun x ->
-    let* sign0 = lift_cmp @@ inst_sign_clo clo0 x in
-    let* sign1 = lift_cmp @@ inst_sign_clo clo1 x in
-    equate_sign sign0 sign1
-  | D.Empty, D.Empty -> ret ()
-  | _, _ -> conv_err @@ ExpectedSignEq (sign0, sign1)
-
 and equate_stable_code univ code0 code1 =
   match code0, code1 with
-  | `Nat, `Nat | `Circle, `Circle | `Univ, `Univ -> ret ()
+  | `Nat, `Nat | `Circle, `Circle | `Telescope, `Telescope | `Univ, `Univ -> ret ()
   | `Pi (base0, fam0), `Pi (base1, fam1)
   | `Sg (base0, fam0), `Sg (base1, fam1) ->
     let* _ = equate_con univ base0 base1 in
@@ -177,28 +165,11 @@ and equate_stable_code univ code0 code1 =
     in
     equate_con tp_bdry bdry0 bdry1
 
-  | `Signature sign0, `Signature sign1 ->
-    equate_sign_code univ sign0 sign1
+  | `Signature tele0, `Signature tele1->
+    equate_con D.Telescope tele0 tele1
   | code0, code1 ->
     conv_err @@ ExpectedConEq (univ, D.StableCode code0, D.StableCode code1)
 
-and equate_sign_code univ sign0 sign1 =
-  let rec go vfams sign0 sign1 =
-    match sign0, sign1 with
-    | [], [] -> ret ()
-    | (lbl0, fam0) :: sign0 , (lbl1, fam1) :: sign1 when Ident.equal lbl0 lbl1 ->
-      let* fam_tp =
-        lift_cmp @@
-        splice_tp @@
-        Splice.tp univ @@ fun univ ->
-        Splice.cons vfams @@ fun args ->
-        Splice.term @@ TB.pis args @@ fun _ -> univ
-      in
-      let* _ = equate_con fam_tp fam0 fam1 in
-      go (vfams @ [fam0]) sign0 sign1
-    | _, _ -> conv_err @@ ExpectedConEq (univ, D.StableCode (`Signature sign0), D.StableCode (`Signature sign1))
-  in go [] sign0 sign1
-
 (* Invariant: tp, con0, con1 not necessarily whnf *)
 and equate_con tp con0 con1 =
   ConvM.abort_if_inconsistent (ret ()) @@
@@ -212,6 +183,8 @@ and equate_con tp con0 con1 =
   | _, D.Split branches, _
   | _, _, D.Split branches ->
     MU.iter (fun (phi, _) -> ConvM.restrict_ [phi] @@ equate_con tp con0 con1) branches
+  | _, D.Quoted id0, D.Quoted id1 when Ident.equal id0 id1 ->
+    ret ()
   | D.Pi (base, _, fam), _, _ ->
     bind_var_ base @@ fun x ->
     let* fib = lift_cmp @@ inst_tp_clo fam x in
@@ -226,6 +199,18 @@ and equate_con tp con0 con1 =
     let* snd0 = lift_cmp @@ do_snd con0 in
     let* snd1 = lift_cmp @@ do_snd con1 in
     equate_con fib snd0 snd1
+  | _, D.TeleNil, D.TeleNil ->
+    ret ()
+  | _, D.TeleCons (id0, code0, tele0), D.TeleCons (id1, code1, tele1) ->
+    let* () = equate_con D.Symbol id0 id1 in
+    let* () = equate_con D.Univ code0 code1 in
+    let* tele_tp =
+      lift_cmp @@
+      Sem.splice_tp @@
+      Splice.con code0 @@ fun code ->
+      Splice.term @@ TB.pi (TB.el code) (fun _ -> TB.telescope)
+    in
+    equate_con tele_tp tele0 tele1
   | D.Signature sign, _, _ ->
     equate_struct sign con0 con1
   | D.Sub (tp, _phi, _), _, _ ->
@@ -317,16 +302,19 @@ and equate_con tp con0 con1 =
     Format.eprintf "failed: %a, %a@." D.pp_con con0 D.pp_con con1;
     conv_err @@ ExpectedConEq (tp, con0, con1)
 
-and equate_struct (sign : D.sign) con0 con1 =
-  match sign with
-  | D.Field (lbl, tp, clo) ->
-    let* field0 = lift_cmp @@ do_proj con0 lbl in
-    let* field1 = lift_cmp @@ do_proj con1 lbl in
+and equate_struct (tele : D.con) con0 con1 =
+  match tele with
+  | D.TeleCons (qid, code, lam) ->
+    let* id = lift_cmp @@ unquote qid in
+    let* field0 = lift_cmp @@ do_proj con0 id in
+    let* field1 = lift_cmp @@ do_proj con1 id in
+    let* tp = lift_cmp @@ do_el code in
     let* () = equate_con tp field0 field1 in
-    let* sign = lift_cmp @@ inst_sign_clo clo field0 in
-    equate_struct sign con0 con1
-  | D.Empty ->
+    let* tele = lift_cmp @@ do_ap lam field0 in
+    equate_struct tele con0 con1
+  | D.TeleNil ->
     ret ()
+  | _ -> failwith "internal error: equate_struct failed"
 
 
 (* Invariant: cut0, cut1 are whnf *)
@@ -402,6 +390,36 @@ and equate_frm k0 k1 =
       TB.el @@ TB.ap mot [TB.loop x]
     in
     equate_con loop_tp loop_case0 loop_case1
+  | D.KPush (qid0, code0, field0), D.KPush (qid1, code1, field1) ->
+    let* () = equate_con D.Symbol qid0 qid1 in
+    let* () = equate_con D.Univ code0 code1 in
+    let* tp = lift_cmp @@ do_el code0 in
+    equate_con tp field0 field1
+  | D.KTeleElim (mot0, nil_case0, cons_case0), D.KTeleElim (mot1, nil_case1, cons_case1) ->
+    let* mot_tp =
+      lift_cmp @@
+      Sem.splice_tp @@
+      Splice.term @@
+      TB.pi TB.telescope @@ fun _ -> TB.univ
+    in
+    let* () = equate_con mot_tp mot0 mot1 in
+    let* () =
+      let* mot_nil = lift_cmp @@ do_ap mot0 D.TeleNil in
+      let* tp_mot_nil = lift_cmp @@ do_el mot_nil in
+      equate_con tp_mot_nil nil_case0 nil_case1
+    in
+    let* cons_tp =
+      lift_cmp @@
+      Sem.splice_tp @@
+      Splice.con mot0 @@ fun mot ->
+      Splice.term @@
+      TB.pi TB.symbol @@ fun qid ->
+      TB.pi TB.univ @@ fun a ->
+      TB.pi (TB.pi (TB.el a) @@ fun _ -> TB.telescope) @@ fun t ->
+      TB.pi (TB.pi (TB.el a) @@ fun x -> TB.el (TB.ap mot [TB.ap t [x]])) @@ fun _ ->
+      TB.el @@ TB.ap mot [TB.cons qid a t]
+    in
+    equate_con cons_tp cons_case0 cons_case1
   | D.KElOut, D.KElOut ->
     ret ()
   | _ ->

src/core/Domain.ml

@@ -38,11 +38,6 @@ struct
   let tm_abort = Split []
   let tp_abort = TpSplit []
 
-  let sign_lbls =
-    function
-    | Field (lbl, _, Clo (sign, _)) -> lbl :: (List.map (fun (lbl, _) -> lbl) sign)
-    | Empty -> []
-
   let dim_to_con =
     function
     | Dim.Dim0 -> Dim0
@@ -99,13 +94,15 @@ struct
   and pp_frame : frm Pp.printer =
     fun fmt ->
     function
-    | KAp (_, con) -> Format.fprintf fmt "ap[%a]" pp_con con
+    | KAp (tp, con) -> Format.fprintf fmt "ap[%a, %a]" pp_tp tp pp_con con
     | KFst -> Format.fprintf fmt "fst"
     | KSnd -> Format.fprintf fmt "snd"
     | KProj lbl -> Format.fprintf fmt "proj[%a]" Ident.pp_user lbl
     | KNatElim _ -> Format.fprintf fmt "<nat-elim>"
     | KCircleElim _ -> Format.fprintf fmt "<circle-elim>"
-    | KElOut -> Uuseg_string.pp_utf_8 fmt "⭝ₑₗ"
+    | KTeleElim _ -> Format.fprintf fmt "<tele-elim>"
+    | KPush _ -> Format.fprintf fmt "<push>"
+    | KElOut -> Uuseg_string.pp_utf_8 fmt "el/out"
 
   and pp_cof : cof Pp.printer =
     fun fmt cof ->
@@ -131,17 +128,11 @@ struct
         (pp_list_group ~left:pp_lsq ~right:pp_rsq ~sep pp_tp) (Bwd.Bwd.to_list tpenv)
         (pp_list_group ~left:pp_lsq ~right:pp_rsq ~sep pp_con) (Bwd.Bwd.to_list conenv)
 
-  and pp_sign_clo : (S.sign clo) Pp.printer =
-    let sep fmt () = Format.fprintf fmt "," in
-    fun fmt (Clo (sign, {tpenv; conenv})) ->
-      Format.fprintf fmt "tpclo[%a ; [%a ; %a]]"
-        S.dump_sign sign
-        (pp_list_group ~left:pp_lsq ~right:pp_rsq ~sep pp_tp) (Bwd.Bwd.to_list tpenv)
-        (pp_list_group ~left:pp_lsq ~right:pp_rsq ~sep pp_con) (Bwd.Bwd.to_list conenv)
-
   and pp_con : con Pp.printer =
     fun fmt ->
     function
+    | Quoted id ->
+      Format.fprintf fmt "`%a" Ident.pp_user id
     | Cut {cut;tp} ->
       Format.fprintf fmt "cut[%a :: %a]" pp_cut cut pp_tp tp
     | Zero ->
@@ -154,6 +145,13 @@ struct
       Format.fprintf fmt "loop[%a]" pp_dim r
     | Pair (con0, con1) ->
       Format.fprintf fmt "pair[%a,%a]" pp_con con0 pp_con con1
+    | TeleNil ->
+      Format.fprintf fmt "tele/nil"
+    | TeleCons (qid, code, tele) ->
+      Format.fprintf fmt "tele/cons[%a, %a, %a]"
+        pp_con qid
+        pp_con code
+        pp_con tele
     | 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
@@ -200,20 +198,18 @@ struct
     | LockedPrfIn _ ->
       Format.fprintf fmt "<wrap>"
 
-
-  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
-    | Empty -> Format.fprintf fmt "sig/empty"
-
   and pp_tp fmt =
     function
     | Pi (base, ident, fam) ->
       Format.fprintf fmt "pi[%a,%a,%a]" pp_tp base Ident.pp ident pp_tp_clo fam
     | Sg _ ->
       Format.fprintf fmt "<sg>"
-    | Signature sign ->
-      Format.fprintf fmt "sig[%a]" pp_sign sign
+    | Symbol ->
+      Format.fprintf fmt "<symbol>"
+    | Telescope ->
+      Format.fprintf fmt "<tele>"
+    | Signature tele ->
+      Format.fprintf fmt "sig[%a]" pp_con tele
     | Sub _ ->
       Format.fprintf fmt "<sub>"
     | TpPrf _ ->
@@ -246,6 +242,7 @@ struct
     | `Ext _ -> Format.fprintf fmt "<code-ext>"
     | `Pi _ -> Format.fprintf fmt "<code-pi>"
     | `Sg _ -> Format.fprintf fmt "<code-sg>"
+    | `Telescope -> Format.fprintf fmt "<code-tele>"
     | `Signature _ -> Format.fprintf fmt "<code-sig>"
     | `Nat -> Format.fprintf fmt "<code-nat>"
     | `Circle -> Format.fprintf fmt "<code-circle>"

src/core/Domain.mli

@@ -28,8 +28,6 @@ module Make : functor (Symbol : Symbol.S) -> sig
   val tm_abort : con
   val tp_abort : tp
 
-  val sign_lbls : sign -> Ident.user list
-
   (** {1 Pretty-printers }
 
       These are only for debugging. *)
@@ -43,5 +41,4 @@ module Make : functor (Symbol : Symbol.S) -> sig
   val pp_hd : hd Pp.printer
   val pp_frame : frm Pp.printer
   val pp_spine : frm list Pp.printer
-  val pp_sign : sign Pp.printer
 end

src/core/DomainData.ml

@@ -17,7 +17,10 @@ struct
     | `Sg of 'a * 'a
     (** Dependent sum type *)
 
-    | `Signature of (Ident.user * 'a) list
+    | `Telescope
+    (** The universe of telescopes *)
+
+    | `Signature of 'a
     (** First-Class Record types *)
 
     | `Ext of int * 'a * [`Global of 'a] * 'a
@@ -48,10 +51,12 @@ struct
   and 'a clo = Clo of 'a * env
   and tp_clo = S.tp clo
   and tm_clo = S.t clo
-  and sign_clo = S.sign clo
 
   (** Value constructors are governed by {!type:con}; we do not maintain in the datatype {i a priori} any invariant that these represent whnfs (weak head normal forms). Whether a value constructor is a whnf is contingent on the ambient local state, such as the cofibration theory. *)
   and con =
+    | Quoted of Ident.user
+    (** A quoted identifier. *)
+
     | Lam of Ident.t * tm_clo
 
     | BindSym of DimProbe.t * con
@@ -68,9 +73,14 @@ struct
     | Base
     | Loop of dim
     | Pair of con * con
+
+    (* [TODO: Reed M, 26/01/2022] Does it make sense to handle these in a similar way to codes? *)
+    | TeleNil
+    | TeleCons of con * con * con
+
     | Struct of (Ident.user * con) list
-    | SubIn of con
 
+    | SubIn of con
     | ElIn of con
     (** The introduction form for the extension of a {i stable} type code only (see {!constructor:ElStable}). *)
 
@@ -83,7 +93,7 @@ struct
 
     | Prf
 
-    | FHCom of [`Nat | `Circle] * dim * dim * cof * con
+    | FHCom of [`Telescope | `Nat | `Circle] * dim * dim * cof * con
 
     | StableCode of con stable_code
     | UnstableCode of con unstable_code
@@ -107,14 +117,13 @@ struct
     | TpSplit of (cof * tp_clo) list
     | Pi of tp * Ident.t * tp_clo
     | Sg of tp * Ident.t * tp_clo
-    | Signature of sign
+    | Symbol
+    | Telescope
+    | Signature of con
     | Nat
     | Circle
     | TpLockedPrf of cof
 
-  and sign =
-    | Field of Ident.user * 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. *)
   and hd =
@@ -135,9 +144,11 @@ struct
     | KAp of tp * con
     | KFst
     | KSnd
+    | KPush of con * con * con
     | KProj of Ident.user
     | KNatElim of con * con * con
     | KCircleElim of con * con * con
+    | KTeleElim of con * con * con
 
     | KElOut
     (** The elimination form for the extension of a {i stable} type code only (see {!constructor:ElStable}). *)