Rectification Campaign II: Restrictions, etc.

Makefile

@@ -22,6 +22,7 @@ examples:
 	${DUNE} exec -- redtt load-file nat.red
 	${DUNE} exec -- redtt load-file int.red
 	${DUNE} exec -- redtt load-file bool.red
+	${DUNE} exec -- redtt load-file bad.red
 	${DUNE} exec -- redtt load-file omega1s1-wip.red
 	${DUNE} exec -- redtt load-file torus.red
 	${DUNE} exec -- redtt load-file modal.red

README.md

@@ -31,7 +31,7 @@ and [cubicaltt](https://github.com/mortberg/cubicaltt).
   supported)  based on the [work of Evan Cavallo and Bob
   Harper](https://arxiv.org/abs/1801.01568)
 
-- experimental support for Fitch-style modal guarded recursion: □, ▷
+- experimental support for Fitch-style modal guarded recursion: ▷
 
 
 Features we intend to add in the near future:

bad.red

@@ -0,0 +1,74 @@
+import path
+
+; Here are some tricky examples that Evan Cavallo came up with to expose bugs.
+
+data O where
+| obase
+| oloop (y : O) @ i
+  [ i=0 ⇒ y
+  | i=1 ⇒ y
+  ]
+
+let thing0 (A : type) (B : (dim → A) → type) (p : dim → A) (b : B p) : B p =
+  let ty : dim → type = λ k →
+    let h : dim → A = λ l →
+      comp 0 l (p 0) [
+      | k=0 ⇒ λ z → p z
+      | k=1 ⇒ λ z → p z
+      ]
+    in
+    B (λ l → h l)
+  in
+  (coe 0 1 b in ty)
+
+let thing1 (A : type) (a : A) : Path A a a =
+  let bar =
+  thing0 A
+    (λ q → Path A (q 0) (q 1))
+    (λ _ → a)
+    (λ _ → a)
+
+  in
+  λ i -> bar i
+
+
+
+let thing (A : type) (a,b : A) (p : Path A a b) : Path (Path A a b) p p =
+  λ i j →
+  let ty : dim → type = λ k →
+    let h : dim → A = λ l →
+      comp 0 l a [
+      | k=0 ⇒ λ z → p z
+      | k=1 ⇒ λ z → p z
+      ]
+    in
+    Path (Path A (h 0) (h 1)) (λ l → h l) (λ l → h l)
+  in
+  (coe 0 1 (λ _ z → p z) in ty) i j
+
+let experiment3 (A : type) (B : A -> type) (u : (a : A) -> B a) : Path ((a : A) -> B a) u u =
+  lam i ->
+    comp 0 1 u [
+    | i=0 => lam j -> u
+    | i=1 => lam j -> u
+    ]
+
+
+
+let experiment (A : type) (u : A)
+  : (p : Path A u u) -> (q : Path (Path A u u) p p) -> Path (Path A u u) p p
+  =
+  lam p q i ->
+    comp 0 1 (lam k -> p k) [
+    | i=0 => lam j k -> q j k
+    | i=1 => lam j k -> p k
+    ]
+
+; TODO: doesn't work yet, need elaborator support
+
+;let experiment (A : type) (u : A) : Path A u u =
+;  lam i ->
+;    comp 0 1 ?cap [
+;    | i=0 => lam j -> ?left
+;    | i=1 => lam j -> ?right
+;    ]

modal.red

@@ -30,57 +30,3 @@ let stream/tl (xs : stream) : ✓ → stream =
 let tts : _ =
   fix xs : stream in
     stream/cons tt xs
-
-
-; To eliminate a box, write 'b !'; this elaborates to the core term `(open b).
-let bool/constant (x : bool) : (b : □ bool) × Path _ x (b !) =
-  elim x [
-  | tt ⇒ < shut tt, λ _ → tt >
-  | ff ⇒ < shut ff, λ _ → ff >
-  ]
-
-let sequence : type = □ stream
-
-
-let Next (A : type) (x : A) ✓ : A =
-  x
-
-let sequence/cons (x : bool) (xs : sequence) : sequence =
-  shut
-    stream/cons
-      (bool/constant x .0 !)
-      (Next stream (xs !))
-      ; this is suspicious: we use this Next in order to essentially
-      ; weaken away the tick that we will not use, in order to get the right number
-      ; of locks deleted. But this is proof-theoretically very strange.
-
-; The proper solution to the problem above is to bind lock names in the syntax and in the context,
-; analogous to tick names. This will make the calculus more baroque, but it will enable a
-; deterministic version of the 'open' rule. The source term for the above would then be:
-;
-;     λ α → stream/cons (bool/constant x .0 α) (λ β → xs α)
-;
-; Above, α is a lock name and β is a tick name; opening with the lock α
-; would *delete* the tick β from the context (thinking backward), which is
-; a tick weakening. the example would typecheck because there is no need for
-; β in xs.
-;
-; For reference, the core-language term would look like the following:
-;
-;    (shut [α]
-;     (stream/cons
-;      (open α (car (bool/constant x)))
-;      (next [β] (open α xs))))
-
-
-
-let sequence/hd (xs : sequence) : bool =
-  stream/hd (xs !)
-
-let sequence/tl (xs : sequence) : sequence =
-  shut
-    stream/tl (xs !) ∙
-
-
-let law/k (A,B : type) (f : □ (A → B)) (x : □ A) : □ B =
-  shut f ! (x !)

src/basis/Monad.ml

@@ -56,4 +56,13 @@ struct
       m >>= fun x ->
       traverse f ms >>= fun xs ->
       M.ret @@ x :: xs
+
+  let rec fold_left f acc xs =
+    match xs with
+    | [] ->
+      M.ret acc
+    | x :: xs ->
+      f acc x >>= fun a ->
+      fold_left f a xs
+
 end

src/basis/Monad.mli

@@ -23,5 +23,6 @@ module Notation (M : S) : Notation with type 'a m := 'a M.m
 module Util (M : S) :
 sig
   val traverse : ('a -> 'b) -> 'a M.m list -> 'a list M.m
+  val fold_left : ('a -> 'b -> 'a M.m) -> 'a -> 'b list -> 'a M.m
 end
 

src/core/Cx.ml

@@ -23,8 +23,7 @@ type cx =
    env : Domain.env;
    qenv : Quote.env;
    ppenv : Pp.env;
-   rel : Restriction.t;
-   all_locks : int}
+   rel : Restriction.t}
 
 type t = cx
 
@@ -39,31 +38,7 @@ let clear_locals cx =
    qenv = Quote.Env.emp;
    hyps = [];
    ppenv = Pp.Env.emp;
-   env = Domain.Env.clear_locals cx.env;
-   all_locks = 0}
-let ext_lock cx =
-  {cx with
-   sign = GlobalEnv.ext_lock cx.sign;
-   hyps = List.map (fun hyp -> {hyp with locked = true}) cx.hyps;
-   all_locks = cx.all_locks + 1}
-
-let hyps_clear_locks hyps =
-  let rec go hyps =
-    match hyps with
-    | [] -> []
-    | hyp :: hyps ->
-      match hyp.classifier with
-      | `Tick -> hyp :: hyps (* Maybe not quite right *)
-      | _ ->
-        {hyp with locked = false} :: go hyps
-  in
-  go hyps
-
-let clear_locks cx =
-  {cx with
-   sign = GlobalEnv.clear_locks cx.sign;
-   hyps = hyps_clear_locks cx.hyps;
-   all_locks = 0}
+   env = Domain.Env.clear_locals cx.env}
 
 let kill_from_tick cx tgen =
   match tgen with
