@@ -5,9 +5,9 @@ Copyright :
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances,
8+{-# LANGUAGE CPP, ConstraintKinds, FlexibleContexts, FlexibleInstances,
99 GeneralizedNewtypeDeriving, PatternGuards, StandaloneDeriving,
10− TypeSynonymInstances #-}
10+ TypeSynonymInstances, UndecidableInstances #-}
1111module Idris.Parser.Helpers where
1212
1313import Idris.AbsSyntax
@@ -23,7 +23,6 @@ import Prelude hiding (pi)
2323import Control.Applicative
2424import Control.Monad
2525import Control.Monad.State.Strict
26−import qualified Data.ByteString.UTF8 as UTF8
2726import Data.Char
2827import qualified Data.HashSet as HS
2928import Data.List
@@ -31,34 +30,40 @@ import qualified Data.Map as M
3130import Data.Maybe
3231import qualified Data.Text as T
3332import System.FilePath
34−import qualified Text.Parser.Char as Chr
35−import Text.Parser.LookAhead
33+import Data.List.NonEmpty (fromList)
34+import qualified Text.Parser.Char
35+import qualified Text.Parser.Combinators
3636import qualified Text.Parser.Token as Tok
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+import Text.Megaparsec ((<?>))
39+import qualified Text.Megaparsec as P
40+import qualified Text.Megaparsec.Char as P
41+import qualified Text.Megaparsec.Char.Lexer as P hiding (space)
42+
43+newtype ParseError = ParseError { parseErrorDoc :: PP.Doc }
4144
4245-- | 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
46+type IdrisParser = StateT IState IdrisInnerParser
47+type IdrisInnerParser = P.Parsec () String
48+type ParseState = P.State String
49+
50+-- | Generalized monadic parsing constraint type
51+type MonadicParsing m = (P.MonadParsec () String m, Tok.TokenParsing m)
5852
5953someSpace' :: MonadicParsing m => m ()
6054someSpace' = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
6155
56+instance Text.Parser.Combinators.Parsing IdrisInnerParser where
57+ eof = P.eof
58+ unexpected msg = P.unexpected . P.Label . fromList $ msg
59+ try = P.try
60+ p <?> s = p <?> s --FIXME:?
61+ notFollowedBy = P.notFollowedBy
62+ --FIXME:
63+instance Text.Parser.Char.CharParsing IdrisInnerParser where
64+ satisfy = P.satisfy
65+ --FIXME:??
66+
6267instance {-# OVERLAPPING #-} Tok.TokenParsing IdrisParser where
6368 someSpace = someSpace'
6469 token p = do s <- get
@@ -70,18 +75,12 @@ instance {-# OVERLAPPING #-} Tok.TokenParsing IdrisParser where
7075 put (s { lastTokenSpan = Just (FC fn (sl, sc) (el, ec)) })
7176 return r
7277
73−-- | Generalized monadic parsing constraint type
74−type MonadicParsing m = (P.DeltaParsing m, LookAheadParsing m, Monad m)
75−
76−newtype ParseError = ParseError { parseErrorDoc :: PP.Doc }
77−
7878-- | Helper to run Idris inner parser based stateT parsers
79−runparser :: StateT st P.Parser res -> st -> String -> String -> Either ParseError res
79+runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Either ParseError res
8080runparser p i inputname s =
81− case P.parseString (evalStateT p i)
82− (P.Directed (UTF8.fromString inputname) 0 0 0 0) s of
83− P.Failure (P.ErrInfo doc _) -> Left (ParseError doc)
84− P.Success value -> Right value
81+ case P.parse (evalStateT p i) inputname s of
82+ Left _ -> Left $ ParseError undefined --FIXME:
83+ Right value -> Right value
8584
8685highlightP :: FC -> OutputAnnotation -> IdrisParser ()
8786highlightP fc annot = do ist <- get
@@ -130,7 +129,7 @@ isEol _ = False
130129
131130-- | A parser that succeeds at the end of the line
132131eol :: MonadicParsing m => m ()
133−eol = () <$ P.satisfy isEol <|> lookAhead P.eof <?> "end of line"
132+eol = () <$ P.satisfy isEol <|> P.lookAhead P.eof <?> "end of line"
134133
135134{- | Consumes a single-line comment
136135
@@ -202,14 +201,15 @@ docComment = do dc <- pushIndent *> docCommentLine
202201 return contents)
203202 <?> ""
204203
205− argDocCommentLine = do string "|||"
206− many (P.satisfy isSpace)
207− char '@'
208− many (P.satisfy isSpace)
204+ argDocCommentLine :: IdrisParser (Name, String)
205+ argDocCommentLine = do P.string "|||"
206+ P.many (P.satisfy isSpace)
207+ P.char '@'
208+ P.many (P.satisfy isSpace)
209209 n <- fst <$> name
210− many (P.satisfy isSpace)
211− docs <- many (P.satisfy (not . isEol))
212− eol ; someSpace'
210+ P.many (P.satisfy isSpace)
211+ docs <- P.many (P.satisfy (not . isEol))
212+ P.eol ; someSpace'
213213 return (n, docs)
214214
215215-- | Parses some white space
@@ -254,30 +254,29 @@ reservedIdentifiers = HS.fromList
254254 ]
255255
256256identifierOrReserved :: MonadicParsing m => m String
257−identifierOrReserved = P.token $ P.try $ do
257+identifierOrReserved = Tok.token $ P.try $ do
258258 c <- P.satisfy isAlpha <|> P.oneOf "_"
259259 cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf "_'.")
260260 return $ c : cs
261261
262262char :: MonadicParsing m => Char -> m Char
263−char = Chr.char
263+char = P.char
264264
265265string :: MonadicParsing m => String -> m String
266−string = Chr.string
266+string = P.string
267267
268268-- | Parses a character as a token
269269lchar :: MonadicParsing m => Char -> m Char
270−lchar = P.token . P.char
270+lchar = Tok.token . P.char
271271
272272-- | Parses a character as a token, returning the source span of the character
273273lcharFC :: MonadicParsing m => Char -> m FC
274274lcharFC ch = do (FC file (l, c) _) <- getFC
275− _ <- P.token (char ch)
275+ _ <- Tok.token (P.char ch)
276276 return $ FC file (l, c) (l, c+1)
277277
278−-- | Parses string as a token
279278symbol :: MonadicParsing m => String -> m ()
280−symbol = void . Tok.symbol
279+symbol = void . P.symbol someSpace'
281280
282281symbolFC :: MonadicParsing m => String -> m FC
283282symbolFC str = do (FC file (l, c) _) <- getFC
@@ -286,7 +285,7 @@ symbolFC str = do (FC file (l, c) _) <- getFC
286285
287286-- | Parses a reserved identifier
288287reserved :: MonadicParsing m => String -> m ()
289−reserved name = P.token $ P.try $ do
288+reserved name = Tok.token $ P.try $ do
290289 P.string name
291290 P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name
292291
@@ -304,7 +303,7 @@ reservedHL str = reservedFC str >>= flip highlightP AnnKeyword
304303-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
305304-- | Parses a reserved operator
306305reservedOp :: MonadicParsing m => String -> m ()
307−reservedOp name = P.token $ P.try $
306+reservedOp name = Tok.token $ P.try $
308307 do string name
309308 P.notFollowedBy operatorLetter <?> ("end of " ++ show name)
310309
@@ -318,8 +317,8 @@ identifier :: (MonadicParsing m) => m (String, FC)
318317identifier = P.try $ do
319318 (FC f (l, c) _) <- getFC
320319 ident <- identifierOrReserved
321− when (ident `HS.member` reservedIdentifiers) $ P.unexpected $ "reserved " ++ ident
322− when (ident == "_") $ P.unexpected "wildcard"
320+ when (ident `HS.member` reservedIdentifiers) $ P.unexpected undefined --FIXME: $ "reserved " ++ ident
321+ when (ident == "_") $ P.unexpected undefined --FIXME: "wildcard"
323322 return (ident, FC f (l, c) (l, c + length ident))
324323
325324-- | Parses an identifier with possible namespace as a name
@@ -330,8 +329,8 @@ iName bad = maybeWithNS identifier False bad <?> "name"
330329maybeWithNS :: (MonadicParsing m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)
331330maybeWithNS parser ascend bad = do
332331 fc <- getFC
333− i <- P.option "" (lookAhead (fst <$> identifier))
334− when (i `elem` bad) $ P.unexpected "reserved identifier"
332+ i <- P.option "" (P.lookAhead (fst <$> identifier))
333+ when (i `elem` bad) $ P.unexpected undefined --FIXME: "reserved identifier"
335334 let transf = if ascend then id else reverse
336335 (x, xs, fc) <- P.choice (transf (parserNoNS parser : parsersNS parser i))
337336 return (mkName (x, xs), fc)
@@ -400,7 +399,7 @@ invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%
400399
401400-- | Parses an operator
402401symbolicOperator :: MonadicParsing m => m String
403−symbolicOperator = do op <- P.token . some $ operatorLetter
402+symbolicOperator = do op <- Tok.token . some $ operatorLetter
404403 when (op `elem` (invalidOperators ++ commentMarkers)) $
405404 fail $ op ++ " is not a valid operator"
406405 return op
@@ -412,32 +411,17 @@ symbolicOperatorFC = do (FC f (l, c) _) <- getFC
412411 return (op, FC f (l, c) (l, c + length op))
413412
414413{- * Position helpers -}
415−{- | Get filename from position (returns "(interactive)" when no source file is given) -}
416−fileName :: P.Delta -> String
417−fileName (P.Directed fn _ _ _ _) = UTF8.toString fn
418−fileName _ = "(interactive)"
419−
420−{- | Get line number from position -}
421−lineNum :: P.Delta -> Int
422−lineNum (P.Lines l _ _ _) = fromIntegral l + 1
423−lineNum (P.Directed _ l _ _ _) = fromIntegral l + 1
424−lineNum _ = 0
425−
426−{- | Get column number from position -}
427−columnNum :: P.Delta -> Int
428−columnNum pos = fromIntegral (P.column pos) + 1
429−
430−
431414{- | Get file position as FC -}
432415getFC :: MonadicParsing m => m FC
433−getFC = do s <- P.position
434− let (dir, file) = splitFileName (fileName s)
435− let f = if dir == addTrailingPathSeparator "." then file else fileName s
436− return $ FC f (lineNum s, columnNum s) (lineNum s, columnNum s) -- TODO: Change to actual spanning
416+getFC = do pos <- P.getPosition
417+ let columnNumber = P.unPos . P.sourceColumn $ pos
418+ let lineNumber = P.unPos . P.sourceLine $ pos
419+ let (dir, file) = splitFileName (P.sourceName pos)
420+ let f = if dir == addTrailingPathSeparator "." then file else P.sourceName pos
421+ return $ FC f (lineNumber, columnNumber) (lineNumber, columnNumber) -- TODO: Change to actual spanning
437422 -- Issue #1594 on the Issue Tracker.
438423 -- https://github.com/idris-lang/Idris-dev/issues/1594
439424
440−
441425{-* Syntax helpers-}
442426-- | Bind constraints to term
443427bindList :: (RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm) -> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
@@ -447,15 +431,15 @@ bindList b ((r, n, fc, t):bs) sc = b r n fc t (bindList b bs sc)
447431{- | @commaSeparated p@ parses one or more occurences of `p`,
448432 separated by commas and optional whitespace. -}
449433commaSeparated :: MonadicParsing m => m a -> m [a]
450−commaSeparated p = p `P.sepBy1` (P.spaces >> P.char ',' >> P.spaces)
434+commaSeparated p = p `P.sepBy1` (P.space >> P.char ',' >> P.space)
451435
452436{- * Layout helpers -}
453437
454438-- | Push indentation to stack
455439pushIndent :: IdrisParser ()
456−pushIndent = do pos <- P.position
440+pushIndent = do columnNumber <- indent
457441 ist <- get
458− put (ist { indent_stack = (fromIntegral (P.column pos) + 1) : indent_stack ist })
442+ put (ist { indent_stack = columnNumber : indent_stack ist })
459443
460444-- | Pops indentation from stack
461445popIndent :: IdrisParser ()
@@ -466,8 +450,8 @@ popIndent = do ist <- get
466450
467451
468452-- | Gets current indentation
469−indent :: IdrisParser Int
470−indent = liftM ((+1) . fromIntegral . P.column) P.position
453+indent :: MonadicParsing m => m Int
454+indent = P.unPos . P.sourceColumn <$> P.getPosition
471455
472456-- | Gets last indentation
473457lastIndent :: IdrisParser Int
@@ -510,8 +494,7 @@ indentedBlockS p = do openBlock
510494
511495-- | Checks if the following character matches provided parser
512496lookAheadMatches :: MonadicParsing m => m a -> m Bool
513−lookAheadMatches p = do match <- lookAhead (optional p)
514− return $ isJust match
497+lookAheadMatches p = isJust <$> P.lookAhead (P.optional p)
515498
516499-- | Parses a start of block
517500openBlock :: IdrisParser ()
@@ -555,7 +538,7 @@ terminator = do lchar ';'; popIndent
555538 if c <= l then popIndent else fail "not a terminator"
556539 <|> do isParen <- lookAheadMatches (P.oneOf ")}")
557540 if isParen then popIndent else fail "not a terminator"
558− <|> lookAhead P.eof
541+ <|> P.lookAhead P.eof
559542
560543-- | Parses and keeps a terminator
561544keepTerminator :: IdrisParser ()
@@ -565,7 +548,7 @@ keepTerminator = () <$ lchar ';'
565548 <|> do isParen <- lookAheadMatches (P.oneOf ")}|")
566549 isIn <- lookAheadMatches (reserved "in")
567550 unless (isIn || isParen) $ fail "not a terminator"
568− <|> lookAhead P.eof
551+ <|> P.lookAhead P.eof
569552
570553-- | Checks if application expression does not end
571554notEndApp :: IdrisParser ()
@@ -577,7 +560,7 @@ notEndBlock :: IdrisParser ()
577560notEndBlock = do ist <- get
578561 case brace_stack ist of
579562 Just lvl : xs -> do i <- indent
580− isParen <- lookAheadMatches (char ')')
563+ isParen <- lookAheadMatches (P.char ')')
581564 when (i < lvl || isParen) (fail "end of block")
582565 _ -> return ()
583566