module Idris.Parser.Helpers
( module Idris.Parser.Stack
, IdrisParser
, parseErrorDoc
, whiteSpace
, someSpace
, eol
, isEol
, char
, symbol
, string
, lookAheadMatches
, lchar
, reserved
, docComment
, token
, natural
, charLiteral
, stringLiteral
, float
, bindList
, maybeWithNS
, iName
, name
, identifier
, packageName
, accessibility
, accData
, addAcc
, fixErrorMsg
, parserWarning
, clearParserWarnings
, reportParserWarnings
, highlight
, keyword
, pushIndent
, popIndent
, indentGt
, notOpenBraces
, openBlock
, closeBlock
, terminator
, notEndBlock
, indentedBlock
, indentedBlock1
, indentedBlockS
, indented
, notEndApp
, commaSeparated
)
where
import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate (pprintErr)
import Idris.Docstrings
import Idris.Options
import Idris.Output (iWarn)
import Idris.Parser.Stack
import Prelude hiding (pi)
import Control.Applicative
import Control.Monad
import Control.Monad.State.Strict
import Data.Char
import qualified Data.HashSet as HS
import Data.List
import qualified Data.List.NonEmpty as NonEmpty
import qualified Data.Map as M
import Data.Maybe
import qualified Data.Text as T
import Text.Megaparsec ((<?>))
import qualified Text.Megaparsec as P
import qualified Text.Megaparsec.Char as P
import qualified Text.Megaparsec.Char.Lexer as P hiding (space)
import qualified Text.PrettyPrint.ANSI.Leijen as PP
type IdrisParser = Parser IState
parseErrorDoc :: ParseError -> PP.Doc
parseErrorDoc = PP.string . prettyError
someSpace :: Parsing m => m ()
someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
token :: Parsing m => m a -> m a
token p = trackExtent p <* whiteSpace
highlight :: (MonadState IState m, Parsing m) => OutputAnnotation -> m a -> m a
highlight annot p = do
(result, fc) <- withExtent p
modify $ \ist -> ist { idris_parserHighlights = (fc, annot) : idris_parserHighlights ist }
return result
keyword :: (Parsing m, MonadState IState m) => String -> m ()
keyword str = highlight AnnKeyword (reserved str)
clearParserWarnings :: Idris ()
clearParserWarnings = do ist <- getIState
putIState ist { parserWarnings = [] }
reportParserWarnings :: Idris ()
reportParserWarnings = do ist <- getIState
mapM_ (uncurry iWarn)
(map (\ (fc, err) -> (fc, pprintErr ist err)) .
reverse .
nubBy (\(fc, err) (fc', err') ->
FC' fc == FC' fc' && err == err') $
parserWarnings ist)
clearParserWarnings
parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()
parserWarning fc warnOpt warnErr = do
ist <- get
let cmdline = opt_cmdline (idris_options ist)
unless (maybe False (`elem` cmdline) warnOpt) $
put ist { parserWarnings = (fc, warnErr) : parserWarnings ist }
simpleWhiteSpace :: Parsing m => m ()
simpleWhiteSpace = () <$ P.satisfy isSpace
isEol :: Char -> Bool
isEol '\n' = True
isEol _ = False
eol :: Parsing m => m ()
eol = () <$ P.satisfy isEol <|> P.lookAhead P.eof <?> "end of line"
singleLineComment :: Parsing m => m ()
singleLineComment = P.hidden (() <$ string "--" *> many (P.satisfy (not . isEol)) *> eol)
multiLineComment :: Parsing m => m ()
multiLineComment = P.hidden $ P.try (string "{-" *> string "-}" *> pure ())
<|> string "{-" *> inCommentChars
where inCommentChars :: Parsing m => m ()
inCommentChars = string "-}" *> pure ()
<|> P.try (multiLineComment) *> inCommentChars
<|> string "|||" *> many (P.satisfy (not . isEol)) *> eol *> inCommentChars
<|> P.skipSome (P.noneOf startEnd) *> inCommentChars
<|> P.oneOf startEnd *> inCommentChars
<?> "end of comment"
startEnd :: String
startEnd = "{}-"
docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])
docComment = do dc <- pushIndent *> docCommentLine
rest <- many (indented docCommentLine)
args <- many $ do (name, first) <- indented argDocCommentLine
rest <- many (indented docCommentLine)
return (name, concat (intersperse "\n" (first:rest)))
popIndent
return (parseDocstring $ T.pack (concat (intersperse "\n" (dc:rest))),
map (\(n, d) -> (n, parseDocstring (T.pack d))) args)
where docCommentLine :: Parsing m => m String
docCommentLine = P.hidden $ P.try $ do
string "|||"
many (P.satisfy (==' '))
contents <- P.option "" (do first <- P.satisfy (\c -> not (isEol c || c == '@'))
res <- many (P.satisfy (not . isEol))
return $ first:res)
eol ; someSpace
return contents
argDocCommentLine :: IdrisParser (Name, String)
argDocCommentLine = do P.string "|||"
P.many (P.satisfy isSpace)
P.char '@'
P.many (P.satisfy isSpace)
n <- name
P.many (P.satisfy isSpace)
docs <- P.many (P.satisfy (not . isEol))
P.eol ; someSpace
return (n, docs)
whiteSpace :: Parsing m => m ()
whiteSpace = someSpace <|> pure ()
stringLiteral :: Parsing m => m String
stringLiteral = token . P.try $ P.char '"' *> P.manyTill P.charLiteral (P.char '"')
charLiteral :: Parsing m => m Char
charLiteral = token . P.try $ P.char '\'' *> P.charLiteral <* P.char '\''
natural :: Parsing m => m Integer
natural = token ( P.try (P.char '0' *> P.char' 'x' *> P.hexadecimal)
<|> P.try (P.char '0' *> P.char' 'o' *> P.octal)
<|> P.try P.decimal)
float :: Parsing m => m Double
float = token . P.try $ P.float
reservedIdentifiers :: HS.HashSet String
reservedIdentifiers = HS.fromList
[ "Type"
, "case", "class", "codata", "constructor", "corecord", "data"
, "do", "dsl", "else", "export", "if", "implementation", "implicit"
, "import", "impossible", "in", "infix", "infixl", "infixr", "instance"
, "interface", "let", "mutual", "namespace", "of", "parameters", "partial"
, "postulate", "private", "proof", "public", "quoteGoal", "record"
, "rewrite", "syntax", "then", "total", "using", "where", "with"
]
identifierOrReserved :: Parsing m => m String
identifierOrReserved = token $ P.try $ do
c <- P.satisfy isAlpha <|> P.oneOf "_"
cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf "_'.")
return $ c : cs
char :: Parsing m => Char -> m Char
char = P.char
string :: Parsing m => String -> m String
string = P.string
lchar :: Parsing m => Char -> m Char
lchar = token . P.char
symbol :: Parsing m => String -> m ()
symbol = void . token . P.string
reserved :: Parsing m => String -> m ()
reserved name = token $ P.try $ do
P.string name
P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name
identifier :: Parsing m => m String
identifier = P.try $ do
ident <- identifierOrReserved
when (ident `HS.member` reservedIdentifiers) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved " ++ ident
when (ident == "_") $ P.unexpected . P.Label . NonEmpty.fromList $ "wildcard"
return ident
iName :: Parsing m => [String] -> m Name
iName bad = maybeWithNS identifier bad <?> "name"
maybeWithNS :: Parsing m => m String -> [String] -> m Name
maybeWithNS parser bad = do
i <- P.option "" (P.lookAhead identifier)
when (i `elem` bad) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved identifier"
mkName <$> P.choice (reverse (parserNoNS parser : parsersNS parser i))
where parserNoNS :: Parsing m => m String -> m (String, String)
parserNoNS = fmap (\x -> (x, ""))
parserNS :: Parsing m => m String -> String -> m (String, String)
parserNS parser ns = do xs <- trackExtent (string ns)
lchar '.'
x <- parser
return (x, xs)
parsersNS :: Parsing m => m String -> String -> [m (String, String)]
parsersNS parser i = [P.try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]
name :: (Parsing m, MonadState IState m) => m Name
name = do
keywords <- syntax_keywords <$> get
aliases <- module_aliases <$> get
n <- iName keywords
return (unalias aliases n)
<?> "name"
where
unalias :: M.Map [T.Text] [T.Text] -> Name -> Name
unalias aliases (NS n ns) | Just ns' <- M.lookup ns aliases = NS n ns'
unalias aliases name = name
initsEndAt :: (a -> Bool) -> [a] -> [[a]]
initsEndAt p [] = []
initsEndAt p (x:xs) | p x = [] : x_inits_xs
| otherwise = x_inits_xs
where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
mkName :: (String, String) -> Name
mkName (n, "") = sUN n
mkName (n, ns) = sNS (sUN n) (reverse (parseNS ns))
where parseNS x = case span (/= '.') x of
(x, "") -> [x]
(x, '.':y) -> x : parseNS y
packageName :: Parsing m => m String
packageName = (:) <$> P.oneOf firstChars <*> many (P.oneOf remChars)
where firstChars = ['a'..'z'] ++ ['A'..'Z']
remChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['-','_']
bindList :: (RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm) -> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList b [] sc = sc
bindList b ((r, n, fc, t):bs) sc = b r n fc t (bindList b bs sc)
commaSeparated :: Parsing m => m a -> m [a]
commaSeparated p = p `P.sepBy1` (P.space >> P.char ',' >> P.space)
pushIndent :: IdrisParser ()
pushIndent = do columnNumber <- indent
ist <- get
put (ist { indent_stack = columnNumber : indent_stack ist })
popIndent :: IdrisParser ()
popIndent = do ist <- get
case indent_stack ist of
[] -> error "The impossible happened! Tried to pop an indentation level where none was pushed (underflow)."
(x : xs) -> put (ist { indent_stack = xs })
indent :: Parsing m => m Int
indent = P.unPos . P.sourceColumn <$> P.getPosition
lastIndent :: (MonadState IState m) => m Int
lastIndent = do ist <- get
case indent_stack ist of
(x : xs) -> return x
_ -> return 1
indented :: IdrisParser a -> IdrisParser a
indented p = notEndBlock *> p <* keepTerminator
indentedBlock :: IdrisParser a -> IdrisParser [a]
indentedBlock p = do openBlock
pushIndent
res <- many (indented p)
popIndent
closeBlock
return res
indentedBlock1 :: IdrisParser a -> IdrisParser [a]
indentedBlock1 p = do openBlock
pushIndent
res <- some (indented p)
popIndent
closeBlock
return res
indentedBlockS :: IdrisParser a -> IdrisParser a
indentedBlockS p = do openBlock
pushIndent
res <- indented p
popIndent
closeBlock
return res
lookAheadMatches :: Parsing m => m a -> m Bool
lookAheadMatches p = isJust <$> P.lookAhead (P.optional p)
openBlock :: IdrisParser ()
openBlock = do lchar '{'
ist <- get
put (ist { brace_stack = Nothing : brace_stack ist })
<|> do ist <- get
lvl' <- indent
let lvl = case brace_stack ist of
Just lvl_old : _ ->
if lvl' <= lvl_old then lvl_old+1
else lvl'
[] -> if lvl' == 1 then 2 else lvl'
_ -> lvl'
put (ist { brace_stack = Just lvl : brace_stack ist })
<?> "start of block"
closeBlock :: IdrisParser ()
closeBlock = do ist <- get
bs <- case brace_stack ist of
[] -> [] <$ P.eof
Nothing : xs -> lchar '}' >> return xs <?> "end of block"
Just lvl : xs -> (do i <- indent
isParen <- lookAheadMatches (char ')')
isIn <- lookAheadMatches (reserved "in")
if i >= lvl && not (isParen || isIn)
then fail "not end of block"
else return xs)
<|> (do notOpenBraces
P.eof
return [])
put (ist { brace_stack = bs })
terminator :: IdrisParser ()
terminator = do lchar ';'; popIndent
<|> do c <- indent; l <- lastIndent
if c <= l then popIndent else fail "not a terminator"
<|> do isParen <- lookAheadMatches (P.oneOf ")}")
if isParen then popIndent else fail "not a terminator"
<|> P.lookAhead P.eof
keepTerminator :: IdrisParser ()
keepTerminator = () <$ lchar ';'
<|> do c <- indent; l <- lastIndent
unless (c <= l) $ fail "not a terminator"
<|> do isParen <- lookAheadMatches (P.oneOf ")}|")
isIn <- lookAheadMatches (reserved "in")
unless (isIn || isParen) $ fail "not a terminator"
<|> P.lookAhead P.eof
notEndApp :: IdrisParser ()
notEndApp = do c <- indent; l <- lastIndent
when (c <= l) (fail "terminator")
notEndBlock :: IdrisParser ()
notEndBlock = do ist <- get
case brace_stack ist of
Just lvl : xs -> do i <- indent
isParen <- lookAheadMatches (P.char ')')
when (i < lvl || isParen) (fail "end of block")
_ -> return ()
indentGt :: (Parsing m, MonadState IState m) => m ()
indentGt = do
li <- lastIndent
i <- indent
when (i <= li) $ fail "Wrong indention: should be greater than context indentation"
notOpenBraces :: IdrisParser ()
notOpenBraces = do ist <- get
when (hasNothing $ brace_stack ist) $ fail "end of input"
where hasNothing :: [Maybe a] -> Bool
hasNothing = any isNothing
accessibility' :: IdrisParser Accessibility
accessibility' = Public <$ reserved "public" <* reserved "export"
<|> Frozen <$ reserved "export"
<|> Private <$ reserved "private"
<?> "accessibility modifier"
accessibility :: IdrisParser Accessibility
accessibility = do acc <- optional accessibility'
case acc of
Just a -> return a
Nothing -> do ist <- get
return (default_access ist)
addAcc :: Name -> Accessibility -> IdrisParser ()
addAcc n a = do i <- get
put (i { hide_list = addDef n a (hide_list i) })
accData :: Accessibility -> Name -> [Name] -> IdrisParser ()
accData Frozen n ns = do addAcc n Public
mapM_ (\n -> addAcc n Private) ns
accData a n ns = do addAcc n a
mapM_ (`addAcc` a) ns
fixErrorMsg :: String -> [String] -> String
fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)