Idris parser with state used during parsing

Generalized monadic parsing constraint type

Helper to run Idris inner parser based stateT parsers

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

Checks if a charcter is end of line

A parser that succeeds at the end of the line

Consumes a single-line comment

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

Consumes a multi-line comment

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

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

Parses a documentation comment

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

Parses some white space

Parses a string literal

Parses a char literal

Parses a natural number

Parses an integral number

Parses a floating point number

Idris Style for parsing identifiers/reserved keywords

Parses a character as a token

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

Parses string as a token

Parses a reserved identifier

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

Parse a reserved identfier, highlighting its span as a keyword

Parses a reserved operator

Parses an identifier as a token

Parses an identifier with possible namespace as a name

Parses an string possibly prefixed by a namespace

Parses a name

List of all initial segments in ascending order of a list. Every such initial segment ends right before an element satisfying the given condition.

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

Parses an operator

Parses an operator

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

Get line number from position

Get column number from position

Get file position as FC

Bind constraints to term

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

Push indentation to stack

Pops indentation from stack

Gets current indentation

Gets last indentation

Applies parser in an indented position

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

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

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

Checks if the following character matches provided parser

Parses a start of block

Parses an end of block

Parses a terminator

Parses and keeps a terminator

Checks if application expression does not end

Checks that it is not end of block

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

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

Greater-than indent property

Greater-than or equal to indent property

Equal indent property

Less-than indent property

Less-than or equal to indent property

Checks that there are no braces that are not closed

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

Adds accessibility option for function

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

Error message with possible fixes list

Collect PClauses with the same function name