module TotalParserCombinators.Laws.KleeneAlgebra where
open import Algebra
open import Data.List
open import Data.List.Properties
open import Data.Nat using (ℕ)
open import Data.Product using (_,_; proj₂)
open import Function using (_$_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
using (_⇔_; equivalence; module Equivalence)
import Relation.Binary.PropositionalEquality as P
open import Relation.Nullary
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics
hiding (_>>=_) renaming (return to return′; _⊛_ to _⊛′_)
infix 4 _≲′_
_≲′_ : ∀ {Tok R xs₁ xs₂} → Parser Tok R xs₁ → Parser Tok R xs₂ → Set₁
p₁ ≲′ p₂ = p₁ ∣ p₂ ≈ p₂
≲⇔≲′ : ∀ {Tok R xs₁ xs₂}
(p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂) →
p₁ ≲ p₂ ⇔ p₁ ≲′ p₂
≲⇔≲′ {xs₁ = xs₁} p₁ p₂ = equivalence
(λ (p₁≲p₂ : p₁ ≲ p₂) {x s} → equivalence (helper p₁≲p₂) (∣-right xs₁))
(λ (p₁≲′p₂ : p₁ ≲′ p₂) s∈p₁ → Equivalence.to p₁≲′p₂ ⟨$⟩ ∣-left s∈p₁)
where
helper : p₁ ≲ p₂ → p₁ ∣ p₂ ≲ p₂
helper p₁≲p₂ (∣-left s∈p₁) = p₁≲p₂ s∈p₁
helper p₁≲p₂ (∣-right .xs₁ s∈p₂) = s∈p₂
record _LeastUpperBoundOf_
{Tok R xs} {f : ℕ → List R}
(lub : Parser Tok R xs)
(p : (n : ℕ) → Parser Tok R (f n)) : Set₁ where
field
upper-bound : ∀ n → p n ≲ lub
least : ∀ {ys} {ub : Parser Tok R ys} →
(∀ n → p n ≲ ub) → lub ≲ ub
*-continuous :
∀ {Tok R₁ R₂ R₃ fs xs}
(p₁ : Parser Tok (List R₁ → R₂ → R₃) fs)
(p₂ : Parser Tok R₁ [])
(p₃ : Parser Tok R₂ xs) →
(p₁ ⊛ p₂ ⋆ ⊛ p₃) LeastUpperBoundOf (λ n → p₁ ⊛ p₂ ↑ n ⊛ p₃)
*-continuous {Tok} {R₁ = R₁} {R₃ = R₃} {fs} {xs} p₁ p₂ p₃ =
record { upper-bound = upper-bound; least = least }
where
upper-bound : ∀ n → p₁ ⊛ p₂ ↑ n ⊛ p₃ ≲ p₁ ⊛ p₂ ⋆ ⊛ p₃
upper-bound n (∈p₁ ⊛′ ∈p₂ⁿ ⊛′ ∈p₃) =
[ ○ - ○ ] [ ○ - ○ ] ∈p₁ ⊛ Exactly.↑≲⋆ n ∈p₂ⁿ ⊛ ∈p₃
least : ∀ {ys} {p : Parser Tok R₃ ys} →
(∀ i → p₁ ⊛ p₂ ↑ i ⊛ p₃ ≲ p) → p₁ ⊛ p₂ ⋆ ⊛ p₃ ≲ p
least ub (∈p₁ ⊛′ ∈p₂⋆ ⊛′ ∈p₃) with Exactly.⋆≲∃↑ ∈p₂⋆
... | (n , ∈p₂ⁿ) = ub n ([ ○ - ○ ] [ ○ - ○ ] ∈p₁ ⊛ ∈p₂ⁿ ⊛ ∈p₃)
not-Kleene-algebra :
∀ {Tok} →
Tok →
(f : ∀ {R xs} → Parser Tok R xs → List (List R)) →
(_⋆′ : ∀ {R xs} (p : Parser Tok R xs) →
Parser Tok (List R) (f p)) →
¬ (∀ {R xs} {p : Parser Tok R xs} →
return [] ∣ (p >>= λ x → (p ⋆′) >>= λ xs → return (x ∷ xs))
≲ (p ⋆′))
not-Kleene-algebra {Tok} t f _⋆′ fold =
KleeneStar.unrestricted-incomplete t f _⋆′ ⋆′-complete
where
⋆′-complete : ∀ {xs ys s} {p : Parser Tok Tok ys} →
xs ∈[ p ]⋆· s → xs ∈ p ⋆′ · s
⋆′-complete [] = fold (∣-left return′)
⋆′-complete (∈p ∷ ∈p⋆) =
fold (∣-right [ [] ]
([ ○ - ○ ] ∈p >>=
fix ([ ○ - ○ ] ⋆′-complete ∈p⋆ >>= return′)))
where
fix = cast∈ P.refl P.refl $ ++-identityʳ _