From c95d1a0787fb92eb011df690b4bdc1029a611c0b Mon Sep 17 00:00:00 2001 From: favonia Date: Tue, 20 Nov 2018 18:21:29 -0600 Subject: [PATCH] Box and cap tactics (#467) * Add the box and cap tactics. * Fill in ML.pp more. * Fix other files in the library. * Tweaks to the pretty printing of the extension types. * Fix a very ??? bug. --- emacs/redtt.el | 2 +- library/basics/hedberg.red | 6 +-- library/paths/equivalence.red | 6 +-- src/core/Tm.ml | 4 +- src/core/Typing.ml | 2 +- src/frontend/Elaborator.ml | 47 +++++++++++++++++++++++ src/frontend/Grammar.mly | 7 +++- src/frontend/Lex.mll | 2 + src/frontend/ML.ml | 70 ++++++++++++++++++++++++++++++++--- vim/syntax/redtt.vim | 2 +- 10 files changed, 131 insertions(+), 17 deletions(-) diff --git a/emacs/redtt.el b/emacs/redtt.el index 63da98c79..8f04ec892 100644 --- a/emacs/redtt.el +++ b/emacs/redtt.el @@ -100,7 +100,7 @@ (defconst redtt-expression-keywords - '("V" "in" "with" "where" "begin" "end" "let" "dim" "elim" "fst" "snd" "coe" "com" "pair" "comp" "fun" "hcom" "vproj" "vin" "lam" "refl" "pre" "kan" "type") + '("V" "in" "with" "where" "begin" "end" "let" "dim" "elim" "fst" "snd" "coe" "com" "pair" "comp" "fun" "hcom" "vproj" "vin" "cap" "box" "lam" "refl" "pre" "kan" "type") "Expression keywords.") (defconst redtt-expression-symbols diff --git a/library/basics/hedberg.red b/library/basics/hedberg.red index 9b1613b58..232f34ea1 100644 --- a/library/basics/hedberg.red +++ b/library/basics/hedberg.red @@ -30,8 +30,8 @@ def paths-stableβ†’set (A : type) (st : (x y : A) β†’ stable (path A x y)) : is- | m=1 β†’ q ] in - let cap (k m : 𝕀) = st (p k) (q k) (Ξ» c β†’ c (square k)) m in - comp 0 1 (cap j i) [ + let mycap (k m : 𝕀) = st (p k) (q k) (Ξ» c β†’ c (square k)) m in + comp 0 1 (mycap j i) [ | i=0 k β†’ st (p j) (p j) (neg/is-prop-over (Ξ» j β†’ neg (path A (p j) (p j))) @@ -40,7 +40,7 @@ def paths-stableβ†’set (A : type) (st : (x y : A) β†’ stable (path A x y)) : is- j) k | i=1 β†’ refl - | βˆ‚[j] k β†’ weak-connection/or A (cap j) i k + | βˆ‚[j] k β†’ weak-connection/or A (mycap j) i k ] -- Hedberg's theorem for decidable path types diff --git a/library/paths/equivalence.red b/library/paths/equivalence.red index 83bd1ff24..b246f55dd 100644 --- a/library/paths/equivalence.red +++ b/library/paths/equivalence.red @@ -17,7 +17,7 @@ def is-equiv/prop/direct (A B : type) (f : A β†’ B) : is-prop (is-equiv _ _ f) = ( c' (a , p) i , Ξ» w β†’ - let cap (j k : 𝕀) : fiber A B f y = + let mycap (j k : 𝕀) : fiber A B f y = comp 1 j (c' w k) [ | k=0 β†’ refl | k=1 β†’ c' w @@ -25,12 +25,12 @@ def is-equiv/prop/direct (A B : type) (f : A β†’ B) : is-prop (is-equiv _ _ f) = in let face/i0 (j k : 𝕀) : fiber A B f y = comp 0 j w [ - | k=0 β†’ cap 0 + | k=0 β†’ mycap 0 | k=1 β†’ c w ] in Ξ» j β†’ - comp 0 1 (cap i j) [ + comp 0 1 (mycap i j) [ | i=0 β†’ face/i0 j | i=1 | j=0 β†’ refl | j=1 k β†’ c' (face/i0 1 k) i diff --git a/src/core/Tm.ml b/src/core/Tm.ml index b78b02a6d..309aa1d85 100644 --- a/src/core/Tm.ml +++ b/src/core/Tm.ml @@ -800,9 +800,9 @@ let rec pp env fmt = begin match sys with | [] -> - Format.fprintf fmt "@[(# <%a>@ %a)@]" pp_strings xs (pp env') cod + Format.fprintf fmt "@[(# <%a>@ %a)@]" pp_strings xs (pp env') cod | _ -> - Format.fprintf fmt "@[(# @[<%a>@ %a@ @[%a@]@])@]" pp_strings xs (pp env') cod (pp_sys env') sys + Format.fprintf fmt "@[(# <%a>@ %a@ @[%a@])@]" pp_strings xs (pp env') cod (pp_sys env') sys end | Restrict face -> diff --git a/src/core/Typing.ml b/src/core/Typing.ml index 82a9c53f8..f8787716e 100644 --- a/src/core/Typing.ml +++ b/src/core/Typing.ml @@ -753,7 +753,7 @@ and infer_spine_ cx hd sp = | T.Cap info -> let fhcom_ty = check_eval_ty cx @@ - T.make @@ T.FHCom {r = info.r; r' = info.r; cap = info.ty; sys = info.sys} + T.make @@ T.FHCom {r = info.r; r' = info.r'; cap = info.ty; sys = info.sys} in let ih = infer_spine_ cx hd sp in Cx.check_eq_ty cx fhcom_ty ih.ty; diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml index e7a8e4640..f9f5e8bc4 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -69,6 +69,8 @@ struct M.ret `Snd | E.VProj -> M.ret `VProj + | E.Cap -> + M.ret `Cap | E.Open -> M.ret `Open @@ -519,6 +521,14 @@ struct let tac1 = elab_chk @@ {e with con = Tuple es} in R.tac_pair tac0 tac1 goal + | [], Tm.FHCom fhcom, Box box -> + elab_box_sys fhcom.r fhcom.r' fhcom.sys box.sys >>= fun (sys, coe_sys) -> + elab_chk box.cap {ty = fhcom.cap; sys = coe_sys} >>= fun cap -> + M.ret @@ Tm.make @@ Tm.Box {r = fhcom.r; r' = fhcom.r'; cap; sys} + + | _, Tm.FHCom fhcom, Box box -> + failwith "box tactic under constraints not implemented yet." + | [], Tm.Univ info, Type (kind, lvl) -> begin if Lvl.greater info.lvl lvl then @@ -690,6 +700,28 @@ struct in go Emp + and elab_box_sys s s' systy (bdrys : E.eterm list) = + let rec go acc coe_acc = + function + | [], [] -> + M.ret @@ (Bwd.to_list acc, Bwd.to_list coe_acc) + + | ((r, r', ty_bnd) :: systy), (bdry :: bdrys) -> + let tys' = Tm.unbind_with (Tm.DownX s', []) ty_bnd in + begin + M.under_restriction r r' begin + elab_chk bdry {ty = tys'; sys = Bwd.to_list acc} + end + end >>= fun obdry -> + let bdry = Option.default Tm.forty_two obdry in + let face = r, r', bdry in + let coe_face = r, r', Tm.up (Tm.Coe {r = s'; r' = s; ty = ty_bnd; tm = bdry}, []) in + go (acc #< face) (coe_acc #< coe_face) (systy, bdrys) + + | _ -> invalid_arg "elab_box_sys" + + in go Emp Emp (systy, bdrys) + and elab_up ty inf = elab_inf inf >>= fun (ty', cmd) -> C.check ~ty @@ Tm.up cmd >>= function @@ -809,6 +841,8 @@ struct M.ret (spine, `Snd) | `VProj -> M.ret (spine, `VProj) + | `Cap -> + M.ret (spine, `Cap) | `Open -> M.ret (spine, `Open) @@ -1057,6 +1091,19 @@ struct raise R.ChkMatch end + | spine, `Cap -> + elab_cut_bwd exp spine >>= fun (ty, cmd) -> + try_nf ty @@ fun ty -> + begin + match unleash ty with + (* FIXME this does not check rigidity because we do not know how to do it + * correctly anyways *) + | Tm.FHCom {r; r'; cap; sys} -> + M.ret (cap, cmd @< Tm.Cap {r; r'; ty = cap; sys}) + | _ -> + raise R.ChkMatch + end + | _ -> failwith "elab_cut" end diff --git a/src/frontend/Grammar.mly b/src/frontend/Grammar.mly index 5a7908ca7..0ee41c14c 100644 --- a/src/frontend/Grammar.mly +++ b/src/frontend/Grammar.mly @@ -42,7 +42,7 @@ %token RIGHT_ARROW RIGHT_TACK %token TIMES AST HASH AT BACKTICK IN WITH WHERE BEGIN END DATA INTRO %token DIM -%token ELIM UNIV LAM PAIR FST SND COMP HCOM COM COE LET FUN V VPROJ VIN REFL +%token ELIM UNIV LAM PAIR FST SND COMP HCOM COM COE LET FUN V VPROJ VIN CAP BOX REFL %token PUBLIC PRIVATE OPAQUE QUIT DEBUG NORMALIZE DEF PRINT CHECK %token TYPE PRE KAN %token META @@ -84,6 +84,8 @@ eproj: { E.Snd } | DOT VPROJ { E.VProj } + | DOT CAP + { E.Cap } atom_econ: | a = ATOM @@ -180,6 +182,9 @@ spine_con: | V; x = ATOM; ty0 = located(atomic); ty1 = located(atomic); equiv = located(atomic) { E.V {x; ty0; ty1; equiv} } + | BOX; cap = located(atomic); sys = pipe_block(located(econ)) + { E.Box {cap; sys}} + %inline block(X): | WITH; x = X; END diff --git a/src/frontend/Lex.mll b/src/frontend/Lex.mll index 5b9d76118..3a60e5da0 100644 --- a/src/frontend/Lex.mll +++ b/src/frontend/Lex.mll @@ -37,6 +37,8 @@ let keywords = ("βˆ‚", BOUNDARY); ("vproj", VPROJ); ("vin", VIN); + ("cap", CAP); + ("box", BOX); ("let", LET); ("fun", FUN); ("def", DEF); diff --git a/src/frontend/ML.ml b/src/frontend/ML.ml index 0bb6f6f7c..1f4d0ed98 100644 --- a/src/frontend/ML.ml +++ b/src/frontend/ML.ml @@ -117,6 +117,8 @@ and econ = | V of {x : string; ty0 : eterm; ty1 : eterm; equiv : eterm} + | Box of {cap : eterm; sys : eterm list} + | Cut of eterm * frame list | Refl @@ -156,6 +158,7 @@ and frame = | Fst | Snd | VProj + | Cap | Open module Env : @@ -196,18 +199,75 @@ struct end (* Please fill this in. I'm just using it for debugging. *) -let pp fmt = +let rec pp fmt = function | Hole _ -> Format.fprintf fmt "" | Hope -> Format.fprintf fmt "" - | Lam _ -> - Format.fprintf fmt "" + | Guess _ -> + Format.fprintf fmt "" + | Var {name; _} -> Format.fprintf fmt "%s" name - | _ -> - Format.fprintf fmt "" + | Num _ -> + Format.fprintf fmt "" + + | Pi _ -> + Format.fprintf fmt "" + | Sg _ -> + Format.fprintf fmt "" + | Ext _ -> + Format.fprintf fmt "" + + | Lam _ -> + Format.fprintf fmt "" + | Tuple _ -> + Format.fprintf fmt "" + + | Coe _ -> + Format.fprintf fmt "" + | HCom _ -> + Format.fprintf fmt "" + | Com _ -> + Format.fprintf fmt "" + + | Type _ -> + Format.fprintf fmt "" + + | Box {cap; sys} -> + Format.fprintf fmt "@[box@ %a@ [%a]@]" pp cap.con (ListUtil.pp "|" pp_eterm) sys + + | V _ -> + Format.fprintf fmt "" + + | Elim _ -> + Format.fprintf fmt "" + | ElimFun _ -> + Format.fprintf fmt "" + + | Let _ -> + Format.fprintf fmt "" + | Cut (hd, stk) -> + Format.fprintf fmt "@[(cut@ %a@ %a)@]" pp_eterm hd (ListUtil.pp " " pp_frame) stk + + | Refl -> + Format.fprintf fmt "refl" + | Quo _ -> + Format.fprintf fmt "" + | RunML _ -> + Format.fprintf fmt "" + +and pp_eterm fmt {con; _} = pp fmt con + +and pp_frame fmt = + function + | App e -> pp_eterm fmt e + | Fst -> Format.fprintf fmt "fst" + | Snd -> Format.fprintf fmt "snd" + | VProj -> Format.fprintf fmt "vproj" + | Cap -> Format.fprintf fmt "cap" + | Open -> Format.fprintf fmt "open" let pp_edecl fmt = function diff --git a/vim/syntax/redtt.vim b/vim/syntax/redtt.vim index 8b9200890..01e665e7c 100644 --- a/vim/syntax/redtt.vim +++ b/vim/syntax/redtt.vim @@ -31,7 +31,7 @@ syn region redttImport matchgroup=redttDecl start="import" end="$\|\(/-\|--\)\@ syn match redttHole '?\k*' syn keyword redttKeyw V in with where begin end dim elim fst snd coe com pair -syn keyword redttKeyw fun hcom comp vproj vin lam refl pre +syn keyword redttKeyw fun hcom comp vproj vin cap box lam refl pre syn keyword redttKeyw kan U type syn keyword redttDecl meta def do let data debug print normalize public private quit opaque