------------------------------------------------------------------------ -- Example: Left recursive expression grammar ------------------------------------------------------------------------ module TotalParserCombinators.Examples.Expression where open import Coinduction open import Data.Char as Char using (Char) open import Data.List open import Data.Nat open import Data.String as String using (String) open import Function open import Relation.Binary.PropositionalEquality as P using (_≡_) open import TotalParserCombinators.BreadthFirst open import TotalParserCombinators.Lib open import TotalParserCombinators.Parser open Token Char Char._≟_ ------------------------------------------------------------------------ -- An expression grammar -- t ∷= t '+' f ∣ f -- f ∷= f '*' a ∣ a -- a ∷= '(' t ')' ∣ n -- Applicative implementation of the grammar. module Applicative where mutual term = ♯ (return (λ e₁ _ e₂ → e₁ + e₂) ⊛ term) ⊛ tok '+' ⊛ factor ∣ factor factor = ♯ (return (λ e₁ _ e₂ → e₁ * e₂) ⊛ factor) ⊛ tok '*' ⊛ atom ∣ atom atom = return (λ _ e _ → e) ⊛ tok '(' ⊛ ♯ term ⊛ tok ')' ∣ number -- Monadic implementation of the grammar. module Monadic where mutual term = factor ∣ ♯ term >>= λ e₁ → tok '+' >>= λ _ → factor >>= λ e₂ → return (e₁ + e₂) factor = atom ∣ ♯ factor >>= λ e₁ → tok '*' >>= λ _ → atom >>= λ e₂ → return (e₁ * e₂) atom = number ∣ tok '(' >>= λ _ → ♯ term >>= λ e → tok ')' >>= λ _ → return e ------------------------------------------------------------------------ -- Unit tests module Tests where test : ∀ {R xs} → Parser Char R xs → String → List R test p = parse p ∘ String.toList -- Some examples have been commented out in order to reduce -- type-checking times. -- ex₁ : test Applicative.term "1*(2+3)" ≡ [ 5 ] -- ex₁ = P.refl -- ex₂ : test Applicative.term "1*(2+3" ≡ [] -- ex₂ = P.refl ex₃ : test Monadic.term "1+2+3" ≡ [ 6 ] ex₃ = P.refl ex₄ : test Monadic.term "+32" ≡ [] ex₄ = P.refl