{-|
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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> String
prettyError

someSpace :: Parsing m => m ()
someSpace :: forall (m :: * -> *). Parsing m => m ()
someSpace = forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall (m :: * -> *). Parsing m => m ()
simpleWhiteSpace forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *). Parsing m => m ()
singleLineComment forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *). Parsing m => m ()
multiLineComment) forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

token :: Parsing m => m a -> m a
token :: forall (m :: * -> *) a. Parsing m => m a -> m a
token m a
p = forall (m :: * -> *) a. Parsing m => m a -> m a
trackExtent m a
p forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (m :: * -> *). Parsing m => m ()
whiteSpace

highlight :: (MonadState IState m, Parsing m) => OutputAnnotation -> m a -> m a
highlight :: forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
annot m a
p = do
  (a
result, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent m a
p
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \IState
ist -> IState
ist { idris_parserHighlights :: Set (FC', OutputAnnotation)
idris_parserHighlights = forall a. Ord a => a -> Set a -> Set a
S.insert (FC -> FC'
FC' FC
fc, OutputAnnotation
annot) (IState -> Set (FC', OutputAnnotation)
idris_parserHighlights IState
ist) }
  forall (m :: * -> *) a. Monad m => a -> m a
return a
result

-- | 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 = forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
str)

clearParserWarnings :: Idris ()
clearParserWarnings :: Idris ()
clearParserWarnings = do IState
ist <- Idris IState
getIState
                         IState -> Idris ()
putIState IState
ist { parserWarnings :: [(FC, Err)]
parserWarnings = [] }

reportParserWarnings :: Idris ()
reportParserWarnings :: Idris ()
reportParserWarnings = do IState
ist <- Idris IState
getIState
                          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry FC -> OutputDoc -> Idris ()
iWarn)
                                (forall a b. (a -> b) -> [a] -> [b]
map (\ (FC
fc, Err
err) -> (FC
fc, IState -> Err -> OutputDoc
pprintErr IState
ist Err
err)) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                 forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                 forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (\(FC
fc, Err
err) (FC
fc', Err
err') ->
                                         FC -> FC'
FC' FC
fc forall a. Eq a => a -> a -> Bool
== FC -> FC'
FC' FC
fc' Bool -> Bool -> Bool
&& Err
err forall a. Eq a => a -> a -> Bool
== Err
err') forall a b. (a -> b) -> a -> b
$
                                 IState -> [(FC, Err)]
parserWarnings IState
ist)
                          Idris ()
clearParserWarnings


parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()
parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()
parserWarning FC
fc Maybe Opt
warnOpt Err
warnErr = do
  IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
  let cmdline :: [Opt]
cmdline = IOption -> [Opt]
opt_cmdline (IState -> IOption
idris_options IState
ist)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
cmdline) Maybe Opt
warnOpt) forall a b. (a -> b) -> a -> b
$
    forall s (m :: * -> *). MonadState s m => s -> m ()
put IState
ist { parserWarnings :: [(FC, Err)]
parserWarnings = (FC
fc, Err
warnErr) forall a. a -> [a] -> [a]
: IState -> [(FC, Err)]
parserWarnings IState
ist }

{- * 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 = () forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
isSpace

-- | 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 = () forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
isEol forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.lookAhead forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"end of line"

{- | Consumes a single-line comment

@
     SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;
@
 -}
singleLineComment :: Parsing m => m ()
singleLineComment :: forall (m :: * -> *). Parsing m => m ()
singleLineComment = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.hidden (() forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m String
string String
"--" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isEol)) forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => m ()
eol)

{- | 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 = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.hidden forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => String -> m String
string String
"{-" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m String
string String
"-}" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
                              forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *). Parsing m => String -> m String
string String
"{-" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => m ()
inCommentChars
  where inCommentChars :: Parsing m => m ()
        inCommentChars :: forall (m :: * -> *). Parsing m => m ()
