Agda-2.2.10: A dependently typed functional programming language and proof assistant




This module defines the things required by Alex and some other Alex related things.


Alex requirements

data AlexInput Source

This is what the lexer manipulates.




lexPos :: !Position

current position

lexInput :: String

current input

lexPrevChar :: !Char

previously read character

alexInputPrevChar :: AlexInput -> CharSource

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

alexGetChar :: AlexInput -> Maybe (Char, AlexInput)Source

Lex a character. No surprises.

Lex actions

type LexAction r = PreviousInput -> CurrentInput -> TokenLength -> Parser rSource

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

type LexPredicate = ([LexState], ParseFlags) -> PreviousInput -> TokenLength -> CurrentInput -> BoolSource

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.

Monad operations