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._≟_
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' ⌋
number : P _
number = digit +
mutual
term = ♯ (♯ term · ♯ tok '+') · ♯ factor
∣ factor
factor = ♯ (♯ factor · ♯ tok '*') · ♯ atom
∣ 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 "1*(2+3)" ≡ true
ex₁ = refl
ex₂ : test term "1*(2+3" ≡ false
ex₂ = refl