[Improved the small-step semantics. Nils Anders Danielsson **20080618114042 + I have now almost managed to prove that the small- and big-step semantics are equivalent. However, it seems as if I need a slightly smarter setup in order to make the last component of the proof productive. ] hunk ./CompilerCorrectness.agda 10 -import Bar; open Bar _⟶_ -import Infinite; open Infinite _⟶_ +import Bar; open Bar _⟶_ +open import Infinite hunk ./CompilerCorrectness.agda 26 +-- "Infinite closure". + +_⟶∞ : State -> Set +_⟶∞ = Infinite _⟶_ + hunk ./CompilerCorrectness/BarTheorem.agda 259 -bar-theorem loop ¬⇑ = ⊥-elim (¬⇑ Loop) +bar-theorem loop ¬⇑ = ⊥-elim (¬⇑ loop⇑) hunk ./CompilerCorrectness/Completeness.agda 11 -import Infinite; open Infinite _⟶_ +open import Infinite hunk ./CompilerCorrectness/Completeness.agda 77 -complete⇑ Loop ~ loop loops +complete⇑ (Loop l) ~ loop ◅∞ complete⇑ l hunk ./CompilerCorrectness/Soundness.agda 10 +open import Semantics.BigStep hunk ./CompilerCorrectness/Soundness.agda 14 -import Infinite; open Infinite _⟶_ hunk ./CompilerCorrectness/Soundness.agda 16 +open import Relation.Binary.PropositionalEquality hunk ./CompilerCorrectness/Soundness.agda 26 - sound₂' : forall {t} (e : Expr t) {i} -> start e i ⟶∞ -> e ⟶∞[ i ] + sound₂' : forall {t} (e : Expr t) {i} -> start e i ⟶∞ -> e ˢ ⟶∞[ i ] hunk ./CompilerCorrectness/Soundness.agda 29 -sound₂ e e⟶∞ = small⇒big⟶∞ e (sound₂' e e⟶∞) +sound₂ e {i} e⟶∞ = + ≡-subst (\x -> x ⇑[ i ]) (left-inverse e) + (small⇒big⟶∞ (sound₂' e e⟶∞)) hunk ./Everything.agda 27 -import Semantics.Equivalence -- Currently contains postulate. +import Semantics.Equivalence -- Currently does not pass the productivity checker. hunk ./Infinite.agda 17 - _◅∞_ : forall {y} -> x ⟶ y -> Infinite _⟶_ y -> Infinite _⟶_ x + _◅∞_ : forall {y} + (x⟶y : x ⟶ y) (y⟶∞ : Infinite _⟶_ y) -> Infinite _⟶_ x hunk ./Semantics/BigStep.agda 33 - Int : forall {t x} -> t ∶ x ⇓[ U ] throw hunk ./Semantics/BigStep.agda 35 + Int : forall {t x} -> t ∶ x ⇓[ U ] throw hunk ./Semantics/BigStep.agda 57 - Loop : forall {i} -> loop ⇑[ i ] + Loop : forall {i} (loop⇑ : loop ⇑[ i ]) -> loop ⇑[ i ] hunk ./Semantics/BigStep.agda 67 +loop⇑ : forall {i} -> loop ⇑[ i ] +loop⇑ ~ Loop loop⇑ + hunk ./Semantics/Equivalence.agda 7 -open import Syntax hiding (⌜_⌝) +open import Syntax hunk ./Semantics/Equivalence.agda 11 -open ⟶-Infinite -open import StatusLemmas +open import Infinite hunk ./Semantics/Equivalence.agda 13 -open import Data.Nat hunk ./Semantics/Equivalence.agda 15 -open import Data.Function -open import Data.Empty -open import Relation.Binary.PropositionalEquality +open import Data.Nat hunk ./Semantics/Equivalence.agda 23 - e ⇓[ i ] v -> Σ₀ \j -> annotate e i ⟶⋆ ⌜ v ⌝ ^ j + e ⇓[ i ] v -> e ˢ ⟶⋆[ i ] done v hunk ./Semantics/Equivalence.agda 26 - e ⇑[ i ] -> annotate e i ⟶∞ + e ⇑[ i ] -> e ˢ ⟶∞[ i ] hunk ./Semantics/Equivalence.agda 30 - ⟶⋆ : forall {t} (e : Expr t) {i j} v -> - annotate e i ⟶⋆ ⌜ v ⌝ ^ j -> e ⇓[ i ] v + ⟶⋆ : forall {t} {e : Exprˢ t} {i} v -> + e ⟶⋆[ i ] done v -> e ˢ⁻¹ ⇓[ i ] v hunk ./Semantics/Equivalence.agda 33 - ⟶∞ : forall {t} {e : Expr t} {i} -> - annotate e i ⟶∞ -> e ⇑[ i ] + ⟶∞ : forall {t} {e : Exprˢ t} {i} -> + e ⟶∞[ i ] -> e ˢ⁻¹ ⇑[ i ] hunk ./Semantics/Equivalence.agda 40 - e ⇓[ i ] v -> Σ₀ \j -> annotate e i ⟶⋆ ⌜ v ⌝ ^ j -big⇒small⇓ (Val {n = n} {i}) = i , (begin val n ^ i ∎) -big⇒small⇓ (Throw {i = i}) = i , (begin throw ^ i ∎) -big⇒small⇓ (Add₁ {x = x} {y} {m} {n} {i} x⇓ y⇓) = i , (begin - annotate x i ⊕ annotate y i ^ i - ⟶⋆⟨ lift⟶⋆ (• •⊕ annotate y i ^ i) (proj₂ $ big⇒small⇓ x⇓) ⟩ - (val m ^ _) ⊕ annotate y i ^ i - ⟶⋆⟨ lift⟶⋆ (val m ^ _ ⊕• • ^ i) (proj₂ $ big⇒small⇓ y⇓) ⟩ - (val m ^ _) ⊕ (val n ^ _) ^ i - ⟶⟨ reduction • Add₁ ⟩ - val (m + n) ^ i - ∎) -big⇒small⇓ (Add₂ {x = x} {y} {i} x↯) = i , (begin - annotate x i ⊕ annotate y i ^ i - ⟶⋆⟨ lift⟶⋆ (• •⊕ annotate y i ^ i) (proj₂ $ big⇒small⇓ x↯) ⟩ - (throw ^ _) ⊕ annotate y i ^ i - ⟶⟨ reduction • Add₂ ⟩ - throw ^ i - ∎) -big⇒small⇓ (Add₃ {x = x} {y} {m} {i} x⇓ y↯) = i , (begin - annotate x i ⊕ annotate y i ^ i - ⟶⋆⟨ lift⟶⋆ (• •⊕ annotate y i ^ i) (proj₂ $ big⇒small⇓ x⇓) ⟩ - (val m ^ _) ⊕ annotate y i ^ i - ⟶⋆⟨ lift⟶⋆ (val m ^ _ ⊕• • ^ i) (proj₂ $ big⇒small⇓ y↯) ⟩ - (val m ^ _) ⊕ (throw ^ _) ^ i - ⟶⟨ reduction • Add₃ ⟩ - throw ^ i - ∎) -big⇒small⇓ (Seqn₁ {x = x} {y} {m} {v} {i} x⇓ y⇒) = _ , (begin - annotate x i >> y ^ i - ⟶⋆⟨ lift⟶⋆ (• •>> y ^ i) (proj₂ $ big⇒small⇓ x⇓) ⟩ - (val m ^ _) >> y ^ i - ⟶⟨ reduction • Seqn₁ ⟩ - annotate y i - ⟶⋆⟨ proj₂ $ big⇒small⇓ y⇒ ⟩ - ⌜ v ⌝ ^ _ - ∎) -big⇒small⇓ (Seqn₂ {x = x} {y} {i} x↯) = _ , (begin - annotate x i >> y ^ i - ⟶⋆⟨ lift⟶⋆ (• •>> y ^ i) (proj₂ $ big⇒small⇓ x↯) ⟩ - (throw ^ _) >> y ^ i - ⟶⟨ reduction • Seqn₂ ⟩ - throw ^ _ - ∎) -big⇒small⇓ (Catch₁ {x = x} {y} {m} {i} x⇓) = _ , (begin - annotate x i catch y ^ i - ⟶⋆⟨ lift⟶⋆ (• •catch y ^ i) (proj₂ $ big⇒small⇓ x⇓) ⟩ - (val m ^ _) catch y ^ i - ⟶⟨ reduction • Catch₁ ⟩ - val m ^ _ - ∎) -big⇒small⇓ (Catch₂ {x = x} {y} {v} {i} x↯ y⇒) = _ , (begin - annotate x i catch y ^ i - ⟶⋆⟨ lift⟶⋆ (• •catch y ^ i) (proj₂ $ big⇒small⇓ x↯) ⟩ - (throw ^ _) catch y ^ i - ⟶⟨ reduction • Catch₂ ⟩ - annotate y B - ⟶⋆⟨ proj₂ $ big⇒small⇓ y⇒ ⟩ - ⌜ v ⌝ ^ _ - ∎) -big⇒small⇓ (Int {x = x}) = B , (begin - annotate x U - ⟶⟨ reduction • Int ⟩ - throw ^ B - ∎) -big⇒small⇓ (Block {x = x} {v} {i} x⇒) = _ , (begin - block x ^ i - ⟶⟨ reduction • Block ⟩ - annotate x B - ⟶⋆⟨ proj₂ $ big⇒small⇓ x⇒ ⟩ - ⌜ v ⌝ ^ _ - ∎) -big⇒small⇓ (Unblock {x = x} {v} {i} x⇒) = _ , (begin - unblock x ^ i - ⟶⟨ reduction • Unblock ⟩ - annotate x U - ⟶⋆⟨ proj₂ $ big⇒small⇓ x⇒ ⟩ - ⌜ v ⌝ ^ _ - ∎) + e ⇓[ i ] v -> e ˢ ⟶⋆[ i ] done v +big⇒small⇓ (Val {n = n}) = begin + run (val n) ⟶⟨ Red • Val ⟩ + done (val n) ∎ +big⇒small⇓ Throw = begin + run throw ⟶⟨ Red • Throw ⟩ + done throw ∎ +big⇒small⇓ (Add₁ {x = x} {y} {m} {n} x⇓ y⇓) = begin + run (x ˢ ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |⊕| > y ˢ) (big⇒small⇓ x⇓) ⟩ + run (done (val m) ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (val m ⊕• •) (big⇒small⇓ y⇓) ⟩ + run (done (val m) ⊕ done (val n)) ⟶⟨ Red • Add₁ ⟩ + done (val (m + n)) ∎ +big⇒small⇓ (Add₂ {x = x} {y} x↯) = begin + run (x ˢ ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |⊕| > y ˢ) (big⇒small⇓ x↯) ⟩ + run (done throw ⊕ y ˢ) ⟶⟨ Red • Add₂ ⟩ + done throw ∎ +big⇒small⇓ (Add₃ {x = x} {y} {m} x⇓ y↯) = begin + run (x ˢ ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |⊕| > y ˢ) (big⇒small⇓ x⇓) ⟩ + run (done (val m) ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (val m ⊕• •) (big⇒small⇓ y↯) ⟩ + run (done (val m) ⊕ done throw) ⟶⟨ Red • Add₃ ⟩ + done throw ∎ +big⇒small⇓ (Seqn₁ {x = x} {y} {m} {v} x⇓ y⇒) = begin + run (x ˢ >> y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |>>| > y ˢ) (big⇒small⇓ x⇓) ⟩ + run (done (val m) >> y ˢ) ⟶⟨ Red • Seqn₁ ⟩ + y ˢ ⟶⋆⟨ big⇒small⇓ y⇒ ⟩ + done v ∎ +big⇒small⇓ (Seqn₂ {x = x} {y} x↯) = begin + run (x ˢ >> y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |>>| > y ˢ) (big⇒small⇓ x↯) ⟩ + run (done throw >> y ˢ) ⟶⟨ Red • Seqn₂ ⟩ + done throw ∎ +big⇒small⇓ (Catch₁ {x = x} {y} {m} x⇓) = begin + run (x ˢ catch y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |catch| > y ˢ) (big⇒small⇓ x⇓) ⟩ + run (done (val m) catch y ˢ) ⟶⟨ Red • Catch₁ ⟩ + done (val m) ∎ +big⇒small⇓ (Catch₂ {x = x} {y} {v} x↯ y⇒) = begin + run (x ˢ catch y ˢ) ⟶⋆⟨ lift⟶⋆ (• •< |catch| > y ˢ) (big⇒small⇓ x↯) ⟩ + run (done throw catch y ˢ) ⟶⋆⟨ lift⟶⋆ (handler• •) (big⇒small⇓ y⇒) ⟩ + run (done throw catch done v) ⟶⟨ Red • Catch₂ ⟩ + done v ∎ +big⇒small⇓ (Int {x = x}) = begin + x ˢ ⟶⟨ Red • (Int (x ˢ-interruptible)) ⟩ + done throw ∎ +big⇒small⇓ (Block {x = x} {v} x⇒) = begin + run (block (x ˢ)) ⟶⋆⟨ lift⟶⋆ (block• •) (big⇒small⇓ x⇒) ⟩ + run (block (done v)) ⟶⟨ Red • Block ⟩ + done v ∎ +big⇒small⇓ (Unblock {x = x} {v} x⇒) = begin + run (unblock (x ˢ)) ⟶⋆⟨ lift⟶⋆ (unblock• •) (big⇒small⇓ x⇒) ⟩ + run (unblock (done v)) ⟶⟨ Red • Unblock ⟩ + done v ∎ hunk ./Semantics/Equivalence.agda 91 -big⇒small⇑ : forall {t} {e : Expr t} {i} -> e ⇑[ i ] -> annotate e i ⟶∞ -big⇒small⇑ Loop ~ reduction • Loop loops -big⇒small⇑ (Add₁ x⇑) ~ lift⟶∞ (• •⊕ _ ^ _) (big⇒small⇑ x⇑) -big⇒small⇑ (Add₂ (_ , x⇓) y⇑) ~ lift⟶⋆ (• •⊕ _ ^ _) (proj₂ $ big⇒small⇓ x⇓) +big⇒small⇑ : forall {t} {e : Expr t} {i} -> e ⇑[ i ] -> e ˢ ⟶∞[ i ] +big⇒small⇑ (Loop loop⇑) ~ Red • Loop ◅∞ big⇒small⇑ loop⇑ +big⇒small⇑ (Add₁ x⇑) ~ lift⟶∞ (• •< |⊕| > _) (big⇒small⇑ x⇑) +big⇒small⇑ (Add₂ (_ , x⇓) y⇑) ~ lift⟶⋆ (• •< |⊕| > _) (big⇒small⇓ x⇓) hunk ./Semantics/Equivalence.agda 96 - lift⟶∞ (val _ ^ _ ⊕• • ^ _) (big⇒small⇑ y⇑) -big⇒small⇑ (Seqn₁ x⇑) ~ lift⟶∞ (• •>> _ ^ _) (big⇒small⇑ x⇑) -big⇒small⇑ (Seqn₂ (_ , x⇓) y⇑) ~ lift⟶⋆ (• •>> _ ^ _) (proj₂ $ big⇒small⇓ x⇓) + lift⟶∞ (val _ ⊕• •) (big⇒small⇑ y⇑) +big⇒small⇑ (Seqn₁ x⇑) ~ lift⟶∞ (• •< |>>| > _) (big⇒small⇑ x⇑) +big⇒small⇑ (Seqn₂ (_ , x⇓) y⇑) ~ lift⟶⋆ (• •< |>>| > _) (big⇒small⇓ x⇓) hunk ./Semantics/Equivalence.agda 100 - reduction • Seqn₁ + Red • Seqn₁ hunk ./Semantics/Equivalence.agda 103 -big⇒small⇑ (Catch₁ x⇑) ~ lift⟶∞ (• •catch _ ^ _) (big⇒small⇑ x⇑) -big⇒small⇑ (Catch₂ x↯ y⇑) ~ lift⟶⋆ (• •catch _ ^ _) (proj₂ $ big⇒small⇓ x↯) +big⇒small⇑ (Catch₁ x⇑) ~ lift⟶∞ (• •< |catch| > _) (big⇒small⇑ x⇑) +big⇒small⇑ (Catch₂ x↯ y⇑) ~ lift⟶⋆ (• •< |catch| > _) (big⇒small⇓ x↯) hunk ./Semantics/Equivalence.agda 106 - reduction • Catch₂ - ◅∞ - big⇒small⇑ y⇑ -big⇒small⇑ (Block x⇑) ~ reduction • Block ◅∞ big⇒small⇑ x⇑ -big⇒small⇑ (Unblock x⇑) ~ reduction • Unblock ◅∞ big⇒small⇑ x⇑ + lift⟶∞ (handler• •) (big⇒small⇑ y⇑) +big⇒small⇑ (Block x⇑) ~ lift⟶∞ (block• •) (big⇒small⇑ x⇑) +big⇒small⇑ (Unblock x⇑) ~ lift⟶∞ (unblock• •) (big⇒small⇑ x⇑) hunk ./Semantics/Equivalence.agda 116 -simplify⇓ : forall {t} {x : Expr t} {i v} -> - unannotate (annotate x i) i ⇓[ i ] v -> x ⇓[ i ] v -simplify⇓ {x = x} {i = i} {v = v} = - ≡-subst (\x -> x ⇓[ i ] v) (left-inverse x i) - -simplify⇓' : forall {t} {x : Expr t} {i v} -> - unannotate' (annotate' x i) i ⇓[ i ] v -> x ⇓[ i ] v -simplify⇓' {x = x} {i = i} {v = v} = - ≡-subst (\x -> x ⇓[ i ] v) (left-inverse' x i) - -module A where - - -- lemma : forall {t} v i j {k} -> unannotate {t} (⌜ v ⌝ ^ i) j ⇓[ k ] v - -- lemma (val n) U U = Val - -- lemma (val n) U B = Unblock Val - -- lemma (val n) B U = Block Val - -- lemma (val n) B B = Val - -- lemma throw U U = Throw - -- lemma throw U B = Unblock Throw - -- lemma throw B U = Block Throw - -- lemma throw B B = Throw - - -- small⇒big⟶ʳ' : forall {t} {e₁ e₂ : AnnExpr' t} {v i₁ i₂} -> - -- e₁ ^ i₁ ⟶ʳ e₂ ^ i₂ -> - -- unannotate' e₂ i₂ ⇓[ i₂ ] v -> - -- unannotate' e₁ i₁ ⇓[ i₁ ] v - -- small⇒big⟶ʳ' Loop ⇓ = ⇓ - -- small⇒big⟶ʳ' (Add₁ {i = i} {j} {k} {m} {n}) Val = Add₁ (lemma (val m) j i) (lemma (val n) k i) - -- small⇒big⟶ʳ' Add₁ Int = Int - -- small⇒big⟶ʳ' (Add₂ {i = i} {j}) Throw = Add₂ (lemma throw j i) - -- small⇒big⟶ʳ' Add₂ Int = Int - -- small⇒big⟶ʳ' (Add₃ {i = i} {j} {k} {m}) Throw = Add₃ (lemma (val m) j i) (lemma throw k i) - -- small⇒big⟶ʳ' Add₃ Int = Int - -- small⇒big⟶ʳ' (Seqn₁ {i = i} {j} {m}) ⇓ = Seqn₁ (lemma (val m) j i) (simplify⇓' ⇓) - -- small⇒big⟶ʳ' (Seqn₂ {i = i} {j}) Throw = Seqn₂ (lemma throw j i) - -- small⇒big⟶ʳ' Seqn₂ Int = Int - -- small⇒big⟶ʳ' (Catch₁ {i = i} {j} {m}) Val = Catch₁ (lemma (val m) j i) - -- small⇒big⟶ʳ' Catch₁ Int = Int - -- small⇒big⟶ʳ' (Catch₂ {i = i} {j}) ⇓ = Catch₂ (lemma throw j i) (simplify⇓' ⇓) - -- small⇒big⟶ʳ' Int Throw = Int - -- small⇒big⟶ʳ' Block ⇓ = Block (simplify⇓' ⇓) - -- small⇒big⟶ʳ' Unblock ⇓ = Unblock (simplify⇓' ⇓) - - -- small⇒big⟶ʳ : forall {t} i (e₁ e₂ : AnnExpr t) {v} -> - -- e₁ ⟶ʳ e₂ -> - -- unannotate e₂ (status e₂) ⇓[ status e₂ ] v -> - -- unannotate e₁ i ⇓[ i ] v - -- small⇒big⟶ʳ U (e₁ ^ U) (e₂ ^ U) r ⇓ = small⇒big⟶ʳ' r ⇓ - -- small⇒big⟶ʳ B (e₁ ^ U) (e₂ ^ U) r ⇓ = Unblock (small⇒big⟶ʳ' r ⇓) - -- small⇒big⟶ʳ U (e₁ ^ B) (e₂ ^ U) r ⇓ = Block (small⇒big⟶ʳ' r ⇓) - -- small⇒big⟶ʳ B (e₁ ^ B) (e₂ ^ U) r ⇓ = small⇒big⟶ʳ' r ⇓ - -- small⇒big⟶ʳ U (e₁ ^ U) (e₂ ^ B) r ⇓ = small⇒big⟶ʳ' r ⇓ - -- small⇒big⟶ʳ B (e₁ ^ U) (e₂ ^ B) r ⇓ = Unblock (small⇒big⟶ʳ' r ⇓) - -- small⇒big⟶ʳ U (e₁ ^ B) (e₂ ^ B) r ⇓ = Block (small⇒big⟶ʳ' r ⇓) - -- small⇒big⟶ʳ B (e₁ ^ B) (e₂ ^ B) r ⇓ = small⇒big⟶ʳ' r ⇓ - - -- small⇒big⟶ : forall {t} (E : EvalCtxt t) {i₁ e₁ e₂ v} -> - -- e₁ ⟶ʳ e₂ -> - -- unannotate (E [ e₂ ]) (status (E [ e₂ ])) ⇓[ status (E [ e₂ ]) ] v -> - -- unannotate (E [ e₁ ]) i₁ ⇓[ i₁ ] v - -- small⇒big⟶ • r ⇓ = small⇒big⟶ʳ _ _ _ r ⇓ - -- small⇒big⟶ (E •⊕ y ^ U) {U} r (Add₁ x↡ y↡) = Add₁ (small⇒big⟶ E r {!x↡ !}) y↡ - -- small⇒big⟶ (E •⊕ y ^ U) {B} r (Add₁ x↡ y↡) = Unblock (Add₁ (small⇒big⟶ E r {!x↡ !}) y↡) - -- small⇒big⟶ (E •⊕ y ^ U) r (Add₂ x↯) = {! !} - -- small⇒big⟶ (E •⊕ y ^ U) r (Add₃ x↡ y↯) = {! !} - -- small⇒big⟶ (E •⊕ y ^ U) r Int = {! !} - -- small⇒big⟶ (E •⊕ y ^ B) r ⇓ = {! !} - -- small⇒big⟶ (E •>> y ^ i) r ⇓ = {! !} - -- small⇒big⟶ (E •catch y ^ i) r ⇓ = {! !} - -- small⇒big⟶ (val n ^ j ⊕• E ^ i) r ⇓ = {! !} - - lemma₂ : forall {t} (e : AnnExpr t) i {v} -> - unannotate e i ⇓[ i ] v -> - unannotate e (status e) ⇓[ status e ] v - lemma₂ (x ^ U) U ⇓ = ⇓ - lemma₂ (x ^ B) U Int = {! !} - lemma₂ (x ^ B) U (Block ⇓) = ⇓ - lemma₂ (x ^ U) B (Unblock ⇓) = ⇓ - lemma₂ (x ^ B) B ⇓ = ⇓ - - lemma₃ : forall {t} (e : AnnExpr t) i {v} -> - unannotate e (status e) ⇓[ status e ] v -> - unannotate e i ⇓[ i ] v - lemma₃ (e ^ U) U ⇓ = ⇓ - lemma₃ (e ^ B) U ⇓ = Block ⇓ - lemma₃ (e ^ U) B ⇓ = Unblock ⇓ - lemma₃ (e ^ B) B ⇓ = ⇓ - - small⇒big⟶ : forall {t} (E : EvalCtxt t) {e₁ e₂ v} -> - e₁ ⟶ʳ e₂ -> - unannotate (E [ e₂ ]) (status (E [ e₂ ])) ⇓[ status (E [ e₂ ]) ] v -> - unannotate (E [ e₁ ]) (status (E [ e₁ ])) ⇓[ status (E [ e₁ ]) ] v - small⇒big⟶ • r ⇓ = {! !} -- small⇒big⟶ʳ _ _ r ⇓ - small⇒big⟶ (E •⊕ y ^ U) r (Add₁ x↡ y↡) = Add₁ (lemma₃ {! !} {! !} {! !}) y↡ -- Add₁ {!small⇒big⟶ E r x↡ !} y↡ - small⇒big⟶ (E •⊕ y ^ U) r (Add₂ x↯) = Add₂ (lemma₃ {! !} _ (small⇒big⟶ E r (lemma₂ _ _ x↯)) ) - small⇒big⟶ (E •⊕ y ^ U) r (Add₃ x↡ y↯) = {! !} - small⇒big⟶ (E •⊕ y ^ U) r Int = Int - small⇒big⟶ (E •⊕ y ^ B) r ⇓ = {! !} - small⇒big⟶ (E •>> y ^ i) r ⇓ = {! !} - small⇒big⟶ (E •catch y ^ i) r ⇓ = {! !} - small⇒big⟶ (val n ^ j ⊕• E ^ i) r ⇓ = {! !} +-- First note that we can map over combinations of evaluation contexts +-- and the big-step relations. hunk ./Semantics/Equivalence.agda 119 - -- small⇒big⟶ : forall {t} (E : EvalCtxt t) {e₁ e₂ i₁ i₂ v} -> - -- e₁ ⟶ʳ e₂ -> - -- unannotate (E [ e₂ ]) i₂ ⇓[ i₂ ] v -> - -- unannotate (E [ e₁ ]) i₁ ⇓[ i₁ ] v - -- small⇒big⟶ • r ⇓ = ? -- small⇒big⟶ʳ _ _ r ⇓ - -- small⇒big⟶ (E •⊕ y ^ U) r (Add₁ x↡ y↡) = Add₁ {!small⇒big⟶ E r x↡ !} y↡ - -- small⇒big⟶ (E •⊕ y ^ U) r (Add₂ x↯) = Add₂ {! !} - -- small⇒big⟶ (E •⊕ y ^ U) r (Add₃ x↡ y↯) = {! !} - -- small⇒big⟶ (E •⊕ y ^ U) r Int = Int - -- small⇒big⟶ (E •⊕ y ^ B) r ⇓ = {! !} - -- small⇒big⟶ (E •>> y ^ i) r ⇓ = {! !} - -- small⇒big⟶ (E •catch y ^ i) r ⇓ = {! !} - -- small⇒big⟶ (val n ^ j ⊕• E ^ i) r ⇓ = {! !} +map⇓ : forall {t} {x₁ x₂ : Exprˢ t} {i j v} (E : EvalCtxt t i j) -> + (forall {v} -> x₁ ˢ⁻¹ ⇓[ i ] v -> x₂ ˢ⁻¹ ⇓[ i ] v) -> + E [ x₁ ] ˢ⁻¹ ⇓[ j ] v -> E [ x₂ ] ˢ⁻¹ ⇓[ j ] v +map⇓ • f ⇓ = f ⇓ +map⇓ (E •< |⊕| > y) f (Add₁ x↡ y↡) = Add₁ (map⇓ E f x↡) y↡ +map⇓ (E •< |⊕| > y) f (Add₂ x↯) = Add₂ (map⇓ E f x↯) +map⇓ (E •< |⊕| > y) f (Add₃ x↡ y↯) = Add₃ (map⇓ E f x↡) y↯ +map⇓ (E •< |⊕| > y) f Int = Int +map⇓ (E •< |>>| > y) f (Seqn₁ x↡ y⇓) = Seqn₁ (map⇓ E f x↡) y⇓ +map⇓ (E •< |>>| > y) f (Seqn₂ x↯) = Seqn₂ (map⇓ E f x↯) +map⇓ (E •< |>>| > y) f Int = Int +map⇓ (E •< |catch| > y) f (Catch₁ x↡) = Catch₁ (map⇓ E f x↡) +map⇓ (E •< |catch| > y) f (Catch₂ x↯ y⇓) = Catch₂ (map⇓ E f x↯) y⇓ +map⇓ (E •< |catch| > y) f Int = Int +map⇓ (val m ⊕• E) f (Add₁ x↡ y↡) = Add₁ x↡ (map⇓ E f y↡) +map⇓ (val m ⊕• E) f (Add₂ x↯) = Add₂ x↯ +map⇓ (val m ⊕• E) f (Add₃ x↡ y↯) = Add₃ x↡ (map⇓ E f y↯) +map⇓ (val m ⊕• E) f Int = Int +map⇓ (handler• E) f (Catch₁ ()) +map⇓ (handler• E) f (Catch₂ x↯ y⇓) = Catch₂ x↯ (map⇓ E f y⇓) +map⇓ (handler• E) f Int = Int +map⇓ (block• E) f (Block x⇓) = Block (map⇓ E f x⇓) +map⇓ (block• E) f Int = Int +map⇓ (unblock• E) f (Unblock x⇓) = Unblock (map⇓ E f x⇓) +map⇓ (unblock• E) f Int = Int hunk ./Semantics/Equivalence.agda 145 - -- small⇒big⟶ (E •⊕ y ^ i) r (Add₁ x↡ y↡) = Add₁ {!small⇒big⟶ E r x↡ !} y↡ - -- small⇒big⟶ (E •⊕ y ^ i) r (Add₂ x↯) = Add₂ {! !} -- small⇒big⟶ E r x↯ - -- small⇒big⟶ (E •⊕ y ^ i) r (Add₃ x↡ y↯) = Add₃ {! !} y↯ -- small⇒big⟶ E r x↡ - -- small⇒big⟶ (E •⊕ y ^ .U) r Int = Int - -- small⇒big⟶ (E •>> y ^ i) r (Seqn₁ x↡ y⇓) = Seqn₁ {! !} y⇓ -- small⇒big⟶ E r x↡ - -- small⇒big⟶ (E •>> y ^ i) r (Seqn₂ x↯) = Seqn₂ {! !} -- small⇒big⟶ E r x↯ - -- small⇒big⟶ (E •>> y ^ .U) r Int = Int - -- small⇒big⟶ (E •catch y ^ i) r (Catch₁ x↡) = Catch₁ {! !} -- small⇒big⟶ E r x↡ - -- small⇒big⟶ (E •catch y ^ i) r (Catch₂ x↯ y⇓) = Catch₂ {! !} y⇓ -- small⇒big⟶ E r x↯ - -- small⇒big⟶ (E •catch y ^ .U) r Int = Int - -- small⇒big⟶ (val n ^ j ⊕• E ^ i) r (Add₁ Val y↡) = Add₁ Val {! !} -- small⇒big⟶ E r y↡ - -- small⇒big⟶ (val n ^ j ⊕• E ^ .U) r (Add₂ Int) = Int - -- small⇒big⟶ (val n ^ j ⊕• E ^ i) r (Add₃ Val y↯) = Add₃ Val {! !} -- small⇒big⟶ E r y↯ - -- small⇒big⟶ (val n ^ j ⊕• E ^ .U) r Int = Int +map⇑ : forall {t} {x₁ x₂ : Exprˢ t} {i j} (E : EvalCtxt t i j) -> + (forall {v} -> x₁ ˢ⁻¹ ⇓[ i ] v -> x₂ ˢ⁻¹ ⇓[ i ] v) -> + (x₁ ˢ⁻¹ ⇑[ i ] -> x₂ ˢ⁻¹ ⇑[ i ]) -> + E [ x₁ ] ˢ⁻¹ ⇑[ j ] -> E [ x₂ ] ˢ⁻¹ ⇑[ j ] +map⇑ • f g ⇑ = g ⇑ +map⇑ (E •< |⊕| > y) f g (Add₁ x⇑) = Add₁ (map⇑ E f g x⇑) +map⇑ (E •< |⊕| > y) f g (Add₂ (_ , x↡) y⇑) = Add₂ (_ , map⇓ E f x↡) y⇑ +map⇑ (E •< |>>| > y) f g (Seqn₁ x⇑) = Seqn₁ (map⇑ E f g x⇑) +map⇑ (E •< |>>| > y) f g (Seqn₂ (_ , x↡) y⇑) = Seqn₂ (_ , map⇓ E f x↡) y⇑ +map⇑ (E •< |catch| > y) f g (Catch₁ x⇑) = Catch₁ (map⇑ E f g x⇑) +map⇑ (E •< |catch| > y) f g (Catch₂ x↯ y⇑) = Catch₂ (map⇓ E f x↯) y⇑ +map⇑ (val m ⊕• E) f g (Add₁ ()) +map⇑ (val m ⊕• E) f g (Add₂ x↡ y⇑) = Add₂ x↡ (map⇑ E f g y⇑) +map⇑ (handler• E) f g (Catch₁ ()) +map⇑ (handler• E) f g (Catch₂ x↯ y⇑) = Catch₂ x↯ (map⇑ E f g y⇑) +map⇑ (block• E) f g (Block x⇑) = Block (map⇑ E f g x⇑) +map⇑ (unblock• E) f g (Unblock x⇑) = Unblock (map⇑ E f g x⇑) hunk ./Semantics/Equivalence.agda 163 -small⇒big⟶⋆' : forall {t} (x : AnnExpr t) {i} v -> - x ⟶⋆ ⌜ v ⌝ ^ i -> unannotate x (status x) ⇓[ status x ] v -small⇒big⟶⋆' .(val n ^ B) {B} (val n) ε = Val -small⇒big⟶⋆' .(val n ^ U) {U} (val n) ε = Val -small⇒big⟶⋆' .(throw ^ B) {B} throw ε = Throw -small⇒big⟶⋆' .(throw ^ U) {U} throw ε = Throw -small⇒big⟶⋆' .(E [ x ]) v (reduction {x} {y} E r ◅ rs) = - A.small⇒big⟶ E r (small⇒big⟶⋆' (E [ y ]) v rs) +-- Then note that the reduction relation is compatible with the +-- big-step relations in the following sense: hunk ./Semantics/Equivalence.agda 166 --- small⇒big⟶⋆' : forall {t} (x : AnnExpr' t) {i j} v -> --- x ^ i ⟶⋆ ⌜ v ⌝ ^ j -> unannotate' x i ⇓[ i ] v --- small⇒big⟶⋆' .(val n) (val n) ε = Val --- small⇒big⟶⋆' .throw throw ε = Throw --- small⇒big⟶⋆' x {B} v (r ◅ rs) = helper (x ^ _) _ v r rs --- where --- helper : forall {t} (x y : AnnExpr t) {j} v -> --- x ⟶ y -> y ⟶⋆ ⌜ v ⌝ ^ j -> --- unannotate x (status x) ⇓[ status x ] v --- helper .(E [ x ]) .(E [ y ]) v (reduction {x} {y} E r) rs = {!small⇒big⟶⋆' (E [ y ]) v rs !} --- small⇒big⟶⋆' x {U} v (r ◅ rs) = {! !} +small⇒big⟶ʳ⇓ : forall {t i} {e₁ e₂ : Exprˢ t} {v} -> + e₁ ⟶ʳ[ i ] e₂ -> e₂ ˢ⁻¹ ⇓[ i ] v -> e₁ ˢ⁻¹ ⇓[ i ] v +small⇒big⟶ʳ⇓ Val ⇓ = ⇓ +small⇒big⟶ʳ⇓ Throw ⇓ = ⇓ +small⇒big⟶ʳ⇓ Loop ⇓ = ⇓ +small⇒big⟶ʳ⇓ Add₁ Val = Add₁ Val Val +small⇒big⟶ʳ⇓ Add₁ Int = Int +small⇒big⟶ʳ⇓ Add₂ Throw = Add₂ Throw +small⇒big⟶ʳ⇓ Add₂ Int = Int +small⇒big⟶ʳ⇓ Add₃ Throw = Add₃ Val Throw +small⇒big⟶ʳ⇓ Add₃ Int = Int +small⇒big⟶ʳ⇓ Seqn₁ ⇓ = Seqn₁ Val ⇓ +small⇒big⟶ʳ⇓ Seqn₂ Throw = Seqn₂ Throw +small⇒big⟶ʳ⇓ Seqn₂ Int = Int +small⇒big⟶ʳ⇓ Catch₁ Val = Catch₁ Val +small⇒big⟶ʳ⇓ Catch₁ Int = Int +small⇒big⟶ʳ⇓ (Catch₂ {v = val n}) Val = Catch₂ Throw Val +small⇒big⟶ʳ⇓ (Catch₂ {v = val n}) Int = Int +small⇒big⟶ʳ⇓ (Catch₂ {v = throw}) Throw = Catch₂ Throw Throw +small⇒big⟶ʳ⇓ (Catch₂ {v = throw}) Int = Int +small⇒big⟶ʳ⇓ (Block {v = val n}) Val = Block Val +small⇒big⟶ʳ⇓ (Block {v = val n}) Int = Int +small⇒big⟶ʳ⇓ (Block {v = throw}) Throw = Block Throw +small⇒big⟶ʳ⇓ (Block {v = throw}) Int = Int +small⇒big⟶ʳ⇓ (Unblock {v = val n}) Val = Unblock Val +small⇒big⟶ʳ⇓ (Unblock {v = val n}) Int = Int +small⇒big⟶ʳ⇓ (Unblock {v = throw}) Throw = Unblock Throw +small⇒big⟶ʳ⇓ (Unblock {v = throw}) Int = Int +small⇒big⟶ʳ⇓ (Int int) Throw = Int +small⇒big⟶ʳ⇓ (Int int) Int = Int hunk ./Semantics/Equivalence.agda 197 -small⇒big⟶⋆ : forall {t} (e : Expr t) {i j} v -> - annotate e i ⟶⋆ ⌜ v ⌝ ^ j -> e ⇓[ i ] v -small⇒big⟶⋆ e {i} v r = simplify⇓ (small⇒big⟶⋆' (annotate e i) v r) +small⇒big⟶ʳ⇑ : forall {t} {e₁ e₂ : Exprˢ t} {i} -> + e₁ ⟶ʳ[ i ] e₂ -> e₂ ˢ⁻¹ ⇑[ i ] -> e₁ ˢ⁻¹ ⇑[ i ] +small⇒big⟶ʳ⇑ Val () +small⇒big⟶ʳ⇑ Throw () +small⇒big⟶ʳ⇑ Loop ⇑ = Loop ⇑ +small⇒big⟶ʳ⇑ Add₁ () +small⇒big⟶ʳ⇑ Add₂ () +small⇒big⟶ʳ⇑ Add₃ () +small⇒big⟶ʳ⇑ Seqn₁ ⇑ = Seqn₂ (_ , Val) ⇑ +small⇒big⟶ʳ⇑ Seqn₂ () +small⇒big⟶ʳ⇑ Catch₁ () +small⇒big⟶ʳ⇑ (Catch₂ {v = val n}) () +small⇒big⟶ʳ⇑ (Catch₂ {v = throw}) () +small⇒big⟶ʳ⇑ (Block {v = val n}) () +small⇒big⟶ʳ⇑ (Block {v = throw}) () +small⇒big⟶ʳ⇑ (Unblock {v = val n}) () +small⇒big⟶ʳ⇑ (Unblock {v = throw}) () +small⇒big⟶ʳ⇑ (Int int) () hunk ./Semantics/Equivalence.agda 216 --- simplify⇑ : forall {t} {x : Expr t} {i j} -> --- unannotate' (annotate' x j) ⇑[ i ] -> x ⇑[ i ] --- simplify⇑ {x = x} {i = i} = ≡-subst (\x -> x ⇑[ i ]) (left-inverse x) +-- It is then easy to prove the desired result in the terminating +-- case. hunk ./Semantics/Equivalence.agda 219 --- small⇒big⟶ʳ⟶∞ : forall {t} {e₁ e₂ : Expr t} {i} -> --- e₁ ⟶ʳ[ i ] e₂ -> e₂ ⟶∞[ i ] -> e₁ ⇑[ i ] --- small⇒big⟶ʳ⟶∞ Loop ⟶∞ = Loop --- small⇒big⟶ʳ⟶∞ Add₁ ⟶∞ = {! !} --- small⇒big⟶ʳ⟶∞ Add₂ ⟶∞ = {! !} --- small⇒big⟶ʳ⟶∞ Add₃ ⟶∞ = {! !} --- small⇒big⟶ʳ⟶∞ Seqn₁ ⟶∞ = {! !} --- small⇒big⟶ʳ⟶∞ Seqn₂ ⟶∞ = {! !} --- small⇒big⟶ʳ⟶∞ Catch₁ ⟶∞ = {! !} --- small⇒big⟶ʳ⟶∞ Catch₂ ⟶∞ = {! !} --- small⇒big⟶ʳ⟶∞ Int ⟶∞ = {! !} --- small⇒big⟶ʳ⟶∞ Block ⟶∞ = {! !} --- small⇒big⟶ʳ⟶∞ Unblock ⟶∞ = {! !} - --- small⇒big⟶⟶∞ : forall {t} {e₁ e₂ : Expr t} {i j} --- (E : EvalCtxt t i j) -> --- e₁ ⟶ʳ[ i ] e₂ -> E [ e₂ ] ⟶∞[ j ] -> E [ e₁ ] ⇑[ j ] --- small⇒big⟶⟶∞ • r rs = small⇒big⟶ʳ⟶∞ r rs --- small⇒big⟶⟶∞ (z •[ z' ] z0) z1 z2 = {! !} --- small⇒big⟶⟶∞ (z [ z' ]• z0) z1 z2 = {! !} --- small⇒big⟶⟶∞ (block• z) z' z0 = {! !} --- small⇒big⟶⟶∞ (unblock• z) z' z0 = {! !} +small⇒big⟶⋆ : forall {t} {e : Exprˢ t} {i} v -> + e ⟶⋆[ i ] done v -> e ˢ⁻¹ ⇓[ i ] v +small⇒big⟶⋆ (val n) ε = Val +small⇒big⟶⋆ throw ε = Throw +small⇒big⟶⋆ v (Red E r ◅ rs) = + map⇓ E (small⇒big⟶ʳ⇓ r) (small⇒big⟶⋆ v rs) hunk ./Semantics/Equivalence.agda 226 --- small⇒big⟶∞' : forall {t} {e : AnnExpr t} -> --- e ⟶∞ -> unannotate e ⇑[ status e ] --- small⇒big⟶∞' (reduction E r ◅∞ rs) = {! !} -- small⇒big⟶⟶∞ E r rs +-- The non-terminating case is not quite as easy, though. Note that +-- the following proof is not productive. The right-hand side inspects +-- the result of the recursive call before emitting the first +-- constructor, so if this proof were a Haskell function its semantics +-- would be ⊥. hunk ./Semantics/Equivalence.agda 232 --- small⇒big⟶∞ : forall {t} {e : Expr t} {i} -> --- annotate e i ⟶∞ -> e ⇑[ i ] --- small⇒big⟶∞ rs = simplify⇑ (small⇒big⟶∞' rs) - --- -- small⇒big⟶∞ (val x) ⟶∞ = {! !} --- -- small⇒big⟶∞ throw ⟶∞ = {! !} --- -- small⇒big⟶∞ loop ⟶∞ = Loop --- -- small⇒big⟶∞ (x ⊕ y) (r ◅∞ rs) = {!r !} --- -- small⇒big⟶∞ (x >> y) ⟶∞ = {! !} --- -- small⇒big⟶∞ (x catch y) ⟶∞ = {! !} --- -- small⇒big⟶∞ (block x) ⟶∞ = {! !} --- -- small⇒big⟶∞ (unblock x) ⟶∞ = {! !} +small⇒big⟶∞ : forall {t} {e : Exprˢ t} {i} -> + e ⟶∞[ i ] -> e ˢ⁻¹ ⇑[ i ] +small⇒big⟶∞ (Red E r ◅∞ rs) ~ + map⇑ E (small⇒big⟶ʳ⇓ r) (small⇒big⟶ʳ⇑ r) (small⇒big⟶∞ rs) hunk ./Semantics/Equivalence.agda 237 --- small⇒big : Small⇒Big --- small⇒big = record { ⟶⋆ = small⇒big⟶⋆; ⟶∞ = small⇒big⟶∞ } +-- In "Coinductive big-step operational semantics" Leroy and Grall use +-- excluded middle to prove this result. I could follow them, but I +-- would prefer not to have to postulate any classical axioms. + +small⇒big : Small⇒Big +small⇒big = record { ⟶⋆ = small⇒big⟶⋆; ⟶∞ = small⇒big⟶∞ } hunk ./Semantics/SmallStep.agda 11 -open import Data.Product +open import Data.Bool hunk ./Semantics/SmallStep.agda 16 --- Redexes +-- Expressions annotated with information about whether they are still +-- running or not hunk ./Semantics/SmallStep.agda 19 -data Redex : forall {t} -> Expr t -> Set where - Loop : Redex loop - Add₁ : forall {t} m v -> Redex {t} (val m ⊕ ⌜ v ⌝) - Add₂ : forall {t} y -> Redex {t} (throw ⊕ y) - Seqn : forall {t} v y -> Redex {t} (⌜ v ⌝ >> y) - Catch : forall {t} v y -> Redex {t} (⌜ v ⌝ catch y) - Block : forall {t} v -> Redex {t} (block ⌜ v ⌝) - Unblock : forall {t} v -> Redex {t} (unblock ⌜ v ⌝) +infixl 7 _⊕_ +infixl 6 _catch_ +infixl 5 _>>_ + +mutual + + data Exprˢ t : Set where + run : (x : Exprˢ' t) -> Exprˢ t + done : (v : Value) -> Exprˢ t + + data Exprˢ' : Totality -> Set where + val : forall {t} (n : ℕ) -> Exprˢ' t + throw : forall {t} -> Exprˢ' t + loop : Exprˢ' partial + _⊕_ : forall {t} (x y : Exprˢ t) -> Exprˢ' t + _>>_ : forall {t} (x y : Exprˢ t) -> Exprˢ' t + _catch_ : forall {t} (x y : Exprˢ t) -> Exprˢ' t + block : forall {t} (x : Exprˢ t) -> Exprˢ' t + unblock : forall {t} (x : Exprˢ t) -> Exprˢ' t + +-- Annotates plain expressions. + +infix 9 _ˢ _ˢ' + +mutual + + _ˢ : forall {t} -> Expr t -> Exprˢ t + x ˢ = run (x ˢ') + + _ˢ' : forall {t} -> Expr t -> Exprˢ' t + val n ˢ' = val n + throw ˢ' = throw + loop ˢ' = loop + (x ⊕ y) ˢ' = x ˢ ⊕ y ˢ + (x >> y) ˢ' = x ˢ >> y ˢ + (x catch y) ˢ' = x ˢ catch y ˢ + block x ˢ' = block (x ˢ) + unblock x ˢ' = unblock (x ˢ) + +-- Removes annotations. + +infix 9 _ˢ⁻¹ _ˢ'⁻¹ + +mutual + + _ˢ⁻¹ : forall {t} -> Exprˢ t -> Expr t + run x ˢ⁻¹ = x ˢ'⁻¹ + done v ˢ⁻¹ = ⌜ v ⌝ + + _ˢ'⁻¹ : forall {t} -> Exprˢ' t -> Expr t + val n ˢ'⁻¹ = val n + throw ˢ'⁻¹ = throw + loop ˢ'⁻¹ = loop + (x ⊕ y) ˢ'⁻¹ = x ˢ⁻¹ ⊕ y ˢ⁻¹ + (x >> y) ˢ'⁻¹ = x ˢ⁻¹ >> y ˢ⁻¹ + (x catch y) ˢ'⁻¹ = x ˢ⁻¹ catch y ˢ⁻¹ + block x ˢ'⁻¹ = block (x ˢ⁻¹) + unblock x ˢ'⁻¹ = unblock (x ˢ⁻¹) + +-- A variant of _<_>_. + +infix 8 _<_>'_ + +_<_>'_ : forall {t} -> Exprˢ t -> Op -> Exprˢ t -> Exprˢ' t +x < |⊕| >' y = x ⊕ y +x < |>>| >' y = x >> y +x < |catch| >' y = x catch y + +------------------------------------------------------------------------ +-- Interruptible expressions + +-- This predicate ensures that a raised exception or interrupt cannot +-- be interrupted before the exception handler has been reached. + +mutual + + interruptible : forall {t} -> Exprˢ t -> Bool + interruptible (run x) = interruptible' x + interruptible (done (val n)) = true + interruptible (done throw) = false + + interruptible' : forall {t} -> Exprˢ' t -> Bool + interruptible' (val n) = true + interruptible' throw = true + interruptible' loop = true + interruptible' (run x ⊕ y) = interruptible' x + interruptible' (x ⊕ y) = interruptible x ∧ interruptible y + interruptible' (run x >> y) = interruptible' x + interruptible' (x >> y) = interruptible x ∧ interruptible y + interruptible' (run x catch y) = interruptible' x + interruptible' (x catch y) = interruptible x ∨ interruptible y + interruptible' (block x) = interruptible x + interruptible' (unblock x) = interruptible x hunk ./Semantics/SmallStep.agda 116 -infix 2 _⟶ʳ_ _∶_⟶ʳ_ +infix 2 _⟶ʳ[_]_ _∶_⟶ʳ[_]_ hunk ./Semantics/SmallStep.agda 121 - _∶_⟶ʳ_ : forall t {e : Expr t} -> Redex e -> Expr t -> Set - t ∶ e₁ ⟶ʳ e₂ = e₁ ⟶ʳ e₂ + _∶_⟶ʳ[_]_ : forall t -> Exprˢ t -> Status -> Exprˢ t -> Set + t ∶ e₁ ⟶ʳ[ i ] e₂ = e₁ ⟶ʳ[ i ] e₂ hunk ./Semantics/SmallStep.agda 124 - data _⟶ʳ_ : forall {t} {e : Expr t} -> Redex e -> Expr t -> Set where - Loop : Loop ⟶ʳ loop - Add₁ : forall {t m n} -> t ∶ Add₁ m (val n) ⟶ʳ val (m + n) - Add₂ : forall {t y} -> t ∶ Add₂ y ⟶ʳ throw - Add₃ : forall {t m} -> t ∶ Add₁ m throw ⟶ʳ throw - Seqn₁ : forall {t m y} -> t ∶ Seqn (val m) y ⟶ʳ y - Seqn₂ : forall {t y} -> t ∶ Seqn throw y ⟶ʳ throw - Catch₁ : forall {t m y} -> t ∶ Catch (val m) y ⟶ʳ val m - Catch₂ : forall {t y} -> t ∶ Catch throw y ⟶ʳ block y - Block : forall {t v} -> t ∶ Block v ⟶ʳ ⌜ v ⌝ - Unblock : forall {t v} -> t ∶ Unblock v ⟶ʳ ⌜ v ⌝ + data _⟶ʳ[_]_ : forall {t} -> Exprˢ t -> Status -> Exprˢ t -> Set where + Val : forall {t i m} -> t ∶ run (val m) ⟶ʳ[ i ] done (val m) + Throw : forall {t i} -> t ∶ run throw ⟶ʳ[ i ] done throw + Loop : forall {i} -> run loop ⟶ʳ[ i ] run loop + Add₁ : forall {t i m n} -> t ∶ run (done (val m) ⊕ done (val n)) ⟶ʳ[ i ] done (val (m + n)) + Add₂ : forall {t i y} -> t ∶ run (done throw ⊕ y) ⟶ʳ[ i ] done throw + Add₃ : forall {t i m} -> t ∶ run (done (val m) ⊕ done throw) ⟶ʳ[ i ] done throw + Seqn₁ : forall {t i m y} -> t ∶ run (done (val m) >> y) ⟶ʳ[ i ] y + Seqn₂ : forall {t i y} -> t ∶ run (done throw >> y) ⟶ʳ[ i ] done throw + Catch₁ : forall {t i m y} -> t ∶ run (done (val m) catch y) ⟶ʳ[ i ] done (val m) + Catch₂ : forall {t i v} -> t ∶ run (done throw catch done v) ⟶ʳ[ i ] done v + Block : forall {t i v} -> t ∶ run (block (done v)) ⟶ʳ[ i ] done v + Unblock : forall {t i v} -> t ∶ run (unblock (done v)) ⟶ʳ[ i ] done v + Int : forall {t x} (int : T (interruptible' x)) -> + t ∶ run x ⟶ʳ[ U ] done throw hunk ./Semantics/SmallStep.agda 146 +infix 7 _•<_>_ val_⊕•_ + hunk ./Semantics/SmallStep.agda 150 - _•<_>_ : forall {i j} (E : EvalCtxt t i j) (op : Op) (y : Expr t) -> + _•<_>_ : forall {i j} (E : EvalCtxt t i j) (op : Op) (y : Exprˢ t) -> hunk ./Semantics/SmallStep.agda 153 + handler• : forall {i j} (E : EvalCtxt t i B) -> EvalCtxt t i j hunk ./Semantics/SmallStep.agda 161 -_[_] : forall {t i j} -> EvalCtxt t i j -> Expr t -> Expr t +_[_] : forall {t i j} -> EvalCtxt t i j -> Exprˢ t -> Exprˢ t hunk ./Semantics/SmallStep.agda 163 -(E •< op > x) [ y ] = E [ y ] < op > x -(val n ⊕• E) [ y ] = val n ⊕ E [ y ] -(block• E) [ y ] = block (E [ y ]) -(unblock• E) [ y ] = unblock (E [ y ]) +(E •< op > x) [ y ] = run (E [ y ] < op >' x) +(val n ⊕• E) [ y ] = run (done (val n) ⊕ E [ y ]) +(handler• E) [ y ] = run (done throw catch E [ y ]) +(block• E) [ y ] = run (block (E [ y ])) +(unblock• E) [ y ] = run (unblock (E [ y ])) hunk ./Semantics/SmallStep.agda 178 +handler• E₁ ∘ E₂ = handler• (E₁ ∘ E₂) hunk ./Semantics/SmallStep.agda 182 --- Inverting a context (turning it outside-in). - -status : forall {t i j} -> EvalCtxt t i j -> Status -status {j = j} • = j -status (E •< op > y) = status E -status (val m ⊕• E) = status E -status (block• E) = B -status (unblock• E) = U - -infix 11 _⁻¹ - -_⁻¹ : forall {t i j} (E : EvalCtxt t i j) -> EvalCtxt t (status E) i -• ⁻¹ = • -(E •< op > y) ⁻¹ = E ⁻¹ ∘ (• •< op > y) -(val m ⊕• E) ⁻¹ = E ⁻¹ ∘ (val m ⊕• •) -block• E ⁻¹ = E ⁻¹ ∘ block• • -unblock• E ⁻¹ = E ⁻¹ ∘ unblock• • - hunk ./Semantics/SmallStep.agda 185 --- Finds the innermost exception-handler in the evaluation context --- (which is assumed to have been inverted). The handler is returned --- in the appropriate context. - -unwind : forall {t i j} -> EvalCtxt t i j -> Expr t -unwind • = throw -- No exception handler. -unwind (E •< |⊕| > y) = unwind E -unwind (E •< |>>| > y) = unwind E -unwind (E •< |catch| > y) = E ⁻¹ [ block y ] - -- Interrupts are blocked in the handler. -unwind (val m ⊕• E) = unwind E -unwind (block• E) = unwind E -unwind (unblock• E) = unwind E - hunk ./Semantics/SmallStep.agda 189 -data _⟶[_]_ : forall {t} -> Expr t -> Status -> Expr t -> Set where - Red : forall {t i j x} {r : Redex x} {y} (E : EvalCtxt t i j) -> - r ⟶ʳ y -> E [ x ] ⟶[ j ] E [ y ] - Int : forall {t j x} (r : Redex x) (E : EvalCtxt t U j) -> - E [ x ] ⟶[ j ] unwind (E ⁻¹) +data _⟶[_]_ : forall {t} -> Exprˢ t -> Status -> Exprˢ t -> Set where + Red : forall {t i j x y} + (E : EvalCtxt t i j) (r : x ⟶ʳ[ i ] y) -> + E [ x ] ⟶[ j ] E [ y ] hunk ./Semantics/SmallStep.agda 194 -Step : forall {t} -> Status -> Expr t -> Expr t -> Set +Step : forall {t} -> Status -> Exprˢ t -> Exprˢ t -> Set hunk ./Semantics/SmallStep.agda 201 -_⟶⋆[_]_ : forall {t} -> Expr t -> Status -> Expr t -> Set +_⟶⋆[_]_ : forall {t} -> Exprˢ t -> Status -> Exprˢ t -> Set hunk ./Semantics/SmallStep.agda 210 -_⟶∞[_] : forall {t} -> Expr t -> Status -> Set +_⟶∞[_] : forall {t} -> Exprˢ t -> Status -> Set hunk ./Semantics/SmallStep.agda 214 --- Some utility functions/lemmas +-- Lemmas about evaluation contexts hunk ./Semantics/SmallStep.agda 220 -∘-lemma (E₁ •< op > y) E₂ = ≡-cong (\x -> x < op > y) (∘-lemma E₁ E₂) -∘-lemma (val n ⊕• E₁) E₂ = ≡-cong (\x -> (val n) ⊕ x) (∘-lemma E₁ E₂) -∘-lemma (block• E₁) E₂ = ≡-cong block (∘-lemma E₁ E₂) -∘-lemma (unblock• E₁) E₂ = ≡-cong unblock (∘-lemma E₁ E₂) - --- Lifting of reductions/reduction sequences. - --- Note that the following lemma is not true. +∘-lemma (E₁ •< op > y) E₂ = ≡-cong (\x -> run (x < op >' y)) (∘-lemma E₁ E₂) +∘-lemma (val n ⊕• E₁) E₂ = ≡-cong (\x -> run (done (val n) ⊕ x)) (∘-lemma E₁ E₂) +∘-lemma (handler• E₁) E₂ = ≡-cong (\x -> run (done throw catch x)) (∘-lemma E₁ E₂) +∘-lemma (block• E₁) E₂ = ≡-cong (\x -> run (block x)) (∘-lemma E₁ E₂) +∘-lemma (unblock• E₁) E₂ = ≡-cong (\x -> run (unblock x)) (∘-lemma E₁ E₂) hunk ./Semantics/SmallStep.agda 226 +-- Lifting of reductions/reduction sequences. + hunk ./Semantics/SmallStep.agda 234 -lift⟶ E₁ (Int {x = x} r E₂) = {! !} hunk ./Semantics/SmallStep.agda 243 +------------------------------------------------------------------------ +-- Lemmas about annotations + +-- Annotated expressions are interruptible. + +_ˢ-interruptible : forall {t} (x : Expr t) -> T (interruptible (x ˢ)) +val n ˢ-interruptible = _ +throw ˢ-interruptible = _ +loop ˢ-interruptible = _ +(x ⊕ y) ˢ-interruptible = x ˢ-interruptible +(x >> y) ˢ-interruptible = x ˢ-interruptible +(x catch y) ˢ-interruptible = x ˢ-interruptible +block x ˢ-interruptible = x ˢ-interruptible +unblock x ˢ-interruptible = x ˢ-interruptible + +-- Deannotating an annotated expression yields the original. + +left-inverse : forall {t} (x : Expr t) -> x ˢ ˢ⁻¹ ≡ x +left-inverse (val n) = ≡-refl +left-inverse throw = ≡-refl +left-inverse loop = ≡-refl +left-inverse (x ⊕ y) = ≡-cong₂ _⊕_ (left-inverse x) (left-inverse y) +left-inverse (x >> y) = ≡-cong₂ _>>_ (left-inverse x) (left-inverse y) +left-inverse (x catch y) = ≡-cong₂ _catch_ (left-inverse x) (left-inverse y) +left-inverse (block x) = ≡-cong block (left-inverse x) +left-inverse (unblock x) = ≡-cong unblock (left-inverse x) + hunk ./StatusLemmas.agda 36 -Bto·⇑ Loop ~ Loop +Bto·⇑ (Loop loop⇑) ~ Loop (Bto·⇑ loop⇑)