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