module stlc.monad.properities.common where

open import stlc.catComb.eval public

open import stlc.monad.impl public

open CatCombValue public

--- CONCATLIST ---
concatList-cons-left : ∀ {A h t t' u} → ⟨ concatList ∣ t , t' ⟩= u → ⟨ concatList {A} ∣ h ⦂ t , t' ⟩= (h ⦂ u)
concatList-cons-left (ev-comp ev-swap x) = ev-concatList-cons-left x

concatList-assoc : ∀ {A a b c u} → ⟨ concatList {A} ∘ ⟨ p₁ , concatList ∘ p₂ ⟩ ∣ (a , (b , c)) ⟩= u → ⟨ concatList ∘ ⟨ concatList ∘ p₁ , p₂ ⟩ ∣ ((a , b) , c) ⟩= u
concatList-assoc (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 x₂)) (ev-comp ev-swap (ev-it-nil ev-id))) = ev-comp (ev-pair (ev-comp ev-p1 ev-concatList-nil-left) ev-p2) x₂
concatList-assoc (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 x₂)) (ev-comp ev-swap (ev-it-cons x₃ (ev-comp ev-p2 ev-cons)))) with concatList-assoc (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 x₂)) (ev-comp ev-swap x₃))
... | ev-comp (ev-pair (ev-comp ev-p1 (ev-comp ev-swap w₁)) ev-p2) w₂ = ev-comp (ev-pair (ev-comp ev-p1 (ev-comp ev-swap (ev-it-cons w₁ (ev-comp ev-p2 ev-cons)))) ev-p2) (concatList-cons-left w₂)

--- FMAP ---
fmap-nil : ∀ {Γ A B s u} {f : CatComb (Γ × A) B} → ⟨ fmap ∣ cur f s , [] ⟩= u → ⟨ nil ∣ ⟨⟩ ⟩= u
fmap-nil ev-fmap-nil = ev-nil

fmap-cons : ∀ {Γ A B s h t u} {f : CatComb (Γ × A) B} → ⟨ fmap ∣ cur f s , h ⦂ t ⟩= u → ⟨ cons ∘ ⟨ f ∘ p₁ , fmap ∘ p₂ ⟩ ∣ (s , h) , (cur f s , t) ⟩= u
fmap-cons (ev-fmap-cons x x₁) = ev-comp (ev-pair (ev-comp ev-p1 x₁) (ev-comp ev-p2 x)) ev-cons

--- FLAT ---
flat-nil : ∀ {A u} → ⟨ flat {A} ∣ [] ⟩= u → ⟨ nil ∣ ⟨⟩ ⟩= u
flat-nil ev-flat-nil = ev-nil

flat-cons : ∀ {A h t u} → ⟨ flat {A} ∣ h ⦂ t ⟩= u → ⟨ concatList ∘ ⟨ p₁ , flat ∘ p₂ ⟩ ∣ h , t ⟩= u
flat-cons (ev-flat-cons x x₁) = ev-comp (ev-pair ev-p1 (ev-comp ev-p2 (ev-comp (ev-pair ev-unit ev-id) x))) x₁

flat-cons-rev : ∀ {A t u h u'} → ⟨ flat {A} ∣ t ⟩= u → ⟨ concatList ∣ h , u ⟩= u' → ⟨ flat ∣ h ⦂ t ⟩= u'
flat-cons-rev (ev-comp (ev-pair ev-unit ev-id) x) y = ev-comp (ev-pair ev-unit ev-id) (ev-it-cons x (ev-comp ev-p2 y))

--- FMAP CONCAT ---
fmap-concat : ∀ {Γ A B s a b u} {f : CatComb (Γ × A) B} → ⟨ fmap ∘ ⟨ p₁ , concatList ∘ p₂ ⟩ ∣ cur f s , (a , b) ⟩= u → ⟨ concatList ∘ ⟨ fmap ∘ p₁ , fmap ∘ p₂ ⟩ ∣ (cur f s , a) , (cur f s , b) ⟩= u
fmap-concat (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 (ev-comp ev-swap (ev-it-nil ev-id)))) x₁) = ev-comp (ev-pair (ev-comp ev-p1 ev-fmap-nil) (ev-comp ev-p2 x₁)) ev-concatList-nil-left
fmap-concat (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 (ev-comp ev-swap (ev-it-cons x₃ (ev-comp ev-p2 ev-cons))))) x₁) with (ev-comp (ev-pair (ev-comp ev-p1 q₁) (ev-comp ev-p2 q₃)) ev-cons) ← fmap-cons x₁ with fmap-concat (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 (ev-comp ev-swap x₃))) q₃)
... | ev-comp (ev-pair (ev-comp ev-p1 w) (ev-comp ev-p2 w₂)) w₁ = ev-comp (ev-pair (ev-comp ev-p1 (ev-it-cons w (ev-comp (ev-pair (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 ev-p1)) (ev-app q₁)) (ev-comp ev-p2 ev-p2)) ev-cons))) (ev-comp ev-p2 w₂)) (concatList-cons-left w₁)

--- FLAT CONCAT ---
flat-concat : ∀ {A a b u} → ⟨ flat ∘ (concatList {list A}) ∣ a , b ⟩= u → ⟨ concatList ∘ ⟨ flat ∘ p₁ , flat ∘ p₂ ⟩ ∣ a , b ⟩= u
flat-concat (ev-comp (ev-comp ev-swap (ev-it-nil ev-id)) x₁) = ev-comp (ev-pair (ev-comp ev-p1 ev-flat-nil) (ev-comp ev-p2 x₁)) ev-concatList-nil-left
flat-concat (ev-comp (ev-comp ev-swap (ev-it-cons x₂ (ev-comp ev-p2 ev-cons))) x₁) with flat-cons x₁
... | ev-comp (ev-pair ev-p1 (ev-comp ev-p2 q₁)) q₂ with flat-concat (ev-comp (ev-comp ev-swap x₂) q₁)
... | ev-comp (ev-pair (ev-comp ev-p1 w₁) (ev-comp ev-p2 w₂)) w₃ with concatList-assoc (ev-comp (ev-pair ev-p1 (ev-comp ev-p2 w₃)) q₂)
... | ev-comp (ev-pair (ev-comp ev-p1 e₁) ev-p2) e₂ = ev-comp (ev-pair (ev-comp ev-p1 (flat-cons-rev w₁ e₁)) (ev-comp ev-p2 w₂)) e₂

nondetBindImpl-nil : ∀ {Γ A B s u} {f : CatComb (Γ × A) (list B)} → ⟨ nondetBindImpl ∣ [] , cur f s ⟩= u → ⟨ nil ∣ ⟨⟩ ⟩= u
nondetBindImpl-nil (ev-comp ev-swap (ev-comp x₁ x₂)) with ev-nil ← fmap-nil x₁ with ev-nil ← flat-nil x₂ = ev-nil