git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Parser/Helpers.hs
559 lines 20 kB history raw
1{-|
2Module : Idris.Parser.Helpers
3Description : Utilities for Idris' parser.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE ConstraintKinds, FlexibleContexts, MultiParamTypeClasses #-}
9module Idris.Parser.Helpers
10 ( module Idris.Parser.Stack
11 -- * The parser
12 , IdrisParser
13 , parseErrorDoc
14 -- * Space
15 , whiteSpace
16 , someSpace
17 , eol
18 , isEol
19 -- * Basic parsers
20 , char
21 , symbol
22 , string
23 , lookAheadMatches
24 -- * Terminals
25 , lchar
26 , reserved
27 , docComment
28 , token
29 , natural
30 , charLiteral
31 , stringLiteral
32 , float
33 -- * Names
34 , bindList
35 , maybeWithNS
36 , iName
37 , name
38 , identifier
39 , identifierWithExtraChars
40 , packageName
41 -- * Access
42 , accessibility
43 , accData
44 , addAcc
45 -- * Warnings and errors
46 , fixErrorMsg
47 , parserWarning
48 , clearParserWarnings
49 , reportParserWarnings
50 -- * Highlighting
51 , highlight
52 , keyword
53 -- * Indentation
54 , pushIndent
55 , popIndent
56 , indentGt
57 , notOpenBraces
58 -- * Indented blocks
59 , openBlock
60 , closeBlock
61 , terminator
62 , notEndBlock
63 , indentedBlock
64 , indentedBlock1
65 , indentedBlockS
66 , indented
67 -- * Miscellaneous
68 , notEndApp
69 , commaSeparated
70 )
71where
73import Idris.AbsSyntax
74import Idris.Core.Evaluate
75import Idris.Core.TT
76import Idris.Delaborate (pprintErr)
77import Idris.Docstrings
78import Idris.Options
79import Idris.Output (iWarn)
80import Idris.Parser.Stack
82import Prelude hiding (pi)
84import Control.Applicative
85import Control.Monad
86import Control.Monad.State.Strict
87import Data.Char
88import qualified Data.HashSet as HS
89import Data.List
90import qualified Data.List.NonEmpty as NonEmpty
91import qualified Data.Map as M
92import Data.Maybe
93import qualified Data.Set as S
94import qualified Data.Text as T
95import Text.Megaparsec ((<?>))
96import qualified Text.Megaparsec as P
97import qualified Text.Megaparsec.Char as P
98import qualified Text.Megaparsec.Char.Lexer as P hiding (space)
99import qualified Text.PrettyPrint.ANSI.Leijen as PP
102-- | Idris parser with state used during parsing
103type IdrisParser = Parser IState
105parseErrorDoc :: ParseError -> PP.Doc
106parseErrorDoc = PP.string . prettyError
108someSpace :: Parsing m => m ()
109someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
111token :: Parsing m => m a -> m a
112token p = trackExtent p <* whiteSpace
114highlight :: (MonadState IState m, Parsing m) => OutputAnnotation -> m a -> m a
115highlight annot p = do
116 (result, fc) <- withExtent p
117 modify $ \ist -> ist { idris_parserHighlights = S.insert (FC' fc, annot) (idris_parserHighlights ist) }
118 return result
120-- | Parse a reserved identfier, highlighting it as a keyword
121keyword :: (Parsing m, MonadState IState m) => String -> m ()
122keyword str = highlight AnnKeyword (reserved str)
124clearParserWarnings :: Idris ()
125clearParserWarnings = do ist <- getIState
126 putIState ist { parserWarnings = [] }
128reportParserWarnings :: Idris ()
129reportParserWarnings = do ist <- getIState
130 mapM_ (uncurry iWarn)
131 (map (\ (fc, err) -> (fc, pprintErr ist err)) .
132 reverse .
133 nubBy (\(fc, err) (fc', err') ->
134 FC' fc == FC' fc' && err == err') $
135 parserWarnings ist)
136 clearParserWarnings
139parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()
140parserWarning fc warnOpt warnErr = do
141 ist <- get
142 let cmdline = opt_cmdline (idris_options ist)
143 unless (maybe False (`elem` cmdline) warnOpt) $
144 put ist { parserWarnings = (fc, warnErr) : parserWarnings ist }
146{- * Space, comments and literals (token/lexing like parsers) -}
148-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)
149simpleWhiteSpace :: Parsing m => m ()
150simpleWhiteSpace = () <$ P.satisfy isSpace
152-- | Checks if a charcter is end of line
153isEol :: Char -> Bool
154isEol '\n' = True
155isEol _ = False
157-- | A parser that succeeds at the end of the line
158eol :: Parsing m => m ()
159eol = () <$ P.satisfy isEol <|> P.lookAhead P.eof <?> "end of line"
161{- | Consumes a single-line comment
164 SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;
166 -}
167singleLineComment :: Parsing m => m ()
168singleLineComment = P.hidden (() <$ string "--" *> many (P.satisfy (not . isEol)) *> eol)
170{- | Consumes a multi-line comment
173 MultiLineComment_t ::=
174 '{ -- }'
175 | '{ -' InCommentChars_t
176 ;
180 InCommentChars_t ::=
181 '- }'
182 | MultiLineComment_t InCommentChars_t
183 | ~'- }'+ InCommentChars_t
184 ;
186-}
187multiLineComment :: Parsing m => m ()
188multiLineComment = P.hidden $ P.try (string "{-" *> string "-}" *> pure ())
189 <|> string "{-" *> inCommentChars
190 where inCommentChars :: Parsing m => m ()
191 inCommentChars = string "-}" *> pure ()
192 <|> P.try (multiLineComment) *> inCommentChars
193 <|> string "|||" *> many (P.satisfy (not . isEol)) *> eol *> inCommentChars
194 <|> P.skipSome (P.noneOf startEnd) *> inCommentChars
195 <|> P.oneOf startEnd *> inCommentChars
196 <?> "end of comment"
197 startEnd :: String
198 startEnd = "{}-"
200{-| Parses a documentation comment
203 DocComment_t ::= DocCommentLine (ArgCommentLine DocCommentLine*)* ;
205 DocCommentLine ::= '|||' ~EOL_t* EOL_t ;
206 ArgCommentLine ::= '|||' '@' ~EOL_t* EOL_t ;
208 -}
209docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])
210docComment = do dc <- pushIndent *> docCommentLine
211 rest <- many (indented docCommentLine)
212 args <- many $ do (name, first) <- indented argDocCommentLine
213 rest <- many (indented docCommentLine)
214 return (name, concat (intersperse "\n" (first:rest)))
215 popIndent
216 return (parseDocstring $ T.pack (concat (intersperse "\n" (dc:rest))),
217 map (\(n, d) -> (n, parseDocstring (T.pack d))) args)
219 where docCommentLine :: Parsing m => m String
220 docCommentLine = P.hidden $ P.try $ do
221 string "|||"
222 many (P.satisfy (==' '))
223 contents <- P.option "" (do first <- P.satisfy (\c -> not (isEol c || c == '@'))
224 res <- many (P.satisfy (not . isEol))
225 return $ first:res)
226 eol ; someSpace
227 return contents
229 argDocCommentLine :: IdrisParser (Name, String)
230 argDocCommentLine = do P.string "|||"
231 P.many (P.satisfy isSpace)
232 P.char '@'
233 P.many (P.satisfy isSpace)
234 n <- name
235 P.many (P.satisfy isSpace)
236 docs <- P.many (P.satisfy (not . isEol))
237 P.eol ; someSpace
238 return (n, docs)
240-- | Parses some white space
241whiteSpace :: Parsing m => m ()
242whiteSpace = someSpace <|> pure ()
244-- | Parses a string literal
245stringLiteral :: Parsing m => m String
246stringLiteral = token . P.try $ P.char '"' *> P.manyTill P.charLiteral (P.char '"')
248-- | Parses a char literal
249charLiteral :: Parsing m => m Char
250charLiteral = token . P.try $ P.char '\'' *> P.charLiteral <* P.char '\''
252-- | Parses a natural number
253natural :: Parsing m => m Integer
254natural = token ( P.try (P.char '0' *> P.char' 'x' *> P.hexadecimal)
255 <|> P.try (P.char '0' *> P.char' 'o' *> P.octal)
256 <|> P.try P.decimal)
258-- | Parses a floating point number
259float :: Parsing m => m Double
260float = token . P.try $ P.float
262{- * Symbols, identifiers, names and operators -}
264reservedIdentifiers :: HS.HashSet String
265reservedIdentifiers = HS.fromList
266 [ "Type"
267 , "case", "class", "codata", "constructor", "corecord", "data"
268 , "do", "dsl", "else", "export", "if", "implementation", "implicit"
269 , "import", "impossible", "in", "infix", "infixl", "infixr", "instance"
270 , "interface", "let", "mutual", "namespace", "of", "parameters", "partial"
271 , "postulate", "private", "proof", "public", "quoteGoal", "record"
272 , "rewrite", "syntax", "then", "total", "using", "where", "with"
273 ]
275identifierOrReservedWithExtraChars :: Parsing m => String -> m String
276identifierOrReservedWithExtraChars extraChars = token $ P.try $ do
277 c <- P.satisfy isAlpha <|> P.oneOf "_"
278 cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf extraChars)
279 return $ c : cs
281char :: Parsing m => Char -> m Char
282char = P.char
284string :: Parsing m => String -> m String
285string = P.string
287-- | Parses a character as a token
288lchar :: Parsing m => Char -> m Char
289lchar = token . P.char
291symbol :: Parsing m => String -> m ()
292symbol = void . token . P.string
294-- | Parses a reserved identifier
295reserved :: Parsing m => String -> m ()
296reserved name = token $ P.try $ do
297 P.string name
298 P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name
300-- | Parses an identifier as a token
301identifierWithExtraChars :: Parsing m => String -> m String
302identifierWithExtraChars extraChars = P.try $ do
303 ident <- identifierOrReservedWithExtraChars extraChars
304 when (ident `HS.member` reservedIdentifiers) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved " ++ ident
305 when (ident == "_") $ P.unexpected . P.Label . NonEmpty.fromList $ "wildcard"
306 return ident
308identifier :: Parsing m => m String
309identifier = identifierWithExtraChars "_'."
311-- | Parses an identifier with possible namespace as a name
312iName :: Parsing m => [String] -> m Name
313iName bad = maybeWithNS identifier bad <?> "name"
315-- | Parses an string possibly prefixed by a namespace
316maybeWithNS :: Parsing m => m String -> [String] -> m Name
317maybeWithNS parser bad = do
318 i <- P.option "" (P.lookAhead identifier)
319 when (i `elem` bad) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved identifier"
320 mkName <$> P.choice (reverse (parserNoNS parser : parsersNS parser i))
321 where parserNoNS :: Parsing m => m String -> m (String, String)
322 parserNoNS = fmap (\x -> (x, ""))
323 parserNS :: Parsing m => m String -> String -> m (String, String)
324 parserNS parser ns = do xs <- trackExtent (string ns)
325 lchar '.'
326 x <- parser
327 return (x, xs)
328 parsersNS :: Parsing m => m String -> String -> [m (String, String)]
329 parsersNS parser i = [P.try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]
331-- | Parses a name
332name :: (Parsing m, MonadState IState m) => m Name
333name = do
334 keywords <- syntax_keywords <$> get
335 aliases <- module_aliases <$> get
336 n <- iName keywords
337 return (unalias aliases n)
338 <?> "name"
339 where
340 unalias :: M.Map [T.Text] [T.Text] -> Name -> Name
341 unalias aliases (NS n ns) | Just ns' <- M.lookup ns aliases = NS n ns'
342 unalias aliases name = name
344{- | List of all initial segments in ascending order of a list. Every
345such initial segment ends right before an element satisfying the given
346condition.
347-}
348initsEndAt :: (a -> Bool) -> [a] -> [[a]]
349initsEndAt p [] = []
350initsEndAt p (x:xs) | p x = [] : x_inits_xs
351 | otherwise = x_inits_xs
352 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
355{- | Create a `Name' from a pair of strings representing a base name and its
356 namespace.
357-}
358mkName :: (String, String) -> Name
359mkName (n, "") = sUN n
360mkName (n, ns) = sNS (sUN n) (reverse (parseNS ns))
361 where parseNS x = case span (/= '.') x of
362 (x, "") -> [x]
363 (x, '.':y) -> x : parseNS y
365-- | Parse a package name
366packageName :: Parsing m => m String
367packageName = (:) <$> P.oneOf firstChars <*> many (P.oneOf remChars)
368 where firstChars = ['a'..'z'] ++ ['A'..'Z']
369 remChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['-','_']
371{- * Position helpers -}
373{-* Syntax helpers-}
374-- | Bind constraints to term
375bindList :: (RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm) -> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
376bindList b [] sc = sc
377bindList b ((r, n, fc, t):bs) sc = b r n fc t (bindList b bs sc)
379{- | @commaSeparated p@ parses one or more occurences of `p`,
380 separated by commas and optional whitespace. -}
381commaSeparated :: Parsing m => m a -> m [a]
382commaSeparated p = p `P.sepBy1` (P.space >> P.char ',' >> P.space)
384{- * Layout helpers -}
386-- | Push indentation to stack
387pushIndent :: IdrisParser ()
388pushIndent = do columnNumber <- indent
389 ist <- get
390 put (ist { indent_stack = columnNumber : indent_stack ist })
392-- | Pops indentation from stack
393popIndent :: IdrisParser ()
394popIndent = do ist <- get
395 case indent_stack ist of
396 [] -> error "The impossible happened! Tried to pop an indentation level where none was pushed (underflow)."
397 (x : xs) -> put (ist { indent_stack = xs })
400-- | Gets current indentation
401indent :: Parsing m => m Int
402indent = P.unPos . P.sourceColumn <$> P.getSourcePos
404-- | Gets last indentation
405lastIndent :: (MonadState IState m) => m Int
406lastIndent = do ist <- get
407 case indent_stack ist of
408 (x : xs) -> return x
409 _ -> return 1
411-- | Applies parser in an indented position
412indented :: IdrisParser a -> IdrisParser a
413indented p = notEndBlock *> p <* keepTerminator
415-- | Applies parser to get a block (which has possibly indented statements)
416indentedBlock :: IdrisParser a -> IdrisParser [a]
417indentedBlock p = do openBlock
418 pushIndent
419 res <- many (indented p)
420 popIndent
421 closeBlock
422 return res
424-- | Applies parser to get a block with at least one statement (which has possibly indented statements)
425indentedBlock1 :: IdrisParser a -> IdrisParser [a]
426indentedBlock1 p = do openBlock
427 pushIndent
428 res <- some (indented p)
429 popIndent
430 closeBlock
431 return res
433-- | Applies parser to get a block with exactly one (possibly indented) statement
434indentedBlockS :: IdrisParser a -> IdrisParser a
435indentedBlockS p = do openBlock
436 pushIndent
437 res <- indented p
438 popIndent
439 closeBlock
440 return res
443-- | Checks if the following character matches provided parser
444lookAheadMatches :: Parsing m => m a -> m Bool
445lookAheadMatches p = isJust <$> P.lookAhead (P.optional p)
447-- | Parses a start of block
448openBlock :: IdrisParser ()
449openBlock = do lchar '{'
450 ist <- get
451 put (ist { brace_stack = Nothing : brace_stack ist })
452 <|> do ist <- get
453 lvl' <- indent
454 -- if we're not indented further, it's an empty block, so
455 -- increment lvl to ensure we get to the end
456 let lvl = case brace_stack ist of
457 Just lvl_old : _ ->
458 if lvl' <= lvl_old then lvl_old+1
459 else lvl'
460 [] -> if lvl' == 1 then 2 else lvl'
461 _ -> lvl'
462 put (ist { brace_stack = Just lvl : brace_stack ist })
463 <?> "start of block"
465-- | Parses an end of block
466closeBlock :: IdrisParser ()
467closeBlock = do ist <- get
468 bs <- case brace_stack ist of
469 [] -> [] <$ P.eof
470 Nothing : xs -> lchar '}' >> return xs <?> "end of block"
471 Just lvl : xs -> (do i <- indent
472 isParen <- lookAheadMatches (char ')')
473 isIn <- lookAheadMatches (reserved "in")
474 if i >= lvl && not (isParen || isIn)
475 then fail "not end of block"
476 else return xs)
477 <|> (do notOpenBraces
478 P.eof
479 return [])
480 put (ist { brace_stack = bs })
482-- | Parses a terminator
483terminator :: IdrisParser ()
484terminator = do lchar ';'; popIndent
485 <|> do c <- indent; l <- lastIndent
486 if c <= l then popIndent else fail "not a terminator"
487 <|> do isParen <- lookAheadMatches (P.oneOf ")}")
488 if isParen then popIndent else fail "not a terminator"
489 <|> P.lookAhead P.eof
491-- | Parses and keeps a terminator
492keepTerminator :: IdrisParser ()
493keepTerminator = () <$ lchar ';'
494 <|> do c <- indent; l <- lastIndent
495 unless (c <= l) $ fail "not a terminator"
496 <|> do isParen <- lookAheadMatches (P.oneOf ")}|")
497 isIn <- lookAheadMatches (reserved "in")
498 unless (isIn || isParen) $ fail "not a terminator"
499 <|> P.lookAhead P.eof
501-- | Checks if application expression does not end
502notEndApp :: IdrisParser ()
503notEndApp = do c <- indent; l <- lastIndent
504 when (c <= l) (fail "terminator")
506-- | Checks that it is not end of block
507notEndBlock :: IdrisParser ()
508notEndBlock = do ist <- get
509 case brace_stack ist of
510 Just lvl : xs -> do i <- indent
511 isParen <- lookAheadMatches (P.char ')')
512 when (i < lvl || isParen) (fail "end of block")
513 _ -> return ()
515indentGt :: (Parsing m, MonadState IState m) => m ()
516indentGt = do
517 li <- lastIndent
518 i <- indent
519 when (i <= li) $ fail "Wrong indention: should be greater than context indentation"
521-- | Checks that there are no braces that are not closed
522notOpenBraces :: IdrisParser ()
523notOpenBraces = do ist <- get
524 when (hasNothing $ brace_stack ist) $ fail "end of input"
525 where hasNothing :: [Maybe a] -> Bool
526 hasNothing = any isNothing
528{- | Parses an accessibilty modifier (e.g. public, private) -}
529accessibility' :: IdrisParser Accessibility
530accessibility' = Public <$ reserved "public" <* reserved "export"
531 <|> Frozen <$ reserved "export"
532 <|> Private <$ reserved "private"
533 <?> "accessibility modifier"
535accessibility :: IdrisParser Accessibility
536accessibility = do acc <- optional accessibility'
537 case acc of
538 Just a -> return a
539 Nothing -> do ist <- get
540 return (default_access ist)
542-- | Adds accessibility option for function
543addAcc :: Name -> Accessibility -> IdrisParser ()
544addAcc n a = do i <- get
545 put (i { hide_list = addDef n a (hide_list i) })
547{- | Add accessbility option for data declarations
548 (works for interfaces too - 'abstract' means the data/interface is visible but members not) -}
549accData :: Accessibility -> Name -> [Name] -> IdrisParser ()
550accData Frozen n ns = do addAcc n Public -- so that it can be used in public definitions
551 mapM_ (\n -> addAcc n Private) ns -- so that they are invisible
552accData a n ns = do addAcc n a
553 mapM_ (`addAcc` a) ns
556{- * Error reporting helpers -}
557{- | Error message with possible fixes list -}
558fixErrorMsg :: String -> [String] -> String
559fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)