Grammar stack overflow

Grammar.idr

module Test

import Text.Lexer
import Text.Parser


data Token : Type where
  AddOp : Token
  MulOp : Token
  IntConst : Token
  LP : Token
  RP : Token

TokenKind Token where
  TokType IntConst = Integer
  TokType AddOp = ()
  TokType MulOp = ()
  TokType LP = ()
  TokType RP = ()

  tokValue IntConst s = (cast s)
  tokValue AddOp _ = ()
  tokValue MulOp _ = ()
  tokValue LP _ = ()
  tokValue RP _ = ()

Eq Token where
  (==) AddOp AddOp = True
  (==) MulOp MulOp = True
  (==) IntConst IntConst = True
  (==) LP LP = True
  (==) RP RP = True
  (==) _ _ = False

namespace Expr
  data Expr : Type where
    IntConst : Integer -> Expr
    Add : Expr -> Expr -> Expr
    Mul : Expr -> Expr -> Expr

gchainl1 : Grammar t True (a -> a -> a) -> Grammar t True a -> Grammar t True a
gchainl1 op p = p >>= rest op p
  where rest : Grammar t True (a -> a -> a) -> Grammar t True a -> (a -> Grammar t False a)
        rest op p a = (do f <- op
                          b <- p
                          rest op p (f a b)) <|> pure a

intConst : Grammar (TokenData (Token Token)) True Integer
intConst = do i <- mapToken tok $ match Test.IntConst
              pure i

mutual
  factor : Grammar (TokenData (Token Token)) True Expr
  factor = (do i <- intConst
               pure (IntConst i)) <|> (between (mapToken tok $ match LP) (mapToken tok $ match RP) expr)

  mulOp : Grammar (TokenData (Token Token)) True (Expr -> Expr -> Expr)
  mulOp = mapToken tok $ match MulOp *> pure Mul

  term : Grammar (TokenData (Token Token)) True Expr
  term = gchainl1 mulOp factor

  addOp : Grammar (TokenData (Token Token)) True (Expr -> Expr -> Expr)
  addOp = mapToken tok $ match AddOp *> pure Add

  expr : Grammar (TokenData (Token Token)) True Expr
  expr = gchainl1 addOp term

test : IO ()
test = case (parse expr [MkToken 0 0 (Tok IntConst "123"), MkToken 0 5 (Tok AddOp "+"), MkToken 0 7 (Tok IntConst "345")]) of
            Left l => print "fail"
            Right (t, _) => print "success"