playing with idris' parser

parsing.idr

import Text.Lexer.Core
import Text.Lexer
import Text.Parser.Core
import Text.Parser


data ExpressionToken = Number Integer
                     | Operator String
                     | OParen
                     | CParen
                     | EndInput

Show ExpressionToken where
    show (Number x) = "number " ++ show x
    show (Operator x) = "operator " ++ x
    show OParen = "("
    show CParen = ")"
    show EndInput = "end of input"

Show (WithBounds ExpressionToken) where
    show (MkBounded l c t) = "line=" ++ show l ++ " col=" ++ show c ++ " tok=" ++ show t

opChars : String
opChars = "+-*"

operator : Lexer
operator = some (oneOf opChars)

toInt' : String -> Integer
toInt' = cast

expressionTokens : TokenMap ExpressionToken
expressionTokens = [
    (digits, \x => Number (toInt' x)),
    (operator, \x => Operator x),
    (is '(', \x => OParen),
    (is ')', \x => CParen)
]

Rule : Type -> Type
Rule ty = Grammar () ExpressionToken True ty

intLiteral : Rule Integer
intLiteral = terminal "" (\x => case x of 
                                    Number i => Just i 
                                    _ => Nothing)