inCommentChars =     forall (m :: * -> *). Parsing m => String -> m String
string String
"-}" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => m ()
multiLineComment) forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => m ()
inCommentChars
                         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *). Parsing m => String -> m String
string String
"|||" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isEol)) forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => m ()
eol forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => m ()
inCommentChars
                         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. MonadPlus m => m a -> m ()
P.skipSome (forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.noneOf String
startEnd) forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => m ()
inCommentChars
                         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
startEnd forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => m ()
inCommentChars
                         forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"end of comment"
        startEnd :: String
        startEnd :: String
startEnd = String
"{}-"

{-| 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 forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => m String
docCommentLine
                [String]
rest <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall a. IdrisParser a -> IdrisParser a
indented forall (m :: * -> *). Parsing m => m String
docCommentLine)
                [(Name, String)]
args <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many forall a b. (a -> b) -> a -> b
$ do (Name
name, String
first) <- forall a. IdrisParser a -> IdrisParser a
indented StateT IState (WriterT FC (Parsec Void String)) (Name, String)
argDocCommentLine
                                  [String]
rest <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall a. IdrisParser a -> IdrisParser a
indented forall (m :: * -> *). Parsing m => m String
docCommentLine)
                                  forall (m :: * -> *) a. Monad m => a -> m a
return (Name
name, forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a. a -> [a] -> [a]
intersperse String
"\n" (String
firstforall a. a -> [a] -> [a]
:[String]
rest)))
                IdrisParser ()
popIndent
                forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> Docstring ()
parseDocstring forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a. a -> [a] -> [a]
intersperse String
"\n" (String
dcforall a. a -> [a] -> [a]
:[String]
rest))),
                        forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, String
d) -> (Name
n, Text -> Docstring ()
parseDocstring (String -> Text
T.pack String
d))) [(Name, String)]
args)

  where docCommentLine :: Parsing m => m String
        docCommentLine :: forall (m :: * -> *). Parsing m => m String
docCommentLine = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.hidden forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ do
                           forall (m :: * -> *). Parsing m => String -> m String
string String
"|||"
                           forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy (forall a. Eq a => a -> a -> Bool
==Char
' '))
                           String
contents <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option String
"" (do Char
first <- forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy (\Token String
c -> Bool -> Bool
not (Char -> Bool
isEol Token String
c Bool -> Bool -> Bool
|| Token String
c forall a. Eq a => a -> a -> Bool
== Char
'@'))
                                                       String
res <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isEol))
                                                       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Char
firstforall a. a -> [a] -> [a]
:String
res)
                           forall (m :: * -> *). Parsing m => m ()
eol ; forall (m :: * -> *). Parsing m => m ()
someSpace
                           forall (m :: * -> *) a. Monad m => a -> m a
return String
contents

        argDocCommentLine :: IdrisParser (Name, String)
        argDocCommentLine :: StateT IState (WriterT FC (Parsec Void String)) (Name, String)
argDocCommentLine = do forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
P.string String
"|||"
                               forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
isSpace)
                               forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
'@'
                               forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
isSpace)
                               Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
                               forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
isSpace)
                               String
docs <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isEol))
                               forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Tokens s)
P.eol ; forall (m :: * -> *). Parsing m => m ()
someSpace
                               forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, String
docs)

-- | Parses some white space
whiteSpace :: Parsing m => m ()
whiteSpace :: forall (m :: * -> *). Parsing m => m ()
whiteSpace = forall (m :: * -> *). Parsing m => m ()
someSpace forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Parses a string literal
stringLiteral :: Parsing m => m String
stringLiteral :: forall (m :: * -> *). Parsing m => m String
stringLiteral = forall (m :: * -> *) a. Parsing m => m a -> m a
token forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
'"' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
P.manyTill forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
P.charLiteral (forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
'"')

-- | Parses a char literal
charLiteral :: Parsing m => m Char
charLiteral :: forall (m :: * -> *). Parsing m => m Char
charLiteral = forall (m :: * -> *) a. Parsing m => m a -> m a
token forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
'\'' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
P.charLiteral forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
'\''

