------------------------------------------------------------------------
-- Laws related to _>>=_
------------------------------------------------------------------------

module TotalParserCombinators.Laws.Monad where

open import Algebra
open import Codata.Musical.Notation
open import Data.List
open import Data.List.Effectful
  using () renaming (module MonadProperties to ListMonad)
import Data.List.Relation.Binary.BagAndSetEquality as BSEq
open import Effect.Monad
open import Function
open import Level

private
  module BagMonoid {k} {A : Set} =
    CommutativeMonoid (BSEq.commutativeMonoid k A)
  open RawMonad {f = zero} Data.List.Effectful.monad
    using () renaming (_>>=_ to _>>=′_)

open import TotalParserCombinators.Derivative
open import TotalParserCombinators.Congruence as Eq
  hiding (return; fail) renaming (_∣_ to _∣′_)
import TotalParserCombinators.Laws.AdditiveMonoid as AdditiveMonoid
open import TotalParserCombinators.Laws.Derivative as Derivative
open import TotalParserCombinators.Laws.ReturnStar as Return⋆
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser

------------------------------------------------------------------------
-- _>>=_, return, _∣_ and fail form a monad with a zero and a plus

-- If the laws below are combined with the additive monoid laws this
-- means that we have something which resembles an idempotent semiring
-- (if we restrict ourselves to language equivalence).

-- The zero laws are proved elsewhere.

open Derivative public
  using () renaming (left-zero->>=  to left-zero;
                     right-zero->>= to right-zero)

left-distributive :  {Tok R₁ R₂ xs} {f g : R₁  List R₂}
                    (p₁ : Parser Tok R₁ xs)
                    (p₂ : (x : R₁)  Parser Tok R₂ (f x))
                    (p₃ : (x : R₁)  Parser Tok R₂ (g x)) 
                    p₁ >>=  x  p₂ x  p₃ x) ≅P p₁ >>= p₂  p₁ >>= p₃
left-distributive {xs = xs} {f} {g} p₁ p₂ p₃ =
  BSEq.>>=-left-distributive xs {f = f}  λ t   (
    D t (p₁ >>=  x  p₂ x  p₃ x))                       ≅⟨ D->>= p₁  x  p₂ x  p₃ x) 

    D t p₁ >>=  x  p₂ x  p₃ x) 
    return⋆ xs >>=  x  D t (p₂ x)  D t (p₃ x))         ≅⟨ left-distributive (D t p₁) p₂ p₃ ∣′
                                                              left-distributive (return⋆ xs)
                                                                 x  D t (p₂ x))  x  D t (p₃ x)) 
    (D t p₁ >>= p₂  D t p₁ >>= p₃) 
    (return⋆ xs >>=  x  D t (p₂ x)) 
     return⋆ xs >>=  x  D t (p₃ x)))                    ≅⟨ AdditiveMonoid.swap
                                                               (D t p₁ >>= p₂) (D t p₁ >>= p₃)
                                                               (return⋆ xs >>=  x  D t (p₂ x)))
                                                               (return⋆ xs >>=  x  D t (p₃ x))) 
    (D t p₁ >>= p₂  return⋆ xs >>=  x  D t (p₂ x))) 
    (D t p₁ >>= p₃  return⋆ xs >>=  x  D t (p₃ x)))    ≅⟨ sym (D->>= p₁ p₂ ∣′ D->>= p₁ p₃) 

    D t (p₁ >>= p₂)  D t (p₁ >>= p₃)                      )

right-distributive :  {Tok R₁ R₂ xs₁ xs₂} {f : R₁  List R₂}
                     (p₁ : Parser Tok R₁ xs₁)
                     (p₂ : Parser Tok R₁ xs₂)
                     (p₃ : (x : R₁)  Parser Tok R₂ (f x)) 
                     (p₁  p₂) >>= p₃ ≅P p₁ >>= p₃  p₂ >>= p₃
right-distributive {xs₁ = xs₁} {xs₂} {f} p₁ p₂ p₃ =
  BagMonoid.reflexive (ListMonad.right-distributive xs₁ xs₂ f)  λ t   (
    D t ((p₁  p₂) >>= p₃)                                  ≅⟨ D->>= (p₁  p₂) p₃ 

    (D t p₁  D t p₂) >>= p₃ 
    return⋆ (xs₁ ++ xs₂) >>=  x  D t (p₃ x))             ≅⟨ ((D t p₁  D t p₂) >>= p₃ ) ∣′
                                                               [  -  -  -  ] Return⋆.distrib-∣ xs₁ xs₂ >>=
                                                                                  x  D t (p₃ x) ) 
    (D t p₁  D t p₂) >>= p₃ 
    (return⋆ xs₁  return⋆ xs₂) >>=  x  D t (p₃ x))      ≅⟨ right-distributive (D t p₁) (D t p₂) p₃ ∣′
                                                               right-distributive (return⋆ xs₁) (return⋆ xs₂)
                                                                                   x  D t (p₃ x)) 
    ((D t p₁ >>= p₃)  (D t p₂ >>= p₃)) 
    (return⋆ xs₁ >>=  x  D t (p₃ x)) 
     return⋆ xs₂ >>=  x  D t (p₃ x)))                    ≅⟨ AdditiveMonoid.swap
                                                                 (D t p₁ >>= p₃) (D t p₂ >>= p₃)
                                                                 (return⋆ xs₁ >>=  x  D t (p₃ x)))
                                                                 (return⋆ xs₂ >>=  x  D t (p₃ x))) 
    (D t p₁ >>= p₃  return⋆ xs₁ >>=  x  D t (p₃ x))) 
    (D t p₂ >>= p₃  return⋆ xs₂ >>=  x  D t (p₃ x)))    ≅⟨ sym (D->>= p₁ p₃ ∣′ D->>= p₂ p₃) 

    D t (p₁ >>= p₃)  D t (p₂ >>= p₃)                       )

