{-|
Module      : Idris.Parser.Helpers
Description : Utilities for Idris' parser.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE ConstraintKinds, FlexibleContexts, MultiParamTypeClasses #-}
module Idris.Parser.Helpers
  ( module Idris.Parser.Stack
    -- * The parser
  , IdrisParser
  , parseErrorDoc
    -- * Space
  , whiteSpace
  , someSpace
  , eol
  , isEol
    -- * Basic parsers
  , char
  , symbol
  , string
  , lookAheadMatches
    -- * Terminals
  , lchar
  , reserved
  , docComment
  , token
  , natural
  , charLiteral
  , stringLiteral
  , float
    -- * Names
  , bindList
  , maybeWithNS
  , iName
  , name
  , identifier
  , identifierWithExtraChars
  , packageName
    -- * Access
  , accessibility
  , accData
  , addAcc
    -- * Warnings and errors
  , fixErrorMsg
  , parserWarning
  , clearParserWarnings
  , reportParserWarnings
    -- * Highlighting
  , highlight
  , keyword
    -- * Indentation
  , pushIndent
  , popIndent
  , indentGt
  , notOpenBraces
    -- * Indented blocks
  , openBlock
  , closeBlock
  , terminator
  , notEndBlock
  , indentedBlock
  , indentedBlock1
  , indentedBlockS
  , indented
    -- * Miscellaneous
  , 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


-- | Idris parser with state used during parsing
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

-- | Parse a reserved identfier, highlighting it as a keyword
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 }

{- * Space, comments and literals (token/lexing like parsers) -}

-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)
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

-- | Checks if a charcter is end of line
isEol :: Char -> Bool
isEol :: Char -> Bool
isEol Char
'\n' = Bool
True
isEol  Char
_   = Bool
False

-- | A parser that succeeds at the end of the line
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"

{- | Consumes a single-line comment

@
     SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;
@
 -}
singleLineComment :: Parsing m => m ()
singleLineComment :: forall (m :: * -> *). Parsing m => m ()
singleLineComment = 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)

{- | Consumes a multi-line comment

@
  MultiLineComment_t ::=
     '{ -- }'
   | '{ -' InCommentChars_t
  ;
@

@
  InCommentChars_t ::=
   '- }'
   | MultiLineComment_t InCommentChars_t
   | ~'- }'+ InCommentChars_t
  ;
@
-}
multiLineComment :: Parsing m => m ()
multiLineComment :: forall (m :: * -> *). Parsing m => m ()
multiLineComment = 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
"{}-"

{-| Parses a documentation comment

@
  DocComment_t ::= DocCommentLine (ArgCommentLine DocCommentLine*)* ;

  DocCommentLine ::= '|||' ~EOL_t* EOL_t ;
  ArgCommentLine ::= '|||' '@' ~EOL_t* EOL_t ;
@
 -}
docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])
docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])
docComment = 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)

-- | Parses some white space
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 ()

-- | Parses a string literal
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
'"')

-- | Parses a char literal
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
'\''

-- | Parses a natural number
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)

-- | Parses a floating point number
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

{- * Symbols, identifiers, names and operators -}

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
identifierOrReservedWithExtraChars :: forall (m :: * -> *). Parsing m => String -> m String
identifierOrReservedWithExtraChars 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

-- | Parses a character as a token
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

-- | Parses a reserved identifier
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

-- | Parses an identifier as a token
identifierWithExtraChars :: Parsing m => String -> m String
identifierWithExtraChars :: forall (m :: * -> *). Parsing m => String -> m String
identifierWithExtraChars 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
"_'."

-- | Parses an identifier with possible namespace as a name
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"

-- | Parses an string possibly prefixed by a namespace
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)]

-- | Parses a name
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

{- | List of all initial segments in ascending order of a list.  Every
such initial segment ends right before an element satisfying the given
condition.
-}
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]


{- | Create a `Name' from a pair of strings representing a base name and its
 namespace.
-}
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

-- | Parse a package name
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
'_']

{- * Position helpers -}

{-* Syntax helpers-}
-- | Bind constraints to term
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 p@ parses one or more occurences of `p`,
     separated by commas and optional whitespace. -}
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)

{- * Layout helpers -}

-- | Push indentation to stack
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 })

-- | Pops indentation from stack
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 })


-- | Gets current indentation
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

-- | Gets last indentation
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

-- | Applies parser in an indented position
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

-- | Applies parser to get a block (which has possibly indented statements)
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

-- | Applies parser to get a block with at least one statement (which has possibly indented statements)
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

-- | Applies parser to get a block with exactly one (possibly indented) statement
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


-- | Checks if the following character matches provided parser
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)

-- | Parses a start of block
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
                    -- if we're not indented further, it's an empty block, so
                    -- increment lvl to ensure we get to the end
                   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"

-- | Parses an end 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 })

-- | Parses a terminator
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

-- | Parses and keeps a terminator
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

-- | Checks if application expression does not end
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")

-- | Checks that it is not end of block
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"

-- | Checks that there are no braces that are not closed
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

{- | Parses an accessibilty modifier (e.g. public, private) -}
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)

-- | Adds accessibility option for function
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) })

{- | Add accessbility option for data declarations
 (works for interfaces too - 'abstract' means the data/interface is visible but members not) -}
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 -- so that it can be used in public definitions
                         (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 -- so that they are invisible
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


{- * Error reporting helpers -}
{- | Error message with possible fixes list -}
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)