A class to parse symbols

liquid-fixpoint parses Symbol and LiquidHaskell instantiates this to LocSymbol for more precise error messages. If liquid-fixpoint is adapted to parse names as LocSymbol as well, this class can be eliminated.

Parser that consumes the given reserved word.

The input token cannot be longer than the given name.

NOTE: we currently don't double-check that the reserved word is in the list of reserved words.

Parser that consumes the given reserved operator.

The input token cannot be longer than the given name.

NOTE: we currently don't double-check that the reserved operator is in the list of reserved operators.

Parser that consumes the given symbol.

The difference with reservedOp is that the given symbol is seen as a token of its own, so the next character that follows does not matter.

symbol :: String -> Parser String symbol x = L.symbol spaces (string x)

Parser that consumes the given symbol.

The difference with reservedOp is that the given symbol is seen as a token of its own, so the next character that follows does not matter.

symbol :: String -> Parser String symbol x = L.symbol spaces (string x)

Parser that consumes the given symbol.

The difference with reservedOp is that the given symbol is seen as a token of its own, so the next character that follows does not matter.

symbol :: String -> Parser String symbol x = L.symbol spaces (string x)

Parser that consumes the given symbol.

The difference with reservedOp is that the given symbol is seen as a token of its own, so the next character that follows does not matter.

symbol :: String -> Parser String symbol x = L.symbol spaces (string x)

Parses a string literal as a lexeme. This is based on megaparsec's charLiteral parser, which claims to handle all the single-character escapes defined by the Haskell grammar.

Symbolic lexeme. Stands on its own.

Lexeme version of lowerIdR.

Raw parser for an identifier starting with a lowercase letter.

See Note [symChars].

Lexeme version of upperIdR.

Raw parser for an identifier starting with an uppercase letter.

See Note [symChars].

Unconstrained identifier, lower- or uppercase.

Must not be a reserved word.

Lexeme version of symbolR.

Raw parser for an identifier starting with any letter.

See Note [symChars].

Parser for literal numeric constants: floats or integers without sign.

Consumes a natural number literal lexeme, which can be in decimal, octal and hexadecimal representation.

This does not parse negative integers. Unary minus is available as an operator in the expression language.

Binder (lowerIdP <* colon)

Parser for sorts (types).

constructing qualifiers

Parses any of the known infix operators.

Located version of infixSymbolP.

Expressions

Parses a predicate.

Unlike for expressions, there is a built-in operator list.

Parser for function applications.

Andres, TODO: Why is this so complicated?

Parsing Qualifiers --------------------------------------------------------

Qualifiers

BareTypes -----------------------------------------------------------------

Refa

(Sorted) Refinements

(Sorted) Refinements with default binder

(Sorted) Refinements with configurable sub-parsers

Parse a block delimited by layout. The block must be indented more than the surrounding blocks, otherwise we return an empty list.

Assumes that the parser for items does not accept the empty string.

Parse a single line that may be continued via layout.

Parse a block of items which can be delimited either via layout or via explicit delimiters as specified.

Assumes that the parser for items does not accept the empty string.

Parse a block of items that are delimited via explicit delimiters. Layout is disabled/reset for the scope of this block.

Parses a block with explicit braces and commas as separator. Used for record constructors in datatypes.

Parses a block via layout or explicit braces and semicolons.

Assumes that the parser for items does not accept the empty string.

However, even in layouted mode, we are allowing semicolons to separate block contents. We also allow semicolons at the beginning, end, and multiple subsequent semicolons, so the resulting parser provides the illusion of allowing empty items.

Consumes all whitespace, including LH comments.

Should not be used directly, but primarily via lexeme.

The only "valid" use case for spaces is in top-level parsing function, to consume initial spaces.

Start a new layout block at the current indentation level.

Remove the topmost element from the layout stack.

Raw (non-whitespace) parser for an identifier adhering to certain conditions.

The arguments are as follows, in order:

• the parser for the initial character,
• a predicate indicating which subsequent characters are ok,
• a check for the entire identifier to be applied in the end,
• an error message to display if the final check fails.

Indentation-aware lexeme parser. Before parsing, establishes whether we are in a position permitted by the layout stack. After the token, consume whitespace and potentially change state.

Make a parser location-aware.

This is at the cost of an imprecise span because we still consume spaces in the end first.

Indentation-aware located lexeme parser.

This is defined in such a way that it determines the actual source range covered by the identifier. I.e., it consumes additional whitespace in the end, but that is not part of the source range reported for the identifier.

Obtain a fresh integer during the parsing process.

Entry point for parsing, for testing.

Take the top-level parser, the source file name, and the input as a string. Fails with an exception on a parse error.

Function to test parsers interactively.

Parse via the given parser, and obtain the rest of the input as well as the final source position.

Predicate version to check if the characer is a valid initial character for lowerIdR.

TODO: What is this needed for?

Initial parser state.

The parser state.

We keep track of the fixities of infix operators.

We also keep track of whether empty list and singleton lists syntax is allowed (and how they are to be interpreted, if they are).

We also keep track of an integer counter that can be used to supply unique integers during the parsing process.

Finally, we keep track of the layout stack.

The layout stack tracks columns at which layout blocks have started.

Add an operator to the parsing state.

Add a new numeric FTyCon (symbol) to the parsing state.

Parser for "atomic" expressions.

This parser is reused by Liquid Haskell.

Parsing Data Declarations -------------------------------------------------

Parser for the reserved constant "true".

Parser for the reserved constant "false".

Parser for literal string contants.