Safe Haskell	None

Idris.ParseHelpers

Contents

Space, comments and literals (token/lexing like parsers)
Symbols, identifiers, names and operators
Position helpers
Syntax helpers
Layout helpers
Error reporting helpers

Synopsis

Documentation

type IdrisParser = StateT IState IdrisInnerParser Source

Idris parser with state used during parsing

newtype IdrisInnerParser a Source

Constructors

IdrisInnerParser
Fields runInnerParser :: Parser a

Instances

Monad IdrisInnerParser
Functor IdrisInnerParser
MonadPlus IdrisInnerParser
Applicative IdrisInnerParser
Alternative IdrisInnerParser
DeltaParsing IdrisInnerParser
TokenParsing IdrisInnerParser
Parsing IdrisInnerParser
CharParsing IdrisInnerParser
LookAheadParsing IdrisInnerParser
MarkParsing Delta IdrisInnerParser
Monoid (IdrisInnerParser a)

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 -> Bool Source

Checks if a charcter is end of line

eol :: MonadicParsing m => m ()Source

isDocCommentMarker :: Char -> Bool Source

Checks if a character is a documentation comment marker

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 :: MonadicParsing m => Char -> m String Source

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 ()Source

Parses some white space

stringLiteral :: MonadicParsing m => m String Source

Parses a string literal

charLiteral :: MonadicParsing m => m Char Source

Parses a char literal

natural :: MonadicParsing m => m Integer Source

Parses a natural number

integer :: MonadicParsing m => m Integer Source

Parses an integral number

float :: MonadicParsing m => m Double Source

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 Char Source

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

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

Parses a character as a token

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

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

identifier :: MonadicParsing m => m String Source

Parses an identifier as a token

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

Parses an identifier with possible namespace as a name

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

Parses an string possibly prefixed by a namespace

name :: IdrisParser Name Source

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) -> Name Source

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

opChars :: String Source

operatorLetter :: MonadicParsing m => m Char Source

operator :: MonadicParsing m => m String Source

Parses an operator

Position helpers

fileName :: Delta -> String Source

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

lineNum :: Delta -> Int Source

Get line number from position

columnNum :: Delta -> Int Source

Get column number from position

getFC :: MonadicParsing m => m FC Source

Get file position as FC

Syntax helpers

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

Bind constraints to term

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

Constructors

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

Error message with possible fixes list

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

Collect PClauses with the same function name