------------------------------------------------------------------------
-- 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.Product
open import Data.Sum
open import Data.Function
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Category.Monad
open RawMonad ¬¬-Monad using (_<$>_)

module Add where

  helper₂ : forall {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↛∞ ⟶∞)

  Pred : forall {t} -> Exprˢ t -> Status -> Exprˢ t -> Set
  Pred y i = \x -> ∃ \n -> x ≡ done (nat n) × y ⟶∞[ i ]

  helper₁ : forall {t} {x y : Exprˢ t} {i} ->
            run (x ⊕ y) ⟶∞[ i ] -> x ⟶⋆∞[ i ] Pred y i
  helper₁ (Red Add₁      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
  helper₁ (Red Add₂      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
  helper₁ (Red Add₃      ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
  helper₁ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
  helper₁ (Addˡ ⟶        ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₁ ⟶∞
  helper₁ (Addʳ ⟶        ◅∞ ⟶∞) ~ ε (_ , ≡-refl , ⟶ ◅∞ helper₂ ⟶∞)

  lemma : forall {t} {x y : Exprˢ t} {i} ->
          run (x ⊕ y) ⟶∞[ i ] ->
          ¬ ¬ (x ⟶∞[ i ] ⊎
               (∃ \n -> (x ⟶⋆[ i ] done (nat n)) × y ⟶∞[ i ]))
  lemma {x = x} {y} {i} ⟶∞ =
    helper <$> reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₁ ⟶∞))
    where
    helper : ∃ (\z -> (x ⟶⋆[ i ] z) × Pred y i z) ⊎ x ⟶∞[ i ] -> _
    helper (inj₁ (.(done (nat n)) , x⟶⋆n , n , ≡-refl , y⟶∞)) = inj₂ (n , x⟶⋆n , y⟶∞)
    helper (inj₂ x⟶∞)                                         = inj₁ x⟶∞

module Seqn where

  Pred : forall {t} -> Exprˢ t -> Status -> Exprˢ t -> Set
  Pred y i = \x -> ∃ \n -> x ≡ done (nat n) × y ⟶∞[ i ]

  helper₁ : forall {t} {x y : Exprˢ t} {i} ->
            run (x >> y) ⟶∞[ i ] -> x ⟶⋆∞[ i ] Pred y i
  helper₁ (Red Seqn₁     ◅∞ ⟶∞) ~ ε (_ , ≡-refl , ⟶∞)
  helper₁ (Red Seqn₂     ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
  helper₁ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
  helper₁ (Seqnˡ ⟶       ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₁ ⟶∞

  lemma : forall {t} {x y : Exprˢ t} {i} ->
          run (x >> y) ⟶∞[ i ] ->
          ¬ ¬ (x ⟶∞[ i ] ⊎
               (∃ \n -> (x ⟶⋆[ i ] done (nat n)) × y ⟶∞[ i ]))
  lemma {x = x} {y} {i} ⟶∞ =
    helper <$> reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₁ ⟶∞))
    where
    helper : ∃ (\z -> (x ⟶⋆[ i ] z) × Pred y i z) ⊎ x ⟶∞[ i ] -> _
    helper (inj₁ (.(done (nat n)) , x⟶⋆n , n , ≡-refl , y⟶∞)) = inj₂ (n , x⟶⋆n , y⟶∞)
    helper (inj₂ x⟶∞)                                         = inj₁ x⟶∞

module Catch where

  helper₂ : forall {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₂ ⟶∞

  Pred : forall {t} -> Exprˢ t -> Status -> Exprˢ t -> Set
  Pred y i = \x -> x ≡ done throw × y ⟶∞[ B ]

  helper₁ : forall {t} {x y : Exprˢ t} {i} ->
            run (x catch y) ⟶∞[ i ] -> x ⟶⋆∞[ i ] Pred y i
  helper₁ (Red Catch₁    ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
  helper₁ (Red Catch₂    ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
  helper₁ (Red (Int int) ◅∞ ⟶∞) ~ ⊥-elim (done↛∞ ⟶∞)
  helper₁ (Catchˡ ⟶      ◅∞ ⟶∞) ~ ⟶ ◅∞ helper₁ ⟶∞
  helper₁ (Catchʳ ⟶      ◅∞ ⟶∞) ~ ε (≡-refl , ⟶ ◅∞ helper₂ ⟶∞)

  lemma : forall {t} {x y : Exprˢ t} {i} ->
          run (x catch y) ⟶∞[ i ] ->
          ¬ ¬ (x ⟶∞[ i ] ⊎ ((x ⟶⋆[ i ] done throw) × y ⟶∞[ B ]))
  lemma {x = x} {y} {i} ⟶∞ =
    helper <$> reductio-ad-absurdum-⊎ (⋆∞⇒∞ (helper₁ ⟶∞))
    where
    helper : ∃ (\z -> (x ⟶⋆[ i ] z) × Pred y i z) ⊎ x ⟶∞[ i ] -> _
    helper (inj₁ (.(done throw) , x⟶⋆↯ , ≡-refl , y⟶∞)) = inj₂ (x⟶⋆↯ , y⟶∞)
    helper (inj₂ x⟶∞)                                   = inj₁ x⟶∞

module Block where

  lemma : forall {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 : forall {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

  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} ⟶∞ =
    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⟶∞