{-# 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 (String -> Doc) -> (ParseError -> String) -> ParseError -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> String
prettyError
someSpace :: Parsing m => m ()
someSpace :: forall (m :: * -> *). Parsing m => m ()
someSpace = m () -> m [()]
forall a. m a -> m [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (m ()
forall (m :: * -> *). Parsing m => m ()
simpleWhiteSpace m () -> m () -> m ()
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m ()
forall (m :: * -> *). Parsing m => m ()
singleLineComment m () -> m () -> m ()
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m ()
forall (m :: * -> *). Parsing m => m ()
multiLineComment) m [()] -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> m ()
forall a. a -> m a
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 = m a -> m a
forall (m :: * -> *) a. Parsing m => m a -> m a
trackExtent m a
p m a -> m () -> m a
forall a b. m a -> m b -> m a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* m ()
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) <- m a -> m (a, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent m a
p
(IState -> IState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((IState -> IState) -> m ()) -> (IState -> IState) -> m ()
forall a b. (a -> b) -> a -> b
$ \IState
ist -> IState
ist { idris_parserHighlights = S.insert (FC' fc, annot) (idris_parserHighlights ist) }
a -> m a
forall a. a -> m a
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 = OutputAnnotation -> m () -> m ()
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (String -> m ()
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 = [] }
reportParserWarnings :: Idris ()
reportParserWarnings :: Idris ()
reportParserWarnings = do IState
ist <- Idris IState
getIState
((FC, OutputDoc) -> Idris ()) -> [(FC, OutputDoc)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((FC -> OutputDoc -> Idris ()) -> (FC, OutputDoc) -> Idris ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry FC -> OutputDoc -> Idris ()
iWarn)
(((FC, Err) -> (FC, OutputDoc)) -> [(FC, Err)] -> [(FC, OutputDoc)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (FC
fc, Err
err) -> (FC
fc, IState -> Err -> OutputDoc
pprintErr IState
ist Err
err)) ([(FC, Err)] -> [(FC, OutputDoc)])
-> ([(FC, Err)] -> [(FC, Err)]) -> [(FC, Err)] -> [(FC, OutputDoc)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
[(FC, Err)] -> [(FC, Err)]
forall a. [a] -> [a]
reverse ([(FC, Err)] -> [(FC, Err)])
-> ([(FC, Err)] -> [(FC, Err)]) -> [(FC, Err)] -> [(FC, Err)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
((FC, Err) -> (FC, Err) -> Bool) -> [(FC, Err)] -> [(FC, Err)]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (\(FC
fc, Err
err) (FC
fc', Err
err') ->
FC -> FC'
FC' FC
fc FC' -> FC' -> Bool
forall a. Eq a => a -> a -> Bool
== FC -> FC'
FC' FC
fc' Bool -> Bool -> Bool
&& Err
err Err -> Err -> Bool
forall a. Eq a => a -> a -> Bool
== Err
err') ([(FC, Err)] -> [(FC, OutputDoc)])
-> [(FC, Err)] -> [(FC, OutputDoc)]
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 <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
let cmdline :: [Opt]
cmdline = IOption -> [Opt]
opt_cmdline (IState -> IOption
idris_options IState
ist)
Bool -> IdrisParser () -> IdrisParser ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool -> (Opt -> Bool) -> Maybe Opt -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
cmdline) Maybe Opt
warnOpt) (IdrisParser () -> IdrisParser ())
-> IdrisParser () -> IdrisParser ()
forall a b. (a -> b) -> a -> b
$
IState -> IdrisParser ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put IState
ist { parserWarnings = (fc, warnErr) : parserWarnings ist }
simpleWhiteSpace :: Parsing m => m ()
simpleWhiteSpace :: forall (m :: * -> *). Parsing m => m ()
simpleWhiteSpace = () () -> m (Token String) -> m ()
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (Token String -> Bool) -> m (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
Token String -> 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 = () () -> m (Token String) -> m ()
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (Token String -> Bool) -> m (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
Token String -> Bool
isEol m () -> m () -> m ()
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m () -> m ()
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.lookAhead m ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof m () -> String -> m ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"end of line"
singleLineComment :: Parsing m => m ()
= m () -> m ()
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.hidden (() () -> m String -> m ()
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m String
forall (m :: * -> *). Parsing m => String -> m String
string String
"--" m () -> m [Token String] -> m [Token String]
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m (Token String) -> m [Token String]
forall a. m a -> m [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ((Token String -> Bool) -> m (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isEol)) m [Token String] -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m ()
forall (m :: * -> *). Parsing m => m ()
eol)
multiLineComment :: Parsing m => m ()
= m () -> m ()
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.hidden (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ m () -> m ()
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (String -> m String
forall (m :: * -> *). Parsing m => String -> m String
string String
"{-" m String -> m String -> m String
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> m String
forall (m :: * -> *). Parsing m => String -> m String
string String
"-}" m String -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
m () -> m () -> m ()
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> m String
forall (m :: * -> *). Parsing m => String -> m String
string String
"{-" m String -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m ()
forall (m :: * -> *). Parsing m => m ()
inCommentChars
where inCommentChars :: Parsing m => m ()
inCommentChars :: forall (m :: * -> *). Parsing m => m ()
inCommentChars = String -> m String
forall (m :: * -> *). Parsing m => String -> m String
string String
"-}" m String -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
m () -> m () -> m ()
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m () -> m ()
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m ()
forall (m :: * -> *). Parsing m => m ()
multiLineComment) m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m ()
forall (m :: * -> *). Parsing m => m ()
inCommentChars
m () -> m () -> m ()
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> m String
forall (m :: * -> *). Parsing m => String -> m String
string String
"|||" m String -> m [Token String] -> m [Token String]
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m (Token String) -> m [Token String]
forall a. m a -> m [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ((Token String -> Bool) -> m (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isEol)) m [Token String] -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m ()
forall (m :: * -> *). Parsing m => m ()
eol m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m ()
forall (m :: * -> *). Parsing m => m ()
inCommentChars
m () -> m () -> m ()
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m (Token String) -> m ()
forall (m :: * -> *) a. MonadPlus m => m a -> m ()
P.skipSome ([Token String] -> m (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.noneOf String
[Token String]
startEnd) m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m ()
forall (m :: * -> *). Parsing m => m ()
inCommentChars
m () -> m () -> m ()
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token String] -> m (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
[Token String]
startEnd m (Token String) -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m ()
forall (m :: * -> *). Parsing m => m ()
inCommentChars
m () -> String -> m ()
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 IdrisParser ()
-> StateT IState (WriterT FC (Parsec Void String)) String
-> StateT IState (WriterT FC (Parsec Void String)) String
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *). Parsing m => m String
docCommentLine
[String]
rest <- StateT IState (WriterT FC (Parsec Void String)) String
-> StateT IState (WriterT FC (Parsec Void String)) [String]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (StateT IState (WriterT FC (Parsec Void String)) String
-> StateT IState (WriterT FC (Parsec Void String)) String
forall a. IdrisParser a -> IdrisParser a
indented StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *). Parsing m => m String
docCommentLine)
[(Name, String)]
args <- StateT IState (WriterT FC (Parsec Void String)) (Name, String)
-> StateT IState (WriterT FC (Parsec Void String)) [(Name, String)]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (StateT IState (WriterT FC (Parsec Void String)) (Name, String)
-> StateT
IState (WriterT FC (Parsec Void String)) [(Name, String)])
-> StateT IState (WriterT FC (Parsec Void String)) (Name, String)
-> StateT IState (WriterT FC (Parsec Void String)) [(Name, String)]
forall a b. (a -> b) -> a -> b
$ do (Name
name, String
first) <- StateT IState (WriterT FC (Parsec Void String)) (Name, String)
-> StateT IState (WriterT FC (Parsec Void String)) (Name, String)
forall a. IdrisParser a -> IdrisParser a
indented StateT IState (WriterT FC (Parsec Void String)) (Name, String)
argDocCommentLine
[String]
rest <- StateT IState (WriterT FC (Parsec Void String)) String
-> StateT IState (WriterT FC (Parsec Void String)) [String]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (StateT IState (WriterT FC (Parsec Void String)) String
-> StateT IState (WriterT FC (Parsec Void String)) String
forall a. IdrisParser a -> IdrisParser a
indented StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *). Parsing m => m String
docCommentLine)
(Name, String)
-> StateT IState (WriterT FC (Parsec Void String)) (Name, String)
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
name, [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
"\n" (String
firstString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
rest)))
IdrisParser ()
popIndent
(Docstring (), [(Name, Docstring ())])
-> IdrisParser (Docstring (), [(Name, Docstring ())])
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> Docstring ()
parseDocstring (Text -> Docstring ()) -> Text -> Docstring ()
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
"\n" (String
dcString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
rest))),
((Name, String) -> (Name, Docstring ()))
-> [(Name, String)] -> [(Name, Docstring ())]
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 = m String -> m String
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.hidden (m String -> m String) -> m String -> m String
forall a b. (a -> b) -> a -> b
$ m String -> m String
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m String -> m String) -> m String -> m String
forall a b. (a -> b) -> a -> b
$ do
String -> m String
forall (m :: * -> *). Parsing m => String -> m String
string String
"|||"
m (Token String) -> m [Token String]
forall a. m a -> m [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ((Token String -> Bool) -> m (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy (Token String -> Token String -> Bool
forall a. Eq a => a -> a -> Bool
==Char
Token String
' '))
String
contents <- String -> m String -> m String
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option String
"" (do Char
first <- (Token String -> Bool) -> m (Token String)
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 Char
Token String
c Bool -> Bool -> Bool
|| Char
Token String
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'@'))
String
res <- m Char -> m String
forall a. m a -> m [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ((Token String -> Bool) -> m (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isEol))
String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ Char
firstChar -> String -> String
forall a. a -> [a] -> [a]
:String
res)
m ()
forall (m :: * -> *). Parsing m => m ()
eol ; m ()
forall (m :: * -> *). Parsing m => m ()
someSpace
String -> m String
forall a. a -> m a
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 Tokens String
-> StateT IState (WriterT FC (Parsec Void String)) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
P.string String
Tokens String
"|||"
StateT IState (WriterT FC (Parsec Void String)) (Token String)
-> StateT IState (WriterT FC (Parsec Void String)) [Token String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many ((Token String -> Bool)
-> StateT IState (WriterT FC (Parsec Void String)) (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
Token String -> Bool
isSpace)
Token String
-> StateT IState (WriterT FC (Parsec Void String)) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
Token String
'@'
StateT IState (WriterT FC (Parsec Void String)) (Token String)
-> StateT IState (WriterT FC (Parsec Void String)) [Token String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many ((Token String -> Bool)
-> StateT IState (WriterT FC (Parsec Void String)) (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
Token String -> Bool
isSpace)
Name
n <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
StateT IState (WriterT FC (Parsec Void String)) (Token String)
-> StateT IState (WriterT FC (Parsec Void String)) [Token String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many ((Token String -> Bool)
-> StateT IState (WriterT FC (Parsec Void String)) (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
Token String -> Bool
isSpace)
String
docs <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many ((Token String -> Bool)
-> StateT IState (WriterT FC (Parsec Void String)) (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isEol))
StateT IState (WriterT FC (Parsec Void String)) (Tokens String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Tokens s)
P.eol ; IdrisParser ()
forall (m :: * -> *). Parsing m => m ()
someSpace
(Name, String)
-> StateT IState (WriterT FC (Parsec Void String)) (Name, String)
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, String
docs)
whiteSpace :: Parsing m => m ()
whiteSpace :: forall (m :: * -> *). Parsing m => m ()
whiteSpace = m ()
forall (m :: * -> *). Parsing m => m ()
someSpace m () -> m () -> m ()
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
stringLiteral :: Parsing m => m String
stringLiteral :: forall (m :: * -> *). Parsing m => m String
stringLiteral = m String -> m String
forall (m :: * -> *) a. Parsing m => m a -> m a
token (m String -> m String)
-> (m String -> m String) -> m String -> m String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m String -> m String
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m String -> m String) -> m String -> m String
forall a b. (a -> b) -> a -> b
$ Token String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
Token String
'"' m Char -> m String -> m String
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m Char -> m Char -> m String
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
P.manyTill m Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
P.charLiteral (Token String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
Token String
'"')
charLiteral :: Parsing m => m Char
charLiteral :: forall (m :: * -> *). Parsing m => m Char
charLiteral = m Char -> m Char
forall (m :: * -> *) a. Parsing m => m a -> m a
token (m Char -> m Char) -> (m Char -> m Char) -> m Char -> m Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Char -> m Char
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m Char -> m Char) -> m Char -> m Char
forall a b. (a -> b) -> a -> b
$ Token String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
Token String
'\'' m Char -> m Char -> m Char
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
P.charLiteral m Char -> m Char -> m Char
forall a b. m a -> m b -> m a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Token String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
Token String
'\''
natural :: Parsing m => m Integer
natural :: forall (m :: * -> *). Parsing m => m Integer
natural = m Integer -> m Integer
forall (m :: * -> *) a. Parsing m => m a -> m a
token ( m Integer -> m Integer
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Token String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
Token String
'0' m Char -> m Char -> m Char
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Token String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char' Char
Token String
'x' m Char -> m Integer -> m Integer
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m Integer
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
P.hexadecimal)
m Integer -> m Integer -> m Integer
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m Integer -> m Integer
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Token String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
Token String
'0' m Char -> m Char -> m Char
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Token String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char' Char
Token String
'o' m Char -> m Integer -> m Integer
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m Integer
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
P.octal)
m Integer -> m Integer -> m Integer
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m Integer -> m Integer
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try m Integer
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 = m Double -> m Double
forall (m :: * -> *) a. Parsing m => m a -> m a
token (m Double -> m Double)
-> (m Double -> m Double) -> m Double -> m Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Double -> m Double
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m Double -> m Double) -> m Double -> m Double
forall a b. (a -> b) -> a -> b
$ m Double
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 = [String] -> HashSet String
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 = m String -> m String
forall (m :: * -> *) a. Parsing m => m a -> m a
token (m String -> m String) -> m String -> m String
forall a b. (a -> b) -> a -> b
$ m String -> m String
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m String -> m String) -> m String -> m String
forall a b. (a -> b) -> a -> b
$ do
Char
c <- (Token String -> Bool) -> m (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
Token String -> Bool
isAlpha m Char -> m Char -> m Char
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token String] -> m (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
[Token String]
"_"
String
cs <- m Char -> m String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many ((Token String -> Bool) -> m (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
Token String -> Bool
isAlphaNum m Char -> m Char -> m Char
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token String] -> m (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
[Token String]
extraChars)
String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String
cs
char :: Parsing m => Char -> m Char
char :: forall (m :: * -> *). Parsing m => Char -> m Char
char = Char -> m Char
Token String -> m (Token String)
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 = String -> m String
Tokens String -> m (Tokens 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 = m Char -> m Char
forall (m :: * -> *) a. Parsing m => m a -> m a
token (m Char -> m Char) -> (Char -> m Char) -> Char -> m Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> m Char
Token String -> m (Token String)
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 = m String -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m String -> m ()) -> (String -> m String) -> String -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m String -> m String
forall (m :: * -> *) a. Parsing m => m a -> m a
token (m String -> m String)
-> (String -> m String) -> String -> m String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m String
Tokens String -> m (Tokens String)
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 = m () -> m ()
forall (m :: * -> *) a. Parsing m => m a -> m a
token (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ m () -> m ()
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
Tokens String -> m (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
P.string String
Tokens String
name
m (Token String) -> m ()
forall a. m a -> m ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
P.notFollowedBy ((Token String -> Bool) -> m (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
Token String -> Bool
isAlphaNum m (Token String) -> m (Token String) -> m (Token String)
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token String] -> m (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
[Token String]
"_'.") m () -> String -> m ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"end of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name
identifierWithExtraChars :: Parsing m => String -> m String
String
extraChars = m String -> m String
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m String -> m String) -> m String -> m String
forall a b. (a -> b) -> a -> b
$ do
String
ident <- String -> m String
forall (m :: * -> *). Parsing m => String -> m String
identifierOrReservedWithExtraChars String
extraChars
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
ident String -> HashSet String -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HS.member` HashSet String
reservedIdentifiers) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ ErrorItem (Token String) -> m ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected (ErrorItem (Token String) -> m ())
-> (String -> ErrorItem (Token String)) -> String -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Char -> ErrorItem (Token String)
forall t. NonEmpty Char -> ErrorItem t
P.Label (NonEmpty Char -> ErrorItem (Token String))
-> (String -> NonEmpty Char) -> String -> ErrorItem (Token String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> NonEmpty Char
forall a. HasCallStack => [a] -> NonEmpty a
NonEmpty.fromList (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"reserved " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ident
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
ident String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"_") (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ ErrorItem (Token String) -> m ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected (ErrorItem (Token String) -> m ())
-> (String -> ErrorItem (Token String)) -> String -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Char -> ErrorItem (Token String)
forall t. NonEmpty Char -> ErrorItem t
P.Label (NonEmpty Char -> ErrorItem (Token String))
-> (String -> NonEmpty Char) -> String -> ErrorItem (Token String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> NonEmpty Char
forall a. HasCallStack => [a] -> NonEmpty a
NonEmpty.fromList (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"wildcard"
String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
ident
identifier :: Parsing m => m String
identifier :: forall (m :: * -> *). Parsing m => m String
identifier = String -> m String
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 = m String -> [String] -> m Name
forall (m :: * -> *). Parsing m => m String -> [String] -> m Name
maybeWithNS m String
forall (m :: * -> *). Parsing m => m String
identifier [String]
bad m Name -> String -> m Name
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 <- String -> m String -> m String
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option String
"" (m String -> m String
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.lookAhead m String
forall (m :: * -> *). Parsing m => m String
identifier)
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
i String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
bad) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ ErrorItem (Token String) -> m ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected (ErrorItem (Token String) -> m ())
-> (String -> ErrorItem (Token String)) -> String -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Char -> ErrorItem (Token String)
forall t. NonEmpty Char -> ErrorItem t
P.Label (NonEmpty Char -> ErrorItem (Token String))
-> (String -> NonEmpty Char) -> String -> ErrorItem (Token String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> NonEmpty Char
forall a. HasCallStack => [a] -> NonEmpty a
NonEmpty.fromList (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"reserved identifier"
(String, String) -> Name
mkName ((String, String) -> Name) -> m (String, String) -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m (String, String)] -> m (String, String)
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice ([m (String, String)] -> [m (String, String)]
forall a. [a] -> [a]
reverse (m String -> m (String, String)
forall (m :: * -> *). Parsing m => m String -> m (String, String)
parserNoNS m String
parser m (String, String) -> [m (String, String)] -> [m (String, String)]
forall a. a -> [a] -> [a]
: m String -> String -> [m (String, String)]
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 = (String -> (String, String)) -> m String -> m (String, String)
forall a b. (a -> b) -> m a -> m b
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 <- m String -> m String
forall (m :: * -> *) a. Parsing m => m a -> m a
trackExtent (String -> m String
forall (m :: * -> *). Parsing m => String -> m String
string String
ns)
Char -> m Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'.'
String
x <- m String
parser
(String, String) -> m (String, String)
forall a. a -> m a
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 = [m (String, String) -> m (String, String)
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m String -> String -> m (String, String)
forall (m :: * -> *).
Parsing m =>
m String -> String -> m (String, String)
parserNS m String
parser String
ns) | String
ns <- ((Char -> Bool) -> String -> [String]
forall a. (a -> Bool) -> [a] -> [[a]]
initsEndAt (Char -> Char -> Bool
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 (IState -> [String]) -> m IState -> m [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m IState
forall s (m :: * -> *). MonadState s m => m s
get
Map [Text] [Text]
aliases <- IState -> Map [Text] [Text]
module_aliases (IState -> Map [Text] [Text]) -> m IState -> m (Map [Text] [Text])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m IState
forall s (m :: * -> *). MonadState s m => m s
get
Name
n <- [String] -> m Name
forall (m :: * -> *). Parsing m => [String] -> m Name
iName [String]
keywords
Name -> m Name
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map [Text] [Text] -> Name -> Name
unalias Map [Text] [Text]
aliases Name
n)
m Name -> String -> m Name
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' <- [Text] -> Map [Text] [Text] -> Maybe [Text]
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 = [] [a] -> [[a]] -> [[a]]
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 a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
cs | [a]
cs <- (a -> Bool) -> [a] -> [[a]]
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) ([String] -> [String]
forall a. [a] -> [a]
reverse (String -> [String]
parseNS String
ns))
where parseNS :: String -> [String]
parseNS String
x = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'.') String
x of
(String
x, String
"") -> [String
x]
(String
x, Char
'.':String
y) -> String
x String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> [String]
parseNS String
y
packageName :: Parsing m => m String
packageName :: forall (m :: * -> *). Parsing m => m String
packageName = (:) (Char -> String -> String) -> m Char -> m (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Token String] -> m (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
[Token String]
firstChars m (String -> String) -> m String -> m String
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m Char -> m String
forall a. m a -> m [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ([Token String] -> m (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
[Token String]
remChars)
where firstChars :: String
firstChars = [Char
'a'..Char
'z'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
'A'..Char
'Z']
remChars :: String
remChars = [Char
'a'..Char
'z'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
'A'..Char
'Z'] String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
'0'..Char
'9'] String -> String -> String
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 m a -> m () -> m [a]
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
`P.sepBy1` (m ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
P.space m () -> m Char -> m Char
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Token String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
Token String
',' m Char -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
P.space)
pushIndent :: IdrisParser ()
pushIndent :: IdrisParser ()
pushIndent = do Int
columnNumber <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). Parsing m => m Int
indent
IState
ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
IState -> IdrisParser ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
ist { indent_stack = columnNumber : indent_stack ist })
popIndent :: IdrisParser ()
popIndent :: IdrisParser ()
popIndent = do IState
ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
case IState -> [Int]
indent_stack IState
ist of
[] -> String -> IdrisParser ()
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) -> IState -> IdrisParser ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
ist { indent_stack = xs })
indent :: Parsing m => m Int
indent :: forall (m :: * -> *). Parsing m => m Int
indent = Pos -> Int
P.unPos (Pos -> Int) -> (SourcePos -> Pos) -> SourcePos -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> Pos
P.sourceColumn (SourcePos -> Int) -> m SourcePos -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SourcePos
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 <- m IState
forall s (m :: * -> *). MonadState s m => m s
get
case IState -> [Int]
indent_stack IState
ist of
(Int
x : [Int]
xs) -> Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
x
[Int]
_ -> Int -> m Int
forall a. a -> m a
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 IdrisParser () -> IdrisParser a -> IdrisParser a
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> IdrisParser a
p IdrisParser a -> IdrisParser () -> IdrisParser a
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* IdrisParser ()
keepTerminator
indentedBlock :: IdrisParser a -> IdrisParser [a]
indentedBlock :: forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
indentedBlock IdrisParser a
p = do IdrisParser ()
openBlock
IdrisParser ()
pushIndent
[a]
res <- IdrisParser a -> IdrisParser [a]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (IdrisParser a -> IdrisParser a
forall a. IdrisParser a -> IdrisParser a
indented IdrisParser a
p)
IdrisParser ()
popIndent
IdrisParser ()
closeBlock
[a] -> IdrisParser [a]
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
res
indentedBlock1 :: IdrisParser a -> IdrisParser [a]
indentedBlock1 :: forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
indentedBlock1 IdrisParser a
p = do IdrisParser ()
openBlock
IdrisParser ()
pushIndent
[a]
res <- IdrisParser a -> IdrisParser [a]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (IdrisParser a -> IdrisParser a
forall a. IdrisParser a -> IdrisParser a
indented IdrisParser a
p)
IdrisParser ()
popIndent
IdrisParser ()
closeBlock
[a] -> IdrisParser [a]
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 <- IdrisParser a -> IdrisParser a
forall a. IdrisParser a -> IdrisParser a
indented IdrisParser a
p
IdrisParser ()
popIndent
IdrisParser ()
closeBlock
a -> IdrisParser a
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 = Maybe a -> Bool
forall a. Maybe a -> Bool
isJust (Maybe a -> Bool) -> m (Maybe a) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe a) -> m (Maybe a)
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.lookAhead (m a -> m (Maybe a)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
P.optional m a
p)
openBlock :: IdrisParser ()
openBlock :: IdrisParser ()
openBlock = do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'
IState
ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
IState -> IdrisParser ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
ist { brace_stack = Nothing : brace_stack ist })
IdrisParser () -> IdrisParser () -> IdrisParser ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do IState
ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
Int
lvl' <- StateT IState (WriterT FC (Parsec Void String)) Int
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' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
lvl_old then Int
lvl_oldInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1
else Int
lvl'
[] -> if Int
lvl' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then Int
2 else Int
lvl'
[Maybe Int]
_ -> Int
lvl'
IState -> IdrisParser ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
ist { brace_stack = Just lvl : brace_stack ist })
IdrisParser () -> String -> IdrisParser ()
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 <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
[Maybe Int]
bs <- case IState -> [Maybe Int]
brace_stack IState
ist of
[] -> [] [Maybe Int]
-> IdrisParser ()
-> StateT IState (WriterT FC (Parsec Void String)) [Maybe Int]
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ IdrisParser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
Maybe Int
Nothing : [Maybe Int]
xs -> Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'}' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [Maybe Int]
-> StateT IState (WriterT FC (Parsec Void String)) [Maybe Int]
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Maybe Int]
-> StateT IState (WriterT FC (Parsec Void String)) [Maybe Int]
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Maybe Int]
xs StateT IState (WriterT FC (Parsec Void String)) [Maybe Int]
-> String
-> StateT IState (WriterT FC (Parsec Void String)) [Maybe Int]
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 <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). Parsing m => m Int
indent
Bool
isParen <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
char Char
')')
Bool
isIn <- IdrisParser ()
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches (String -> IdrisParser ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"in")
if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
lvl Bool -> Bool -> Bool
&& Bool -> Bool
not (Bool
isParen Bool -> Bool -> Bool
|| Bool
isIn)
then String
-> StateT IState (WriterT FC (Parsec Void String)) [Maybe Int]
forall a.
String -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"not end of block"
else [Maybe Int]
-> StateT IState (WriterT FC (Parsec Void String)) [Maybe Int]
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Maybe Int]
xs)
StateT IState (WriterT FC (Parsec Void String)) [Maybe Int]
-> StateT IState (WriterT FC (Parsec Void String)) [Maybe Int]
-> StateT IState (WriterT FC (Parsec Void String)) [Maybe Int]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do IdrisParser ()
notOpenBraces
IdrisParser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
[Maybe Int]
-> StateT IState (WriterT FC (Parsec Void String)) [Maybe Int]
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return [])
IState -> IdrisParser ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
ist { brace_stack = bs })
terminator :: IdrisParser ()
terminator :: IdrisParser ()
terminator = do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
';'; IdrisParser ()
popIndent
IdrisParser () -> IdrisParser () -> IdrisParser ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Int
c <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). Parsing m => m Int
indent; Int
l <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). MonadState IState m => m Int
lastIndent
if Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
l then IdrisParser ()
popIndent else String -> IdrisParser ()
forall a.
String -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"not a terminator"
IdrisParser () -> IdrisParser () -> IdrisParser ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Bool
isParen <- StateT IState (WriterT FC (Parsec Void String)) (Token String)
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches ([Token String]
-> StateT IState (WriterT FC (Parsec Void String)) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
[Token String]
")}")
if Bool
isParen then IdrisParser ()
popIndent else String -> IdrisParser ()
forall a.
String -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"not a terminator"
IdrisParser () -> IdrisParser () -> IdrisParser ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser () -> IdrisParser ()
forall a. IdrisParser a -> IdrisParser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.lookAhead IdrisParser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
keepTerminator :: IdrisParser ()
keepTerminator :: IdrisParser ()
keepTerminator = () ()
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser ()
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
';'
IdrisParser () -> IdrisParser () -> IdrisParser ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Int
c <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). Parsing m => m Int
indent; Int
l <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). MonadState IState m => m Int
lastIndent
Bool -> IdrisParser () -> IdrisParser ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
l) (IdrisParser () -> IdrisParser ())
-> IdrisParser () -> IdrisParser ()
forall a b. (a -> b) -> a -> b
$ String -> IdrisParser ()
forall a.
String -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"not a terminator"
IdrisParser () -> IdrisParser () -> IdrisParser ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Bool
isParen <- StateT IState (WriterT FC (Parsec Void String)) (Token String)
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches ([Token String]
-> StateT IState (WriterT FC (Parsec Void String)) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
[Token String]
")}|")
Bool
isIn <- IdrisParser ()
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches (String -> IdrisParser ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"in")
Bool -> IdrisParser () -> IdrisParser ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
isIn Bool -> Bool -> Bool
|| Bool
isParen) (IdrisParser () -> IdrisParser ())
-> IdrisParser () -> IdrisParser ()
forall a b. (a -> b) -> a -> b
$ String -> IdrisParser ()
forall a.
String -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"not a terminator"
IdrisParser () -> IdrisParser () -> IdrisParser ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser () -> IdrisParser ()
forall a. IdrisParser a -> IdrisParser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.lookAhead IdrisParser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
notEndApp :: IdrisParser ()
notEndApp :: IdrisParser ()
notEndApp = do Int
c <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). Parsing m => m Int
indent; Int
l <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). MonadState IState m => m Int
lastIndent
Bool -> IdrisParser () -> IdrisParser ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
l) (String -> IdrisParser ()
forall a.
String -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"terminator")
notEndBlock :: IdrisParser ()
notEndBlock :: IdrisParser ()
notEndBlock = do IState
ist <- StateT IState (WriterT FC (Parsec Void String)) IState
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 <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). Parsing m => m Int
indent
Bool
isParen <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches (Token String
-> StateT IState (WriterT FC (Parsec Void String)) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
Token String
')')
Bool -> IdrisParser () -> IdrisParser ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
lvl Bool -> Bool -> Bool
|| Bool
isParen) (String -> IdrisParser ()
forall a.
String -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"end of block")
[Maybe Int]
_ -> () -> IdrisParser ()
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 <- m Int
forall (m :: * -> *). MonadState IState m => m Int
lastIndent
Int
i <- m Int
forall (m :: * -> *). Parsing m => m Int
indent
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
li) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall a. String -> m a
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 <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
Bool -> IdrisParser () -> IdrisParser ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Maybe Int] -> Bool
forall a. [Maybe a] -> Bool
hasNothing ([Maybe Int] -> Bool) -> [Maybe Int] -> Bool
forall a b. (a -> b) -> a -> b
$ IState -> [Maybe Int]
brace_stack IState
ist) (IdrisParser () -> IdrisParser ())
-> IdrisParser () -> IdrisParser ()
forall a b. (a -> b) -> a -> b
$ String -> IdrisParser ()
forall a.
String -> StateT IState (WriterT FC (Parsec Void String)) a
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 = (Maybe a -> Bool) -> [Maybe a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe a -> Bool
forall a. Maybe a -> Bool
isNothing
accessibility' :: IdrisParser Accessibility
accessibility' :: IdrisParser Accessibility
accessibility' = Accessibility
Public Accessibility -> IdrisParser () -> IdrisParser Accessibility
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> IdrisParser ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"public" IdrisParser Accessibility
-> IdrisParser () -> IdrisParser Accessibility
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* String -> IdrisParser ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"export"
IdrisParser Accessibility
-> IdrisParser Accessibility -> IdrisParser Accessibility
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Accessibility
Frozen Accessibility -> IdrisParser () -> IdrisParser Accessibility
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> IdrisParser ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"export"
IdrisParser Accessibility
-> IdrisParser Accessibility -> IdrisParser Accessibility
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Accessibility
Private Accessibility -> IdrisParser () -> IdrisParser Accessibility
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> IdrisParser ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"private"
IdrisParser Accessibility -> String -> IdrisParser Accessibility
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 <- IdrisParser Accessibility
-> StateT
IState (WriterT FC (Parsec Void String)) (Maybe Accessibility)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional IdrisParser Accessibility
accessibility'
case Maybe Accessibility
acc of
Just Accessibility
a -> Accessibility -> IdrisParser Accessibility
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Accessibility
a
Maybe Accessibility
Nothing -> do IState
ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
Accessibility -> IdrisParser Accessibility
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
IState -> IdrisParser ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
i { hide_list = addDef n a (hide_list 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
(Name -> IdrisParser ()) -> [Name] -> IdrisParser ()
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
(Name -> IdrisParser ()) -> [Name] -> IdrisParser ()
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 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", possible fixes:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
"\n\nor\n\n" [String]
fixes)