module stlc.value.equality where

open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥)
open import Data.Product renaming (_,_ to ⦅_,_⦆; _×_ to _⊗_) public
import Relation.Binary.PropositionalEquality as Eq

open import helper.iso using (_⇔_) public

open import stlc.catComb.eval public

open CatCombValue public

infix  _≣_
infix  _≣'_

data _≣_ : ∀ {A} → (a b : CatCombValue A) → Set
_≣'_ : ∀ {A} → (a b : CatCombValue A) → Set

data _≣_  where
  unit : ⟨⟩ ≣ ⟨⟩
  nat : ∀ {x} → `nat x ≣ `nat x
  pair : ∀ {A B s s' t t'} → s ≣ s' → t ≣ t' → _≣_ {A × B} (s , t) (s' , t')
  cur : ∀ {A B C D f g} {s : CatCombValue C} {s'' : CatCombValue D} → (∀ {s₁ s₂ : CatCombValue A} {t t'} → s₁ ≣' s₂ → ⟨ f ∣ s , s₁ ⟩= t → ⟨ g ∣ s'' , s₂ ⟩= t' → t ≣ t') → _≣_ {A ⇒ B} (cur f s) (cur g s'')
--- COPRODUCT ---
  inl : ∀ {A B t t'} → t ≣ t' → _≣_ {A + B} (L t) (L t')
  inr : ∀ {A B t t'} → t ≣ t' → _≣_ {A + B} (R t) (R t')
--- LIST OBJECT ---
  nil : ∀ {A} → _≣_ {list A} [] []
  cons : ∀ {A h h' t t'} → h ≣ h' → t ≣ t' → _≣_ {list A} (h ⦂ t) (h' ⦂ t')

_≣'_ {unit} ⟨⟩ ⟨⟩ = ⊤
_≣'_ {A × A₁} (a , a₁) (b , b₁) = (a ≣' b) ⊗ (a₁ ≣' b₁)
_≣'_ {A ⇒ A₁} (cur f a) (cur g b) = ∀ {s₁ s₂ : CatCombValue A} {t t'} → s₁ ≣' s₂ → ⟨ f ∣ a , s₁ ⟩= t → ⟨ g ∣ b , s₂ ⟩= t' → t ≣' t'
_≣'_ {nat} (`nat x) (`nat x₁) = x Eq.≡ x₁
--- COPRODUCT ---
_≣'_ {A + A₁} (L a) (L b) = a ≣' b
_≣'_ {A + A₁} (L a) (R b) = ⊥
_≣'_ {A + A₁} (R a) (L b) = ⊥
_≣'_ {A + A₁} (R a) (R b) = a ≣' b
--- LIST OBJECT ---
_≣'_ {list A} [] [] = ⊤
_≣'_ {list A} [] (b ⦂ b₁) = ⊥
_≣'_ {list A} (a ⦂ a₁) [] = ⊥
_≣'_ {list A} (a ⦂ a₁) (b ⦂ b₁) = a ≣' b ⊗ a₁ ≣' b₁

≣⇔≣' : ∀ {A} {a b : CatCombValue A} → a ≣ b ⇔ a ≣' b
≣⇔≣' =
  record
    { to = to
    ; from = from
    }
  where
    to : ∀ {A} {a b : CatCombValue A} → a ≣ b → a ≣' b
    to unit = tt
    to nat = Eq.refl
    to (pair x x₁) = ⦅ to x , to x₁ ⦆
    to (cur x) x₁ x₂ x₃ = to (x x₁ x₂ x₃)
    to (inl x) = to x
    to (inr x) = to x
    to nil = tt
    to (cons x x₁) = ⦅ to x , to x₁ ⦆

    from : ∀ {A} {a b : CatCombValue A} → a ≣' b → a ≣ b
    from {.unit} {⟨⟩} {⟨⟩} tt = unit
    from {.nat} {`nat x₁} {`nat .x₁} Eq.refl = nat
    from {.(_ × _)} {a , a₁} {b , b₁} ⦅ fst , snd ⦆ = pair (from fst) (from snd)
    from {.(_ ⇒ _)} {cur x₁ a} {cur x₂ b} x = cur (λ x₃ x₄ x₅ → from (x x₃ x₄ x₅))
    from {.(_ + _)} {L a} {L b} x = inl (from x)
    from {.(_ + _)} {R a} {R b} x = inr (from x)
    from {.(list _)} {[]} {[]} tt = nil
    from {.(list _)} {a ⦂ a₁} {b ⦂ b₁} ⦅ fst , snd ⦆ = cons (from fst) (from snd)