module TotalParserCombinators.Derivative.Corollaries where
open import Data.List
open import Data.Product
open import Function
import Function.Related.Propositional as Related
import Relation.Binary.PropositionalEquality as P
open Related using (SK-sym)
open import TotalParserCombinators.Derivative.Definition
open import TotalParserCombinators.Derivative.LeftInverse
open import TotalParserCombinators.Derivative.RightInverse
open import TotalParserCombinators.Derivative.SoundComplete
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics
correct : ∀ {Tok R xs x s} {t} {p : Parser Tok R xs} →
x ∈ D t p · s ↔ x ∈ p · t ∷ s
correct {p = p} =
mk↔ {to = sound p}
( (λ { P.refl → sound∘complete _ })
, (λ { P.refl → complete∘sound p _ })
)
mono : ∀ {Tok R xs₁ xs₂ t}
{p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
p₁ ≲ p₂ → D t p₁ ≲ D t p₂
mono p₁≲p₂ =
Equivalence.from ≲⇔≲→
(complete ∘ Equivalence.to ≲⇔≲→ p₁≲p₂ ∘ sound _)
cong : ∀ {k Tok R xs₁ xs₂}
{p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
p₁ ∼[ k ] p₂ → ∀ {t} → D t p₁ ∼[ k ] D t p₂
cong {p₁ = p₁} {p₂} p₁≈p₂ {t} {x} {s} =
x ∈ D t p₁ · s ↔⟨ correct ⟩
x ∈ p₁ · t ∷ s ∼⟨ p₁≈p₂ ⟩
x ∈ p₂ · t ∷ s ↔⟨ SK-sym correct ⟩
x ∈ D t p₂ · s ∎
where open Related.EquationalReasoning