From 28d9d4462401683d366a096c5a9dcf8291fdd5d2 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 26 Jan 2022 08:04:49 -0800 Subject: [PATCH 01/13] Add in the 'tele' universe of telescopes --- src/core/Conversion.ml | 12 ++++++++++++ src/core/Domain.ml | 9 +++++++++ src/core/DomainData.ml | 7 ++++++- src/core/Quote.ml | 17 +++++++++++++++++ src/core/RefineError.ml | 2 ++ src/core/RefineErrorData.ml | 1 + src/core/Refiner.ml | 30 ++++++++++++++++++++++++++++++ src/core/Refiner.mli | 6 ++++++ src/core/Semantics.ml | 20 +++++++++++++++++++- src/core/Syntax.ml | 22 +++++++++++++++++++++- src/core/SyntaxData.ml | 4 ++++ src/core/TermBuilder.ml | 3 +++ src/core/TermBuilder.mli | 2 ++ 13 files changed, 132 insertions(+), 3 deletions(-) diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml index 4c248ac01..230d772b2 100644 --- a/src/core/Conversion.ml +++ b/src/core/Conversion.ml @@ -95,6 +95,7 @@ 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.Telescope, D.Telescope -> ret () | D.Signature sign1, D.Signature sign2 -> equate_sign sign1 sign2 | D.Sub (tp0, phi0, clo0), D.Sub (tp1, phi1, clo1) -> let* () = equate_tp tp0 tp1 in @@ -226,6 +227,17 @@ 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) when Ident.equal id0 id1 -> + 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.tele) + in + equate_con tele_tp tele0 tele1 | D.Signature sign, _, _ -> equate_struct sign con0 con1 | D.Sub (tp, _phi, _), _, _ -> diff --git a/src/core/Domain.ml b/src/core/Domain.ml index fa13afa35..4eab1e2c7 100644 --- a/src/core/Domain.ml +++ b/src/core/Domain.ml @@ -154,6 +154,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 (x, code, tele) -> + Format.fprintf fmt "tele/cons[%a, %a, %a]" + Ident.pp_user x + 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 @@ -212,6 +219,8 @@ struct Format.fprintf fmt "pi[%a,%a,%a]" pp_tp base Ident.pp ident pp_tp_clo fam | Sg _ -> Format.fprintf fmt "" + | Telescope -> + Format.fprintf fmt "" | Signature sign -> Format.fprintf fmt "sig[%a]" pp_sign sign | Sub _ -> diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml index d2ce93cf0..07f9edf0e 100644 --- a/src/core/DomainData.ml +++ b/src/core/DomainData.ml @@ -68,9 +68,13 @@ struct | Base | Loop of dim | Pair of con * con + + | TeleNil + | TeleCons of Ident.user * 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}). *) @@ -107,6 +111,7 @@ struct | TpSplit of (cof * tp_clo) list | Pi of tp * Ident.t * tp_clo | Sg of tp * Ident.t * tp_clo + | Telescope | Signature of sign | Nat | Circle diff --git a/src/core/Quote.ml b/src/core/Quote.ml index 1bb4a059f..2d0553963 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -104,6 +104,21 @@ 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 (id, code, tele) -> + let* tele_tp = + lift_cmp @@ + Sem.splice_tp @@ + Splice.con code @@ fun code -> + Splice.term @@ + TB.pi (TB.el code) (fun _ -> TB.tele) + in + let+ code = quote_con D.Univ code + and+ tele = quote_con tele_tp tele in + S.TeleCons (id, code, tele) + | D.Signature sign, _ -> let+ tfields = quote_fields sign con in S.Struct tfields @@ -430,6 +445,8 @@ 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.Telescope -> + ret S.Telescope | D.Signature sign -> let+ sign = quote_sign sign in S.Signature sign diff --git a/src/core/RefineError.ml b/src/core/RefineError.ml index ca31f4ea7..cc7f99bec 100644 --- a/src/core/RefineError.ml +++ b/src/core/RefineError.ml @@ -18,6 +18,8 @@ let pp_connective fmt = Format.fprintf fmt "pi" | `Sg -> Format.fprintf fmt "sg" + | `Telescope -> + Format.fprintf fmt "tele" | `Signature -> Format.fprintf fmt "sig" | `Univ -> diff --git a/src/core/RefineErrorData.ml b/src/core/RefineErrorData.ml index 157a85d2f..7e9eb1866 100644 --- a/src/core/RefineErrorData.ml +++ b/src/core/RefineErrorData.ml @@ -10,6 +10,7 @@ struct type connective = [ `Pi | `Sg + | `Telescope | `Signature | `Nat | `Circle diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 87e3b556e..5135b4c29 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -521,6 +521,36 @@ struct RM.expected_connective `Sg tp end +module Telescope = +struct + let formation : T.Tp.tac = + T.Tp.rule @@ + RM.ret S.Telescope + + let nil : T.Chk.tac = + T.Chk.rule @@ + function + | D.Telescope -> + RM.ret S.TeleNil + | tp -> RM.expected_connective `Telescope tp + + (* [TODO: Reed M, 26/01/2022] Boundaries? *) + let cons (id : Ident.user) (tac_code : T.Chk.tac) (tac_tele : T.Chk.tac) = + T.Chk.rule @@ + function + | (D.Telescope) -> + 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.tele) + in + let+ tele = T.Chk.run tac_tele tele_tp in + S.TeleCons (id, code, tele) + | tp -> RM.expected_connective `Telescope tp +end module Signature = struct diff --git a/src/core/Refiner.mli b/src/core/Refiner.mli index 8a9af8743..057ddc53b 100644 --- a/src/core/Refiner.mli +++ b/src/core/Refiner.mli @@ -101,6 +101,12 @@ module Sg : sig val pi2 : Syn.tac -> Syn.tac end +module Telescope : sig + val formation : Tp.tac + val nil : Chk.tac + val cons : Ident.user -> Chk.tac -> Chk.tac -> Chk.tac +end + module Signature : sig val formation : Tp.tac telescope -> Tp.tac val intro : (Ident.user -> Chk.tac option) -> Chk.tac diff --git a/src/core/Semantics.ml b/src/core/Semantics.ml index a1e099c6c..140ba4425 100644 --- a/src/core/Semantics.ml +++ b/src/core/Semantics.ml @@ -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 @@ -337,6 +343,8 @@ 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.Telescope -> + ret D.Telescope | D.Signature sign -> let+ sign = subst_sign r x sign in D.Signature sign @@ -504,6 +512,8 @@ 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.Telescope -> + ret D.Telescope | S.Signature sign -> let+ vsign = eval_sign sign in D.Signature vsign @@ -599,6 +609,12 @@ 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 (id, code, tele) -> + let+ code = eval code + and+ tele = eval tele in + D.TeleCons (id, code, tele) | S.Struct fields -> let+ vfields = MU.map (MU.second eval) fields in D.Struct vfields @@ -811,7 +827,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.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) -> diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index a9d0d5488..019733994 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -41,9 +41,12 @@ 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 (x, code, tele) -> Format.fprintf fmt "tele/cons[%a, %a, %a]" Ident.pp_user x dump code dump tele + | Struct fields -> Format.fprintf fmt "struct[%a]" dump_struct fields | 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 "" @@ -102,6 +105,7 @@ 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 "" + | Telescope -> Format.fprintf fmt "tp/tele" | Signature fields -> Format.fprintf fmt "tp/sig[%a]" dump_sign fields | Nat -> Format.fprintf fmt "nat" | Circle -> Format.fprintf fmt "circle" @@ -129,6 +133,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 @@ -148,8 +153,13 @@ struct | Lam _ -> double_arrow | Ap _ -> juxtaposition | Pair _ -> tuple + + | TeleNil -> atom + | TeleCons _ -> cons + | Struct _ -> juxtaposition | Proj _ -> proj + | CofSplit _ -> tuple | Cof (Cof.Eq _) -> cof_eq | Cof (Cof.Join [] | Cof.Meet []) -> atom @@ -198,6 +208,7 @@ struct | Sub _ -> juxtaposition | Pi _ -> arrow | Sg _ -> times + | Telescope -> atom | Signature _ -> juxtaposition | TpESub _ -> substitution | TpLockedPrf _ -> juxtaposition @@ -250,6 +261,13 @@ struct (pp env P.(left_of juxtaposition)) tm0 (pp_atomic env) tm1 | Pair (tm0, tm1) -> pp_tuple (pp env P.isolated) fmt [tm0; tm1] + | TeleNil -> + () + | TeleCons (x, code, tele) -> + Format.fprintf fmt "(%a : %a)@ @,%a" + Ident.pp_user x + (pp env P.(right_of colon)) code + (pp env penv) tele | Struct fields -> Format.fprintf fmt "@[struct %a@]" (pp_fields pp env) fields | Proj (tm, lbl) -> @@ -513,6 +531,8 @@ struct (pp_tp env P.(right_of colon)) base Uuseg_string.pp_utf_8 "×" (pp_tp envx P.(right_of times)) fam + | Telescope -> + Format.fprintf fmt "tele" | Signature fields -> Format.fprintf fmt "sig %a" (pp_sign env) fields | Sub (tp, phi, tm) -> diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml index bba146002..6ea1cac12 100644 --- a/src/core/SyntaxData.ml +++ b/src/core/SyntaxData.ml @@ -24,6 +24,9 @@ struct | Fst of t | Snd of t + | TeleNil + | TeleCons of Ident.user * t * t + | Struct of (Ident.user * t) list | Proj of t * Ident.user @@ -76,6 +79,7 @@ struct | Sub of tp * t * t | Pi of tp * Ident.t * tp | Sg of tp * Ident.t * tp + | Telescope | Signature of sign | Nat | Circle diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml index 287336d0d..84ee88d50 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -153,6 +153,9 @@ let snd m = let+ x = m in S.Snd x +let tele = + ret S.Telescope + let struct_ mfields = let+ fields = MU.map (MU.second (fun x -> x)) mfields in S.Struct fields diff --git a/src/core/TermBuilder.mli b/src/core/TermBuilder.mli index d10011513..6fbfa03de 100644 --- a/src/core/TermBuilder.mli +++ b/src/core/TermBuilder.mli @@ -30,6 +30,8 @@ val snd : t m -> t m val lams : Ident.t list -> (t m list -> t m) -> t m +val tele : tp m + val struct_ : (Ident.user * t m) list -> t m val proj : t m -> Ident.user -> t m From c6e7a99705fc237bc95abf9a3075c2bf29b6f1b0 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 26 Jan 2022 10:33:09 -0800 Subject: [PATCH 02/13] Add some basic tests for telescopes --- cooltt-lib | 1 + src/core/Tactic.ml | 4 +++ src/core/Tactic.mli | 1 + src/core/TermBuilder.ml | 11 +++++++ src/core/TermBuilder.mli | 3 ++ src/frontend/Tactics.ml | 7 ++++ src/frontend/Tactics.mli | 4 +++ unit-test/Framework.ml | 70 ++++++++++++++++++++++++++++++++++++++++ unit-test/Framework.mli | 18 +++++++++++ unit-test/Records.ml | 42 ++++++++++++++++++++++++ unit-test/dune | 7 ++++ 11 files changed, 168 insertions(+) create mode 100644 cooltt-lib create mode 100644 unit-test/Framework.ml create mode 100644 unit-test/Framework.mli create mode 100644 unit-test/Records.ml create mode 100644 unit-test/dune 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/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 84ee88d50..c47c47c64 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -156,6 +156,14 @@ let snd m = let tele = ret S.Telescope +let nil = + ret S.TeleNil + +let cons id mcode mtele = + let+ code = mcode + and+ tele = mtele in + S.TeleCons (id, code, tele) + let struct_ mfields = let+ fields = MU.map (MU.second (fun x -> x)) mfields in S.Struct fields @@ -257,6 +265,9 @@ let signature (mfields : (Ident.user * (S.t m list -> S.tp m)) list) : _ m = let+ fields = scope_fields [] mfields in S.Signature fields +let code_univ = + ret S.CodeUniv + let code_pi mbase mfam : _ m = let+ base = mbase and+ fam = mfam in diff --git a/src/core/TermBuilder.mli b/src/core/TermBuilder.mli index 6fbfa03de..623b15a36 100644 --- a/src/core/TermBuilder.mli +++ b/src/core/TermBuilder.mli @@ -31,6 +31,8 @@ val snd : t m -> t m val lams : Ident.t list -> (t m list -> t m) -> t m val tele : tp m +val nil : t m +val cons : Ident.user -> t m -> t m -> t m val struct_ : (Ident.user * t m) list -> t m val proj : t m -> Ident.user -> t m @@ -81,6 +83,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 diff --git a/src/frontend/Tactics.ml b/src/frontend/Tactics.ml index a05bbe851..9d9046f38 100644 --- a/src/frontend/Tactics.ml +++ b/src/frontend/Tactics.ml @@ -151,3 +151,10 @@ 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 diff --git a/src/frontend/Tactics.mli b/src/frontend/Tactics.mli index bc14d811a..4666de3fc 100644 --- a/src/frontend/Tactics.mli +++ b/src/frontend/Tactics.mli @@ -31,3 +31,7 @@ module Elim : sig : case_tac list -> Chk.tac end + +module Pi : sig + val intros : (Ident.t * Chk.tac) list -> Chk.tac -> Chk.tac +end 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..97ba1c9da --- /dev/null +++ b/unit-test/Records.ml @@ -0,0 +1,42 @@ +open Basis +open Core +open Frontend + +open Framework + +open Monad.Notation (RM) + +let tele_monoid () = + let expected [] = + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.term @@ + TB.cons (`User ["carrier"]) TB.code_univ @@ TB.lam ~ident:(`User ["carrier"]) @@ fun el_carrier -> + let carrier = TB.el_out el_carrier in + TB.cons (`User ["mul"]) (TB.code_pis [carrier; TB.lam @@ fun _ -> carrier] @@ fun _ -> carrier) @@ TB.lam ~ident:(`User ["mul"]) @@ fun _ -> + TB.cons (`User ["unit"]) carrier @@ TB.lam ~ident:(`User ["unit"]) @@ fun _ -> + TB.nil + in + let actual [] = + let tac = + R.Telescope.cons (`User ["carrier"]) R.Univ.univ @@ R.Pi.intro ~ident:(`User ["carrier"]) @@ fun carrier -> + let tac_carrier = T.Chk.syn @@ R.El.elim @@ T.Var.syn carrier in + R.Telescope.cons (`User ["mul"]) (Tactics.Pi.intros [`Anon, tac_carrier; `Anon, tac_carrier] tac_carrier) @@ R.Pi.intro ~ident:(`User ["mul"]) @@ fun _ -> + R.Telescope.cons (`User ["unit"]) tac_carrier @@ R.Pi.intro ~ident:(`User ["unit"]) @@ fun _ -> + R.Telescope.nil + in + let* tele = T.Chk.run tac D.Telescope in + RM.lift_ev @@ Sem.eval tele + in + Alcotest.check (check_tm [] (RM.ret D.Telescope)) + "elaborate the telescope of a monoid" + expected + actual + +let () = + let open Alcotest in + run "Records" [ + "Telescope Elaboration", [ + test_case "tele/monoid/elab" `Quick tele_monoid + ] + ] 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 From 461dfe923bcf4c0764f722c01e19548ea6a114ec Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 26 Jan 2022 14:24:42 -0800 Subject: [PATCH 03/13] Telescope elimination --- src/core/Conversion.ml | 25 +++++++++++++ src/core/Domain.ml | 1 + src/core/DomainData.ml | 1 + src/core/Quote.ml | 26 ++++++++++++++ src/core/Semantics.ml | 44 +++++++++++++++++++++++ src/core/Syntax.ml | 14 ++++++++ src/core/SyntaxData.ml | 1 + src/core/TermBuilder.ml | 7 ++++ src/core/TermBuilder.mli | 1 + unit-test/Records.ml | 76 +++++++++++++++++++++++++++++++++------- 10 files changed, 183 insertions(+), 13 deletions(-) diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml index 230d772b2..ee7d57b2f 100644 --- a/src/core/Conversion.ml +++ b/src/core/Conversion.ml @@ -414,6 +414,31 @@ and equate_frm k0 k1 = TB.el @@ TB.ap mot [TB.loop x] in equate_con loop_tp loop_case0 loop_case1 + | 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.tele @@ 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.univ @@ fun a -> + TB.pi (TB.pi (TB.el a) @@ fun _ -> TB.tele) @@ fun t -> + TB.pi (TB.pi (TB.el a) @@ fun x -> TB.el (TB.ap mot [TB.ap t [x]])) @@ fun _ -> + (* [TODO: Reed M, 26/01/2022] Rethink identifiers in telescopes! *) + TB.el @@ TB.ap mot [TB.cons (`User ["FIXME"]) 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 4eab1e2c7..24b18d9bd 100644 --- a/src/core/Domain.ml +++ b/src/core/Domain.ml @@ -105,6 +105,7 @@ struct | KProj lbl -> Format.fprintf fmt "proj[%a]" Ident.pp_user lbl | KNatElim _ -> Format.fprintf fmt "" | KCircleElim _ -> Format.fprintf fmt "" + | KTeleElim _ -> Format.fprintf fmt "" | KElOut -> Uuseg_string.pp_utf_8 fmt "⭝ₑₗ" and pp_cof : cof Pp.printer = diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml index 07f9edf0e..41cf9489b 100644 --- a/src/core/DomainData.ml +++ b/src/core/DomainData.ml @@ -143,6 +143,7 @@ struct | 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 2d0553963..66a437e34 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -658,6 +658,32 @@ 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.KTeleElim (mot, nil_case, cons_case) -> + let* mot_tp = + lift_cmp @@ + Sem.splice_tp @@ + Splice.term @@ + TB.pi TB.tele @@ 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.univ @@ fun a -> + TB.pi (TB.pi (TB.el a) @@ fun _ -> TB.tele) @@ fun t -> + TB.pi (TB.pi (TB.el a) @@ fun x -> TB.el (TB.ap mot [TB.ap t [x]])) @@ fun _ -> + (* [TODO: Reed M, 26/01/2022] Rethink identifiers in telescopes! *) + TB.el @@ TB.ap mot [TB.cons (`User ["FIXME"]) 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/Semantics.ml b/src/core/Semantics.ml index 140ba4425..fd0b500dc 100644 --- a/src/core/Semantics.ml +++ b/src/core/Semantics.ml @@ -484,6 +484,11 @@ 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) and subst_sp : D.dim -> DimProbe.t -> D.frm list -> D.frm list CM.m = @@ -615,6 +620,12 @@ and eval : S.t -> D.con EvM.m = let+ code = eval code and+ tele = eval tele in D.TeleCons (id, 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 @@ -1219,6 +1230,38 @@ and cut_frm_sign (cut : D.cut) (sign : D.sign) (lbl : Ident.user) = | D.Empty -> 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 (id, code, tele) -> + splice_tm @@ + Splice.con mot @@ fun mot -> + Splice.con nil @@ fun nil -> + Splice.con cons @@ fun cons -> + Splice.con code @@ fun code -> + Splice.con tele @@ fun tele -> + Splice.term @@ + TB.ap cons [code; tele; TB.lam ~ident:(id :> Ident.t) @@ 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) + | _ -> + throw @@ NbeFailed ("couldn't eliminate telescope in do_tele_elim") + 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) @@ @@ -1800,6 +1843,7 @@ and do_frm 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 = diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index 019733994..15dcb9868 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -43,6 +43,7 @@ struct | TeleNil -> Format.fprintf fmt "tele/nil" | TeleCons (x, code, tele) -> Format.fprintf fmt "tele/cons[%a, %a, %a]" Ident.pp_user x dump code dump tele + | TeleElim (mot, nil, cons, tele) -> Format.fprintf fmt "tele/elim[%a, %a, %a, %a]" dump mot dump cons dump nil dump tele | Struct fields -> Format.fprintf fmt "struct[%a]" dump_struct fields | Proj (tm, lbl) -> Format.fprintf fmt "proj[%a, %a]" dump tm Ident.pp_user lbl @@ -156,6 +157,7 @@ struct | TeleNil -> atom | TeleCons _ -> cons + | TeleElim _ -> juxtaposition | Struct _ -> juxtaposition | Proj _ -> proj @@ -263,11 +265,23 @@ struct pp_tuple (pp env P.isolated) fmt [tm0; tm1] | TeleNil -> () + | TeleCons (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 (x, code, tele) -> Format.fprintf fmt "(%a : %a)@ @,%a" Ident.pp_user x (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 fields -> Format.fprintf fmt "@[struct %a@]" (pp_fields pp env) fields | Proj (tm, lbl) -> diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml index 6ea1cac12..7657e1f37 100644 --- a/src/core/SyntaxData.ml +++ b/src/core/SyntaxData.ml @@ -26,6 +26,7 @@ struct | TeleNil | TeleCons of Ident.user * t * t + | TeleElim of t * t * t * t | Struct of (Ident.user * t) list | Proj of t * Ident.user diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml index c47c47c64..6786a30f0 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -164,6 +164,13 @@ let cons id mcode mtele = and+ tele = mtele in S.TeleCons (id, 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 diff --git a/src/core/TermBuilder.mli b/src/core/TermBuilder.mli index 623b15a36..057b361b6 100644 --- a/src/core/TermBuilder.mli +++ b/src/core/TermBuilder.mli @@ -33,6 +33,7 @@ val lams : Ident.t list -> (t m list -> t m) -> t m val tele : tp m val nil : t m val cons : Ident.user -> 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 proj : t m -> Ident.user -> t m diff --git a/unit-test/Records.ml b/unit-test/Records.ml index 97ba1c9da..6843d9313 100644 --- a/unit-test/Records.ml +++ b/unit-test/Records.ml @@ -6,18 +6,32 @@ open Framework open Monad.Notation (RM) -let tele_monoid () = - let expected [] = - RM.lift_cmp @@ - Sem.splice_tm @@ - Splice.term @@ - TB.cons (`User ["carrier"]) TB.code_univ @@ TB.lam ~ident:(`User ["carrier"]) @@ fun el_carrier -> - let carrier = TB.el_out el_carrier in - TB.cons (`User ["mul"]) (TB.code_pis [carrier; TB.lam @@ fun _ -> carrier] @@ fun _ -> carrier) @@ TB.lam ~ident:(`User ["mul"]) @@ fun _ -> - TB.cons (`User ["unit"]) carrier @@ TB.lam ~ident:(`User ["unit"]) @@ fun _ -> - TB.nil - in - let actual [] = +(** The telescope for a monoid (without laws!) *) +let monoid_tele _ = + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.term @@ + TB.cons (`User ["carrier"]) TB.code_univ @@ TB.lam ~ident:(`User ["carrier"]) @@ fun el_carrier -> + let carrier = TB.el_out el_carrier in + TB.cons (`User ["mul"]) (TB.code_pis [carrier; TB.lam @@ fun _ -> carrier] @@ fun _ -> carrier) @@ TB.lam ~ident:(`User ["mul"]) @@ fun _ -> + TB.cons (`User ["unit"]) carrier @@ TB.lam ~ident:(`User ["unit"]) @@ fun _ -> + TB.nil + +(** The telescope for a group (without laws!) *) +let group_tele _ = + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.term @@ + TB.cons (`User ["carrier"]) TB.code_univ @@ TB.lam ~ident:(`User ["carrier"]) @@ fun el_carrier -> + let carrier = TB.el_out el_carrier in + TB.cons (`User ["mul"]) (TB.code_pis [carrier; TB.lam @@ fun _ -> carrier] @@ fun _ -> carrier) @@ TB.lam ~ident:(`User ["mul"]) @@ fun _ -> + TB.cons (`User ["unit"]) carrier @@ TB.lam ~ident:(`User ["unit"]) @@ fun _ -> + TB.cons (`User ["inv"]) (TB.code_pis [carrier] @@ fun _ -> carrier) @@ TB.lam ~ident:(`User ["inv"]) @@ fun _ -> + TB.nil + +(** Test that we can elaborate the telescope of a monoid properly. *) +let tele_elab_monoid () = + let actual _ = let tac = R.Telescope.cons (`User ["carrier"]) R.Univ.univ @@ R.Pi.intro ~ident:(`User ["carrier"]) @@ fun carrier -> let tac_carrier = T.Chk.syn @@ R.El.elim @@ T.Var.syn carrier in @@ -30,13 +44,49 @@ let tele_monoid () = in Alcotest.check (check_tm [] (RM.ret D.Telescope)) "elaborate the telescope of a monoid" + monoid_tele + actual + +(** Test that telescope elimination works as expected. *) +let tele_elim_unfold () = + let expected [] = + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.term @@ + TB.code_pi TB.code_univ @@ TB.lam ~ident:(`User ["carrier"]) @@ fun el_carrier -> + let carrier = TB.el_out el_carrier in + TB.code_pi (TB.code_pis [carrier; TB.lam @@ fun _ -> carrier] @@ fun _ -> carrier) @@ TB.lam ~ident:(`User ["mul"]) @@ fun _ -> + TB.code_pi carrier @@ TB.lam ~ident:(`User ["unit"]) @@ fun _ -> + TB.code_univ + in + let actual [] = + let* tele = monoid_tele [] in + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.con tele @@ fun tele -> + Splice.term @@ + let cons_case = + TB.lam ~ident:(`User ["A"]) @@ fun a -> + TB.lam @@ fun _ -> + TB.lam ~ident:(`User ["B"]) @@ fun b -> + TB.code_pi a @@ TB.lam ~ident:(`User ["a"]) @@ fun ax -> + TB.ap b [ax] + in + TB.tele_elim (TB.lam @@ fun _ -> TB.code_univ) TB.code_univ cons_case tele + in + Alcotest.check (check_tm [] (RM.ret D.Telescope)) + "telescope elimination works" expected actual let () = let open Alcotest in + Debug.debug_mode true; run "Records" [ "Telescope Elaboration", [ - test_case "tele/monoid/elab" `Quick tele_monoid + test_case "tele/elab/monoid" `Quick tele_elab_monoid + ]; + "Telescope Elimination", [ + test_case "tele/elim/unfold" `Quick tele_elim_unfold ] ] From 3011648913ad67a45622783108c9ba199192d589 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 26 Jan 2022 14:42:45 -0800 Subject: [PATCH 04/13] Telescope codes --- src/core/Conversion.ml | 2 +- src/core/Domain.ml | 1 + src/core/DomainData.ml | 5 ++++- src/core/Quote.ml | 3 +++ src/core/Refiner.ml | 4 ++++ src/core/Refiner.mli | 1 + src/core/Semantics.ml | 42 +++++++++++++++++++++++++++++++++++++--- src/core/Serialize.ml | 6 ++++-- src/core/Syntax.ml | 6 ++++++ src/core/SyntaxData.ml | 1 + src/core/TermBuilder.ml | 3 +++ src/core/TermBuilder.mli | 1 + 12 files changed, 68 insertions(+), 7 deletions(-) diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml index ee7d57b2f..5d59a3d67 100644 --- a/src/core/Conversion.ml +++ b/src/core/Conversion.ml @@ -145,7 +145,7 @@ and equate_sign sign0 sign1 = and equate_stable_code univ code0 code1 = match code0, code1 with - | `Nat, `Nat | `Circle, `Circle | `Univ, `Univ -> ret () + | `Nat, `Nat | `Circle, `Circle | `Telescope, `Telescope | `Univ, `Univ -> ret () | `Pi (base0, fam0), `Pi (base1, fam1) | `Sg (base0, fam0), `Sg (base1, fam1) -> let* _ = equate_con univ base0 base1 in diff --git a/src/core/Domain.ml b/src/core/Domain.ml index 24b18d9bd..5a19cc07a 100644 --- a/src/core/Domain.ml +++ b/src/core/Domain.ml @@ -256,6 +256,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/DomainData.ml b/src/core/DomainData.ml index 41cf9489b..b8d66cc21 100644 --- a/src/core/DomainData.ml +++ b/src/core/DomainData.ml @@ -17,6 +17,9 @@ struct | `Sg of 'a * 'a (** Dependent sum type *) + | `Telescope + (** The universe of telescopes *) + | `Signature of (Ident.user * 'a) list (** First-Class Record types *) @@ -87,7 +90,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 diff --git a/src/core/Quote.ml b/src/core/Quote.ml index 66a437e34..b9ea37f10 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -327,6 +327,9 @@ and quote_stable_code univ = | `Circle -> ret S.CodeCircle + | `Telescope -> + ret S.CodeTelescope + | `Univ -> ret S.CodeUniv diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 5135b4c29..e13bf8ee7 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -689,6 +689,10 @@ struct let+ tp, fam = quantifier tac_base tac_fam univ in S.CodeSg (tp, fam) + let tele : T.Chk.tac = + univ_tac "Univ.tele" @@ fun _ -> + RM.ret S.CodeTelescope + (* [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, diff --git a/src/core/Refiner.mli b/src/core/Refiner.mli index 057ddc53b..578b3d200 100644 --- a/src/core/Refiner.mli +++ b/src/core/Refiner.mli @@ -61,6 +61,7 @@ module Univ : sig val circle : Chk.tac val pi : Chk.tac -> Chk.tac -> Chk.tac val sg : Chk.tac -> Chk.tac -> Chk.tac + val tele : 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 diff --git a/src/core/Semantics.ml b/src/core/Semantics.ml index fd0b500dc..43a54e1f5 100644 --- a/src/core/Semantics.ml +++ b/src/core/Semantics.ml @@ -406,7 +406,7 @@ and subst_stable_code : D.dim -> DimProbe.t -> D.con D.stable_code -> D.con D.st 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 = @@ -727,12 +727,17 @@ and eval : S.t -> D.con EvM.m = let+ vbase = eval base and+ vfam = eval fam in D.StableCode (`Sg (vbase, vfam)) + + | S.CodeTelescope -> + ret (D.StableCode `Telescope) + | S.CodeSignature fields -> let+ vfields = fields |> MU.map @@ fun (ident, tp) -> let+ vtp = eval tp in (ident, vtp) in D.StableCode (`Signature vfields) + | S.CodeNat -> ret @@ D.StableCode `Nat @@ -1258,6 +1263,33 @@ and do_tele_elim (mot : D.con) (nil : D.con) (cons : D.con) (con : D.con) : D.co 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_tele 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 @@ -1526,6 +1558,10 @@ 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] + + | `Telescope -> + ret D.Telescope + | `Signature fields -> let (lbls, field_cons) = ListUtil.unzip fields in splice_tp @@ @@ -1606,7 +1642,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 -> @@ -1725,7 +1761,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 -> diff --git a/src/core/Serialize.ml b/src/core/Serialize.ml index 09f907848..40433a4f1 100644 --- a/src/core/Serialize.ml +++ b/src/core/Serialize.ml @@ -549,10 +549,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 @@ -689,10 +690,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 15dcb9868..d56da6338 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -74,6 +74,7 @@ struct | CodeExt _ -> Format.fprintf fmt "" | CodePi _ -> Format.fprintf fmt "" | CodeSg _ -> Format.fprintf fmt "" + | CodeTelescope -> Format.fprintf fmt "" | CodeSignature fields -> Format.fprintf fmt "sig[%a]" (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp_user lbl dump tp)) @@ -179,6 +180,7 @@ struct | SubIn _ | SubOut _ | ElIn _ | ElOut _ -> passed | CodePi _ -> arrow | CodeSg _ -> times + | CodeTelescope -> atom | CodeSignature _ -> juxtaposition | CodeExt _ -> juxtaposition @@ -408,8 +410,12 @@ struct Uuseg_string.pp_utf_8 "Σ" (pp_atomic env) base (pp_atomic env) tm + + | CodeTelescope -> + Format.fprintf fmt "tele" | CodeSignature fields -> Format.fprintf fmt "@[sig %a@]" (pp_fields pp_binders env) fields + | CodeExt (_, fam, `Global phi, bdry) -> Format.fprintf fmt "@[ext %a %a %a@]" (pp_atomic env) fam diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml index 7657e1f37..afda184cc 100644 --- a/src/core/SyntaxData.ml +++ b/src/core/SyntaxData.ml @@ -57,6 +57,7 @@ struct | CodeExt of int * t * [`Global of t] * t | CodePi of t * t | CodeSg of t * t + | CodeTelescope | CodeSignature of (Ident.user * t) list | CodeNat | CodeUniv diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml index 6786a30f0..8229cff8d 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -156,6 +156,9 @@ let snd m = let tele = ret S.Telescope +let code_tele = + ret S.CodeTelescope + let nil = ret S.TeleNil diff --git a/src/core/TermBuilder.mli b/src/core/TermBuilder.mli index 057b361b6..66b1df5fb 100644 --- a/src/core/TermBuilder.mli +++ b/src/core/TermBuilder.mli @@ -31,6 +31,7 @@ val snd : t m -> t m val lams : Ident.t list -> (t m list -> t m) -> t m val tele : tp m +val code_tele : t m val nil : t m val cons : Ident.user -> t m -> t m -> t m val tele_elim : t m -> t m -> t m -> t m -> t m From 440a13c5aa43488014ddd713f631f1bd080ecf70 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 26 Jan 2022 14:49:16 -0800 Subject: [PATCH 05/13] Add macro for unfolding a telescope --- src/core/Splice.ml | 16 ++++++++++++++++ src/core/Splice.mli | 5 +++++ unit-test/Records.ml | 11 +---------- 3 files changed, 22 insertions(+), 10 deletions(-) diff --git a/src/core/Splice.ml b/src/core/Splice.ml index 264953013..2d05f5129 100644 --- a/src/core/Splice.ml +++ b/src/core/Splice.ml @@ -174,4 +174,20 @@ struct term @@ TB.ap bdy [TB.prf] end +module Tele = +struct + let unfold code tele = + F.con code @@ fun code -> + F.con tele @@ fun tele -> + let nil_case = code in + let cons_case = + TB.lam ~ident:(`User ["A"]) @@ fun a -> + TB.lam @@ fun _ -> + TB.lam ~ident:(`User ["B"]) @@ fun b -> + TB.code_pi a @@ TB.lam ~ident:(`User ["a"]) @@ fun ax -> + TB.ap b [ax] + in + term @@ TB.tele_elim (TB.lam @@ fun _ -> TB.code_univ) nil_case cons_case tele +end + include F diff --git a/src/core/Splice.mli b/src/core/Splice.mli index a465db08c..abc24fe86 100644 --- a/src/core/Splice.mli +++ b/src/core/Splice.mli @@ -47,3 +47,8 @@ sig val unstable_code : D.con D.unstable_code -> bdry val unstable_frm : D.cut -> D.unstable_frm -> bdry end + +module Tele : +sig + val unfold : D.con -> D.con -> S.t t +end diff --git a/unit-test/Records.ml b/unit-test/Records.ml index 6843d9313..71b3a6fb8 100644 --- a/unit-test/Records.ml +++ b/unit-test/Records.ml @@ -63,16 +63,7 @@ let tele_elim_unfold () = let* tele = monoid_tele [] in RM.lift_cmp @@ Sem.splice_tm @@ - Splice.con tele @@ fun tele -> - Splice.term @@ - let cons_case = - TB.lam ~ident:(`User ["A"]) @@ fun a -> - TB.lam @@ fun _ -> - TB.lam ~ident:(`User ["B"]) @@ fun b -> - TB.code_pi a @@ TB.lam ~ident:(`User ["a"]) @@ fun ax -> - TB.ap b [ax] - in - TB.tele_elim (TB.lam @@ fun _ -> TB.code_univ) TB.code_univ cons_case tele + Splice.Tele.unfold (D.StableCode `Univ) tele in Alcotest.check (check_tm [] (RM.ret D.Telescope)) "telescope elimination works" From 1e6ab625ddb2d074fd2273e062a300dd9e42c61f Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 26 Jan 2022 16:08:42 -0800 Subject: [PATCH 06/13] Port over signatures to use telescopes instead --- src/core/Conversion.ml | 51 +++-------- src/core/Domain.ml | 23 +---- src/core/Domain.mli | 3 - src/core/DomainData.ml | 10 +-- src/core/Quote.ml | 37 +++----- src/core/Quote.mli | 1 - src/core/RefineError.ml | 2 +- src/core/RefineErrorData.ml | 2 +- src/core/RefineMonad.ml | 5 +- src/core/RefineMonad.mli | 2 +- src/core/Refiner.ml | 175 +++++------------------------------- src/core/Refiner.mli | 6 +- src/core/Semantics.ml | 125 ++++++++++---------------- src/core/Semantics.mli | 1 - src/core/Serialize.ml | 42 ++------- src/core/Syntax.ml | 36 ++++---- src/core/Syntax.mli | 4 - src/core/SyntaxData.ml | 6 +- src/core/TermBuilder.ml | 14 +-- src/core/TermBuilder.mli | 2 +- src/frontend/Elaborator.ml | 27 ++---- src/frontend/Tactics.ml | 12 +++ src/frontend/Tactics.mli | 4 + 23 files changed, 161 insertions(+), 429 deletions(-) diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml index 5d59a3d67..eb2e4c3f5 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) -> @@ -96,7 +93,7 @@ let rec equate_tp (tp0 : D.tp) (tp1 : D.tp) = let* fib1 = lift_cmp @@ inst_tp_clo fam1 x in equate_tp fib0 fib1 | D.Telescope, D.Telescope -> ret () - | D.Signature sign1, D.Signature sign2 -> equate_sign sign1 sign2 + | 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 @@ -132,17 +129,6 @@ 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 | `Telescope, `Telescope | `Univ, `Univ -> ret () @@ -178,28 +164,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 ()) @@ @@ -329,16 +298,18 @@ 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) -> +and equate_struct (tele : D.con) con0 con1 = + match tele with + | D.TeleCons (lbl, code, lam) -> let* field0 = lift_cmp @@ do_proj con0 lbl in let* field1 = lift_cmp @@ do_proj con1 lbl 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 *) diff --git a/src/core/Domain.ml b/src/core/Domain.ml index 5a19cc07a..d03e41be7 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 @@ -132,14 +127,6 @@ 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 @@ -208,12 +195,6 @@ 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) -> @@ -222,8 +203,8 @@ struct Format.fprintf fmt "" | Telescope -> Format.fprintf fmt "" - | Signature sign -> - Format.fprintf fmt "sig[%a]" pp_sign sign + | Signature tele -> + Format.fprintf fmt "sig[%a]" pp_con tele | Sub _ -> Format.fprintf fmt "" | TpPrf _ -> 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 b8d66cc21..437b59a15 100644 --- a/src/core/DomainData.ml +++ b/src/core/DomainData.ml @@ -20,7 +20,7 @@ struct | `Telescope (** The universe of telescopes *) - | `Signature of (Ident.user * 'a) list + | `Signature of 'a (** First-Class Record types *) | `Ext of int * 'a * [`Global of 'a] * 'a @@ -51,7 +51,6 @@ 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 = @@ -72,6 +71,7 @@ struct | 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 Ident.user * con * con @@ -115,14 +115,12 @@ struct | Pi of tp * Ident.t * tp_clo | Sg of tp * Ident.t * tp_clo | Telescope - | Signature of sign + (* [TODO: Reed M, 26/01/2022] Should this be something like the stable code situation? *) + | 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 = diff --git a/src/core/Quote.ml b/src/core/Quote.ml index b9ea37f10..8736ff5b7 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -295,15 +295,17 @@ 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) -> +and quote_fields (tele : D.con) con : (Ident.user * S.t) list m = + match tele with + | D.TeleCons (lbl, code, lam) -> let* fcon = lift_cmp @@ do_proj con lbl in - let* sign = lift_cmp @@ inst_sign_clo sign_clo fcon 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 + let+ tfields = quote_fields tele con in (lbl, tfield) :: tfields - | D.Empty -> ret [] + | 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 *) @@ -354,10 +356,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 = @@ -424,16 +425,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 @@ -450,9 +441,9 @@ and quote_tp (tp : D.tp) = S.Sg (tbase, ident, tfam) | D.Telescope -> ret S.Telescope - | D.Signature sign -> - let+ sign = quote_sign sign in - S.Signature sign + | D.Signature tele -> + let+ tele = quote_con D.Telescope tele in + S.Signature tele | D.Univ -> ret S.Univ | D.ElStable code -> 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 cc7f99bec..430c32b9e 100644 --- a/src/core/RefineError.ml +++ b/src/core/RefineError.ml @@ -69,7 +69,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 7e9eb1866..54c19465b 100644 --- a/src/core/RefineErrorData.ml +++ b/src/core/RefineErrorData.ml @@ -28,7 +28,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 e13bf8ee7..023a22682 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -554,15 +554,10 @@ 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 @@ -573,21 +568,22 @@ 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 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 (lbl, code, lam) -> let tac = match tacs lbl with | Some tac -> tac | None -> Hole.unleash_hole (Ident.user_to_string_opt lbl) 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 lbl) @@ 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 + (lbl, 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" @@ @@ -597,16 +593,17 @@ 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) (lbl : 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) -> + | D.TeleCons (flbl, code, _) when Ident.equal flbl lbl -> + RM.lift_cmp @@ Sem.do_el code + | D.TeleCons (flbl, __, lam) -> let* vfield = RM.lift_ev @@ Sem.eval @@ S.Proj (tstruct, flbl) in - let* vsign = RM.lift_cmp @@ Sem.inst_sign_clo clo vfield in + let* vsign = RM.lift_cmp @@ Sem.do_ap lam vfield in go vsign - | D.Empty -> RM.expected_field sign tstruct lbl - in go sign + | _ -> RM.expected_field tele tstruct lbl + in go tele let proj tac lbl : T.Syn.tac = T.Syn.rule ~name:"Signature.proj" @@ @@ -693,134 +690,10 @@ struct univ_tac "Univ.tele" @@ fun _ -> RM.ret S.CodeTelescope - (* [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 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 578b3d200..f43e59058 100644 --- a/src/core/Refiner.mli +++ b/src/core/Refiner.mli @@ -62,9 +62,7 @@ module Univ : sig val pi : Chk.tac -> Chk.tac -> Chk.tac val sg : Chk.tac -> Chk.tac -> Chk.tac val tele : 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 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 @@ -109,7 +107,7 @@ module Telescope : sig 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 43a54e1f5..36eb02ac2 100644 --- a/src/core/Semantics.ml +++ b/src/core/Semantics.ml @@ -308,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 @@ -321,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 @@ -345,9 +329,9 @@ and subst_tp : D.dim -> DimProbe.t -> D.tp -> D.tp CM.m = D.Sg (base, ident, fam) | D.Telescope -> ret D.Telescope - | 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 @@ -399,9 +383,9 @@ 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 @@ -495,15 +479,6 @@ 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 @@ -519,9 +494,9 @@ and eval_tp : S.tp -> D.tp EvM.m = D.Sg (vbase, ident, D.Clo (fam, env)) | S.Telescope -> ret D.Telescope - | S.Signature sign -> - let+ vsign = eval_sign sign in - D.Signature vsign + | S.Signature tele -> + let+ tele = eval tele in + D.Signature tele | S.Univ -> ret D.Univ | S.El tm -> @@ -731,12 +706,9 @@ and eval : S.t -> D.con EvM.m = | S.CodeTelescope -> ret (D.StableCode `Telescope) - | S.CodeSignature fields -> - let+ vfields = fields |> MU.map @@ fun (ident, tp) -> - let+ vtp = eval tp in - (ident, vtp) - in - D.StableCode (`Signature vfields) + | S.CodeSignature tele -> + let+ tele = eval tele in + D.StableCode (`Signature tele) | S.CodeNat -> ret @@ D.StableCode `Nat @@ -1154,12 +1126,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 @@ -1223,16 +1189,19 @@ 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) (lbl : 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 (flbl, code, _) when Ident.equal flbl lbl -> + let+ tp = do_el code in + cut_frm ~tp ~cut (D.KProj lbl) + | D.TeleCons (flbl, _, lam) -> + let* field = cut_frm_tele cut tele flbl 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 lbl + | _ -> 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 = @@ -1311,8 +1280,8 @@ and do_proj (con : D.con) (lbl : Ident.user) : D.con CM.m = 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 @@ -1562,11 +1531,8 @@ and unfold_el : D.con D.stable_code -> D.tp CM.m = | `Telescope -> ret D.Telescope - | `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 + | `Signature tele -> + ret @@ D.Signature tele | `Ext (n, fam, `Global phi, bdry) -> splice_tp @@ @@ -1659,14 +1625,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 -> @@ -1740,16 +1706,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 -> diff --git a/src/core/Semantics.mli b/src/core/Semantics.mli index 0d9306118..20a57d8f4 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 diff --git a/src/core/Serialize.ml b/src/core/Serialize.ml index 40433a4f1..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" @@ -593,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)] -> @@ -628,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) @@ -677,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 diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index d56da6338..b2e4f7e5b 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -45,7 +45,7 @@ struct | TeleCons (x, code, tele) -> Format.fprintf fmt "tele/cons[%a, %a, %a]" Ident.pp_user x dump code dump tele | TeleElim (mot, nil, cons, tele) -> Format.fprintf fmt "tele/elim[%a, %a, %a, %a]" dump mot dump cons dump nil dump tele - | Struct fields -> Format.fprintf fmt "struct[%a]" dump_struct fields + | Struct tele -> Format.fprintf fmt "struct[%a]" dump_struct tele | Proj (tm, lbl) -> Format.fprintf fmt "proj[%a, %a]" dump tm Ident.pp_user lbl | Coe _ -> Format.fprintf fmt "" @@ -75,10 +75,9 @@ struct | CodePi _ -> Format.fprintf fmt "" | CodeSg _ -> Format.fprintf fmt "" | CodeTelescope -> Format.fprintf fmt "" - | CodeSignature fields -> + | 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 "" @@ -89,11 +88,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 @@ -108,7 +104,7 @@ struct | Pi (base, ident, fam) -> Format.fprintf fmt "pi[%a, %a, %a]" dump_tp base Ident.pp ident dump_tp fam | Sg _ -> Format.fprintf fmt "" | Telescope -> Format.fprintf fmt "tp/tele" - | Signature fields -> Format.fprintf fmt "tp/sig[%a]" dump_sign fields + | Signature tele -> Format.fprintf fmt "tp/sig[%a]" dump tele | Nat -> Format.fprintf fmt "nat" | Circle -> Format.fprintf fmt "circle" | TpESub _ -> Format.fprintf fmt "" @@ -245,14 +241,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 -> @@ -284,8 +280,8 @@ struct (pp_atomic env) mot (pp env P.isolated) nil (pp env P.isolated) cons - | Struct fields -> - Format.fprintf fmt "@[struct %a@]" (pp_fields pp env) fields + | Struct tele -> + Format.fprintf fmt "@[struct %a@]" (pp_tele pp env) tele | Proj (tm, lbl) -> Format.fprintf fmt "@[%a %@ %a@]" (pp env P.(left_of proj)) tm Ident.pp_user lbl | CofSplit branches -> @@ -413,8 +409,8 @@ struct | CodeTelescope -> Format.fprintf fmt "tele" - | CodeSignature fields -> - Format.fprintf fmt "@[sig %a@]" (pp_fields pp_binders env) fields + | CodeSignature tele -> + Format.fprintf fmt "@[sig %a@]" (pp env penv) tele | CodeExt (_, fam, `Global phi, bdry) -> Format.fprintf fmt "@[ext %a %a %a@]" @@ -526,8 +522,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 @@ -553,8 +547,8 @@ struct (pp_tp envx P.(right_of times)) fam | Telescope -> Format.fprintf fmt "tele" - | Signature fields -> - Format.fprintf fmt "sig %a" (pp_sign env) fields + | 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 afda184cc..c6ce183cf 100644 --- a/src/core/SyntaxData.ml +++ b/src/core/SyntaxData.ml @@ -58,7 +58,7 @@ struct | CodePi of t * t | CodeSg of t * t | CodeTelescope - | CodeSignature of (Ident.user * t) list + | CodeSignature of t | CodeNat | CodeUniv | CodeV of t * t * t * t @@ -82,14 +82,12 @@ struct | Pi of tp * Ident.t * tp | Sg of tp * Ident.t * tp | Telescope - | Signature of sign + | 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/TermBuilder.ml b/src/core/TermBuilder.ml index 8229cff8d..fea236db1 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -263,17 +263,9 @@ 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_univ = ret S.CodeUniv diff --git a/src/core/TermBuilder.mli b/src/core/TermBuilder.mli index 66b1df5fb..2b49d89a2 100644 --- a/src/core/TermBuilder.mli +++ b/src/core/TermBuilder.mli @@ -70,7 +70,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 diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml index d229bda06..52bee37bf 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 @@ -112,12 +103,12 @@ struct 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.Tele.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 tac = R.Signature.formation (Tactics.Tele.of_list tacs) in *) + (* Tp tac *) let sub tac_tp tac_phi tac_pel : tac = let tac = R.Sub.formation (as_tp tac_tp) tac_phi (fun _ -> tac_pel) in @@ -299,15 +290,15 @@ and chk_tm : CS.con -> T.Chk.tac = Tactics.tac_nary_quantifier quant tacs @@ chk_tm body | 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.Tele.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) + failwith "[FIXME] Core.Core.chk_tm: Patching" + | 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) + failwith "[FIXME] Core.Core.chk_tm: Total Space" + | 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/Tactics.ml b/src/frontend/Tactics.ml index 9d9046f38..49b81b74a 100644 --- a/src/frontend/Tactics.ml +++ b/src/frontend/Tactics.ml @@ -158,3 +158,15 @@ struct 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 Tele = +struct + let rec of_list tacs = + match tacs with + | [] -> + R.Telescope.nil + | (lbl, tac) :: tacs -> + R.Telescope.cons lbl tac @@ + R.Pi.intro ~ident:(lbl :> Ident.t) @@ fun _ -> + of_list tacs +end diff --git a/src/frontend/Tactics.mli b/src/frontend/Tactics.mli index 4666de3fc..609232c22 100644 --- a/src/frontend/Tactics.mli +++ b/src/frontend/Tactics.mli @@ -35,3 +35,7 @@ end module Pi : sig val intros : (Ident.t * Chk.tac) list -> Chk.tac -> Chk.tac end + +module Tele : sig + val of_list : (Ident.user * Chk.tac) list -> Chk.tac +end From d85409a7fa60e8bddc8ca6709b89067ce574c9bf Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 26 Jan 2022 17:24:35 -0800 Subject: [PATCH 07/13] Reimplement record patches with our new framework --- src/core/Domain.ml | 2 +- src/frontend/Elaborator.ml | 3 +- src/frontend/Tactics.ml | 69 ++++++++++++++++++++++++++++++++++++++ src/frontend/Tactics.mli | 4 +++ test/patch.cooltt | 62 +++++++++++++++++----------------- 5 files changed, 107 insertions(+), 33 deletions(-) diff --git a/src/core/Domain.ml b/src/core/Domain.ml index d03e41be7..a2bb2c173 100644 --- a/src/core/Domain.ml +++ b/src/core/Domain.ml @@ -101,7 +101,7 @@ struct | KNatElim _ -> Format.fprintf fmt "" | KCircleElim _ -> Format.fprintf fmt "" | KTeleElim _ -> Format.fprintf fmt "" - | KElOut -> Uuseg_string.pp_utf_8 fmt "⭝ₑₗ" + | KElOut -> Uuseg_string.pp_utf_8 fmt "el/out" and pp_cof : cof Pp.printer = fun fmt cof -> diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml index 52bee37bf..9d48101b6 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -294,7 +294,8 @@ and chk_tm : CS.con -> T.Chk.tac = R.Univ.signature tacs | CS.Patch (tp, patches) -> - failwith "[FIXME] Core.Core.chk_tm: Patching" + 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) -> failwith "[FIXME] Core.Core.chk_tm: Total Space" diff --git a/src/frontend/Tactics.ml b/src/frontend/Tactics.ml index 49b81b74a..6e4ff2fa2 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 @@ -159,6 +161,73 @@ struct tac_nary_quantifier quant tac_args tac_ret 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 (id, code, lam) -> + Debug.print "Doing El for code %a@." D.pp_con code; + 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* 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 (id, 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 +end + module Tele = struct let rec of_list tacs = diff --git a/src/frontend/Tactics.mli b/src/frontend/Tactics.mli index 609232c22..11402743a 100644 --- a/src/frontend/Tactics.mli +++ b/src/frontend/Tactics.mli @@ -36,6 +36,10 @@ module Pi : sig val intros : (Ident.t * Chk.tac) list -> Chk.tac -> Chk.tac end +module Signature : sig + val patch : Chk.tac -> (Ident.user -> Chk.tac option) -> Chk.tac +end + module Tele : sig val of_list : (Ident.user * Chk.tac) list -> 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}})) From 2d5d5a3df673acea49b1620e68681198967de7d4 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 27 Jan 2022 16:36:37 -0800 Subject: [PATCH 08/13] [WIP] Start working in the machinery required for 'total' --- src/core/Conversion.ml | 10 ++++-- src/core/Domain.ml | 1 + src/core/DomainData.ml | 1 + src/core/Quote.ml | 11 ++++-- src/core/Refiner.ml | 2 +- src/core/Semantics.ml | 46 ++++++++++++++++++++++-- src/core/Splice.ml | 16 --------- src/core/Splice.mli | 5 --- src/core/Syntax.ml | 8 +++++ src/core/SyntaxData.ml | 1 + src/core/TermBuilder.ml | 73 ++++++++++++++++++++++++++++++++++++-- src/core/TermBuilder.mli | 11 ++++-- src/frontend/Elaborator.ml | 3 +- src/frontend/Tactics.ml | 39 ++++++++++++++++++++ src/frontend/Tactics.mli | 1 + unit-test/Records.ml | 49 ++++++++++++++++++++----- 16 files changed, 234 insertions(+), 43 deletions(-) diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml index eb2e4c3f5..695d0955d 100644 --- a/src/core/Conversion.ml +++ b/src/core/Conversion.ml @@ -204,7 +204,7 @@ and equate_con tp con0 con1 = lift_cmp @@ Sem.splice_tp @@ Splice.con code0 @@ fun code -> - Splice.term @@ TB.pi (TB.el code) (fun _ -> TB.tele) + Splice.term @@ TB.pi (TB.el code) (fun _ -> TB.telescope) in equate_con tele_tp tele0 tele1 | D.Signature sign, _, _ -> @@ -385,12 +385,16 @@ and equate_frm k0 k1 = TB.el @@ TB.ap mot [TB.loop x] in equate_con loop_tp loop_case0 loop_case1 + | D.KPush (lbl0, code0, field0), D.KPush (lbl1, code1, field1) when Ident.equal lbl0 lbl1 -> + 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.tele @@ fun _ -> TB.univ + TB.pi TB.telescope @@ fun _ -> TB.univ in let* () = equate_con mot_tp mot0 mot1 in let* () = @@ -404,7 +408,7 @@ and equate_frm k0 k1 = Splice.con mot0 @@ fun mot -> Splice.term @@ TB.pi TB.univ @@ fun a -> - TB.pi (TB.pi (TB.el a) @@ fun _ -> TB.tele) @@ fun t -> + 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 _ -> (* [TODO: Reed M, 26/01/2022] Rethink identifiers in telescopes! *) TB.el @@ TB.ap mot [TB.cons (`User ["FIXME"]) a t] diff --git a/src/core/Domain.ml b/src/core/Domain.ml index a2bb2c173..e3b434c44 100644 --- a/src/core/Domain.ml +++ b/src/core/Domain.ml @@ -101,6 +101,7 @@ struct | KNatElim _ -> Format.fprintf fmt "" | KCircleElim _ -> Format.fprintf fmt "" | KTeleElim _ -> Format.fprintf fmt "" + | KPush _ -> Format.fprintf fmt "" | KElOut -> Uuseg_string.pp_utf_8 fmt "el/out" and pp_cof : cof Pp.printer = diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml index 437b59a15..b74a8b0cc 100644 --- a/src/core/DomainData.ml +++ b/src/core/DomainData.ml @@ -141,6 +141,7 @@ struct | KAp of tp * con | KFst | KSnd + | KPush of Ident.user * con * con | KProj of Ident.user | KNatElim of con * con * con | KCircleElim of con * con * con diff --git a/src/core/Quote.ml b/src/core/Quote.ml index 8736ff5b7..89ea72062 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -113,7 +113,7 @@ let rec quote_con (tp : D.tp) con = Sem.splice_tp @@ Splice.con code @@ fun code -> Splice.term @@ - TB.pi (TB.el code) (fun _ -> TB.tele) + TB.pi (TB.el code) (fun _ -> TB.telescope) in let+ code = quote_con D.Univ code and+ tele = quote_con tele_tp tele in @@ -652,12 +652,17 @@ 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 (lbl, code, field) -> + 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 (lbl, tcode, tfield, tm) | D.KTeleElim (mot, nil_case, cons_case) -> let* mot_tp = lift_cmp @@ Sem.splice_tp @@ Splice.term @@ - TB.pi TB.tele @@ fun _ -> TB.univ + TB.pi TB.telescope @@ fun _ -> TB.univ in let* tmot = quote_con mot_tp mot in let* tnil_case = @@ -671,7 +676,7 @@ and quote_frm tm = Splice.con mot @@ fun mot -> Splice.term @@ TB.pi TB.univ @@ fun a -> - TB.pi (TB.pi (TB.el a) @@ fun _ -> TB.tele) @@ fun t -> + 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 _ -> (* [TODO: Reed M, 26/01/2022] Rethink identifiers in telescopes! *) TB.el @@ TB.ap mot [TB.cons (`User ["FIXME"]) a t] diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 023a22682..0a44172a8 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -545,7 +545,7 @@ struct RM.lift_cmp @@ Sem.splice_tp @@ Splice.con vcode @@ fun code -> - Splice.term @@ TB.pi (TB.el code) (fun _ -> TB.tele) + Splice.term @@ TB.pi (TB.el code) (fun _ -> TB.telescope) in let+ tele = T.Chk.run tac_tele tele_tp in S.TeleCons (id, code, tele) diff --git a/src/core/Semantics.ml b/src/core/Semantics.ml index 36eb02ac2..3904e1dda 100644 --- a/src/core/Semantics.ml +++ b/src/core/Semantics.ml @@ -473,6 +473,10 @@ 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.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 = @@ -604,6 +608,11 @@ and eval : S.t -> D.con EvM.m = | S.Struct fields -> let+ vfields = MU.map (MU.second eval) fields in D.Struct vfields + | S.Push (lbl, code, field, str) -> + let* code = eval code in + let* field = eval field in + let* str = eval str in + lift_cmp @@ do_push lbl code field str | S.Proj (t, lbl) -> let* con = eval t in lift_cmp @@ do_proj con lbl @@ -1246,7 +1255,7 @@ and do_tele_elim (mot : D.con) (nil : D.con) (cons : D.con) (con : D.con) : D.co TB.lam @@ fun i -> let fhcom = TB.el_out @@ - TB.hcom TB.code_tele r i phi @@ + TB.hcom TB.code_telescope r i phi @@ TB.lam @@ fun j -> TB.lam @@ fun prf -> TB.el_in @@ TB.ap bdy [j; prf] @@ -1263,6 +1272,36 @@ and do_tele_elim (mot : D.con) (nil : D.con) (cons : D.con) (con : D.con) : D.co throw @@ NbeFailed ("couldn't eliminate telescope in do_tele_elim") end +and do_push (lbl : Ident.user) (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 code @@ fun code -> + Splice.con field @@ fun field -> + Splice.Macro.commute_split con phis (TB.push lbl code field) in + begin + inspect_con ~style:`UnfoldNone con |>> + function + | D.Struct fields -> ret @@ D.Struct ((lbl, 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 code @@ fun code -> + Splice.con tele @@ fun tele -> + Splice.term @@ + (* We need to know the code of the type here! *) + TB.signature (TB.cons lbl code (TB.lam @@ fun _ -> tele)) + in + cut_frm ~tp ~cut (D.KPush (lbl, 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) @@ @@ -1274,7 +1313,9 @@ 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 @@ -1843,6 +1884,7 @@ 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 diff --git a/src/core/Splice.ml b/src/core/Splice.ml index 2d05f5129..264953013 100644 --- a/src/core/Splice.ml +++ b/src/core/Splice.ml @@ -174,20 +174,4 @@ struct term @@ TB.ap bdy [TB.prf] end -module Tele = -struct - let unfold code tele = - F.con code @@ fun code -> - F.con tele @@ fun tele -> - let nil_case = code in - let cons_case = - TB.lam ~ident:(`User ["A"]) @@ fun a -> - TB.lam @@ fun _ -> - TB.lam ~ident:(`User ["B"]) @@ fun b -> - TB.code_pi a @@ TB.lam ~ident:(`User ["a"]) @@ fun ax -> - TB.ap b [ax] - in - term @@ TB.tele_elim (TB.lam @@ fun _ -> TB.code_univ) nil_case cons_case tele -end - include F diff --git a/src/core/Splice.mli b/src/core/Splice.mli index abc24fe86..a465db08c 100644 --- a/src/core/Splice.mli +++ b/src/core/Splice.mli @@ -47,8 +47,3 @@ sig val unstable_code : D.con D.unstable_code -> bdry val unstable_frm : D.cut -> D.unstable_frm -> bdry end - -module Tele : -sig - val unfold : D.con -> D.con -> S.t t -end diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index b2e4f7e5b..e61a57696 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -46,6 +46,7 @@ struct | TeleElim (mot, nil, cons, tele) -> Format.fprintf fmt "tele/elim[%a, %a, %a, %a]" dump mot dump cons dump nil dump tele | Struct tele -> Format.fprintf fmt "struct[%a]" dump_struct tele + | Push (lbl, code, field, str) -> Format.fprintf fmt "push[%a, %a, %a, %a]" Ident.pp_user lbl 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 "" @@ -157,6 +158,7 @@ struct | TeleElim _ -> juxtaposition | Struct _ -> juxtaposition + | Push _ -> juxtaposition | Proj _ -> proj | CofSplit _ -> tuple @@ -282,6 +284,12 @@ struct (pp env P.isolated) cons | Struct tele -> Format.fprintf fmt "@[struct %a@]" (pp_tele pp env) tele + | Push (lbl, code, field, str) -> + Format.fprintf fmt "@[push %a %a %a %a@]" + Ident.pp_user lbl + (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 | CofSplit branches -> diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml index c6ce183cf..0f2dab22b 100644 --- a/src/core/SyntaxData.ml +++ b/src/core/SyntaxData.ml @@ -29,6 +29,7 @@ struct | TeleElim of t * t * t * t | Struct of (Ident.user * t) list + | Push of Ident.user * t * t * t | Proj of t * Ident.user | Coe of t * t * t * t diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml index fea236db1..76c43ab31 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -153,10 +153,10 @@ let snd m = let+ x = m in S.Snd x -let tele = +let telescope = ret S.Telescope -let code_tele = +let code_telescope = ret S.CodeTelescope let nil = @@ -178,6 +178,12 @@ let struct_ mfields = let+ fields = MU.map (MU.second (fun x -> x)) mfields in S.Struct fields +let push lbl mcode mfield mstr = + let+ code = mcode + and+ field = mfield + and+ str = mstr in + S.Push (lbl, code, field, str) + let proj m lbl = let+ x = m in S.Proj (x, lbl) @@ -267,6 +273,10 @@ 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 @@ -777,6 +787,65 @@ struct end end +module Tele = +struct + + (** Unfold a telescope into a pi type. *) + let unfold tele code = + let nil_case = code in + let cons_case = + lam ~ident:(`User ["A"]) @@ fun a -> + lam @@ fun _ -> + lam ~ident:(`User ["B"]) @@ fun b -> + code_pi a @@ lam ~ident:(`User ["a"]) @@ fun ax -> + ap b [ax] + in + tele_elim (lam @@ fun _ -> code_univ) nil_case cons_case tele + + let extend tele fam = + let mot = + lam @@ fun t -> + code_pi (unfold t code_telescope) @@ lam @@ fun _ -> code_telescope + in + let nil_case = + lam @@ fun t -> t + in + let cons_case = + lam @@ fun a -> + lam @@ fun _ -> + lam @@ fun p -> + lam @@ fun k -> + (* [TODO: Reed M, 26/01/2022] It's somewhat unclear what identifier to use here... *) + cons (`User ["FIXME"]) a @@ lam @@ fun z -> ap p [z; ap k [z]] + in + ap (tele_elim mot nil_case cons_case tele) [fam] + + (* To be able to write this, I need to be able to cons something onto a struct... *) + let curry tele code uncurried = + let mot = + lam @@ fun t -> + code_pi (code_pi (code_signature t) @@ lam @@ fun _ -> code) @@ lam @@ fun _ -> + unfold t code + in + let nil_case = + lam @@ fun k -> + el_in @@ + ap k [struct_ []] + in + let cons_case = + lam @@ fun code -> + lam @@ fun _ -> + lam @@ fun c -> + lam @@ fun u -> + el_in @@ + lam @@ fun field -> + (* [TODO: Reed M, 27/01/2022] It's somewhat unclear what identifier to use here... *) + ap c [field; lam @@ fun t_struct -> ap u [push (`User ["FIXME"]) code field t_struct]] + in + ap (tele_elim mot nil_case cons_case tele) [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 2b49d89a2..2cee0377a 100644 --- a/src/core/TermBuilder.mli +++ b/src/core/TermBuilder.mli @@ -30,13 +30,14 @@ val snd : t m -> t m val lams : Ident.t list -> (t m list -> t m) -> t m -val tele : tp m -val code_tele : t m +val telescope : tp m +val code_telescope : t m val nil : t m val cons : Ident.user -> 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 : Ident.user -> t m -> t m -> t m -> t m val proj : t m -> Ident.user -> t m val zero : t m @@ -145,6 +146,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/Elaborator.ml b/src/frontend/Elaborator.ml index 9d48101b6..6aafafc26 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -298,7 +298,8 @@ and chk_tm : CS.con -> T.Chk.tac = Tactics.Signature.patch (chk_tm tp) (R.Signature.find_field_tac tacs) | CS.Total (tp, patches) -> - failwith "[FIXME] Core.Core.chk_tm: Total Space" + 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/Tactics.ml b/src/frontend/Tactics.ml index 6e4ff2fa2..76342fe7c 100644 --- a/src/frontend/Tactics.ml +++ b/src/frontend/Tactics.ml @@ -226,6 +226,45 @@ struct 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 @@ + TB.Tele.extend tele (TB.Tele.curry tele TB.code_telescope @@ TB.lam @@ fun str -> TB.cons (`User ["FIXME"]) (TB.ap tm [str]) (TB.lam @@ fun _ -> TB.nil)) + 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 module Tele = diff --git a/src/frontend/Tactics.mli b/src/frontend/Tactics.mli index 11402743a..e45646807 100644 --- a/src/frontend/Tactics.mli +++ b/src/frontend/Tactics.mli @@ -38,6 +38,7 @@ end module Signature : sig val patch : Chk.tac -> (Ident.user -> Chk.tac option) -> Chk.tac + val total : Syn.tac -> Chk.tac end module Tele : sig diff --git a/unit-test/Records.ml b/unit-test/Records.ml index 71b3a6fb8..f1b58700f 100644 --- a/unit-test/Records.ml +++ b/unit-test/Records.ml @@ -43,9 +43,7 @@ let tele_elab_monoid () = RM.lift_ev @@ Sem.eval tele in Alcotest.check (check_tm [] (RM.ret D.Telescope)) - "elaborate the telescope of a monoid" - monoid_tele - actual + "elaborate the telescope of a monoid" monoid_tele actual (** Test that telescope elimination works as expected. *) let tele_elim_unfold () = @@ -63,12 +61,46 @@ let tele_elim_unfold () = let* tele = monoid_tele [] in RM.lift_cmp @@ Sem.splice_tm @@ - Splice.Tele.unfold (D.StableCode `Univ) tele + Splice.con tele @@ fun tele -> + Splice.term @@ + TB.Tele.unfold tele TB.code_univ in Alcotest.check (check_tm [] (RM.ret D.Telescope)) - "telescope elimination works" - expected - actual + "telescope elimination works" expected actual + +let tele_elim_curry () = + let tp = + let* tele = monoid_tele [] in + RM.lift_cmp @@ + Sem.splice_tp @@ + Splice.con tele @@ fun tele -> + Splice.term @@ + TB.el @@ TB.Tele.unfold tele TB.code_univ + in + let expected [] = + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.term @@ + TB.el_in @@ + TB.lam ~ident:(`User ["carrier"]) @@ fun carrier -> + TB.el_in @@ + TB.lam @@ fun _ -> + TB.el_in @@ + TB.lam @@ fun _ -> + TB.el_in @@ + carrier + in + let actual [] = + let* tele = monoid_tele [] in + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.con tele @@ fun tele -> + Splice.term @@ + TB.Tele.curry tele TB.code_univ (TB.lam @@ fun str -> TB.proj str (`User ["carrier"])) + in + Alcotest.check (check_tm [] tp) + "currying works" expected actual + let () = let open Alcotest in @@ -78,6 +110,7 @@ let () = test_case "tele/elab/monoid" `Quick tele_elab_monoid ]; "Telescope Elimination", [ - test_case "tele/elim/unfold" `Quick tele_elim_unfold + test_case "tele/elim/unfold" `Quick tele_elim_unfold; + test_case "tele/elim/uncurry" `Quick tele_elim_curry ] ] From 0641e2e5a4a13632523aef78b146cca0d1f0f091 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 27 Jan 2022 16:53:01 -0800 Subject: [PATCH 09/13] Define the type of quoted symbols --- src/core/Conversion.ml | 2 ++ src/core/Domain.ml | 4 ++++ src/core/DomainData.ml | 5 ++++- src/core/Quote.ml | 5 +++++ src/core/RefineError.ml | 2 ++ src/core/RefineErrorData.ml | 1 + src/core/Refiner.ml | 20 +++++++++++++++++--- src/core/Refiner.mli | 5 +++++ src/core/Semantics.ml | 12 +++++++----- src/core/Syntax.ml | 10 ++++++++-- src/core/SyntaxData.ml | 3 +++ 11 files changed, 58 insertions(+), 11 deletions(-) diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml index 695d0955d..7a1419cd3 100644 --- a/src/core/Conversion.ml +++ b/src/core/Conversion.ml @@ -182,6 +182,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 diff --git a/src/core/Domain.ml b/src/core/Domain.ml index e3b434c44..e60b06aaf 100644 --- a/src/core/Domain.ml +++ b/src/core/Domain.ml @@ -131,6 +131,8 @@ struct 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 -> @@ -202,6 +204,8 @@ struct Format.fprintf fmt "pi[%a,%a,%a]" pp_tp base Ident.pp ident pp_tp_clo fam | Sg _ -> Format.fprintf fmt "" + | Symbol -> + Format.fprintf fmt "" | Telescope -> Format.fprintf fmt "" | Signature tele -> diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml index b74a8b0cc..431188cbd 100644 --- a/src/core/DomainData.ml +++ b/src/core/DomainData.ml @@ -54,6 +54,9 @@ struct (** 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 @@ -114,8 +117,8 @@ struct | TpSplit of (cof * tp_clo) list | Pi of tp * Ident.t * tp_clo | Sg of tp * Ident.t * tp_clo + | Symbol | Telescope - (* [TODO: Reed M, 26/01/2022] Should this be something like the stable code situation? *) | Signature of con | Nat | Circle diff --git a/src/core/Quote.ml b/src/core/Quote.ml index 89ea72062..25a07a398 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) @@ -439,6 +442,8 @@ 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.Symbol -> + ret S.Symbol | D.Telescope -> ret S.Telescope | D.Signature tele -> diff --git a/src/core/RefineError.ml b/src/core/RefineError.ml index 430c32b9e..367066847 100644 --- a/src/core/RefineError.ml +++ b/src/core/RefineError.ml @@ -18,6 +18,8 @@ let pp_connective fmt = Format.fprintf fmt "pi" | `Sg -> Format.fprintf fmt "sg" + | `Symbol -> + Format.fprintf fmt "symbol" | `Telescope -> Format.fprintf fmt "tele" | `Signature -> diff --git a/src/core/RefineErrorData.ml b/src/core/RefineErrorData.ml index 54c19465b..c5b1a0925 100644 --- a/src/core/RefineErrorData.ml +++ b/src/core/RefineErrorData.ml @@ -10,6 +10,7 @@ struct type connective = [ `Pi | `Sg + | `Symbol | `Telescope | `Signature | `Nat diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 0a44172a8..42aff62bb 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -521,14 +521,28 @@ struct RM.expected_connective `Sg tp end +module Symbol = +struct + let formation : T.Tp.tac = + T.Tp.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 @@ + T.Tp.rule ~name:"Telescope.formation" @@ RM.ret S.Telescope let nil : T.Chk.tac = - T.Chk.rule @@ + T.Chk.rule ~name:"Telescope.nil" @@ function | D.Telescope -> RM.ret S.TeleNil @@ -536,7 +550,7 @@ struct (* [TODO: Reed M, 26/01/2022] Boundaries? *) let cons (id : Ident.user) (tac_code : T.Chk.tac) (tac_tele : T.Chk.tac) = - T.Chk.rule @@ + T.Chk.rule ~name:"Telescope.cons" @@ function | (D.Telescope) -> let* code = T.Chk.run tac_code D.Univ in diff --git a/src/core/Refiner.mli b/src/core/Refiner.mli index f43e59058..26d813399 100644 --- a/src/core/Refiner.mli +++ b/src/core/Refiner.mli @@ -100,6 +100,11 @@ 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 diff --git a/src/core/Semantics.ml b/src/core/Semantics.ml index 3904e1dda..e6ca473ca 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 -> @@ -327,8 +327,6 @@ 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.Telescope -> - ret D.Telescope | D.Signature tele -> let+ tele = subst_con r x tele in D.Signature tele @@ -337,7 +335,7 @@ and subst_tp : D.dim -> DimProbe.t -> D.tp -> D.tp CM.m = 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 @@ -496,6 +494,8 @@ 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.Symbol -> + ret D.Symbol | S.Telescope -> ret D.Telescope | S.Signature tele -> @@ -548,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 -> @@ -824,7 +826,7 @@ 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.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 _ -> diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index e61a57696..e075d8853 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 @@ -104,6 +105,7 @@ 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 "" + | 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" @@ -148,7 +150,7 @@ 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 @@ -202,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 @@ -319,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 []) -> @@ -553,6 +557,8 @@ struct (pp_tp env P.(right_of colon)) base Uuseg_string.pp_utf_8 "×" (pp_tp envx P.(right_of times)) fam + | Symbol -> + Format.fprintf fmt "symbol" | Telescope -> Format.fprintf fmt "tele" | Signature tele -> diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml index 0f2dab22b..83a8acb97 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,6 +25,7 @@ struct | Fst of t | Snd of t + | TeleNil | TeleCons of Ident.user * t * t | TeleElim of t * t * t * t @@ -82,6 +84,7 @@ struct | Sub of tp * t * t | Pi of tp * Ident.t * tp | Sg of tp * Ident.t * tp + | Symbol | Telescope | Signature of t | Nat From 7e53c62a317ed19fb02193a24c80f597d0b88ecd Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Fri, 28 Jan 2022 17:02:12 -0800 Subject: [PATCH 10/13] [WIP] Keep working towards first-class telescopes --- src/core/Conversion.ml | 18 +++-- src/core/Domain.ml | 6 +- src/core/DomainData.ml | 4 +- src/core/Quote.ml | 27 +++---- src/core/Refiner.ml | 110 +++++++++++++++++++++-------- src/core/Refiner.mli | 3 +- src/core/Semantics.ml | 59 ++++++++++------ src/core/Semantics.mli | 1 + src/core/Syntax.ml | 18 ++--- src/core/SyntaxData.ml | 4 +- src/core/TermBuilder.ml | 69 ++++++++++++------ src/core/TermBuilder.mli | 7 +- src/frontend/ConcreteSyntaxData.ml | 6 ++ src/frontend/Driver.ml | 6 ++ src/frontend/Elaborator.ml | 24 +++++-- src/frontend/Grammar.mly | 22 +++++- src/frontend/Lex.mll | 6 ++ src/frontend/Tactics.ml | 105 ++++++++++++++++++++++----- src/frontend/Tactics.mli | 9 +-- 19 files changed, 365 insertions(+), 139 deletions(-) diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml index 7a1419cd3..b17faa033 100644 --- a/src/core/Conversion.ml +++ b/src/core/Conversion.ml @@ -92,6 +92,7 @@ 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.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) -> @@ -200,7 +201,8 @@ and equate_con tp con0 con1 = equate_con fib snd0 snd1 | _, D.TeleNil, D.TeleNil -> ret () - | _, D.TeleCons (id0, code0, tele0), D.TeleCons (id1, code1, tele1) when Ident.equal id0 id1 -> + | _, 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 @@ @@ -302,9 +304,10 @@ and equate_con tp con0 con1 = and equate_struct (tele : D.con) con0 con1 = match tele with - | D.TeleCons (lbl, code, lam) -> - let* field0 = lift_cmp @@ do_proj con0 lbl in - let* field1 = lift_cmp @@ do_proj con1 lbl in + | 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* tele = lift_cmp @@ do_ap lam field0 in @@ -387,7 +390,8 @@ and equate_frm k0 k1 = TB.el @@ TB.ap mot [TB.loop x] in equate_con loop_tp loop_case0 loop_case1 - | D.KPush (lbl0, code0, field0), D.KPush (lbl1, code1, field1) when Ident.equal lbl0 lbl1 -> + | 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 @@ -409,11 +413,11 @@ and equate_frm k0 k1 = 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 _ -> - (* [TODO: Reed M, 26/01/2022] Rethink identifiers in telescopes! *) - TB.el @@ TB.ap mot [TB.cons (`User ["FIXME"]) a t] + TB.el @@ TB.ap mot [TB.cons qid a t] in equate_con cons_tp cons_case0 cons_case1 | D.KElOut, D.KElOut -> diff --git a/src/core/Domain.ml b/src/core/Domain.ml index e60b06aaf..d198d0249 100644 --- a/src/core/Domain.ml +++ b/src/core/Domain.ml @@ -94,7 +94,7 @@ 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 @@ -147,9 +147,9 @@ struct Format.fprintf fmt "pair[%a,%a]" pp_con con0 pp_con con1 | TeleNil -> Format.fprintf fmt "tele/nil" - | TeleCons (x, code, tele) -> + | TeleCons (qid, code, tele) -> Format.fprintf fmt "tele/cons[%a, %a, %a]" - Ident.pp_user x + pp_con qid pp_con code pp_con tele | Struct fields -> diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml index 431188cbd..e5f663670 100644 --- a/src/core/DomainData.ml +++ b/src/core/DomainData.ml @@ -76,7 +76,7 @@ struct (* [TODO: Reed M, 26/01/2022] Does it make sense to handle these in a similar way to codes? *) | TeleNil - | TeleCons of Ident.user * con * con + | TeleCons of con * con * con | Struct of (Ident.user * con) list @@ -144,7 +144,7 @@ struct | KAp of tp * con | KFst | KSnd - | KPush of Ident.user * con * con + | KPush of con * con * con | KProj of Ident.user | KNatElim of con * con * con | KCircleElim of con * con * con diff --git a/src/core/Quote.ml b/src/core/Quote.ml index 25a07a398..d0fa6a720 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -110,17 +110,18 @@ let rec quote_con (tp : D.tp) con = | _, D.TeleNil -> ret S.TeleNil - | _, D.TeleCons (id, code, tele) -> + | _, 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) + TB.pi (TB.el @@ code) (fun _ -> TB.telescope) in - let+ code = quote_con D.Univ code - and+ tele = quote_con tele_tp tele in - S.TeleCons (id, code, tele) + 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 @@ -300,13 +301,14 @@ let rec quote_con (tp : D.tp) con = and quote_fields (tele : D.con) con : (Ident.user * S.t) list m = match tele with - | D.TeleCons (lbl, code, lam) -> - let* fcon = lift_cmp @@ do_proj con lbl in + | 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 tele con in - (lbl, tfield) :: tfields + (id, tfield) :: tfields | D.TeleNil -> ret [] | _ -> failwith "internal error: quote_fields" @@ -657,11 +659,12 @@ 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 (lbl, code, field) -> + | 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 (lbl, tcode, tfield, tm) + S.Push (tqid, tcode, tfield, tm) | D.KTeleElim (mot, nil_case, cons_case) -> let* mot_tp = lift_cmp @@ @@ -680,11 +683,11 @@ and quote_frm tm = 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 _ -> - (* [TODO: Reed M, 26/01/2022] Rethink identifiers in telescopes! *) - TB.el @@ TB.ap mot [TB.cons (`User ["FIXME"]) a t] + 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) diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 42aff62bb..126eccc96 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -524,7 +524,7 @@ end module Symbol = struct let formation : T.Tp.tac = - T.Tp.rule ~name:"Symbol.formation" @@ + T.Tp.virtual_rule ~name:"Symbol.formation" @@ RM.ret S.Symbol let quote id : T.Chk.tac = @@ -541,29 +541,71 @@ struct 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" @@ - function - | D.Telescope -> - RM.ret S.TeleNil - | tp -> RM.expected_connective `Telescope tp + fun tp -> + let+ () = assert_tele tp in + S.TeleNil (* [TODO: Reed M, 26/01/2022] Boundaries? *) - let cons (id : Ident.user) (tac_code : T.Chk.tac) (tac_tele : T.Chk.tac) = + let cons (qid_tac : T.Chk.tac) (tac_code : T.Chk.tac) (tac_tele : T.Chk.tac) = T.Chk.rule ~name:"Telescope.cons" @@ - function - | (D.Telescope) -> - 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) + 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 - let+ tele = T.Chk.run tac_tele tele_tp in - S.TeleCons (id, code, tele) - | tp -> RM.expected_connective `Telescope tp + 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 = @@ -584,17 +626,19 @@ struct 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 (lbl, code, lam) -> - let tac = match tacs lbl 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* tp = RM.lift_cmp @@ Sem.do_el code in - let* tfield = T.Chk.brun tac (tp, phi, D.un_lam @@ D.compose (D.proj lbl) @@ D.Lam (`Anon, phi_clo)) 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* tele = RM.lift_cmp @@ Sem.do_ap lam vfield in let+ fields = intro_fields phi phi_clo tele tacs in - (lbl, tfield) :: fields + (id, tfield) :: fields | D.TeleNil -> RM.ret [] | _ -> failwith "[FIXME] Containers.Signature.intro_fields: Handle this case better! This could be a cut!" @@ -607,16 +651,20 @@ struct S.Struct fields | (tp, _, _) -> RM.expected_connective `Signature tp - let proj_tp (tele : D.con) (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.TeleCons (flbl, code, _) when Ident.equal flbl lbl -> - RM.lift_cmp @@ Sem.do_el code - | D.TeleCons (flbl, __, lam) -> - let* vfield = RM.lift_ev @@ Sem.eval @@ S.Proj (tstruct, flbl) in - let* vsign = RM.lift_cmp @@ Sem.do_ap lam vfield in - go vsign - | _ -> RM.expected_field tele tstruct lbl + (* | D.TeleCons (flbl, code, _) when Ident.equal flbl lbl -> *) + (* RM.lift_cmp @@ Sem.do_el code *) + | 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* vfield = RM.lift_ev @@ Sem.eval @@ S.Proj (tstruct, proj_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 = diff --git a/src/core/Refiner.mli b/src/core/Refiner.mli index 26d813399..77bae8b82 100644 --- a/src/core/Refiner.mli +++ b/src/core/Refiner.mli @@ -108,7 +108,8 @@ end module Telescope : sig val formation : Tp.tac val nil : Chk.tac - val cons : Ident.user -> Chk.tac -> Chk.tac -> 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 diff --git a/src/core/Semantics.ml b/src/core/Semantics.ml index e6ca473ca..75bb0bdfb 100644 --- a/src/core/Semantics.ml +++ b/src/core/Semantics.ml @@ -597,10 +597,11 @@ and eval : S.t -> D.con EvM.m = lift_cmp @@ do_snd con | S.TeleNil -> ret D.TeleNil - | S.TeleCons (id, code, tele) -> - let+ code = eval code + | S.TeleCons (qid, code, tele) -> + let+ qid = eval qid + and+ code = eval code and+ tele = eval tele in - D.TeleCons (id, code, tele) + D.TeleCons (qid, code, tele) | S.TeleElim (mot, nil, cons, tele) -> let* mot = eval mot in let* nil = eval nil in @@ -610,11 +611,12 @@ and eval : S.t -> D.con EvM.m = | S.Struct fields -> let+ vfields = MU.map (MU.second eval) fields in D.Struct vfields - | S.Push (lbl, code, field, str) -> + | 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 lbl code field str + lift_cmp @@ do_push qid code field str | S.Proj (t, lbl) -> let* con = eval t in lift_cmp @@ do_proj con lbl @@ -1201,17 +1203,19 @@ and do_snd con : D.con CM.m = end (** We are trying to compute the type of the cute here? *) -and cut_frm_tele (cut : D.cut) (tele : D.con) (lbl : Ident.user) = +and cut_frm_tele (cut : D.cut) (tele : D.con) (cut_id : Ident.user) = let open CM in match tele with - | D.TeleCons (flbl, code, _) when Ident.equal flbl lbl -> - let+ tp = do_el code in - cut_frm ~tp ~cut (D.KProj lbl) - | D.TeleCons (flbl, _, lam) -> - let* field = cut_frm_tele cut tele flbl 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 lbl + | 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") @@ -1223,15 +1227,16 @@ and do_tele_elim (mot : D.con) (nil : D.con) (cons : D.con) (con : D.con) : D.co function | D.TeleNil -> ret nil - | D.TeleCons (id, code, tele) -> + | 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 [code; tele; TB.lam ~ident:(id :> Ident.t) @@ fun x -> TB.tele_elim mot nil cons (TB.ap tele [x])] + 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 -> @@ -1274,18 +1279,21 @@ and do_tele_elim (mot : D.con) (nil : D.con) (cons : D.con) (con : D.con) : D.co throw @@ NbeFailed ("couldn't eliminate telescope in do_tele_elim") end -and do_push (lbl : Ident.user) (code : D.con) (field : D.con) (con : D.con) : D.con CM.m = +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 lbl code field) in + Splice.Macro.commute_split con phis (TB.push qid code field) in begin inspect_con ~style:`UnfoldNone con |>> function - | D.Struct fields -> ret @@ D.Struct ((lbl, field) :: fields) + | 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 -> @@ -1293,13 +1301,13 @@ and do_push (lbl : Ident.user) (code : D.con) (field : D.con) (con : D.con) : D. | 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 @@ - (* We need to know the code of the type here! *) - TB.signature (TB.cons lbl code (TB.lam @@ fun _ -> tele)) + TB.signature (TB.cons qid code (TB.lam @@ fun _ -> tele)) in - cut_frm ~tp ~cut (D.KPush (lbl, code, field)) + cut_frm ~tp ~cut (D.KPush (qid, code, field)) | _ -> throw @@ NbeFailed ("Couldn't push argument in do_push") end @@ -1901,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 20a57d8f4..f0b629d35 100644 --- a/src/core/Semantics.mli +++ b/src/core/Semantics.mli @@ -37,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/Syntax.ml b/src/core/Syntax.ml index e075d8853..8a361f0e4 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -43,11 +43,11 @@ struct | Snd tm -> Format.fprintf fmt "snd[%a]" dump tm | TeleNil -> Format.fprintf fmt "tele/nil" - | TeleCons (x, code, tele) -> Format.fprintf fmt "tele/cons[%a, %a, %a]" Ident.pp_user x dump code dump tele - | TeleElim (mot, nil, cons, tele) -> Format.fprintf fmt "tele/elim[%a, %a, %a, %a]" dump mot dump cons dump nil dump tele + | 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 (lbl, code, field, str) -> Format.fprintf fmt "push[%a, %a, %a, %a]" Ident.pp_user lbl dump code dump field dump str + | 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 "" @@ -267,15 +267,15 @@ struct pp_tuple (pp env P.isolated) fmt [tm0; tm1] | TeleNil -> () - | TeleCons (ident, code, Lam (_, body)) -> + | 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 (x, code, tele) -> + | TeleCons (qid, code, tele) -> Format.fprintf fmt "(%a : %a)@ @,%a" - Ident.pp_user x + (pp env penv) qid (pp env P.(right_of colon)) code (pp env penv) tele | TeleElim (mot, nil, cons, tele) -> @@ -286,14 +286,14 @@ struct (pp env P.isolated) cons | Struct tele -> Format.fprintf fmt "@[struct %a@]" (pp_tele pp env) tele - | Push (lbl, code, field, str) -> + | Push (qid, code, field, str) -> Format.fprintf fmt "@[push %a %a %a %a@]" - Ident.pp_user lbl + (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 diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml index 83a8acb97..7f911c840 100644 --- a/src/core/SyntaxData.ml +++ b/src/core/SyntaxData.ml @@ -27,11 +27,11 @@ struct | TeleNil - | TeleCons of Ident.user * t * t + | TeleCons of t * t * t | TeleElim of t * t * t * t | Struct of (Ident.user * t) list - | Push of Ident.user * t * t * t + | Push of t * t * t * t | Proj of t * Ident.user | Coe of t * t * t * t diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml index 76c43ab31..12835ed19 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -153,6 +153,12 @@ 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 @@ -162,10 +168,11 @@ let code_telescope = let nil = ret S.TeleNil -let cons id mcode mtele = - let+ code = mcode +let cons mqid mcode mtele = + let+ qid = mqid + and+ code = mcode and+ tele = mtele in - S.TeleCons (id, code, tele) + S.TeleCons (qid, code, tele) let tele_elim mmot mnil mcons mtele = let+ mot = mmot @@ -178,11 +185,12 @@ let struct_ mfields = let+ fields = MU.map (MU.second (fun x -> x)) mfields in S.Struct fields -let push lbl mcode mfield mstr = - let+ code = mcode +let push mqid mcode mfield mstr = + let+ qid = mqid + and+ code = mcode and+ field = mfield and+ str = mstr in - S.Push (lbl, code, field, str) + S.Push (qid, code, field, str) let proj m lbl = let+ x = m in @@ -792,57 +800,74 @@ struct (** Unfold a telescope into a pi type. *) let unfold tele code = - let nil_case = code in + let mot = lam @@ fun _ -> code_univ in + let nil_case = el_in code in let cons_case = - lam ~ident:(`User ["A"]) @@ fun a -> lam @@ fun _ -> - lam ~ident:(`User ["B"]) @@ fun b -> + 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 - tele_elim (lam @@ fun _ -> code_univ) nil_case cons_case tele + 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 _ -> - lam @@ fun p -> + (* c : Π (x : a) → `Π unfold (t x) → `telescope *) + lam @@ fun c -> + el_in @@ lam @@ fun k -> - (* [TODO: Reed M, 26/01/2022] It's somewhat unclear what identifier to use here... *) - cons (`User ["FIXME"]) a @@ lam @@ fun z -> ap p [z; ap k [z]] + el_in @@ + cons qid a @@ lam @@ fun z -> el_out @@ ap (el_out @@ ap c [z]) [ap (el_out k) [z]] in - ap (tele_elim mot nil_case cons_case tele) [fam] + el_out @@ ap (el_out @@ tele_elim mot nil_case cons_case tele) [fam] - (* To be able to write this, I need to be able to cons something onto a struct... *) let curry tele code uncurried = + (* NOTE: unfold : tele → univ → univ *) let mot = lam @@ fun t -> code_pi (code_pi (code_signature t) @@ lam @@ fun _ -> code) @@ lam @@ fun _ -> unfold t code in let nil_case = - lam @@ fun k -> el_in @@ - ap k [struct_ []] + (* k : `Π (k : `Π `sig [] → code) *) + lam @@ fun k -> + ap (el_out k) [el_in @@ struct_ []] in let cons_case = - lam @@ fun code -> + lam @@ fun qid -> + (* a : univ *) + lam @@ fun a -> + (* t : telescope *) lam @@ fun _ -> + (* c : Π (x : a) → unfold (t x) code → *) lam @@ fun c -> - lam @@ fun u -> el_in @@ + (* u : *) + lam @@ fun u -> lam @@ fun field -> - (* [TODO: Reed M, 27/01/2022] It's somewhat unclear what identifier to use here... *) - ap c [field; lam @@ fun t_struct -> ap u [push (`User ["FIXME"]) code field t_struct]] + ap (el_out c) [field; lam @@ fun t_struct -> ap (el_out u) [el_in @@ push qid a field t_struct]] in - ap (tele_elim mot nil_case cons_case tele) [uncurried] + ap (el_out @@ tele_elim mot nil_case cons_case tele) [el_in @@ uncurried] end (* [TODO: Reed M, 26/01/2022] Move this into the unit test suite. *) diff --git a/src/core/TermBuilder.mli b/src/core/TermBuilder.mli index 2cee0377a..f6ff07f0d 100644 --- a/src/core/TermBuilder.mli +++ b/src/core/TermBuilder.mli @@ -30,14 +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 : Ident.user -> t m -> t m -> 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 : Ident.user -> t m -> t m -> t m -> 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 diff --git a/src/frontend/ConcreteSyntaxData.ml b/src/frontend/ConcreteSyntaxData.ml index 01bf0788d..34edeb0e1 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,7 @@ type decl = | Print of Ident.t node | Import of string list * con option | NormalizeTerm of con + | DumpTerm of con | 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..561bb20e7 100644 --- a/src/frontend/Driver.ml +++ b/src/frontend/Driver.ml @@ -175,6 +175,12 @@ 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 + let+ vtm = RM.lift_ev @@ Sem.eval tm in + Debug.print "Dumping Term: %a@." D.pp_con vtm; + 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 6aafafc26..139b4df44 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -39,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 @@ -100,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 (Tactics.Tele.of_list tacs) in + let tac = R.Univ.signature (Tactics.Telescope.of_list tacs) in Code tac | None -> failwith "[FIXME] Core.CoolTp.signature: Handle the case when a signature is full of types!" - (* let tac = R.Signature.formation (Tactics.Tele.of_list tacs) in *) - (* Tp tac *) let sub tac_tp tac_phi tac_pel : tac = let tac = R.Sub.formation (as_tp tac_tp) tac_phi (fun _ -> tac_pel) in @@ -289,8 +290,23 @@ 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 = Tactics.Tele.of_list @@ 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) -> diff --git a/src/frontend/Grammar.mly b/src/frontend/Grammar.mly index c36be59d6..9eb20fb85 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 %token IMPORT %token ELIM %token SEMISEMI EOF @@ -145,6 +145,8 @@ decl: { Quit } | NORMALIZE; tm = term { NormalizeTerm tm } + | DUMP; tm = term + { DumpTerm tm } | unitpath = IMPORT; m = ioption(bracketed_modifier) { Import (unitpath, m) } | PRINT; name = name @@ -241,6 +243,10 @@ plain_atomic_term_except_name: { Base } | CIRCLE { Circle } + | NIL + { Nil } + | TELESCOPE + { Telescope } | TYPE { Type } | name = HOLE_NAME @@ -315,14 +321,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,6 +397,10 @@ pat_lbl: { ["base"] } | LOOP { ["loop"] } + | NIL + { ["nil"] } + | CONS + { ["cons"] } | lbl = path { lbl } diff --git a/src/frontend/Lex.mll b/src/frontend/Lex.mll index 3c2f4389d..5b513a8b1 100644 --- a/src/frontend/Lex.mll +++ b/src/frontend/Lex.mll @@ -22,6 +22,7 @@ let commands = ("#fail", FAIL); ("#normalize", NORMALIZE); ("#print", PRINT); + ("#dump", DUMP); ("#quit", QUIT); ] @@ -35,9 +36,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 76342fe7c..ed718d3a9 100644 --- a/src/frontend/Tactics.ml +++ b/src/frontend/Tactics.ml @@ -114,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 @@ -161,14 +188,63 @@ struct 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 + Debug.print "[EXTEND] Constructing Family Type@."; + 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 *) + Debug.print "[EXTEND] Checking Family Type@."; + let* fam = T.Chk.run fam_tac fam_tp in + Debug.print "[EXTEND] Evaluating Family Type@."; + let* vfam = RM.lift_ev @@ Sem.eval fam in + Debug.print "[EXTEND] Extending Telescope@."; + 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 + (* [TODO: Reed M, 28/01/2022] We should probably normalize somewhere here! *) + Debug.print "[EXTEND] Extended Telescope@."; + 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 (id, code, lam) -> - Debug.print "Doing El for code %a@." D.pp_con code; + | D.TeleCons (qid, code, lam) -> + let* id = RM.lift_cmp @@ Sem.unquote qid in + Debug.print "[PATCH] Doing el on field code %a@." D.pp_con code; let* tp = RM.lift_cmp @@ Sem.do_el code in + Debug.print "[PATCH] Did el on field type %a@." D.pp_tp tp; (* 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'. *) @@ -196,6 +272,7 @@ struct 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 -> @@ -204,7 +281,7 @@ struct let+ patched_tele = patch_fields tele patch_tacs in S.Lam ((id :> Ident.t), patched_tele) in - S.TeleCons (id, tpatch_code, tpatch_lam) + S.TeleCons (tqid, tpatch_code, tpatch_lam) | con -> RM.quote_con D.Telescope con @@ -215,7 +292,9 @@ struct (* [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 + Debug.print "[PATCH] El on code %a@." D.pp_con vcode; let* tp = RM.lift_cmp @@ Sem.do_el vcode in + Debug.print "[PATCH] WHNF on type %a@." D.pp_tp tp; let* whnf_tp = RM.lift_cmp @@ Sem.whnf_tp_ ~style:`UnfoldAll tp in begin match whnf_tp with @@ -249,13 +328,19 @@ struct | _ -> RM.expected_connective `Univ fam in let* vtm = RM.lift_ev @@ Sem.eval tm in + (* NOTE: The motive for 'TB.curry' must be a code, hence the el_out. *) let* vtotal_tele = RM.lift_cmp @@ Sem.splice_tm @@ Splice.con tele @@ fun tele -> Splice.con vtm @@ fun tm -> Splice.term @@ - TB.Tele.extend tele (TB.Tele.curry tele TB.code_telescope @@ TB.lam @@ fun str -> TB.cons (`User ["FIXME"]) (TB.ap tm [str]) (TB.lam @@ fun _ -> TB.nil)) + 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 [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 @@ -266,15 +351,3 @@ struct end - -module Tele = -struct - let rec of_list tacs = - match tacs with - | [] -> - R.Telescope.nil - | (lbl, tac) :: tacs -> - R.Telescope.cons lbl tac @@ - R.Pi.intro ~ident:(lbl :> Ident.t) @@ fun _ -> - of_list tacs -end diff --git a/src/frontend/Tactics.mli b/src/frontend/Tactics.mli index e45646807..a2ea10505 100644 --- a/src/frontend/Tactics.mli +++ b/src/frontend/Tactics.mli @@ -36,11 +36,12 @@ 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 - -module Tele : sig - val of_list : (Ident.user * Chk.tac) list -> Chk.tac -end From b33e531e455110ac428c807fe3e411a5c91761d4 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Mon, 31 Jan 2022 11:52:33 -0800 Subject: [PATCH 11/13] Fix issues with various elaborator tricks for telescopes --- src/core/Refiner.ml | 5 ++--- src/core/TermBuilder.ml | 36 ++++++++++++++++++++++++++---------- src/frontend/Tactics.ml | 17 +++-------------- 3 files changed, 31 insertions(+), 27 deletions(-) diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 126eccc96..9b77f843c 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -654,14 +654,13 @@ struct let proj_tp (tele : D.con) (tstruct : S.t) (proj_id : Ident.user) : D.tp m = let rec go = function - (* | D.TeleCons (flbl, code, _) when Ident.equal flbl lbl -> *) - (* RM.lift_cmp @@ Sem.do_el code *) | 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* vfield = RM.lift_ev @@ Sem.eval @@ S.Proj (tstruct, proj_id) in + 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 diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml index 12835ed19..28ae106bc 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -797,6 +797,17 @@ 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 = @@ -841,33 +852,38 @@ struct el_out @@ ap (el_out @@ tele_elim mot nil_case cons_case tele) [fam] let curry tele code uncurried = - (* NOTE: unfold : tele → univ → univ *) 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 @@ - (* k : `Π (k : `Π `sig [] → code) *) - lam @@ fun k -> - ap (el_out k) [el_in @@ struct_ []] + (* 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 : telescope *) + (* t : Π a → telescope *) lam @@ fun _ -> - (* c : Π (x : a) → unfold (t x) code → *) + (* c : Π (x : a) → `Π (k : `Π `sig (t x) → code) → unfold (t x) code *) lam @@ fun c -> el_in @@ - (* u : *) + (* u : `Π `sig (cons qid a t) → a *) lam @@ fun u -> - lam @@ fun field -> - ap (el_out c) [field; lam @@ fun t_struct -> ap (el_out u) [el_in @@ push qid a field t_struct]] + 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 - ap (el_out @@ tele_elim mot nil_case cons_case tele) [el_in @@ uncurried] + (* 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. *) diff --git a/src/frontend/Tactics.ml b/src/frontend/Tactics.ml index ed718d3a9..d627437d5 100644 --- a/src/frontend/Tactics.ml +++ b/src/frontend/Tactics.ml @@ -206,7 +206,6 @@ struct | D.Telescope -> let* tele = T.Chk.run tele_tac D.Telescope in let* vtele = RM.lift_ev @@ Sem.eval tele in - Debug.print "[EXTEND] Constructing Family Type@."; let* fam_tp = RM.lift_cmp @@ Sem.splice_tp @@ @@ -215,11 +214,8 @@ struct TB.el @@ TB.Tele.unfold tele TB.code_telescope in (* [TODO: Reed M, 28/01/2022] Insert the correct amount of Pi.intro here *) - Debug.print "[EXTEND] Checking Family Type@."; let* fam = T.Chk.run fam_tac fam_tp in - Debug.print "[EXTEND] Evaluating Family Type@."; let* vfam = RM.lift_ev @@ Sem.eval fam in - Debug.print "[EXTEND] Extending Telescope@."; let* extended_tele = RM.lift_cmp @@ Sem.splice_tm @@ @@ -228,8 +224,6 @@ struct Splice.term @@ TB.Tele.extend tele fam in - (* [TODO: Reed M, 28/01/2022] We should probably normalize somewhere here! *) - Debug.print "[EXTEND] Extended Telescope@."; RM.quote_con D.Telescope extended_tele | tp -> RM.expected_connective `Telescope tp end @@ -237,14 +231,11 @@ 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 - Debug.print "[PATCH] Doing el on field code %a@." D.pp_con code; let* tp = RM.lift_cmp @@ Sem.do_el code in - Debug.print "[PATCH] Did el on field type %a@." D.pp_tp tp; (* 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'. *) @@ -292,9 +283,7 @@ struct (* [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 - Debug.print "[PATCH] El on code %a@." D.pp_con vcode; let* tp = RM.lift_cmp @@ Sem.do_el vcode in - Debug.print "[PATCH] WHNF on type %a@." D.pp_tp tp; let* whnf_tp = RM.lift_cmp @@ Sem.whnf_tp_ ~style:`UnfoldAll tp in begin match whnf_tp with @@ -328,7 +317,6 @@ struct | _ -> RM.expected_connective `Univ fam in let* vtm = RM.lift_ev @@ Sem.eval tm in - (* NOTE: The motive for 'TB.curry' must be a code, hence the el_out. *) let* vtotal_tele = RM.lift_cmp @@ Sem.splice_tm @@ @@ -336,8 +324,9 @@ struct 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 [str]) (TB.lam @@ fun _ -> TB.nil) + 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 From 801c0aa26ac96ba5f3b4ae1d82b98ed3f82e4356 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Mon, 31 Jan 2022 11:53:29 -0800 Subject: [PATCH 12/13] Add #dump and #debug commands --- src/frontend/ConcreteSyntaxData.ml | 1 + src/frontend/Driver.ml | 5 +++++ src/frontend/Grammar.mly | 11 +++++++++-- src/frontend/Lex.mll | 1 + 4 files changed, 16 insertions(+), 2 deletions(-) diff --git a/src/frontend/ConcreteSyntaxData.ml b/src/frontend/ConcreteSyntaxData.ml index 34edeb0e1..f85230d8f 100644 --- a/src/frontend/ConcreteSyntaxData.ml +++ b/src/frontend/ConcreteSyntaxData.ml @@ -106,6 +106,7 @@ type decl = | 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 561bb20e7..45f0094e0 100644 --- a/src/frontend/Driver.ml +++ b/src/frontend/Driver.ml @@ -178,9 +178,14 @@ and execute_decl : CS.decl -> command = | 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/Grammar.mly b/src/frontend/Grammar.mly index 9eb20fb85..c986a0c97 100644 --- a/src/frontend/Grammar.mly +++ b/src/frontend/Grammar.mly @@ -45,7 +45,7 @@ %token NIL CONS TELESCOPE ROW SIG STRUCT AS EXTEND %token EXT %token COE COM HCOM HFILL -%token QUIT NORMALIZE PRINT DEF AXIOM FAIL DUMP +%token QUIT NORMALIZE PRINT DEF AXIOM FAIL DUMP DEBUG %token IMPORT %token ELIM %token SEMISEMI EOF @@ -147,6 +147,8 @@ decl: { NormalizeTerm tm } | DUMP; tm = term { DumpTerm tm } + | DEBUG; b = flag + { Debug b } | unitpath = IMPORT; m = ioption(bracketed_modifier) { Import (unitpath, m) } | PRINT; name = name @@ -404,7 +406,6 @@ pat_lbl: | lbl = path { lbl } - pat: | lbl = pat_lbl args = list(pat_arg) { Pat {lbl; args} } @@ -430,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 5b513a8b1..c68ac2436 100644 --- a/src/frontend/Lex.mll +++ b/src/frontend/Lex.mll @@ -23,6 +23,7 @@ let commands = ("#normalize", NORMALIZE); ("#print", PRINT); ("#dump", DUMP); + ("#debug", DEBUG); ("#quit", QUIT); ] From 4e95a8d7bedf105b9689e2145bcb3a2042992258 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Mon, 31 Jan 2022 11:55:21 -0800 Subject: [PATCH 13/13] Remove outdated unit tests --- unit-test/Records.ml | 104 +------------------------------------------ 1 file changed, 1 insertion(+), 103 deletions(-) diff --git a/unit-test/Records.ml b/unit-test/Records.ml index f1b58700f..f13e171fd 100644 --- a/unit-test/Records.ml +++ b/unit-test/Records.ml @@ -6,111 +6,9 @@ open Framework open Monad.Notation (RM) -(** The telescope for a monoid (without laws!) *) -let monoid_tele _ = - RM.lift_cmp @@ - Sem.splice_tm @@ - Splice.term @@ - TB.cons (`User ["carrier"]) TB.code_univ @@ TB.lam ~ident:(`User ["carrier"]) @@ fun el_carrier -> - let carrier = TB.el_out el_carrier in - TB.cons (`User ["mul"]) (TB.code_pis [carrier; TB.lam @@ fun _ -> carrier] @@ fun _ -> carrier) @@ TB.lam ~ident:(`User ["mul"]) @@ fun _ -> - TB.cons (`User ["unit"]) carrier @@ TB.lam ~ident:(`User ["unit"]) @@ fun _ -> - TB.nil - -(** The telescope for a group (without laws!) *) -let group_tele _ = - RM.lift_cmp @@ - Sem.splice_tm @@ - Splice.term @@ - TB.cons (`User ["carrier"]) TB.code_univ @@ TB.lam ~ident:(`User ["carrier"]) @@ fun el_carrier -> - let carrier = TB.el_out el_carrier in - TB.cons (`User ["mul"]) (TB.code_pis [carrier; TB.lam @@ fun _ -> carrier] @@ fun _ -> carrier) @@ TB.lam ~ident:(`User ["mul"]) @@ fun _ -> - TB.cons (`User ["unit"]) carrier @@ TB.lam ~ident:(`User ["unit"]) @@ fun _ -> - TB.cons (`User ["inv"]) (TB.code_pis [carrier] @@ fun _ -> carrier) @@ TB.lam ~ident:(`User ["inv"]) @@ fun _ -> - TB.nil - -(** Test that we can elaborate the telescope of a monoid properly. *) -let tele_elab_monoid () = - let actual _ = - let tac = - R.Telescope.cons (`User ["carrier"]) R.Univ.univ @@ R.Pi.intro ~ident:(`User ["carrier"]) @@ fun carrier -> - let tac_carrier = T.Chk.syn @@ R.El.elim @@ T.Var.syn carrier in - R.Telescope.cons (`User ["mul"]) (Tactics.Pi.intros [`Anon, tac_carrier; `Anon, tac_carrier] tac_carrier) @@ R.Pi.intro ~ident:(`User ["mul"]) @@ fun _ -> - R.Telescope.cons (`User ["unit"]) tac_carrier @@ R.Pi.intro ~ident:(`User ["unit"]) @@ fun _ -> - R.Telescope.nil - in - let* tele = T.Chk.run tac D.Telescope in - RM.lift_ev @@ Sem.eval tele - in - Alcotest.check (check_tm [] (RM.ret D.Telescope)) - "elaborate the telescope of a monoid" monoid_tele actual - -(** Test that telescope elimination works as expected. *) -let tele_elim_unfold () = - let expected [] = - RM.lift_cmp @@ - Sem.splice_tm @@ - Splice.term @@ - TB.code_pi TB.code_univ @@ TB.lam ~ident:(`User ["carrier"]) @@ fun el_carrier -> - let carrier = TB.el_out el_carrier in - TB.code_pi (TB.code_pis [carrier; TB.lam @@ fun _ -> carrier] @@ fun _ -> carrier) @@ TB.lam ~ident:(`User ["mul"]) @@ fun _ -> - TB.code_pi carrier @@ TB.lam ~ident:(`User ["unit"]) @@ fun _ -> - TB.code_univ - in - let actual [] = - let* tele = monoid_tele [] in - RM.lift_cmp @@ - Sem.splice_tm @@ - Splice.con tele @@ fun tele -> - Splice.term @@ - TB.Tele.unfold tele TB.code_univ - in - Alcotest.check (check_tm [] (RM.ret D.Telescope)) - "telescope elimination works" expected actual - -let tele_elim_curry () = - let tp = - let* tele = monoid_tele [] in - RM.lift_cmp @@ - Sem.splice_tp @@ - Splice.con tele @@ fun tele -> - Splice.term @@ - TB.el @@ TB.Tele.unfold tele TB.code_univ - in - let expected [] = - RM.lift_cmp @@ - Sem.splice_tm @@ - Splice.term @@ - TB.el_in @@ - TB.lam ~ident:(`User ["carrier"]) @@ fun carrier -> - TB.el_in @@ - TB.lam @@ fun _ -> - TB.el_in @@ - TB.lam @@ fun _ -> - TB.el_in @@ - carrier - in - let actual [] = - let* tele = monoid_tele [] in - RM.lift_cmp @@ - Sem.splice_tm @@ - Splice.con tele @@ fun tele -> - Splice.term @@ - TB.Tele.curry tele TB.code_univ (TB.lam @@ fun str -> TB.proj str (`User ["carrier"])) - in - Alcotest.check (check_tm [] tp) - "currying works" expected actual - - let () = let open Alcotest in Debug.debug_mode true; run "Records" [ - "Telescope Elaboration", [ - test_case "tele/elab/monoid" `Quick tele_elab_monoid - ]; - "Telescope Elimination", [ - test_case "tele/elim/unfold" `Quick tele_elim_unfold; - test_case "tele/elim/uncurry" `Quick tele_elim_curry - ] + "Telescope Elimination", [] ]