[Simplified the method used to make bar-thm pass the productivity checker. Nils Anders Danielsson **20080717231227 + It is now very similar to the method used by complete⇑. ] hunk ./Bar.agda 17 -open import Infinite hiding (∞′→∞; ∞″→∞; ∞→∞′) +open import Infinite hiding (∞′→∞; ∞″→∞; ∞″→∞′; ∞→∞′) hunk ./Bar.agda 127 - ↑_ : x ◁∞″ P -> x ◁∞′ P + via : (x⟶ : x ⟶) (x⟶y◁∞P : forall {y} -> x ⟶ y -> y ◁∞″ P) -> + x ◁∞′ P hunk ./Bar.agda 131 - via : (x⟶ : x ⟶) (x⟶y◁∞P : forall {y} -> x ⟶ y -> y ◁∞′ P) -> - x ◁∞″ P + ↓_ : (x◁∞P : x ◁∞′ P) -> x ◁∞″ P hunk ./Bar.agda 134 - (Q◁∞P : forall {y} -> y ∈ Q -> y ◁∞′ P) -> + (Q◁∞P : forall {y} -> y ∈ Q -> y ◁∞″ P) -> hunk ./Bar.agda 137 --- 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. +-- The first constructor can be accessed in finite time. hunk ./Bar.agda 139 -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) +∞″→∞′ : forall {x P} -> x ◁∞″ P -> x ◁∞′ P +∞″→∞′ (↓ x◁∞P) = x◁∞P +∞″→∞′ (◁∞′-trans x◁∞Q Q◁∞P) with ∞″→∞′ x◁∞Q +∞″→∞′ (◁∞′-trans x◁∞Q Q◁∞P) | directly x∈P = ∞″→∞′ (Q◁∞P x∈P) +∞″→∞′ (◁∞′-trans x◁∞Q Q◁∞P) | via x⟶ x⟶y◁∞P = + via x⟶ (\x⟶y -> ◁∞′-trans (x⟶y◁∞P x⟶y) Q◁∞P) hunk ./Bar.agda 151 - ∞′→∞ (directly x∈P) ~ directly 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 ./Bar.agda 155 - ∞″→∞ 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)) + ∞″→∞ x◁∞P ~ ∞′→∞ (∞″→∞′ x◁∞P) hunk ./Bar.agda 159 -∞→∞′ (via x⟶ x⟶y◁∞P) ~ ↑ via x⟶ (\x⟶y -> ∞→∞′ (x⟶y◁∞P x⟶y)) +∞→∞′ (via x⟶ x⟶y◁∞P) ~ via x⟶ (\x⟶y -> ↓ ∞→∞′ (x⟶y◁∞P x⟶y)) hunk ./CompilerCorrectness/BarTheorem.agda 37 -P ∋◁∞ Q = forall {y} -> y ∈ P -> y ◁∞′ Q +P ∋◁∞ Q = forall {y} -> y ∈ P -> y ◁∞″ Q hunk ./CompilerCorrectness/BarTheorem.agda 47 -bar-thm {t = t} ⌜ nat n ⌝ ~ via (, push) helper₁ +bar-thm {t = t} ⌜ nat n ⌝ ~ ↓ via (, push) helper₁ hunk ./CompilerCorrectness/BarTheorem.agda 51 - helper₁ push ~ directly (returns Val) - helper₁ interrupt ~ directly (throws Int) + helper₁ push ~ ↓ directly (returns Val) + helper₁ interrupt ~ ↓ directly (throws Int) hunk ./CompilerCorrectness/BarTheorem.agda 54 -bar-thm {t = t} ⌜ throw ⌝ ~ via (, throw) helper₁ +bar-thm {t = t} ⌜ throw ⌝ ~ ↓ via (, throw) helper₁ hunk ./CompilerCorrectness/BarTheorem.agda 58 - helper₁ throw ~ directly (throws Val) - helper₁ interrupt ~ directly (throws Int) + helper₁ throw ~ ↓ directly (throws Val) + helper₁ interrupt ~ ↓ directly (throws Int) hunk ./CompilerCorrectness/BarTheorem.agda 65 - helper₆ nat ~ directly (throws Int) + helper₆ nat ~ ↓ directly (throws Int) hunk ./CompilerCorrectness/BarTheorem.agda 69 - helper₅ nat ~ ↑ via (, nat) helper₆ + helper₅ nat ~ ↓ via (, nat) helper₆ hunk ./CompilerCorrectness/BarTheorem.agda 74 - helper₄ x↡ y↯ nat ~ directly (throws (Add₃ x↡ y↯)) + helper₄ x↡ y↯ nat ~ ↓ directly (throws (Add₃ x↡ y↯)) hunk ./CompilerCorrectness/BarTheorem.agda 80 - helper₃ x↡ y↡ add ~ directly (returns (Add₁ x↡ y↡)) - helper₃ _ _ interrupt ~ ↑ via (, nat) helper₅ + helper₃ x↡ y↡ add ~ ↓ directly (returns (Add₁ x↡ y↡)) + 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 93 - helper₁ (throws x↯) ~ directly (throws (Add₂ x↯)) - helper₁ (returns x↡) ~ ↑ ◁∞′-trans (bar-thm y) (helper₂ x↡) + helper₁ (throws x↯) ~ ↓ directly (throws (Add₂ x↯)) + helper₁ (returns x↡) ~ ◁∞′-trans (bar-thm y) (helper₂ x↡) hunk ./CompilerCorrectness/BarTheorem.agda 100 - helper₄ nat ~ directly (throws Int) + helper₄ nat ~ ↓ directly (throws Int) hunk ./CompilerCorrectness/BarTheorem.agda 105 - helper₃ x↡ (returns y↡) ~ directly (returns (Seqn₁ x↡ y↡)) - helper₃ x↡ (throws y↯) ~ directly (throws (Seqn₁ x↡ y↯)) + helper₃ x↡ (returns y↡) ~ ↓ directly (returns (Seqn₁ x↡ y↡)) + helper₃ x↡ (throws y↯) ~ ↓ directly (throws (Seqn₁ x↡ y↯)) hunk ./CompilerCorrectness/BarTheorem.agda 112 - helper₂ x↡ pop ~ ↑ ◁∞′-trans (bar-thm 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 118 - helper₁ (throws x↯) ~ directly (throws (Seqn₂ x↯)) - helper₁ (returns x↡) ~ ↑ via (, pop) (helper₂ x↡) + 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-thm (x catch y) ~ ↓ via (, mark) helper₁ hunk ./CompilerCorrectness/BarTheorem.agda 126 - helper₉ x↯ y↯ int ~ directly (throws (Catch₂ x↯ y↯)) + helper₉ x↯ y↯ int ~ ↓ directly (throws (Catch₂ x↯ y↯)) hunk ./CompilerCorrectness/BarTheorem.agda 132 - helper₈ x↯ y↡ reset ~ directly (returns (Catch₂ x↯ y↡)) + helper₈ x↯ y↡ reset ~ ↓ directly (returns (Catch₂ x↯ y↡)) 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-thm 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 163 - helper₃ x↡ unmark ~ directly (returns (Catch₁ x↡)) - helper₃ _ interrupt ~ ↑ via (, nat) helper₄ + helper₃ x↡ unmark ~ ↓ directly (returns (Catch₁ x↡)) + 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-thm x) helper₂ - helper₁ interrupt ~ directly (throws Int) + helper₁ mark ~ ◁∞′-trans (bar-thm x) helper₂ + helper₁ interrupt ~ ↓ directly (throws Int) hunk ./CompilerCorrectness/BarTheorem.agda 180 -bar-thm (block x) ~ via (, set) helper₁ +bar-thm (block x) ~ ↓ via (, set) helper₁ hunk ./CompilerCorrectness/BarTheorem.agda 185 - helper₄ x↯ int ~ directly (throws (Block x↯)) + helper₄ x↯ int ~ ↓ directly (throws (Block x↯)) hunk ./CompilerCorrectness/BarTheorem.agda 191 - helper₃ x↡ reset ~ directly (returns (Block x↡)) + helper₃ x↡ reset ~ ↓ directly (returns (Block x↡)) 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-thm x) helper₂ - helper₁ interrupt ~ directly (throws Int) + helper₁ set ~ ◁∞′-trans (bar-thm x) helper₂ + helper₁ interrupt ~ ↓ directly (throws Int) hunk ./CompilerCorrectness/BarTheorem.agda 205 -bar-thm (unblock x) ~ via (, set) helper₁ +bar-thm (unblock x) ~ ↓ via (, set) helper₁ hunk ./CompilerCorrectness/BarTheorem.agda 210 - helper₆ x↯ int ~ directly (throws (Unblock x↯)) + helper₆ x↯ int ~ ↓ directly (throws (Unblock x↯)) 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 225 - helper₃ x↡ reset ~ directly (returns (Unblock x↡)) - helper₃ _ interrupt ~ ↑ via (, nat) helper₄ + helper₃ x↡ reset ~ ↓ directly (returns (Unblock x↡)) + 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-thm x) helper₂ - helper₁ interrupt ~ directly (throws Int) + helper₁ set ~ ◁∞′-trans (bar-thm x) helper₂ + helper₁ interrupt ~ ↓ directly (throws Int) hunk ./CompilerCorrectness/BarTheorem.agda 240 -bar-thm (loop x) ~ via (, loop) helper₁ +bar-thm (loop x) ~ ↓ via (, loop) helper₁ hunk ./CompilerCorrectness/BarTheorem.agda 244 - helper₄ nat ~ directly (throws Int) + helper₄ nat ~ ↓ directly (throws Int) hunk ./CompilerCorrectness/BarTheorem.agda 250 - helper₃ x↡ pop ~ ↑ bar-thm (loop x) - helper₃ _ interrupt ~ ↑ via (, nat) helper₄ + helper₃ x↡ pop ~ bar-thm (loop x) + helper₃ _ interrupt ~ ↓ via (, nat) helper₄ hunk ./CompilerCorrectness/BarTheorem.agda 256 - helper₂ (throws x↯) ~ directly (throws (Loop (Seqn₂ x↯))) - helper₂ (returns x↡) ~ ↑ via (, pop) (helper₃ x↡) + helper₂ (throws x↯) ~ ↓ directly (throws (Loop (Seqn₂ x↯))) + helper₂ (returns x↡) ~ ↓ via (, pop) (helper₃ x↡) hunk ./CompilerCorrectness/BarTheorem.agda 261 - helper₁ loop ~ ↑ ◁∞′-trans (bar-thm x) helper₂ - helper₁ interrupt ~ directly (throws Int) + helper₁ loop ~ ◁∞′-trans (bar-thm x) helper₂ + helper₁ interrupt ~ ↓ directly (throws Int)