module TotalRecognisers.Simple.Expression where
open import Codata.Musical.Notation
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 (_·_)
bit = tok '0' ∣ tok '1'
number = bit · ♯ (empty ∣ number)
mutual
term = factor · ♯ (tok '+' · ♯ term)
∣ factor
factor = atom · ♯ (tok '*' · ♯ factor)
∣ atom
atom = tok '(' · ♯ term · ♯ tok ')'
∣ number
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