diff --git a/cooltt-lib b/cooltt-lib new file mode 100644 index 000000000..30e36ec40 --- /dev/null +++ b/cooltt-lib @@ -0,0 +1 @@ +{ "format": "1.0.0" } \ No newline at end of file diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml index 4c248ac01..b17faa033 100644 --- a/src/core/Conversion.ml +++ b/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 () | _ -> diff --git a/src/core/Domain.ml b/src/core/Domain.ml index fa13afa35..d198d0249 100644 --- a/src/core/Domain.ml +++ b/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 "" | KCircleElim _ -> Format.fprintf fmt "" - | KElOut -> Uuseg_string.pp_utf_8 fmt "⭝ₑₗ" + | KTeleElim _ -> Format.fprintf fmt "" + | KPush _ -> Format.fprintf fmt "" + | 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 "" - - 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 "" - | Signature sign -> - Format.fprintf fmt "sig[%a]" pp_sign sign + | Symbol -> + Format.fprintf fmt "" + | Telescope -> + Format.fprintf fmt "" + | Signature tele -> + Format.fprintf fmt "sig[%a]" pp_con tele | Sub _ -> Format.fprintf fmt "" | TpPrf _ -> @@ -246,6 +242,7 @@ struct | `Ext _ -> Format.fprintf fmt "" | `Pi _ -> Format.fprintf fmt "" | `Sg _ -> Format.fprintf fmt "" + | `Telescope -> Format.fprintf fmt "" | `Signature _ -> Format.fprintf fmt "" | `Nat -> Format.fprintf fmt "" | `Circle -> Format.fprintf fmt "" diff --git a/src/core/Domain.mli b/src/core/Domain.mli index ea53d28e0..4eade2079 100644 --- a/src/core/Domain.mli +++ b/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 diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml index d2ce93cf0..e5f663670 100644 --- a/src/core/DomainData.ml +++ b/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}). *) diff --git a/src/core/Quote.ml b/src/core/Quote.ml index 1bb4a059f..d0fa6a720 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -81,6 +81,9 @@ let rec quote_con (tp : D.tp) con = S.Var ix end + | _, D.Quoted id -> + ret @@ S.Quoted id + | _, D.Cut {cut = (hd, sp); tp = _} -> quote_cut (hd, sp) @@ -104,6 +107,22 @@ let rec quote_con (tp : D.tp) con = and+ tsnd = quote_con fib snd in S.Pair (tfst, tsnd) + | _, D.TeleNil -> + ret S.TeleNil + + | _, D.TeleCons (qid, code, tele) -> + let* tele_tp = + lift_cmp @@ + Sem.splice_tp @@ + Splice.con code @@ fun code -> + Splice.term @@ + TB.pi (TB.el @@ code) (fun _ -> TB.telescope) + in + let* qid = quote_con D.Symbol qid in + let* code = quote_con D.Univ code in + let+ tele = quote_con tele_tp tele in + S.TeleCons (qid, code, tele) + | D.Signature sign, _ -> let+ tfields = quote_fields sign con in S.Struct tfields @@ -280,15 +299,18 @@ let rec quote_con (tp : D.tp) con = Format.eprintf "bad: %a / %a@." D.pp_tp tp D.pp_con con; throw @@ QuotationError (Error.IllTypedQuotationProblem (tp, con)) -and quote_fields (sign : D.sign) con : (Ident.user * S.t) list m = - match sign with - | D.Field (lbl, tp, sign_clo) -> - let* fcon = lift_cmp @@ do_proj con lbl in - let* sign = lift_cmp @@ inst_sign_clo sign_clo fcon in +and quote_fields (tele : D.con) con : (Ident.user * S.t) list m = + match tele with + | D.TeleCons (qid, code, lam) -> + let* id = lift_cmp @@ unquote qid in + let* fcon = lift_cmp @@ do_proj con id in + let* tp = lift_cmp @@ do_el code in + let* tele = lift_cmp @@ do_ap lam fcon in let* tfield = quote_con tp fcon in - let+ tfields = quote_fields sign con in - (lbl, tfield) :: tfields - | D.Empty -> ret [] + let+ tfields = quote_fields tele con in + (id, tfield) :: tfields + | D.TeleNil -> ret [] + | _ -> failwith "internal error: quote_fields" and quote_stable_field_code univ args (lbl, fam) = (* See [NOTE: Sig Code Quantifiers] for more details *) @@ -312,6 +334,9 @@ and quote_stable_code univ = | `Circle -> ret S.CodeCircle + | `Telescope -> + ret S.CodeTelescope + | `Univ -> ret S.CodeUniv @@ -336,10 +361,9 @@ and quote_stable_code univ = lift_cmp @@ do_ap fam var in S.CodeSg (tbase, tfam) - | `Signature fields -> - let+ tfields = MU.map_accum_left_m (quote_stable_field_code univ) fields - in - S.CodeSignature tfields + | `Signature tele -> + let+ tele = quote_con D.Telescope tele in + S.CodeSignature tele | `Ext (n, code, `Global phi, bdry) -> let+ tphi = @@ -406,16 +430,6 @@ and quote_tp_clo base fam = let* tp = lift_cmp @@ inst_tp_clo fam var in quote_tp tp -and quote_sign : D.sign -> S.sign m = - function - | Field (ident, field, clo) -> - let* tfield = quote_tp field in - bind_var field @@ fun var -> - let* fields = lift_cmp @@ inst_sign_clo clo var in - let+ tfields = quote_sign fields in - (ident, tfield) :: tfields - | Empty -> ret [] - and quote_tp (tp : D.tp) = let* veil = read_veil in let* tp = contractum_or tp <@> lift_cmp @@ Sem.whnf_tp ~style:(`Veil veil) tp in @@ -430,9 +444,13 @@ and quote_tp (tp : D.tp) = let* tbase = quote_tp base in let+ tfam = quote_tp_clo base fam in S.Sg (tbase, ident, tfam) - | D.Signature sign -> - let+ sign = quote_sign sign in - S.Signature sign + | D.Symbol -> + ret S.Symbol + | D.Telescope -> + ret S.Telescope + | D.Signature tele -> + let+ tele = quote_con D.Telescope tele in + S.Signature tele | D.Univ -> ret S.Univ | D.ElStable code -> @@ -641,6 +659,38 @@ and quote_frm tm = in let* tloop_case = quote_con loop_tp loop_case in ret @@ S.CircleElim (tmot, tbase_case, tloop_case, tm) + | D.KPush (qid, code, field) -> + let* tqid = quote_con D.Symbol qid in + let* tcode = quote_con D.Univ code in + let* tp = lift_cmp @@ Sem.do_el code in + let+ tfield = quote_con tp field in + S.Push (tqid, tcode, tfield, tm) + | D.KTeleElim (mot, nil_case, cons_case) -> + let* mot_tp = + lift_cmp @@ + Sem.splice_tp @@ + Splice.term @@ + TB.pi TB.telescope @@ fun _ -> TB.univ + in + let* tmot = quote_con mot_tp mot in + let* tnil_case = + let* mot_nil = lift_cmp @@ do_ap mot D.TeleNil in + let* tp_mot_nil = lift_cmp @@ do_el mot_nil in + quote_con tp_mot_nil nil_case + in + let* cons_tp = + lift_cmp @@ + Sem.splice_tp @@ + Splice.con mot @@ 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 + let+ tcons_case = quote_con cons_tp cons_case in + S.TeleElim (tmot, tnil_case, tcons_case, tm) | D.KFst -> ret @@ S.Fst tm | D.KSnd -> diff --git a/src/core/Quote.mli b/src/core/Quote.mli index 3a4fe5cec..8976da48f 100644 --- a/src/core/Quote.mli +++ b/src/core/Quote.mli @@ -7,7 +7,6 @@ module S := Syntax val quote_con : D.tp -> D.con -> S.t quote val quote_tp : D.tp -> S.tp quote -val quote_sign : D.sign -> S.sign quote val quote_cut : D.cut -> S.t quote val quote_cof : D.cof -> S.t quote val quote_dim : D.dim -> S.t quote diff --git a/src/core/RefineError.ml b/src/core/RefineError.ml index ca31f4ea7..367066847 100644 --- a/src/core/RefineError.ml +++ b/src/core/RefineError.ml @@ -18,6 +18,10 @@ let pp_connective fmt = Format.fprintf fmt "pi" | `Sg -> Format.fprintf fmt "sg" + | `Symbol -> + Format.fprintf fmt "symbol" + | `Telescope -> + Format.fprintf fmt "tele" | `Signature -> Format.fprintf fmt "sig" | `Univ -> @@ -67,7 +71,7 @@ let pp fmt = "Expected true cofibration: %a" (S.pp ppenv) cof | ExpectedField (ppenv, sign, tm, lbl) -> - Fmt.fprintf fmt "Expected (%a : sig %a) to have field %a" (S.pp ppenv) tm (S.pp_sign ppenv) sign Ident.pp_user lbl + Fmt.fprintf fmt "Expected (%a : sig %a) to have field %a" (S.pp ppenv) tm (S.pp ppenv) sign Ident.pp_user lbl | FieldNameMismatches (expected, actual) -> Fmt.fprintf fmt "Field names mismatch, expected [%a] but got [%a]" (Pp.pp_sep_list Ident.pp_user) expected (Pp.pp_sep_list Ident.pp_user) actual | VirtualType -> diff --git a/src/core/RefineErrorData.ml b/src/core/RefineErrorData.ml index 157a85d2f..c5b1a0925 100644 --- a/src/core/RefineErrorData.ml +++ b/src/core/RefineErrorData.ml @@ -10,6 +10,8 @@ struct type connective = [ `Pi | `Sg + | `Symbol + | `Telescope | `Signature | `Nat | `Circle @@ -27,7 +29,7 @@ struct type t = | UnboundVariable of Ident.t | FieldNameMismatches of Ident.user list * Ident.user list - | ExpectedField of Pp.env * S.sign * S.t * Ident.user + | ExpectedField of Pp.env * S.t * S.t * Ident.user | ExpectedEqual of Pp.env * S.tp * S.t * S.t * Conversion.Error.t | ExpectedEqualTypes of Pp.env * S.tp * S.tp * Conversion.Error.t | ExpectedConnective of connective * Pp.env * S.tp diff --git a/src/core/RefineMonad.ml b/src/core/RefineMonad.ml index 71ad65880..5f6906a44 100644 --- a/src/core/RefineMonad.ml +++ b/src/core/RefineMonad.ml @@ -89,9 +89,6 @@ let quote_con tp con = let quote_tp tp = lift_qu @@ Qu.quote_tp tp -let quote_sign sign = - lift_qu @@ Qu.quote_sign sign - let quote_cut cut = lift_qu @@ Qu.quote_cut cut @@ -144,7 +141,7 @@ let expected_connective conn tp = let expected_field sign con lbl = with_pp @@ fun ppenv -> - let* tsign = quote_sign sign in + let* tsign = quote_con D.Telescope sign in refine_err @@ Err.ExpectedField (ppenv, tsign, con, lbl) let field_names_mismatch ~expected ~actual = diff --git a/src/core/RefineMonad.mli b/src/core/RefineMonad.mli index dd69b72eb..23e89b6e5 100644 --- a/src/core/RefineMonad.mli +++ b/src/core/RefineMonad.mli @@ -42,5 +42,5 @@ val equate : D.tp -> D.con -> D.con -> unit m val with_pp : (Pp.env -> 'a m) -> 'a m val expected_connective : RefineError.connective -> D.tp -> 'a m -val expected_field : D.sign -> S.t -> Ident.user -> 'a m +val expected_field : D.con -> S.t -> Ident.user -> 'a m val field_names_mismatch : expected:Ident.user list -> actual:Ident.user list -> 'a m diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 87e3b556e..9b77f843c 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -521,18 +521,99 @@ struct RM.expected_connective `Sg tp end +module Symbol = +struct + let formation : T.Tp.tac = + T.Tp.virtual_rule ~name:"Symbol.formation" @@ + RM.ret S.Symbol + + let quote id : T.Chk.tac = + T.Chk.rule ~name:"Symbol.quote" @@ + function + | D.Symbol -> RM.ret @@ S.Quoted id + | tp -> RM.expected_connective `Symbol tp + +end + +module Telescope = +struct + let formation : T.Tp.tac = + T.Tp.rule ~name:"Telescope.formation" @@ + RM.ret S.Telescope + + let assert_tele = + function + | D.Telescope -> RM.ret () + | tp -> RM.expected_connective `Nat tp + + let nil : T.Chk.tac = + T.Chk.rule ~name:"Telescope.nil" @@ + fun tp -> + let+ () = assert_tele tp in + S.TeleNil + + (* [TODO: Reed M, 26/01/2022] Boundaries? *) + let cons (qid_tac : T.Chk.tac) (tac_code : T.Chk.tac) (tac_tele : T.Chk.tac) = + T.Chk.rule ~name:"Telescope.cons" @@ + fun tp -> + let* () = assert_tele tp in + let* qid = T.Chk.run qid_tac D.Symbol in + let* code = T.Chk.run tac_code D.Univ in + let* vcode = RM.lift_ev @@ Sem.eval code in + let* tele_tp = + RM.lift_cmp @@ + Sem.splice_tp @@ + Splice.con vcode @@ fun code -> + Splice.term @@ TB.pi (TB.el code) (fun _ -> TB.telescope) + in + let+ tele = T.Chk.run tac_tele tele_tp in + S.TeleCons (qid, code, tele) + + let elim (mot_tac : T.Chk.tac) (nil_case_tac : T.Chk.tac) (cons_case_tac : T.Chk.tac) (scrut_tac : T.Syn.tac) : T.Syn.tac = + T.Syn.rule ~name:"Telescope.elim" @@ + let* tscrut, teletp = T.Syn.run scrut_tac in + let* () = assert_tele teletp in + let* tmot = + T.Chk.run mot_tac @<< + RM.lift_cmp @@ Sem.splice_tp @@ + Splice.term @@ + TB.pi TB.telescope @@ fun _ -> TB.univ + in + let* vmot = RM.lift_ev @@ Sem.eval tmot in + + let* tcase_nil = + let* code = RM.lift_cmp @@ Sem.do_ap vmot D.TeleNil in + let* tp = RM.lift_cmp @@ Sem.do_el code in + T.Chk.run nil_case_tac tp + in + + let* tcase_cons = + let* cons_tp = + RM.lift_cmp @@ Sem.splice_tp @@ + Splice.con vmot @@ 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 + T.Chk.run cons_case_tac cons_tp + in + let+ fib_scrut = + let* vscrut = RM.lift_ev @@ Sem.eval tscrut in + let* code = RM.lift_cmp @@ Sem.do_ap vmot vscrut in + RM.lift_cmp @@ Sem.do_el code + in + S.TeleElim (tmot, tcase_nil, tcase_cons, tscrut), fib_scrut +end module Signature = struct - let formation (tacs : T.Tp.tac telescope) : T.Tp.tac = - let rec form_fields tele = - function - | Bind (lbl, tac, tacs) -> - let* tp = T.Tp.run tac in - let* vtp = RM.lift_ev @@ Sem.eval_tp tp in - T.abstract ~ident:(lbl :> Ident.t) vtp @@ fun var -> form_fields (Snoc (tele, (lbl, tp))) (tacs var) - | Done -> RM.ret @@ S.Signature (Bwd.to_list tele) - in T.Tp.rule ~name:"Signature.formation" @@ form_fields Emp tacs + let formation (tele_tac : T.Chk.tac) : T.Tp.tac = + T.Tp.rule ~name:"Signature.formation" @@ + let+ tele = T.Chk.run tele_tac D.Telescope in + S.Signature tele let rec find_field_tac (fields : (Ident.user * T.Chk.tac) list) (lbl : Ident.user) : T.Chk.tac option = match fields with @@ -543,21 +624,24 @@ struct | [] -> None - - let rec intro_fields phi phi_clo (sign : D.sign) (tacs : Ident.user -> T.Chk.tac option) : (Ident.user * S.t) list m = - match sign with - | D.Field (lbl, tp, sign_clo) -> - let tac = match tacs lbl with + let rec intro_fields phi phi_clo (tele : D.con) (tacs : Ident.user -> T.Chk.tac option) : (Ident.user * S.t) list m = + match tele with + | D.TeleCons (qid, code, lam) -> + (* [TODO: Reed M, 27/01/2022] Fishy? *) + let* id = RM.lift_cmp @@ Sem.unquote qid in + let tac = match tacs id with | Some tac -> tac - | None -> Hole.unleash_hole (Ident.user_to_string_opt lbl) + | None -> Hole.unleash_hole (Ident.user_to_string_opt id) in - let* tfield = T.Chk.brun tac (tp, phi, D.un_lam @@ D.compose (D.proj lbl) @@ D.Lam (`Anon, phi_clo)) in + let* tp = RM.lift_cmp @@ Sem.do_el code in + let* tfield = T.Chk.brun tac (tp, phi, D.un_lam @@ D.compose (D.proj id) @@ D.Lam (`Anon, phi_clo)) in let* vfield = RM.lift_ev @@ Sem.eval tfield in - let* tsign = RM.lift_cmp @@ Sem.inst_sign_clo sign_clo vfield in - let+ tfields = intro_fields phi phi_clo tsign tacs in - (lbl, tfield) :: tfields - | D.Empty -> + let* tele = RM.lift_cmp @@ Sem.do_ap lam vfield in + let+ fields = intro_fields phi phi_clo tele tacs in + (id, tfield) :: fields + | D.TeleNil -> RM.ret [] + | _ -> failwith "[FIXME] Containers.Signature.intro_fields: Handle this case better! This could be a cut!" let intro (tacs : Ident.user -> T.Chk.tac option) : T.Chk.tac = T.Chk.brule ~name:"Signature.intro" @@ @@ -567,16 +651,20 @@ struct S.Struct fields | (tp, _, _) -> RM.expected_connective `Signature tp - let proj_tp (sign : D.sign) (tstruct : S.t) (lbl : Ident.user) : D.tp m = + let proj_tp (tele : D.con) (tstruct : S.t) (proj_id : Ident.user) : D.tp m = let rec go = function - | D.Field (flbl, tp, _) when Ident.equal flbl lbl -> RM.ret tp - | D.Field (flbl, __, clo) -> - let* vfield = RM.lift_ev @@ Sem.eval @@ S.Proj (tstruct, flbl) in - let* vsign = RM.lift_cmp @@ Sem.inst_sign_clo clo vfield in - go vsign - | D.Empty -> RM.expected_field sign tstruct lbl - in go sign + | D.TeleCons (qid, code, lam) -> + let* id = RM.lift_cmp @@ Sem.unquote qid in + if Ident.equal id proj_id then + RM.lift_cmp @@ Sem.do_el code + else + let* id = RM.lift_cmp @@ Sem.unquote qid in + let* vfield = RM.lift_ev @@ Sem.eval @@ S.Proj (tstruct, id) in + let* vsign = RM.lift_cmp @@ Sem.do_ap lam vfield in + go vsign + | _ -> RM.expected_field tele tstruct proj_id + in go tele let proj tac lbl : T.Syn.tac = T.Syn.rule ~name:"Signature.proj" @@ @@ -659,134 +747,14 @@ struct let+ tp, fam = quantifier tac_base tac_fam univ in S.CodeSg (tp, fam) - (* [NOTE: Sig Code Quantifiers] - When we are creating a code for a signature, we need to make sure - that we can depend on the values of previous fields. To achieve this, - we do something similar to pi/sigma codes, and add in extra pi types to - bind the names of previous fields. As an example, the signature: - sig (x : type) - (y : (arg : x) -> type) - (z : (arg1 : x) -> (arg2 : y) -> type) - will produce the following goals: - type - (x : type) -> type - (x : type) -> (y : type) -> type - and once the tactics for each field are run, we will get the following - signature code (notice the lambdas!): - sig (x : type) - (y : x => (arg : x) -> type) - (z : x => y => (arg1 : x) -> (arg2 : y) -> type) - *) - let signature (tacs : (Ident.user * T.Chk.tac) list) : T.Chk.tac = - univ_tac "Univ.signature" @@ fun univ -> - let+ fields = quantifiers (List.map (fun (lbl, tac) -> (lbl, T.Chk.run tac)) tacs) univ in - S.CodeSignature fields - - (* [NOTE: Patch Quantifiers] - As described in [NOTE: Sig Code Quantifiers], the field types of a signature code - all use lambdas to bind variables from earlier on in the signature. Therefore, - when we construct the patched versions of the field codes, we need to re-insert - the lambdas. - - However, the situation is made more complicated by the fact that we only patching - _some_ of the values of the signature type. This means that we can't just naively - apply the field code to all the previous patch values, as their may not be any patch values - for some fields! - - This requires us to run each of the patch tactics at pi types, which then causes - the patches to be lambdas. This means that we need to do some fancier application - when we construct the final codes. Most notably, we need to make sure to properly - eliminate the 'ext' types introduced by previous patches. - *) - let patch_fields (sign : (Ident.user * D.con) list) (tacs : Ident.user -> T.Chk.tac option) (univ : D.tp) : S.t m = - let rec go (field_names : Ident.user list) (codes : D.con list) (elim_conns : (S.t TB.m -> S.t TB.m) list) sign = - match sign with - | (field_name, vfield_tp) :: sign -> - let* (code, elim_conn) = - match tacs field_name with - | Some tac -> - let* patch_tp = - RM.lift_cmp @@ - Sem.splice_tp @@ - Splice.con vfield_tp @@ fun field_tp -> - Splice.cons codes @@ fun codes -> Splice.term @@ TB.pis ~idents:(field_names :> Ident.t list) codes @@ fun args -> TB.el @@ TB.ap field_tp @@ ListUtil.zip_with (@@) elim_conns args - in - let* patch = T.Chk.run tac patch_tp in - let* vpatch = RM.lift_ev @@ Sem.eval patch in - let+ ext_code = - RM.lift_cmp @@ - Sem.splice_tm @@ - Splice.con vfield_tp @@ fun field_tp -> - Splice.con vpatch @@ fun patch -> - Splice.term @@ TB.lams (field_names :> Ident.t list) @@ fun args -> TB.code_ext 0 (TB.ap field_tp @@ ListUtil.zip_with (@@) elim_conns args) TB.top @@ TB.lam @@ fun _ -> TB.ap patch args - in - (ext_code, fun arg -> TB.sub_out @@ TB.el_out arg) - | None -> - let+ code = - RM.lift_cmp @@ - Sem.splice_tm @@ - Splice.con vfield_tp @@ fun field_tp -> - Splice.term @@ TB.lams (field_names :> Ident.t list) @@ fun args -> TB.ap field_tp @@ ListUtil.zip_with (@@) elim_conns args - in - (code, Fun.id) - in - go (field_names @ [field_name]) (codes @ [code]) (elim_conns @ [elim_conn]) sign - | [] -> - let* qsign = quote_sign_codes (List.combine field_names codes) univ in - RM.ret @@ S.CodeSignature qsign - in go [] [] [] sign + let tele : T.Chk.tac = + univ_tac "Univ.tele" @@ fun _ -> + RM.ret S.CodeTelescope - let patch (sig_tac : T.Chk.tac) (tacs : Ident.user -> T.Chk.tac option) : T.Chk.tac = - univ_tac "Univ.patch" @@ fun univ -> - let* code = T.Chk.run sig_tac univ in - let* vcode = RM.lift_ev @@ Sem.eval code in - let* tp = RM.lift_cmp @@ Sem.do_el vcode in - let* whnf_tp = RM.lift_cmp @@ Sem.whnf_tp_ ~style:`UnfoldAll tp in - match whnf_tp with - | D.ElStable (`Signature sign) -> - patch_fields sign tacs univ - | _ -> - RM.expected_connective `Signature whnf_tp - - let total (fam_tac : T.Syn.tac) : T.Chk.tac = - univ_tac "Univ.total" @@ fun univ -> - let* (tm, tp) = T.Syn.run fam_tac in - let* vtm = RM.lift_ev @@ Sem.eval tm in - match tp with - | D.Pi (D.ElStable (`Signature vsign) as base, ident, clo) -> - (* HACK: Because we are using Weak Tarski Universes, we can't just - use the conversion checker to equate 'fam' and 'univ', as - 'fam' may be 'el code-univ' instead. - - Therefore, we do an explicit check here instead. - If we add universe levels, this code should probably be reconsidered. *) - let* _ = T.abstract ~ident base @@ fun var -> - let* fam = RM.lift_cmp @@ Sem.inst_tp_clo clo (T.Var.con var) in - match fam with - | D.Univ -> RM.ret () - | D.ElStable `Univ -> RM.ret () - | _ -> RM.expected_connective `Univ fam - in - let (sign_names, vsign_codes) = List.split vsign in - let* qsign = quote_sign_codes vsign univ in - (* See [NOTE: Sig Code Quantifiers]. *) - let* fib_tp = - RM.lift_cmp @@ - Sem.splice_tp @@ - Splice.tp univ @@ fun univ -> - Splice.cons vsign_codes @@ fun sign_codes -> - Splice.term @@ TB.pis ~idents:(sign_names :> Ident.t list) sign_codes @@ fun _ -> univ - in - let* fib = - RM.lift_cmp @@ - Sem.splice_tm @@ - Splice.con vtm @@ fun tm -> - Splice.term @@ TB.lams (sign_names :> Ident.t list) @@ fun args -> TB.el_out @@ TB.ap tm [TB.el_in @@ TB.struct_ @@ List.combine sign_names args] - in - let+ qfib = RM.quote_con fib_tp fib in - S.CodeSignature (qsign @ [`User ["fib"], qfib]) - | D.Pi (base, _, _) -> RM.expected_connective `Signature base - | _ -> RM.expected_connective `Pi tp + let signature (tele_tac : T.Chk.tac) : T.Chk.tac = + univ_tac "Univ.signature" @@ fun _ -> + let+ tele = T.Chk.run tele_tac D.Telescope in + S.CodeSignature tele let ext (n : int) (tac_fam : T.Chk.tac) (tac_cof : T.Chk.tac) (tac_bdry : T.Chk.tac) : T.Chk.tac = univ_tac "Univ.ext" @@ fun univ -> diff --git a/src/core/Refiner.mli b/src/core/Refiner.mli index 8a9af8743..77bae8b82 100644 --- a/src/core/Refiner.mli +++ b/src/core/Refiner.mli @@ -61,9 +61,8 @@ module Univ : sig val circle : Chk.tac val pi : Chk.tac -> Chk.tac -> Chk.tac val sg : Chk.tac -> Chk.tac -> Chk.tac - val signature : (Ident.user * Chk.tac) list -> Chk.tac - val patch : Chk.tac -> (Ident.user -> Chk.tac option) -> Chk.tac - val total : Syn.tac -> Chk.tac + val tele : Chk.tac + val signature : Chk.tac -> Chk.tac val ext : int -> Chk.tac -> Chk.tac -> Chk.tac -> Chk.tac val code_v : Chk.tac -> Chk.tac -> Chk.tac -> Chk.tac -> Chk.tac val coe : Chk.tac -> Chk.tac -> Chk.tac -> Chk.tac -> Syn.tac @@ -101,8 +100,20 @@ module Sg : sig val pi2 : Syn.tac -> Syn.tac end +module Symbol : sig + val formation : Tp.tac + val quote : Ident.user -> Chk.tac +end + +module Telescope : sig + val formation : Tp.tac + val nil : Chk.tac + val cons : Chk.tac -> Chk.tac -> Chk.tac -> Chk.tac + val elim : Chk.tac -> Chk.tac -> Chk.tac -> Syn.tac -> Syn.tac +end + module Signature : sig - val formation : Tp.tac telescope -> Tp.tac + val formation : Chk.tac -> Tp.tac val intro : (Ident.user -> Chk.tac option) -> Chk.tac val proj : Syn.tac -> Ident.user -> Syn.tac diff --git a/src/core/Semantics.ml b/src/core/Semantics.ml index a1e099c6c..75bb0bdfb 100644 --- a/src/core/Semantics.ml +++ b/src/core/Semantics.ml @@ -176,7 +176,7 @@ and push_subst_con : D.dim -> DimProbe.t -> D.con -> D.con CM.m = fun r x -> let open CM in function - | D.Dim0 | D.Dim1 | D.Prf | D.Zero | D.Base | D.StableCode (`Nat | `Circle | `Univ) as con -> ret con + | D.Quoted _ | D.Dim0 | D.Dim1 | D.Prf | D.Zero | D.Base | D.StableCode (`Nat | `Circle | `Univ) as con -> ret con | D.LetSym (s, y, con) -> push_subst_con r x @<< push_subst_con s y con | D.Suc con -> @@ -202,6 +202,12 @@ and push_subst_con : D.dim -> DimProbe.t -> D.con -> D.con CM.m = let+ con0 = subst_con r x con0 and+ con1 = subst_con r x con1 in D.Pair (con0, con1) + | D.TeleNil -> + ret D.TeleNil + | D.TeleCons (id, code, tele) -> + let+ code = push_subst_con r x code + and+ tele = push_subst_con r x tele in + D.TeleCons (id, code, tele) | D.Struct fields -> let+ fields = MU.map (MU.second (subst_con r x)) fields in D.Struct fields @@ -302,12 +308,6 @@ and subst_tp_clo : D.dim -> DimProbe.t -> D.tp_clo -> D.tp_clo CM.m = let+ env = subst_env r x env in D.Clo (tp, env) -and subst_sign_clo : D.dim -> DimProbe.t -> D.sign_clo -> D.sign_clo CM.m = - fun r x (Clo (sign, env)) -> - let open CM in - let+ env = subst_env r x env in - D.Clo (sign, env) - and subst_env : D.dim -> DimProbe.t -> D.env -> D.env CM.m = fun r x {tpenv; conenv} -> let open CM in @@ -315,16 +315,6 @@ and subst_env : D.dim -> DimProbe.t -> D.env -> D.env CM.m = and+ conenv = MU.map_bwd (subst_con r x) conenv in D.{tpenv; conenv} -and subst_sign : D.dim -> DimProbe.t -> D.sign -> D.sign CM.m = - fun r x -> - let open CM in - function - | D.Field (ident, tp, clo) -> - let+ tp = subst_tp r x tp - and+ clo = subst_sign_clo r x clo in - D.Field (ident, tp, clo) - | D.Empty -> ret D.Empty - and subst_tp : D.dim -> DimProbe.t -> D.tp -> D.tp CM.m = fun r x -> let open CM in @@ -337,15 +327,15 @@ and subst_tp : D.dim -> DimProbe.t -> D.tp -> D.tp CM.m = let+ base = subst_tp r x base and+ fam = subst_tp_clo r x fam in D.Sg (base, ident, fam) - | D.Signature sign -> - let+ sign = subst_sign r x sign in - D.Signature sign + | D.Signature tele -> + let+ tele = subst_con r x tele in + D.Signature tele | D.Sub (base, phi, clo) -> let+ base = subst_tp r x base and+ phi = subst_cof r x phi and+ clo = subst_clo r x clo in D.Sub (base, phi, clo) - | D.Univ | D.Nat | D.Circle | D.TpDim | D.TpCof as con -> ret con + | D.Symbol | D.Telescope | D.Univ | D.Nat | D.Circle | D.TpDim | D.TpCof as con -> ret con | D.TpPrf phi -> let+ phi = subst_cof r x phi in D.TpPrf phi @@ -391,14 +381,14 @@ and subst_stable_code : D.dim -> DimProbe.t -> D.con D.stable_code -> D.con D.st let+ con0 = subst_con r x con0 and+ con1 = subst_con r x con1 in `Sg (con0, con1) - | `Signature fields -> - let+ fields = MU.map (MU.second (subst_con r x)) fields in - `Signature fields + | `Signature tele -> + let+ tele = subst_con r x tele in + `Signature tele | `Ext (n, code, `Global cof, con) -> let+ code = subst_con r x code and+ con = subst_con r x con in `Ext (n, code, `Global cof, con) - | `Nat | `Circle | `Univ as code -> + | `Nat | `Circle | `Telescope | `Univ as code -> ret code and subst_cut : D.dim -> DimProbe.t -> D.cut -> D.cut CM.m = @@ -476,21 +466,21 @@ and subst_frm : D.dim -> DimProbe.t -> D.frm -> D.frm CM.m = and+ con1 = subst_con r x con1 and+ con2 = subst_con r x con2 in D.KCircleElim (con0, con1, con2) + | D.KTeleElim (con0, con1, con2) -> + let+ con0 = subst_con r x con0 + and+ con1 = subst_con r x con1 + and+ con2 = subst_con r x con2 in + D.KTeleElim (con0, con1, con2) + | D.KPush (lbl, con0, con1) -> + let+ con0 = subst_con r x con0 + and+ con1 = subst_con r x con1 in + D.KPush (lbl, con0, con1) and subst_sp : D.dim -> DimProbe.t -> D.frm list -> D.frm list CM.m = fun r x -> CM.MU.map @@ subst_frm r x -and eval_sign : S.sign -> D.sign EvM.m = - let open EvM in - function - | [] -> ret D.Empty - | (ident, field) :: fields -> - let+ env = read_local - and+ vfield = eval_tp field in - D.Field (ident, vfield, D.Clo (fields, env)) - and eval_tp : S.tp -> D.tp EvM.m = let open EvM in function @@ -504,9 +494,13 @@ and eval_tp : S.tp -> D.tp EvM.m = let+ env = read_local and+ vbase = eval_tp base in D.Sg (vbase, ident, D.Clo (fam, env)) - | S.Signature sign -> - let+ vsign = eval_sign sign in - D.Signature vsign + | S.Symbol -> + ret D.Symbol + | S.Telescope -> + ret D.Telescope + | S.Signature tele -> + let+ tele = eval tele in + D.Signature tele | S.Univ -> ret D.Univ | S.El tm -> @@ -554,6 +548,8 @@ and eval : S.t -> D.con EvM.m = append [vdef] @@ eval body | S.Ann (term, _) -> eval term + | S.Quoted id -> + ret @@ D.Quoted id | S.Zero -> ret D.Zero | S.Suc t -> @@ -599,9 +595,28 @@ and eval : S.t -> D.con EvM.m = | S.Snd t -> let* con = eval t in lift_cmp @@ do_snd con + | S.TeleNil -> + ret D.TeleNil + | S.TeleCons (qid, code, tele) -> + let+ qid = eval qid + and+ code = eval code + and+ tele = eval tele in + D.TeleCons (qid, code, tele) + | S.TeleElim (mot, nil, cons, tele) -> + let* mot = eval mot in + let* nil = eval nil in + let* cons = eval cons in + let* tele = eval tele in + lift_cmp @@ do_tele_elim mot nil cons tele | S.Struct fields -> let+ vfields = MU.map (MU.second eval) fields in D.Struct vfields + | S.Push (qid, code, field, str) -> + let* qid = eval qid in + let* code = eval code in + let* field = eval field in + let* str = eval str in + lift_cmp @@ do_push qid code field str | S.Proj (t, lbl) -> let* con = eval t in lift_cmp @@ do_proj con lbl @@ -700,12 +715,14 @@ and eval : S.t -> D.con EvM.m = let+ vbase = eval base and+ vfam = eval fam in D.StableCode (`Sg (vbase, vfam)) - | S.CodeSignature fields -> - let+ vfields = fields |> MU.map @@ fun (ident, tp) -> - let+ vtp = eval tp in - (ident, vtp) - in - D.StableCode (`Signature vfields) + + | S.CodeTelescope -> + ret (D.StableCode `Telescope) + + | S.CodeSignature tele -> + let+ tele = eval tele in + D.StableCode (`Signature tele) + | S.CodeNat -> ret @@ D.StableCode `Nat @@ -811,7 +828,9 @@ and eval_cof tphi = and whnf_con ~style : D.con -> D.con whnf CM.m = let open CM in function - | D.Lam _ | D.BindSym _ | D.Zero | D.Suc _ | D.Base | D.Pair _ | D.Struct _ | D.SubIn _ | D.ElIn _ | D.LockedPrfIn _ + | D.Quoted _ | D.Lam _ | D.BindSym _ | D.Zero | D.Suc _ | D.Base + | D.Pair _ | D.TeleNil | D.TeleCons _ | D.Struct _ + | D.SubIn _ | D.ElIn _ | D.LockedPrfIn _ | D.Cof _ | D.Dim0 | D.Dim1 | D.Prf | D.StableCode _ | D.DimProbe _ -> ret `Done | D.LetSym (r, x, con) -> @@ -1120,12 +1139,6 @@ and inst_tm_clo : D.tm_clo -> D.con -> D.con CM.m = CM.lift_ev {env with conenv = Snoc (env.conenv, x)} @@ eval bdy -and inst_sign_clo : D.sign_clo -> D.con -> D.sign CM.m = - fun clo x -> - match clo with - | D.Clo (sign, env) -> - CM.lift_ev {env with conenv = Snoc (env.conenv, x)} @@ eval_sign sign - (* reduces a constructor to something that is stable to pattern match on *) and whnf_inspect_con ~style con = let open CM in @@ -1189,18 +1202,116 @@ and do_snd con : D.con CM.m = throw @@ NbeFailed ("Couldn't snd argument in do_snd") end -and cut_frm_sign (cut : D.cut) (sign : D.sign) (lbl : Ident.user) = +(** We are trying to compute the type of the cute here? *) +and cut_frm_tele (cut : D.cut) (tele : D.con) (cut_id : Ident.user) = let open CM in - match sign with - | D.Field (flbl, tp, _) when Ident.equal flbl lbl -> ret @@ cut_frm ~tp ~cut (D.KProj lbl) - | D.Field (flbl, _, clo) -> - (* FIXME: Is this right?? *) - let* field = cut_frm_sign cut sign flbl in - let* sign = inst_sign_clo clo field in - cut_frm_sign cut sign lbl - | D.Empty -> + match tele with + | D.TeleCons (qid, code, lam) -> + let* id = unquote qid in + if Ident.equal id cut_id then + let+ tp = do_el code in + cut_frm ~tp ~cut (D.KProj cut_id) + else + let* field = cut_frm_tele cut tele id in + (* NOTE: Recall that we are using lambdas for the "rest" part of a telescope. *) + let* tele = do_ap lam field in + cut_frm_tele cut tele cut_id + | _ -> throw @@ NbeFailed ("Couldn't find field label in cut_frm_sign") +and do_tele_elim (mot : D.con) (nil : D.con) (cons : D.con) (con : D.con) : D.con CM.m = + let open CM in + abort_if_inconsistent (ret D.tm_abort) @@ + begin + inspect_con ~style:`UnfoldNone con |>> + function + | D.TeleNil -> + ret nil + | D.TeleCons (qid, code, tele) -> + splice_tm @@ + Splice.con mot @@ fun mot -> + Splice.con nil @@ fun nil -> + Splice.con cons @@ fun cons -> + Splice.con qid @@ fun qid -> + Splice.con code @@ fun code -> + Splice.con tele @@ fun tele -> + Splice.term @@ + TB.ap cons [qid; code; tele; TB.lam @@ fun x -> TB.tele_elim mot nil cons (TB.ap tele [x])] + | D.Split branches -> + splice_tm @@ + Splice.con mot @@ fun mot -> + Splice.con nil @@ fun nil -> + Splice.con cons @@ fun cons -> + Splice.Macro.commute_split con (List.map fst branches) @@ TB.tele_elim mot nil cons + | D.Cut { cut;_ } -> + let* fib = do_ap mot con in + let+ elfib = do_el fib in + cut_frm ~tp:elfib ~cut @@ + D.KTeleElim (mot, nil, cons) + | D.FHCom (`Telescope, r, s, phi, bdy) -> + splice_tm @@ + Splice.con mot @@ fun mot -> + Splice.dim r @@ fun r -> + Splice.dim s @@ fun s -> + Splice.cof phi @@ fun phi -> + Splice.con bdy @@ fun bdy -> + Splice.con nil @@ fun nil -> + Splice.con cons @@ fun cons -> + Splice.term @@ + let fam = + TB.lam @@ fun i -> + let fhcom = + TB.el_out @@ + TB.hcom TB.code_telescope r i phi @@ + TB.lam @@ fun j -> + TB.lam @@ fun prf -> + TB.el_in @@ TB.ap bdy [j; prf] + in + TB.ap mot [fhcom] + in + let bdy' = + TB.lam @@ fun i -> + TB.lam @@ fun prf -> + TB.tele_elim mot nil cons @@ TB.ap bdy [i; prf] + in + TB.com fam r s phi bdy' + | _ -> + throw @@ NbeFailed ("couldn't eliminate telescope in do_tele_elim") + end + +and do_push (qid : D.con) (code : D.con) (field : D.con) (con : D.con) : D.con CM.m = + let open CM in + abort_if_inconsistent (ret D.tm_abort) @@ + let splitter con phis = + splice_tm @@ + Splice.con qid @@ fun qid -> + Splice.con code @@ fun code -> + Splice.con field @@ fun field -> + Splice.Macro.commute_split con phis (TB.push qid code field) in + begin + inspect_con ~style:`UnfoldNone con |>> + function + | D.Struct fields -> + let+ id = unquote qid in + D.Struct ((id, field) :: fields) + | D.Split branches -> + splitter con @@ List.map fst branches + | D.Cut {tp = D.TpSplit branches; _} as con -> + splitter con @@ List.map fst branches + | D.Cut { tp = D.Signature tele; cut } -> + let+ tp = + splice_tp @@ + Splice.con qid @@ fun qid -> + Splice.con code @@ fun code -> + Splice.con tele @@ fun tele -> + Splice.term @@ + TB.signature (TB.cons qid code (TB.lam @@ fun _ -> tele)) + in + cut_frm ~tp ~cut (D.KPush (qid, code, field)) + | _ -> + throw @@ NbeFailed ("Couldn't push argument in do_push") + end + and do_proj (con : D.con) (lbl : Ident.user) : D.con CM.m = let open CM in abort_if_inconsistent (ret D.tm_abort) @@ @@ -1212,14 +1323,16 @@ and do_proj (con : D.con) (lbl : Ident.user) : D.con CM.m = begin match List.assoc_opt lbl fields with | Some con -> ret con - | None -> throw @@ NbeFailed "Couldn't proj argument in do_proj, struct was missing field" + | None -> + Debug.print "bad do_proj: projecting %a from %a@." Ident.pp_user lbl D.pp_con con; + throw @@ NbeFailed "Couldn't proj argument in do_proj, struct was missing field" end | D.Split branches -> splitter con @@ List.map fst branches | D.Cut {tp = D.TpSplit branches; _} as con -> splitter con @@ List.map fst branches - | D.Cut {tp = D.Signature sign; cut} -> - cut_frm_sign cut sign lbl + | D.Cut {tp = D.Signature tele; cut} -> + cut_frm_tele cut tele lbl | _ -> throw @@ NbeFailed ("Couldn't proj argument in do_proj") end @@ -1465,11 +1578,12 @@ and unfold_el : D.con D.stable_code -> D.tp CM.m = Splice.term @@ TB.sg (TB.el base) @@ fun x -> TB.el @@ TB.ap fam [x] - | `Signature fields -> - let (lbls, field_cons) = ListUtil.unzip fields in - splice_tp @@ - Splice.cons field_cons @@ fun fields -> - Splice.term @@ TB.signature @@ List.map2 (fun ident fam -> (ident, fun args -> TB.el @@ TB.ap fam args)) lbls fields + + | `Telescope -> + ret D.Telescope + + | `Signature tele -> + ret @@ D.Signature tele | `Ext (n, fam, `Global phi, bdry) -> splice_tp @@ @@ -1545,7 +1659,7 @@ and enact_rigid_coe line r r' con tag = | `Stable (x, code) -> begin match code with - | `Nat | `Circle | `Univ -> ret con + | `Nat | `Circle | `Telescope | `Univ -> ret con | `Pi (basex, famx) -> splice_tm @@ Splice.con (D.BindSym (x, basex)) @@ fun base_line -> @@ -1562,14 +1676,14 @@ and enact_rigid_coe line r r' con tag = Splice.dim r' @@ fun r' -> Splice.con con @@ fun bdy -> Splice.term @@ TB.Kan.coe_sg ~base_line ~fam_line ~r ~r' ~bdy - | `Signature fields -> - let (lbls, fams) = ListUtil.unzip fields in + | `Signature tele -> splice_tm @@ - Splice.cons (List.map (fun famx -> D.BindSym (x, famx)) fams) @@ fun fam_lines -> - Splice.dim r @@ fun r -> - Splice.dim r' @@ fun r' -> - Splice.con con @@ fun bdy -> - Splice.term @@ TB.Kan.coe_sign ~field_lines:(ListUtil.zip lbls fam_lines) ~r ~r' ~bdy + failwith "[FIXME] Basis.Basis.enact_rigid_coe: Coercions " + (* Splice.cons (List.map (fun famx -> D.BindSym (x, famx)) fams) @@ fun fam_lines -> *) + (* Splice.dim r @@ fun r -> *) + (* Splice.dim r' @@ fun r' -> *) + (* Splice.con con @@ fun bdy -> *) + (* Splice.term @@ TB.Kan.coe_sign ~field_lines:(ListUtil.zip lbls fam_lines) ~r ~r' ~bdy *) | `Ext (n, famx, `Global cof, bdryx) -> splice_tm @@ Splice.con cof @@ fun cof -> @@ -1643,16 +1757,17 @@ and enact_rigid_hcom code r r' phi bdy tag = Splice.con bdy @@ fun bdy -> Splice.term @@ TB.Kan.hcom_sg ~base ~fam ~r ~r' ~phi ~bdy - | `Signature fields -> - let (lbls, fams) = ListUtil.unzip fields in - splice_tm @@ - Splice.cons fams @@ fun fams -> - Splice.dim r @@ fun r -> - Splice.dim r' @@ fun r' -> - Splice.cof phi @@ fun phi -> - Splice.con bdy @@ fun bdy -> - Splice.term @@ - TB.Kan.hcom_sign ~fields:(ListUtil.zip lbls fams) ~r ~r' ~phi ~bdy + | `Signature tele -> + failwith "[FIXME] Basis.Basis.enact_rigid_hcom: signatures?" + (* let (lbls, fams) = ListUtil.unzip fields in *) + (* splice_tm @@ *) + (* Splice.cons fams @@ fun fams -> *) + (* Splice.dim r @@ fun r -> *) + (* Splice.dim r' @@ fun r' -> *) + (* Splice.cof phi @@ fun phi -> *) + (* Splice.con bdy @@ fun bdy -> *) + (* Splice.term @@ *) + (* TB.Kan.hcom_sign ~fields:(ListUtil.zip lbls fams) ~r ~r' ~phi ~bdy *) | `Ext (n, fam, `Global cof, bdry) -> splice_tm @@ Splice.con cof @@ fun cof -> @@ -1664,7 +1779,7 @@ and enact_rigid_hcom code r r' phi bdy tag = Splice.con bdy @@ fun bdy -> Splice.term @@ TB.Kan.hcom_ext ~n ~cof ~fam ~bdry ~r ~r' ~phi ~bdy - | `Circle | `Nat as tag -> + | `Telescope | `Circle | `Nat as tag -> let+ bdy' = splice_tm @@ Splice.con bdy @@ fun bdy -> @@ -1779,9 +1894,11 @@ and do_frm con = | D.KAp (_, con') -> do_ap con con' | D.KFst -> do_fst con | D.KSnd -> do_snd con + | D.KPush (lbl, code, field) -> do_push lbl code field con | D.KProj lbl -> do_proj con lbl | D.KNatElim (mot, case_zero, case_suc) -> do_nat_elim mot case_zero case_suc con | D.KCircleElim (mot, case_base, case_loop) -> do_circle_elim mot case_base case_loop con + | D.KTeleElim (mot, case_nil, case_cons) -> do_tele_elim mot case_nil case_cons con | D.KElOut -> do_el_out con and do_spine con = @@ -1792,6 +1909,13 @@ and do_spine con = let* con' = do_frm con k in do_spine con' sp +(* NOTE: This should be safe to use in most situations, due to the stratification + of Symbols as virtual types *) +and unquote con = + let open CM in + match con with + | D.Quoted sym -> ret sym + | _ -> throw (NbeFailed "bad unquote") and splice_tm t = let env, tm = Splice.compile t in diff --git a/src/core/Semantics.mli b/src/core/Semantics.mli index 0d9306118..f0b629d35 100644 --- a/src/core/Semantics.mli +++ b/src/core/Semantics.mli @@ -25,7 +25,6 @@ val normalize_cof : D.cof -> D.cof compute val inst_tp_clo : D.tp_clo -> D.con -> D.tp compute val inst_tm_clo : D.tm_clo -> D.con -> D.con compute -val inst_sign_clo : D.sign_clo -> D.con -> D.sign compute val do_ap : D.con -> D.con -> D.con compute val do_ap2 : D.con -> D.con -> D.con -> D.con compute @@ -38,6 +37,7 @@ val do_el_out : D.con -> D.con compute val unfold_el : D.con D.stable_code -> D.tp compute val do_el : D.con -> D.tp compute val do_spine : D.con -> D.frm list -> D.con compute +val unquote : D.con -> Ident.user compute val con_to_dim : D.con -> D.dim compute val con_to_cof : D.con -> D.cof compute diff --git a/src/core/Serialize.ml b/src/core/Serialize.ml index 09f907848..1950308ae 100644 --- a/src/core/Serialize.ml +++ b/src/core/Serialize.ml @@ -145,7 +145,7 @@ struct | S.CodeExt (n, fam, `Global phi, tbdry) -> labeled "code_ext" [json_of_int n; json_of_tm fam; json_of_tm phi; json_of_tm tbdry] | S.CodePi (tbase, tfam) -> labeled "code_pi" [json_of_tm tbase; json_of_tm tfam] | S.CodeSg (tbase, tfam) -> labeled "code_sg" [json_of_tm tbase; json_of_tm tfam] - | S.CodeSignature sign -> labeled "code_sign" [json_of_labeled json_of_tm sign] + | S.CodeSignature sign -> labeled "code_sign" [json_of_tm sign] | S.CodeNat -> `String "code_nat" | S.CodeUniv -> `String "code_univ" | S.CodeV (r, pcode, code, pequiv) -> labeled "code_v" [json_of_tm r; json_of_tm pcode; json_of_tm code; json_of_tm pequiv] @@ -174,15 +174,12 @@ struct | S.Sub (tp, tphi, tm) -> labeled "sub" [json_of_tp tp; json_of_tm tphi; json_of_tm tm] | S.Pi (base, nm, fib) -> labeled "pi" [json_of_tp base; json_of_ident nm; json_of_tp fib ] | S.Sg (base, nm, fib) -> labeled "sg" [json_of_tp base; json_of_ident nm; json_of_tp fib ] - | S.Signature sign -> labeled "sign" [json_of_sign sign] + | S.Signature sign -> labeled "sign" [json_of_tm sign] | S.Nat -> `String "nat" | S.Circle -> `String "circle" | S.TpESub (sub, tp) -> labeled "subst" [json_of_sub sub; json_of_tp tp ] | S.TpLockedPrf tm -> labeled "locked" [json_of_tm tm] - and json_of_sign : S.sign -> J.value = - fun sign -> json_of_labeled json_of_tp sign - let json_of_ctx ctx : J.value = `A (List.map (fun (nm, tp) -> json_of_pair (json_of_ident nm) (json_of_tp tp)) ctx) @@ -332,7 +329,7 @@ struct let fam = json_to_tm j_fam in S.CodeSg (base, fam) | `A [`String "code_sign"; j_sign] -> - let sign = json_to_labeled json_to_tm j_sign in + let sign = json_to_tm j_sign in S.CodeSignature sign | `String "code_nat" -> S.CodeNat | `String "code_univ" -> S.CodeUniv @@ -406,7 +403,7 @@ struct let fib = json_to_tp j_fib in S.Pi (base, nm, fib) | `A [`String "sign"; j_sign] -> - let sign = json_to_labeled json_to_tp j_sign in + let sign = json_to_tm j_sign in S.Signature sign | `String "nat" -> S.Nat | `String "circle" -> S.Nat @@ -419,9 +416,6 @@ struct S.TpLockedPrf tm | j -> J.parse_error j "Syntax.json_to_tp" - and json_to_sign : J.value -> S.sign = - fun j_sign -> json_to_labeled json_to_tp j_sign - let json_to_ctx : J.value -> (Ident.t * S.tp) list = function | `A j_ctx -> j_ctx |> List.map @@ fun binding -> @@ -466,10 +460,6 @@ struct function | Clo (tp, env) -> labeled "clo" [Syntax.json_of_tp tp; json_of_env env] - and json_of_sign_clo : D.sign_clo -> J.value = - function - | Clo (sign, env) -> labeled "clo" [Syntax.json_of_sign sign; json_of_env env] - and json_of_env {tpenv; conenv} : J.value = `O [("tpenv", json_of_bwd json_of_tp tpenv); ("conenv", json_of_bwd json_of_con conenv)] @@ -496,16 +486,11 @@ struct | TpSplit branches -> labeled "tp_split" (json_of_alist json_of_cof json_of_tp_clo branches) | Pi (tp, ident, clo) -> labeled "pi" [json_of_tp tp; json_of_ident ident; json_of_tp_clo clo] | Sg (tp, ident, clo) -> labeled "sg" [json_of_tp tp; json_of_ident ident; json_of_tp_clo clo] - | Signature sign -> labeled "signature" [json_of_sign sign] + | Signature sign -> labeled "signature" [json_of_con sign] | Nat -> `String "nat" | Circle -> `String "circle" | TpLockedPrf cof -> labeled "tp_locked_prf" [json_of_cof cof] - and json_of_sign : D.sign -> J.value = - function - | D.Empty -> `String "empty" - | D.Field (lbl, tp, clo) -> labeled "field" [json_of_user lbl; json_of_tp tp; json_of_sign_clo clo] - and json_of_hd : D.hd -> J.value = function | D.Global sym -> labeled "global" [Global.serialize sym] @@ -538,7 +523,7 @@ struct function | `Pi (base, fam) -> labeled "pi" [json_of_con base; json_of_con fam] | `Sg (base, fam) -> labeled "sg" [json_of_con base; json_of_con fam] - | `Signature sign -> labeled "signature" [json_of_labeled json_of_con sign] + | `Signature sign -> labeled "signature" [json_of_con sign] | `Ext (n, code, `Global phi, fam) -> labeled "ext" [json_of_int n; json_of_con code; json_of_con phi; json_of_con fam] | `Nat -> `String "nat" | `Circle -> `String "circle" @@ -549,10 +534,11 @@ struct | `HCom (src, trg, cof, con) -> labeled "hcom" [json_of_dim src; json_of_dim trg; json_of_cof cof; json_of_con con] | `V (r, pcode, code, pequiv) -> labeled "v" [json_of_dim r; json_of_con pcode; json_of_con code; json_of_con pequiv] - and json_of_fhcom_tag : [`Nat | `Circle] -> J.value = + and json_of_fhcom_tag : [`Nat | `Circle | `Telescope] -> J.value = function | `Nat -> `String "nat" | `Circle -> `String "circle" + | `Telescope -> `String "tele" let rec json_to_con : J.value -> D.con = function @@ -592,11 +578,6 @@ struct | `A [`String "clo"; j_tp; j_env] -> Clo (Syntax.json_to_tp j_tp, json_to_env j_env) | j -> J.parse_error j "Domain.json_to_tp_clo" - and json_to_sign_clo : J.value -> D.sign_clo = - function - | `A [`String "clo"; j_sign; j_env] -> Clo (Syntax.json_to_sign j_sign, json_to_env j_env) - | j -> J.parse_error j "Domain.json_to_tp_clo" - and json_to_env : J.value -> D.env = function | `O [("tpenv", j_tpenv); ("conenv", j_conenv)] -> @@ -627,18 +608,12 @@ struct | `A (`String "tp_split" :: j_branches) -> TpSplit (json_to_alist json_to_cof json_to_tp_clo j_branches) | `A [`String "pi"; j_tp; j_ident; j_clo] -> Pi (json_to_tp j_tp, json_to_ident j_ident, json_to_tp_clo j_clo) | `A [`String "sg"; j_tp; j_ident; j_clo] -> Sg (json_to_tp j_tp, json_to_ident j_ident, json_to_tp_clo j_clo) - | `A [`String "signature"; j_sign] -> Signature (json_to_sign j_sign) + | `A [`String "signature"; j_sign] -> Signature (json_to_con j_sign) | `String "nat" -> Nat | `String "circle" -> Circle | `A [`String "tp_locked_prf"; j_cof] -> TpLockedPrf (json_to_cof j_cof) | j -> J.parse_error j "Domain.json_to_tp" - and json_to_sign : J.value -> D.sign = - function - | `String "empty" -> Empty - | `A [`String "field"; j_lbl; j_tp; j_clo] -> Field (json_to_user j_lbl, json_to_tp j_tp, json_to_sign_clo j_clo) - | j -> J.parse_error j "Domain.json_to_sign" - and json_to_hd : J.value -> D.hd = function | `A [`String "global"; j_sym] -> Global (Global.deserialize j_sym) @@ -676,7 +651,7 @@ struct function | `A [`String "pi"; j_base; j_fam] -> `Pi (json_to_con j_base, json_to_con j_fam) | `A [`String "sg"; j_base; j_fam] -> `Sg (json_to_con j_base, json_to_con j_fam) - | `A [`String "signature"; j_sign] -> `Signature (json_to_labeled json_to_con j_sign) + | `A [`String "signature"; j_sign] -> `Signature (json_to_con j_sign) | `A [`String "ext"; j_n; j_code; j_phi; j_fam] -> `Ext (json_to_int j_n, json_to_con j_code, `Global (json_to_con j_phi), json_to_con j_fam) | `String "nat" -> `Nat | `String "circle" -> `Circle @@ -689,10 +664,11 @@ struct | `A [`String "v"; j_r; j_pcode; j_code; j_pequiv] -> `V (json_to_dim j_r, json_to_con j_pcode, json_to_con j_code, json_to_con j_pequiv) | j -> J.parse_error j "Domain.json_to_unstable_code" - and json_to_fhcom_tag : J.value -> [ `Nat | `Circle ] = + and json_to_fhcom_tag : J.value -> [ `Nat | `Circle | `Telescope ] = function | `String "nat" -> `Nat | `String "circle" -> `Circle + | `String "tele" -> `Telescope | j -> J.parse_error j "Domain.json_to_fhcom_tag" end diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index a9d0d5488..8a361f0e4 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -25,6 +25,7 @@ struct | Global _ -> Format.fprintf fmt "" | Let _ -> Format.fprintf fmt "" | Ann _ -> Format.fprintf fmt "" + | Quoted u -> Format.fprintf fmt "'%a" Ident.pp_user u | Zero -> Format.fprintf fmt "zero" | Suc tm -> Format.fprintf fmt "suc[%a]" dump tm @@ -41,9 +42,14 @@ struct | Fst tm -> Format.fprintf fmt "fst[%a]" dump tm | Snd tm -> Format.fprintf fmt "snd[%a]" dump tm - | Struct fields -> Format.fprintf fmt "struct[%a]" dump_struct fields + | TeleNil -> Format.fprintf fmt "tele/nil" + | TeleCons (qid, code, tele) -> Format.fprintf fmt "tele/cons[%a, %a, %a]" dump qid dump code dump tele + | TeleElim (mot, nil, cons, tele) -> Format.fprintf fmt "tele/elim[%a, %a, %a, %a]" dump mot dump nil dump cons dump tele + | Struct tele -> Format.fprintf fmt "struct[%a]" dump_struct tele + | Push (qid, code, field, str) -> Format.fprintf fmt "push[%a, %a, %a, %a]" dump qid dump code dump field dump str | Proj (tm, lbl) -> Format.fprintf fmt "proj[%a, %a]" dump tm Ident.pp_user lbl + | Coe _ -> Format.fprintf fmt "" | HCom _ -> Format.fprintf fmt "" | Com _ -> Format.fprintf fmt "" @@ -70,10 +76,10 @@ struct | CodeExt _ -> Format.fprintf fmt "" | CodePi _ -> Format.fprintf fmt "" | CodeSg _ -> Format.fprintf fmt "" - | CodeSignature fields -> + | CodeTelescope -> Format.fprintf fmt "" + | CodeSignature tele -> Format.fprintf fmt "sig[%a]" - (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp_user lbl dump tp)) - fields + dump tele | CodeNat -> Format.fprintf fmt "nat" | CodeUniv -> Format.fprintf fmt "univ" | CodeV _ -> Format.fprintf fmt "" @@ -84,11 +90,8 @@ struct | LockedPrfIn _ -> Format.fprintf fmt "" | LockedPrfUnlock _ -> Format.fprintf fmt "" - and dump_struct fmt fields = - Format.fprintf fmt "%a" (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp_user lbl dump tp)) fields - - and dump_sign fmt sign = - Format.fprintf fmt "%a" (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp_user lbl dump_tp tp)) sign + and dump_struct fmt tele = + Format.fprintf fmt "%a" (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp_user lbl dump tp)) tele and dump_tp fmt = function @@ -102,7 +105,9 @@ struct | Sub _ -> Format.fprintf fmt "" | Pi (base, ident, fam) -> Format.fprintf fmt "pi[%a, %a, %a]" dump_tp base Ident.pp ident dump_tp fam | Sg _ -> Format.fprintf fmt "" - | Signature fields -> Format.fprintf fmt "tp/sig[%a]" dump_sign fields + | Symbol -> Format.fprintf fmt "tp/symbol" + | Telescope -> Format.fprintf fmt "tp/tele" + | Signature tele -> Format.fprintf fmt "tp/sig[%a]" dump tele | Nat -> Format.fprintf fmt "nat" | Circle -> Format.fprintf fmt "circle" | TpESub _ -> Format.fprintf fmt "" @@ -129,6 +134,7 @@ struct let tuple = delimited let substitution = right 10 let juxtaposition = left 9 + let cons = right 8 let proj = right 8 let sub_compose = left 7 let cof_eq = nonassoc 6 @@ -144,12 +150,19 @@ struct (** assumes [Debug.is_debug_mode ()] = [false] *) let classify_tm : tm -> t = function - | Var _ | Global _ -> atom + | Var _ | Global _ | Quoted _ -> atom | Lam _ -> double_arrow | Ap _ -> juxtaposition | Pair _ -> tuple + + | TeleNil -> atom + | TeleCons _ -> cons + | TeleElim _ -> juxtaposition + | Struct _ -> juxtaposition + | Push _ -> juxtaposition | Proj _ -> proj + | CofSplit _ -> tuple | Cof (Cof.Eq _) -> cof_eq | Cof (Cof.Join [] | Cof.Meet []) -> atom @@ -167,6 +180,7 @@ struct | SubIn _ | SubOut _ | ElIn _ | ElOut _ -> passed | CodePi _ -> arrow | CodeSg _ -> times + | CodeTelescope -> atom | CodeSignature _ -> juxtaposition | CodeExt _ -> juxtaposition @@ -190,7 +204,7 @@ struct let classify_tp : tp -> t = function - | Univ | TpDim | TpCof | Nat | Circle -> atom + | Symbol | Univ | TpDim | TpCof | Nat | Circle -> atom | El _ -> passed | TpVar _ -> atom | TpPrf _ -> delimited @@ -198,6 +212,7 @@ struct | Sub _ -> juxtaposition | Pi _ -> arrow | Sg _ -> times + | Telescope -> atom | Signature _ -> juxtaposition | TpESub _ -> substitution | TpLockedPrf _ -> juxtaposition @@ -230,14 +245,14 @@ struct let ppenv_bind env ident = Pp.Env.bind env @@ Ident.to_string_opt ident - let rec pp_fields pp_field env fmt = + let rec pp_tele pp_field env fmt = function | [] -> () - | ((lbl, tp) :: fields) -> + | ((lbl, tp) :: tele) -> Format.fprintf fmt "(%a : %a)@ @,%a" Ident.pp_user lbl (pp_field env P.(right_of colon)) tp - (pp_fields pp_field env) fields + (pp_tele pp_field env) tele let rec pp env = pp_braced_cond P.classify_tm @@ fun penv fmt -> @@ -250,10 +265,35 @@ struct (pp env P.(left_of juxtaposition)) tm0 (pp_atomic env) tm1 | Pair (tm0, tm1) -> pp_tuple (pp env P.isolated) fmt [tm0; tm1] - | Struct fields -> - Format.fprintf fmt "@[struct %a@]" (pp_fields pp env) fields + | TeleNil -> + () + | TeleCons (Quoted ident, code, Lam (_, body)) -> + let (x, envx) = ppenv_bind env (ident :> Ident.t) in + Format.fprintf fmt "(%s : %a)@ @,%a" + x + (pp env P.(right_of colon)) code + (pp envx penv) body + | TeleCons (qid, code, tele) -> + Format.fprintf fmt "(%a : %a)@ @,%a" + (pp env penv) qid + (pp env P.(right_of colon)) code + (pp env penv) tele + | TeleElim (mot, nil, cons, tele) -> + Format.fprintf fmt "@[elim %a %@ %a@ @[[ nil => %a@ | cons => %a@ ]@]@]" + (pp_atomic env) tele + (pp_atomic env) mot + (pp env P.isolated) nil + (pp env P.isolated) cons + | Struct tele -> + Format.fprintf fmt "@[struct %a@]" (pp_tele pp env) tele + | Push (qid, code, field, str) -> + Format.fprintf fmt "@[push %a %a %a %a@]" + (pp env penv) qid + (pp env penv) code + (pp env penv) field + (pp env penv) str | Proj (tm, lbl) -> - Format.fprintf fmt "@[%a %@ %a@]" (pp env P.(left_of proj)) tm Ident.pp_user lbl + Format.fprintf fmt "@[%a.%a@]" (pp env P.(left_of proj)) tm Ident.pp_user lbl | CofSplit branches -> let pp_sep fmt () = Format.fprintf fmt "@ | " in pp_bracketed_list ~pp_sep (pp_cof_split_branch env) fmt branches @@ -281,6 +321,8 @@ struct pp_var env fmt ix | Global sym -> Symbol.pp fmt sym + | Quoted id -> + Format.fprintf fmt "`%a" Ident.pp_user id | Cof (Cof.Eq (r, s)) -> Format.fprintf fmt "%a = %a" (pp env P.(left_of cof_eq)) r (pp env P.(right_of cof_eq)) s | Cof (Cof.Join []) -> @@ -376,8 +418,12 @@ struct Uuseg_string.pp_utf_8 "Σ" (pp_atomic env) base (pp_atomic env) tm - | CodeSignature fields -> - Format.fprintf fmt "@[sig %a@]" (pp_fields pp_binders env) fields + + | CodeTelescope -> + Format.fprintf fmt "tele" + | CodeSignature tele -> + Format.fprintf fmt "@[sig %a@]" (pp env penv) tele + | CodeExt (_, fam, `Global phi, bdry) -> Format.fprintf fmt "@[ext %a %a %a@]" (pp_atomic env) fam @@ -488,8 +534,6 @@ struct Uuseg_string.pp_utf_8 "∘" (pp_sub env P.(right_of sub_compose)) sb1 - and pp_sign env fmt (sign : sign) : unit = pp_fields pp_tp env fmt sign - and pp_tp env = pp_braced_cond P.classify_tp @@ fun penv fmt -> function @@ -513,8 +557,12 @@ struct (pp_tp env P.(right_of colon)) base Uuseg_string.pp_utf_8 "×" (pp_tp envx P.(right_of times)) fam - | Signature fields -> - Format.fprintf fmt "sig %a" (pp_sign env) fields + | Symbol -> + Format.fprintf fmt "symbol" + | Telescope -> + Format.fprintf fmt "tele" + | Signature tele -> + Format.fprintf fmt "sig %a" (pp env penv) tele | Sub (tp, phi, tm) -> let _x, envx = ppenv_bind env `Anon in Format.fprintf fmt "@[sub %a %a@ %a@]" diff --git a/src/core/Syntax.mli b/src/core/Syntax.mli index d8aab309b..b7964bb38 100644 --- a/src/core/Syntax.mli +++ b/src/core/Syntax.mli @@ -17,9 +17,6 @@ module Make : functor (Symbol : Symbol.S) -> sig (** Print a core language term. *) val pp : Pp.env -> t Pp.printer - (** Print a signature. *) - val pp_sign : Pp.env -> sign Pp.printer - (** Print a core language type. *) val pp_tp : Pp.env -> tp Pp.printer @@ -35,6 +32,5 @@ module Make : functor (Symbol : Symbol.S) -> sig When debugging, we are not likely to have enough context to use the nice pretty printers above; as a last resort, {!val:dump} and {!val:dump_tp} may be used. *) val dump : t Pp.printer - val dump_sign : sign Pp.printer val dump_tp : tp Pp.printer end diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml index bba146002..7f911c840 100644 --- a/src/core/SyntaxData.ml +++ b/src/core/SyntaxData.ml @@ -8,6 +8,7 @@ struct | Global of Symbol.t | Let of t * Ident.t * t | Ann of t * tp + | Quoted of Ident.user | Zero | Suc of t @@ -24,7 +25,13 @@ struct | Fst of t | Snd of t + + | TeleNil + | TeleCons of t * t * t + | TeleElim of t * t * t * t + | Struct of (Ident.user * t) list + | Push of t * t * t * t | Proj of t * Ident.user | Coe of t * t * t * t @@ -53,7 +60,8 @@ struct | CodeExt of int * t * [`Global of t] * t | CodePi of t * t | CodeSg of t * t - | CodeSignature of (Ident.user * t) list + | CodeTelescope + | CodeSignature of t | CodeNat | CodeUniv | CodeV of t * t * t * t @@ -76,14 +84,14 @@ struct | Sub of tp * t * t | Pi of tp * Ident.t * tp | Sg of tp * Ident.t * tp - | Signature of sign + | Symbol + | Telescope + | Signature of t | Nat | Circle | TpESub of sub * tp | TpLockedPrf of t - and sign = (Ident.user * tp) list - (** The language of substitions from {{:https://arxiv.org/abs/1102.2405} Abel, Coquand, and Pagano}. *) and sub = | SbI diff --git a/src/core/Tactic.ml b/src/core/Tactic.ml index 0f291b01c..b4215de63 100644 --- a/src/core/Tactic.ml +++ b/src/core/Tactic.ml @@ -75,6 +75,7 @@ module rec Var : sig val prf : D.cof -> tac val con : tac -> D.con val syn : tac -> Syn.tac + val chk : tac -> Chk.tac val abstract : ?ident:Ident.t -> D.tp -> (tac -> 'a RM.m) -> 'a RM.m end = struct @@ -87,6 +88,9 @@ struct let+ tm = RM.quote_con tp con in tm, tp + let chk v = + Chk.syn @@ syn v + let abstract : ?ident:Ident.t -> D.tp -> (Var.tac -> 'a RM.m) -> 'a RM.m = fun ?(ident = `Anon) tp kont -> RM.abstract ident tp @@ fun (con : D.con) -> diff --git a/src/core/Tactic.mli b/src/core/Tactic.mli index ff70ad795..64fb5df0d 100644 --- a/src/core/Tactic.mli +++ b/src/core/Tactic.mli @@ -59,6 +59,7 @@ sig val prf : D.cof -> tac val con : tac -> D.con val syn : tac -> Syn.tac + val chk : tac -> Chk.tac end type var = Var.tac diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml index 287336d0d..28ae106bc 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -153,10 +153,45 @@ let snd m = let+ x = m in S.Snd x +let symbol = + ret S.Symbol + +let quoted id = + ret @@ S.Quoted id + +let telescope = + ret S.Telescope + +let code_telescope = + ret S.CodeTelescope + +let nil = + ret S.TeleNil + +let cons mqid mcode mtele = + let+ qid = mqid + and+ code = mcode + and+ tele = mtele in + S.TeleCons (qid, code, tele) + +let tele_elim mmot mnil mcons mtele = + let+ mot = mmot + and+ nil = mnil + and+ cons = mcons + and+ tele = mtele in + S.TeleElim (mot, nil, cons, tele) + let struct_ mfields = let+ fields = MU.map (MU.second (fun x -> x)) mfields in S.Struct fields +let push mqid mcode mfield mstr = + let+ qid = mqid + and+ code = mcode + and+ field = mfield + and+ str = mstr in + S.Push (qid, code, field, str) + let proj m lbl = let+ x = m in S.Proj (x, lbl) @@ -242,17 +277,16 @@ let sg ?(ident = `Anon) mbase mfam : _ m = and+ fam = scope mfam in S.Sg (base, ident, fam) -let signature (mfields : (Ident.user * (S.t m list -> S.tp m)) list) : _ m = - let rec scope_fields bound = - function - | [] -> ret [] - | ((ident, mfield) :: mfields) -> - let* field = mfield bound in - let+ fields = scope @@ fun tm -> scope_fields (bound @ [tm]) mfields in - (ident, field) :: fields - in - let+ fields = scope_fields [] mfields in - S.Signature fields +let signature mtele : _ m = + let+ tele = mtele in + S.Signature tele + +let code_signature mtele : _ m = + let+ tele = mtele in + S.CodeSignature tele + +let code_univ = + ret S.CodeUniv let code_pi mbase mfam : _ m = let+ base = mbase @@ -761,6 +795,98 @@ struct end end +module Tele = +struct + (* [NOTE: Telescope Macros + Weak Tarski Universes] + All of the macros below rely heavily on the elimination + form for 'tele', and often use somewhat fancy motives. + When done naively, this makes calling these macros + an extremely error prone process! + + Therefore, we want to ensure that all of the callers of these + macros don't need to ensure that they prepare the + arguments with the correct "calling convention" + (for lack of a better term) by inserting a ton of + 'el_in' or 'el_out' terms into the macro arguments. *) + + (** Unfold a telescope into a pi type. *) + let unfold tele code = + let mot = lam @@ fun _ -> code_univ in + let nil_case = el_in code in + let cons_case = + lam @@ fun _ -> + lam ~ident:(`User ["a"]) @@ fun a -> + lam @@ fun _ -> + lam ~ident:(`User ["b"]) @@ fun b -> + el_in @@ + code_pi a @@ lam ~ident:(`User ["a"]) @@ fun ax -> + el_out @@ + ap b [ax] + in + el_out @@ tele_elim mot nil_case cons_case tele + + let extend tele fam = + (* NOTE: unfold : tele → univ → univ *) + let mot = + lam @@ fun t -> + code_pi (unfold t code_telescope) @@ lam @@ fun _ -> code_telescope + in + let nil_case = + el_in @@ + lam @@ fun t -> t + in + (* Π (qid : symbol) → Π (a : univ) → Π (t : telescope) → `Π (unfold t `telescope) → `telescope *) + let cons_case = + lam @@ fun qid -> + (* a : univ *) + lam @@ fun a -> + (* t : telescope *) + lam @@ fun _ -> + (* c : Π (x : a) → `Π unfold (t x) → `telescope *) + lam @@ fun c -> + el_in @@ + lam @@ fun k -> + el_in @@ + cons qid a @@ lam @@ fun z -> el_out @@ ap (el_out @@ ap c [z]) [ap (el_out k) [z]] + in + el_out @@ ap (el_out @@ tele_elim mot nil_case cons_case tele) [fam] + + let curry tele code uncurried = + let mot = + lam @@ fun t -> + (* `Π (k : `Π `sig t → code) → unfold t code *) + code_pi (code_pi (code_signature t) @@ lam @@ fun _ -> code) @@ lam @@ fun _ -> + unfold t code + in + let nil_case = + el_in @@ + (* u : `Π (k : `Π `sig [] → code) *) + lam @@ fun u -> + ap (el_out u) [el_in @@ struct_ []] + in + let cons_case = + lam @@ fun qid -> + (* a : univ *) + lam @@ fun a -> + (* t : Π a → telescope *) + lam @@ fun _ -> + (* c : Π (x : a) → `Π (k : `Π `sig (t x) → code) → unfold (t x) code *) + lam @@ fun c -> + el_in @@ + (* u : `Π `sig (cons qid a t) → a *) + lam @@ fun u -> + el_in @@ + (* x : a *) + lam @@ fun x -> + (* unfold (t x) code *) + ap (el_out @@ ap c [x]) [el_in @@ lam @@ fun t_struct -> ap (el_out u) [el_in @@ push qid a x (el_out @@ t_struct)]] + in + (* See [NOTE: Telescope Macros + Weak Tarski Universes] for the reasoning behind this eta-expansion. *) + let el_uncurried = el_in @@ lam @@ fun str -> el_in @@ ap uncurried [el_out str] in + ap (el_out @@ tele_elim mot nil_case cons_case tele) [el_uncurried] +end + +(* [TODO: Reed M, 26/01/2022] Move this into the unit test suite. *) module Test = struct let closed_form_hcom_v = diff --git a/src/core/TermBuilder.mli b/src/core/TermBuilder.mli index d10011513..f6ff07f0d 100644 --- a/src/core/TermBuilder.mli +++ b/src/core/TermBuilder.mli @@ -30,7 +30,17 @@ val snd : t m -> t m val lams : Ident.t list -> (t m list -> t m) -> t m +val symbol : tp m +val quoted : Ident.user -> t m + +val telescope : tp m +val code_telescope : t m +val nil : t m +val cons : t m -> t m -> t m -> t m +val tele_elim : t m -> t m -> t m -> t m -> t m + val struct_ : (Ident.user * t m) list -> t m +val push : t m -> t m -> t m -> t m -> t m val proj : t m -> Ident.user -> t m val zero : t m @@ -64,7 +74,7 @@ val circle_elim : t m -> t m -> t m -> t m -> t m val pi : ?ident:Ident.t -> tp m -> tp b -> tp m val sg : ?ident:Ident.t -> tp m -> tp b -> tp m -val signature : (Ident.user * (t m list -> tp m)) list -> tp m +val signature : t m -> tp m val sub : tp m -> t m -> t b -> tp m val tp_prf : t m -> tp m val tp_dim : tp m @@ -79,6 +89,7 @@ val locked_prf_unlock : tp m -> cof:t m -> prf:t m -> bdy:t m -> t m val cube : int -> (t m list -> tp m) -> tp m +val code_univ : t m val code_pi : t m -> t m -> t m val code_sg : t m -> t m -> t m val code_path : t m -> t m -> t m @@ -138,6 +149,12 @@ module Kan : sig end end +module Tele : sig + val unfold : t m -> t m -> t m + val extend : t m -> t m -> t m + val curry : t m -> t m -> t m -> t m +end + module Test : sig val print_example : unit -> unit end diff --git a/src/frontend/ConcreteSyntaxData.ml b/src/frontend/ConcreteSyntaxData.ml index 01bf0788d..f85230d8f 100644 --- a/src/frontend/ConcreteSyntaxData.ml +++ b/src/frontend/ConcreteSyntaxData.ml @@ -34,6 +34,11 @@ and con_ = | Lam of Ident.t list * con | Ap of con * con list | Sg of cell list * con + | Nil + | Cons of con * con * con + | Telescope + | Row of field list + | Extend of con * con | Signature of field list | Struct of field list | Proj of con * Ident.user @@ -100,6 +105,8 @@ type decl = | Print of Ident.t node | Import of string list * con option | NormalizeTerm of con + | DumpTerm of con + | Debug of bool | Fail of {name : Ident.t; args : cell list; def : con; tp : con; info : info} | Quit diff --git a/src/frontend/Driver.ml b/src/frontend/Driver.ml index 8f8f0b7d6..45f0094e0 100644 --- a/src/frontend/Driver.ml +++ b/src/frontend/Driver.ml @@ -175,6 +175,17 @@ and execute_decl : CS.decl -> command = let* tm' = RM.quote_con vtp vtm in let+ () = RM.emit term.info pp_message @@ OutputMessage (NormalizedTerm {orig = tm; nf = tm'}) in Continue Fun.id + | CS.DumpTerm term -> + RM.veil (Veil.const `Transparent) @@ + let* tm, _ = Tactic.Syn.run @@ Elaborator.syn_tm term in + Debug.print "Syntax: %a@." S.dump tm; + let+ vtm = RM.lift_ev @@ Sem.eval tm in + Debug.print "Dumping Term: %a@." D.pp_con vtm; + Continue Fun.id + | CS.Debug b -> + Debug.debug_mode b; + Printexc.record_backtrace b; + RM.ret @@ Continue Fun.id | CS.Fail {name; args; def; tp; info} -> let* res = RM.trap @@ elaborate_typed_term (Ident.to_string name) args tp def in print_fail name info res diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml index d229bda06..139b4df44 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -32,15 +32,6 @@ let rec unfold idents k = let span = Env.location env in RM.throw @@ Err.RefineError (Err.UnboundVariable ident, span) -(* Account for the lambda-bound signature field dependencies. - See [NOTE: Sig Code Quantifiers] for more info. *) -let bind_sig_tacs (tacs : ('a Ident.some * T.Chk.tac) list) : ('a Ident.some * T.Chk.tac) list = - let bind_tac lbls (lbl, tac) = - let tac = Bwd.fold_right (fun lbl tac -> R.Pi.intro ~ident:(lbl :> Ident.t) (fun _ -> tac)) lbls tac in - Snoc (lbls, lbl) , (lbl, tac) - in - snd @@ ListUtil.map_accum_left bind_tac Emp tacs - module CoolTp : sig include T.Tactic @@ -48,6 +39,7 @@ sig val as_tp : tac -> T.Tp.tac val pi : tac -> Ident.t -> tac -> tac val sg : tac -> Ident.t -> tac -> tac + val tele : tac val signature : (Ident.user * tac) list -> tac val sub : tac -> T.Chk.tac -> T.Chk.tac -> tac val ext : int -> T.Chk.tac -> T.Chk.tac -> T.Chk.tac -> tac @@ -109,15 +101,15 @@ struct let tac = R.Sg.formation tac_base (ident, fun _ -> tac_fam) in Tp tac + let tele = Code R.Univ.tele + let signature (tacs : (Ident.user * tac) list) : tac = match (as_codes tacs) with | Some tacs -> - let tac = R.Univ.signature (bind_sig_tacs tacs) in + let tac = R.Univ.signature (Tactics.Telescope.of_list tacs) in Code tac | None -> - let tele = List.fold_right (fun (nm, tac) tele -> R.Bind (nm, as_tp tac, fun _ -> tele)) tacs R.Done in - let tac = R.Signature.formation tele in - Tp tac + failwith "[FIXME] Core.CoolTp.signature: Handle the case when a signature is full of types!" let sub tac_tp tac_phi tac_pel : tac = let tac = R.Sub.formation (as_tp tac_tp) tac_phi (fun _ -> tac_pel) in @@ -298,16 +290,33 @@ and chk_tm : CS.con -> T.Chk.tac = let quant base (nm, fam) = R.Univ.sg base (R.Pi.intro ~ident:nm fam) in Tactics.tac_nary_quantifier quant tacs @@ chk_tm body + | CS.Telescope -> + R.Univ.tele + + | CS.Nil -> + R.Telescope.nil + + | CS.Cons (qid, code, tele) -> + R.Telescope.cons (chk_tm qid) (chk_tm code) (chk_tm tele) + + | CS.Row fields -> + Tactics.Telescope.of_list @@ List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) fields + + | CS.Extend (row, fam) -> + Tactics.Telescope.extend (chk_tm row) (chk_tm fam) + | CS.Signature fields -> - let tacs = bind_sig_tacs @@ List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) fields in + let tacs = Tactics.Telescope.of_list @@ List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) fields in R.Univ.signature tacs | CS.Patch (tp, patches) -> - let tacs = bind_sig_tacs @@ List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) patches in - R.Univ.patch (chk_tm tp) (R.Signature.find_field_tac tacs) + let tacs = List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) patches in + Tactics.Signature.patch (chk_tm tp) (R.Signature.find_field_tac tacs) + | CS.Total (tp, patches) -> - let tacs = bind_sig_tacs @@ List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) patches in - R.Univ.patch (R.Univ.total (syn_tm tp)) (R.Signature.find_field_tac tacs) + let tacs = List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) patches in + Tactics.Signature.patch (Tactics.Signature.total (syn_tm tp)) (R.Signature.find_field_tac tacs) + | CS.V (r, pcode, code, pequiv) -> R.Univ.code_v (chk_tm r) (chk_tm pcode) (chk_tm code) (chk_tm pequiv) diff --git a/src/frontend/Grammar.mly b/src/frontend/Grammar.mly index c36be59d6..c986a0c97 100644 --- a/src/frontend/Grammar.mly +++ b/src/frontend/Grammar.mly @@ -42,10 +42,10 @@ %token LET IN SUB %token SUC NAT ZERO UNFOLD GENERALIZE WITH %token CIRCLE BASE LOOP -%token SIG STRUCT AS +%token NIL CONS TELESCOPE ROW SIG STRUCT AS EXTEND %token EXT %token COE COM HCOM HFILL -%token QUIT NORMALIZE PRINT DEF AXIOM FAIL +%token QUIT NORMALIZE PRINT DEF AXIOM FAIL DUMP DEBUG %token IMPORT %token ELIM %token SEMISEMI EOF @@ -145,6 +145,10 @@ decl: { Quit } | NORMALIZE; tm = term { NormalizeTerm tm } + | DUMP; tm = term + { DumpTerm tm } + | DEBUG; b = flag + { Debug b } | unitpath = IMPORT; m = ioption(bracketed_modifier) { Import (unitpath, m) } | PRINT; name = name @@ -241,6 +245,10 @@ plain_atomic_term_except_name: { Base } | CIRCLE { Circle } + | NIL + { Nil } + | TELESCOPE + { Telescope } | TYPE { Type } | name = HOLE_NAME @@ -315,14 +323,22 @@ plain_term_except_cof_case: { t } | ELIM; cases = cases { LamElim cases } + | ELIM; WITH; mot = atomic_term; cases = cases; scrut = atomic_term + { Elim { mot; cases; scrut } } | tele = nonempty_list(tele_cell); RIGHT_ARROW; cod = term { Pi (tele, cod) } | tele = nonempty_list(tele_cell); TIMES; cod = term { Sg (tele, cod) } | SIG; tele = list(field); { Signature tele } + | CONS; qid = atomic_term; code = atomic_term; tele = atomic_term + { Cons (qid, code, tele) } + | ROW; tele = list(field); + { Row tele } | STRUCT; tele = list(field); { Struct tele } + | row = atomic_term; EXTEND; fam = atomic_term + { Extend (row, fam) } | dom = term; RIGHT_ARROW; cod = term { Pi ([Cell {names = [`Anon]; tp = dom}], cod) } | dom = term; TIMES; cod = term @@ -383,10 +399,13 @@ pat_lbl: { ["base"] } | LOOP { ["loop"] } + | NIL + { ["nil"] } + | CONS + { ["cons"] } | lbl = path { lbl } - pat: | lbl = pat_lbl args = list(pat_arg) { Pat {lbl; args} } @@ -412,3 +431,9 @@ patches: tele_cell: | LPR names = nonempty_list(plain_name); COLON tp = term; RPR { Cell {names; tp} } + +flag: + | TOPC + { true } + | BOTC + { false } diff --git a/src/frontend/Lex.mll b/src/frontend/Lex.mll index 3c2f4389d..c68ac2436 100644 --- a/src/frontend/Lex.mll +++ b/src/frontend/Lex.mll @@ -22,6 +22,8 @@ let commands = ("#fail", FAIL); ("#normalize", NORMALIZE); ("#print", PRINT); + ("#dump", DUMP); + ("#debug", DEBUG); ("#quit", QUIT); ] @@ -35,9 +37,14 @@ let keywords = ("base", BASE); ("loop", LOOP); ("circle", CIRCLE); + ("nil", NIL); + ("cons", CONS); + ("tele", TELESCOPE); + ("row", ROW); ("sig", SIG); ("struct", STRUCT); ("as", AS); + ("extend", EXTEND); ("🍪", CIRCLE); ("let", LET); ("in", IN); diff --git a/src/frontend/Tactics.ml b/src/frontend/Tactics.ml index a05bbe851..d627437d5 100644 --- a/src/frontend/Tactics.ml +++ b/src/frontend/Tactics.ml @@ -9,8 +9,10 @@ module S = Syntax module R = Refiner module CS = ConcreteSyntax module Sem = Semantics +module TB = TermBuilder open Monad.Notation (RM) +module CM = struct include Monads.CmpM include Monad.Notation (Monads.CmpM) module MU = Monad.Util (Monads.CmpM) end let elab_err err = let* env = RM.read in @@ -112,6 +114,33 @@ struct | None -> RM.ret @@ R.Hole.unleash_hole @@ Some "loop" in T.Syn.run @@ R.Circle.elim mot tac_base tac_loop scrut + | D.Telescope, mot -> + let* tac_nil = + match find_case ["nil"] cases with + | Some ([], tac) -> RM.ret tac + | Some _ -> elab_err ElabError.MalformedCase + | None -> RM.ret @@ R.Hole.unleash_hole @@ Some "nil" + in + let* tac_cons = + match find_case ["cons"] cases with + | Some ([`Simple nm_qid; `Simple nm_code; `Simple nm_tele], tac) -> + RM.ret @@ + R.Pi.intro ~ident:nm_qid @@ fun _ -> + R.Pi.intro ~ident:nm_code @@ fun _ -> + R.Pi.intro ~ident:nm_tele @@ fun _ -> + R.Pi.intro @@ fun _ -> + tac + | Some ([`Simple nm_qid; `Simple nm_code; `Inductive (nm_tele, nm_ih)], tac) -> + RM.ret @@ + R.Pi.intro ~ident:nm_qid @@ fun _ -> + R.Pi.intro ~ident:nm_code @@ fun _ -> + R.Pi.intro ~ident:nm_tele @@ fun _ -> + R.Pi.intro ~ident:nm_ih @@ fun _ -> + tac + | Some _ -> elab_err ElabError.MalformedCase + | None -> RM.ret @@ R.Hole.unleash_hole @@ Some "cons" + in + T.Syn.run @@ R.Telescope.elim mot tac_nil tac_cons scrut | _ -> RM.with_pp @@ fun ppenv -> let* tp = RM.quote_tp ind_tp in @@ -151,3 +180,163 @@ struct | _ -> RM.expected_connective `Pi tp end + +module Pi = +struct + let intros tac_args tac_ret = + let quant base (nm, fam) = R.Univ.pi base (R.Pi.intro ~ident:nm fam) in + tac_nary_quantifier quant tac_args tac_ret +end + + +module Telescope = +struct + let rec of_list tacs = + match tacs with + | [] -> + R.Telescope.nil + | (lbl, tac) :: tacs -> + R.Telescope.cons (R.Symbol.quote lbl) tac @@ + R.Pi.intro ~ident:(lbl :> Ident.t) @@ fun _ -> + of_list tacs + + let extend (tele_tac : T.Chk.tac) (fam_tac : T.Chk.tac) = + T.Chk.rule ~name:"Telescope.extend" @@ + function + | D.Telescope -> + let* tele = T.Chk.run tele_tac D.Telescope in + let* vtele = RM.lift_ev @@ Sem.eval tele in + let* fam_tp = + RM.lift_cmp @@ + Sem.splice_tp @@ + Splice.con vtele @@ fun tele -> + Splice.term @@ + TB.el @@ TB.Tele.unfold tele TB.code_telescope + in + (* [TODO: Reed M, 28/01/2022] Insert the correct amount of Pi.intro here *) + let* fam = T.Chk.run fam_tac fam_tp in + let* vfam = RM.lift_ev @@ Sem.eval fam in + let* extended_tele = + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.con vtele @@ fun tele -> + Splice.con vfam @@ fun fam -> + Splice.term @@ + TB.Tele.extend tele fam + in + RM.quote_con D.Telescope extended_tele + | tp -> RM.expected_connective `Telescope tp +end + +module Signature = +struct + + let rec patch_fields (tele : D.con) (patch_tacs : Ident.user -> T.Chk.tac option) : S.t m = + match tele with + | D.TeleCons (qid, code, lam) -> + let* id = RM.lift_cmp @@ Sem.unquote qid in + let* tp = RM.lift_cmp @@ Sem.do_el code in + (* NOTE: When we add on an extension type, we need to be careful + to insert the requisite elimination forms for the subtype! + This is handled by the 'elim_con'. *) + let* (patch_code, elim_con) = + begin + match patch_tacs id with + | Some tac -> + let* patch = T.Chk.run tac tp in + let* vpatch = RM.lift_ev @@ Sem.eval patch in + let+ ext_code = + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.con code @@ fun code -> + Splice.con vpatch @@ fun patch -> + Splice.term @@ + TB.code_ext 0 code TB.top @@ TB.lam @@ fun _ -> patch + in + let elim_ext arg = + let open CM in + RM.lift_cmp @@ Sem.do_sub_out @<< Sem.do_el_out arg + in + (ext_code, elim_ext) + | None -> + RM.ret (code, RM.ret) + end + in + let* patch_tp = RM.lift_cmp @@ Sem.do_el patch_code in + let* tqid = RM.quote_con D.Symbol qid in + let* tpatch_code = RM.quote_con D.Univ patch_code in + let+ tpatch_lam = + RM.abstract (id :> Ident.t) patch_tp @@ fun x -> + let* elim_x = elim_con x in + let* tele = RM.lift_cmp @@ Sem.do_ap lam elim_x in + let+ patched_tele = patch_fields tele patch_tacs in + S.Lam ((id :> Ident.t), patched_tele) + in + S.TeleCons (tqid, tpatch_code, tpatch_lam) + | con -> + RM.quote_con D.Telescope con + + let patch (sign_tac : T.Chk.tac) (patch_tacs : Ident.user -> T.Chk.tac option) : T.Chk.tac = + T.Chk.rule ~name:"Signature.patch" @@ + function + | D.Univ -> + (* [TODO: Reed M, 26/01/2022] Is there a better way to extract the index out of a signature type? *) + let* code = T.Chk.run sign_tac D.Univ in + let* vcode = RM.lift_ev @@ Sem.eval code in + let* tp = RM.lift_cmp @@ Sem.do_el vcode in + let* whnf_tp = RM.lift_cmp @@ Sem.whnf_tp_ ~style:`UnfoldAll tp in + begin + match whnf_tp with + | D.ElStable (`Signature tele) -> + let+ patched_tele = patch_fields tele patch_tacs in + S.CodeSignature patched_tele + | _ -> + RM.expected_connective `Signature whnf_tp + end + | tp -> RM.expected_connective `Univ tp + + let total (fam_tac : T.Syn.tac) : T.Chk.tac = + T.Chk.rule ~name:"Signature.total" @@ + function + | D.Univ -> + let* (tm, tp) = T.Syn.run fam_tac in + begin + match tp with + | D.Pi (D.ElStable (`Signature tele) as base, ident, clo) -> + (* HACK: Because we are using Weak Tarski Universes, we can't just + use the conversion checker to equate 'fam' and 'univ', as + 'fam' may be 'el code-univ' instead. + + Therefore, we do an explicit check here instead. + If we add universe levels, this code should probably be reconsidered. *) + let* _ = T.abstract ~ident base @@ fun var -> + let* fam = RM.lift_cmp @@ Sem.inst_tp_clo clo (T.Var.con var) in + match fam with + | D.Univ -> RM.ret () + | D.ElStable `Univ -> RM.ret () + | _ -> RM.expected_connective `Univ fam + in + let* vtm = RM.lift_ev @@ Sem.eval tm in + let* vtotal_tele = + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.con tele @@ fun tele -> + Splice.con vtm @@ fun tm -> + Splice.term @@ + let curried = + TB.Tele.curry tele TB.code_telescope @@ + TB.lam @@ fun str -> + TB.cons (TB.quoted (`User ["fibre"])) (TB.el_out @@ TB.ap tm [TB.el_in @@ str]) (TB.lam @@ fun _ -> TB.nil) + + in + TB.Tele.extend tele curried + in + let+ total_tele = RM.quote_con D.Telescope vtotal_tele in + S.CodeSignature total_tele + | D.Pi (base, _, _) -> RM.expected_connective `Signature base + | _ -> RM.expected_connective `Pi tp + end + | tp -> RM.expected_connective `Univ tp + + +end diff --git a/src/frontend/Tactics.mli b/src/frontend/Tactics.mli index bc14d811a..a2ea10505 100644 --- a/src/frontend/Tactics.mli +++ b/src/frontend/Tactics.mli @@ -31,3 +31,17 @@ module Elim : sig : case_tac list -> Chk.tac end + +module Pi : sig + val intros : (Ident.t * Chk.tac) list -> Chk.tac -> Chk.tac +end + +module Telescope : sig + val of_list : (Ident.user * Chk.tac) list -> Chk.tac + val extend : Chk.tac -> Chk.tac -> Chk.tac +end + +module Signature : sig + val patch : Chk.tac -> (Ident.user -> Chk.tac option) -> Chk.tac + val total : Syn.tac -> Chk.tac +end diff --git a/test/patch.cooltt b/test/patch.cooltt index ca3700742..0ef4a5cf3 100644 --- a/test/patch.cooltt +++ b/test/patch.cooltt @@ -11,34 +11,34 @@ def patch/inhabit/hole : el-patch := struct (A : ?) (a : ?) #print el-patch-partial #print patch/inhabit -def patch-depends : type := {sig (A : type) (B : type)} as [ A .= nat | B .= A ] -#print patch-depends -def patch-depends/inhabit : patch-depends := struct (A : nat) (B : nat) - -def testing (A Z : type) (B : A → type) (p : Z → sig (x : A) (bx : B x)) (z : Z) : sig (x : A) (bx : B x) as [ x .= p z.x | bx .= p z.bx ] := - p z - -#print testing - --- Record Patching + Total Space Conversion -#fail total-space/fail (fam : sig (A : type) (a : A) -> nat -> type) : type := fam # [] - -def category : type := - sig (ob : type) - (hom : sig (s : ob) (t : ob) → type) - (idn : (x : ob) -> hom # [ s .= x | t .= x ]) - (seq : (f : hom # []) -> (g : hom # [ s .= f.t ]) -> hom # [ s .= f.s | t .= g.t ]) - (seqL : (f : hom # []) -> path {hom # [ s .= f.s | t .= f.t ]} {seq {idn {f.s}} f} f) - (seqR : (f : hom # []) -> path {hom # [ s .= f.s | t .= f.t ]} {seq f {idn {f.t}}} f) - (seqA : (f : hom # []) -> (g : hom # [ s .= f.t ]) -> (h : hom # [ s .= g.t ]) -> path {hom # [ s .= f.s | t .= h.t ]} {seq f {seq g h}} {seq {seq f g} h}) - -#print category - -def types : category := - struct (ob : type) - (hom : args => {args.s} -> {args.t}) - (idn : x => struct (s : x) (t : x) (fib : x => x)) - (seq : f g => struct (s : f.s) (t : g.t) (fib : x => g.fib {f.fib x})) - (seqL : f i => f) - (seqR : f i => f) - (seqA : f g h i => struct (s : f.s) (t : h.t) (fib : x => {h.fib} {{g.fib} {{f.fib} x}})) +-- def patch-depends : type := {sig (A : type) (B : type)} as [ A .= nat | B .= A ] +-- #print patch-depends +-- def patch-depends/inhabit : patch-depends := struct (A : nat) (B : nat) + +-- def testing (A Z : type) (B : A → type) (p : Z → sig (x : A) (bx : B x)) (z : Z) : sig (x : A) (bx : B x) as [ x .= p z.x | bx .= p z.bx ] := +-- p z + +-- #print testing + +-- -- Record Patching + Total Space Conversion +-- #fail total-space/fail (fam : sig (A : type) (a : A) -> nat -> type) : type := fam # [] + +-- def category : type := +-- sig (ob : type) +-- (hom : sig (s : ob) (t : ob) → type) +-- (idn : (x : ob) -> hom # [ s .= x | t .= x ]) +-- (seq : (f : hom # []) -> (g : hom # [ s .= f.t ]) -> hom # [ s .= f.s | t .= g.t ]) +-- (seqL : (f : hom # []) -> path {hom # [ s .= f.s | t .= f.t ]} {seq {idn {f.s}} f} f) +-- (seqR : (f : hom # []) -> path {hom # [ s .= f.s | t .= f.t ]} {seq f {idn {f.t}}} f) +-- (seqA : (f : hom # []) -> (g : hom # [ s .= f.t ]) -> (h : hom # [ s .= g.t ]) -> path {hom # [ s .= f.s | t .= h.t ]} {seq f {seq g h}} {seq {seq f g} h}) + +-- #print category + +-- def types : category := +-- struct (ob : type) +-- (hom : args => {args.s} -> {args.t}) +-- (idn : x => struct (s : x) (t : x) (fib : x => x)) +-- (seq : f g => struct (s : f.s) (t : g.t) (fib : x => g.fib {f.fib x})) +-- (seqL : f i => f) +-- (seqR : f i => f) +-- (seqA : f g h i => struct (s : f.s) (t : h.t) (fib : x => {h.fib} {{g.fib} {{f.fib} x}})) diff --git a/unit-test/Framework.ml b/unit-test/Framework.ml new file mode 100644 index 000000000..ebd8c2d06 --- /dev/null +++ b/unit-test/Framework.ml @@ -0,0 +1,70 @@ +open Basis +open Core +open Frontend + +open CodeUnit + +module S = Syntax +module D = Domain + +module Sem = Semantics +module TB = TermBuilder + +module T = Tactic +module R = Refiner +module Elab = Elaborator +module RM = RefineMonad + +module Env = RefineEnv +open Monad.Notation (RM) +module RMU = Monad.Util (RM) + +(** Testing Utilities *) +let library_manager = + match Bantorra.Manager.init ~anchor:"cooltt-lib" ~routers:[] with + | Ok ans -> ans + | Error (`InvalidRouter msg) -> failwith msg (* this should not happen! *) + +let current_lib = + match Bantorra.Manager.load_library_from_cwd library_manager with + | Error (`InvalidLibrary err) -> failwith err + | Ok (lib, _) -> lib + +(** Add an axiom to the current testing context. *) +let bind_axiom (id : string) (tp : S.tp) : S.t RM.m = + let* vtp = RM.lift_ev @@ Sem.eval_tp tp in + let+ sym = RM.add_global (`User [id]) vtp None in + S.Global sym + +(** Check that two terms of type {mtp} are convertible in under a list of {axioms}. *) +let check_tm (axioms : (string * S.tp) list) (mtp : D.tp RM.m) : (S.t list -> D.con RM.m) Alcotest.testable = + let state = RefineState.init_unit CodeUnitID.top_level @@ RefineState.init in + let env = RefineEnv.init current_lib in + let pp fmt m = + let tm = RM.run state env @@ + let* tp = mtp in + let* globals = RMU.map (fun (str, tp) -> bind_axiom str tp) axioms in + let* v = m globals in + RM.quote_con tp v + in + match tm with + | Ok tm -> S.pp Pp.Env.emp fmt tm + | Error err -> Format.fprintf fmt "Error: %s" (Printexc.to_string err) + in + Alcotest.testable pp @@ fun m0 m1 -> + let res = + RM.run state env @@ + let* tp = mtp in + let* globals = RMU.map (fun (str, tp) -> bind_axiom str tp) axioms in + let* v0 = m0 globals in + let* v1 = m1 globals in + RM.lift_conv_ @@ Conversion.equate_con tp v0 v1 + in + match res with + | Ok _ -> true + | Error (Conversion.ConversionError err) -> + (* [TODO: Reed M, 18/01/2022] Register some exception printers instead. *) + Format.printf "Conversion Failed: %a@." Conversion.Error.pp err; + false + | Error _ -> + false diff --git a/unit-test/Framework.mli b/unit-test/Framework.mli new file mode 100644 index 000000000..a0407d5fc --- /dev/null +++ b/unit-test/Framework.mli @@ -0,0 +1,18 @@ +open Core +open Frontend +open CodeUnit + +(** Common Re-Exports *) +module S = Syntax +module D = Domain + +module Sem = Semantics +module TB = TermBuilder + +module T = Tactic +module R = Refiner +module Elab = Elaborator +module RM = RefineMonad + +(** Alcotest checker for semantic terms in some context. *) +val check_tm : (string * S.tp) list -> D.tp RM.m -> (S.t list -> D.con RM.m) Alcotest.testable diff --git a/unit-test/Records.ml b/unit-test/Records.ml new file mode 100644 index 000000000..f13e171fd --- /dev/null +++ b/unit-test/Records.ml @@ -0,0 +1,14 @@ +open Basis +open Core +open Frontend + +open Framework + +open Monad.Notation (RM) + +let () = + let open Alcotest in + Debug.debug_mode true; + run "Records" [ + "Telescope Elimination", [] + ] diff --git a/unit-test/dune b/unit-test/dune new file mode 100644 index 000000000..0e9308715 --- /dev/null +++ b/unit-test/dune @@ -0,0 +1,7 @@ +(tests + (names records framework) + (libraries cooltt.frontend alcotest) + (flags + (:standard -w -8)) + (deps + (glob_files ./cooltt-lib))) \ No newline at end of file