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

Applicative IdrisInnerParser

Alternative IdrisInnerParser

MonadPlus IdrisInnerParser

TokenParsing IdrisInnerParser

TokenParsing IdrisParser

CharParsing IdrisInnerParser

LookAheadParsing IdrisInnerParser

Parsing IdrisInnerParser

DeltaParsing IdrisInnerParser

HasLastTokenSpan IdrisParser

MarkParsing Delta IdrisInnerParser

Monoid a => Monoid (IdrisInnerParser a)

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

Generalized monadic parsing constraint type

class HasLastTokenSpan m where

Methods

getLastTokenSpan :: m (Maybe FC)

Instances

HasLastTokenSpan IdrisParser

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

Helper to run Idris inner parser based stateT parsers

highlightP :: FC -> OutputAnnotation -> IdrisParser ()

noDocCommentHere :: String -> IdrisParser ()

clearParserWarnings :: Idris ()

reportParserWarnings :: Idris ()

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

A parser that succeeds at the end of the line

singleLineComment :: MonadicParsing m => m ()

Consumes a single-line comment

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

multiLineComment :: MonadicParsing m => m ()

Consumes a multi-line comment

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

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

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

Parses a documentation comment

  DocComment_t ::=   ||| ~EOL_t* EOL_t
                 ;

whiteSpace :: MonadicParsing m => m ()

Parses some white space

stringLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC)

Parses a string literal

charLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (Char, FC)

Parses a char literal

natural :: (MonadicParsing m, HasLastTokenSpan m) => m (Integer, FC)

Parses a natural number

integer :: MonadicParsing m => m Integer

Parses an integral number

float :: (MonadicParsing m, HasLastTokenSpan m) => m (Double, FC)

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

lcharFC :: MonadicParsing m => Char -> m FC

Parses a character as a token, returning the source span of the character

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

Parses string as a token

symbolFC :: MonadicParsing m => String -> m FC

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

Parses a reserved identifier

reservedFC :: MonadicParsing m => String -> m FC

Parses a reserved identifier, computing its span. Assumes that reserved identifiers never contain line breaks.

reservedHL :: String -> IdrisParser ()

Parse a reserved identfier, highlighting its span as a keyword

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

Parses a reserved operator

reservedOpFC :: MonadicParsing m => String -> m FC

identifier :: MonadicParsing m => m (String, FC)

Parses an identifier as a token

iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)

Parses an identifier with possible namespace as a name

maybeWithNS :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)

Parses an string possibly prefixed by a namespace

name :: IdrisParser (Name, FC)

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

commentMarkers :: [String]

invalidOperators :: [String]

operator :: MonadicParsing m => m String

Parses an operator

operatorFC :: MonadicParsing m => m (String, FC)

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 -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PTerm -> PTerm

Bind constraints to term

commaSeparated :: MonadicParsing m => m a -> m [a]

commaSeparated p parses one or more occurences of p, separated by commas and optional whitespace.

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