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