```------------------------------------------------------------------------
-- 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.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.

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
```