Agda.Syntax.Parser.Alex

This is what the lexer manipulates.

A lens for lexInput.

Get the previously lexed character. Same as lexPrevChar. Alex needs this to be defined to handle "patterns with a left-context".

Returns the next character, and updates the AlexInput value.

This function is not suitable for use by Alex 2, because it can return non-ASCII characters.

Returns the next byte, and updates the AlexInput value.

A trick is used to handle the fact that there are more than 256 Unicode code points. The function translates characters to bytes in the following way:

• Whitespace characters other than '\t' and '\n' are translated to ' '.

• Non-ASCII alphabetical characters are translated to 'z'.

• Other non-ASCII printable characters are translated to '+'.

• Everything else is translated to '\1'.

Note that it is important that there are no keywords containing 'z', '+', ' ' or '\1'.

This function is used by Alex (version 3).

In the lexer, regular expressions are associated with lex actions who's task it is to construct the tokens.

Sometimes regular expressions aren't enough. Alex provides a way to do arbitrary computations to see if the input matches. This is done with a lex predicate.

Conjunction of LexPredicates.

Disjunction of LexPredicates.

Negation of LexPredicates.