@@ -144,7 +119,6 @@ let lookup i {hyps; _} =
     hyp.classifier
 
 let lookup_constant nm tw cx =
-  (* For constants, the only locks that are relevant are the global ones. Ignore the local locks. *)
   GlobalEnv.lookup_ty cx.sign nm tw
 
 let restrict cx r r' =
@@ -228,5 +202,4 @@ let init globals =
    qenv = Quote.Env.emp;
    hyps = [];
    ppenv = Pp.Env.emp;
-   rel = GlobalEnv.restriction globals;
-   all_locks = 0}
+   rel = GlobalEnv.restriction globals}

src/core/Cx.mli

@@ -10,10 +10,7 @@ val qenv : t -> Quote.env
 
 val clear_locals : t -> t
 
-(* Modal left adjoints *)
-val ext_lock : t -> t
-val clear_locks : t -> t
-
+(* Modal *)
 val kill_from_tick : t -> Domain.tick_gen -> t
 
 val ext_ty : t -> nm:string option -> value -> t * value

src/core/Domain.ml

@@ -93,10 +93,6 @@ and pp_con fmt : con -> unit =
     Format.fprintf fmt "<dfix>"
   | DFixLine _ ->
     Format.fprintf fmt "<dfix-line>"
-  | BoxModality _ ->
-    Format.fprintf fmt "<box-modality>"
-  | Shut _ ->
-    Format.fprintf fmt "<shut>"
   | Data lbl ->
     Uuseg_string.pp_utf_8 fmt lbl
   | Intro info ->
