Idris.ParseHelpers

Documentation

type IdrisParser = StateT IState IdrisInnerParser

Idris parser with state used during parsing

newtype IdrisInnerParser a

Constructors

IdrisInnerParser

Fields

runInnerParser :: Parser a

Instances

Monad IdrisInnerParser

Functor IdrisInnerParser

MonadPlus IdrisInnerParser

Applicative IdrisInnerParser

Alternative IdrisInnerParser

TokenParsing IdrisInnerParser

CharParsing IdrisInnerParser

LookAheadParsing IdrisInnerParser

Parsing IdrisInnerParser

DeltaParsing IdrisInnerParser

MarkParsing Delta IdrisInnerParser

Monoid a => Monoid (IdrisInnerParser a)

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

Generalized monadic parsing constraint type

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

Helper to run Idris inner parser based stateT parsers

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

simpleWhiteSpace :: MonadicParsing m => m ()

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

isEol :: Char -> Bool

Checks if a charcter is end of line

eol :: MonadicParsing m => m ()

isDocCommentMarker :: Char -> Bool

Checks if a character is a documentation comment marker

singleLineComment :: MonadicParsing m => m ()

Consumes a single-line comment

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

multiLineComment :: MonadicParsing m => m ()

Consumes a multi-line comment

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

  InCommentChars_t ::=
   '- }'
   | MultiLineComment_t InCommentChars_t
   | ~'- }'+ InCommentChars_t
  ;

docComment :: MonadicParsing m => Char -> m String

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

  DocComment_t ::=   '--' DocCommentMarker_t ~EOL_t* EOL_t
                  | '{ -' DocCommentMarket_t ~'- }'* '- }'
                 ;

whiteSpace :: MonadicParsing m => m ()

Parses some white space

stringLiteral :: MonadicParsing m => m String

Parses a string literal

charLiteral :: MonadicParsing m => m Char

 Parses a char literal

natural :: MonadicParsing m => m Integer

Parses a natural number

integer :: MonadicParsing m => m Integer

Parses an integral number

float :: MonadicParsing m => m Double

Parses a floating point number

Symbols, identifiers, names and operators

idrisStyle :: MonadicParsing m => IdentifierStyle m

Idris Style for parsing identifiers/reserved keywords

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

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

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

Parses a character as a token

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

Parses string as a token

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

Parses a reserved identifier

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

Parses a reserved operator

identifier :: MonadicParsing m => m String

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

Parses an identifier with possible namespace as a name

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

Parses an string possibly prefixed by a namespace

name :: IdrisParser Name

Parses a name

initsEndAt :: (a -> Bool) -> [a] -> [[a]]

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

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

opChars :: String

operatorLetter :: MonadicParsing m => m Char

operator :: MonadicParsing m => m String

Parses an operator

Position helpers

fileName :: Delta -> String

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

lineNum :: Delta -> Int

Get line number from position

columnNum :: Delta -> Int

Get column number from position

getFC :: MonadicParsing m => m FC

Get file position as FC

Syntax helpers

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

Bind constraints to term

Layout helpers

pushIndent :: IdrisParser ()

Push indentation to stack

popIndent :: IdrisParser ()

Pops indentation from stack

indent :: IdrisParser Int

Gets current indentation

lastIndent :: IdrisParser Int

Gets last indentation

indented :: IdrisParser a -> IdrisParser a

Applies parser in an indented position

indentedBlock :: IdrisParser a -> IdrisParser [a]

Applies parser to get a block (which has possibly indented statements)

indentedBlock1 :: IdrisParser a -> IdrisParser [a]

Applies parser to get a block with at least one statement (which has possibly indented statements)

indentedBlockS :: IdrisParser a -> IdrisParser a

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

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

Checks if the following character matches provided parser

openBlock :: IdrisParser ()

Parses a start of block

closeBlock :: IdrisParser ()

Parses an end of block

terminator :: IdrisParser ()

Parses a terminator

keepTerminator :: IdrisParser ()

Parses and keeps a terminator

notEndApp :: IdrisParser ()

Checks if application expression does not end

notEndBlock :: IdrisParser ()

Checks that it is not end of block

data IndentProperty

Representation of an operation that can compare the current indentation with the last indentation, and an error message if it fails

Constructors

IndentProperty (Int -> Int -> Bool) String

indentPropHolds :: IndentProperty -> IdrisParser ()

Allows comparison of indent, and fails if property doesn't hold

gtProp :: IndentProperty

Greater-than indent property

gteProp :: IndentProperty

Greater-than or equal to indent property

eqProp :: IndentProperty

Equal indent property

ltProp :: IndentProperty

Less-than indent property

lteProp :: IndentProperty

Less-than or equal to indent property

notOpenBraces :: IdrisParser ()

Checks that there are no braces that are not closed

accessibility :: IdrisParser Accessibility

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

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

Adds accessibility option for function

accData :: Maybe Accessibility -> Name -> [Name] -> IdrisParser ()

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] -> String

Error message with possible fixes list

collect :: [PDecl] -> [PDecl]

Collect PClauses with the same function name