------------------------------------------------------------------------
-- Example: Right recursive expression grammar
------------------------------------------------------------------------

module TotalRecognisers.Simple.Expression where

open import Coinduction
open import Data.Bool
open import Data.Char as Char using (Char)
open import Data.String as String using (String)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable

import TotalRecognisers.Simple as P

private
  open module PC = P Char Char._≟_ hiding (_·_)
  open PC.P using (_·_)

------------------------------------------------------------------------
-- Recognisers for bits and binary numbers

-- Bits.

bit = tok '0' ∣ tok '1'

-- Numbers.

number = bit · ♯ (empty ∣ number)

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

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

mutual

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

  factor = atom · ♯ (tok '*' · ♯ factor)
         ∣ 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 "0*(0+0)" ≡ true
  ex₁ = refl

  ex₂ : test term "0*(0+0" ≡ false
  ex₂ = refl