[Made loop take an argument. Nils Anders Danielsson **20080626114103 + This makes some proofs more realistic. + Note that some proofs now fail to pass the productivity checker. They are productive, though (as far as I can tell). ] hunk ./AlgebraicProperties.agda 171 - with _⊑_.⇓ (_≈_.⊒ (assoc ⌜ nat 0 ⌝ (loop catch ⌜ nat 0 ⌝) ⌜ nat 0 ⌝)) + with _⊑_.⇓ (_≈_.⊒ (assoc ⌜ nat 0 ⌝ (loop ⌜ nat 0 ⌝ catch ⌜ nat 0 ⌝) ⌜ nat 0 ⌝)) hunk ./AlgebraicProperties.agda 176 -... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₁ ()))))) Val) -... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₂ () _))))) Val) +... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₁ ↡))))) Val) = loop-¬⇓ nat-¬↯ (, ↡) +... | Block (Seqn₁ (Catch₁ (Unblock (Block (Seqn₁ (Catch₁ (Unblock Val)) (Catch₂ ↯ _))))) Val) = loop-¬⇓ nat-¬↯ (, ↯) hunk ./AlgebraicProperties.agda 230 - with _⊑_.⇓ (_≈_.⊑ (⊕-comm ⌜ throw ⌝ loop)) {i = B} (Add₂ Val) -... | Add₂ () -... | Add₃ () _ + with _⊑_.⇓ (_≈_.⊑ (⊕-comm ⌜ throw ⌝ (loop ⌜ nat 0 ⌝))) + {i = B} (Add₂ Val) +... | Add₂ ↡ = loop-¬⇓ nat-¬↯ (, ↡) +... | Add₃ ↯ _ = loop-¬⇓ nat-¬↯ (, ↯) hunk ./CompilerCorrectness.agda 15 +open import Data.Colist hunk ./CompilerCorrectness/BarTheorem.agda 31 -Matches⁺⇒Matches ._ (returns ⇓) = returns ⇓ +Matches⁺⇒Matches ._ (returns ↡) = returns ↡ hunk ./CompilerCorrectness/BarTheorem.agda 42 --- 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. +-- The bar theorem, written in continuation-passing style. + +-- TODO: Convince the productivity checker that this definition is +-- productive. hunk ./CompilerCorrectness/BarTheorem.agda 51 -bar-thm {t = t} ⌜ nat n ⌝ κ ~ via (_ , push) (helper₁ κ) +bar-thm {t = t} ⌜ nat n ⌝ κ ~ via (, push) (helper₁ κ) hunk ./CompilerCorrectness/BarTheorem.agda 59 -bar-thm {t = t} ⌜ throw ⌝ κ ~ via (_ , throw) (helper₁ κ) +bar-thm {t = t} ⌜ throw ⌝ κ ~ via (, throw) (helper₁ κ) hunk ./CompilerCorrectness/BarTheorem.agda 77 - helper₅ κ nat ~ via (_ , nat) (helper₆ κ) + helper₅ κ nat ~ via (, nat) (helper₆ κ) hunk ./CompilerCorrectness/BarTheorem.agda 83 - helper₄ κ x⇓ y↯ nat ~ κ (throws (Add₃ x⇓ y↯)) + helper₄ κ x↡ y↯ nat ~ κ (throws (Add₃ x↡ y↯)) hunk ./CompilerCorrectness/BarTheorem.agda 89 - helper₃ κ x⇓ y⇓ add ~ κ (returns (Add₁ x⇓ y⇓)) - helper₃ κ _ _ interrupt ~ via (_ , nat) (helper₅ κ) + helper₃ κ x↡ y↡ add ~ κ (returns (Add₁ x↡ y↡)) + helper₃ κ _ _ interrupt ~ via (, nat) (helper₅ κ) hunk ./CompilerCorrectness/BarTheorem.agda 96 - 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 103 - helper₁ κ (returns x⇓) ~ bar-thm y (helper₂ κ x⇓) + helper₁ κ (returns x↡) ~ bar-thm y (helper₂ κ x↡) hunk ./CompilerCorrectness/BarTheorem.agda 116 - helper₃ κ x⇓ (returns y⇓) ~ κ (returns (Seqn₁ x⇓ y⇓)) - helper₃ κ x⇓ (throws y↯) ~ κ (throws (Seqn₁ x⇓ y↯)) + helper₃ κ x↡ (returns y↡) ~ κ (returns (Seqn₁ x↡ y↡)) + helper₃ κ x↡ (throws y↯) ~ κ (throws (Seqn₁ x↡ y↯)) hunk ./CompilerCorrectness/BarTheorem.agda 123 - helper₂ κ x⇓ pop ~ bar-thm y (helper₃ κ x⇓) - helper₂ κ _ interrupt ~ via (_ , nat) (helper₄ κ) + helper₂ κ x↡ pop ~ bar-thm y (helper₃ κ x↡) + helper₂ κ _ interrupt ~ via (, nat) (helper₄ κ) hunk ./CompilerCorrectness/BarTheorem.agda 130 - helper₁ κ (returns x⇓) ~ via (_ , pop) (helper₂ κ x⇓) + helper₁ κ (returns x↡) ~ via (, pop) (helper₂ κ x↡) hunk ./CompilerCorrectness/BarTheorem.agda 132 -bar-thm (x catch y) κ ~ via (_ , mark) (helper₁ κ) +bar-thm (x catch y) κ ~ via (, mark) (helper₁ κ) hunk ./CompilerCorrectness/BarTheorem.agda 144 - helper₈ κ x↯ y⇓ reset ~ κ (returns (Catch₂ x↯ y⇓)) + helper₈ κ x↯ y↡ reset ~ κ (returns (Catch₂ x↯ y↡)) hunk ./CompilerCorrectness/BarTheorem.agda 150 - 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 163 - helper₅ κ x↯ ~ via (_ , han) (helper₆ κ x↯) + helper₅ κ x↯ ~ via (, han) (helper₆ κ x↯) hunk ./CompilerCorrectness/BarTheorem.agda 175 - helper₃ κ x⇓ unmark ~ κ (returns (Catch₁ x⇓)) - helper₃ κ _ interrupt ~ via (_ , nat) (helper₄ κ) + helper₃ κ x↡ unmark ~ κ (returns (Catch₁ x↡)) + helper₃ κ _ interrupt ~ via (, nat) (helper₄ κ) hunk ./CompilerCorrectness/BarTheorem.agda 182 - helper₂ κ (returns x⇓) ~ via (_ , unmark) (helper₃ κ x⇓) + helper₂ κ (returns x↡) ~ via (, unmark) (helper₃ κ x↡) hunk ./CompilerCorrectness/BarTheorem.agda 192 -bar-thm (block x) κ ~ via (_ , set) (helper₁ κ) +bar-thm (block x) κ ~ via (, set) (helper₁ κ) hunk ./CompilerCorrectness/BarTheorem.agda 204 - helper₃ κ x⇓ reset ~ κ (returns (Block x⇓)) + helper₃ κ x↡ reset ~ κ (returns (Block x↡)) hunk ./CompilerCorrectness/BarTheorem.agda 209 - 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 218 -bar-thm (unblock x) κ ~ via (_ , set) (helper₁ κ) +bar-thm (unblock x) κ ~ via (, set) (helper₁ κ) hunk ./CompilerCorrectness/BarTheorem.agda 230 - helper₅ κ x↯ ~ via (_ , int) (helper₆ κ x↯) + helper₅ κ x↯ ~ via (, int) (helper₆ κ x↯) hunk ./CompilerCorrectness/BarTheorem.agda 241 - helper₃ κ x⇓ reset ~ κ (returns (Unblock x⇓)) - helper₃ κ _ interrupt ~ via (_ , nat) (helper₄ κ) + helper₃ κ x↡ reset ~ κ (returns (Unblock x↡)) + helper₃ κ _ interrupt ~ via (, nat) (helper₄ κ) hunk ./CompilerCorrectness/BarTheorem.agda 247 - helper₂ κ (returns x⇓) ~ via (_ , reset) (helper₃ κ x⇓) + helper₂ κ (returns x↡) ~ via (, reset) (helper₃ κ x↡) hunk ./CompilerCorrectness/BarTheorem.agda 256 -bar-thm loop κ ~ via (_ , loop) (helper₁ ≡-refl κ) +bar-thm (loop x) κ ~ via (, loop) (helper₁ κ) hunk ./CompilerCorrectness/BarTheorem.agda 258 - 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) + 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 i m s P} -> + Cont (Matches⁺ ops s (loop x) i) P -> + x ⇓[ i ] nat m -> + 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↡) + + 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) hunk ./CompilerCorrectness/Completeness.agda 30 +code-nonempty (loop x) ops = []≢∷ hunk ./CompilerCorrectness/Completeness.agda 36 -code-nonempty loop ops = []≢∷ hunk ./CompilerCorrectness/Completeness.agda 42 - complete⇓ : forall {t} {e : Expr t} {ops i s n} -> + complete↡ : forall {t} {e : Expr t} {ops i s n} -> hunk ./CompilerCorrectness/Completeness.agda 45 - complete⇓ Val = push ◅ ε - complete⇓ (Add₁ x y) = complete⇓ x ◅◅ complete⇓ y ◅◅ add ◅ ε - complete⇓ (Seqn₁ x y) = complete⇓ x ◅◅ pop ◅ complete⇓ y - complete⇓ (Catch₁ x) = mark ◅ complete⇓ x ◅◅ unmark ◅ ε - complete⇓ (Catch₂ x y) = mark ◅ complete↯ x ◅◅ han ◅ complete⇓ y ◅◅ + complete↡ Val = push ◅ ε + complete↡ (Loop l) = loop ◅ complete↡ l + complete↡ (Add₁ x y) = complete↡ x ◅◅ complete↡ y ◅◅ add ◅ ε + complete↡ (Seqn₁ x y) = complete↡ x ◅◅ pop ◅ complete↡ y + complete↡ (Catch₁ x) = mark ◅ complete↡ x ◅◅ unmark ◅ ε + complete↡ (Catch₂ x y) = mark ◅ complete↯ x ◅◅ han ◅ complete↡ y ◅◅ hunk ./CompilerCorrectness/Completeness.agda 52 - complete⇓ (Block x) = set ◅ complete⇓ x ◅◅ reset ◅ ε - complete⇓ (Unblock x) = set ◅ complete⇓ x ◅◅ reset ◅ ε + complete↡ (Block x) = set ◅ complete↡ x ◅◅ reset ◅ ε + complete↡ (Unblock x) = set ◅ complete↡ x ◅◅ reset ◅ ε hunk ./CompilerCorrectness/Completeness.agda 58 + complete↯ (Loop l) = loop ◅ complete↯ l hunk ./CompilerCorrectness/Completeness.agda 60 - complete↯ (Add₃ x y) = complete⇓ x ◅◅ complete↯ y ◅◅ nat ◅ ε - complete↯ (Seqn₁ x y) = complete⇓ x ◅◅ pop ◅ complete↯ y + complete↯ (Add₃ x y) = complete↡ x ◅◅ complete↯ y ◅◅ nat ◅ ε + complete↯ (Seqn₁ x y) = complete↡ x ◅◅ pop ◅ complete↯ y hunk ./CompilerCorrectness/Completeness.agda 74 -complete₁ e (returns ⇓) = complete⇓ ⇓ +complete₁ e (returns ↡) = complete↡ ↡ hunk ./CompilerCorrectness/Completeness.agda 77 +-- TODO: Convince the productivity checker that this definition is +-- productive. + hunk ./CompilerCorrectness/Completeness.agda 84 -complete⇑ (Add₂ x y) ~ complete⇓ (proj₂ x) ◅◅∞ complete⇑ y +complete⇑ (Add₂ x y) ~ complete↡ (proj₂ x) ◅◅∞ complete⇑ y hunk ./CompilerCorrectness/Completeness.agda 86 -complete⇑ (Seqn₂ x y) ~ complete⇓ (proj₂ x) ◅◅∞ pop ◅∞ complete⇑ y +complete⇑ (Seqn₂ x y) ~ complete↡ (proj₂ x) ◅◅∞ pop ◅∞ complete⇑ y hunk ./Semantics/BigStep.agda 25 + Loop : forall {x v i} ( ⇓ : x >> loop x ⇓[ i ] v) -> loop x ⇓[ i ] v hunk ./Semantics/BigStep.agda 57 - Loop : forall {i} (loop⇑ : loop ⇑[ i ]) -> loop ⇑[ i ] + Loop : forall {x i} ( ⇑ : x >> loop x ⇑[ i ]) -> loop x ⇑[ i ] hunk ./Semantics/BigStep.agda 67 -loop⇑ : forall {i} -> loop ⇑[ i ] -loop⇑ ~ Loop loop⇑ - hunk ./Semantics/Equivalence.agda 13 +open import Totality hunk ./Semantics/Equivalence.agda 51 +big⇒small⇓ (Loop {x = x} {v} ⇓) = begin + run (loop (x ˢ)) ⟶⟨ Red Loop ⟩ + run (x ˢ >> run (loop (x ˢ))) ⟶⋆⟨ big⇒small⇓ ⇓ ⟩ + done v ∎ hunk ./Semantics/Equivalence.agda 99 +-- TODO: Convince the productivity checker that this definition is +-- productive. + hunk ./Semantics/Equivalence.agda 179 -small⇒big⟶ʳ⇓ Val ⇓ = ⇓ -small⇒big⟶ʳ⇓ Loop ⇓ = ⇓ -small⇒big⟶ʳ⇓ Add₁ Val = Add₁ Val Val -small⇒big⟶ʳ⇓ Add₁ Int = Int -small⇒big⟶ʳ⇓ Add₂ Val = Add₂ Val -small⇒big⟶ʳ⇓ Add₂ Int = Int -small⇒big⟶ʳ⇓ Add₃ Val = Add₃ Val Val -small⇒big⟶ʳ⇓ Add₃ Int = Int -small⇒big⟶ʳ⇓ Seqn₁ ⇓ = Seqn₁ Val ⇓ -small⇒big⟶ʳ⇓ Seqn₂ Val = Seqn₂ Val -small⇒big⟶ʳ⇓ Seqn₂ Int = Int -small⇒big⟶ʳ⇓ Catch₁ Val = Catch₁ Val -small⇒big⟶ʳ⇓ Catch₁ Int = Int -small⇒big⟶ʳ⇓ Catch₂ Val = Catch₂ Val Val -small⇒big⟶ʳ⇓ Catch₂ Int = Int -small⇒big⟶ʳ⇓ Block Val = Block Val -small⇒big⟶ʳ⇓ Block Int = Int -small⇒big⟶ʳ⇓ Unblock Val = Unblock Val -small⇒big⟶ʳ⇓ Unblock Int = Int -small⇒big⟶ʳ⇓ (Int int) Val = Int -small⇒big⟶ʳ⇓ (Int int) Int = Int +small⇒big⟶ʳ⇓ Val ⇓ = ⇓ +small⇒big⟶ʳ⇓ Loop (Seqn₁ x↡ y⇓) = y⇓ +small⇒big⟶ʳ⇓ Loop (Seqn₂ x↯) = Loop (Seqn₂ x↯) +small⇒big⟶ʳ⇓ Loop Int = Int +small⇒big⟶ʳ⇓ Add₁ Val = Add₁ Val Val +small⇒big⟶ʳ⇓ Add₁ Int = Int +small⇒big⟶ʳ⇓ Add₂ Val = Add₂ Val +small⇒big⟶ʳ⇓ Add₂ Int = Int +small⇒big⟶ʳ⇓ Add₃ Val = Add₃ Val Val +small⇒big⟶ʳ⇓ Add₃ Int = Int +small⇒big⟶ʳ⇓ Seqn₁ ⇓ = Seqn₁ Val ⇓ +small⇒big⟶ʳ⇓ Seqn₂ Val = Seqn₂ Val +small⇒big⟶ʳ⇓ Seqn₂ Int = Int +small⇒big⟶ʳ⇓ Catch₁ Val = Catch₁ Val +small⇒big⟶ʳ⇓ Catch₁ Int = Int +small⇒big⟶ʳ⇓ Catch₂ Val = Catch₂ Val Val +small⇒big⟶ʳ⇓ Catch₂ Int = Int +small⇒big⟶ʳ⇓ Block Val = Block Val +small⇒big⟶ʳ⇓ Block Int = Int +small⇒big⟶ʳ⇓ Unblock Val = Unblock Val +small⇒big⟶ʳ⇓ Unblock Int = Int +small⇒big⟶ʳ⇓ (Int int) Val = Int +small⇒big⟶ʳ⇓ (Int int) Int = Int hunk ./Semantics/Equivalence.agda 249 -small⇒big⟶∞ (run ⌜ v ⌝) i (Red Val ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞) -small⇒big⟶∞ (run ⌜ v ⌝) .U (Red (Int int) ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞) -small⇒big⟶∞ (run loop) i ⟶∞ ¬⇑ = ¬⇑ loop⇑ -small⇒big⟶∞ (run (x ⊕ y)) i ⟶∞ ¬⇑ = Add.lemma ⟶∞ helper +small⇒big⟶∞ (run ⌜ v ⌝) i (Red Val ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞) +small⇒big⟶∞ (run ⌜ v ⌝) .U (Red (Int int) ◅∞ ⟶∞) ¬⇑ = ⊥-elim (done↛∞ ⟶∞) +small⇒big⟶∞ (run (loop x)) i ⟶∞ ¬⇑ = Loop.lemma ⟶∞ helper + where + helper : x ⟶∞[ i ] ⊎ ∃ (\n -> x ⟶⋆[ i ] done (nat n)) -> ⊥ + helper (inj₁ x⟶∞) = small⇒big⟶∞ x i x⟶∞ (¬⇑ ∘ Loop ∘ Seqn₁) + helper (inj₂ (n , x⟶⋆n)) = ¬⇑ (loop-⇑ (n , small⇒big⟶⋆ x⟶⋆n)) +small⇒big⟶∞ (run (x ⊕ y)) i ⟶∞ ¬⇑ = Add.lemma ⟶∞ helper hunk ./Semantics/Equivalence/Lemmas.agda 44 - lemma {x = x} {y} {i} x⊕y⟶∞ = - map-¬¬ helper $ reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₁ x⊕y⟶∞)) + lemma {x = x} {y} {i} ⟶∞ = + map-¬¬ helper $ reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₁ ⟶∞)) hunk ./Semantics/Equivalence/Lemmas.agda 67 - lemma {x = x} {y} {i} x⊕y⟶∞ = - map-¬¬ helper $ reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₁ x⊕y⟶∞)) + lemma {x = x} {y} {i} ⟶∞ = + map-¬¬ helper $ reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₁ ⟶∞)) hunk ./Semantics/Equivalence/Lemmas.agda 97 - lemma {x = x} {y} {i} x⊕y⟶∞ = - map-¬¬ helper $ reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₁ x⊕y⟶∞)) + lemma {x = x} {y} {i} ⟶∞ = + map-¬¬ helper $ reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₁ ⟶∞)) hunk ./Semantics/Equivalence/Lemmas.agda 120 +module Loop where + + Pred : Status -> Exprˢ partial -> Set + Pred i = \x -> ∃ \n -> x ≡ done (nat n) + + helper₂ : forall {y i x} -> Seqn.Pred y i x -> Pred i x + helper₂ (n , eq , _) = (n , eq) + + helper₁ : forall {x i} -> + run (loop x) ⟶∞[ i ] -> x ⟶⋆∞[ i ] Pred i + helper₁ (Red Loop ◅∞ ⟶∞) = map⋆∞ id id helper₂ (Seqn.helper₁ ⟶∞) + helper₁ (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞) + + lemma : forall {x i} -> + run (loop x) ⟶∞[ i ] -> + ¬ ¬ (x ⟶∞[ i ] ⊎ ∃ \n -> (x ⟶⋆[ i ] done (nat n))) + lemma {x = x} {i} ⟶∞ = + map-¬¬ helper $ reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₁ ⟶∞)) + where + helper : ∃ (\z -> (x ⟶⋆[ i ] z) × Pred i z) ⊎ x ⟶∞[ i ] -> _ + helper (inj₁ (.(done (nat n)) , x⟶⋆n , n , ≡-refl)) = inj₂ (n , x⟶⋆n) + helper (inj₂ x⟶∞) = inj₁ x⟶∞ + hunk ./Semantics/SmallStep.agda 34 - loop : Exprˢ' partial + loop : Exprˢ partial -> Exprˢ' partial hunk ./Semantics/SmallStep.agda 52 - loop ˢ' = loop + loop x ˢ' = loop (x ˢ) hunk ./Semantics/SmallStep.agda 71 - loop ˢ'⁻¹ = loop + loop x ˢ'⁻¹ = loop (x ˢ⁻¹) hunk ./Semantics/SmallStep.agda 93 - interruptible' loop = true + interruptible' (loop x) = true hunk ./Semantics/SmallStep.agda 118 - Loop : forall {i} -> run loop ⟶ʳ[ i ] run loop + Loop : forall {i x} -> run (loop x) ⟶ʳ[ i ] run (x >> run (loop x)) hunk ./Semantics/SmallStep.agda 182 -loop ˢ-interruptible = _ +loop x ˢ-interruptible = _ hunk ./Semantics/SmallStep.agda 193 -left-inverse loop = ≡-refl +left-inverse (loop x) = ≡-cong loop (left-inverse x) hunk ./Semantics/SmallStep.agda 208 -run⟶ loop = (, Red Loop) +run⟶ (loop x) = (, Red Loop) hunk ./Semantics/SmallStep/StepGroups.agda 35 - size' loop = 0 + size' (loop x) = size x hunk ./StatusLemmas.agda 20 +Bto·⇓ (Loop ⇓) = Loop (Bto·⇓ ⇓) hunk ./StatusLemmas.agda 63 -¬UtoB' UtoB' with UtoB' (loop catch ⌜ nat 0 ⌝) (0 , Catch₂ Int Val) -... | (n , Catch₁ ()) -... | (n , Catch₂ () _) +¬UtoB' UtoB' + with UtoB' (loop ⌜ nat 0 ⌝ catch ⌜ nat 0 ⌝) (0 , Catch₂ Int Val) +... | (n , Catch₁ ⇓) = loop-¬⇓ nat-¬↯ (nat n , ⇓) +... | (n , Catch₂ (Loop (Seqn₁ _ ↯)) _) = loop-¬⇓ nat-¬↯ (throw , ↯) +... | (n , Catch₂ (Loop (Seqn₂ ())) _) hunk ./Syntax.agda 33 - loop : Expr partial + loop : Expr partial -> Expr partial hunk ./Totality.agda 15 +-- Some properties of loop. + +loop-⇑ : forall {x i} -> x ↡[ i ] -> loop x ⇑[ i ] +loop-⇑ x↡ ~ Loop (Seqn₂ x↡ (loop-⇑ x↡)) + +loop-¬⇓ : forall {x} -> ¬ x ↯[ B ] -> ¬ loop x ⇓[ B ] +loop-¬⇓ ¬x↯ (v , Loop (Seqn₁ _ ⇓)) = loop-¬⇓ ¬x↯ (v , ⇓) +loop-¬⇓ ¬x↯ (.throw , Loop (Seqn₂ x↯)) = ¬x↯ x↯ + +loop-¬↡ : forall {x i} -> ¬ loop x ↡[ i ] +loop-¬↡ (n , Loop (Seqn₁ x↡ y⇓)) = loop-¬↡ (n , y⇓) + +-- A utility function. + +nat-¬↯ : forall {n t} -> ¬ ⌜_⌝ {t = t} (nat n) ↯[ B ] +nat-¬↯ () + hunk ./Totality.agda 35 -¬defined ⇓ with ⇓ loop B -... | (_ , ()) +¬defined ⇓ = loop-¬⇓ nat-¬↯ (⇓ (loop ⌜ nat 0 ⌝) B) hunk ./Totality.agda 88 -can-throw? ⌜ nat m ⌝ B = no helper - where - helper : ¬ ⌜ nat m ⌝ ↯[ B ] - helper () +can-throw? ⌜ nat m ⌝ B = no nat-¬↯ hunk ./Totality.agda 133 - helper : ¬ ⌜ throw ⌝ ↡[ i ] + helper : ¬ ⌜_⌝ {t = total} throw ↡[ i ] hunk ./VirtualMachine.agda 5 +-- To avoid having to deal with labels/jumps this virtual machine is +-- non-standard in several ways: +-- +-- • Instructions can contain instruction sequences. +-- • Instructions can contain uncompiled expressions. +-- • The virtual machine invokes the compiler. + hunk ./VirtualMachine.agda 32 - loop : Inst + loop : Expr partial -> Inst hunk ./VirtualMachine.agda 59 -data _⟶_ : State -> State -> Set where - push : forall {n ops i s} -> - ⟨ push n ∷ ops , i , s ⟩ ⟶ ⟨ ops , i , nat n ∷ s ⟩ - throw : forall {ops i s} -> - ⟨ throw ∷ ops , i , s ⟩ ⟶ ⟪ i , s ⟫ - loop : forall {ops i s} -> - ⟨ loop ∷ ops , i , s ⟩ ⟶ ⟨ loop ∷ ops , i , s ⟩ - add : forall {ops i m n s} -> - ⟨ add ∷ ops , i , nat n ∷ nat m ∷ s ⟩ ⟶ - ⟨ ops , i , nat (m + n) ∷ s ⟩ - pop : forall {ops i n s} -> - ⟨ pop ∷ ops , i , nat n ∷ s ⟩ ⟶ ⟨ ops , i , s ⟩ - mark : forall {ops' ops i s} -> - ⟨ mark ops' ∷ ops , i , s ⟩ ⟶ ⟨ ops , i , han ops' ∷ s ⟩ - unmark : forall {ops i x c s} -> - ⟨ unmark ∷ ops , i , x ∷ han c ∷ s ⟩ ⟶ ⟨ ops , i , x ∷ s ⟩ - set : forall {i' ops i s} -> - ⟨ set i' ∷ ops , i , s ⟩ ⟶ ⟨ ops , i' , int i ∷ s ⟩ - reset : forall {ops i x i' s} -> - ⟨ reset ∷ ops , i , x ∷ int i' ∷ s ⟩ ⟶ - ⟨ ops , i' , x ∷ s ⟩ +mutual hunk ./VirtualMachine.agda 61 - interrupt : forall {op ops s} -> - ⟨ op ∷ ops , U , s ⟩ ⟶ ⟪ U , s ⟫ + data _⟶_ : State -> State -> Set where + push : forall {n ops i s} -> ⟨ push n ∷ ops , i , s ⟩ ⟶ ⟨ ops , i , nat n ∷ s ⟩ + add : forall {ops i m n s} -> ⟨ add ∷ ops , i , nat n ∷ nat m ∷ s ⟩ ⟶ ⟨ ops , i , nat (m + n) ∷ s ⟩ + pop : forall {ops i n s} -> ⟨ pop ∷ ops , i , nat n ∷ s ⟩ ⟶ ⟨ ops , i , s ⟩ + mark : forall {ops' ops i s} -> ⟨ mark ops' ∷ ops , i , s ⟩ ⟶ ⟨ ops , i , han ops' ∷ s ⟩ + unmark : forall {ops i x c s} -> ⟨ unmark ∷ ops , i , x ∷ han c ∷ s ⟩ ⟶ ⟨ ops , i , x ∷ s ⟩ + set : forall {i' ops i s} -> ⟨ set i' ∷ ops , i , s ⟩ ⟶ ⟨ ops , i' , int i ∷ s ⟩ + reset : forall {ops i x i' s} -> ⟨ reset ∷ ops , i , x ∷ int i' ∷ s ⟩ ⟶ ⟨ ops , i' , x ∷ s ⟩ + loop : forall {x ops i s} -> ⟨ loop x ∷ ops , i , s ⟩ ⟶ ⟨ comp x (pop ∷ loop x ∷ ops) , i , s ⟩ + throw : forall {ops i s} -> ⟨ throw ∷ ops , i , s ⟩ ⟶ ⟪ i , s ⟫ hunk ./VirtualMachine.agda 72 - nat : forall {i n s} -> - ⟪ i , nat n ∷ s ⟫ ⟶ ⟪ i , s ⟫ - int : forall {i i' s} -> - ⟪ i , int i' ∷ s ⟫ ⟶ ⟪ i' , s ⟫ - han : forall {i ops s} -> - ⟪ i , han ops ∷ s ⟫ ⟶ ⟨ ops , B , int i ∷ s ⟩ + interrupt : forall {op ops s} -> ⟨ op ∷ ops , U , s ⟩ ⟶ ⟪ U , s ⟫ hunk ./VirtualMachine.agda 74 ------------------------------------------------------------------------- --- Compiler + nat : forall {i n s} -> ⟪ i , nat n ∷ s ⟫ ⟶ ⟪ i , s ⟫ + int : forall {i i' s} -> ⟪ i , int i' ∷ s ⟫ ⟶ ⟪ i' , s ⟫ + han : forall {i ops s} -> ⟪ i , han ops ∷ s ⟫ ⟶ ⟨ ops , B , int i ∷ s ⟩ hunk ./VirtualMachine.agda 78 --- Compiler from the high-level language to the virtual machine --- language. + -- Compiler from the high-level language to the virtual machine + -- language. hunk ./VirtualMachine.agda 81 -comp : forall {t} -> Expr t -> Code -> Code -comp ⌜ nat n ⌝ ops = push n ∷ ops -comp ⌜ throw ⌝ ops = throw ∷ ops -comp loop ops = loop ∷ ops -comp (x ⊕ y) ops = comp x (comp y (add ∷ ops)) -comp (x >> y) ops = comp x (pop ∷ comp y ops) -comp (x catch y) ops = mark (comp y (reset ∷ ops)) ∷ comp x (unmark ∷ ops) -comp (block x) ops = set B ∷ comp x (reset ∷ ops) -comp (unblock x) ops = set U ∷ comp x (reset ∷ ops) + comp : forall {t} -> Expr t -> Code -> Code + comp ⌜ nat n ⌝ ops = push n ∷ ops + comp ⌜ throw ⌝ ops = throw ∷ ops + comp (loop x) ops = loop x ∷ ops + comp (x ⊕ y) ops = comp x (comp y (add ∷ ops)) + comp (x >> y) ops = comp x (pop ∷ comp y ops) + comp (x catch y) ops = mark (comp y (reset ∷ ops)) ∷ comp x (unmark ∷ ops) + comp (block x) ops = set B ∷ comp x (reset ∷ ops) + comp (unblock x) ops = set U ∷ comp x (reset ∷ ops)