left-identity :  {Tok R₁ R₂} {f : R₁  List R₂}
                (x : R₁) (p : (x : R₁)  Parser Tok R₂ (f x)) 
                return x >>= p ≅P p x
left-identity {f = f} x p =
  BagMonoid.reflexive (ListMonad.left-identity x f)  λ t   (
    D t (return x >>= p)                              ≅⟨ D->>= (return x) p 
    fail >>= p  return⋆ [ x ] >>=  x  D t (p x))  ≅⟨ left-zero p ∣′
                                                         [  -  -  -  ] AdditiveMonoid.right-identity (return x) >>=
                                                                            x  D t (p x) ) 
    fail  return x >>=  x  D t (p x))             ≅⟨ AdditiveMonoid.left-identity (return x >>=  x  D t (p x))) 
    return x >>=  x  D t (p x))                    ≅⟨ left-identity x  x  D t (p x)) 
    D t (p x)                                         )

right-identity :  {Tok R xs}
                 (p : Parser Tok R xs)  p >>= return ≅P p
right-identity {xs = xs} p =
  BagMonoid.reflexive (ListMonad.right-identity xs)  λ t   (
    D t (p >>= return)                              ≅⟨ D->>= p return 
    D t p >>= return  return⋆ xs >>=  _  fail)  ≅⟨ right-identity (D t p) ∣′ right-zero (return⋆ xs) 
    D t p             fail                         ≅⟨ AdditiveMonoid.right-identity (D t p) 
    D t p                                           )

associative :  {Tok R₁ R₂ R₃ xs}
                {f : R₁  List R₂} {g : R₂  List R₃}
              (p₁ : Parser Tok R₁ xs)
              (p₂ : (x : R₁)  Parser Tok R₂ (f x))
              (p₃ : (x : R₂)  Parser Tok R₃ (g x)) 
              p₁ >>=  x  p₂ x >>= p₃) ≅P p₁ >>= p₂ >>= p₃
associative {xs = xs} {f} {g} p₁ p₂ p₃ =
  BagMonoid.reflexive (ListMonad.associative xs f g)  λ t   (
    D t (p₁ >>= λ x  p₂ x >>= p₃)                               ≅⟨ D->>= p₁  x  p₂ x >>= p₃) 

    D t p₁ >>=  x  p₂ x >>= p₃) 
    return⋆ xs >>=  x  D t (p₂ x >>= p₃))                     ≅⟨ associative (D t p₁) p₂ p₃ ∣′
                                                                    [  -  -  -  ] return⋆ xs  >>=  x  D->>= (p₂ x) p₃) 
    D t p₁ >>= p₂ >>= p₃ 
    return⋆ xs >>=
       x  D t (p₂ x) >>= p₃ 
             return⋆ (f x) >>= λ x  D t (p₃ x))                 ≅⟨ (D t p₁ >>= p₂ >>= p₃ ) ∣′
                                                                    left-distributive (return⋆ xs)
                                                                                       x  D t (p₂ x) >>= p₃)
                                                                                       x  return⋆ (f x) >>=  x  D t (p₃ x))) 
    D t p₁ >>= p₂ >>= p₃ 
    (return⋆ xs >>=  x  D t (p₂ x) >>= p₃) 
     return⋆ xs >>=  x  return⋆ (f x) >>= λ x  D t (p₃ x)))  ≅⟨ (D t p₁ >>= p₂ >>= p₃ ) ∣′
                                                                    (associative (return⋆ xs)  x  D t (p₂ x)) p₃ ∣′
                                                                     associative (return⋆ xs) (return⋆  f)  x  D t (p₃ x))) 
    D t p₁ >>= p₂ >>= p₃ 
    (return⋆ xs >>=  x  D t (p₂ x)) >>= p₃ 
     return⋆ xs >>= (return⋆  f) >>= λ x  D t (p₃ x))          ≅⟨ sym $ AdditiveMonoid.associative
                                                                            (D t p₁ >>= p₂ >>= p₃)
                                                                            (return⋆ xs >>=  x  D t (p₂ x)) >>= p₃)
                                                                            (return⋆ xs >>= (return⋆  f) >>=  x  D t (p₃ x))) 
    D t p₁ >>= p₂ >>= p₃ 
    return⋆ xs >>=  x  D t (p₂ x)) >>= p₃ 
    return⋆ xs >>= (return⋆  f) >>=  x  D t (p₃ x))          ≅⟨ sym (right-distributive
                                                                           (D t p₁ >>= p₂)
                                                                           (return⋆ xs >>=  x  D t (p₂ x)))
                                                                           p₃) ∣′
                                                                    [  -  -  -  ] sym (Return⋆.distrib->>= xs f) >>=
                                                                                       x  D t (p₃ x) ) 
    (D t p₁ >>= p₂ 
     return⋆ xs >>=  x  D t (p₂ x))) >>= p₃ 
    return⋆ (xs >>=′ f) >>=  x  D t (p₃ x))                   ≅⟨ [  -  -  -  ] sym (D->>= p₁ p₂) >>=  x  p₃ x ) ∣′
                                                                    (return⋆ (xs >>=′ f) >>=  x  D t (p₃ x)) ) 
    D t (p₁ >>= p₂) >>= p₃ 
    return⋆ (xs >>=′ f) >>=  x  D t (p₃ x))                   ≅⟨ sym $ D->>= (p₁ >>= p₂) p₃ 

    D t (p₁ >>= p₂ >>= p₃)                                       )