Idris.Parser.Helpers

Documentation

module Idris.Parser.Stack

The parser

type IdrisParser = Parser IState

Idris parser with state used during parsing

parseErrorDoc :: ParseError -> Doc

Space

whiteSpace :: Parsing m => m ()

Parses some white space

someSpace :: Parsing m => m ()

eol :: Parsing m => m ()

A parser that succeeds at the end of the line

isEol :: Char -> Bool

Checks if a charcter is end of line

Basic parsers

char :: Parsing m => Char -> m Char

symbol :: Parsing m => String -> m ()

string :: Parsing m => String -> m String

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

Checks if the following character matches provided parser

Terminals

lchar :: Parsing m => Char -> m Char

Parses a character as a token

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

Parses a reserved identifier

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

Parses a documentation comment

  DocComment_t ::= DocCommentLine (ArgCommentLine DocCommentLine*)* ;

  DocCommentLine ::= ||| ~EOL_t* EOL_t ;
  ArgCommentLine ::= ||| '@' ~EOL_t* EOL_t ;

token :: Parsing m => m a -> m a

natural :: Parsing m => m Integer

Parses a natural number

charLiteral :: Parsing m => m Char

Parses a char literal

stringLiteral :: Parsing m => m String

Parses a string literal

float :: Parsing m => m Double

Parses a floating point number

Names

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

Bind constraints to term

maybeWithNS :: Parsing m => m String -> [String] -> m Name

Parses an string possibly prefixed by a namespace

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

Parses an identifier with possible namespace as a name

name :: (Parsing m, MonadState IState m) => m Name

Parses a name

identifier :: Parsing m => m String

identifierWithExtraChars :: Parsing m => String -> m String

Parses an identifier as a token

packageName :: Parsing m => m String

Parse a package name

Access

accessibility :: IdrisParser Accessibility

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

Add accessbility option for data declarations (works for interfaces too - abstract means the data/interface is visible but members not)

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

Adds accessibility option for function

Warnings and errors

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

Error message with possible fixes list

parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()

clearParserWarnings :: Idris ()

reportParserWarnings :: Idris ()

Highlighting

highlight :: (MonadState IState m, Parsing m) => OutputAnnotation -> m a -> m a

keyword :: (Parsing m, MonadState IState m) => String -> m ()

Parse a reserved identfier, highlighting it as a keyword

Indentation

pushIndent :: IdrisParser ()

Push indentation to stack

popIndent :: IdrisParser ()

Pops indentation from stack

indentGt :: (Parsing m, MonadState IState m) => m ()

notOpenBraces :: IdrisParser ()

Checks that there are no braces that are not closed

Indented blocks

openBlock :: IdrisParser ()

Parses a start of block

closeBlock :: IdrisParser ()

Parses an end of block

terminator :: IdrisParser ()

Parses a terminator

notEndBlock :: IdrisParser ()

Checks that it is not end of block

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

indented :: IdrisParser a -> IdrisParser a

Applies parser in an indented position

Miscellaneous

notEndApp :: IdrisParser ()

Checks if application expression does not end

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

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