------------------------------------------------------------------------ -- This module proves that the context-sensitive language aⁿbⁿcⁿ can -- be recognised ------------------------------------------------------------------------ -- This is obvious given the proof in -- TotalRecognisers.LeftRecursion.ExpressiveStrength but the code -- below provides a non-trivial example of the use of the parser -- combinators. module TotalRecognisers.LeftRecursion.NotOnlyContextFree where open import Algebra open import Coinduction open import Data.Bool using (Bool; true; false; _∨_) open import Function open import Data.List as List using (List; []; _∷_; _++_; [_]) private module ListMonoid {A : Set} = Monoid (List.monoid A) open import Data.Nat as Nat using (ℕ; zero; suc; _+_) import Data.Nat.Properties as NatProp open NatProp.SemiringSolver private module NatCS = CommutativeSemiring NatProp.commutativeSemiring open import Data.Product open import Relation.Binary open import Relation.Binary.PropositionalEquality open import Relation.Nullary open ≡-Reasoning import TotalRecognisers.LeftRecursion import TotalRecognisers.LeftRecursion.Lib as Lib ------------------------------------------------------------------------ -- The alphabet data Tok : Set where a b c : Tok _≟_ : Decidable (_≡_ {A = Tok}) a ≟ a = yes refl a ≟ b = no λ() a ≟ c = no λ() b ≟ a = no λ() b ≟ b = yes refl b ≟ c = no λ() c ≟ a = no λ() c ≟ b = no λ() c ≟ c = yes refl open TotalRecognisers.LeftRecursion Tok open Lib Tok private open module TokTok = Lib.Tok Tok _≟_ using (tok) ------------------------------------------------------------------------ -- An auxiliary definition and a boring lemma infixr 8 _^^_ _^^_ : Tok → ℕ → List Tok _^^_ = flip List.replicate private shallow-comm : ∀ i n → i + suc n ≡ suc (i + n) shallow-comm i n = solve 2 (λ i n → i :+ (con 1 :+ n) := con 1 :+ i :+ n) refl i n ------------------------------------------------------------------------ -- Some lemmas relating _^^_, _^_ and tok tok-^-complete : ∀ t i → t ^^ i ∈ tok t ^ i tok-^-complete t zero = empty tok-^-complete t (suc i) = add-♭♯ ⟨ false ^ i ⟩-nullable TokTok.complete · tok-^-complete t i tok-^-sound : ∀ t i {s} → s ∈ tok t ^ i → s ≡ t ^^ i tok-^-sound t zero empty = refl tok-^-sound t (suc i) (t∈ · s∈) with TokTok.sound (drop-♭♯ ⟨ false ^ i ⟩-nullable t∈) ... | refl = cong (_∷_ t) (tok-^-sound t i s∈) ------------------------------------------------------------------------ -- aⁿbⁿcⁿ -- The context-sensitive language { aⁿbⁿcⁿ | n ∈ ℕ } can be recognised -- using the parser combinators defined in this development. private -- The two functions below are not actually mutually recursive, but -- are placed in a mutual block to ensure that the constraints -- generated by the second function can be used to instantiate the -- underscore in the body of the first. mutual aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index : ℕ → Bool aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index _ = _ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ : (i : ℕ) → P (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index i) aⁿbⁱ⁺ⁿcⁱ⁺ⁿ i = cast lem (♯? (tok a) · ♯ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ (suc i)) ∣ tok b ^ i ⊙ tok c ^ i where lem = left-zero (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index (suc i)) aⁿbⁿcⁿ : P true aⁿbⁿcⁿ = aⁿbⁱ⁺ⁿcⁱ⁺ⁿ 0 -- Let us prove that aⁿbⁿcⁿ is correctly defined. aⁿbⁿcⁿ-string : ℕ → List Tok aⁿbⁿcⁿ-string n = a ^^ n ++ b ^^ n ++ c ^^ n private aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-string : ℕ → ℕ → List Tok aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-string n i = a ^^ n ++ b ^^ (i + n) ++ c ^^ (i + n) aⁿbⁿcⁿ-complete : ∀ n → aⁿbⁿcⁿ-string n ∈ aⁿbⁿcⁿ aⁿbⁿcⁿ-complete n = aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete n 0 where aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete : ∀ n i → aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-string n i ∈ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ i aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete zero i with i + 0 | proj₂ NatCS.+-identity i ... | .i | refl = ∣-right {n₁ = false} (helper b · helper c) where helper = λ (t : Tok) → add-♭♯ ⟨ false ^ i ⟩-nullable (tok-^-complete t i) aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete (suc n) i with i + suc n | shallow-comm i n ... | .(suc i + n) | refl = ∣-left \$ cast {eq = lem} ( add-♭♯ (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index (suc i)) TokTok.complete · aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-complete n (suc i)) where lem = left-zero (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index (suc i)) aⁿbⁿcⁿ-sound : ∀ {s} → s ∈ aⁿbⁿcⁿ → ∃ λ n → s ≡ aⁿbⁿcⁿ-string n aⁿbⁿcⁿ-sound = aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound 0 where aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound : ∀ {s} i → s ∈ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ i → ∃ λ n → s ≡ aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-string n i aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound i (∣-left (cast (t∈ · s∈))) with TokTok.sound (drop-♭♯ (aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-index (suc i)) t∈) ... | refl with aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound (suc i) s∈ ... | (n , refl) = suc n , (begin a ^^ suc n ++ b ^^ (suc i + n) ++ c ^^ (suc i + n) ≡⟨ cong (λ i → a ^^ suc n ++ b ^^ i ++ c ^^ i) (sym (shallow-comm i n)) ⟩ a ^^ suc n ++ b ^^ (i + suc n) ++ c ^^ (i + suc n) ∎) aⁿbⁱ⁺ⁿcⁱ⁺ⁿ-sound i (∣-right (_·_ {s₁} {s₂} s₁∈ s₂∈)) = 0 , (begin s₁ ++ s₂ ≡⟨ cong₂ _++_ (tok-^-sound b i (drop-♭♯ ⟨ false ^ i ⟩-nullable s₁∈)) (tok-^-sound c i (drop-♭♯ ⟨ false ^ i ⟩-nullable s₂∈)) ⟩ b ^^ i ++ c ^^ i ≡⟨ cong (λ i → b ^^ i ++ c ^^ i) (sym (proj₂ NatCS.+-identity i)) ⟩ b ^^ (i + 0) ++ c ^^ (i + 0) ∎)