module TotalParserCombinators.Laws.Derivative where
open import Algebra
open import Codata.Musical.Notation
open import Data.List
import Data.List.Effectful as List
import Data.List.Relation.Binary.BagAndSetEquality as BSEq
open import Data.Maybe using (Maybe); open Data.Maybe.Maybe
open import Function using (_∘_; _$_)
private
module BagMonoid {k} {A : Set} =
CommutativeMonoid (BSEq.commutativeMonoid k A)
open import TotalParserCombinators.Derivative
open import TotalParserCombinators.Congruence as Eq
hiding (return; fail)
import TotalParserCombinators.Laws.AdditiveMonoid as AdditiveMonoid
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser
D-return⋆ : ∀ {Tok R t} (xs : List R) →
D t (return⋆ xs) ≅P fail {Tok = Tok}
D-return⋆ [] = fail ∎
D-return⋆ {t = t} (x ∷ xs) =
fail ∣ D t (return⋆ xs) ≅⟨ AdditiveMonoid.left-identity (D t (return⋆ xs)) ⟩
D t (return⋆ xs) ≅⟨ D-return⋆ xs ⟩
fail ∎
mutual
D-⊛ : ∀ {Tok R₁ R₂ fs xs t}
(p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs))
(p₂ : ∞⟨ fs ⟩Parser Tok R₁ (flatten xs)) →
D t (p₁ ⊛ p₂) ≅P
D t (♭? p₁) ⊛ ♭? p₂ ∣ return⋆ (flatten fs) ⊛ D t (♭? p₂)
D-⊛ {fs = nothing} {xs = just _} {t = t} p₁ p₂ =
D t p₁ ⊛ ♭ p₂ ≅⟨ sym $ AdditiveMonoid.right-identity (D t p₁ ⊛ ♭ p₂) ⟩
D t p₁ ⊛ ♭ p₂ ∣ fail ≅⟨ (D t p₁ ⊛ ♭ p₂ ∎) ∣ sym (left-zero-⊛ (D t (♭ p₂))) ⟩
D t p₁ ⊛ ♭ p₂ ∣ fail ⊛ D t (♭ p₂) ∎
D-⊛ {fs = nothing} {xs = nothing} {t = t} p₁ p₂ =
D t (p₁ ⊛ p₂) ≅⟨ [ ◌ - ○ - ○ - ○ ] D t (♭ p₁) ∎ ⊛ (♭ p₂ ∎) ⟩
D t (♭ p₁) ⊛ ♭ p₂ ≅⟨ sym $ AdditiveMonoid.right-identity (D t (♭ p₁) ⊛ ♭ p₂) ⟩
D t (♭ p₁) ⊛ ♭ p₂ ∣ fail ≅⟨ (D t (♭ p₁) ⊛ ♭ p₂ ∎) ∣ sym (left-zero-⊛ (D t (♭ p₂))) ⟩
D t (♭ p₁) ⊛ ♭ p₂ ∣ fail ⊛ D t (♭ p₂) ∎
D-⊛ {fs = just _} {xs = just _} {t = t} p₁ p₂ =
D t (p₁ ⊛ p₂) ∎
D-⊛ {fs = just fs} {xs = nothing} {t = t} p₁ p₂ =
D t (p₁ ⊛ p₂) ≅⟨ [ ◌ - ○ - ○ - ○ ] D t (♭ p₁) ∎ ⊛ (p₂ ∎) ∣
(return⋆ fs ⊛ D t p₂ ∎) ⟩
D t (♭ p₁) ⊛ p₂ ∣ return⋆ fs ⊛ D t p₂ ∎
left-zero-⊛ : ∀ {Tok R₁ R₂ xs} (p : Parser Tok R₁ xs) →
fail ⊛ p ≅P fail {R = R₂}
left-zero-⊛ {xs = xs} p =
BagMonoid.reflexive (List.Applicative.left-zero xs) ∷ λ t → ♯ (
D t (fail ⊛ p) ≅⟨ D-⊛ fail p ⟩
fail ⊛ p ∣ fail ⊛ D t p ≅⟨ left-zero-⊛ p ∣ left-zero-⊛ (D t p) ⟩
fail ∣ fail ≅⟨ AdditiveMonoid.right-identity fail ⟩
fail ∎)
right-zero-⊛ : ∀ {Tok R₁ R₂ fs} (p : Parser Tok (R₁ → R₂) fs) →
p ⊛ fail ≅P fail
right-zero-⊛ {fs = fs} p =
BagMonoid.reflexive (List.Applicative.right-zero fs) ∷ λ t → ♯ (
D t (p ⊛ fail) ≅⟨ D-⊛ p fail ⟩
D t p ⊛ fail ∣ return⋆ fs ⊛ fail ≅⟨ right-zero-⊛ (D t p) ∣ right-zero-⊛ (return⋆ fs) ⟩
fail ∣ fail ≅⟨ AdditiveMonoid.left-identity fail ⟩
fail ∎)
D-return-⊛ : ∀ {Tok R₁ R₂ xs t}
(f : R₁ → R₂) (p : Parser Tok R₁ xs) →
D t (return f ⊛ p) ≅P return f ⊛ D t p
D-return-⊛ {t = t} f p =
D t (return f ⊛ p) ≅⟨ D-⊛ (return f) p ⟩
fail ⊛ p ∣ return⋆ [ f ] ⊛ D t p ≅⟨ left-zero-⊛ p ∣
[ ○ - ○ - ○ - ○ ] AdditiveMonoid.right-identity (return f) ⊛ (D t p ∎) ⟩
fail ∣ return f ⊛ D t p ≅⟨ AdditiveMonoid.left-identity (return f ⊛ D t p) ⟩
return f ⊛ D t p ∎
mutual
D->>= : ∀ {Tok R₁ R₂ xs t} {f : Maybe (R₁ → List R₂)}
(p₁ : ∞⟨ f ⟩Parser Tok R₁ (flatten xs))
(p₂ : (x : R₁) → ∞⟨ xs ⟩Parser Tok R₂ (apply f x)) →
D t (p₁ >>= p₂) ≅P
D t (♭? p₁) >>= (♭? ∘ p₂) ∣
return⋆ (flatten xs) >>= (λ x → D t (♭? (p₂ x)))
D->>= {xs = nothing} {t = t} {f = just _} p₁ p₂ =
D t p₁ >>= (♭ ∘ p₂) ≅⟨ sym $ AdditiveMonoid.right-identity (D t p₁ >>= (♭ ∘ p₂)) ⟩
D t p₁ >>= (♭ ∘ p₂) ∣ fail ≅⟨ (D t p₁ >>= (♭ ∘ p₂) ∎) ∣
sym (left-zero->>= (λ x → D t (♭ (p₂ x)))) ⟩
D t p₁ >>= (♭ ∘ p₂) ∣ fail >>= (λ x → D t (♭ (p₂ x))) ∎
D->>= {xs = just xs} {t = t} {f = just _} p₁ p₂ =
D t p₁ >>= p₂ ∣ return⋆ xs >>= (λ x → D t (p₂ x)) ∎
D->>= {xs = nothing} {t = t} {f = nothing} p₁ p₂ =
D t (p₁ >>= p₂) ≅⟨ [ ◌ - ○ - ○ - ○ ] _ ∎ >>= (λ _ → _ ∎) ⟩
D t (♭ p₁) >>= (♭ ∘ p₂) ≅⟨ sym $ AdditiveMonoid.right-identity (D t (♭ p₁) >>= (♭ ∘ p₂)) ⟩
D t (♭ p₁) >>= (♭ ∘ p₂) ∣ fail ≅⟨ (D t (♭ p₁) >>= (♭ ∘ p₂) ∎) ∣
sym (left-zero->>= (λ x → D t (♭ (p₂ x)))) ⟩
D t (♭ p₁) >>= (♭ ∘ p₂) ∣ fail >>= (λ x → D t (♭ (p₂ x))) ∎
D->>= {xs = just xs} {t = t} {f = nothing} p₁ p₂ =
D t (p₁ >>= p₂) ≅⟨ [ ◌ - ○ - ○ - ○ ] _ ∎ >>= (λ _ → _ ∎) ∣ (_ ∎) ⟩
D t (♭ p₁) >>= p₂ ∣ return⋆ xs >>= (λ x → D t (p₂ x)) ∎
left-zero->>= : ∀ {Tok R₁ R₂} {f : R₁ → List R₂}
(p : (x : R₁) → Parser Tok R₂ (f x)) →
fail >>= p ≅P fail
left-zero->>= {f = f} p =
BagMonoid.reflexive (List.MonadProperties.left-zero f) ∷ λ t → ♯ (
D t (fail >>= p) ≅⟨ D->>= {t = t} fail p ⟩
fail >>= p ∣ fail >>= (λ x → D t (p x)) ≅⟨ left-zero->>= p ∣ left-zero->>= (λ x → D t (p x)) ⟩
fail ∣ fail ≅⟨ AdditiveMonoid.right-identity fail ⟩
fail ∎)
right-zero->>= : ∀ {Tok R₁ R₂} {xs : List R₁}
(p : Parser Tok R₁ xs) →
p >>= (λ _ → fail) ≅P fail {Tok = Tok} {R = R₂}
right-zero->>= {xs = xs} p =
BagMonoid.reflexive (List.MonadProperties.right-zero xs) ∷ λ t → ♯ (
D t (p >>= λ _ → fail) ≅⟨ D->>= p (λ _ → fail) ⟩
D t p >>= (λ _ → fail) ∣ return⋆ xs >>= (λ _ → fail) ≅⟨ right-zero->>= (D t p) ∣ right-zero->>= (return⋆ xs) ⟩
fail ∣ fail ≅⟨ AdditiveMonoid.left-identity fail ⟩
fail ∎)