module TotalParserCombinators.Laws where
open import Algebra
open import Category.Monad
open import Coinduction
open import Data.List as List
import Data.List.Any as Any
import Data.List.Any.BagAndSetEquality as Eq
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open Any.Membership-≡ using (bag) renaming (_≈[_]_ to _List-≈[_]_)
private
module BagMonoid {A : Set} =
CommutativeMonoid (Eq.commutativeMonoid _ A)
open module ListMonad = RawMonad List.monad
using () renaming (_⊛_ to _⊛′_)
open import TotalParserCombinators.BreadthFirst.Derivative
open import TotalParserCombinators.Congruence
hiding (return; fail; token)
open import TotalParserCombinators.Lib hiding (module Return⋆)
open import TotalParserCombinators.Parser
import TotalParserCombinators.Laws.AdditiveMonoid
module AdditiveMonoid = TotalParserCombinators.Laws.AdditiveMonoid
import TotalParserCombinators.Laws.Derivative
module D = TotalParserCombinators.Laws.Derivative
hiding (left-zero-⊛; right-zero-⊛;
left-zero->>=; right-zero->>=)
import TotalParserCombinators.Laws.ReturnStar
module Return⋆ = TotalParserCombinators.Laws.ReturnStar
import TotalParserCombinators.Laws.ApplicativeFunctor
module ApplicativeFunctor =
TotalParserCombinators.Laws.ApplicativeFunctor
import TotalParserCombinators.Laws.Monad
module Monad = TotalParserCombinators.Laws.Monad
import TotalParserCombinators.Laws.KleeneAlgebra
module KleeneAlgebra = TotalParserCombinators.Laws.KleeneAlgebra
module <$> where
open D
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
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 ∎
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) ∎
module Nonempty where
zero : ∀ {Tok R} → nonempty {Tok = Tok} {R = R} fail ≅P fail
zero = BagMonoid.refl ∷ λ t → ♯ (fail ∎)
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)
module Cast where
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 ∎)