Copyright | License : BSD3 |
---|---|
Maintainer | The Idris Community. |
Safe Haskell | None |
Language | Haskell98 |
- type IdrisParser = StateT IState IdrisInnerParser
- newtype IdrisInnerParser a = IdrisInnerParser {
- runInnerParser :: Parser a
- type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)
- class HasLastTokenSpan m where
- runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Result res
- highlightP :: FC -> OutputAnnotation -> IdrisParser ()
- noDocCommentHere :: String -> IdrisParser ()
- clearParserWarnings :: Idris ()
- reportParserWarnings :: Idris ()
- parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()
- simpleWhiteSpace :: MonadicParsing m => m ()
- isEol :: Char -> Bool
- eol :: MonadicParsing m => m ()
- singleLineComment :: MonadicParsing m => m ()
- multiLineComment :: MonadicParsing m => m ()
- docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])
- whiteSpace :: MonadicParsing m => m ()
- stringLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC)
- charLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (Char, FC)
- natural :: (MonadicParsing m, HasLastTokenSpan m) => m (Integer, FC)
- integer :: MonadicParsing m => m Integer
- float :: (MonadicParsing m, HasLastTokenSpan m) => m (Double, FC)
- idrisStyle :: MonadicParsing m => IdentifierStyle m
- char :: MonadicParsing m => Char -> m Char
- string :: MonadicParsing m => String -> m String
- lchar :: MonadicParsing m => Char -> m Char
- lcharFC :: MonadicParsing m => Char -> m FC
- symbol :: MonadicParsing m => String -> m String
- symbolFC :: MonadicParsing m => String -> m FC
- reserved :: MonadicParsing m => String -> m ()
- reservedFC :: MonadicParsing m => String -> m FC
- reservedHL :: String -> IdrisParser ()
- reservedOp :: MonadicParsing m => String -> m ()
- reservedOpFC :: MonadicParsing m => String -> m FC
- identifier :: MonadicParsing m => m (String, FC)
- iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)
- maybeWithNS :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)
- name :: IdrisParser (Name, FC)
- initsEndAt :: (a -> Bool) -> [a] -> [[a]]
- mkName :: (String, String) -> Name
- opChars :: String
- operatorLetter :: MonadicParsing m => m Char
- commentMarkers :: [String]
- invalidOperators :: [String]
- operator :: MonadicParsing m => m String
- operatorFC :: MonadicParsing m => m (String, FC)
- fileName :: Delta -> String
- lineNum :: Delta -> Int
- columnNum :: Delta -> Int
- getFC :: MonadicParsing m => m FC
- bindList :: (Name -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PTerm -> PTerm
- commaSeparated :: MonadicParsing m => m a -> m [a]
- pushIndent :: IdrisParser ()
- popIndent :: IdrisParser ()
- indent :: IdrisParser Int
- lastIndent :: IdrisParser Int
- indented :: IdrisParser a -> IdrisParser a
- indentedBlock :: IdrisParser a -> IdrisParser [a]
- indentedBlock1 :: IdrisParser a -> IdrisParser [a]
- indentedBlockS :: IdrisParser a -> IdrisParser a
- lookAheadMatches :: MonadicParsing m => m a -> m Bool
- openBlock :: IdrisParser ()
- closeBlock :: IdrisParser ()
- terminator :: IdrisParser ()
- keepTerminator :: IdrisParser ()
- notEndApp :: IdrisParser ()
- notEndBlock :: IdrisParser ()
- data IndentProperty = IndentProperty (Int -> Int -> Bool) String
- indentPropHolds :: IndentProperty -> IdrisParser ()
- gtProp :: IndentProperty
- gteProp :: IndentProperty
- eqProp :: IndentProperty
- ltProp :: IndentProperty
- lteProp :: IndentProperty
- notOpenBraces :: IdrisParser ()
- accessibility' :: IdrisParser Accessibility
- accessibility :: IdrisParser Accessibility
- addAcc :: Name -> Accessibility -> IdrisParser ()
- accData :: Accessibility -> Name -> [Name] -> IdrisParser ()
- fixErrorMsg :: String -> [String] -> String
- collect :: [PDecl] -> [PDecl]
Documentation
type IdrisParser = StateT IState IdrisInnerParser Source #
Idris parser with state used during parsing
newtype IdrisInnerParser a Source #
type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m) Source #
Generalized monadic parsing constraint type
class HasLastTokenSpan m where Source #
getLastTokenSpan :: m (Maybe FC) Source #
runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Result res Source #
Helper to run Idris inner parser based stateT parsers
highlightP :: FC -> OutputAnnotation -> IdrisParser () Source #
noDocCommentHere :: String -> IdrisParser () Source #
clearParserWarnings :: Idris () Source #
reportParserWarnings :: Idris () Source #
parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser () Source #
Space, comments and literals (token/lexing like parsers)
simpleWhiteSpace :: MonadicParsing m => m () Source #
Consumes any simple whitespace (any character which satisfies Char.isSpace)
eol :: MonadicParsing m => m () Source #
A parser that succeeds at the end of the line
singleLineComment :: MonadicParsing m => m () Source #
Consumes a single-line comment
SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;
multiLineComment :: MonadicParsing m => m () Source #
Consumes a multi-line comment
MultiLineComment_t ::= '{ -- }' | '{ -' InCommentChars_t ;
InCommentChars_t ::= '- }' | MultiLineComment_t InCommentChars_t | ~'- }'+ InCommentChars_t ;
docComment :: IdrisParser (Docstring (), [(Name, Docstring ())]) Source #
Parses a documentation comment
DocComment_t ::= |||
~EOL_t* EOL_t
;
whiteSpace :: MonadicParsing m => m () Source #
Parses some white space
stringLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) Source #
Parses a string literal
charLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (Char, FC) Source #
Parses a char literal
natural :: (MonadicParsing m, HasLastTokenSpan m) => m (Integer, FC) Source #
Parses a natural number
integer :: MonadicParsing m => m Integer Source #
Parses an integral number
float :: (MonadicParsing m, HasLastTokenSpan m) => m (Double, FC) Source #
Parses a floating point number
Symbols, identifiers, names and operators
idrisStyle :: MonadicParsing m => IdentifierStyle m Source #
Idris Style for parsing identifiers/reserved keywords
lcharFC :: MonadicParsing m => Char -> m FC Source #
Parses a character as a token, returning the source span of the character
reserved :: MonadicParsing m => String -> m () Source #
Parses a reserved identifier
reservedFC :: MonadicParsing m => String -> m FC Source #
Parses a reserved identifier, computing its span. Assumes that reserved identifiers never contain line breaks.
reservedHL :: String -> IdrisParser () Source #
Parse a reserved identfier, highlighting its span as a keyword
reservedOp :: MonadicParsing m => String -> m () Source #
Parses a reserved operator
reservedOpFC :: MonadicParsing m => String -> m FC Source #
identifier :: MonadicParsing m => m (String, FC) Source #
Parses an identifier as a token
iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC) Source #
Parses an identifier with possible namespace as a name
maybeWithNS :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) -> Bool -> [String] -> m (Name, FC) Source #
Parses an string possibly prefixed by a namespace
initsEndAt :: (a -> Bool) -> [a] -> [[a]] Source #
List of all initial segments in ascending order of a list. Every such initial segment ends right before an element satisfying the given condition.
mkName :: (String, String) -> Name Source #
Create a Name
from a pair of strings representing a base name and its
namespace.
operatorLetter :: MonadicParsing m => m Char Source #
commentMarkers :: [String] Source #
invalidOperators :: [String] Source #
operator :: MonadicParsing m => m String Source #
Parses an operator
operatorFC :: MonadicParsing m => m (String, FC) Source #
Parses an operator
Position helpers
fileName :: Delta -> String Source #
Get filename from position (returns "(interactive)" when no source file is given)
getFC :: MonadicParsing m => m FC Source #
Get file position as FC
Syntax helpers
bindList :: (Name -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PTerm -> PTerm Source #
Bind constraints to term
commaSeparated :: MonadicParsing m => m a -> m [a] Source #
commaSeparated p
parses one or more occurences of p
,
separated by commas and optional whitespace.
Layout helpers
pushIndent :: IdrisParser () Source #
Push indentation to stack
popIndent :: IdrisParser () Source #
Pops indentation from stack
indent :: IdrisParser Int Source #
Gets current indentation
lastIndent :: IdrisParser Int Source #
Gets last indentation
indented :: IdrisParser a -> IdrisParser a Source #
Applies parser in an indented position
indentedBlock :: IdrisParser a -> IdrisParser [a] Source #
Applies parser to get a block (which has possibly indented statements)
indentedBlock1 :: IdrisParser a -> IdrisParser [a] Source #
Applies parser to get a block with at least one statement (which has possibly indented statements)
indentedBlockS :: IdrisParser a -> IdrisParser a Source #
Applies parser to get a block with exactly one (possibly indented) statement
lookAheadMatches :: MonadicParsing m => m a -> m Bool Source #
Checks if the following character matches provided parser
openBlock :: IdrisParser () Source #
Parses a start of block
closeBlock :: IdrisParser () Source #
Parses an end of block
terminator :: IdrisParser () Source #
Parses a terminator
keepTerminator :: IdrisParser () Source #
Parses and keeps a terminator
notEndApp :: IdrisParser () Source #
Checks if application expression does not end
notEndBlock :: IdrisParser () Source #
Checks that it is not end of block
data IndentProperty Source #
Representation of an operation that can compare the current indentation with the last indentation, and an error message if it fails
IndentProperty (Int -> Int -> Bool) String |
indentPropHolds :: IndentProperty -> IdrisParser () Source #
Allows comparison of indent, and fails if property doesn't hold
gtProp :: IndentProperty Source #
Greater-than indent property
gteProp :: IndentProperty Source #
Greater-than or equal to indent property
eqProp :: IndentProperty Source #
Equal indent property
ltProp :: IndentProperty Source #
Less-than indent property
lteProp :: IndentProperty Source #
Less-than or equal to indent property
notOpenBraces :: IdrisParser () Source #
Checks that there are no braces that are not closed
accessibility' :: IdrisParser Accessibility Source #
Parses an accessibilty modifier (e.g. public, private)
addAcc :: Name -> Accessibility -> IdrisParser () Source #
Adds accessibility option for function
accData :: Accessibility -> Name -> [Name] -> IdrisParser () Source #
Add accessbility option for data declarations
(works for classes too - abstract
means the data/class is visible but members not)