-- | Parses a natural number
natural :: Parsing m => m Integer
natural :: forall (m :: * -> *). Parsing m => m Integer
natural = forall (m :: * -> *) a. Parsing m => m a -> m a
token (    forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
'0' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char' Char
'x' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
P.hexadecimal)
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
'0' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char' Char
'o' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
P.octal)
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
P.decimal)

-- | Parses a floating point number
float :: Parsing m => m Double
float :: forall (m :: * -> *). Parsing m => m Double
float = forall (m :: * -> *) a. Parsing m => m a -> m a
token forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, RealFloat a) =>
m a
P.float

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

reservedIdentifiers :: HS.HashSet String
reservedIdentifiers :: HashSet String
reservedIdentifiers = forall a. (Eq a, Hashable a) => [a] -> HashSet a
HS.fromList
  [ String
"Type"
  , String
"case", String
"class", String
"codata", String
"constructor", String
"corecord", String
"data"
  , String
"do", String
"dsl", String
"else", String
"export", String
"if", String
"implementation", String
"implicit"
  , String
"import", String
"impossible", String
"in", String
"infix", String
"infixl", String
"infixr", String
"instance"
  , String
"interface", String
"let", String
"mutual", String
"namespace", String
"of", String
"parameters", String
"partial"
  , String
"postulate", String
"private", String
"proof", String
"public", String
"quoteGoal", String
"record"
  , String
"rewrite", String
"syntax", String
"then", String
"total", String
"using", String
"where", String
"with"
  ]

identifierOrReservedWithExtraChars :: Parsing m => String -> m String
identifierOrReservedWithExtraChars :: forall (m :: * -> *). Parsing m => String -> m String
identifierOrReservedWithExtraChars String
extraChars = forall (m :: * -> *) a. Parsing m => m a -> m a
token forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ do
  Char
c <- forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
isAlpha forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
"_"
  String
cs <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
isAlphaNum forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
extraChars)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Char
c forall a. a -> [a] -> [a]
: String
cs

char :: Parsing m => Char -> m Char
char :: forall (m :: * -> *). Parsing m => Char -> m Char
char = forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char

string :: Parsing m => String -> m String
string :: forall (m :: * -> *). Parsing m => String -> m String
string = forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
P.string

-- | Parses a character as a token
lchar :: Parsing m => Char -> m Char
lchar :: forall (m :: * -> *). Parsing m => Char -> m Char
lchar = forall (m :: * -> *) a. Parsing m => m a -> m a
token forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char

symbol :: Parsing m => String -> m ()
symbol :: forall (m :: * -> *). Parsing m => String -> m ()
symbol = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Parsing m => m a -> m a
token forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
P.string

-- | Parses a reserved identifier
reserved :: Parsing m => String -> m ()
reserved :: forall (m :: * -> *). Parsing m => String -> m ()
reserved String
name = forall (m :: * -> *) a. Parsing m => m a -> m a
token forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ do
  forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
P.string String
name
  forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
P.notFollowedBy (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy Char -> Bool
isAlphaNum forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
"_'.") forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"end of " forall a. [a] -> [a] -> [a]
++ String
name

-- | Parses an identifier as a token
identifierWithExtraChars :: Parsing m => String -> m String
identifierWithExtraChars :: forall (m :: * -> *). Parsing m => String -> m String
identifierWithExtraChars String
extraChars = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ do
  String
