module stlc.catComb.logicalRelation where

open import Data.Unit using (⊤; tt)
open import Data.Product using (Σ; ∃; Σ-syntax; ∃-syntax; proj₁; proj₂) renaming (_,_ to ⦅_,_⦆; _×_ to _⊗_) public

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

open import stlc.catComb.eval

open CatCombValue

infix 4 ⊩_
infix 4 ⊩'_

data ⊩_ : ∀ {A : Type} → CatCombValue A → Set
⊩'_ : ∀ {A : Type} → CatCombValue A → Set

data ⊩_ where
  unit : ⊩ ⟨⟩
  nat : ∀ {x} → ⊩ `nat x
  pair : ∀ {A B s t} → (⊩ s) ⊗ (⊩ t) → ⊩_ {A × B} (s , t)
  cur : ∀ {A A₁ A₂ s} {f : CatComb (A × A₁) A₂} → (∀ {s₁} → ⊩' s₁ → ∃[ t ] ⟨ f ∣ s , s₁ ⟩= t ⊗ ⊩ t) → ⊩ cur f s
--- COPRODUCT ---
  inl : ∀ {A B s} → ⊩ s → ⊩ L_ {A} {B} s
  inr : ∀ {A B s} → ⊩ s → ⊩ R_ {A} {B} s
--- LIST OBJECT ---
  nil : ∀ {A} → ⊩ [] {A}
  cons : ∀ {A h t} → ⊩ h → ⊩ t → ⊩_ {list A} (h ⦂ t)

⊩' ⟨⟩ = ⊤
⊩' `nat x = ⊤
⊩' (s , s₁) = (⊩' s) ⊗ (⊩' s₁)
⊩' cur f s = ∀ {s₁} → ⊩' s₁ → ∃[ t ] ⟨ f ∣ s , s₁ ⟩= t ⊗ (⊩' t)
⊩' L s = ⊩' s
⊩' R s = ⊩' s
--- LIST OBJECT ---
⊩' [] = ⊤
⊩' h ⦂ t = (⊩' h) ⊗ (⊩' t)

⊩⇔⊩' : ∀ {A s} → ⊩ s ⇔ ⊩'_ {A} s
⊩⇔⊩' =
  record
    { to = to
    ; from = from
    }
  where
    to : ∀ {A s} → ⊩ s → ⊩'_ {A} s
    to {.unit} {⟨⟩} _ = tt
    to {.nat} {`nat _} _ = tt
    to {.(_ × _)} {_ , _} (pair ⦅ x₁ , x₂ ⦆) = ⦅ to x₁ , to x₂ ⦆
    to {.(_ ⇒ _)} {cur _ _} (cur f) s with f s
    ... | ⦅ t , ⦅ s₁ , s₂ ⦆ ⦆ = ⦅ t , ⦅ s₁ , (to s₂) ⦆ ⦆
    to {.(_ + _)} {L _} (inl x) = to x
    to {.(_ + _)} {R _} (inr x) = to x
    to nil = tt
    to (cons x x₁) = ⦅ to x , to x₁ ⦆

    from : ∀ {A s} → ⊩'_ {A} s → ⊩ s
    from {.unit} {⟨⟩} _ = unit
    from {.nat} {`nat _} _ = nat
    from {.(_ × _)} {_ , _} x = pair ⦅ from (proj₁ x) , from (proj₂ x) ⦆
    from {.(_ ⇒ _)} {cur _ _} f = cur λ s → ⦅ proj₁ (f s) , ⦅ proj₁ (proj₂ (f s)) , from (proj₂ (proj₂ (f s))) ⦆ ⦆
    from {.(_ + _)} {L _} x = inl (from x)
    from {.(_ + _)} {R _} x = inr (from x)
    from {list A} {[]} x = nil
    from {list A} {s ⦂ s₁} x = cons (from (proj₁ x)) (from (proj₂ x))