@@ -4,7 +4,7 @@ module Idris.Parser where
44import Prelude hiding (pi)
55
66import Text.Trifecta.Delta
7−import Text.Trifecta hiding (span, token, whiteSpace, stringLiteral, charLiteral, natural, symbol, char, string)
7+import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)
88import Text.Parser.LookAhead
99import Text.Parser.Expression
1010import qualified Text.Parser.Token as Tok
@@ -56,15 +56,18 @@ import System.FilePath
5656
5757
5858-- | Idris parser with state used during parsing
59−type IdrisParser = StateT IState Parser
59+type IdrisParser = StateT IState IdrisInnerParser
60+
61+newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }
62+ deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, Parsing, DeltaParsing, MarkParsing Delta, Monoid)
63+
64+instance TokenParsing IdrisInnerParser where
65+ someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
6066
6167-- | Generalized monadic parsing constraint type
6268type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)
6369
6470{- * Space, comments and literals (token/lexing like parsers) -}
65−-- | Parses a token by applying parser and then consuming all following whiteSpace
66−lexeme :: MonadicParsing m => m a -> m a
67−lexeme p = p <* whiteSpace
6871
6972-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)
7073simpleWhiteSpace :: MonadicParsing m => m ()
@@ -135,29 +138,29 @@ docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; ret
135138 <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")
136139 <?> ""
137140
138−-- | Consumes whitespace (and comments)
141+-- | Parses some white space
139142whiteSpace :: MonadicParsing m => m ()
140−whiteSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
143+whiteSpace = Tok.whiteSpace
141144
142145-- | Parses a string literal
143146stringLiteral :: MonadicParsing m => m String
144−stringLiteral = lexeme $ Tok.stringLiteral
147+stringLiteral = Tok.stringLiteral
145148
146149-- | Parses a char literal
147150charLiteral :: MonadicParsing m => m Char
148−charLiteral = lexeme $ Tok.charLiteral
151+charLiteral = Tok.charLiteral
149152
150153-- | Parses a natural number
151154natural :: MonadicParsing m => m Integer
152−natural = lexeme $ Tok.natural
155+natural = Tok.natural
153156
154157-- | Parses an integral number
155158integer :: MonadicParsing m => m Integer
156−integer = lexeme $ Tok.integer
159+integer = Tok.integer
157160
158161-- | Parses a floating point number
159162float :: MonadicParsing m => m Double
160−float = lexeme $ Tok.double
163+float = Tok.double
161164
162165{- * Symbols, identifiers, names and operators -}
163166
@@ -186,28 +189,28 @@ char = Chr.char
186189string :: MonadicParsing m => String -> m String
187190string = Chr.string
188191
189−-- | Parses a character as a lexeme
192+-- | Parses a character as a token
190193lchar :: MonadicParsing m => Char -> m Char
191−lchar = lexeme . char
194+lchar = token . char
192195
193−-- | Parses string as a lexeme
196+-- | Parses string as a token
194197symbol :: MonadicParsing m => String -> m String
195−symbol = lexeme . Tok.symbol
198+symbol = Tok.symbol
196199
197200-- | Parses a reserved identifier
198201reserved :: MonadicParsing m => String -> m ()
199−reserved = lexeme . Tok.reserve idrisStyle
202+reserved = Tok.reserve idrisStyle
200203
201204-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
202205-- | Parses a reserved operator
203206reservedOp :: MonadicParsing m => String -> m ()
204−reservedOp name = lexeme $ try $
207+reservedOp name = token $ try $
205208 do string name
206209 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
207210
208−-- | Parses an identifier as a lexeme
211+-- | Parses an identifier as a token
209212identifier :: MonadicParsing m => m String
210−identifier = lexeme $ Tok.ident idrisStyle
213+identifier = token $ Tok.ident idrisStyle
211214
212215-- | Parses an identifier with possible namespace as a name
213216iName :: MonadicParsing m => [String] -> m Name
@@ -261,7 +264,7 @@ operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
261264
262265-- | Parses an operator
263266operator :: MonadicParsing m => m String
264−operator = do op <- lexeme . some $ operatorLetter
267+operator = do op <- token . some $ operatorLetter
265268 when (op == ":") $ fail "(:) is not a valid operator"
266269 return op
267270
@@ -2536,17 +2539,17 @@ fullTactic syn = do t <- tactic syn
25362539{- * Loading and parsing -}
25372540{- | Parses an expression from input -}
25382541parseExpr :: IState -> String -> Result PTerm
2539−parseExpr st = parseString (evalStateT (fullExpr defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
2542+parseExpr st = parseString (runInnerParser (evalStateT (fullExpr defaultSyntax) st)) (Directed (UTF8.fromString "(input)") 0 0 0 0)
25402543
25412544{- | Parses a tactic from input -}
25422545parseTactic :: IState -> String -> Result PTactic
2543−parseTactic st = parseString (evalStateT (fullTactic defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
2546+parseTactic st = parseString (runInnerParser (evalStateT (fullTactic defaultSyntax) st)) (Directed (UTF8.fromString "(input)") 0 0 0 0)
25442547
25452548-- | Parse module header and imports
25462549parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)
25472550parseImports fname input
25482551 = do i <- getIState
2549− case parseString (evalStateT imports i) (Directed (UTF8.fromString fname) 0 0 0 0) input of
2552+ case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
25502553 Failure err -> fail (show err)
25512554 Success (x, i) -> do -- Discard state updates (there should be
25522555 -- none anyway)
@@ -2570,7 +2573,7 @@ parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
25702573 Idris [PDecl]
25712574parseProg syn fname input mrk
25722575 = do i <- getIState
2573− case parseString (evalStateT mainProg i) (Directed (UTF8.fromString fname) 0 0 0 0) input of
2576+ case parseString (runInnerParser (evalStateT mainProg i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
25742577 Failure doc -> do iputStrLn (show doc)
25752578 -- FIXME: Get error location from trifecta
25762579 --let errl = sourceLine (errorPos err)