@@ -236,9 +232,6 @@ and pp_neu fmt neu =
   | FixLine _ ->
     Format.fprintf fmt "<fix-line>"
 
-  | Open _ ->
-    Format.fprintf fmt "<open>"
-
 and pp_elim_clauses fmt clauses =
   let pp_sep fmt () = Format.fprintf fmt "@ " in
   Format.pp_print_list ~pp_sep pp_elim_clause fmt clauses

src/core/DomainData.ml

@@ -8,7 +8,6 @@ type tick_gen =
   [`Lvl of string option * int | `Global of Name.t ]
 
 type tick =
-  | TickConst
   | TickGen of tick_gen
 
 
@@ -44,9 +43,6 @@ type con =
   | DFix of {ty : value; clo : clo}
   | DFixLine of {x : atom; ty : value; clo : clo}
 
-  | BoxModality of value
-  | Shut of value
-
   | Data of Desc.data_label
   | Intro of
       {dlbl : Desc.data_label;
@@ -87,8 +83,6 @@ and neu =
   | Fix of tick_gen * value * clo
   | FixLine of atom * tick_gen * value * clo
 
-  | Open of neu
-
 and nf = {ty : value; el : value}
 
 and abs = value IAbs.abs

src/core/GlobalEnv.ml

@@ -16,7 +16,6 @@ type t =
   {rel : Restriction.t;
    data_decls : (Tm.tm, Tm.tm Desc.Boundary.term) Desc.desc StringTable.t;
    table : (entry param * lock_info) T.t;
-   lock : int -> bool;
    killed : int -> bool;
    under_tick : int -> bool;
    len : int}
@@ -26,7 +25,6 @@ let emp () =
   {table = T.empty;
    data_decls = StringTable.empty;
    rel = Restriction.emp ();
-   lock = (fun _ -> false);
    killed = (fun _ -> false);
    under_tick = (fun _ -> false);
    len = 0}
@@ -73,15 +71,6 @@ let ext_dim (sg : t) nm : t =
   ext_ sg ~constant:false nm `I
 
 
-let ext_lock (sg : t) : t =
-  {sg with
-   lock = fun i -> if i < sg.len then true else sg.lock i}
-
-let clear_locks (sg : t) : t =
-  {sg with
-   lock = (fun i -> if sg.under_tick i then sg.lock i else false)}
-
-
 let rec index_of pred xs =
   match xs with
   | [] -> failwith "index_of"
@@ -97,9 +86,8 @@ let kill_from_tick (sg : t) nm : t =
 
 let lookup_entry sg nm tw =
   let prm, linfo = T.find nm sg.table in
-  let locked = sg.lock linfo.birth in
   let killed = sg.killed linfo.birth in
-  if not linfo.constant && (locked || killed) then
+  if not linfo.constant && killed then
     failwith "GlobalEnv.lookup_entry: not accessible (modal!!)"
   else
     match prm, tw with
@@ -142,7 +130,7 @@ let pp fmt sg =
     | `Tw _ ->
       Format.fprintf fmt "%a[twin]"
         Name.pp nm
-    | (`Tick | `I | `P _) ->
+    | (`Tick | `I | `P _ | `Def _) ->
       Format.fprintf fmt "%a"
         Name.pp nm
   in

src/core/GlobalEnv.mli

@@ -15,9 +15,7 @@ val ext : t -> Name.t -> entry param -> t
 val ext_meta : t -> Name.t -> entry param -> t
 val ext_dim : t -> Name.t -> t
 val ext_tick : t -> Name.t -> t
-val ext_lock : t -> t
 val restrict : Tm.tm -> Tm.tm -> t -> t
-val clear_locks : t -> t
 val kill_from_tick : t -> Name.t -> t
 
 

src/core/Kind.mli

@@ -0,0 +1,4 @@
+type t = [`Reg | `Kan | `Pre]
+
+val lte : t -> t -> bool
+val pp : t Pp.t0

src/core/Lvl.mli

@@ -0,0 +1,6 @@
+type t = [`Omega | `Const of int]
+
+val greater : t -> t -> bool
+val lte : t -> t -> bool
+val shift : int -> t -> t
+val pp : t Pp.t0