From 73c2895e38738f6e240b3e328b7e2d1227d74f9c Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Sat, 30 Apr 2022 14:19:26 -0400 Subject: [PATCH 1/3] bye-bye ElIn/ElOut --- src/core/Conversion.ml | 18 +++++----- src/core/Domain.ml | 5 --- src/core/Domain.mli | 1 - src/core/DomainData.ml | 9 +---- src/core/Quote.ml | 25 +++++--------- src/core/Refiner.ml | 16 ++++----- src/core/Semantics.ml | 74 +++++++++++++--------------------------- src/core/Semantics.mli | 1 - src/core/Serialize.ml | 12 ------- src/core/Syntax.ml | 13 ++----- src/core/SyntaxData.ml | 3 -- src/core/TermBuilder.ml | 59 ++++++++++++-------------------- src/core/TermBuilder.mli | 3 -- src/frontend/Tactics.ml | 14 ++++---- 14 files changed, 81 insertions(+), 172 deletions(-) diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml index f674decca..33a41914a 100644 --- a/src/core/Conversion.ml +++ b/src/core/Conversion.ml @@ -106,8 +106,12 @@ let rec equate_tp (tp0 : D.tp) (tp1 : D.tp) = | D.Circle, D.Circle | D.Univ, D.Univ -> ret () - | D.ElStable code0, D.ElStable code1 -> - equate_stable_code D.Univ code0 code1 + | D.ElStable code0, _ -> + let* tp0 = ConvM.lift_cmp @@ Sem.unfold_el code0 in + equate_tp tp0 tp1 + | _, D.ElStable code1 -> + let* tp1 = ConvM.lift_cmp @@ Sem.unfold_el code1 in + equate_tp tp0 tp1 | D.ElCut cut0, D.ElCut cut1 -> equate_cut cut0 cut1 | D.ElUnstable (`HCom (r0, s0, phi0, bdy0)), D.ElUnstable (`HCom (r1, s1, phi1, bdy1)) -> @@ -232,10 +236,8 @@ and equate_con tp con0 con1 = let* out1 = lift_cmp @@ do_sub_out con1 in equate_con tp out0 out1 | D.ElStable code, _, _ -> - let* out0 = lift_cmp @@ do_el_out con0 in - let* out1 = lift_cmp @@ do_el_out con1 in let* tp = lift_cmp @@ unfold_el code in - equate_con tp out0 out1 + equate_con tp con0 con1 | _, D.Zero, D.Zero -> ret () | _, D.Suc con0, D.Suc con1 -> @@ -260,7 +262,7 @@ and equate_con tp con0 con1 = Splice.con bdy @@ fun bdy -> Splice.term @@ TB.lam @@ fun i -> TB.lam @@ fun prf -> - TB.el_in @@ TB.ap bdy [i; prf] + TB.ap bdy [i; prf] in let* bdy0' = fix_body bdy0 in let* bdy1' = fix_body bdy1 in @@ -271,7 +273,7 @@ and equate_con tp con0 con1 = Splice.con bdy @@ fun bdy -> Splice.term @@ TB.lam @@ fun i -> TB.lam @@ fun prf -> - TB.el_in @@ TB.ap bdy [i; prf] + TB.ap bdy [i; prf] in let* bdy0' = fix_body bdy0 in let* bdy1' = fix_body bdy1 in @@ -401,8 +403,6 @@ and equate_frm k0 k1 = TB.el @@ TB.ap mot [TB.loop x] in equate_con loop_tp loop_case0 loop_case1 - | D.KElOut, D.KElOut -> - ret () | _ -> conv_err @@ ExpectedFrmEq (k0, k1) diff --git a/src/core/Domain.ml b/src/core/Domain.ml index afa64b698..ca4dc1b68 100644 --- a/src/core/Domain.ml +++ b/src/core/Domain.ml @@ -33,8 +33,6 @@ struct let snd = Lam (`Anon, Clo (S.Snd (S.Var 0), {tpenv = Emp; conenv = Emp})) let proj lbl = Lam (`Anon, Clo (S.Proj (S.Var 0, lbl), {tpenv = Emp; conenv = Emp})) - let el_out = Lam (`Anon, Clo (S.ElOut (S.Var 0), {tpenv = Emp; conenv = Emp})) - let tm_abort = Split [] let tp_abort = TpSplit [] @@ -106,7 +104,6 @@ struct | KProj lbl -> Format.fprintf fmt "proj[%a]" Ident.pp_user lbl | KNatElim _ -> Format.fprintf fmt "" | KCircleElim _ -> Format.fprintf fmt "" - | KElOut -> Uuseg_string.pp_utf_8 fmt "⭝ₑₗ" and pp_cof : cof Pp.printer = fun fmt cof -> @@ -174,8 +171,6 @@ struct Format.fprintf fmt "dim0" | Dim1 -> Format.fprintf fmt "dim1" - | ElIn con -> - Format.fprintf fmt "el/in[%a]" pp_con con | StableCode `Nat -> Format.fprintf fmt "nat/code" | StableCode `Circle -> diff --git a/src/core/Domain.mli b/src/core/Domain.mli index ea53d28e0..e0a781ba8 100644 --- a/src/core/Domain.mli +++ b/src/core/Domain.mli @@ -23,7 +23,6 @@ module Make : functor (Symbol : Symbol.S) -> sig val fst : con val snd : con val proj : Ident.user -> con - val el_out : con val tm_abort : con val tp_abort : tp diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml index b028bdf41..cd9965646 100644 --- a/src/core/DomainData.ml +++ b/src/core/DomainData.ml @@ -70,10 +70,7 @@ struct | Pair of con * con | Struct of (Ident.user * con) list | SubIn of con - - | ElIn of con - (** The introduction form for the extension of a {i stable} type code only (see {!constructor:ElStable} and {!constructor:ElUnstable}). *) - + | Dim0 | Dim1 | DimProbe of DimProbe.t @@ -139,10 +136,6 @@ struct | KNatElim of con * con * con | KCircleElim of con * con * con - | KElOut - (** The elimination form for the extension of a {i stable} type code only (see {!constructor:ElStable}). *) - - (** An {i unstable} frame is a {i dimension substitution-unstable} elimination form with a hole in place of its principal argument. *) and unstable_frm = | KHCom of dim * dim * cof * con diff --git a/src/core/Quote.ml b/src/core/Quote.ml index 0902c7c92..531360af5 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -115,12 +115,8 @@ let rec quote_con (tp : D.tp) con = S.SubIn tout | D.ElStable code, _ -> - let+ tout = - let* unfolded = lift_cmp @@ unfold_el code in - let* out = lift_cmp @@ do_el_out con in - quote_con unfolded out - in - S.ElIn tout + let* unfolded = lift_cmp @@ unfold_el code in + quote_con unfolded con | _, D.Zero -> ret S.Zero @@ -160,10 +156,9 @@ let rec quote_con (tp : D.tp) con = Splice.con bdy @@ fun bdy -> Splice.term @@ TB.lam @@ fun i -> TB.lam @@ fun prf -> - TB.el_in @@ TB.ap bdy [i; prf] + TB.ap bdy [i; prf] in - let+ tm = quote_hcom (D.StableCode `Nat) r s phi bdy' in - S.ElOut tm + quote_hcom (D.StableCode `Nat) r s phi bdy' | _univ, D.UnstableCode (`V (r, pcode, code, pequiv)) -> let+ tr, t_pcode, tcode, t_pequiv = quote_v_data r pcode code pequiv in @@ -176,10 +171,9 @@ let rec quote_con (tp : D.tp) con = Splice.con bdy @@ fun bdy -> Splice.term @@ TB.lam @@ fun i -> TB.lam @@ fun prf -> - TB.el_in @@ TB.ap bdy [i; prf] + TB.ap bdy [i; prf] in - let+ tm = quote_hcom (D.StableCode `Univ) r s phi bdy' in - S.ElOut tm + quote_hcom (D.StableCode `Univ) r s phi bdy' | D.Circle, D.FHCom (`Circle, r, s, phi, bdy) -> let* bdy' = @@ -187,10 +181,9 @@ let rec quote_con (tp : D.tp) con = Splice.con bdy @@ fun bdy -> Splice.term @@ TB.lam @@ fun i -> TB.lam @@ fun prf -> - TB.el_in @@ TB.ap bdy [i; prf] + TB.ap bdy [i; prf] in - let+ tm = quote_hcom (D.StableCode `Circle) r s phi bdy' in - S.ElOut tm + quote_hcom (D.StableCode `Circle) r s phi bdy' | D.ElUnstable (`HCom (r,s,phi,bdy)), _ -> let+ tr = quote_dim r @@ -650,5 +643,3 @@ and quote_frm tm = | D.KAp (tp, con) -> let+ targ = quote_con tp con in S.Ap (tm, targ) - | D.KElOut -> - ret @@ S.ElOut tm diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 6dc3070e3..6b83c5eef 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -653,7 +653,7 @@ struct 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) + (ext_code, TB.sub_out) | None -> let+ code = RM.lift_cmp @@ @@ -697,7 +697,7 @@ struct 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] + Splice.term @@ TB.lams (sign_names :> Ident.t list) @@ fun args -> TB.ap tm [TB.struct_ @@ List.combine sign_names args] in let+ qfib = RM.quote_con fib_tp fib in S.CodeSignature (qsign @ [`User ["fib"], qfib]) @@ -745,7 +745,7 @@ struct TB.ap bdry [TB.prf] in let+ ttm = RM.lift_qu @@ Qu.quote_con tp tm in - S.ElIn (S.SubIn ttm) + S.SubIn ttm | tp -> RM.expected_connective `ElExt tp let code_v (tac_dim : T.Chk.tac) (tac_pcode: T.Chk.tac) (tac_code : T.Chk.tac) (tac_pequiv : T.Chk.tac) : T.Chk.tac = @@ -936,14 +936,14 @@ struct let intro tac = T.Chk.brule ~name:"El.intro" @@ fun (tp, phi, clo) -> let* unfolded = dest_el tp in - let+ tm = T.Chk.brun tac (unfolded, phi, D.un_lam @@ D.compose D.el_out @@ D.Lam (`Anon, clo)) in - S.ElIn tm + T.Chk.brun tac (unfolded, phi, D.un_lam @@ D.Lam (`Anon, clo)) let elim tac = T.Syn.rule ~name:"El.elim" @@ let* tm, tp = T.Syn.run tac in let+ unfolded = dest_el tp in - S.ElOut tm, unfolded + tm, unfolded + end @@ -1214,7 +1214,7 @@ struct let assert_nat = function - | D.Nat -> RM.ret () + | D.Nat | D.ElStable `Nat -> RM.ret () | tp -> RM.expected_connective `Nat tp let rec int_to_term = @@ -1282,7 +1282,7 @@ struct let assert_circle = function - | D.Circle -> RM.ret () + | D.Circle | D.ElStable `Circle -> RM.ret () | tp -> RM.expected_connective `Circle tp let base = diff --git a/src/core/Semantics.ml b/src/core/Semantics.ml index af59fbc6f..45809bf7d 100644 --- a/src/core/Semantics.ml +++ b/src/core/Semantics.ml @@ -122,9 +122,6 @@ and push_subst_con : D.dim -> DimProbe.t -> D.con -> D.con CM.m = | D.StableCode code -> let+ code = subst_stable_code r x code in D.StableCode code - | D.ElIn con -> - let+ con = subst_con r x con in - D.ElIn con | D.SubIn con -> let+ con = subst_con r x con in D.SubIn con @@ -375,7 +372,7 @@ and subst_frm : D.dim -> DimProbe.t -> D.frm -> D.frm CM.m = fun r x -> let open CM in function - | D.KFst | D.KSnd | D.KElOut | D.KProj _ as frm -> ret frm + | D.KFst | D.KSnd | D.KProj _ as frm -> ret frm | D.KAp (tp, arg) -> let+ tp = subst_tp r x tp and+ arg = subst_con r x arg in @@ -564,12 +561,6 @@ and eval : S.t -> D.con EvM.m = | S.SubIn tm -> let+ con = eval tm in D.SubIn con - | S.ElOut tm -> - let* con = eval tm in - lift_cmp @@ do_el_out con - | S.ElIn tm -> - let+ con = eval tm in - D.ElIn con | S.Dim0 -> ret D.Dim0 | S.Dim1 -> ret D.Dim1 | S.Cof cof_f -> @@ -726,7 +717,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.Pair _ | D.Struct _ | D.SubIn _ | D.ElIn _ | D.LockedPrfIn _ + | D.Lam _ | D.BindSym _ | D.Zero | D.Suc _ | D.Base | D.Pair _ | D.Struct _ | D.SubIn _ | D.LockedPrfIn _ | D.Cof _ | D.Dim0 | D.Dim1 | D.Prf | D.StableCode _ | D.DimProbe _ -> ret `Done | D.LetSym (r, x, con) -> @@ -941,11 +932,10 @@ and do_nat_elim (mot : D.con) zero (suc : D.con) : D.con -> D.con CM.m = let fam = TB.lam @@ fun i -> let fhcom = - TB.el_out @@ TB.hcom TB.code_nat r i phi @@ TB.lam @@ fun j -> TB.lam @@ fun prf -> - TB.el_in @@ TB.ap bdy [j; prf] + TB.ap bdy [j; prf] in TB.ap mot [fhcom] in @@ -997,11 +987,10 @@ and do_circle_elim (mot : D.con) base (loop : D.con) c : D.con CM.m = let fam = TB.lam @@ fun i -> let fhcom = - TB.el_out @@ TB.hcom TB.code_circle r i phi @@ TB.lam @@ fun j -> TB.lam @@ fun prf -> - TB.el_in @@ TB.ap bdy [j; prf] + TB.ap bdy [j; prf] in TB.ap mot [fhcom] in @@ -1079,6 +1068,9 @@ and do_fst con : D.con CM.m = splitter con @@ List.map fst branches | D.Cut {tp = D.Sg (base, _, _); cut} -> ret @@ cut_frm ~tp:base ~cut D.KFst + | D.Cut {tp = D.ElStable (`Sg _ as code) ; cut} -> + let* tp = unfold_el code in + do_fst (D.Cut {tp ; cut}) | _ -> throw @@ NbeFailed "Couldn't fst argument in do_fst" end @@ -1100,6 +1092,9 @@ and do_snd con : D.con CM.m = let* fst = do_fst con in let+ fib = inst_tp_clo fam fst in cut_frm ~tp:fib ~cut D.KSnd + | D.Cut {tp = D.ElStable (`Sg _ as code) ; cut} -> + let* tp = unfold_el code in + do_snd (D.Cut {tp ; cut}) | _ -> throw @@ NbeFailed ("Couldn't snd argument in do_snd") end @@ -1135,6 +1130,9 @@ and do_proj (con : D.con) (lbl : Ident.user) : D.con CM.m = splitter con @@ List.map fst branches | D.Cut {tp = D.Signature sign; cut} -> cut_frm_sign cut sign lbl + | D.Cut {tp = D.ElStable (`Signature _ as code); cut} -> + let* tp = unfold_el code in + do_proj (D.Cut {tp ; cut}) lbl | _ -> throw @@ NbeFailed ("Couldn't proj argument in do_proj") end @@ -1176,7 +1174,9 @@ and do_ap con arg = | D.Cut {tp = D.Pi (base, _, fam); cut} -> let+ fib = inst_tp_clo fam arg in cut_frm ~tp:fib ~cut @@ D.KAp (base, arg) - + | D.Cut {tp = D.ElStable ((`Pi _ | `Ext _) as code); cut} -> + let* tp = unfold_el code in + do_ap (D.Cut {tp ; cut}) arg | D.Cut {tp = D.TpSplit branches; _} as con -> splitter con @@ List.map fst branches @@ -1202,6 +1202,9 @@ and do_sub_out con = ret con | D.Cut {tp = D.Sub (tp, phi, clo); cut} -> ret @@ D.Cut {tp; cut = D.UnstableCut (cut, D.KSubOut (phi, clo)), []} + | D.Cut {tp = D.ElStable (`Ext (0,_,_,_) as code) ; cut} -> + let* tp = unfold_el code in + do_sub_out (D.Cut {tp ; cut}) | D.Split branches as con -> splitter con @@ List.map fst branches | D.Cut {tp = D.TpSplit branches; _} as con -> @@ -1294,34 +1297,6 @@ and do_rigid_vproj r pcode code pequiv v = throw @@ NbeFailed "do_rigid_vproj" end -and do_el_out con = - let open CM in - abort_if_inconsistent (ret D.tm_abort) @@ - let splitter con phis = - splice_tm @@ - Splice.con con @@ fun tm -> - Splice.cons (List.map D.cof_to_con phis) @@ fun phis -> - Splice.term @@ - TB.cof_split @@ List.map (fun phi -> phi, TB.el_out tm) phis - in - begin - inspect_con ~style:`UnfoldNone con |>> - function - | D.ElIn con -> - ret con - | D.Split branches as con -> - splitter con @@ List.map fst branches - | D.Cut {tp = D.TpSplit branches; _} as con -> - splitter con @@ List.map fst branches - | D.Cut {tp = D.ElStable code; cut} -> - let+ tp = unfold_el code in - cut_frm ~tp ~cut D.KElOut - | _ -> - Format.eprintf "bad el/out: %a@." D.pp_con con; - throw @@ NbeFailed "do_el_out" - end - - and do_el : D.con -> D.tp CM.m = let open CM in fun con -> @@ -1342,7 +1317,7 @@ and do_el : D.con -> D.tp CM.m = splitter con @@ List.map fst branches | D.Cut {tp = D.TpSplit branches; _} as con -> splitter con @@ List.map fst branches - | D.Cut {cut; tp = D.Univ} -> + | D.Cut {cut; tp = D.Univ | D.ElStable `Univ} -> ret @@ D.ElCut cut | D.StableCode code -> ret @@ D.ElStable code @@ -1586,18 +1561,18 @@ and enact_rigid_hcom code r r' phi bdy tag = Splice.con bdy @@ fun bdy -> Splice.term @@ TB.lam @@ fun i -> TB.lam @@ fun prf -> - TB.el_out @@ TB.ap bdy [i; prf] + TB.ap bdy [i; prf] in - D.ElIn (D.FHCom (tag, r, r', phi, bdy')) + D.FHCom (tag, r, r', phi, bdy') | `Univ -> let+ bdy' = splice_tm @@ Splice.con bdy @@ fun bdy -> Splice.term @@ TB.lam @@ fun i -> TB.lam @@ fun prf -> - TB.el_out @@ TB.ap bdy [i; prf] + TB.ap bdy [i; prf] in - D.ElIn (D.UnstableCode (`HCom (r, r', phi, bdy'))) + D.UnstableCode (`HCom (r, r', phi, bdy')) end | `Unstable code -> begin @@ -1698,7 +1673,6 @@ 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.KElOut -> do_el_out con and do_spine con = let open CM in diff --git a/src/core/Semantics.mli b/src/core/Semantics.mli index 23a719ab3..9901925de 100644 --- a/src/core/Semantics.mli +++ b/src/core/Semantics.mli @@ -31,7 +31,6 @@ val do_fst : D.con -> D.con compute val do_snd : D.con -> D.con compute val do_proj : D.con -> Ident.user -> D.con compute val do_sub_out : D.con -> D.con compute -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 diff --git a/src/core/Serialize.ml b/src/core/Serialize.ml index 1c6c3b0ea..5cc3cdcd3 100644 --- a/src/core/Serialize.ml +++ b/src/core/Serialize.ml @@ -137,8 +137,6 @@ struct | S.ForallCof cof -> labeled "forall" [json_of_tm cof] | S.CofSplit branches -> labeled "split" @@ List.map (fun (tphi, tm) -> json_of_pair (json_of_tm tphi) (json_of_tm tm)) branches | S.Prf -> `String "prf" - | S.ElIn tm -> labeled "el_in" [json_of_tm tm] - | S.ElOut tm -> labeled "el_out" [json_of_tm tm] | S.Box (r, s, phi, sides, cap) -> labeled "box" [json_of_tm r; json_of_tm s; json_of_tm phi; json_of_tm sides; json_of_tm cap] | S.Cap (r, s, phi, code, box) -> labeled "cap" [json_of_tm r; json_of_tm s; json_of_tm phi; json_of_tm code; json_of_tm box] | S.VIn (r, pequiv, pivot, base) -> labeled "v_in" [json_of_tm r; json_of_tm pequiv; json_of_tm pivot; json_of_tm base] @@ -285,12 +283,6 @@ struct let branches = List.map (json_to_pair json_to_tm json_to_tm) j_branches in S.CofSplit branches | `String "prf" -> S.Prf - | `A [`String "el_in"; j_tm] -> - let tm = json_to_tm j_tm in - S.ElIn tm - | `A [`String "el_out"; j_tm] -> - let tm = json_to_tm j_tm in - S.ElOut tm | `A [`String "box"; j_r; j_s; j_phi; j_sides; j_cap] -> let r = json_to_tm j_r in let s = json_to_tm j_s in @@ -445,7 +437,6 @@ struct | Pair (con0, con1) -> labeled "pair" [json_of_con con0; json_of_con con1] | Struct fields -> labeled "struct" [json_of_labeled json_of_con fields] | SubIn con -> labeled "sub_in" [json_of_con con] - | ElIn con -> labeled "el_in" [json_of_con con] | Dim0 -> `String "dim0" | Dim1 -> `String "dim1" | DimProbe dim_probe -> labeled "dim_probe" [DimProbe.serialize dim_probe] @@ -522,7 +513,6 @@ struct | D.KProj lbl -> labeled "k_proj" [json_of_user lbl] | D.KNatElim (mot, z, s) -> labeled "k_nat_elim" [json_of_con mot; json_of_con z; json_of_con s] | D.KCircleElim (mot, b, l) -> labeled "k_circle_elim" [json_of_con mot; json_of_con b; json_of_con l] - | D.KElOut -> `String "k_el_out" and json_of_unstable_frm : D.unstable_frm -> J.value = function @@ -568,7 +558,6 @@ struct | `A [`String "pair"; j_con0; j_con1] -> Pair (json_to_con j_con0, json_to_con j_con1) | `A [`String "struct"; j_fields] -> Struct (json_to_labeled json_to_con j_fields) | `A [`String "sub_in"; j_con] -> SubIn (json_to_con j_con) - | `A [`String "el_in"; j_con] -> ElIn (json_to_con j_con) | `String "dim0" -> Dim0 | `String "dim1" -> Dim1 | `A [`String "dim_probe"; j_dim_probe] -> DimProbe (DimProbe.deserialize j_dim_probe) @@ -656,7 +645,6 @@ struct | `A [`String "k_proj"; j_lbl] -> KProj (json_to_user j_lbl) | `A [`String "k_nat_elim"; j_mot; j_z; j_s] -> KNatElim (json_to_con j_mot, json_to_con j_z, json_to_con j_s) | `A [`String "k_circle_elim"; j_mot; j_b; j_l] -> KCircleElim (json_to_con j_mot, json_to_con j_b, json_to_con j_l) - | `String "k-el_out" -> KElOut | j -> J.parse_error j "Domain.json_to_frm" and json_to_unstable_frm : J.value -> D.unstable_frm = diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index bac4d0fe7..0b84f9a2f 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -58,9 +58,6 @@ struct | CofSplit branches -> Format.fprintf fmt "cof/split[%a]" (Pp.pp_sep_list dump_branch) branches | Prf -> Format.fprintf fmt "prf" - | ElIn tm -> Format.fprintf fmt "el/in[%a]" dump tm - | ElOut tm -> Format.fprintf fmt "el/out[%a]" dump tm - | Box _ -> Format.fprintf fmt "" | Cap _ -> Format.fprintf fmt "" @@ -160,7 +157,7 @@ struct | NatElim _ | Loop _ | CircleElim _ -> juxtaposition - | SubIn _ | SubOut _ | ElIn _ | ElOut _ -> passed + | SubIn _ | SubOut _ -> passed | CodePi _ -> arrow | CodeSg _ -> times | CodeSignature _ -> juxtaposition @@ -330,11 +327,7 @@ struct Format.fprintf fmt "sub/in %a" (pp_atomic env) tm | SubOut tm when Debug.is_debug_mode () -> Format.fprintf fmt "sub/out %a" (pp_atomic env) tm - | ElIn tm when Debug.is_debug_mode () -> - Format.fprintf fmt "el/in %a" (pp_atomic env) tm - | ElOut tm when Debug.is_debug_mode () -> - Format.fprintf fmt "el/out %a" (pp_atomic env) tm - | SubIn tm | SubOut tm | ElIn tm | ElOut tm -> + | SubIn tm | SubOut tm -> pp env penv fmt tm | CodePi (base, fam) when Debug.is_debug_mode () -> @@ -566,7 +559,7 @@ struct Format.fprintf fmt "%a %a" Uuseg_string.pp_utf_8 x (pp_lambdas envx) tm - | (SubIn tm | SubOut tm | ElIn tm | ElOut tm) when not @@ Debug.is_debug_mode () -> + | (SubIn tm | SubOut tm) when not @@ Debug.is_debug_mode () -> pp_lambdas env fmt tm | _ -> Format.fprintf fmt "=>@ @[%a@]" diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml index 05485796e..66af9b834 100644 --- a/src/core/SyntaxData.ml +++ b/src/core/SyntaxData.ml @@ -42,9 +42,6 @@ struct | CofSplit of (t * t) list | Prf - | ElIn of t - | ElOut of t - | Box of t * t * t * t * t | Cap of t * t * t * t * t diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml index ba3f1f824..94ba2353d 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -64,10 +64,6 @@ module MU = Monad.Util (M) type 'a b = S.t m -> 'a m -let el_in m : _ m = - let+ tm = m in - S.ElIn tm - let tp_locked_prf mphi : _ m = let+ phi = mphi in S.TpLockedPrf phi @@ -83,11 +79,6 @@ let locked_prf_unlock mtp ~cof ~prf ~bdy = and+ bdy = bdy in S.LockedPrfUnlock {tp; cof; prf; bdy} - -let el_out m : _ m = - let+ tm = m in - S.ElOut tm - let lam ?(ident = `Anon) mbdy : _ m = scope @@ fun var -> let+ bdy = mbdy var in @@ -424,22 +415,22 @@ struct let code_equiv code_a code_b = code_sg (code_pi code_a @@ lam @@ fun _ -> code_b) @@ lam @@ fun f -> code_pi code_b @@ lam @@ fun y -> - code_is_contr @@ code_fiber code_a code_b (el_out f) y + code_is_contr @@ code_fiber code_a code_b f y let equiv_fwd equiv = - el_out @@ fst @@ el_out equiv + fst equiv (* CJHM CCHM names *) let equiv_fiber_contr equiv y = - ap (el_out @@ snd @@ el_out equiv) [y] + ap (snd equiv) [y] (* CJHM CCHM names *) let equiv_inv equiv y = - fst @@ el_out @@ equiv_fiber_contr equiv y + fst @@ equiv_fiber_contr equiv y (* CJHM CCHM names *) let equiv_inv_path equiv y p = - ap (el_out @@ snd @@ el_out @@ equiv_fiber_contr equiv y) [p] + ap (snd @@ equiv_fiber_contr equiv y) [p] end module Kan = @@ -448,29 +439,26 @@ struct type hcom = r:S.t m -> r':S.t m -> phi:S.t m -> bdy:S.t m -> S.t m let coe_pi ~base_line ~fam_line ~r ~r' ~bdy : _ m = - el_in @@ lam @@ fun arg -> let_ (lam @@ fun i -> coe base_line r' i arg) @@ fun coe_base_line -> let fib_line = lam @@ fun i -> ap fam_line [i; ap coe_base_line [i]] in coe fib_line r r' @@ - ap (el_out bdy) [ap coe_base_line [r]] + ap bdy [ap coe_base_line [r]] let hcom_pi ~fam ~r ~r' ~phi ~bdy : _ m = - el_in @@ lam @@ fun arg -> let tfib = ap fam [arg] in hcom tfib r r' phi @@ lam @@ fun i -> lam @@ fun prf -> - ap (el_out (ap bdy [i; prf])) [arg] + ap (ap bdy [i; prf]) [arg] let coe_sg ~base_line ~fam_line ~r ~r' ~bdy : _ m = - let fst_line = lam @@ fun i -> coe base_line r i @@ fst @@ el_out bdy in + let fst_line = lam @@ fun i -> coe base_line r i @@ fst @@ bdy in let fib_line = lam @@ fun i -> ap fam_line [i; ap fst_line [i]] in - el_in @@ pair (ap fst_line [r']) - (coe fib_line r r' @@ snd @@ el_out bdy) + (coe fib_line r r' @@ snd @@ bdy) let hcom_sg ~base ~fam ~r ~r' ~phi ~bdy : _ m = let p0_line = @@ -478,7 +466,7 @@ struct hcom base r i phi @@ lam @@ fun j -> lam @@ fun prf -> - fst @@ el_out @@ ap bdy [j; prf] + fst @@ ap bdy [j; prf] in let p0 = ap p0_line [r'] in let fib_line = @@ -489,19 +477,18 @@ struct com fib_line r r' phi @@ lam @@ fun i -> lam @@ fun prf -> - snd @@ el_out @@ ap bdy [i; prf] + snd @@ ap bdy [i; prf] in - el_in @@ pair p0 p1 let coe_sign ~field_lines ~r ~r' ~bdy : _ m = let mk_line bound_lines (lbl, fam_line) = let fib_line = lam @@ fun i -> ap fam_line (i :: List.map (fun (_, line) -> ap line [i]) bound_lines) in - let line = lam @@ fun i -> coe fib_line r i @@ proj (el_out bdy) lbl in + let line = lam @@ fun i -> coe fib_line r i @@ proj bdy lbl in bound_lines @ [(lbl, line)] in let field_coe_lines = List.fold_left mk_line [] field_lines in - el_in @@ struct_ @@ List.map (fun (lbl, fam_line) -> lbl, ap fam_line [r']) field_coe_lines + struct_ @@ List.map (fun (lbl, fam_line) -> lbl, ap fam_line [r']) field_coe_lines let hcom_sign ~fields ~r ~r' ~phi ~bdy : _ m = let mk_line bound_lines (lbl, fam) = @@ -528,10 +515,9 @@ struct proj (ap bdy [j; prf]) lbl in List.fold_left mk_line [(lbl, p0_line)] fields in - el_in @@ struct_ @@ List.map (fun (lbl, p_line) -> lbl, ap p_line [r']) lines + struct_ @@ List.map (fun (lbl, p_line) -> lbl, ap p_line [r']) lines let coe_ext ~n ~cof ~fam_line ~bdry_line ~r ~r' ~bdy = - el_in @@ nlam n @@ fun js -> sub_in @@ let_ (ap cof js) @@ fun cof_js -> @@ -540,10 +526,9 @@ struct lam @@ fun _ -> cof_split [cof_js, ap bdry_line @@ i :: js @ [prf] - ; eq i r, sub_out @@ ap (el_out bdy) js] + ; eq i r, sub_out @@ ap bdy js] let hcom_ext ~n ~cof ~fam ~bdry ~r ~r' ~phi ~bdy = - el_in @@ nlam n @@ fun js -> sub_in @@ let_ (ap cof js) @@ fun cof_js -> @@ -553,7 +538,7 @@ struct lam @@ fun _p -> cof_split [ cof_js, ap bdry @@ js @ [prf] - ; join [phi; eq k r], sub_out @@ ap (el_out (ap bdy [k; prf])) js + ; join [phi; eq k r], sub_out @@ ap (ap bdy [k; prf]) js ] module V : @@ -618,19 +603,19 @@ struct (coe (lam code_) r i (ap f_tilde [r; prf; bdy])) in lam @@ fun _ -> - coe line r r' @@ el_in @@ lam @@ fun _ -> sub_in @@ ap f_tilde [r; prf; bdy] + coe line r r' @@ lam @@ fun _ -> sub_in @@ ap f_tilde [r; prf; bdy] end @@ fun r_tilde -> let_ ~ident:(`Machine "S") begin lam @@ fun _ -> Equiv.equiv_inv_path (ap (pequiv_ r') [prf]) o_tilde @@ (* "q_tilde" *) - el_in @@ cof_split + cof_split [forall (fun i -> eq (s_ i) dim0), pair (coe (lam @@ fun j -> ap (pcode_ j) [prf]) r r' bdy) (ap r_tilde [prf]); eq r r', pair bdy - (el_in @@ lam @@ fun _ -> sub_in @@ vproj (s_ r) (pcode_ r) (code_ r) (pequiv_ r) bdy)] + (lam @@ fun _ -> sub_in @@ vproj (s_ r) (pcode_ r) (code_ r) (pequiv_ r) bdy)] end @@ fun s_tilde -> let_ ~ident:(`Machine "T") @@ -641,7 +626,7 @@ struct lam @@ fun _ -> cof_split [eq j dim0, Equiv.equiv_inv (ap (pequiv_ r') [prf]) o_tilde; (* "p_tilde" *) - join [forall (fun i -> eq (s_ i) dim0); eq r r'], sub_out @@ ap (el_out @@ ap s_tilde [prf]) [j]] + join [forall (fun i -> eq (s_ i) dim0); eq r r'], sub_out @@ ap (ap s_tilde [prf]) [j]] end @@ fun t_tilde -> let_ ~ident:(`Machine "U") @@ -651,10 +636,10 @@ struct lam @@ fun _ -> cof_split [join [eq k dim1; eq r r'], o_tilde; - eq (s_ r') dim0, sub_out @@ ap (el_out @@ snd @@ el_out @@ ap t_tilde [prf]) [k]] + eq (s_ r') dim0, sub_out @@ ap (snd @@ ap t_tilde [prf]) [k]] end @@ fun u_tilde -> - vin (s_ r') (pequiv_ r') (lam @@ fun _ -> fst @@ el_out @@ ap t_tilde [prf]) u_tilde + vin (s_ r') (pequiv_ r') (lam @@ fun _ -> fst @@ ap t_tilde [prf]) u_tilde end module FHCom : diff --git a/src/core/TermBuilder.mli b/src/core/TermBuilder.mli index b2f0e557e..c706ae8ae 100644 --- a/src/core/TermBuilder.mli +++ b/src/core/TermBuilder.mli @@ -50,9 +50,6 @@ val tm_abort : t m val sub_out : t m -> t m val sub_in : t m -> t m -val el_in : t m -> t m -val el_out : t m -> t m - val univ : tp m val nat : tp m val code_nat : t m diff --git a/src/frontend/Tactics.ml b/src/frontend/Tactics.ml index c93a1e50a..c56f720ad 100644 --- a/src/frontend/Tactics.ml +++ b/src/frontend/Tactics.ml @@ -166,7 +166,7 @@ struct let* tscrut, ind_tp = T.Syn.run scrut in let scrut = T.Syn.rule @@ RM.ret (tscrut, ind_tp) (* only makes sense because because I know 'scrut' won't be used under some binder *) in match ind_tp, mot with - | D.Nat, mot -> + | (D.Nat | D.ElStable `Nat) , mot -> let* tac_zero : T.Chk.tac = match find_case ["zero"] cases with | Some ([], tac) -> RM.ret tac @@ -183,7 +183,7 @@ struct | None -> RM.ret @@ R.Hole.unleash_hole @@ Some "suc" in T.Syn.run @@ R.Nat.elim mot tac_zero tac_suc scrut - | D.Circle, mot -> + | (D.Circle | D.ElStable `Circle), mot -> let* tac_base : T.Chk.tac = match find_case ["base"] cases with | Some ([], tac) -> RM.ret tac @@ -221,7 +221,7 @@ struct let mot_tac : T.Chk.tac = R.Pi.intro @@ fun var -> (* of inductive type *) T.Chk.brule @@ fun _goal -> - let* fib = RM.lift_cmp @@ Sem.inst_tp_clo fam @@ D.ElIn (T.Var.con var) in + let* fib = RM.lift_cmp @@ Sem.inst_tp_clo fam @@ T.Var.con var in let* tfib = RM.quote_tp fib in match tfib with | S.El code -> @@ -233,7 +233,7 @@ struct R.Pi.intro @@ fun x -> T.Chk.syn @@ elim mot_tac cases @@ - R.El.elim @@ T.Var.syn x + T.Var.syn x | _ -> RM.expected_connective `Pi tp end @@ -289,15 +289,14 @@ struct Splice.con p @@ fun p -> Splice.con q @@ fun q -> Splice.term @@ - TB.el_in @@ TB.lam @@ fun i -> TB.sub_in @@ TB.hcom code TB.dim0 TB.dim1 (TB.boundary i) @@ TB.lam @@ fun j -> TB.lam @@ fun _ -> TB.cof_split [ - TB.join [TB.eq j TB.dim0; TB.eq i TB.dim0], TB.sub_out @@ TB.ap (TB.el_out p) [i]; - TB.eq i TB.dim1, TB.sub_out @@ TB.ap (TB.el_out q) [j] + TB.join [TB.eq j TB.dim0; TB.eq i TB.dim0], TB.sub_out @@ TB.ap p [i]; + TB.eq i TB.dim1, TB.sub_out @@ TB.ap q [j] ] in let+ tpath = RM.quote_con path_tp path in @@ -321,7 +320,6 @@ struct Sem.splice_tm @@ Splice.con x @@ fun x -> Splice.term @@ - TB.el_in @@ TB.lam @@ fun _ -> TB.sub_in @@ x in let+ trefl = RM.quote_con refl_tp refl in From 89ce557eaa4b91a80aae86a4ba3af347b95668db Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Sat, 30 Apr 2022 14:22:47 -0400 Subject: [PATCH 2/3] delete uncessary ConvM --- src/core/Conversion.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml index 33a41914a..53147ce73 100644 --- a/src/core/Conversion.ml +++ b/src/core/Conversion.ml @@ -107,10 +107,10 @@ let rec equate_tp (tp0 : D.tp) (tp1 : D.tp) = | D.Univ, D.Univ -> ret () | D.ElStable code0, _ -> - let* tp0 = ConvM.lift_cmp @@ Sem.unfold_el code0 in + let* tp0 = lift_cmp @@ Sem.unfold_el code0 in equate_tp tp0 tp1 | _, D.ElStable code1 -> - let* tp1 = ConvM.lift_cmp @@ Sem.unfold_el code1 in + let* tp1 = lift_cmp @@ Sem.unfold_el code1 in equate_tp tp0 tp1 | D.ElCut cut0, D.ElCut cut1 -> equate_cut cut0 cut1 From 1f0377bfb14ff084855cc2d62e18703bd83212e2 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Sat, 30 Apr 2022 14:43:44 -0400 Subject: [PATCH 3/3] remove hack from intro_conversions --- src/frontend/Tactics.ml | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) diff --git a/src/frontend/Tactics.ml b/src/frontend/Tactics.ml index c56f720ad..bea40ea20 100644 --- a/src/frontend/Tactics.ml +++ b/src/frontend/Tactics.ml @@ -115,14 +115,8 @@ let rec intro_subtypes_and_total : T.Chk.tac -> T.Chk.tac = RM.ret tac let intro_conversions (tac : T.Syn.tac) : T.Chk.tac = - (* HACK: Because we are using Weak Tarski Universes, we can't just - use the conversion checker to equate 'tp` and 'univ', as - 'tp' 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. *) T.Chk.rule ~name:"intro_conversions" @@ function - | D.Univ | D.ElStable `Univ as tp -> + | D.Univ as tp -> let* tm, tp' = T.Syn.run tac in let* vtm = RM.lift_ev @@ Sem.eval tm in begin @@ -130,12 +124,10 @@ let intro_conversions (tac : T.Syn.tac) : T.Chk.tac = | D.Pi (D.ElStable (`Signature vsign) as base, ident, clo) -> let* tac' = T.abstract ~ident base @@ fun var -> let* fam = RM.lift_cmp @@ Sem.inst_tp_clo clo (T.Var.con var) in - let* fam = RM.lift_cmp @@ Sem.whnf_tp_ ~style:`UnfoldAll fam in - (* Same HACK *) - match fam with - | D.Univ - | D.ElStable `Univ -> RM.ret @@ R.Univ.total vsign vtm - | _ -> RM.ret @@ T.Chk.syn tac + let* conv = RM.trap @@ RM.lift_conv_ @@ Conversion.equate_tp fam D.Univ in + match conv with + | Ok () -> RM.ret @@ R.Univ.total vsign vtm + | Error _ -> RM.ret @@ T.Chk.syn tac in T.Chk.run tac' tp | _ -> T.Chk.run (T.Chk.syn tac) tp