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

Agda.Syntax.Parser.Alex

Contents

Description

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

Synopsis

Alex requirements

data AlexInput Source

This is what the lexer manipulates.

Constructors

AlexInput 

Fields

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