The parse monad.

The result of parsing something.

The parser state. Contains everything the parser and the lexer could ever need.

Parse errors: what you get if parsing fails.

Warnings for parsing.

For context sensitive lexing alex provides what is called start codes in the Alex documentation. It is really an integer representing the state of the lexer, so we call it LexState instead.

We need to keep track of the context to do layout. The context specifies the indentation columns of the open layout blocks. See Agda.Syntax.Parser.Layout for more informaton.

The stack of layout blocks.

When we encounter a layout keyword, we push a Tentative block with noColumn. This is replaced by aproper column once we reach the next token.

Status of a layout column (see #1145). A layout column is Tentative until we encounter a new line. This allows stacking of layout keywords.

Inside a LayoutContext the sequence of Confirmed columns needs to be strictly increasing. 'Tentative columns between Confirmed columns need to be strictly increasing as well.

A (layout) column.

Parser flags.

Constructs the initial state of the parser. The string argument is the input string, the file path is only there because it's part of a position.

The default flags.

The most general way of parsing a string. The Agda.Syntax.Parser will define more specialised functions that supply the ParseFlags and the LexState.

The even more general way of parsing a string.

Parses a string as if it were the contents of the given file Useful for integrating preprocessors.

The parse interval is between the last position and the current position.

Return the current layout block.

When we see a layout keyword, by default we expect a Tentative block.

Records a warning.

Throw a parse error at the current position.

Fake a parse error at the specified position. Used, for instance, when lexing nested comments, which when failing will always fail at the end of the file. A more informative position is the beginning of the failing comment.

Use parseErrorAt or parseError as appropriate.

Report a parse error at the beginning of the given Range.

For lexical errors we want to report the current position as the site of the error, whereas for parse errors the previous position is the one we're interested in (since this will be the position of the token we just lexed). This function does parseErrorAt the current position.