module CC.BigStepErasedDeterministic where

open import Data.Empty using (βŠ₯; βŠ₯-elim)
open import Data.Bool using (true; false) renaming (Bool to 𝔹)
open import Data.Sum using (_⊎_; inj₁; injβ‚‚)
open import Data.Product using (_Γ—_; βˆƒ; βˆƒ-syntax; Ξ£; Ξ£-syntax) renaming (_,_ to ⟨_,_⟩)
open import Relation.Nullary using (Β¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.PropositionalEquality using (_≑_; _β‰’_; refl; trans; cong; sym)
open import Function using (case_of_)

open import Common.Utils
open import Common.Types
open import Memory.Heap
open import CC.CCStatics
open import CC.BigStepErased


⇓ₑ-deterministic : βˆ€ {M ΞΌ μ₁ ΞΌβ‚‚ pc} {V₁ Vβ‚‚}
  β†’ ΞΌ ∣ pc ⊒ M ⇓ₑ V₁ ∣ μ₁
  β†’ ΞΌ ∣ pc ⊒ M ⇓ₑ Vβ‚‚ ∣ ΞΌβ‚‚
    -------------------------------------
  β†’ V₁ ≑ Vβ‚‚ Γ— μ₁ ≑ ΞΌβ‚‚
⇓ₑ-deterministic (⇓ₑ-val _) (⇓ₑ-val _) = ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-app L⇓ƛN M⇓V N[V]⇓W) (⇓ₑ-app L⇓ƛN† M⇓V† N[V]⇓W†) =
  case ⇓ₑ-deterministic L⇓ƛN L⇓ƛN† of Ξ» where
  ⟨ refl , refl ⟩ β†’
    case ⇓ₑ-deterministic M⇓V M⇓V† of Ξ» where
    ⟨ refl , refl ⟩ β†’
      case ⇓ₑ-deterministic N[V]⇓W N[V]⇓W† of Ξ» where
      ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-app L⇓ƛN _ _) (⇓ₑ-app-● L⇓● _) =
  contradiction (⇓ₑ-deterministic L⇓ƛN L⇓●) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-app-● L⇓● _) (⇓ₑ-app L⇓ƛN _ _) =
  contradiction (⇓ₑ-deterministic L⇓● L⇓ƛN) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-app-● L⇓● M⇓V) (⇓ₑ-app-● L⇓●† M⇓V†) =
  case ⇓ₑ-deterministic L⇓● L⇓●† of Ξ» where
  ⟨ refl , refl ⟩ β†’
    case ⇓ₑ-deterministic M⇓V M⇓V† of Ξ» where
    ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-if-true L⇓true M⇓V) (⇓ₑ-if-true L⇓true† M⇓V†) =
  case ⇓ₑ-deterministic L⇓true L⇓true† of Ξ» where
  ⟨ refl , refl ⟩ β†’
    case ⇓ₑ-deterministic M⇓V M⇓V† of Ξ» where
    ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-if-true L⇓true _) (⇓ₑ-if-false L⇓false _) =
  contradiction (⇓ₑ-deterministic L⇓true L⇓false) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-if-true L⇓true _) (⇓ₑ-if-● L⇓●) =
  contradiction (⇓ₑ-deterministic L⇓true L⇓●) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-if-false L⇓false N⇓V) (⇓ₑ-if-false L⇓false† N⇓V†) =
  case ⇓ₑ-deterministic L⇓false L⇓false† of Ξ» where
  ⟨ refl , refl ⟩ β†’
    case ⇓ₑ-deterministic N⇓V N⇓V† of Ξ» where
    ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-if-false L⇓false _) (⇓ₑ-if-true L⇓true _) =
  contradiction (⇓ₑ-deterministic L⇓false L⇓true) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-if-false L⇓false _) (⇓ₑ-if-● L⇓●) =
  contradiction (⇓ₑ-deterministic L⇓false L⇓●) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-if-● L⇓●) (⇓ₑ-if-true L⇓true _) =
  contradiction (⇓ₑ-deterministic L⇓● L⇓true ) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-if-● L⇓●) (⇓ₑ-if-false L⇓false _) =
  contradiction (⇓ₑ-deterministic L⇓● L⇓false) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-if-● L⇓●) (⇓ₑ-if-● L⇓●†) =
  case ⇓ₑ-deterministic L⇓● L⇓●† of Ξ» where
  ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-let M⇓V N[V]⇓W) (⇓ₑ-let M⇓V† N[V]⇓W†) =
  case ⇓ₑ-deterministic M⇓V M⇓V† of Ξ» where
  ⟨ refl , refl ⟩ β†’
    case ⇓ₑ-deterministic N[V]⇓W N[V]⇓W† of Ξ» where
    ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-ref? M⇓V fresh _) (⇓ₑ-ref? M⇓V† fresh† _) =
  case ⇓ₑ-deterministic M⇓V M⇓V† of Ξ» where
  ⟨ refl , refl ⟩ β†’
    case trans fresh (sym fresh†) of Ξ» where
      refl β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-ref?-● M⇓V) (⇓ₑ-ref?-● M⇓V†) =
  case ⇓ₑ-deterministic M⇓V M⇓V† of Ξ» where
  ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-ref M⇓V fresh) (⇓ₑ-ref M⇓V† fresh†) =
  case ⇓ₑ-deterministic M⇓V M⇓V† of Ξ» where
  ⟨ refl , refl ⟩ β†’
    case trans fresh (sym fresh†) of Ξ» where
      refl β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-ref-● M⇓V) (⇓ₑ-ref-● M⇓V†) =
  case ⇓ₑ-deterministic M⇓V M⇓V† of Ξ» where
  ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-deref M⇓a eq) (⇓ₑ-deref M⇓a† eq†) =
  case ⇓ₑ-deterministic M⇓a M⇓a† of Ξ» where
  ⟨ refl , refl ⟩ β†’
    case trans (sym eq) eq† of Ξ» where
    refl β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-deref M⇓a _) (⇓ₑ-deref-● M⇓●) =
  contradiction (⇓ₑ-deterministic M⇓a M⇓●) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-deref-● M⇓●) (⇓ₑ-deref M⇓a _) =
  contradiction (⇓ₑ-deterministic M⇓● M⇓a) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-deref-● M⇓●) (⇓ₑ-deref-● M⇓●†) =
  case ⇓ₑ-deterministic M⇓● M⇓●† of Ξ» where
  ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-assign? L⇓a M⇓V _) (⇓ₑ-assign? L⇓a† M⇓V† _) =
  case ⇓ₑ-deterministic L⇓a L⇓a† of Ξ» where
  ⟨ refl , refl ⟩ β†’
    case ⇓ₑ-deterministic M⇓V M⇓V† of Ξ» where
    ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-assign? L⇓a _ _) (⇓ₑ-assign?-● L⇓● _) =
  contradiction (⇓ₑ-deterministic L⇓a L⇓●) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-assign?-● L⇓● _) (⇓ₑ-assign? L⇓a _ _) =
  contradiction (⇓ₑ-deterministic L⇓● L⇓a) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-assign?-● L⇓● M⇓V) (⇓ₑ-assign?-● L⇓●† M⇓V†) =
  case ⇓ₑ-deterministic L⇓● L⇓●† of Ξ» where
  ⟨ refl , refl ⟩ β†’
    case ⇓ₑ-deterministic M⇓V M⇓V† of Ξ» where
    ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-assign L⇓a M⇓V) (⇓ₑ-assign L⇓a† M⇓V†) =
  case ⇓ₑ-deterministic L⇓a L⇓a† of Ξ» where
  ⟨ refl , refl ⟩ β†’
    case ⇓ₑ-deterministic M⇓V M⇓V† of Ξ» where
    ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩
⇓ₑ-deterministic (⇓ₑ-assign L⇓a _) (⇓ₑ-assign-● L⇓● _) =
  contradiction (⇓ₑ-deterministic L⇓a L⇓●) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-assign-● L⇓● _) (⇓ₑ-assign L⇓a _) =
  contradiction (⇓ₑ-deterministic L⇓● L⇓a) (Ξ» ())
⇓ₑ-deterministic (⇓ₑ-assign-● L⇓● M⇓V) (⇓ₑ-assign-● L⇓●† M⇓V†) =
  case ⇓ₑ-deterministic L⇓● L⇓●† of Ξ» where
  ⟨ refl , refl ⟩ β†’
    case ⇓ₑ-deterministic M⇓V M⇓V† of Ξ» where
    ⟨ refl , refl ⟩ β†’ ⟨ refl , refl ⟩