module stlc.monad.properities.monadAssoc where

open import stlc.monad.properities.common

open import stlc.value.properities

monadAssoc-state : ∀ {Γ A A₁ A₂ A₃ A₄ B B₁ C s s' s'' s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ s₉ s₁₀ s₁₁ s₁₂ s₁₃ s₁₄ s₁₅ s₁₆ s₁₇ s₁₈ s₁₉ t t'} {f : CatComb (A₄ × B₁) (B₁ × A)} {f₁  : CatComb (A₁ × B) (B₁ ⇒ (B₁ × C))} {h   : CatComb Γ (B ⇒ B₁ ⇒ (B₁ × C))} {f₂  : CatComb (A₂ × A) (B₁ ⇒ (B₁ × B))} {g   : CatComb Γ (A ⇒ B₁ ⇒ (B₁ × B))} {f'  : CatComb (A₃ × B₁) (B₁ × A)} → ⟨ app ∣ s₁₉ , s₁₇ ⟩= t' → ⟨ app ∣ s₁₅ , s₁₈ ⟩= s₁₉ → ⟨ app ∣ s₁₄ , s₁₂ ⟩= (s₁₇ , s₁₈) → ⟨ h ∣ s'' ⟩= s₁₅ → ⟨ app ∣ s₁₆ , s₁₃ ⟩= s₁₄ → ⟨ g ∣ s'' ⟩= s₁₆ → ⟨ g ∣ s ⟩= cur f₂ s₂ → ⟨ h ∣ s ⟩= cur f₁ s₁ → ⟨ f ∣ s₁₁ , s₁₀ ⟩= (s₁₂ , s₁₃) → ⟨ app ∣ s₉ , s₇ ⟩= t → ⟨ f₁ ∣ s₁ , s₈ ⟩= s₉ → ⟨ app ∣ s₆ , s₄ ⟩= (s₇ , s₈) → ⟨ f₂ ∣ s₂ , s₅ ⟩= s₆ → ⟨ f' ∣ s' , s₃ ⟩= (s₄ , s₅) → s₃ ≣' s₁₀ → cur f' s' ≣ cur f s₁₁ → s ≣ s'' → t ≣ t'
monadAssoc-state x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁ x₁₂ x₁₃ e₁ (cur e₂) e₃ with pair e₄ e₅ ← e₂ e₁ x₁₃ x₈ with cur e₆ ← ≣injective x₆ x₅ e₃ with ev-app x₄ ← x₄ with e₇ ← e₆ (_⇔_.to ≣⇔≣' e₅) x₁₂ x₄ with pair e₈ e₉ ← ≣injective x₁₁ x₂ (pair e₇ e₄) with cur e₁₀ ← ≣injective x₇ x₃ e₃ with ev-app x₁ ← x₁ with e₁₁ ← e₁₀ (_⇔_.to ≣⇔≣' e₉) x₁₀ x₁ = ≣injective x₉ x (pair e₁₁ e₈)

monadAssoc-cont : ∀ {Γ A A₁ A₂ A₃ A₄ B C C₁ s s' s''' s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ s₉ s₁₀ t t'} {f : CatComb (A₄ × B ⇒ C) C} {f₁ : CatComb (A₁ × B) ((C₁ ⇒ C) ⇒ C)} {f₂  : CatComb (A₂ × A) ((B ⇒ C) ⇒ C)} {g : CatComb Γ (A ⇒ (B ⇒ C) ⇒ C)} {h   : CatComb (A₃ × A ⇒ C) C} {h₁  : CatComb Γ (B ⇒ (C₁ ⇒ C) ⇒ C)} → ⟨ app ∘ ⟨ p₁ ∘ p₁ , cur (app ∘ ⟨ app ∘ ⟨ p₂ ∘ p₁ ∘ p₁ , p₂ ⟩ , p₂ ∘ p₁ ⟩) ⟩ ∣ s₈ , s₉ , s₆ ⟩= t' → ⟨ h₁ ∣ s''' ⟩= s₉ → ⟨ app ∣ s₁₀ , s₇ ⟩= s₈ → ⟨ g ∣ s''' ⟩= s₁₀ → ⟨ g ∣ s ⟩= cur f₂ s₂ → ⟨ h₁ ∣ s ⟩= cur f₁ s₁ → ⟨ f ∣ s₅ , cur (app ∘ ⟨ app ∘ ⟨ p₂ ∘ p₁ ∘ p₁ , p₂ ⟩ , p₂ ∘ p₁ ⟩) (cur (app ∘ ⟨ p₁ ∘ p₁ , cur (app ∘ ⟨ app ∘ ⟨ p₂ ∘ p₁ ∘ p₁ , p₂ ⟩ , p₂ ∘ p₁ ⟩) ⟩) (cur h s' , cur f₂ s₂) , cur f₁ s₁ , s₃) ⟩= t → ⟨ f₂ ∣ s₂ , s₄ ⟩= cur f s₅ → s₄ ≣' s₇ → s₃ ≣ s₆ → s ≣ s''' → t ≣' t'
monadAssoc-cont x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ e₁ with cur e₂ ← ≣injective x₅ x₁ e₁ with cur e₃ ← ≣injective x₄ x₃ e₁ with ev-app x₂ ← x₂ with cur e₄ ← e₃ x₈ x₇ x₂ with ev-bind-cont (ev-app x) ← x = _⇔_.to ≣⇔≣' (e₄ (λ { x₁₁ (ev-comp (ev-pair (ev-comp ev-p2p1p1-p2 (ev-app x₁₂)) (ev-comp ev-p1 ev-p2)) x₁₄) (ev-comp (ev-pair (ev-comp ev-p2p1p1-p2 (ev-app x₁₃)) (ev-comp ev-p1 ev-p2)) x₁₅) → _⇔_.to ≣⇔≣' (≣injective x₁₄ x₁₅ (pair (e₂ x₁₁ x₁₂ x₁₃) x₉))}) x₆ x)

monadAssoc : ∀ {Γ A A₁ A₂ B C TA TB TC s s' s₁ s₂ s₃ s₄ s₅ t t'} {g : CatComb Γ (A ⇒ TB)} {h : CatComb Γ (B ⇒ TC)} {f₁ : CatComb (A₁ × B) TC} {f₂ : CatComb (A₂ × A) TB} {ma : Monad {A} TA} {mb : Monad {B} TB} {mc : Monad {C} TC} {sab : SameMonad ma mb} {sbc : SameMonad mb mc} → ⟨ getBindImpl (sameMonadTrans sab sbc) ∣ s₄ , cur (bind {s = sbc} ∘ ⟨ app ∘ ⟨ g ∘ p₁ , p₂ ⟩ , h ∘ p₁ ⟩) s' ⟩= t' → ⟨ getBindImpl sbc ∣ s₅ , cur f₁ s₁ ⟩= t → ⟨ h ∣ s ⟩= cur f₁ s₁ → ⟨ getBindImpl sab ∣ s₃ , cur f₂ s₂ ⟩= s₅ → ⟨ g ∣ s ⟩= cur f₂ s₂ → s ≣ s' → s₃ ≣ s₄ → t ≣ t'
--- EXCEPTION ---
monadAssoc {sab = exception} {exception} (ev-comp ev-swap (ev-copair1 (ev-app (ev-comp (ev-pair (ev-comp (ev-pair (ev-comp ev-p1 x₁) ev-p2) x₃) (ev-comp ev-p1 x₄)) (ev-bind (ev-comp ev-swap x₂)))))) (ev-comp ev-swap y₁) z (ev-comp ev-swap (ev-copair1 (ev-app w₁))) q e₁ (inl e₂) with cur e₃ ← ≣injective q x₁ e₁ with ev-app x₃ ← x₃ with e₄ ← e₃ (_⇔_.to ≣⇔≣' e₂) w₁ x₃ with e₅ ← ≣injective z x₄ e₁ = ≣injective y₁ x₂ (pair e₅ e₄)
monadAssoc {sab = exception} {exception} (ev-comp ev-swap (ev-copair2 (ev-comp ev-p2 ev-i2))) (ev-comp ev-swap (ev-copair2 (ev-comp ev-p2 ev-i2))) z (ev-comp ev-swap (ev-copair2 (ev-comp ev-p2 ev-i2))) q e₁ (inr e₂) = inr e₂
--- STATE ---
monadAssoc {s₃ = cur f' s'} {sab = state} {state} ev-cur ev-cur z ev-cur q e₁ e₂ = cur (λ { x (ev-bind-state (ev-app (ev-bind-state (ev-app x₁) (ev-app x₄) x₅)) (ev-app x₂) x₃) (ev-bind-state (ev-app y₁) (ev-app (ev-comp (ev-pair (ev-comp (ev-pair (ev-comp ev-p1 y₂) ev-p2) y₄) (ev-comp ev-p1 y₅)) (ev-bind ev-cur))) (ev-app (ev-bind-state z₁ z₂ z₃))) →  monadAssoc-state z₃ z₂ z₁ y₅ y₄ y₂ q z y₁ x₃ x₂ x₅ x₄ x₁ x e₂ e₁})
--- NONDETERMINISM ---
monadAssoc {s₃ = []} {sab = nondeterminism} {nondeterminism} x y z w q e nil with ev-nil ← nondetBindImpl-nil w | ev-nil ← nondetBindImpl-nil x with ev-nil ← nondetBindImpl-nil y = nil
monadAssoc {s₃ = m ⦂ t} {sab = nondeterminism} {nondeterminism} (ev-comp ev-swap (ev-comp fmap_d_m⦂t flat_fmap_d_m⦂t)) (ev-comp ev-swap (ev-comp fmap_h flat_fmap_h)) z (ev-comp ev-swap (ev-comp fmap_g_m⦂t flat_fmap_g_m⦂t)) q e₁ (cons e₂ e₃) with fmap-cons fmap_g_m⦂t
... | ev-comp (ev-pair (ev-comp ev-p1 g_m) (ev-comp ev-p2 fmap_g_t)) ev-cons with flat-cons flat_fmap_g_m⦂t
... | ev-comp (ev-pair ev-p1 (ev-comp ev-p2 flat_fmap_g_t)) g_m++flat_fmap_g_t with fmap-concat (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 g_m++flat_fmap_g_t)) fmap_h)
... | ev-comp (ev-pair (ev-comp ev-p1 fmap_h_g_m) (ev-comp ev-p2 fmap_h_flat_fmap_g_t)) fmap_h_g_m++fmap_h_flat_fmap_g_t with flat-concat (ev-comp fmap_h_g_m++fmap_h_flat_fmap_g_t flat_fmap_h)
... | ev-comp (ev-pair (ev-comp ev-p1 flat_fmap_h_g_m) (ev-comp ev-p2 flat_fmap_h_flat_fmap_g_t)) flat_fmap_h_g_m++flat_fmap_h_flat_fmap_g_t with fmap-cons fmap_d_m⦂t
... | ev-comp (ev-pair (ev-comp ev-p1 (ev-comp (ev-pair (ev-comp (ev-pair (ev-comp ev-p1 g) ev-p2) app_g_m) (ev-comp ev-p1 h)) (ev-bind (ev-comp ev-swap (ev-comp fmap_h_g_m₂ flat_fmap_h_g_m₂))))) (ev-comp ev-p2 fmap_d_t)) ev-cons with e₄ ← ≣injective z h e₁ with cur e₅ ← ≣injective q g e₁ with ev-app g_m₂ ← app_g_m with e₆ ← e₅ (_⇔_.to ≣⇔≣' e₂) g_m g_m₂ with flat-cons flat_fmap_d_m⦂t
... | ev-comp (ev-pair ev-p1 (ev-comp ev-p2 flat_fmap_d_t)) flat_fmap_h_g_m₂++flat_fmap_d_t with e₇ ← ≣injective fmap_h_g_m fmap_h_g_m₂ (pair e₄ e₆) with e₈ ← ≣injective flat_fmap_h_g_m flat_fmap_h_g_m₂ e₇ with monadAssoc {s₃ = t} {sab =  nondeterminism} {nondeterminism} (ev-comp ev-swap (ev-comp fmap_d_t flat_fmap_d_t)) (ev-comp ev-swap (ev-comp fmap_h_flat_fmap_g_t flat_fmap_h_flat_fmap_g_t)) z (ev-comp ev-swap (ev-comp fmap_g_t flat_fmap_g_t)) q e₁ e₃
... | ww = ≣injective flat_fmap_h_g_m++flat_fmap_h_flat_fmap_g_t flat_fmap_h_g_m₂++flat_fmap_d_t (pair e₈ ww)
--- CONTINUATION ---
monadAssoc {s₃ = cur h s'} {sab = continuation} {continuation} ev-cur ev-cur x₂ ev-cur x₄ e₁ (cur e₂) = cur (λ { x (ev-bind-cont (ev-app (ev-bind-cont (ev-app x₁)))) (ev-bind-cont (ev-app x₃)) → e₂ (λ { x₅ (ev-comp (ev-pair (ev-comp ev-p2p1p1-p2 (ev-app x₈)) (ev-comp ev-p1 ev-p2)) (ev-app x₆)) (ev-comp (ev-pair (ev-comp ev-p2p1p1-p2 (ev-app (ev-comp (ev-pair (ev-comp (ev-pair (ev-comp ev-p1 x₁₂) ev-p2) x₁₁) (ev-comp ev-p1 x₁₀)) (ev-bind ev-cur)))) (ev-comp ev-p1 ev-p2)) (ev-app x₇)) → monadAssoc-cont x₇ x₁₀ x₁₁ x₁₂ x₄ x₂ x₆ x₈ x₅ (_⇔_.from ≣⇔≣' x) e₁}) x₁ x₃})