[Made the bar theorem useful by switching from _◁_ to _◁∞_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080624132947] hunk ./CompilerCorrectness/BarTheorem.agda 4
-
--- This theorem is currently unused.
-
+
hunk ./CompilerCorrectness/BarTheorem.agda 11
-open import Totality
hunk ./CompilerCorrectness/BarTheorem.agda 15
-open import Data.Empty
-open import Relation.Nullary
+open import Data.Function using (_∘_)
hunk ./CompilerCorrectness/BarTheorem.agda 17
+open import Relation.Binary.PropositionalEquality
hunk ./CompilerCorrectness/BarTheorem.agda 34
--- The bar theorem.
+-- Some abbreviations, used by the bar theorem below.
hunk ./CompilerCorrectness/BarTheorem.agda 36
-bar-theorem : forall {t} (e : Expr t) {ops i s} ->
-              ¬ e ⇑[ i ] ->
-              ⟨ comp e ops , i , s ⟩ ◁ Matches⁺ ops s e i
-bar-theorem {t = t} (val n) ¬⇑ = via (_ , push) helper
+Cont : Pred State -> Pred State -> Set
+Cont P Q = forall {y} -> y ∈ P -> y ◁∞ Q
+
+Cont⟶ : State -> Pred State -> Set
+Cont⟶ x = Cont (_⟶_ x)
+
+-- The bar theorem. Written in continuation-passing style since I
+-- thought that the use of ◁∞-trans would not fare well with the
+-- productivity checker. This rewrite turned out to be unnecessary,
+-- but it would make the hack in the loop case below unnecessary if
+-- the productivity checker kept track of "productivity-preserving"
+-- definitions.
+
+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-thm {t = t} (val n) κ ~ via (_ , push) (helper₁ κ)
hunk ./CompilerCorrectness/BarTheorem.agda 55
-  helper : forall {ops i s y} ->
-           ⟨ push n ∷ ops , i , s ⟩ ⟶ y ->
-           y ◁ Matches⁺ ops s {t = t} (val n) i
-  helper push      = directly (returns Val)
-  helper interrupt = directly (throws Int)
+  helper₁ : forall {ops i s P} ->
+            Cont (Matches⁺ ops s (val {t = t} n) i) P ->
+            Cont⟶ ⟨ push n ∷ ops , i , s ⟩ P
+  helper₁ κ push      ~ κ (returns Val)
+  helper₁ κ interrupt ~ κ (throws Int)
hunk ./CompilerCorrectness/BarTheorem.agda 61
-bar-theorem {t = t} throw ¬⇑ = via (_ , throw) helper
+bar-thm {t = t} throw κ ~ via (_ , throw) (helper₁ κ)
hunk ./CompilerCorrectness/BarTheorem.agda 63
-  helper : forall {ops i s y} ->
-           ⟨ throw ∷ ops , i , s ⟩ ⟶ y ->
-           y ◁ Matches⁺ ops s {t = t} throw i
-  helper throw     = directly (throws Throw)
-  helper interrupt = directly (throws Int)
+  helper₁ : forall {ops i s P} ->
+            Cont (Matches⁺ ops s (throw {t = t}) i) P ->
+            Cont⟶ ⟨ throw ∷ ops , i , s ⟩ P
+  helper₁ κ throw     ~ κ (throws Throw)
+  helper₁ κ interrupt ~ κ (throws Int)
hunk ./CompilerCorrectness/BarTheorem.agda 69
-bar-theorem (x ⊕ y) ¬⇑ = ◁-trans (bar-theorem x (¬⇑-⊕ˡ ¬⇑))
-                                 (helper₁ ¬⇑)
+bar-thm (x ⊕ y) κ ~ bar-thm x (helper₁ κ)
hunk ./CompilerCorrectness/BarTheorem.agda 71
-  helper₆ : forall {ops m s z} ->
-            ⟪ U , val m ∷ s ⟫ ⟶ z ->
-            z ◁ Matches⁺ ops s (x ⊕ y) U
-  helper₆ val = directly (throws Int)
+  helper₆ : forall {ops m s P} ->
+            Cont (Matches⁺ ops s (x ⊕ y) U) P ->
+            Cont⟶ ⟪ U , val m ∷ s ⟫ P
+  helper₆ κ val ~ κ (throws Int)
hunk ./CompilerCorrectness/BarTheorem.agda 76
-  helper₅ : forall {ops m n s z} ->
-            ⟪ U , val n ∷ val m ∷ s ⟫ ⟶ z ->
-            z ◁ Matches⁺ ops s (x ⊕ y) U
-  helper₅ val = via (_ , val) helper₆
+  helper₅ : forall {ops m n s P} ->
+            Cont (Matches⁺ ops s (x ⊕ y) U) P ->
+            Cont⟶ ⟪ U , val n ∷ val m ∷ s ⟫ P
+  helper₅ κ val ~ via (_ , val) (helper₆ κ)
hunk ./CompilerCorrectness/BarTheorem.agda 81
-  helper₄ : forall {ops i m s z} ->
+  helper₄ : forall {ops i m s P} ->
+            Cont (Matches⁺ ops s (x ⊕ y) i) P ->
hunk ./CompilerCorrectness/BarTheorem.agda 84
-            ⟪ i , val m ∷ s ⟫ ⟶ z ->
-            z ◁ Matches⁺ ops s (x ⊕ y) i
-  helper₄ x⇓ y↯ val = directly (throws (Add₃ x⇓ y↯))
+            Cont⟶ ⟪ i , val m ∷ s ⟫ P
+  helper₄ κ x⇓ y↯ val ~ κ (throws (Add₃ x⇓ y↯))
hunk ./CompilerCorrectness/BarTheorem.agda 87
-  helper₃ : forall {ops i n m s z} ->
+  helper₃ : forall {ops i n m s P} ->
+            Cont (Matches⁺ ops s (x ⊕ y) i) P ->
hunk ./CompilerCorrectness/BarTheorem.agda 90
-            ⟨ add ∷ ops , i , val n ∷ val m ∷ s ⟩ ⟶ z ->
-            z ◁ Matches⁺ ops s (x ⊕ y) i
-  helper₃ x⇓ y⇓ add       = directly (returns (Add₁ x⇓ y⇓))
-  helper₃ _  _  interrupt = via (_ , val) helper₅
+            Cont⟶ ⟨ add ∷ ops , i , val n ∷ val m ∷ s ⟩ P
+  helper₃ κ x⇓ y⇓ add       ~ κ (returns (Add₁ x⇓ y⇓))
+  helper₃ κ _  _  interrupt ~ via (_ , val) (helper₅ κ)
hunk ./CompilerCorrectness/BarTheorem.agda 94
-  helper₂ : forall {ops i m s z} ->
+  helper₂ : forall {ops i m s P} ->
+            Cont (Matches⁺ ops s (x ⊕ y) i) P ->
hunk ./CompilerCorrectness/BarTheorem.agda 97
-            Matches⁺ (add ∷ ops) (val m ∷ s) y i z ->
-            z ◁ Matches⁺ ops s (x ⊕ y) i
-  helper₂ x⇓ (returns y⇓) = via (_ , add) (helper₃ x⇓ y⇓)
-  helper₂ x⇓ (throws y↯)  = via (_ , val) (helper₄ x⇓ y↯)
+            Cont (Matches⁺ (add ∷ ops) (val m ∷ s) y i) P
+  helper₂ κ x⇓ (returns y⇓) ~ via (_ , add) (helper₃ κ x⇓ y⇓)
+  helper₂ κ x⇓ (throws y↯)  ~ via (_ , val) (helper₄ κ x⇓ y↯)
hunk ./CompilerCorrectness/BarTheorem.agda 101
-  helper₁ : forall {ops i s z} ->
-            ¬ x ⊕ y ⇑[ i ] ->
-            Matches⁺ (comp y (add ∷ ops)) s x i z ->
-            z ◁ Matches⁺ ops s (x ⊕ y) i
-  helper₁ _  (throws  x↯) = directly (throws (Add₂ x↯))
-  helper₁ ¬⇑ (returns x⇓) = ◁-trans (bar-theorem y (¬⇑-⊕ʳ ¬⇑ (_ , x⇓)))
-                                    (helper₂ x⇓)
+  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⇓)
hunk ./CompilerCorrectness/BarTheorem.agda 107
-bar-theorem (x >> y) ¬⇑ = ◁-trans (bar-theorem x (¬⇑->>ˡ ¬⇑))
-                                  (helper₁ ¬⇑)
+bar-thm (x >> y) κ ~ bar-thm x (helper₁ κ)
hunk ./CompilerCorrectness/BarTheorem.agda 109
-  helper₄ : forall {ops m s z} ->
-            ⟪ U , val m ∷ s ⟫ ⟶ z ->
-            z ◁ Matches⁺ ops s (x >> y) U
-  helper₄ val = directly (throws Int)
+  helper₄ : forall {ops m s P} ->
+            Cont (Matches⁺ ops s (x >> y) U) P ->
+            Cont⟶ ⟪ U , val m ∷ s ⟫ P
+  helper₄ κ val ~ κ (throws Int)
hunk ./CompilerCorrectness/BarTheorem.agda 114
-  helper₃ : forall {ops i m s z} ->
+  helper₃ : forall {ops i m s P} ->
+            Cont (Matches⁺ ops s (x >> y) i) P ->
hunk ./CompilerCorrectness/BarTheorem.agda 117
-            Matches⁺ ops s y i z ->
-            z ◁ Matches⁺ ops s (x >> y) i
-  helper₃ x⇓ (returns y⇓) = directly (returns (Seqn₁ x⇓ y⇓))
-  helper₃ x⇓ (throws  y↯) = directly (throws  (Seqn₁ x⇓ y↯))
+            Cont (Matches⁺ ops s y i) P
+  helper₃ κ x⇓ (returns y⇓) ~ κ (returns (Seqn₁ x⇓ y⇓))
+  helper₃ κ x⇓ (throws  y↯) ~ κ (throws  (Seqn₁ x⇓ y↯))
hunk ./CompilerCorrectness/BarTheorem.agda 121
-  helper₂ : forall {ops i m s z} ->
-            ¬ x >> y ⇑[ i ] -> x ⇓[ i ] val m ->
-            ⟨ pop ∷ comp y ops , i , val m ∷ s ⟩ ⟶ z ->
-            z ◁ Matches⁺ ops s (x >> y) i
-  helper₂ ¬⇑ x⇓ pop       = ◁-trans (bar-theorem y (¬⇑->>ʳ ¬⇑ (_ , x⇓)))
-                                    (helper₃ x⇓)
-  helper₂ _  _  interrupt = via (_ , val) helper₄
+  helper₂ : forall {ops i m s P} ->
+            Cont (Matches⁺ ops s (x >> y) i) P ->
+            x ⇓[ i ] val m ->
+            Cont⟶ ⟨ pop ∷ comp y ops , i , val m ∷ s ⟩ P
+  helper₂ κ x⇓ pop       ~ bar-thm y (helper₃ κ x⇓)
+  helper₂ κ _  interrupt ~ via (_ , val) (helper₄ κ)
hunk ./CompilerCorrectness/BarTheorem.agda 128
-  helper₁ : forall {ops i s z} ->
-            ¬ x >> y ⇑[ i ] ->
-            Matches⁺ (pop ∷ comp y ops) s x i z ->
-            z ◁ Matches⁺ ops s (x >> y) i
-  helper₁ _  (throws  x↯) = directly (throws (Seqn₂ x↯))
-  helper₁ ¬⇑ (returns x⇓) = via (_ , pop) (helper₂ ¬⇑ x⇓)
+  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⇓)
hunk ./CompilerCorrectness/BarTheorem.agda 134
-bar-theorem (x catch y) ¬⇑ = via (_ , mark) (helper₁ ¬⇑)
+bar-thm (x catch y) κ ~ via (_ , mark) (helper₁ κ)
hunk ./CompilerCorrectness/BarTheorem.agda 136
-  helper₉ : forall {ops i s z} ->
+  helper₉ : forall {ops i s P} ->
+            Cont (Matches⁺ ops s (x catch y) i) P ->
hunk ./CompilerCorrectness/BarTheorem.agda 139
-            ⟪ B , int i ∷ s ⟫ ⟶ z ->
-            z ◁ Matches⁺ ops s (x catch y) i
-  helper₉ x↯ y↯ int = directly (throws (Catch₂ x↯ y↯))
+            Cont⟶ ⟪ B , int i ∷ s ⟫ P
+  helper₉ κ x↯ y↯ int ~ κ (throws (Catch₂ x↯ y↯))
hunk ./CompilerCorrectness/BarTheorem.agda 142
-  helper₈ : forall {ops i n s z} ->
+  helper₈ : forall {ops i n s P} ->
+            Cont (Matches⁺ ops s (x catch y) i) P ->
hunk ./CompilerCorrectness/BarTheorem.agda 145
-            ⟨ reset ∷ ops , B , val n ∷ int i ∷ s ⟩ ⟶ z ->
-            z ◁ Matches⁺ ops s (x catch y) i
-  helper₈ x↯ y⇓ reset = directly (returns (Catch₂ x↯ y⇓))
+            Cont⟶ ⟨ reset ∷ ops , B , val n ∷ int i ∷ s ⟩ P
+  helper₈ κ x↯ y⇓ reset ~ κ (returns (Catch₂ x↯ y⇓))
hunk ./CompilerCorrectness/BarTheorem.agda 148
-  helper₇ : forall {ops i s z} ->
+  helper₇ : forall {ops i s P} ->
+            Cont (Matches⁺ ops s (x catch y) i) P ->
hunk ./CompilerCorrectness/BarTheorem.agda 151
-            Matches⁺ (reset ∷ ops) (int i ∷ s) y B z ->
-            z ◁ 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↯)
+            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↯)
hunk ./CompilerCorrectness/BarTheorem.agda 155
-  helper₆ : forall {ops i s z} ->
-            ¬ x catch y ⇑[ i ] -> x ↯[ i ] ->
-            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ⟶ z ->
-            z ◁ Matches⁺ ops s (x catch y) i
-  helper₆ ¬⇑ x↯ han = ◁-trans (bar-theorem y (¬⇑-catchʳ ¬⇑ x↯))
-                              (helper₇ x↯)
+  helper₆ : forall {ops i s P} ->
+            Cont (Matches⁺ ops s (x catch y) i) P ->
+            x ↯[ i ] ->
+            Cont⟶ ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ P
+  helper₆ κ x↯ han ~ bar-thm y (helper₇ κ x↯)
hunk ./CompilerCorrectness/BarTheorem.agda 161
-  helper₅ : forall {ops i s} ->
-            ¬ x catch y ⇑[ i ] -> x ↯[ i ] ->
-            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ◁
-            Matches⁺ ops s (x catch y) i
-  helper₅ ¬⇑ x↯ = via (_ , han) (helper₆ ¬⇑ x↯)
+  helper₅ : forall {ops i s P} ->
+            Cont (Matches⁺ ops s (x catch y) i) P ->
+            x ↯[ i ] ->
+            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ◁∞ P
+  helper₅ κ x↯ ~ via (_ , han) (helper₆ κ x↯)
hunk ./CompilerCorrectness/BarTheorem.agda 167
-  helper₄ : forall {ops m s z} ->
-            ¬ x catch y ⇑[ U ] ->
-            ⟪ U , val m ∷ han (comp y (reset ∷ ops)) ∷ s ⟫ ⟶ z ->
-            z ◁ Matches⁺ ops s (x catch y) U
-  helper₄ ¬⇑ val = helper₅ ¬⇑ Int
+  helper₄ : forall {ops m s P} ->
+            Cont (Matches⁺ ops s (x catch y) U) P ->
+            Cont⟶ ⟪ U , val m ∷ han (comp y (reset ∷ ops)) ∷ s ⟫ P
+  helper₄ κ val ~ helper₅ κ Int
hunk ./CompilerCorrectness/BarTheorem.agda 172
-  helper₃ : forall {ops i m s z} ->
-            ¬ x catch y ⇑[ i ] -> x ⇓[ i ] val m ->
-            ⟨ unmark ∷ ops , i ,
-              val m ∷ han (comp y (reset ∷ ops)) ∷ s ⟩ ⟶ z ->
-            z ◁ Matches⁺ ops s (x catch y) i
-  helper₃ _  x⇓ unmark    = directly (returns (Catch₁ x⇓))
-  helper₃ ¬⇑ _  interrupt = via (_ , val) (helper₄ ¬⇑)
+  helper₃ : forall {ops i m s P} ->
+            Cont (Matches⁺ ops s (x catch y) i) P ->
+            x ⇓[ i ] val m ->
+            Cont⟶ ⟨ unmark ∷ ops , i ,
+                    val m ∷ han (comp y (reset ∷ ops)) ∷ s ⟩ P
+  helper₃ κ x⇓ unmark    ~ κ (returns (Catch₁ x⇓))
+  helper₃ κ _  interrupt ~ via (_ , val) (helper₄ κ)
hunk ./CompilerCorrectness/BarTheorem.agda 180
-  helper₂ : forall {ops i s z} ->
-            ¬ x catch y ⇑[ i ] ->
-            Matches⁺ (unmark ∷ ops) (han (comp y (reset ∷ ops)) ∷ s)
-                     x i z ->
-            z ◁ Matches⁺ ops s (x catch y) i
-  helper₂ ¬⇑ (returns x⇓) = via (_ , unmark) (helper₃ ¬⇑ x⇓)
-  helper₂ ¬⇑ (throws  x↯) = helper₅ ¬⇑ x↯
+  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↯
hunk ./CompilerCorrectness/BarTheorem.agda 187
-  helper₁ : forall {ops i s z} ->
-            ¬ x catch y ⇑[ i ] ->
-            ⟨ mark (comp y (reset ∷ ops)) ∷
-              comp x (unmark ∷ ops) , i , s ⟩ ⟶ z ->
-            z ◁ Matches⁺ ops s (x catch y) i
-  helper₁ ¬⇑ mark      = ◁-trans (bar-theorem x (¬⇑-catchˡ ¬⇑))
-                                 (helper₂ ¬⇑)
-  helper₁ _  interrupt = directly (throws Int)
+  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)
hunk ./CompilerCorrectness/BarTheorem.agda 194
-bar-theorem (block x) ¬⇑ = via (_ , set) helper₁
+bar-thm (block x) κ ~ via (_ , set) (helper₁ κ)
hunk ./CompilerCorrectness/BarTheorem.agda 196
-  helper₄ : forall {ops i s y} ->
+  helper₄ : forall {ops i s P} ->
+            Cont (Matches⁺ ops s (block x) i) P ->
hunk ./CompilerCorrectness/BarTheorem.agda 199
-            ⟪ B , int i ∷ s ⟫ ⟶ y ->
-            y ◁ Matches⁺ ops s (block x) i
-  helper₄ x↯ int = directly (throws (Block x↯))
+            Cont⟶ ⟪ B , int i ∷ s ⟫ P
+  helper₄ κ x↯ int ~ κ (throws (Block x↯))
hunk ./CompilerCorrectness/BarTheorem.agda 202
-  helper₃ : forall {ops i m s y} ->
+  helper₃ : forall {ops i m s P} ->
+            Cont (Matches⁺ ops s (block x) i) P ->
hunk ./CompilerCorrectness/BarTheorem.agda 205
-            ⟨ reset ∷ ops , B , val m ∷ int i ∷ s ⟩ ⟶ y ->
-            y ◁ Matches⁺ ops s (block x) i
-  helper₃ x⇓ reset = directly (returns (Block x⇓))
+            Cont⟶ ⟨ reset ∷ ops , B , val m ∷ int i ∷ s ⟩ P
+  helper₃ κ x⇓ reset ~ κ (returns (Block x⇓))
hunk ./CompilerCorrectness/BarTheorem.agda 208
-  helper₂ : forall {ops i s y} ->
-            Matches⁺ (reset ∷ ops) (int i ∷ s) x B y ->
-            y ◁ Matches⁺ ops s (block x) i
-  helper₂ (returns x⇓) = via (_ , reset) (helper₃ x⇓)
-  helper₂ (throws  x↯) = via (_ , int)   (helper₄ x↯)
+  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↯)
hunk ./CompilerCorrectness/BarTheorem.agda 214
-  helper₁ : forall {ops i s y} ->
-            ⟨ set B ∷ comp x (reset ∷ ops) , i , s ⟩ ⟶ y ->
-            y ◁ Matches⁺ ops s (block x) i
-  helper₁ set       = ◁-trans (bar-theorem x (¬⇑-block ¬⇑))
-                              helper₂
-  helper₁ interrupt = directly (throws Int)
+  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)
hunk ./CompilerCorrectness/BarTheorem.agda 220
-bar-theorem (unblock x) ¬⇑ = via (_ , set) helper₁
+bar-thm (unblock x) κ ~ via (_ , set) (helper₁ κ)
hunk ./CompilerCorrectness/BarTheorem.agda 222
-  helper₆ : forall {ops i s y} ->
+  helper₆ : forall {ops i s P} ->
+            Cont (Matches⁺ ops s (unblock x) i) P ->
hunk ./CompilerCorrectness/BarTheorem.agda 225
-            ⟪ U , int i ∷ s ⟫ ⟶ y ->
-            y ◁ Matches⁺ ops s (unblock x) i
-  helper₆ x↯ int = directly (throws (Unblock x↯))
+            Cont⟶ ⟪ U , int i ∷ s ⟫ P
+  helper₆ κ x↯ int ~ κ (throws (Unblock x↯))
hunk ./CompilerCorrectness/BarTheorem.agda 228
-  helper₅ : forall {ops i s} ->
+  helper₅ : forall {ops i s P} ->
+            Cont (Matches⁺ ops s (unblock x) i) P ->
hunk ./CompilerCorrectness/BarTheorem.agda 231
-            ⟪ U , int i ∷ s ⟫ ◁ Matches⁺ ops s (unblock x) i
-  helper₅ x↯ = via (_ , int) (helper₆ x↯)
+            ⟪ U , int i ∷ s ⟫ ◁∞ P
+  helper₅ κ x↯ ~ via (_ , int) (helper₆ κ x↯)
hunk ./CompilerCorrectness/BarTheorem.agda 234
-  helper₄ : forall {ops i m s y} ->
-            ⟪ U , val m ∷ int i ∷ s ⟫ ⟶ y ->
-            y ◁ Matches⁺ ops s (unblock x) i
-  helper₄ val = helper₅ Int
+  helper₄ : forall {ops i m s P} ->
+            Cont (Matches⁺ ops s (unblock x) i) P ->
+            Cont⟶ ⟪ U , val m ∷ int i ∷ s ⟫ P
+  helper₄ κ val ~ helper₅ κ Int
hunk ./CompilerCorrectness/BarTheorem.agda 239
-  helper₃ : forall {ops i m s y} ->
+  helper₃ : forall {ops i m s P} ->
+            Cont (Matches⁺ ops s (unblock x) i) P ->
hunk ./CompilerCorrectness/BarTheorem.agda 242
-            ⟨ reset ∷ ops , U , val m ∷ int i ∷ s ⟩ ⟶ y ->
-            y ◁ Matches⁺ ops s (unblock x) i
-  helper₃ x⇓ reset     = directly (returns (Unblock x⇓))
-  helper₃ _  interrupt = via (_ , val) helper₄
+            Cont⟶ ⟨ reset ∷ ops , U , val m ∷ int i ∷ s ⟩ P
+  helper₃ κ x⇓ reset     ~ κ (returns (Unblock x⇓))
+  helper₃ κ _  interrupt ~ via (_ , val) (helper₄ κ)
hunk ./CompilerCorrectness/BarTheorem.agda 246
-  helper₂ : forall {ops i s y} ->
-            Matches⁺ (reset ∷ ops) (int i ∷ s) x U y ->
-            y ◁ Matches⁺ ops s (unblock x) i
-  helper₂ (returns x⇓) = via (_ , reset) (helper₃ x⇓)
-  helper₂ (throws  x↯) = helper₅ x↯
+  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↯
hunk ./CompilerCorrectness/BarTheorem.agda 252
-  helper₁ : forall {ops i s y} ->
-            ⟨ set U ∷ comp x (reset ∷ ops) , i , s ⟩ ⟶ y ->
-            y ◁ Matches⁺ ops s (unblock x) i
-  helper₁ set       = ◁-trans (bar-theorem x (¬⇑-unblock ¬⇑))
-                              helper₂
-  helper₁ interrupt = directly (throws Int)
+  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)
hunk ./CompilerCorrectness/BarTheorem.agda 258
-bar-theorem loop ¬⇑ = ⊥-elim (¬⇑ loop⇑)
+bar-thm loop κ ~ via (_ , loop) (helper₁ ≡-refl κ)
+  where
+  helper₁ : forall {ops i s P} {x : Expr partial} ->
+            x ≡ loop -> -- This argument is included so that the
+                        -- termination checker can see that the
+                        -- argument to the recursive call is the same
+                        -- as the input to bar-thm.
+            Cont (Matches⁺ ops s loop i) P ->
+            Cont⟶ ⟨ loop ∷ ops , i , s ⟩ P
+  helper₁ ≡-refl κ loop      ~ bar-thm loop κ
+  helper₁ _      κ interrupt ~ κ (throws Int)
+
+-- 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
hunk ./CompilerCorrectness/Soundness.agda 14
+open import CompilerCorrectness.BarTheorem
+import Bar; open Bar _⟶_
hunk ./CompilerCorrectness/Soundness.agda 22
-postulate
-  sound₁ : forall {t} (e : Expr t) {i} -> Sound₁ e i
+matches-final : forall {t e i c} -> Matches {t} e i c -> c ↛
+matches-final (returns _) (_ , ())
+matches-final (throws _)  (_ , ())
+
+final-final : forall {c} -> Final c -> c ↛
+final-final (returns _ _) (_ , ())
+final-final (throws _)    (_ , ())
+
+sound₁ : forall {t} (e : Expr t) {i} -> Sound₁ e i
+sound₁ e e⟶⋆s s↛ =
+  bar∞-lemma matches-final
+             (◁∞-map Matches⁺⇒Matches (bar-theorem e))
+             e⟶⋆s (final-final s↛)
hunk ./Everything.agda 61
-import CompilerCorrectness.BarTheorem  -- Currently unused.
-import CompilerCorrectness.Soundness   -- Currently contains postulates.
+import CompilerCorrectness.BarTheorem
+import CompilerCorrectness.Soundness  -- Currently contains postulates.
hunk ./Totality.agda 185
--- Finally some boring lemmas related to the absence of
--- non-termination.
-
-¬⇑-⊕ˡ : forall {t} {x y : Expr t} {i} ->
-        ¬ x ⊕ y ⇑[ i ] -> ¬ x ⇑[ i ]
-¬⇑-⊕ˡ ¬⇑ = \x⇑ -> ¬⇑ (Add₁ x⇑)
-
-¬⇑-⊕ʳ : forall {t} {x y : Expr t} {i} ->
-        ¬ x ⊕ y ⇑[ i ] -> x ↡[ i ] -> ¬ y ⇑[ i ]
-¬⇑-⊕ʳ ¬⇑ x⇓ = \y⇑ -> ¬⇑ (Add₂ x⇓ y⇑)
-
-¬⇑->>ˡ : forall {t} {x y : Expr t} {i} ->
-         ¬ x >> y ⇑[ i ] -> ¬ x ⇑[ i ]
-¬⇑->>ˡ ¬⇑ = \x⇑ -> ¬⇑ (Seqn₁ x⇑)
-
-¬⇑->>ʳ : forall {t} {x y : Expr t} {i} ->
-         ¬ x >> y ⇑[ i ] -> x ↡[ i ] -> ¬ y ⇑[ i ]
-¬⇑->>ʳ ¬⇑ x⇓ = \y⇑ -> ¬⇑ (Seqn₂ x⇓ y⇑)
-
-¬⇑-catchˡ : forall {t} {x y : Expr t} {i} ->
-            ¬ x catch y ⇑[ i ] -> ¬ x ⇑[ i ]
-¬⇑-catchˡ ¬⇑ = \x⇑ -> ¬⇑ (Catch₁ x⇑)
-
-¬⇑-catchʳ : forall {t} {x y : Expr t} {i} ->
-            ¬ x catch y ⇑[ i ] -> x ↯[ i ] -> ¬ y ⇑[ B ]
-¬⇑-catchʳ ¬⇑ x↯ = \y⇑ -> ¬⇑ (Catch₂ x↯ y⇑)
-
-¬⇑-block : forall {t} {x : Expr t} {i} ->
-           ¬ block x ⇑[ i ] -> ¬ x ⇑[ B ]
-¬⇑-block ¬⇑ = \x⇑ -> ¬⇑ (Block x⇑)
-
-¬⇑-unblock : forall {t} {x : Expr t} {i} ->
-             ¬ unblock x ⇑[ i ] -> ¬ x ⇑[ U ]
-¬⇑-unblock ¬⇑ = \x⇑ -> ¬⇑ (Unblock x⇑)
-