------------------------------------------------------------------------
-- 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 Codata.Musical.Notation
open import Data.Bool using (Bool; true; false; _∨_)
open import Function
open import Data.List as List using (List; []; _∷_; _++_; [_])
import Data.List.Properties
private
  module ListMonoid {A : Set} =
    Monoid (Data.List.Properties.++-monoid A)
open import Data.Nat as Nat using (; zero; suc; _+_)
import Data.Nat.Properties as NatProp
private
  module NatCS = CommutativeSemiring NatProp.+-*-commutativeSemiring
import Data.Nat.Solver
open Data.Nat.Solver.+-*-Solver
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)
      )