idris-1.3.0: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Parser.Helpers

Contents

Description

 

Synopsis

Documentation

The parser

type IdrisParser = Parser IState Source #

Idris parser with state used during parsing

Space

whiteSpace :: Parsing m => m () Source #

Parses some white space

someSpace :: Parsing m => m () Source #

eol :: Parsing m => m () Source #

A parser that succeeds at the end of the line

isEol :: Char -> Bool Source #

Checks if a charcter is end of line

Basic parsers

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

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

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

Checks if the following character matches provided parser

Terminals

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

Parses a character as a token

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

Parses a reserved identifier

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

Parses a documentation comment

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

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

natural :: Parsing m => m Integer Source #

Parses a natural number

charLiteral :: Parsing m => m Char Source #

Parses a char literal

stringLiteral :: Parsing m => m String Source #

Parses a string literal

float :: Parsing m => m Double Source #

Parses a floating point number

Names

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

Bind constraints to term

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

Parses an string possibly prefixed by a namespace

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

Parses an identifier with possible namespace as a name

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

Parses a name

identifier :: Parsing m => m String Source #

Parses an identifier as a token

packageName :: Parsing m => m String Source #

Parse a package name

Access

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

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

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

Adds accessibility option for function

Warnings and errors

fixErrorMsg :: String -> [String] -> String Source #

Error message with possible fixes list

Highlighting

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

Parse a reserved identfier, highlighting it as a keyword

Indentation

pushIndent :: IdrisParser () Source #

Push indentation to stack

popIndent :: IdrisParser () Source #

Pops indentation from stack

notOpenBraces :: IdrisParser () Source #

Checks that there are no braces that are not closed

Indented blocks

openBlock :: IdrisParser () Source #

Parses a start of block

closeBlock :: IdrisParser () Source #

Parses an end of block

terminator :: IdrisParser () Source #

Parses a terminator

notEndBlock :: IdrisParser () Source #

Checks that it is not end of block

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 a Source #

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

indented :: IdrisParser a -> IdrisParser a Source #

Applies parser in an indented position

Miscellaneous

notEndApp :: IdrisParser () Source #

Checks if application expression does not end

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

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