@@ -5,9 +5,7 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances,
9− GeneralizedNewtypeDeriving, PatternGuards, StandaloneDeriving,
10− TypeSynonymInstances #-}
8+{-# LANGUAGE ConstraintKinds, FlexibleContexts #-}
119module Idris.Parser.Helpers where
1210
1311import Idris.AbsSyntax
@@ -23,71 +21,58 @@ import Prelude hiding (pi)
2321import Control.Applicative
2422import Control.Monad
2523import Control.Monad.State.Strict
26−import qualified Data.ByteString.UTF8 as UTF8
2724import Data.Char
2825import qualified Data.HashSet as HS
2926import Data.List
27+import qualified Data.List.NonEmpty as NonEmpty
3028import qualified Data.Map as M
3129import Data.Maybe
3230import qualified Data.Text as T
31+import Data.Void (Void(..))
3332import System.FilePath
34−import qualified Text.Parser.Char as Chr
35−import Text.Parser.LookAhead
36−import qualified Text.Parser.Token as Tok
33+import Text.Megaparsec ((<?>))
34+import qualified Text.Megaparsec as P
35+import qualified Text.Megaparsec.Char as P
36+import qualified Text.Megaparsec.Char.Lexer as P hiding (space)
3737import qualified Text.PrettyPrint.ANSI.Leijen as PP
38−import Text.Trifecta ((<?>))
39−import qualified Text.Trifecta as P
40−import qualified Text.Trifecta.Delta as P
38+
4139
4240-- | Idris parser with state used during parsing
43−type IdrisParser = StateT IState P.Parser
44−
45−#if MIN_VERSION_base(4,9,0)
46−instance {-# OVERLAPPING #-} P.DeltaParsing IdrisParser where
47− line = lift P.line
48− {-# INLINE line #-}
49− position = lift P.position
50− {-# INLINE position #-}
51− slicedWith f (StateT m) = StateT $ \s -> P.slicedWith (\(a,s') b -> (f a b, s')) $ m s
52− {-# INLINE slicedWith #-}
53− rend = lift P.rend
54− {-# INLINE rend #-}
55− restOfLine = lift P.restOfLine
56− {-# INLINE restOfLine #-}
57−#endif
58−
59−someSpace' :: MonadicParsing m => m ()
60−someSpace' = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
61−
62−instance {-# OVERLAPPING #-} P.TokenParsing IdrisParser where
63− someSpace = someSpace'
64− token p = do s <- get
65− (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC
66− -- See Issue #1594
67− r <- p
68− (FC fn _ (el, ec)) <- getFC
69− whiteSpace
70− put (s { lastTokenSpan = Just (FC fn (sl, sc) (el, ec)) })
71− return r
41+type IdrisParser = StateT IState IdrisInnerParser
42+type IdrisInnerParser = P.Parsec Void String
43+type ParseState = P.State String
44+data ParseError = ParseError String (P.ParseError (P.Token String) Void)
45+
46+parseErrorPretty :: ParseError -> String
47+parseErrorPretty (ParseError s err) = P.parseErrorPretty' s err
48+
49+parseErrorDoc :: ParseError -> PP.Doc
50+parseErrorDoc = PP.string . parseErrorPretty
7251
7352-- | Generalized monadic parsing constraint type
74−type MonadicParsing m = (P.DeltaParsing m, LookAheadParsing m, Monad m)
53+type MonadicParsing m = (P.MonadParsec Void String m)
7554
76−class HasLastTokenSpan m where
77− getLastTokenSpan :: m (Maybe FC)
55+someSpace :: MonadicParsing m => m ()
56+someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
7857
79−instance HasLastTokenSpan IdrisParser where
80− getLastTokenSpan = lastTokenSpan <$> get
58+tokenFC :: MonadicParsing m => m a -> m (a, FC)
59+tokenFC p = do (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC
60+ -- See Issue #1594
61+ r <- p
62+ (FC fn _ (el, ec)) <- getFC
63+ whiteSpace
64+ return (r, FC fn (sl, sc) (el, ec))
8165
82−newtype ParseError = ParseError { parseErrorDoc :: PP.Doc }
66+token :: MonadicParsing m => m a -> m a
67+token p = p <* whiteSpace
8368
8469-- | Helper to run Idris inner parser based stateT parsers
85−runparser :: StateT st P.Parser res -> st -> String -> String -> Either ParseError res
70+runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Either ParseError res
8671runparser p i inputname s =
87− case P.parseString (evalStateT p i)
88− (P.Directed (UTF8.fromString inputname) 0 0 0 0) s of
89− P.Failure (P.ErrInfo doc _) -> Left (ParseError doc)
90− P.Success value -> Right value
72+ case P.parse (evalStateT p i) inputname s of
73+ Left err -> Left $ ParseError s err
74+ Right v -> Right v
75+
9176
9277highlightP :: FC -> OutputAnnotation -> IdrisParser ()
9378highlightP fc annot = do ist <- get
@@ -136,7 +121,7 @@ isEol _ = False
136121
137122-- | A parser that succeeds at the end of the line
138123eol :: MonadicParsing m => m ()
139−eol = () <$ P.satisfy isEol <|> lookAhead P.eof <?> "end of line"
124+eol = () <$ P.satisfy isEol <|> P.lookAhead P.eof <?> "end of line"
140125
141126{- | Consumes a single-line comment
142127
@@ -145,10 +130,7 @@ eol = () <$ P.satisfy isEol <|> lookAhead P.eof <?> "end of line"
145130@
146131 -}
147132singleLineComment :: MonadicParsing m => m ()
148−singleLineComment = (string "--" *>
149− many (P.satisfy (not . isEol)) *>
150− eol *> pure ())
151− <?> ""
133+singleLineComment = P.hidden (() <$ string "--" *> many (P.satisfy (not . isEol)) *> eol)
152134
153135{- | Consumes a multi-line comment
154136
@@ -168,9 +150,8 @@ singleLineComment = (string "--" *>
168150@
169151-}
170152multiLineComment :: MonadicParsing m => m ()
171−multiLineComment = P.try (string "{-" *> (string "-}") *> pure ())
172− <|> string "{-" *> inCommentChars
173− <?> ""
153+multiLineComment = P.hidden $ P.try (string "{-" *> string "-}" *> pure ())
154+ <|> string "{-" *> inCommentChars
174155 where inCommentChars :: MonadicParsing m => m ()
175156 inCommentChars = string "-}" *> pure ()
176157 <|> P.try (multiLineComment) *> inCommentChars
@@ -199,56 +180,47 @@ docComment = do dc <- pushIndent *> docCommentLine
199180 map (\(n, d) -> (n, parseDocstring (T.pack d))) args)
200181
201182 where docCommentLine :: MonadicParsing m => m String
202− docCommentLine = P.try (do string "|||"
203− many (P.satisfy (==' '))
204− contents <- P.option "" (do first <- P.satisfy (\c -> not (isEol c || c == '@'))
205− res <- many (P.satisfy (not . isEol))
206− return $ first:res)
207− eol ; someSpace'
208− return contents)
209− <?> ""
210−
211− argDocCommentLine = do string "|||"
212− many (P.satisfy isSpace)
213− char '@'
214− many (P.satisfy isSpace)
183+ docCommentLine = P.hidden $ P.try $ do
184+ string "|||"
185+ many (P.satisfy (==' '))
186+ contents <- P.option "" (do first <- P.satisfy (\c -> not (isEol c || c == '@'))
187+ res <- many (P.satisfy (not . isEol))
188+ return $ first:res)
189+ eol ; someSpace
190+ return contents
191+
192+ argDocCommentLine :: IdrisParser (Name, String)
193+ argDocCommentLine = do P.string "|||"
194+ P.many (P.satisfy isSpace)
195+ P.char '@'
196+ P.many (P.satisfy isSpace)
215197 n <- fst <$> name
216− many (P.satisfy isSpace)
217− docs <- many (P.satisfy (not . isEol))
218− eol ; someSpace'
198+ P.many (P.satisfy isSpace)
199+ docs <- P.many (P.satisfy (not . isEol))
200+ P.eol ; someSpace
219201 return (n, docs)
220202
221203-- | Parses some white space
222204whiteSpace :: MonadicParsing m => m ()
223−whiteSpace = Tok.whiteSpace
205+whiteSpace = someSpace <|> pure ()
224206
225207-- | Parses a string literal
226−stringLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC)
227−stringLiteral = do str <- Tok.stringLiteral
228− fc <- getLastTokenSpan
229− return (str, fromMaybe NoFC fc)
208+stringLiteral :: MonadicParsing m => m (String, FC)
209+stringLiteral = tokenFC . P.try $ P.char '"' *> P.manyTill P.charLiteral (P.char '"')
230210
231211-- | Parses a char literal
232−charLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (Char, FC)
233−charLiteral = do ch <- Tok.charLiteral
234− fc <- getLastTokenSpan
235− return (ch, fromMaybe NoFC fc)
212+charLiteral :: IdrisParser (Char, FC)
213+charLiteral = tokenFC . P.try $ P.char '\'' *> P.charLiteral <* P.char '\''
236214
237215-- | Parses a natural number
238−natural :: (MonadicParsing m, HasLastTokenSpan m) => m (Integer, FC)
239−natural = do n <- Tok.natural
240− fc <- getLastTokenSpan
241− return (n, fromMaybe NoFC fc)
242−
243−-- | Parses an integral number
244−integer :: MonadicParsing m => m Integer
245−integer = Tok.integer
216+natural :: IdrisParser (Integer, FC)
217+natural = tokenFC ( P.try (P.char '0' *> P.char' 'x' *> P.hexadecimal)
218+ <|> P.try (P.char '0' *> P.char' 'o' *> P.octal)
219+ <|> P.try P.decimal)
246220
247221-- | Parses a floating point number
248−float :: (MonadicParsing m, HasLastTokenSpan m) => m (Double, FC)
249−float = do f <- Tok.double
250− fc <- getLastTokenSpan
251− return (f, fromMaybe NoFC fc)
222+float :: IdrisParser (Double, FC)
223+float = tokenFC . P.try $ P.float
252224
253225{- * Symbols, identifiers, names and operators -}
254226
@@ -264,30 +236,29 @@ reservedIdentifiers = HS.fromList
264236 ]
265237
266238identifierOrReserved :: MonadicParsing m => m String
267−identifierOrReserved = P.token $ P.try $ do
239+identifierOrReserved = token $ P.try $ do
268240 c <- P.satisfy isAlpha <|> P.oneOf "_"
269241 cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf "_'.")
270242 return $ c : cs
271243
272244char :: MonadicParsing m => Char -> m Char
273−char = Chr.char
245+char = P.char
274246
275247string :: MonadicParsing m => String -> m String
276−string = Chr.string
248+string = P.string
277249
278250-- | Parses a character as a token
279251lchar :: MonadicParsing m => Char -> m Char
280−lchar = P.token . P.char
252+lchar = token . P.char
281253
282254-- | Parses a character as a token, returning the source span of the character
283255lcharFC :: MonadicParsing m => Char -> m FC
284256lcharFC ch = do (FC file (l, c) _) <- getFC
285− _ <- P.token (char ch)
257+ _ <- token (P.char ch)
286258 return $ FC file (l, c) (l, c+1)
287259
288−-- | Parses string as a token
289260symbol :: MonadicParsing m => String -> m ()
290−symbol = void . Tok.symbol
261+symbol = void . P.symbol someSpace
291262
292263symbolFC :: MonadicParsing m => String -> m FC
293264symbolFC str = do (FC file (l, c) _) <- getFC
@@ -296,7 +267,7 @@ symbolFC str = do (FC file (l, c) _) <- getFC
296267
297268-- | Parses a reserved identifier
298269reserved :: MonadicParsing m => String -> m ()
299−reserved name = P.token $ P.try $ do
270+reserved name = token $ P.try $ do
300271 P.string name
301272 P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name
302273
@@ -314,7 +285,7 @@ reservedHL str = reservedFC str >>= flip highlightP AnnKeyword
314285-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
315286-- | Parses a reserved operator
316287reservedOp :: MonadicParsing m => String -> m ()
317−reservedOp name = P.token $ P.try $
288+reservedOp name = token $ P.try $
318289 do string name
319290 P.notFollowedBy operatorLetter <?> ("end of " ++ show name)
320291
@@ -328,8 +299,8 @@ identifier :: (MonadicParsing m) => m (String, FC)
328299identifier = P.try $ do
329300 (FC f (l, c) _) <- getFC
330301 ident <- identifierOrReserved
331− when (ident `HS.member` reservedIdentifiers) $ P.unexpected $ "reserved " ++ ident
332− when (ident == "_") $ P.unexpected "wildcard"
302+ when (ident `HS.member` reservedIdentifiers) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved " ++ ident
303+ when (ident == "_") $ P.unexpected . P.Label . NonEmpty.fromList $ "wildcard"
333304 return (ident, FC f (l, c) (l, c + length ident))
334305
335306-- | Parses an identifier with possible namespace as a name
@@ -340,8 +311,8 @@ iName bad = maybeWithNS identifier False bad <?> "name"
340311maybeWithNS :: (MonadicParsing m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)
341312maybeWithNS parser ascend bad = do
342313 fc <- getFC
343− i <- P.option "" (lookAhead (fst <$> identifier))
344− when (i `elem` bad) $ P.unexpected "reserved identifier"
314+ i <- P.option "" (P.lookAhead (fst <$> identifier))
315+ when (i `elem` bad) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved identifier"
345316 let transf = if ascend then id else reverse
346317 (x, xs, fc) <- P.choice (transf (parserNoNS parser : parsersNS parser i))
347318 return (mkName (x, xs), fc)
@@ -410,7 +381,7 @@ invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%
410381
411382-- | Parses an operator
412383symbolicOperator :: MonadicParsing m => m String
413−symbolicOperator = do op <- P.token . some $ operatorLetter
384+symbolicOperator = do op <- token . some $ operatorLetter
414385 when (op `elem` (invalidOperators ++ commentMarkers)) $
415386 fail $ op ++ " is not a valid operator"
416387 return op
@@ -422,32 +393,17 @@ symbolicOperatorFC = do (FC f (l, c) _) <- getFC
422393 return (op, FC f (l, c) (l, c + length op))
423394
424395{- * Position helpers -}
425−{- | Get filename from position (returns "(interactive)" when no source file is given) -}
426−fileName :: P.Delta -> String
427−fileName (P.Directed fn _ _ _ _) = UTF8.toString fn
428−fileName _ = "(interactive)"
429−
430−{- | Get line number from position -}
431−lineNum :: P.Delta -> Int
432−lineNum (P.Lines l _ _ _) = fromIntegral l + 1
433−lineNum (P.Directed _ l _ _ _) = fromIntegral l + 1
434−lineNum _ = 0
435−
436−{- | Get column number from position -}
437−columnNum :: P.Delta -> Int
438−columnNum pos = fromIntegral (P.column pos) + 1
439−
440−
441396{- | Get file position as FC -}
442397getFC :: MonadicParsing m => m FC
443−getFC = do s <- P.position
444− let (dir, file) = splitFileName (fileName s)
445− let f = if dir == addTrailingPathSeparator "." then file else fileName s
446− return $ FC f (lineNum s, columnNum s) (lineNum s, columnNum s) -- TODO: Change to actual spanning
398+getFC = do pos <- P.getPosition
399+ let columnNumber = P.unPos . P.sourceColumn $ pos
400+ let lineNumber = P.unPos . P.sourceLine $ pos
401+ let (dir, file) = splitFileName (P.sourceName pos)
402+ let f = if dir == addTrailingPathSeparator "." then file else P.sourceName pos
403+ return $ FC f (lineNumber, columnNumber) (lineNumber, columnNumber) -- TODO: Change to actual spanning
447404 -- Issue #1594 on the Issue Tracker.
448405 -- https://github.com/idris-lang/Idris-dev/issues/1594
449406
450−
451407{-* Syntax helpers-}
452408-- | Bind constraints to term
453409bindList :: (RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm) -> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
@@ -457,15 +413,15 @@ bindList b ((r, n, fc, t):bs) sc = b r n fc t (bindList b bs sc)
457413{- | @commaSeparated p@ parses one or more occurences of `p`,
458414 separated by commas and optional whitespace. -}
459415commaSeparated :: MonadicParsing m => m a -> m [a]
460−commaSeparated p = p `P.sepBy1` (P.spaces >> P.char ',' >> P.spaces)
416+commaSeparated p = p `P.sepBy1` (P.space >> P.char ',' >> P.space)
461417
462418{- * Layout helpers -}
463419
464420-- | Push indentation to stack
465421pushIndent :: IdrisParser ()
466−pushIndent = do pos <- P.position
422+pushIndent = do columnNumber <- indent
467423 ist <- get
468− put (ist { indent_stack = (fromIntegral (P.column pos) + 1) : indent_stack ist })
424+ put (ist { indent_stack = columnNumber : indent_stack ist })
469425
470426-- | Pops indentation from stack
471427popIndent :: IdrisParser ()
@@ -476,8 +432,8 @@ popIndent = do ist <- get
476432
477433
478434-- | Gets current indentation
479−indent :: IdrisParser Int
480−indent = liftM ((+1) . fromIntegral . P.column) P.position
435+indent :: MonadicParsing m => m Int
436+indent = P.unPos . P.sourceColumn <$> P.getPosition
481437
482438-- | Gets last indentation
483439lastIndent :: IdrisParser Int
@@ -520,8 +476,7 @@ indentedBlockS p = do openBlock
520476
521477-- | Checks if the following character matches provided parser
522478lookAheadMatches :: MonadicParsing m => m a -> m Bool
523−lookAheadMatches p = do match <- lookAhead (optional p)
524− return $ isJust match
479+lookAheadMatches p = isJust <$> P.lookAhead (P.optional p)
525480
526481-- | Parses a start of block
527482openBlock :: IdrisParser ()
@@ -565,7 +520,7 @@ terminator = do lchar ';'; popIndent
565520 if c <= l then popIndent else fail "not a terminator"
566521 <|> do isParen <- lookAheadMatches (P.oneOf ")}")
567522 if isParen then popIndent else fail "not a terminator"
568− <|> lookAhead P.eof
523+ <|> P.lookAhead P.eof
569524
570525-- | Parses and keeps a terminator
571526keepTerminator :: IdrisParser ()
@@ -575,7 +530,7 @@ keepTerminator = () <$ lchar ';'
575530 <|> do isParen <- lookAheadMatches (P.oneOf ")}|")
576531 isIn <- lookAheadMatches (reserved "in")
577532 unless (isIn || isParen) $ fail "not a terminator"
578− <|> lookAhead P.eof
533+ <|> P.lookAhead P.eof
579534
580535-- | Checks if application expression does not end
581536notEndApp :: IdrisParser ()
@@ -587,7 +542,7 @@ notEndBlock :: IdrisParser ()
587542notEndBlock = do ist <- get
588543 case brace_stack ist of
589544 Just lvl : xs -> do i <- indent
590− isParen <- lookAheadMatches (char ')')
545+ isParen <- lookAheadMatches (P.char ')')
591546 when (i < lvl || isParen) (fail "end of block")
592547 _ -> return ()
593548