------------------------------------------------------------------------
-- Various parser combinator laws
------------------------------------------------------------------------

-- Note that terms like "monad" and "Kleene algebra" are interpreted
-- liberally in the modules listed below.

module TotalParserCombinators.Laws where

open import Algebra
open import Category.Monad
open import Coinduction
open import Data.List as List
open import Data.List.Any.Membership.Propositional
  using (bag) renaming (_∼[_]_ to _List-∼[_]_)
import Data.List.Any.BagAndSetEquality as Eq
open import Data.Maybe
open import Function
import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_)

private
  module BagMonoid {k} {A : Set} =
    CommutativeMonoid (Eq.commutativeMonoid k A)
  open module ListMonad = RawMonad {f = Level.zero} List.monad
    using () renaming (_⊛_ to _⊛′_)

open import TotalParserCombinators.Derivative using (D)
open import TotalParserCombinators.Congruence
  hiding (return; fail; token)
open import TotalParserCombinators.Lib hiding (module Return⋆)
open import TotalParserCombinators.Parser

------------------------------------------------------------------------
-- Reexported modules

-- Laws related to _∣_.

import TotalParserCombinators.Laws.AdditiveMonoid
module AdditiveMonoid = TotalParserCombinators.Laws.AdditiveMonoid

-- Laws related to D.

import TotalParserCombinators.Laws.Derivative
module D = TotalParserCombinators.Laws.Derivative
  hiding (left-zero-⊛; right-zero-⊛;
          left-zero->>=; right-zero->>=)

-- Laws related to return⋆.

import TotalParserCombinators.Laws.ReturnStar
module Return⋆ = TotalParserCombinators.Laws.ReturnStar

-- Laws related to _⊛_.

import TotalParserCombinators.Laws.ApplicativeFunctor
module ApplicativeFunctor =
  TotalParserCombinators.Laws.ApplicativeFunctor

-- Laws related to _>>=_.

import TotalParserCombinators.Laws.Monad
module Monad = TotalParserCombinators.Laws.Monad

-- Do the parser combinators form a Kleene algebra?

import TotalParserCombinators.Laws.KleeneAlgebra
module KleeneAlgebra = TotalParserCombinators.Laws.KleeneAlgebra

------------------------------------------------------------------------
-- Some laws for _<$>_

module <$> where

  open D

  -- _<$>_ could have been defined using return and _⊛_.

  return-⊛ :  {Tok R₁ R₂ xs} {f : R₁  R₂} (p : Parser Tok R₁ xs) 
             f <$> p ≅P return f  p
  return-⊛ {xs = xs} {f} p =
    BagMonoid.reflexive (lemma xs)  λ t   (
      f <$> D t p         ≅⟨ return-⊛ (D t p) 
      return f  D t p    ≅⟨ sym $ D-return-⊛ f p 
      D t (return f  p)  )
    where
    lemma :  xs  List.map f xs  ([ f ] ⊛′ xs)
    lemma []       = P.refl
    lemma (x  xs) = P.cong (_∷_ (f x)) $ lemma xs

  -- fail is a zero for _<$>_.

  zero :  {Tok R₁ R₂} {f : R₁  R₂} 
         f <$> fail {Tok = Tok} ≅P fail
  zero {f = f} =
    f <$> fail       ≅⟨ return-⊛ fail 
    return f  fail  ≅⟨ ApplicativeFunctor.right-zero (return f) 
    fail             

  -- A variant of ApplicativeFunctor.homomorphism.

  homomorphism :  {Tok R₁ R₂} (f : R₁  R₂) {x} 
                 f <$> return {Tok = Tok} x ≅P return (f x)
  homomorphism f {x} =
    f <$> return x       ≅⟨ return-⊛ {f = f} (return x) 
    return f  return x  ≅⟨ ApplicativeFunctor.homomorphism f x 
    return (f x)         

------------------------------------------------------------------------
-- A law for nonempty

module Nonempty where

  -- fail is a zero for nonempty.

  zero :  {Tok R}  nonempty {Tok = Tok} {R = R} fail ≅P fail
  zero = BagMonoid.refl  λ t   (fail )

  -- nonempty (return x) is parser equivalent to fail.

  nonempty-return :
     {Tok R} {x : R}  nonempty {Tok = Tok} (return x) ≅P fail
  nonempty-return = BagMonoid.refl  λ t   (fail )

  -- nonempty can be defined in terms of token, _>>=_ and D.

  private

    nonempty′ :  {Tok R xs} (p : Parser Tok R xs)  Parser Tok R []
    nonempty′ p = token >>= λ t  D t p

  nonempty-definable :  {Tok R xs} (p : Parser Tok R xs) 
                       nonempty p ≅P nonempty′ p
  nonempty-definable p = BagMonoid.refl  λ t   (
    D t p              ≅⟨ sym $ Monad.left-identity t  t′  D t′ p) 
    ret-D t            ≅⟨ sym $ AdditiveMonoid.right-identity (ret-D t) 
    ret-D t  fail     ≅⟨ (ret-D t )  sym (Monad.left-zero _) 
    D t (nonempty′ p)  )
    where ret-D = λ (t : _)  return t >>=  t′  D t′ p)

------------------------------------------------------------------------
-- A law for cast

module Cast where

  -- Casts can be erased.

  correct :  {Tok R xs₁ xs₂}
              {xs₁≈xs₂ : xs₁ List-∼[ bag ] xs₂}
              {p : Parser Tok R xs₁} 
            cast xs₁≈xs₂ p ≅P p
  correct {xs₁≈xs₂ = xs₁≈xs₂} {p} =
    BagMonoid.sym xs₁≈xs₂  λ t   (D t p )

------------------------------------------------------------------------
-- A law for subst

module Subst where

  -- Uses of subst can be erased.

  correct :  {Tok R xs₁ xs₂}
              (xs₁≡xs₂ : xs₁  xs₂)
              {p : Parser Tok R xs₁} 
            P.subst (Parser Tok R) xs₁≡xs₂ p ≅P p
  correct P.refl {p} = p 

  correct∞ :  {Tok R xs₁ xs₂ A} {m : Maybe A}
              (xs₁≡xs₂ : xs₁  xs₂)
              (p : ∞⟨ m ⟩Parser Tok R xs₁) 
             ♭? (P.subst (∞⟨ m ⟩Parser Tok R) xs₁≡xs₂ p) ≅P ♭? p
  correct∞ P.refl p = ♭? p