module Semantics.Equivalence.Lemmas where
open import Syntax
open import Infinite
open import Semantics.SmallStep
open import Data.Empty
open import Data.Function
module Add where
helper : ∀ {t} {y : Exprˢ t} {m i} →
run (done (nat m) ⊕ y) ⟶∞[ i ] → y ⟶∞[ i ]
helper (Red Add₁ ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
helper (Red Add₃ ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
helper (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
helper (Addʳ ⟶ ◅∞ ⟶∞) ~ ⟶ ◅∞ helper ⟶∞
helper (Addˡ (Red (Int _)) ◅∞ Red (Int ()) ◅∞ ⟶∞)
helper (Addˡ (Red (Int _)) ◅∞ Addˡ (Red (Int ())) ◅∞ ⟶∞)
helper (Addˡ (Red (Int _)) ◅∞ Red Add₂ ◅∞ ⟶∞) =
⊥-elim (done↛∞ ⟶∞)
data Pred {t} (y : Exprˢ t) i : Exprˢ t → Set where
• : ∀ n (y⟶∞ : y ⟶∞[ i ]) → Pred y i (done (nat n))
lemma : ∀ {t} {x y : Exprˢ t} {i} →
run (x ⊕ y) ⟶∞[ i ] → x ⟶⋆∞[ i ] Pred y i
lemma (Red Add₁ ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red Add₂ ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red Add₃ ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Addˡ ⟶ ◅∞ ⟶∞) ~ ⟶ ◅∞ lemma ⟶∞
lemma (Addʳ ⟶ ◅∞ ⟶∞) = ε (• _ (⟶ ◅∞ helper ⟶∞))
module Seqn where
open Add public using (Pred; •)
lemma : ∀ {t} {x y : Exprˢ t} {i} →
run (x >> y) ⟶∞[ i ] → x ⟶⋆∞[ i ] Pred y i
lemma (Red Seqn₁ ◅∞ ⟶∞) = ε (• _ ⟶∞)
lemma (Red Seqn₂ ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Seqnˡ ⟶ ◅∞ ⟶∞) ~ ⟶ ◅∞ lemma ⟶∞
module Catch where
helper : ∀ {t} {y : Exprˢ t} {i} →
run (done throw catch y) ⟶∞[ i ] → y ⟶∞[ B ]
helper (Red Catch₂ ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
helper (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
helper (Catchˡ (Red (Int ())) ◅∞ ⟶∞)
helper (Catchʳ ⟶ ◅∞ ⟶∞) ~ ⟶ ◅∞ helper ⟶∞
data Pred {t} (y : Exprˢ t) i : Exprˢ t → Set where
• : (y⟶∞ : y ⟶∞[ B ]) → Pred y i (done throw)
lemma : ∀ {t} {x y : Exprˢ t} {i} →
run (x catch y) ⟶∞[ i ] → x ⟶⋆∞[ i ] Pred y i
lemma (Red Catch₁ ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red Catch₂ ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Catchˡ ⟶ ◅∞ ⟶∞) ~ ⟶ ◅∞ lemma ⟶∞
lemma (Catchʳ ⟶ ◅∞ ⟶∞) = ε (• (⟶ ◅∞ helper ⟶∞))
module Block where
lemma : ∀ {t} {x : Exprˢ t} {i} → run (block x) ⟶∞[ i ] → x ⟶∞[ B ]
lemma (Red Block ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Blockˡ ⟶ ◅∞ ⟶∞) ~ ⟶ ◅∞ lemma ⟶∞
module Unblock where
lemma : ∀ {t} {x : Exprˢ t} {i} → run (unblock x) ⟶∞[ i ] → x ⟶∞[ U ]
lemma (Red Unblock ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Unblockˡ ⟶ ◅∞ ⟶∞) ~ ⟶ ◅∞ lemma ⟶∞
module Loop where
data Pred i : Exprˢ partial → Set where
• : ∀ n → Pred i (done (nat n))
helper : ∀ {y i x} → Seqn.Pred y i x → Pred i x
helper (Seqn.• n _) = • n
lemma : ∀ {x i} → run (loop x) ⟶∞[ i ] → x ⟶⋆∞[ i ] Pred i
lemma (Red Loop ◅∞ ⟶∞) = map⋆∞ id id helper (Seqn.lemma ⟶∞)
lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)