ParseError.idr

data Ty = N
        | Arrow Ty Ty

-- Lexer: token definition
public export
data Token = Var String
           | Keyword String
           | Symbol String
           | Ignore String

export
Show Token where
    show (Var x) = "Var" ++ x
    show (Keyword s) = s
    show (Symbol s) = s
    show (Ignore _) = ""

comment : Lexer
comment = is ';' <+> is ';' <+> some (isNot '\n') <+> is '\n'

keywords : List String
keywords = ["z", "s", "Z", "S", "rec", "nat", "N"]

symbols : List String
symbols = ["(", ")", "[", "]", ",", ".", "\\", "->"]

var : Lexer
var = pred idBegin <+> many (pred idChar)
  where
    idBegin : Char -> Bool
    idBegin '_' = True
    idBegin x = isAlpha x
    
    idChar : Char -> Bool
    idChar '\'' = True
    idChar '_' = True
    idChar x = isAlphaNum x

validSymbol : Lexer
validSymbol = some (oneOf ",.\\()[]->")


rawTokens : TokenMap Token
rawTokens = 
  map (\x => (exact x, Keyword)) keywords ++
  map (\x => (exact x, Symbol)) symbols ++
  [(var, Var), 
   (comment, Ignore),
   (validSymbol, Symbol),
   (space, Ignore)]
   
public export
data Token = Var String
           | Keyword String
           | Symbol String
           | Ignore String

-- I stole this from edwinb
export
lex : String -> Either (List (TokenData Token)) (Int, Int, String)
lex str
  = case Lexer.lex rawTokens str of
         (tok, (_, _, "")) => Left (filter notIgnore tok)
         (_, fail) => Right fail
  where
    notIgnore : TokenData Token -> Bool
    notIgnore token = case tok token of
                            Ignore _ => False
                            _ => True


-- Rules
symbol : String -> Rule ()
symbol req
    = terminal (\x => case tok x of
                           Symbol s => if s == req then Just ()
                                                   else Nothing
                           _ => Nothing)

keyword : String -> Rule ()
keyword req
    = terminal (\x => case tok x of
                           Keyword s => if s == req then Just ()
                                                    else Nothing
                           _ => Nothing)

var : Rule String
var = terminal (\x => case tok x of
                           Var str => Just str
                           _ => Nothing)

||| This is what's causing the trouble
type : Rule Ty
type = do keyword "nat"
          commit
          pure N
   <|> do t1 <- type; symbol "->"; t2 <- type
          commit
          pure (Arrow N N)
   
          
-- Parsing
public export
Rule : Type -> Type
Rule ty = Grammar (TokenData Token) True ty

public export
EmptyRule : Type -> Type
EmptyRule ty = Grammar (TokenData Token) False ty

public export
data ParseError = ParseFail String (Maybe (Int, Int)) (List Token)
                | LexFail (Int, Int, String)


public export
parseStr : String -> Rule t -> Either t ParseError
parseStr str rule
  = case lex str of
         Right lexError => Right $ LexFail lexError
         Left toks =>
           case parse toks (do res <- rule; eof; pure res) of
                Left (Error err []) => Right $ ParseFail err Nothing []
                Left (Error err (t::ts)) => Right $ ParseFail err (Just (line t, col t)) (map tok (t::ts))
                Right (val, _) => Left val

mutual
  simpleType : Rule Ty
  simpleType = do symbol "("; commit
                  t <- type
                  symbol ")"
                  pure t
           <|> do keyword "nat"; pure N


  type : Rule Ty
  type = do t1 <- simpleType
            symbol "->"; commit
            t2 <- type
            pure $ Arrow t1 t2
     <|> simpleType