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

module TotalRecognisers.LeftRecursion.Expression where

open import Codata.Musical.Notation
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.toℕ '0' ≤? Char.toℕ  t   
                Char.toℕ  t  ≤? Char.toℕ '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