[Stopped using continuation-passing style in the proof of the bar theorem.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080717200813] hunk ./CompilerCorrectness/BarTheorem.agda 34
--- Some abbreviations, used by the bar theorem below.
+-- Some abbreviations, used in the proof of the bar theorem.
hunk ./CompilerCorrectness/BarTheorem.agda 36
-Cont : Pred State -> Pred State -> Set
-Cont P Q = forall {y} -> y ∈ P -> y ◁∞ Q
+_∋◁∞_ : Pred State -> Pred State -> Set
+P ∋◁∞ Q = forall {y} -> y ∈ P -> y ◁∞ Q
hunk ./CompilerCorrectness/BarTheorem.agda 39
-Cont⟶ : State -> Pred State -> Set
-Cont⟶ x = Cont (_⟶_ x)
+_⟶◁∞_ : State -> Pred State -> Set
+_⟶◁∞_ x = _∋◁∞_ (_⟶_ x)
hunk ./CompilerCorrectness/BarTheorem.agda 42
--- The bar theorem, written in continuation-passing style.
-
--- TODO: Convince the productivity checker that this definition is
--- productive.
+-- The bar theorem.
hunk ./CompilerCorrectness/BarTheorem.agda 44
-bar-thm : forall {t} (e : Expr t) {ops i s P} ->
-          Cont (Matches⁺ ops s e i) P ->
-          ⟨ comp e ops , i , s ⟩ ◁∞ P
+bar-theorem : forall {t} (e : Expr t) {ops i s} ->
+              ⟨ comp e ops , i , s ⟩ ◁∞ Matches⁺ ops s e i
hunk ./CompilerCorrectness/BarTheorem.agda 47
-bar-thm {t = t} ⌜ nat n ⌝ κ ~ via (, push) (helper₁ κ)
+bar-theorem {t = t} ⌜ nat n ⌝ ~ via (, push) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 49
-  helper₁ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s {t} ⌜ nat n ⌝ i) P ->
-            Cont⟶ ⟨ push n ∷ ops , i , s ⟩ P
-  helper₁ κ push      ~ κ (returns Val)
-  helper₁ κ interrupt ~ κ (throws Int)
+  helper₁ : forall {ops i s} ->
+            ⟨ push n ∷ ops , i , s ⟩ ⟶◁∞ Matches⁺ ops s {t} ⌜ nat n ⌝ i
+  helper₁ push      ~ directly (returns Val)
+  helper₁ interrupt ~ directly (throws Int)
hunk ./CompilerCorrectness/BarTheorem.agda 54
-bar-thm {t = t} ⌜ throw ⌝ κ ~ via (, throw) (helper₁ κ)
+bar-theorem {t = t} ⌜ throw ⌝ ~ via (, throw) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 56
-  helper₁ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s {t} ⌜ throw ⌝ i) P ->
-            Cont⟶ ⟨ throw ∷ ops , i , s ⟩ P
-  helper₁ κ throw     ~ κ (throws Val)
-  helper₁ κ interrupt ~ κ (throws Int)
+  helper₁ : forall {ops i s} ->
+            ⟨ throw ∷ ops , i , s ⟩ ⟶◁∞ Matches⁺ ops s {t} ⌜ throw ⌝ i
+  helper₁ throw     ~ directly (throws Val)
+  helper₁ interrupt ~ directly (throws Int)
hunk ./CompilerCorrectness/BarTheorem.agda 61
-bar-thm (x ⊕ y) κ ~ bar-thm x (helper₁ κ)
+bar-theorem (x ⊕ y) ~ ◁∞-trans (bar-theorem x) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 63
-  helper₆ : forall {ops m s P} ->
-            Cont (Matches⁺ ops s (x ⊕ y) U) P ->
-            Cont⟶ ⟪ U , nat m ∷ s ⟫ P
-  helper₆ κ nat ~ κ (throws Int)
+  helper₆ : forall {ops m s} ->
+            ⟪ U , nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x ⊕ y) U
+  helper₆ nat ~ directly (throws Int)
hunk ./CompilerCorrectness/BarTheorem.agda 67
-  helper₅ : forall {ops m n s P} ->
-            Cont (Matches⁺ ops s (x ⊕ y) U) P ->
-            Cont⟶ ⟪ U , nat n ∷ nat m ∷ s ⟫ P
-  helper₅ κ nat ~ via (, nat) (helper₆ κ)
+  helper₅ : forall {ops m n s} ->
+            ⟪ U , nat n ∷ nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x ⊕ y) U
+  helper₅ nat ~ via (, nat) helper₆
hunk ./CompilerCorrectness/BarTheorem.agda 71
-  helper₄ : forall {ops i m s P} ->
-            Cont (Matches⁺ ops s (x ⊕ y) i) P ->
+  helper₄ : forall {ops i m s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 73
-            Cont⟶ ⟪ i , nat m ∷ s ⟫ P
-  helper₄ κ x↡ y↯ nat ~ κ (throws (Add₃ x↡ y↯))
+            ⟪ i , nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x ⊕ y) i
+  helper₄ x↡ y↯ nat ~ directly (throws (Add₃ x↡ y↯))
hunk ./CompilerCorrectness/BarTheorem.agda 76
-  helper₃ : forall {ops i n m s P} ->
-            Cont (Matches⁺ ops s (x ⊕ y) i) P ->
+  helper₃ : forall {ops i n m s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 78
-            Cont⟶ ⟨ add ∷ ops , i , nat n ∷ nat m ∷ s ⟩ P
-  helper₃ κ x↡ y↡ add       ~ κ (returns (Add₁ x↡ y↡))
-  helper₃ κ _  _  interrupt ~ via (, nat) (helper₅ κ)
+            ⟨ add ∷ ops , i , nat n ∷ nat m ∷ s ⟩ ⟶◁∞
+            Matches⁺ ops s (x ⊕ y) i
+  helper₃ x↡ y↡ add       ~ directly (returns (Add₁ x↡ y↡))
+  helper₃ _  _  interrupt ~ via (, nat) helper₅
hunk ./CompilerCorrectness/BarTheorem.agda 83
-  helper₂ : forall {ops i m s P} ->
-            Cont (Matches⁺ ops s (x ⊕ y) i) P ->
+  helper₂ : forall {ops i m s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 85
-            Cont (Matches⁺ (add ∷ ops) (nat m ∷ s) y i) P
-  helper₂ κ x↡ (returns y↡) ~ via (, add) (helper₃ κ x↡ y↡)
-  helper₂ κ x↡ (throws y↯)  ~ via (, nat) (helper₄ κ x↡ y↯)
+            Matches⁺ (add ∷ ops) (nat m ∷ s) y i ∋◁∞
+            Matches⁺ ops s (x ⊕ y) i
+  helper₂ x↡ (returns y↡) ~ via (, add) (helper₃ x↡ y↡)
+  helper₂ x↡ (throws y↯)  ~ via (, nat) (helper₄ x↡ y↯)
hunk ./CompilerCorrectness/BarTheorem.agda 90
-  helper₁ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (x ⊕ y) i) P ->
-            Cont (Matches⁺ (comp y (add ∷ ops)) s x i) P
-  helper₁ κ (throws  x↯) ~ κ (throws (Add₂ x↯))
-  helper₁ κ (returns x↡) ~ bar-thm y (helper₂ κ x↡)
+  helper₁ : forall {ops i s} ->
+            Matches⁺ (comp y (add ∷ ops)) s x i ∋◁∞
+            Matches⁺ ops s (x ⊕ y) i
+  helper₁ (throws  x↯) ~ directly (throws (Add₂ x↯))
+  helper₁ (returns x↡) ~ ◁∞-trans (bar-theorem y) (helper₂ x↡)
hunk ./CompilerCorrectness/BarTheorem.agda 96
-bar-thm (x >> y) κ ~ bar-thm x (helper₁ κ)
+bar-theorem (x >> y) ~ ◁∞-trans (bar-theorem x) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 98
-  helper₄ : forall {ops m s P} ->
-            Cont (Matches⁺ ops s (x >> y) U) P ->
-            Cont⟶ ⟪ U , nat m ∷ s ⟫ P
-  helper₄ κ nat ~ κ (throws Int)
+  helper₄ : forall {ops m s} ->
+            ⟪ U , nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x >> y) U
+  helper₄ nat ~ directly (throws Int)
hunk ./CompilerCorrectness/BarTheorem.agda 102
-  helper₃ : forall {ops i m s P} ->
-            Cont (Matches⁺ ops s (x >> y) i) P ->
+  helper₃ : forall {ops i m s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 104
-            Cont (Matches⁺ ops s y i) P
-  helper₃ κ x↡ (returns y↡) ~ κ (returns (Seqn₁ x↡ y↡))
-  helper₃ κ x↡ (throws  y↯) ~ κ (throws  (Seqn₁ x↡ y↯))
+            Matches⁺ ops s y i ∋◁∞ Matches⁺ ops s (x >> y) i
+  helper₃ x↡ (returns y↡) ~ directly (returns (Seqn₁ x↡ y↡))
+  helper₃ x↡ (throws  y↯) ~ directly (throws  (Seqn₁ x↡ y↯))
hunk ./CompilerCorrectness/BarTheorem.agda 108
-  helper₂ : forall {ops i m s P} ->
-            Cont (Matches⁺ ops s (x >> y) i) P ->
+  helper₂ : forall {ops i m s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 110
-            Cont⟶ ⟨ pop ∷ comp y ops , i , nat m ∷ s ⟩ P
-  helper₂ κ x↡ pop       ~ bar-thm y (helper₃ κ x↡)
-  helper₂ κ _  interrupt ~ via (, nat) (helper₄ κ)
+            ⟨ pop ∷ comp y ops , i , nat m ∷ s ⟩ ⟶◁∞
+            Matches⁺ ops s (x >> y) i
+  helper₂ x↡ pop       ~ ◁∞-trans (bar-theorem y) (helper₃ x↡)
+  helper₂ _  interrupt ~ via (, nat) helper₄
hunk ./CompilerCorrectness/BarTheorem.agda 115
-  helper₁ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (x >> y) i) P ->
-            Cont (Matches⁺ (pop ∷ comp y ops) s x i) P
-  helper₁ κ (throws  x↯) ~ κ (throws (Seqn₂ x↯))
-  helper₁ κ (returns x↡) ~ via (, pop) (helper₂ κ x↡)
+  helper₁ : forall {ops i s} ->
+            Matches⁺ (pop ∷ comp y ops) s x i ∋◁∞
+            Matches⁺ ops s (x >> y) i
+  helper₁ (throws  x↯) ~ directly (throws (Seqn₂ x↯))
+  helper₁ (returns x↡) ~ via (, pop) (helper₂ x↡)
hunk ./CompilerCorrectness/BarTheorem.agda 121
-bar-thm (x catch y) κ ~ via (, mark) (helper₁ κ)
+bar-theorem (x catch y) ~ via (, mark) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 123
-  helper₉ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (x catch y) i) P ->
+  helper₉ : forall {ops i s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 125
-            Cont⟶ ⟪ B , int i ∷ s ⟫ P
-  helper₉ κ x↯ y↯ int ~ κ (throws (Catch₂ x↯ y↯))
+            ⟪ B , int i ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x catch y) i
+  helper₉ x↯ y↯ int ~ directly (throws (Catch₂ x↯ y↯))
hunk ./CompilerCorrectness/BarTheorem.agda 128
-  helper₈ : forall {ops i n s P} ->
-            Cont (Matches⁺ ops s (x catch y) i) P ->
+  helper₈ : forall {ops i n s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 130
-            Cont⟶ ⟨ reset ∷ ops , B , nat n ∷ int i ∷ s ⟩ P
-  helper₈ κ x↯ y↡ reset ~ κ (returns (Catch₂ x↯ y↡))
+            ⟨ reset ∷ ops , B , nat n ∷ int i ∷ s ⟩ ⟶◁∞
+            Matches⁺ ops s (x catch y) i
+  helper₈ x↯ y↡ reset ~ directly (returns (Catch₂ x↯ y↡))
hunk ./CompilerCorrectness/BarTheorem.agda 134
-  helper₇ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (x catch y) i) P ->
+  helper₇ : forall {ops i s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 136
-            Cont (Matches⁺ (reset ∷ ops) (int i ∷ s) y B) P
-  helper₇ κ x↯ (returns y↡) ~ via (, reset) (helper₈ κ x↯ y↡)
-  helper₇ κ x↯ (throws  y↯) ~ via (, int)   (helper₉ κ x↯ y↯)
+            Matches⁺ (reset ∷ ops) (int i ∷ s) y B ∋◁∞
+            Matches⁺ ops s (x catch y) i
+  helper₇ x↯ (returns y↡) ~ via (, reset) (helper₈ x↯ y↡)
+  helper₇ x↯ (throws  y↯) ~ via (, int)   (helper₉ x↯ y↯)
hunk ./CompilerCorrectness/BarTheorem.agda 141
-  helper₆ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (x catch y) i) P ->
+  helper₆ : forall {ops i s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 143
-            Cont⟶ ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ P
-  helper₆ κ x↯ han ~ bar-thm y (helper₇ κ x↯)
+            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ⟶◁∞
+            Matches⁺ ops s (x catch y) i
+  helper₆ x↯ han ~ ◁∞-trans (bar-theorem y) (helper₇ x↯)
hunk ./CompilerCorrectness/BarTheorem.agda 147
-  helper₅ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (x catch y) i) P ->
+  helper₅ : forall {ops i s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 149
-            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ◁∞ P
-  helper₅ κ x↯ ~ via (, han) (helper₆ κ x↯)
+            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ◁∞
+            Matches⁺ ops s (x catch y) i
+  helper₅ x↯ ~ via (, han) (helper₆ x↯)
hunk ./CompilerCorrectness/BarTheorem.agda 153
-  helper₄ : forall {ops m s P} ->
-            Cont (Matches⁺ ops s (x catch y) U) P ->
-            Cont⟶ ⟪ U , nat m ∷ han (comp y (reset ∷ ops)) ∷ s ⟫ P
-  helper₄ κ nat ~ helper₅ κ Int
+  helper₄ : forall {ops m s} ->
+            ⟪ U , nat m ∷ han (comp y (reset ∷ ops)) ∷ s ⟫ ⟶◁∞
+            Matches⁺ ops s (x catch y) U
+  helper₄ nat ~ helper₅ Int
hunk ./CompilerCorrectness/BarTheorem.agda 158
-  helper₃ : forall {ops i m s P} ->
-            Cont (Matches⁺ ops s (x catch y) i) P ->
+  helper₃ : forall {ops i m s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 160
-            Cont⟶ ⟨ unmark ∷ ops , i ,
-                    nat m ∷ han (comp y (reset ∷ ops)) ∷ s ⟩ P
-  helper₃ κ x↡ unmark    ~ κ (returns (Catch₁ x↡))
-  helper₃ κ _  interrupt ~ via (, nat) (helper₄ κ)
+            ⟨ unmark ∷ ops , i ,
+              nat m ∷ han (comp y (reset ∷ ops)) ∷ s ⟩ ⟶◁∞
+            Matches⁺ ops s (x catch y) i
+  helper₃ x↡ unmark    ~ directly (returns (Catch₁ x↡))
+  helper₃ _  interrupt ~ via (, nat) helper₄
hunk ./CompilerCorrectness/BarTheorem.agda 166
-  helper₂ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (x catch y) i) P ->
-            Cont (Matches⁺ (unmark ∷ ops)
-                           (han (comp y (reset ∷ ops)) ∷ s) x i) P
-  helper₂ κ (returns x↡) ~ via (, unmark) (helper₃ κ x↡)
-  helper₂ κ (throws  x↯) ~ helper₅ κ x↯
+  helper₂ : forall {ops i s} ->
+            Matches⁺ (unmark ∷ ops)
+                     (han (comp y (reset ∷ ops)) ∷ s) x i ∋◁∞
+            Matches⁺ ops s (x catch y) i
+  helper₂ (returns x↡) ~ via (, unmark) (helper₃ x↡)
+  helper₂ (throws  x↯) ~ helper₅ x↯
hunk ./CompilerCorrectness/BarTheorem.agda 173
-  helper₁ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (x catch y) i) P ->
-            Cont⟶ ⟨ mark (comp y (reset ∷ ops)) ∷
-                      comp x (unmark ∷ ops) , i , s ⟩ P
-  helper₁ κ mark      ~ bar-thm x (helper₂ κ)
-  helper₁ κ interrupt ~ κ (throws Int)
+  helper₁ : forall {ops i s} ->
+            ⟨ mark (comp y (reset ∷ ops)) ∷
+                comp x (unmark ∷ ops) , i , s ⟩ ⟶◁∞
+            Matches⁺ ops s (x catch y) i
+  helper₁ mark      ~ ◁∞-trans (bar-theorem x) helper₂
+  helper₁ interrupt ~ directly (throws Int)
hunk ./CompilerCorrectness/BarTheorem.agda 180
-bar-thm (block x) κ ~ via (, set) (helper₁ κ)
+bar-theorem (block x) ~ via (, set) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 182
-  helper₄ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (block x) i) P ->
+  helper₄ : forall {ops i s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 184
-            Cont⟶ ⟪ B , int i ∷ s ⟫ P
-  helper₄ κ x↯ int ~ κ (throws (Block x↯))
+            ⟪ B , int i ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (block x) i
+  helper₄ x↯ int ~ directly (throws (Block x↯))
hunk ./CompilerCorrectness/BarTheorem.agda 187
-  helper₃ : forall {ops i m s P} ->
-            Cont (Matches⁺ ops s (block x) i) P ->
+  helper₃ : forall {ops i m s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 189
-            Cont⟶ ⟨ reset ∷ ops , B , nat m ∷ int i ∷ s ⟩ P
-  helper₃ κ x↡ reset ~ κ (returns (Block x↡))
+            ⟨ reset ∷ ops , B , nat m ∷ int i ∷ s ⟩ ⟶◁∞
+            Matches⁺ ops s (block x) i
+  helper₃ x↡ reset ~ directly (returns (Block x↡))
hunk ./CompilerCorrectness/BarTheorem.agda 193
-  helper₂ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (block x) i) P ->
-            Cont (Matches⁺ (reset ∷ ops) (int i ∷ s) x B) P
-  helper₂ κ (returns x↡) ~ via (, reset) (helper₃ κ x↡)
-  helper₂ κ (throws  x↯) ~ via (, int)   (helper₄ κ x↯)
+  helper₂ : forall {ops i s} ->
+            Matches⁺ (reset ∷ ops) (int i ∷ s) x B ∋◁∞
+            Matches⁺ ops s (block x) i
+  helper₂ (returns x↡) ~ via (, reset) (helper₃ x↡)
+  helper₂ (throws  x↯) ~ via (, int)   (helper₄ x↯)
hunk ./CompilerCorrectness/BarTheorem.agda 199
-  helper₁ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (block x) i) P ->
-            Cont⟶ ⟨ set B ∷ comp x (reset ∷ ops) , i , s ⟩ P
-  helper₁ κ set       ~ bar-thm x (helper₂ κ)
-  helper₁ κ interrupt ~ κ (throws Int)
+  helper₁ : forall {ops i s} ->
+            ⟨ set B ∷ comp x (reset ∷ ops) , i , s ⟩ ⟶◁∞
+            Matches⁺ ops s (block x) i
+  helper₁ set       ~ ◁∞-trans (bar-theorem x) helper₂
+  helper₁ interrupt ~ directly (throws Int)
hunk ./CompilerCorrectness/BarTheorem.agda 205
-bar-thm (unblock x) κ ~ via (, set) (helper₁ κ)
+bar-theorem (unblock x) ~ via (, set) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 207
-  helper₆ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (unblock x) i) P ->
+  helper₆ : forall {ops i s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 209
-            Cont⟶ ⟪ U , int i ∷ s ⟫ P
-  helper₆ κ x↯ int ~ κ (throws (Unblock x↯))
+            ⟪ U , int i ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (unblock x) i
+  helper₆ x↯ int ~ directly (throws (Unblock x↯))
hunk ./CompilerCorrectness/BarTheorem.agda 212
-  helper₅ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (unblock x) i) P ->
+  helper₅ : forall {ops i s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 214
-            ⟪ U , int i ∷ s ⟫ ◁∞ P
-  helper₅ κ x↯ ~ via (, int) (helper₆ κ x↯)
+            ⟪ U , int i ∷ s ⟫ ◁∞ (Matches⁺ ops s (unblock x) i)
+  helper₅ x↯ ~ via (, int) (helper₆ x↯)
hunk ./CompilerCorrectness/BarTheorem.agda 217
-  helper₄ : forall {ops i m s P} ->
-            Cont (Matches⁺ ops s (unblock x) i) P ->
-            Cont⟶ ⟪ U , nat m ∷ int i ∷ s ⟫ P
-  helper₄ κ nat ~ helper₅ κ Int
+  helper₄ : forall {ops i m s} ->
+            ⟪ U , nat m ∷ int i ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (unblock x) i
+  helper₄ nat ~ helper₅ Int
hunk ./CompilerCorrectness/BarTheorem.agda 221
-  helper₃ : forall {ops i m s P} ->
-            Cont (Matches⁺ ops s (unblock x) i) P ->
+  helper₃ : forall {ops i m s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 223
-            Cont⟶ ⟨ reset ∷ ops , U , nat m ∷ int i ∷ s ⟩ P
-  helper₃ κ x↡ reset     ~ κ (returns (Unblock x↡))
-  helper₃ κ _  interrupt ~ via (, nat) (helper₄ κ)
+            ⟨ reset ∷ ops , U , nat m ∷ int i ∷ s ⟩ ⟶◁∞
+            Matches⁺ ops s (unblock x) i
+  helper₃ x↡ reset     ~ directly (returns (Unblock x↡))
+  helper₃ _  interrupt ~ via (, nat) helper₄
hunk ./CompilerCorrectness/BarTheorem.agda 228
-  helper₂ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (unblock x) i) P ->
-            Cont (Matches⁺ (reset ∷ ops) (int i ∷ s) x U) P
-  helper₂ κ (returns x↡) ~ via (, reset) (helper₃ κ x↡)
-  helper₂ κ (throws  x↯) ~ helper₅ κ x↯
+  helper₂ : forall {ops i s} ->
+            Matches⁺ (reset ∷ ops) (int i ∷ s) x U ∋◁∞
+            Matches⁺ ops s (unblock x) i
+  helper₂ (returns x↡) ~ via (, reset) (helper₃ x↡)
+  helper₂ (throws  x↯) ~ helper₅ x↯
hunk ./CompilerCorrectness/BarTheorem.agda 234
-  helper₁ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (unblock x) i) P ->
-            Cont⟶ ⟨ set U ∷ comp x (reset ∷ ops) , i , s ⟩ P
-  helper₁ κ set       ~ bar-thm x (helper₂ κ)
-  helper₁ κ interrupt ~ κ (throws Int)
+  helper₁ : forall {ops i s} ->
+            ⟨ set U ∷ comp x (reset ∷ ops) , i , s ⟩ ⟶◁∞
+            Matches⁺ ops s (unblock x) i
+  helper₁ set       ~ ◁∞-trans (bar-theorem x) helper₂
+  helper₁ interrupt ~ directly (throws Int)
hunk ./CompilerCorrectness/BarTheorem.agda 240
-bar-thm (loop x) κ ~ via (, loop) (helper₁ κ)
+bar-theorem (loop x) ~ via (, loop) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 242
-  helper₄ : forall {ops m s P} ->
-            Cont (Matches⁺ ops s (loop x) U) P ->
-            Cont⟶ ⟪ U , nat m ∷ s ⟫ P
-  helper₄ κ nat ~ κ (throws Int)
+  helper₄ : forall {ops m s} ->
+            ⟪ U , nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (loop x) U
+  helper₄ nat ~ directly (throws Int)
hunk ./CompilerCorrectness/BarTheorem.agda 246
-  helper₃ : forall {ops i m s P} ->
-            Cont (Matches⁺ ops s (loop x) i) P ->
+  helper₃ : forall {ops i m s} ->
hunk ./CompilerCorrectness/BarTheorem.agda 248
-            Cont⟶ ⟨ pop ∷ loop x ∷ ops , i , nat m ∷ s ⟩ P
-  helper₃ κ x↡ pop       ~ bar-thm (loop x) κ
-  helper₃ κ _  interrupt ~ via (, nat) (helper₄ κ)
-
-  helper₂ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (loop x) i) P ->
-            Cont (Matches⁺ (pop ∷ loop x ∷ ops) s x i) P
-  helper₂ κ (throws  x↯) ~ κ (throws (Loop (Seqn₂ x↯)))
-  helper₂ κ (returns x↡) ~ via (, pop) (helper₃ κ x↡)
+            ⟨ pop ∷ loop x ∷ ops , i , nat m ∷ s ⟩ ⟶◁∞
+            Matches⁺ ops s (loop x) i
+  helper₃ x↡ pop       ~ bar-theorem (loop x)
+  helper₃ _  interrupt ~ via (, nat) helper₄
hunk ./CompilerCorrectness/BarTheorem.agda 253
-  helper₁ : forall {ops i s P} ->
-            Cont (Matches⁺ ops s (loop x) i) P ->
-            Cont⟶ ⟨ loop x ∷ ops , i , s ⟩ P
-  helper₁ κ loop      ~ bar-thm x (helper₂ κ)
-  helper₁ κ interrupt ~ κ (throws Int)
+  helper₂ : forall {ops i s} ->
+            Matches⁺ (pop ∷ loop x ∷ ops) s x i ∋◁∞
+            Matches⁺ ops s (loop x) i
+  helper₂ (throws  x↯) ~ directly (throws (Loop (Seqn₂ x↯)))
+  helper₂ (returns x↡) ~ via (, pop) (helper₃ x↡)
hunk ./CompilerCorrectness/BarTheorem.agda 259
--- The bar theorem.
-
-bar-theorem : forall {t} (e : Expr t) {ops i s} ->
-              ⟨ comp e ops , i , s ⟩ ◁∞ Matches⁺ ops s e i
-bar-theorem e = bar-thm e directly
+  helper₁ : forall {ops i s} ->
+            ⟨ loop x ∷ ops , i , s ⟩ ⟶◁∞ Matches⁺ ops s (loop x) i
+  helper₁ loop      ~ ◁∞-trans (bar-theorem x) helper₂
+  helper₁ interrupt ~ directly (throws Int)