module stlc.monad.properities.monadIdR where

open import stlc.monad.properities.common

open import stlc.value.properities

monadIdR-nondeterminism : ∀ {A A₁ s s₁ s₂ t t'} → ⟨ flat {A} ∣ s₂ ⟩= t → ⟨ fmap ∣ cur {A = A₁} (ret {m = nondeterminism} ∘ p₂) s , s₁ ⟩= s₂ → s₁ ≣ t' → t ≣ t'
monadIdR-nondeterminism {s₁ = []} ev-flat-nil ev-fmap-nil x₂ = x₂
monadIdR-nondeterminism {s₁ = s₁ ⦂ s₂} (ev-flat-cons x (ev-concatList-cons-left (ev-it-nil ev-id))) (ev-fmap-cons x₁ (ev-comp ev-p2 (ev-ret ev-ret-nondet))) (cons e₁ e₂) with e ← monadIdR-nondeterminism (ev-comp (ev-pair ev-unit ev-id) x) x₁ e₂ = cons e₁ e

monadIdR : ∀ {Γ A TA s s₁ t t'} {ma : Monad {A} TA} {saa : SameMonad ma ma} → ⟨ getBindImpl saa ∣ s₁ , cur {Γ} (ret {m = ma} ∘ p₂) s ⟩= t → s₁ ≣ t' → t ≣ t'
monadIdR {saa = exception} (ev-comp (ev-pair ev-p2 ev-p1) (ev-copair1 (ev-app (ev-comp ev-p2 (ev-ret ev-i1))))) e = e
monadIdR {saa = exception} (ev-comp (ev-pair ev-p2 ev-p1) (ev-copair2 (ev-comp ev-p2 ev-i2))) e = e
monadIdR {t' = cur g t} {saa = state} ev-cur (cur e) = cur (λ { x (ev-bind-state (ev-app x₁) (ev-app (ev-comp ev-p2 (ev-ret ev-cur))) (ev-app ev-swap)) x₂ → e x x₁ x₂})
monadIdR {saa = nondeterminism} (ev-comp ev-swap (ev-comp x₁ x₂)) e = monadIdR-nondeterminism x₂ x₁ e
monadIdR {t' = cur g t} {saa = continuation} ev-cur (cur e) = cur (λ { {cur h s} {cur h' s'} x (ev-bind-cont (ev-app x₁)) x₂ → e (λ { x₃ (ev-comp (ev-pair (ev-comp ev-p2p1p1-p2 (ev-app (ev-comp ev-p2 (ev-ret ev-cur)))) (ev-comp ev-p1 ev-p2)) (ev-app (ev-comp ev-swap (ev-app x₄)))) x₅ → x x₃ x₄ x₅}) x₁ x₂ })