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

@@ -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

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

library/paths/equivalence.red

@@ -17,20 +17,20 @@ 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
         ]
       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

src/core/Tm.ml

@@ -800,9 +800,9 @@ let rec pp env fmt =
       begin
         match sys with
         | [] ->
-          Format.fprintf fmt "@[<hv1>(# <%a>@ %a)@]" pp_strings xs (pp env') cod
+          Format.fprintf fmt "@[<hov1>(# <%a>@ %a)@]" pp_strings xs (pp env') cod
         | _ ->
-          Format.fprintf fmt "@[<hv1>(# @[<hv1><%a>@ %a@ @[<hv>%a@]@])@]" pp_strings xs (pp env') cod (pp_sys env') sys
+          Format.fprintf fmt "@[<hov1>(# <%a>@ %a@ @[<hv>%a@])@]" pp_strings xs (pp env') cod (pp_sys env') sys
       end
 
     | Restrict face ->

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;

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

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

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);

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 "<hole>"
   | Hope ->
     Format.fprintf fmt "<hope>"
-  | Lam _ ->
-    Format.fprintf fmt "<lam>"
+  | Guess _ ->
+    Format.fprintf fmt "<guess>"
+
   | Var {name; _} ->
     Format.fprintf fmt "%s" name
-  | _ ->
-    Format.fprintf fmt "<eterm>"
+  | Num _ ->
+    Format.fprintf fmt "<num>"
+
+  | Pi _ ->
+    Format.fprintf fmt "<pi>"
+  | Sg _ ->
+    Format.fprintf fmt "<sg>"
+  | Ext _ ->
+    Format.fprintf fmt "<ext>"
+
+  | Lam _ ->
+    Format.fprintf fmt "<lam>"
+  | Tuple _ ->
+    Format.fprintf fmt "<tuple>"
+
+  | Coe _ ->
+    Format.fprintf fmt "<coe>"
+  | HCom _ ->
+    Format.fprintf fmt "<hcom>"
+  | Com _ ->
+    Format.fprintf fmt "<com>"
+
+  | Type _ ->
+    Format.fprintf fmt "<type>"
+
+  | Box {cap; sys} ->
+    Format.fprintf fmt "@[box@ %a@ [%a]@]" pp cap.con (ListUtil.pp "|" pp_eterm) sys
+
+  | V _ ->
+    Format.fprintf fmt "<V>"
+
+  | Elim _ ->
+    Format.fprintf fmt "<elim>"
+  | ElimFun _ ->
+    Format.fprintf fmt "<elim-fun>"
+
+  | Let _ ->
+    Format.fprintf fmt "<let>"
+  | Cut (hd, stk) ->
+    Format.fprintf fmt "@[<hov1>(cut@ %a@ %a)@]" pp_eterm hd (ListUtil.pp " " pp_frame) stk
+
+  | Refl ->
+    Format.fprintf fmt "refl"
+  | Quo _ ->
+    Format.fprintf fmt "<quo>"
+  | RunML _ ->
+    Format.fprintf fmt "<run-ml>"
+
+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

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