ident <- forall (m :: * -> *). Parsing m => String -> m String
identifierOrReservedWithExtraChars String
extraChars
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
ident forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HS.member` HashSet String
reservedIdentifiers) forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. NonEmpty Char -> ErrorItem t
P.Label forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> NonEmpty a
NonEmpty.fromList forall a b. (a -> b) -> a -> b
$ String
"reserved " forall a. [a] -> [a] -> [a]
++ String
ident
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
ident forall a. Eq a => a -> a -> Bool
== String
"_") forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. NonEmpty Char -> ErrorItem t
P.Label forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> NonEmpty a
NonEmpty.fromList forall a b. (a -> b) -> a -> b
$ String
"wildcard"
  forall (m :: * -> *) a. Monad m => a -> m a
return String
ident

identifier :: Parsing m => m String
identifier :: forall (m :: * -> *). Parsing m => m String
identifier = forall (m :: * -> *). Parsing m => String -> m String
identifierWithExtraChars String
"_'."

-- | 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 = forall (m :: * -> *). Parsing m => m String -> [String] -> m Name
maybeWithNS forall (m :: * -> *). Parsing m => m String
identifier [String]
bad forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"name"

-- | 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 <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option String
"" (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.lookAhead forall (m :: * -> *). Parsing m => m String
identifier)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
bad) forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. NonEmpty Char -> ErrorItem t
P.Label forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> NonEmpty a
NonEmpty.fromList forall a b. (a -> b) -> a -> b
$ String
"reserved identifier"
  (String, String) -> Name
mkName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice (forall a. [a] -> [a]
reverse (forall (m :: * -> *). Parsing m => m String -> m (String, String)
parserNoNS m String
parser forall a. a -> [a] -> [a]
: forall (m :: * -> *).
Parsing m =>
m String -> String -> [m (String, String)]
parsersNS m String
parser String
i))
  where parserNoNS :: Parsing m => m String -> m (String, String)
        parserNoNS :: forall (m :: * -> *). Parsing m => m String -> m (String, String)
parserNoNS = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\String
x -> (String
x, String
""))
        parserNS   :: Parsing m => m String -> String -> m (String, String)
        parserNS :: forall (m :: * -> *).
Parsing m =>
m String -> String -> m (String, String)
parserNS   m String
parser String
ns = do String
xs <- forall (m :: * -> *) a. Parsing m => m a -> m a
trackExtent (forall (m :: * -> *). Parsing m => String -> m String
string String
ns)
                                  forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'.'
                                  String
x <- m String
parser
                                  forall (m :: * -> *) a. Monad m => a -> m a
return (String
x, String
xs)
        parsersNS  :: Parsing m => m String -> String -> [m (String, String)]
        parsersNS :: forall (m :: * -> *).
Parsing m =>
m String -> String -> [m (String, String)]
parsersNS m String
parser String
i = [forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *).
Parsing m =>
m String -> String -> m (String, String)
parserNS m String
parser String
ns) | String
ns <- (forall a. (a -> Bool) -> [a] -> [[a]]
initsEndAt (forall a. Eq a => a -> a -> Bool
==Char
'.') String
i)]

-- | 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
    Map [Text] [Text]
aliases  <- IState -> Map [Text] [Text]
module_aliases  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
    Name
n <- forall (m :: * -> *). Parsing m => [String] -> m Name
iName [String]
keywords
    forall (m :: * -> *) a. Monad m => a -> m a
return (Map [Text] [Text] -> Name -> Name
unalias Map [Text] [Text]
aliases Name
n)
   forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"name"
  where
    unalias :: M.Map [T.Text] [T.Text] -> Name -> Name
    unalias :: Map [Text] [Text] -> Name -> Name
unalias Map [Text] [Text]
aliases (NS Name
n [Text]
ns) | Just [Text]
ns' <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup [Text]
ns Map [Text] [Text]
aliases = Name -> [Text] -> Name
NS Name
n [Text]
ns'
    unalias Map [Text] [Text]
aliases Name
name = Name
name

{- | 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 = [] forall a. a -> [a] -> [a]
: [[a]]
x_inits_xs
                    | Bool
otherwise = [[a]]
x_inits_xs
  where x_inits_xs :: [[a]]
x_inits_xs = [a
x forall a. a -> [a] -> [a]
: [a]
cs | [a]
cs <- forall a. (a -> Bool) -> [a] -> [[a]]
initsEndAt a -> Bool
p [a]
xs]


{- | 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) (forall a. [a] -> [a]
reverse (String -> [String]
parseNS String
ns))
  where parseNS :: String -> [String]
parseNS String
x = case forall a. (a -> Bool) -> [a] -> ([a], [a])
span (forall a. Eq a => a -> a -> Bool
/= Char
'.') String
x of
                      (String
x, String
"")    -> [String
x]
                      (String
x, Char
'.':String
y) -> String
x forall a. a -> [a] -> [a]
: String -> [String]
parseNS String
y

-- | Parse a package name
packageName :: Parsing m => m String
packageName :: forall (m :: * -> *). Parsing m => m String
packageName = (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
firstChars forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
remChars)
  where firstChars :: String
firstChars = [Char
'a'..Char
'z'] forall a. [a] -> [a] -> [a]
++ [Char
'A'..Char
'Z']
        remChars :: String
remChars = [Char
'a'..Char
'z'] forall a. [a] -> [a] -> [a]
++ [Char
'A'..Char
'Z'] forall a. [a] -> [a] -> [a]
++ [Char
'0'..Char
'9'] forall a. [a] -> [a] -> [a]
++ [Char
'-',Char
'_']

{- * 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 forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
`P.sepBy1` (forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
P.space forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
',' forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
P.space)

{- * Layout helpers -}

-- | Push indentation to stack
pushIndent :: IdrisParser ()
pushIndent :: IdrisParser ()
pushIndent = do Int
columnNumber <- forall (m :: * -> *). Parsing m => m Int
indent
                IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
ist { indent_stack :: [Int]
indent_stack = Int
columnNumber forall a. a -> [a] -> [a]
: IState -> [Int]
indent_stack IState
ist })

-- | Pops indentation from stack
popIndent :: IdrisParser ()
popIndent :: IdrisParser ()
popIndent = do IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
               case IState -> [Int]
indent_stack IState
ist of
                 [] -> forall a. HasCallStack => String -> a
error String
"The impossible happened! Tried to pop an indentation level where none was pushed (underflow)."
                 (Int
x : [Int]
xs) -> forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
ist { indent_stack :: [Int]
indent_stack = [Int]
xs })


-- | Gets current indentation
indent :: Parsing m => m Int
indent :: forall (m :: * -> *). Parsing m => m Int
indent = Pos -> Int
P.unPos forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> Pos
P.sourceColumn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
P.getSourcePos

-- | Gets last indentation
lastIndent :: (MonadState IState m) => m Int
lastIndent :: forall (m :: * -> *). MonadState IState m => m Int
lastIndent = do IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                case IState -> [Int]
indent_stack IState
ist of
                  (Int
x : [Int]
xs) -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
x
                  [Int]
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
1

-- | Applies parser in an indented position
indented :: IdrisParser a -> IdrisParser a
indented :: forall a. IdrisParser a -> IdrisParser a
indented IdrisParser a
p = IdrisParser ()
notEndBlock forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> IdrisParser a
p forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* IdrisParser ()
keepTerminator

-- | Applies parser to get a block (which has possibly indented statements)
indentedBlock :: IdrisParser a -> IdrisParser [a]
indentedBlock :: forall a. IdrisParser a -> IdrisParser [a]
indentedBlock IdrisParser a
p = do IdrisParser ()
openBlock
                     IdrisParser ()
pushIndent
                     [a]
res <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall a. IdrisParser a -> IdrisParser a
indented IdrisParser a
p)
                     IdrisParser ()
popIndent
                     IdrisParser ()
closeBlock
                     forall (m :: * -> *) a. Monad m => a -> m a
return [a]
res

-- | Applies parser to get a block with at least one statement (which has possibly indented statements)
indentedBlock1 :: IdrisParser a -> IdrisParser [a]
indentedBlock1 :: forall a. IdrisParser a -> IdrisParser [a]
indentedBlock1 IdrisParser a
p = do IdrisParser ()
openBlock
                      IdrisParser ()
pushIndent
                      [a]
res <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (forall a. IdrisParser a -> IdrisParser a
indented IdrisParser a
p)
                      IdrisParser ()
popIndent
                      IdrisParser ()
closeBlock
                      forall (m :: * -> *) a. Monad m => a -> m a
return [a]
res

-- | 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 <- forall a. IdrisParser a -> IdrisParser a
indented IdrisParser a
p
                      IdrisParser ()
popIndent
                      IdrisParser ()
closeBlock
                      forall (m :: * -> *) a. Monad m => a -> m a
return a
res


-- | 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 = forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.lookAhead (forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
P.optional m a
p)

-- | Parses a start of block
openBlock :: IdrisParser ()
openBlock :: IdrisParser ()
openBlock =     do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'
                   IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                   forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
ist { brace_stack :: [Maybe Int]
brace_stack = forall a. Maybe a
Nothing forall a. a -> [a] -> [a]
: IState -> [Maybe Int]
brace_stack IState
ist })
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                   Int
lvl' <- forall (m :: * -> *). Parsing m => m Int
indent
                    -- 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' forall a. Ord a => a -> a -> Bool
<= Int
lvl_old then Int
lvl_oldforall a. Num a => a -> a -> a
+Int
1
                                                          else Int
lvl'
                                   [] -> if Int
lvl' forall a. Eq a => a -> a -> Bool
== Int
1 then Int
2 else Int
lvl'
                                   [Maybe Int]
_ -> Int
lvl'
                   forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
ist { brace_stack :: [Maybe Int]
brace_stack = forall a. a -> Maybe a
Just Int
lvl forall a. a -> [a] -> [a]
: IState -> [Maybe Int]
brace_stack IState
ist })
            forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"start of block"

-- | Parses an end of block
closeBlock :: IdrisParser ()
closeBlock :: IdrisParser ()
closeBlock = do IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                [Maybe Int]
bs <- case IState -> [Maybe Int]
brace_stack IState
ist of
                        []  -> [] forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
                        Maybe Int
Nothing : [Maybe Int]
xs -> forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'}' forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return [Maybe Int]
xs forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"end of block"
                        Just Int
lvl : [Maybe Int]
xs -> (do Int
i   <- forall (m :: * -> *). Parsing m => m Int
indent
                                             Bool
isParen <- forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches (forall (m :: * -> *). Parsing m => Char -> m Char
char Char
')')
                                             Bool
isIn <- forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"in")
                                             if Int
i forall a. Ord a => a -> a -> Bool
>= Int
lvl Bool -> Bool -> Bool
&& Bool -> Bool
not (Bool
isParen Bool -> Bool -> Bool
|| Bool
isIn)
                                                then forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"not end of block"
                                                else forall (m :: * -> *) a. Monad m => a -> m a
return [Maybe Int]
xs)
                                          forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do IdrisParser ()
notOpenBraces
                                                  forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
                                                  forall (m :: * -> *) a. Monad m => a -> m a
return [])
                forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
ist { brace_stack :: [Maybe Int]
brace_stack = [Maybe Int]
bs })

-- | Parses a terminator
terminator :: IdrisParser ()
terminator :: IdrisParser ()
terminator =     do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
';'; IdrisParser ()
popIndent
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Int
c <- forall (m :: * -> *). Parsing m => m Int
indent; Int
l <- forall (m :: * -> *). MonadState IState m => m Int
lastIndent
                    if Int
c forall a. Ord a => a -> a -> Bool
<= Int
l then IdrisParser ()
popIndent else forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"not a terminator"
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Bool
isParen <- forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches (forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
")}")
                    if Bool
isParen then IdrisParser ()
popIndent else forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"not a terminator"
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.lookAhead forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof

-- | Parses and keeps a terminator
keepTerminator :: IdrisParser ()
keepTerminator :: IdrisParser ()
keepTerminator =  () forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
';'
              forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Int
c <- forall (m :: * -> *). Parsing m => m Int
indent; Int
l <- forall (m :: * -> *). MonadState IState m => m Int
lastIndent
                     forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
c forall a. Ord a => a -> a -> Bool
<= Int
l) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"not a terminator"
              forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Bool
isParen <- forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches (forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
")}|")
                     Bool
isIn <- forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"in")
                     forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
isIn Bool -> Bool -> Bool
|| Bool
isParen) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"not a terminator"
              forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.lookAhead forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof

-- | Checks if application expression does not end
notEndApp :: IdrisParser ()
notEndApp :: IdrisParser ()
notEndApp = do Int
c <- forall (m :: * -> *). Parsing m => m Int
indent; Int
l <- forall (m :: * -> *). MonadState IState m => m Int
lastIndent
               forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
c forall a. Ord a => a -> a -> Bool
<= Int
l) (forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"terminator")

-- | Checks that it is not end of block
notEndBlock :: IdrisParser ()
notEndBlock :: IdrisParser ()
notEndBlock = do IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                 case IState -> [Maybe Int]
brace_stack IState
ist of
                      Just Int
lvl : [Maybe Int]
xs -> do Int
i <- forall (m :: * -> *). Parsing m => m Int
indent
                                          Bool
isParen <- forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches (forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
')')
                                          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
i forall a. Ord a => a -> a -> Bool
< Int
lvl Bool -> Bool -> Bool
|| Bool
isParen) (forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"end of block")
                      [Maybe Int]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

indentGt :: (Parsing m, MonadState IState m) => m ()
indentGt :: forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt = do
  Int
li <- forall (m :: * -> *). MonadState IState m => m Int
lastIndent
  Int
i <- forall (m :: * -> *). Parsing m => m Int
indent
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
i forall a. Ord a => a -> a -> Bool
<= Int
li) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Wrong indention: should be greater than context indentation"

-- | Checks that there are no braces that are not closed
notOpenBraces :: IdrisParser ()
notOpenBraces :: IdrisParser ()
notOpenBraces = do IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                   forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. [Maybe a] -> Bool
hasNothing forall a b. (a -> b) -> a -> b
$ IState -> [Maybe Int]
brace_stack IState
ist) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"end of input"
  where hasNothing :: [Maybe a] -> Bool
        hasNothing :: forall a. [Maybe a] -> Bool
hasNothing = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Maybe a -> Bool
isNothing

{- | Parses an accessibilty modifier (e.g. public, private) -}
accessibility' :: IdrisParser Accessibility
accessibility' :: IdrisParser Accessibility
accessibility' = Accessibility
Public  forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"public" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"export"
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Accessibility
Frozen  forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"export"
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Accessibility
Private forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"private"
             forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"accessibility modifier"

accessibility :: IdrisParser Accessibility
accessibility :: IdrisParser Accessibility
accessibility = do Maybe Accessibility
acc <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional IdrisParser Accessibility
accessibility'
                   case Maybe Accessibility
acc of
                        Just Accessibility
a -> forall (m :: * -> *) a. Monad m => a -> m a
return Accessibility
a
                        Maybe Accessibility
Nothing -> do IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                                      forall (m :: * -> *) a. Monad m => a -> m a
return (IState -> Accessibility
default_access IState
ist)

-- | Adds accessibility option for function
addAcc :: Name -> Accessibility -> IdrisParser ()
addAcc :: Name -> Accessibility -> IdrisParser ()
addAcc Name
n Accessibility
a = do IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
                forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
i { hide_list :: Ctxt Accessibility
hide_list = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n Accessibility
a (IState -> Ctxt Accessibility
hide_list IState
i) })

{- | 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
                         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
                    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 forall a. [a] -> [a] -> [a]
++ String
", possible fixes:\n" forall a. [a] -> [a] -> [a]
++ (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
intersperse String
"\n\nor\n\n" [String]
fixes)