[Made the bar theorem pass the productivity checker.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080717224930] hunk ./Bar.agda 17
-open import Infinite
+open import Infinite hiding (∞′→∞; ∞″→∞; ∞→∞′)
hunk ./Bar.agda 119
+------------------------------------------------------------------------
+-- The code below can be used to handle some not obviously productive
+-- definitions
+
+mutual
+
+  codata _◁∞′_ (x : S) (P : Pred S) : Set1 where
+    directly : (x∈P : x ∈ P) -> x ◁∞′ P
+    ↑_       : x ◁∞″ P -> x ◁∞′ P
+
+  data _◁∞″_ (x : S) (P : Pred S) : Set1 where
+    via       : (x⟶ : x ⟶) (x⟶y◁∞P : forall {y} -> x ⟶ y -> y ◁∞′ P) ->
+                x ◁∞″ P
+    ◁∞′-trans : forall {Q}
+                (x◁∞Q : x ◁∞″ Q)
+                (Q◁∞P : forall {y} -> y ∈ Q -> y ◁∞′ P) ->
+                x ◁∞″ P
+
+-- A generalisation of ◁∞′-trans.
+
+◁∞′-trans′ : forall {x P Q} ->
+             x ◁∞′ P -> (forall {y} -> y ∈ P -> y ◁∞′ Q) -> x ◁∞′ Q
+◁∞′-trans′ (directly x∈P)          P◁∞Q ~ P◁∞Q x∈P
+◁∞′-trans′ (↑ via x⟶ x⟶y◁∞P)       P◁∞Q ~ ↑ via x⟶ (\x⟶y -> ◁∞′-trans′ (x⟶y◁∞P x⟶y) P◁∞Q)
+◁∞′-trans′ (↑ ◁∞′-trans x◁∞P P◁∞Q) Q◁∞R ~ ↑ ◁∞′-trans x◁∞P (\y∈P -> ◁∞′-trans′ (P◁∞Q y∈P) Q◁∞R)
+
+-- The first step can be accessed in finite time.
+
+data _◁∞‴_ (x : S) (P : Pred S) : Set1 where
+  via : (x⟶ : x ⟶) (x⟶y◁∞P : forall {y} -> x ⟶ y -> y ◁∞′ P) ->
+        x ◁∞‴ P
+
+via-view : forall {x P} -> x ◁∞″ P -> x ◁∞‴ P
+via-view (via x⟶ x⟶y◁∞P)       = via x⟶ x⟶y◁∞P
+via-view (◁∞′-trans x◁∞P P◁∞Q) with via-view x◁∞P
+via-view (◁∞′-trans x◁∞P P◁∞Q) | via x⟶ x⟶y◁∞P =
+  via x⟶ (\x⟶y -> ◁∞′-trans′ (x⟶y◁∞P x⟶y) P◁∞Q)
+
+-- _◁∞_ and _◁∞′_ are equivalent.
+
+mutual
+
+  ∞′→∞ : forall {x P} -> x ◁∞′ P -> x ◁∞ P
+  ∞′→∞ (directly x∈P) ~ directly x∈P
+  ∞′→∞ (↑ x◁∞P)       ~ ∞″→∞ x◁∞P
+
+  ∞″→∞ : forall {x P} -> x ◁∞″ P -> x ◁∞ P
+  ∞″→∞ x◁∞P ~ ∞‴→∞ (via-view x◁∞P)
+
+  ∞‴→∞ : forall {x P} -> x ◁∞‴ P -> x ◁∞ P
+  ∞‴→∞ (via x⟶ x⟶y◁∞P) ~ via x⟶ (\x⟶y -> ∞′→∞ (x⟶y◁∞P x⟶y))
+
+∞→∞′ : forall {x P} -> x ◁∞ P -> x ◁∞′ P
+∞→∞′ (directly x∈P)  ~ directly x∈P
+∞→∞′ (via x⟶ x⟶y◁∞P) ~ ↑ via x⟶ (\x⟶y -> ∞→∞′ (x⟶y◁∞P x⟶y))
+
hunk ./CompilerCorrectness/BarTheorem.agda 36
-_∋◁∞_ : Pred State -> Pred State -> Set
-P ∋◁∞ Q = forall {y} -> y ∈ P -> y ◁∞ Q
+_∋◁∞_ : Pred State -> Pred State -> Set1
+P ∋◁∞ Q = forall {y} -> y ∈ P -> y ◁∞′ Q
hunk ./CompilerCorrectness/BarTheorem.agda 39
-_⟶◁∞_ : State -> Pred State -> Set
+_⟶◁∞_ : State -> Pred State -> Set1
hunk ./CompilerCorrectness/BarTheorem.agda 44
-bar-theorem : forall {t} (e : Expr t) {ops i s} ->
-              ⟨ comp e ops , i , s ⟩ ◁∞ Matches⁺ ops s e i
+bar-thm : forall {t} (e : Expr t) {ops i s} ->
+          ⟨ comp e ops , i , s ⟩ ◁∞″ Matches⁺ ops s e i
hunk ./CompilerCorrectness/BarTheorem.agda 47
-bar-theorem {t = t} ⌜ nat n ⌝ ~ via (, push) helper₁
+bar-thm {t = t} ⌜ nat n ⌝ ~ via (, push) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 54
-bar-theorem {t = t} ⌜ throw ⌝ ~ via (, throw) helper₁
+bar-thm {t = t} ⌜ throw ⌝ ~ via (, throw) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 61
-bar-theorem (x ⊕ y) ~ ◁∞-trans (bar-theorem x) helper₁
+bar-thm (x ⊕ y) ~ ◁∞′-trans (bar-thm x) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 69
-  helper₅ nat ~ via (, nat) helper₆
+  helper₅ nat ~ ↑ via (, nat) helper₆
hunk ./CompilerCorrectness/BarTheorem.agda 81
-  helper₃ _  _  interrupt ~ via (, nat) helper₅
+  helper₃ _  _  interrupt ~ ↑ via (, nat) helper₅
hunk ./CompilerCorrectness/BarTheorem.agda 87
-  helper₂ x↡ (returns y↡) ~ via (, add) (helper₃ x↡ y↡)
-  helper₂ x↡ (throws y↯)  ~ via (, nat) (helper₄ x↡ y↯)
+  helper₂ x↡ (returns y↡) ~ ↑ via (, add) (helper₃ x↡ y↡)
+  helper₂ x↡ (throws y↯)  ~ ↑ via (, nat) (helper₄ x↡ y↯)
hunk ./CompilerCorrectness/BarTheorem.agda 94
-  helper₁ (returns x↡) ~ ◁∞-trans (bar-theorem y) (helper₂ x↡)
+  helper₁ (returns x↡) ~ ↑ ◁∞′-trans (bar-thm y) (helper₂ x↡)
hunk ./CompilerCorrectness/BarTheorem.agda 96
-bar-theorem (x >> y) ~ ◁∞-trans (bar-theorem x) helper₁
+bar-thm (x >> y) ~ ◁∞′-trans (bar-thm x) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 112
-  helper₂ x↡ pop       ~ ◁∞-trans (bar-theorem y) (helper₃ x↡)
-  helper₂ _  interrupt ~ via (, nat) helper₄
+  helper₂ x↡ pop       ~ ↑ ◁∞′-trans (bar-thm y) (helper₃ x↡)
+  helper₂ _  interrupt ~ ↑ via (, nat) helper₄
hunk ./CompilerCorrectness/BarTheorem.agda 119
-  helper₁ (returns x↡) ~ via (, pop) (helper₂ x↡)
+  helper₁ (returns x↡) ~ ↑ via (, pop) (helper₂ x↡)
hunk ./CompilerCorrectness/BarTheorem.agda 121
-bar-theorem (x catch y) ~ via (, mark) helper₁
+bar-thm (x catch y) ~ via (, mark) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 138
-  helper₇ x↯ (returns y↡) ~ via (, reset) (helper₈ x↯ y↡)
-  helper₇ x↯ (throws  y↯) ~ via (, int)   (helper₉ x↯ y↯)
+  helper₇ x↯ (returns y↡) ~ ↑ via (, reset) (helper₈ x↯ y↡)
+  helper₇ x↯ (throws  y↯) ~ ↑ via (, int)   (helper₉ x↯ y↯)
hunk ./CompilerCorrectness/BarTheorem.agda 145
-  helper₆ x↯ han ~ ◁∞-trans (bar-theorem y) (helper₇ x↯)
+  helper₆ x↯ han ~ ↑ ◁∞′-trans (bar-thm y) (helper₇ x↯)
hunk ./CompilerCorrectness/BarTheorem.agda 149
-            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ◁∞
+            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ◁∞′
hunk ./CompilerCorrectness/BarTheorem.agda 151
-  helper₅ x↯ ~ via (, han) (helper₆ x↯)
+  helper₅ x↯ ~ ↑ via (, han) (helper₆ x↯)
hunk ./CompilerCorrectness/BarTheorem.agda 164
-  helper₃ _  interrupt ~ via (, nat) helper₄
+  helper₃ _  interrupt ~ ↑ via (, nat) helper₄
hunk ./CompilerCorrectness/BarTheorem.agda 170
-  helper₂ (returns x↡) ~ via (, unmark) (helper₃ x↡)
+  helper₂ (returns x↡) ~ ↑ via (, unmark) (helper₃ x↡)
hunk ./CompilerCorrectness/BarTheorem.agda 177
-  helper₁ mark      ~ ◁∞-trans (bar-theorem x) helper₂
+  helper₁ mark      ~ ↑ ◁∞′-trans (bar-thm x) helper₂
hunk ./CompilerCorrectness/BarTheorem.agda 180
-bar-theorem (block x) ~ via (, set) helper₁
+bar-thm (block x) ~ via (, set) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 196
-  helper₂ (returns x↡) ~ via (, reset) (helper₃ x↡)
-  helper₂ (throws  x↯) ~ via (, int)   (helper₄ x↯)
+  helper₂ (returns x↡) ~ ↑ via (, reset) (helper₃ x↡)
+  helper₂ (throws  x↯) ~ ↑ via (, int)   (helper₄ x↯)
hunk ./CompilerCorrectness/BarTheorem.agda 202
-  helper₁ set       ~ ◁∞-trans (bar-theorem x) helper₂
+  helper₁ set       ~ ↑ ◁∞′-trans (bar-thm x) helper₂
hunk ./CompilerCorrectness/BarTheorem.agda 205
-bar-theorem (unblock x) ~ via (, set) helper₁
+bar-thm (unblock x) ~ via (, set) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 214
-            ⟪ U , int i ∷ s ⟫ ◁∞ (Matches⁺ ops s (unblock x) i)
-  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 226
-  helper₃ _  interrupt ~ via (, nat) helper₄
+  helper₃ _  interrupt ~ ↑ via (, nat) helper₄
hunk ./CompilerCorrectness/BarTheorem.agda 231
-  helper₂ (returns x↡) ~ via (, reset) (helper₃ x↡)
+  helper₂ (returns x↡) ~ ↑ via (, reset) (helper₃ x↡)
hunk ./CompilerCorrectness/BarTheorem.agda 237
-  helper₁ set       ~ ◁∞-trans (bar-theorem x) helper₂
+  helper₁ set       ~ ↑ ◁∞′-trans (bar-thm x) helper₂
hunk ./CompilerCorrectness/BarTheorem.agda 240
-bar-theorem (loop x) ~ via (, loop) helper₁
+bar-thm (loop x) ~ via (, loop) helper₁
hunk ./CompilerCorrectness/BarTheorem.agda 250
-  helper₃ x↡ pop       ~ bar-theorem (loop x)
-  helper₃ _  interrupt ~ via (, nat) helper₄
+  helper₃ x↡ pop       ~ ↑ bar-thm (loop x)
+  helper₃ _  interrupt ~ ↑ via (, nat) helper₄
hunk ./CompilerCorrectness/BarTheorem.agda 257
-  helper₂ (returns x↡) ~ via (, pop) (helper₃ x↡)
+  helper₂ (returns x↡) ~ ↑ via (, pop) (helper₃ x↡)
hunk ./CompilerCorrectness/BarTheorem.agda 261
-  helper₁ loop      ~ ◁∞-trans (bar-theorem x) helper₂
+  helper₁ loop      ~ ↑ ◁∞′-trans (bar-thm x) helper₂
hunk ./CompilerCorrectness/BarTheorem.agda 264
+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)
+