------------------------------------------------------------------------
-- The proof of small⇒big⟶∞ uses the lemmas proved here
------------------------------------------------------------------------

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↛∞ ⟶∞)