module stlc.catComb.eval where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong)

open import stlc.catComb public
open import stlc.value using (CatCombValue) public
open import stlc.monad.impl

open CatCombValue

data ⟨_∣_⟩=_ : ∀ {A B} → CatComb A B → CatCombValue A → CatCombValue B → Set where
  ev-unit : ∀ {A} {s : CatCombValue A} → ⟨ ! ∣ s ⟩= ⟨⟩
  ev-nat : ∀ {A x} {s : CatCombValue A} → ⟨ nat x ∣ s ⟩= (`nat x)
  ev-id : ∀ {A} {s : CatCombValue A} → ⟨ id ∣ s ⟩= s
  ev-comp : ∀ {A B C s s₁ s₂} {f : CatComb A B} {g : CatComb B C} → ⟨ f ∣ s ⟩= s₁ → ⟨ g ∣ s₁ ⟩= s₂ → ⟨ g ∘ f ∣ s ⟩= s₂
--- PRODUCT ---
  ev-pair : ∀ {A B C} {f : CatComb A B} {g : CatComb A C} {s s₁ s₂} → ⟨ f ∣ s ⟩= s₁ → ⟨ g ∣ s ⟩= s₂ → ⟨ ⟨ f , g ⟩ ∣ s ⟩= (s₁ , s₂)
  ev-p1 : ∀ {A B} {s₁ : CatCombValue A} {s₂ : CatCombValue B} → ⟨ p₁ ∣ s₁ , s₂ ⟩= s₁
  ev-p2 : ∀ {A B} {s₁ : CatCombValue A} {s₂ : CatCombValue B} → ⟨ p₂ ∣ s₁ , s₂ ⟩= s₂
--- EXPONENTIAL ---
  ev-cur : ∀ {A B C s} {f : CatComb (A × B) C} → ⟨ cur f ∣ s ⟩= cur f s
  ev-app : ∀ {A B C s t s₁} {f : CatComb (A × B) C} → ⟨ f ∣ s , t ⟩= s₁ → ⟨ app ∣ cur f s , t ⟩= s₁
--- COPRODUCT ---
  ev-copair1 : ∀ {A B C D s₁ s₂ t} {f : CatComb (A × B) D} {g : CatComb (A × C) D} → ⟨ f ∣ s₁ , s₂ ⟩= t → ⟨ [_,_] f g ∣ s₁ , L s₂ ⟩= t
  ev-copair2 : ∀ {A B C D s₁ s₂ t} {f : CatComb (A × B) D} {g : CatComb (A × C) D} → ⟨ g ∣ s₁ , s₂ ⟩= t → ⟨ [_,_] f g ∣ s₁ , R s₂ ⟩= t
  ev-i1 : ∀ {A B} {s : CatCombValue A} → ⟨ i1 {A} {B} ∣ s ⟩= (L s)
  ev-i2 : ∀ {A B} {s : CatCombValue B} → ⟨ i2 {A} {B} ∣ s ⟩= (R s)
--- LIST OBJECT ---
  ev-nil : ∀ {A} → ⟨ nil {A} ∣ ⟨⟩ ⟩= []
  ev-cons : ∀ {A} {h : CatCombValue A} {t : CatCombValue (list A)} → ⟨ cons ∣ h , t ⟩= (h ⦂ t)
  ev-it-nil : ∀ {A X P p s} {x : CatComb P X} {r : CatComb (P × (A × X)) X} → ⟨ x ∣ p ⟩= s → ⟨ it x r ∣ p , [] ⟩= s
  ev-it-cons : ∀ {A X P p s s' h t} {x : CatComb P X} {r : CatComb (P × (A × X)) X} → ⟨ it x r ∣ p , t ⟩= s' →  ⟨ r ∣ p , (h , s') ⟩= s → ⟨ it x r ∣ p , h ⦂ t ⟩= s
--- MONAD ---
  ev-ret : ∀ {A TA a t} {m : Monad {A} TA} → ⟨ getReturnImpl m ∣ a ⟩= t → ⟨ ret {m = m} ∣ a ⟩= t
  ev-bind : ∀ {A B TA TB a t} {ma : Monad {A} TA} {mb : Monad {B} TB} {s : SameMonad ma mb} → ⟨ getBindImpl s ∣ a ⟩= t → ⟨ bind {s = s} ∣ a ⟩= t

ev-it-id : ∀ {A l} → ⟨ it {A} id (cons ∘ p₂) ∣ [] , l ⟩= l
ev-it-id {l = []} = ev-it-nil ev-id
ev-it-id {l = l ⦂ l₁} = ev-it-cons ev-it-id (ev-comp ev-p2 ev-cons)

uniqueness : ∀ {A B s t t'} {f : CatComb A B} → ⟨ f ∣ s ⟩= t → ⟨ f ∣ s ⟩= t' → t ≡ t'
uniqueness ev-unit ev-unit = refl
uniqueness ev-nat ev-nat = refl
uniqueness ev-id ev-id = refl
uniqueness (ev-comp x x₁) (ev-comp y y₁) rewrite uniqueness x y = uniqueness x₁ y₁
uniqueness (ev-pair x x₁) (ev-pair {s₁ = s₁} y y₁) with uniqueness x y | uniqueness x₁ y₁
... | z | w rewrite z = cong (s₁ ,_) w
uniqueness ev-p1 ev-p1 = refl
uniqueness ev-p2 ev-p2 = refl
uniqueness ev-cur ev-cur = refl
uniqueness (ev-app x) (ev-app y) = uniqueness x y
--- COPRODUCT ---
uniqueness (ev-copair1 x) (ev-copair1 y) = uniqueness x y
uniqueness (ev-copair2 x) (ev-copair2 y) = uniqueness x y
uniqueness ev-i1 ev-i1 = refl
uniqueness ev-i2 ev-i2 = refl
--- LIST OBJECT ---
uniqueness ev-nil ev-nil = refl
uniqueness ev-cons ev-cons = refl
uniqueness (ev-it-nil x) (ev-it-nil y) = uniqueness x y
uniqueness (ev-it-cons {p = p} {s = s} {h = h} {r = r} x x₁) (ev-it-cons {s = s'} y y₁) with uniqueness x y
... | z rewrite cong (λ x → ⟨ r ∣ p , (h , x) ⟩= s) z = uniqueness x₁ y₁
--- MONAD ---
uniqueness (ev-ret x) (ev-ret y) = uniqueness x y
uniqueness (ev-bind x) (ev-bind y) = uniqueness x y

--- PATTERNS ---
pattern ev-swap = ev-pair ev-p2 ev-p1

pattern ev-bind-state x y z = (ev-comp (ev-pair (ev-pair (ev-comp ev-p1 ev-p1) ev-p2) (ev-comp ev-p1 ev-p2)) (ev-comp (ev-pair (ev-comp ev-p1 x) ev-p2) (ev-comp (ev-pair (ev-pair ev-p2 (ev-comp ev-p1 ev-p2)) (ev-comp ev-p1 ev-p1)) (ev-comp (ev-pair (ev-comp ev-p1 y) ev-p2) z))))

pattern ev-concatList-nil-left = ev-comp ev-swap (ev-it-nil ev-id)
pattern ev-concatList-cons-left x = ev-comp ev-swap (ev-it-cons x (ev-comp ev-p2 ev-cons))

pattern ev-fmap-nil = (ev-it-nil (ev-comp ev-unit ev-nil))
pattern ev-fmap-cons x x₁ = (ev-it-cons x (ev-comp (ev-pair (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 ev-p1)) (ev-app x₁)) (ev-comp ev-p2 ev-p2)) ev-cons))

pattern ev-flat-nil = ev-comp (ev-pair ev-unit ev-id) (ev-it-nil ev-nil)
pattern ev-flat-cons x x₁ = (ev-comp (ev-pair ev-unit ev-id) (ev-it-cons x (ev-comp ev-p2 x₁)))

pattern ev-ret-nondet = ev-comp (ev-pair ev-id (ev-comp ev-unit ev-nil)) ev-cons
pattern ev-bind-cont x = ev-comp (ev-pair (ev-comp ev-p1 ev-p1) ev-cur) x
pattern ev-p2p1p1-p2 = ev-pair (ev-comp ev-p1 (ev-comp ev-p1 ev-p2)) ev-p2