------------------------------------------------------------------------
-- Example: Left recursive expression grammar
------------------------------------------------------------------------

module TotalRecognisers.LeftRecursion.Expression where

open import Coinduction
open import Data.Bool hiding (_∧_)
open import Data.Char as Char using (Char)
open import Data.Nat using (ℕ; _≤?_)
open import Data.String as String using (String)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable

import TotalRecognisers.LeftRecursion as P
import TotalRecognisers.LeftRecursion.Lib as Lib

open P Char
open Lib Char
open KleeneStar₁
open Tok Char._≟_

------------------------------------------------------------------------
-- Recognisers for digits and numbers

-- Digits.

digit : P _
digit = sat in-range
  where
  in-range : Char → Bool
  in-range t = ⌊ Char.toNat '0' ≤? Char.toNat  t  ⌋ ∧
               ⌊ Char.toNat  t  ≤? Char.toNat '9' ⌋

-- Numbers.

number : P _
number = digit +

------------------------------------------------------------------------
-- An expression grammar

-- t ∷= t '+' f ∣ f
-- f ∷= f '*' a ∣ a
-- a ∷= '(' t ')' ∣ n

mutual

  term   = ♯ (♯ term · ♯ tok '+') · ♯ factor
         ∣ factor

  factor = ♯ (♯ factor · ♯ tok '*') · ♯ atom
         ∣ atom

  atom   = ♯ (♯ tok '(' · ♯ term) · ♯ tok ')'
         ∣ number

------------------------------------------------------------------------
-- Unit tests

module Tests where

  test : ∀ {n} → P n → String → Bool
  test p s = ⌊ String.toList s ∈? p ⌋

  ex₁ : test term "1*(2+3)" ≡ true
  ex₁ = refl

  ex₂ : test term "1*(2+3" ≡ false
  ex₂ = refl