module TotalParserCombinators.Laws where
open import Algebra hiding (module KleeneAlgebra)
open import Codata.Musical.Notation
open import Data.List as List
import Data.List.Effectful
open import Data.List.Properties
open import Data.List.Relation.Binary.BagAndSetEquality as Eq
using (bag) renaming (_∼[_]_ to _List-∼[_]_)
open import Data.Maybe hiding (_>>=_)
open import Effect.Monad
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} Data.List.Effectful.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
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 as AF
hiding (module <$>)
module ApplicativeFunctor = AF
import TotalParserCombinators.Laws.ApplicativeFunctor
module <$> =
TotalParserCombinators.Laws.ApplicativeFunctor.<$>
import TotalParserCombinators.Laws.Monad
module Monad = TotalParserCombinators.Laws.Monad
import TotalParserCombinators.Laws.KleeneAlgebra
module KleeneAlgebra = TotalParserCombinators.Laws.KleeneAlgebra
module Nonempty where
zero : ∀ {Tok R} → nonempty {Tok = Tok} {R = R} fail ≅P fail
zero = BagMonoid.refl ∷ λ t → ♯ (fail ∎)
nonempty-return :
∀ {Tok R} {x : R} → nonempty {Tok = Tok} (return x) ≅P fail
nonempty-return = 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 ∎)
module Subst where
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 ∎