{-|
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
  (result, fc) <- m a -> m (a, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent m a
p
  modify $ \IState
ist -> IState
ist { idris_parserHighlights = S.insert (FC' fc, annot) (idris_parserHighlights ist) }
  return 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 ist <- Idris IState
getIState
                         putIState ist { parserWarnings = [] }

reportParserWarnings :: Idris ()
reportParserWarnings :: Idris ()
reportParserWarnings = do ist <- Idris IState
getIState
                          mapM_ (uncurry iWarn)
                                (map (\ (FC
fc, Err
err) -> (FC
fc, IState -> Err -> OutputDoc
pprintErr IState
ist Err
err)) .
                                 reverse .
                                 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') $
                                 parserWarnings ist)
                          clearParserWarnings


parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()
parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()
parserWarning FC
fc Maybe Opt
warnOpt Err
warnErr = do
  ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
  let cmdline = IOption -> [Opt]
opt_cmdline (IState -> IOption
idris_options IState
ist)
  unless (maybe False (`elem` cmdline) warnOpt) $
    put 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 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
                rest <- many (indented docCommentLine)
                args <- many $ do (name, first) <- indented argDocCommentLine
                                  rest <- many (indented docCommentLine)
                                  return (name, concat (intersperse "\n" (first:rest)))
                popIndent
                return (parseDocstring $ T.pack (concat (intersperse "\n" (dc:rest))),
                        map (\(Name
n, String
d) -> (Name
n, Text -> Docstring ()
parseDocstring (String -> Text
T.pack String
d))) 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
' '))
                           contents <- String -> m String -> m String
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option String
"" (do 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
'@'))
                                                       res <- many (P.satisfy (not . isEol))
                                                       return $ first:res)
                           eol ; someSpace
                           return 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)
                               n <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
                               P.many (P.satisfy isSpace)
                               docs <- P.many (P.satisfy (not . isEol))
                               P.eol ; someSpace
                               return (n, 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
  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]
"_"
  cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf extraChars)
  return $ c : 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
  ident <- String -> m String
forall (m :: * -> *). Parsing m => String -> m String
identifierOrReservedWithExtraChars String
extraChars
  when (ident `HS.member` reservedIdentifiers) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved " ++ ident
  when (ident == "_") $ P.unexpected . P.Label . NonEmpty.fromList $ "wildcard"
  return 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
  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)
  when (i `elem` bad) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved identifier"
  mkName <$> P.choice (reverse (parserNoNS parser : parsersNS parser i))
  where parserNoNS :: Parsing m => m String -> m (String, String)
        parserNoNS :: 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 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)
                                  lchar '.'
                                  x <- parser
                                  return (x, 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
    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
    aliases  <- module_aliases  <$> get
    n <- iName keywords
    return (unalias aliases 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 columnNumber <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). Parsing m => m Int
indent
                ist <- get
                put (ist { indent_stack = columnNumber : indent_stack ist })

-- | Pops indentation from stack
popIndent :: IdrisParser ()
popIndent :: IdrisParser ()
popIndent = do ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
               case indent_stack 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 ist <- m IState
forall s (m :: * -> *). MonadState s m => m s
get
                case indent_stack 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
                     res <- IdrisParser a
-> StateT IState (WriterT FC (Parsec Void String)) [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)
                     popIndent
                     closeBlock
                     return 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
                      res <- IdrisParser a
-> StateT IState (WriterT FC (Parsec Void String)) [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)
                      popIndent
                      closeBlock
                      return 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
                      res <- IdrisParser a -> IdrisParser a
forall a. IdrisParser a -> IdrisParser a
indented IdrisParser a
p
                      popIndent
                      closeBlock
                      return 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
'{'
                   ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                   put (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 ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                   lvl' <- indent
                    -- if we're not indented further, it's an empty block, so
                    -- increment lvl to ensure we get to the end
                   let 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'
                   put (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 ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                bs <- case brace_stack 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 i   <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). Parsing m => m Int
indent
                                             isParen <- lookAheadMatches (char ')')
                                             isIn <- lookAheadMatches (reserved "in")
                                             if i >= lvl && not (isParen || isIn)
                                                then fail "not end of block"
                                                else return 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 [])
                put (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 c <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). Parsing m => m Int
indent; l <- lastIndent
                    if c <= l then popIndent else fail "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 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 isParen then popIndent else fail "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 c <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). Parsing m => m Int
indent; l <- lastIndent
                     unless (c <= l) $ fail "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 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]
")}|")
                     isIn <- lookAheadMatches (reserved "in")
                     unless (isIn || isParen) $ fail "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 c <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). Parsing m => m Int
indent; l <- lastIndent
               when (c <= l) (fail "terminator")

-- | Checks that it is not end of block
notEndBlock :: IdrisParser ()
notEndBlock :: IdrisParser ()
notEndBlock = do ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                 case brace_stack ist of
                      Just Int
lvl : [Maybe Int]
xs -> do i <- StateT IState (WriterT FC (Parsec Void String)) Int
forall (m :: * -> *). Parsing m => m Int
indent
                                          isParen <- lookAheadMatches (P.char ')')
                                          when (i < lvl || isParen) (fail "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
  li <- m Int
forall (m :: * -> *). MonadState IState m => m Int
lastIndent
  i <- indent
  when (i <= li) $ fail "Wrong indention: should be greater than context indentation"

-- | Checks that there are no braces that are not closed
notOpenBraces :: IdrisParser ()
notOpenBraces :: IdrisParser ()
notOpenBraces = do ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                   when (hasNothing $ brace_stack ist) $ fail "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 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 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 ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                                      return (default_access ist)

-- | Adds accessibility option for function
addAcc :: Name -> Accessibility -> IdrisParser ()
addAcc :: Name -> Accessibility -> IdrisParser ()
addAcc Name
n Accessibility
a = do i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                put (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)