idris-0.9.15: Functional Programming Language with Dependent Types

Safe HaskellNone





type IdrisParser = StateT IState IdrisInnerParserSource

Idris parser with state used during parsing

type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)Source

Generalized monadic parsing constraint type

runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Result resSource

Helper to run Idris inner parser based stateT parsers

Space, comments and literals (token/lexing like parsers)

simpleWhiteSpace :: MonadicParsing m => m ()Source

Consumes any simple whitespace (any character which satisfies Char.isSpace)

isEol :: Char -> BoolSource

Checks if a charcter is end of line

singleLineComment :: MonadicParsing m => m ()Source

Consumes a single-line comment

     SingleLineComment_t ::= '--' EOL_t
                        |     '--' ~DocCommentMarker_t ~EOL_t* EOL_t

multiLineComment :: MonadicParsing m => m ()Source

Consumes a multi-line comment

  MultiLineComment_t ::=
     '{ -- }'
   | '{ -' ~DocCommentMarker_t InCommentChars_t
  InCommentChars_t ::=
   '- }'
   | MultiLineComment_t InCommentChars_t
   | ~'- }'+ InCommentChars_t

docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])Source

Parses a documentation comment (similar to haddock) given a marker character

  DocComment_t ::=   ||| ~EOL_t* EOL_t

whiteSpace :: MonadicParsing m => m ()Source

Parses some white space

stringLiteral :: MonadicParsing m => m StringSource

Parses a string literal

natural :: MonadicParsing m => m IntegerSource

Parses a natural number

integer :: MonadicParsing m => m IntegerSource

Parses an integral number

float :: MonadicParsing m => m DoubleSource

Parses a floating point number

Symbols, identifiers, names and operators

idrisStyle :: MonadicParsing m => IdentifierStyle mSource

Idris Style for parsing identifiers/reserved keywords

char :: MonadicParsing m => Char -> m CharSource

string :: MonadicParsing m => String -> m StringSource

lchar :: MonadicParsing m => Char -> m CharSource

Parses a character as a token

symbol :: MonadicParsing m => String -> m StringSource

Parses string as a token

reserved :: MonadicParsing m => String -> m ()Source

Parses a reserved identifier

reservedOp :: MonadicParsing m => String -> m ()Source

Parses a reserved operator

iName :: MonadicParsing m => [String] -> m NameSource

Parses an identifier with possible namespace as a name

maybeWithNS :: MonadicParsing m => m String -> Bool -> [String] -> m NameSource

Parses an string possibly prefixed by a namespace

name :: IdrisParser NameSource

Parses a name

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) -> NameSource

Create a Name from a pair of strings representing a base name and its namespace.

opChars :: StringSource

operator :: MonadicParsing m => m StringSource

Parses an operator

Position helpers

fileName :: Delta -> StringSource

Get filename from position (returns (interactive) when no source file is given)

lineNum :: Delta -> IntSource

Get line number from position

columnNum :: Delta -> IntSource

Get column number from position

getFC :: MonadicParsing m => m FCSource

Get file position as FC

Syntax helpers

bindList :: (Name -> PTerm -> PTerm -> PTerm) -> [(Name, PTerm)] -> PTerm -> PTermSource

Bind constraints to term

Layout helpers

pushIndent :: IdrisParser ()Source

Push indentation to stack

popIndent :: IdrisParser ()Source

Pops indentation from stack

indent :: IdrisParser IntSource

Gets current indentation

lastIndent :: IdrisParser IntSource

Gets last indentation

indented :: IdrisParser a -> IdrisParser aSource

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 aSource

Applies parser to get a block with exactly one (possibly indented) statement

lookAheadMatches :: MonadicParsing m => m a -> m BoolSource

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 :: IndentPropertySource

Greater-than indent property

gteProp :: IndentPropertySource

Greater-than or equal to indent property

eqProp :: IndentPropertySource

Equal indent property

ltProp :: IndentPropertySource

Less-than indent property

lteProp :: IndentPropertySource

Less-than or equal to indent property

notOpenBraces :: IdrisParser ()Source

Checks that there are no braces that are not closed

accessibility :: IdrisParser AccessibilitySource

Parses an accessibilty modifier (e.g. public, private)

addAcc :: Name -> Maybe Accessibility -> IdrisParser ()Source

Adds accessibility option for function

accData :: Maybe 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)

Error reporting helpers

fixErrorMsg :: String -> [String] -> StringSource

Error message with possible fixes list

collect :: [PDecl] -> [PDecl]Source

Collect PClauses with the same function name