module stlc.catComb.properities.propA where

open import stlc.monad.properities.common
open import stlc.catComb.properities.common

propA-bind-state : ∀ {A₁ A₂ A B S x y} → (f  : CatComb (A₁ × S) (S × A)) → (g  : CatComb (A₂ × A) (S ⇒ (S × B))) → (s₁ : CatCombValue S) → (x₁ : ⊩' s₁) → (ff : {s₁ = s₂ : CatCombValue S} → ⊩' s₂ → ∃-syntax (λ t → (⟨ f ∣ x , s₂ ⟩= t) ⊗ ⊩ t)) → (gg : {s₁ = s₂ : CatCombValue A} → ⊩' s₂ → ∃-syntax (λ t → (⟨ g ∣ y , s₂ ⟩= t) ⊗ ⊩ t)) → ∃[ t ] ⟨ app ∘ ⟨ app ∘ p₁ , p₂ ⟩ ∘ ⟨ ⟨ p₂ , p₂ ∘ p₁ ⟩ , p₁ ∘ p₁ ⟩ ∘ ⟨ app ∘ p₁ , p₂ ⟩ ∘ ⟨ ⟨ p₁ ∘ p₁ , p₂ ⟩ , p₂ ∘ p₁ ⟩ ∣ cur f x , cur g y , s₁ ⟩= t ⊗ ⊩ t
propA-bind-state f g s₁ x₁ ff gg with ff {s₁} x₁
... | ⦅ (tS , tA) , ⦅ e₁ , pair ⦅ stS , stA ⦆ ⦆ ⦆ with gg {tA} (_⇔_.to ⊩⇔⊩' stA)
... | ⦅ cur x a , ⦅ e₂ , cur hh ⦆ ⦆ with hh {tS} (_⇔_.to ⊩⇔⊩' stS)
... | ⦅ t , ⦅ e₃ , snd ⦆ ⦆ = ⦅ t , ⦅ ev-bind-state (ev-app e₁) (ev-app e₂) (ev-app e₃) , snd ⦆ ⦆

concatListValues : ∀ {A} → CatCombValue (list A) → CatCombValue (list A) → CatCombValue (list A)
concatListValues [] y = y
concatListValues (x ⦂ xs) y = x ⦂ (concatListValues xs y)

concatListEvValue : ∀ {A h tt} → ⟨ concatList {A} ∣ h , tt ⟩= concatListValues h tt
concatListEvValue {h = []} = ev-comp ev-swap (ev-it-nil ev-id)
concatListEvValue {h = h ⦂ hs} with (ev-comp ev-swap x) ← concatListEvValue {h = hs} = ev-comp ev-swap (ev-it-cons x (ev-comp ev-p2 ev-cons))

⊩concatListValues : ∀ {A h tt} → ⊩ h → ⊩ tt → ⊩ concatListValues {A} h tt
⊩concatListValues nil y = y
⊩concatListValues (cons x x₁) y = cons x (⊩concatListValues x₁ y)

propA-ret-cont : ∀ {A A₁ R s s₁} {h : CatComb (A₁ × A) R} → ∃-syntax (λ t → (⟨ h ∣ s₁ , s ⟩= t) ⊗ ⊩' t) → ∃-syntax (λ t → (⟨ app ∘ ⟨ p₂ , p₁ ⟩ ∣ s , cur h s₁ ⟩= t) ⊗ ⊩ t)
propA-ret-cont ⦅ t , ⦅ fst , snd ⦆ ⦆ = ⦅ t , ⦅ (ev-comp ev-swap (ev-app fst)) , (_⇔_.from ⊩⇔⊩' snd) ⦆ ⦆

propA-bind-cont2 : ∀ {A A₁ A₂ A₃ B C s s' s₁} {h : CatComb (A₁ × A ⇒ C) C} {h' : CatComb (A₂ × A) ((B ⇒ C) ⇒ C)} {h₁ : CatComb (A₃ × B) C} → (y  : {s₂ : CatCombValue A} → ⊩' s₂ → ∃-syntax (λ t → (⟨ h' ∣ s' , s₂ ⟩= t) ⊗ ⊩ t)) → (x₁ : {s₂ : CatCombValue B} → ⊩' s₂ → ∃-syntax (λ t → (⟨ h₁ ∣ s₁ , s₂ ⟩= t) ⊗ ⊩' t)) → ({s₂ : CatCombValue A} → ⊩' s₂ → ∃-syntax (λ t → (⟨ app ∘ ⟨ app ∘ ⟨ p₂ ∘ p₁ ∘ p₁ , p₂ ⟩ , p₂ ∘ p₁ ⟩ ∣ cur h s , cur h' s' , cur h₁ s₁ , s₂ ⟩= t) ⊗ ⊩' t))
propA-bind-cont2 y x₁ {s₂} x with y {s₂} x
... | ⦅ cur g st , ⦅ fst , cur x₂ ⦆ ⦆ with x₂ (λ {x₃ → x₁ x₃})
... | ⦅ t , ⦅ fst₁ , snd ⦆ ⦆ = ⦅ t , ⦅ (ev-comp (ev-pair (ev-comp ev-p2p1p1-p2 (ev-app fst)) (ev-comp ev-p1 ev-p2)) (ev-app fst₁)) , _⇔_.to ⊩⇔⊩' snd ⦆ ⦆

propA-bind-cont : ∀ {A A₁ A₂ A₃ B C s s' s₁} {h : CatComb (A₁ × A ⇒ C) C} {h' : CatComb (A₂ × A) ((B ⇒ C) ⇒ C)} {h₁ : CatComb (A₃ × B) C} → (x₁ : {s₂ : CatCombValue B} → ⊩' s₂ → ∃-syntax (λ t → (⟨ h₁ ∣ s₁ , s₂ ⟩= t) ⊗ ⊩' t)) → (y  : {s₂ : CatCombValue A} → ⊩' s₂ → ∃-syntax (λ t → (⟨ h' ∣ s' , s₂ ⟩= t) ⊗ ⊩ t)) → (x  : {s₂ : CatCombValue (A ⇒ C)} → ⊩' s₂ → ∃-syntax (λ t → (⟨ h ∣ s , s₂ ⟩= t) ⊗ ⊩ t)) → ∃-syntax (λ t → (⟨ app ∘ ⟨ p₁ ∘ p₁ , cur (app ∘ ⟨ app ∘ ⟨ p₂ ∘ p₁ ∘ p₁ , p₂ ⟩ , p₂ ∘ p₁ ⟩) ⟩ ∣ cur h s , cur h' s' , cur h₁ s₁ ⟩= t) ⊗ ⊩ t)
propA-bind-cont {s = s} {s'} {s₁} {h} {h'} {h₁} x₁ y x with x {s₂ = cur (app ∘ ⟨ app ∘ ⟨ p₂ ∘ p₁ ∘ p₁ , p₂ ⟩ , p₂ ∘ p₁ ⟩) (cur h s , cur h' s' , cur h₁ s₁)} (propA-bind-cont2 y x₁)
... | ⦅ t , ⦅ fst , snd ⦆ ⦆ = ⦅ t , ⦅ ev-bind-cont (ev-app fst) , snd ⦆ ⦆

propA : ∀ {A B s} → (f : CatComb A B) → ⊩ s → ∃[ t ] ⟨ f ∣ s ⟩= t ⊗ (⊩ t)
propA ! _ = ⦅ ⟨⟩ , ⦅ ev-unit , unit ⦆ ⦆
propA (nat n) _ = ⦅ (`nat n) , ⦅ ev-nat , nat ⦆ ⦆
propA {s = s} id x = ⦅ s , ⦅ ev-id , x ⦆ ⦆
propA (f ∘ g) x with propA g x
... | ⦅ _ , ⦅ x₁ , x₂ ⦆ ⦆ with propA f x₂
... | ⦅ t , ⦅ y₁ , y₂ ⦆ ⦆ = ⦅ t , ⦅ ev-comp x₁ y₁ , y₂ ⦆ ⦆
--- PRODUCT ---
propA ⟨ f , g ⟩ x with propA f x | propA g x
... | ⦅ t₁ , ⦅ x₁ , x₂ ⦆ ⦆ | ⦅ t₂ , ⦅ y₁ , y₂ ⦆ ⦆ = ⦅ (t₁ , t₂) , (⦅ ev-pair x₁ y₁ , pair ⦅ x₂ , y₂ ⦆ ⦆) ⦆
propA {s = s₁ , _} p₁ (pair ⦅ fst₁ , snd₁ ⦆) = ⦅ s₁ , ⦅ ev-p1 , fst₁ ⦆ ⦆
propA {s = _ , s₂} p₂ (pair ⦅ fst₁ , snd₁ ⦆) = ⦅ s₂ , ⦅ ev-p2 , snd₁ ⦆ ⦆
--- EXPONENTIAL ---
propA {s = s} (cur f) x = ⦅ (cur f s) , ⦅ ev-cur , cur (λ {s₁ → propA f (pair ⦅ x , _⇔_.from ⊩⇔⊩' s₁ ⦆)} ) ⦆ ⦆
propA app (pair ⦅ cur f , x ⦆) with f (_⇔_.to ⊩⇔⊩' x)
... | ⦅ t , ⦅ x₁ , x₂ ⦆ ⦆ = ⦅ t , ⦅ ev-app x₁ , x₂ ⦆ ⦆
--- COPRODUCT ---
propA [ f , g ] (pair ⦅ e , inl y ⦆) with propA f (pair ⦅ e , y ⦆)
... | ⦅ t , ⦅ x₁ , x₂ ⦆ ⦆ = ⦅ t , ⦅ ev-copair1 x₁ , x₂ ⦆ ⦆
propA [ f , g ] (pair ⦅ e , inr y ⦆) with propA g (pair ⦅ e , y ⦆)
... | ⦅ t , ⦅ x₁ , x₂ ⦆ ⦆ = ⦅ t , ⦅ ev-copair2 x₁ , x₂ ⦆ ⦆
propA {s = s} i1 z = ⦅ L s , ⦅ ev-i1 , inl z ⦆ ⦆
propA {s = s} i2 z = ⦅ R s , ⦅ ev-i2 , inr z ⦆ ⦆
--- LIST OBJECT ---
propA {s = ⟨⟩} (nil) _ = ⦅ [] , ⦅ ev-nil , nil ⦆ ⦆
propA {s = h , t} cons (pair x) = ⦅ h ⦂ t , ⦅ ev-cons , cons (proj₁ x) (proj₂ x) ⦆ ⦆
propA {s = p , []} (it x r) (pair x₁) with propA x (proj₁ x₁)
... | ⦅ s , z ⦆ = ⦅ s , ⦅ (ev-it-nil (proj₁ z)) , (proj₂ z) ⦆ ⦆
propA {s = p , h ⦂ t} (it x r) (pair ⦅ snd , cons fst fst₁ ⦆) with propA {s = p , t} (it x r) (pair ⦅ snd , fst₁ ⦆)
... | ⦅ s' , z ⦆ with propA {s = p , (h , s')} r (pair ⦅ snd , pair ⦅ fst , proj₂ z ⦆ ⦆)
... | ⦅ s , w ⦆ = ⦅ s , ⦅ ev-it-cons (proj₁ z) (proj₁ w) , proj₂ w ⦆ ⦆
--- MONAD ---
propA {s = s} (ret {m = exception}) x = ⦅ L s , ⦅ ev-ret ev-i1 , inl x ⦆ ⦆
propA {s = s} (ret {m = state}) x = ⦅ cur ⟨ p₂ , p₁ ⟩ s , ⦅ (ev-ret ev-cur) , cur (λ {s₁} x₁ → ⦅ (s₁ , s) , ⦅ (ev-pair ev-p2 ev-p1) , (pair ⦅ _⇔_.from ⊩⇔⊩' x₁ , x ⦆) ⦆ ⦆) ⦆ ⦆
propA {s = s} (ret {m = nondeterminism}) x = ⦅ (s ⦂ []) , ⦅ (ev-ret (ev-comp (ev-pair ev-id (ev-comp ev-unit ev-nil)) ev-cons)) , (cons x nil) ⦆ ⦆
propA {s = s} (ret {m = continuation}) x = ⦅ cur (app ∘ ⟨ p₂ , p₁ ⟩) s , ⦅ (ev-ret ev-cur) , cur (λ { {cur h s₁} x₁ → propA-ret-cont (x₁ (_⇔_.to ⊩⇔⊩' x)) }) ⦆ ⦆
propA {s = L s , cur x₁ s₁} (bind {s = exception}) (pair ⦅ inl fst , cur x ⦆) with x {s₁ = s} (_⇔_.to ⊩⇔⊩' fst)
... | ⦅ fst₁ , ⦅ fst₂ , snd ⦆ ⦆ = ⦅ fst₁ , ⦅ (ev-bind (ev-comp (ev-pair ev-p2 ev-p1) (ev-copair1 (ev-app fst₂)))) , snd ⦆ ⦆
propA {s = R s , cur x₁ s₁} (bind {s = exception}) (pair ⦅ inr fst , snd ⦆) = ⦅ R s , ⦅ (ev-bind (ev-comp (ev-pair ev-p2 ev-p1) (ev-copair2 (ev-comp ev-p2 ev-i2)))) , inr fst ⦆ ⦆
propA {s = cur {B = S} f x , cur g y} (bind {A} {B} {s = state}) (pair ⦅ cur ff , cur gg ⦆) = ⦅ (cur (app ∘ ⟨ app ∘ p₁ , p₂ ⟩ ∘ ⟨ ⟨ p₂ , p₂ ∘ p₁ ⟩ , p₁ ∘ p₁ ⟩ ∘ ⟨ app ∘ p₁ , p₂ ⟩ ∘ ⟨ ⟨ p₁ ∘ p₁ , p₂ ⟩ , p₂ ∘ p₁ ⟩) ((cur f x) , (cur g y))) , ⦅ (ev-bind ev-cur) , (cur (λ {s₁} x₁ → propA-bind-state f g s₁ x₁ ff gg)) ⦆ ⦆
propA (bind {A} {B} {s = nondeterminism}) (pair {s = []} {t = cur x t} ⦅ fst , snd ⦆) = ⦅ [] , ⦅ (ev-bind (ev-comp ev-swap (ev-comp ev-fmap-nil ev-flat-nil))) , nil ⦆ ⦆
propA (bind {A} {B} {s = nondeterminism}) (pair {s = s ⦂ s₁} {t = cur x t} ⦅ cons fst fst₁ , cur snd₁ ⦆) with propA (bind {A} {B} {s = nondeterminism}) (pair {s = s₁} {t = cur x t} ⦅ fst₁ , cur snd₁ ⦆) | snd₁ {s} (_⇔_.to ⊩⇔⊩' fst)
... | ⦅ tt , ⦅ ev-bind (ev-comp ev-swap (ev-comp fmap_s₁ flat_fmap_s₁)) , snd₂ ⦆ ⦆ | ⦅ h , ⦅ fst₃ , snd₃ ⦆ ⦆ = ⦅ concatListValues h tt , ⦅ (ev-bind (ev-comp ev-swap (ev-comp (ev-it-cons fmap_s₁ (ev-comp (ev-pair (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 ev-p1)) (ev-app fst₃)) (ev-comp ev-p2 ev-p2)) ev-cons)) (flat-cons-rev flat_fmap_s₁ concatListEvValue)))) , ⊩concatListValues snd₃ snd₂ ⦆ ⦆
propA {s = cur h s , cur h' s'} (bind {A} {B} {s = continuation}) (pair ⦅ cur x , cur y ⦆) = ⦅ cur (app ∘ ⟨ p₁ ∘ p₁ , cur (app ∘ ⟨ app ∘ ⟨ p₂ ∘ p₁ ∘ p₁ , p₂ ⟩ , p₂ ∘ p₁ ⟩) ⟩) (cur h s , cur h' s') , ⦅ (ev-bind ev-cur) , (cur λ { {cur h₁ s₁} x₁ → propA-bind-cont x₁ y x } ) ⦆ ⦆