module TotalParserCombinators.Recogniser.Expression where
open import Coinduction
open import Data.Bool
open import Data.Char as Char using (Char)
open import Data.List
open import Data.String as String using (String)
open import Function
open import Relation.Binary.PropositionalEquality
open import TotalParserCombinators.BreadthFirst
import TotalParserCombinators.Lib as Lib
open import TotalParserCombinators.Recogniser
tok : Char → P Char []
tok c = lift $ Lib.Token.tok Char Char._≟_ c
number : P Char []
number = lift Lib.number
mutual
term = ♯ term · tok '+' · factor
∣ factor
factor = ♯ factor · tok '*' · atom
∣ atom
atom = tok '(' · ♯ term · tok ')'
∣ number
module Tests where
test : ∀ {n} → P Char n → String → Bool
test p s = not $ null $ parse ⟦ p ⟧ (String.toList s)
ex₁ : test term "1*(2+3)" ≡ true
ex₁ = refl
ex₂ : test term "1*(2+3" ≡ false
ex₂ = refl