Agda.Syntax.Parser.Alex

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

Alex requirements

data AlexInput

This is what the lexer manipulates.

Constructors

AlexInput

Fields

• lexSrcFile :: !SrcFile

  File.

• lexPos :: !PositionWithoutFile

  Current position.

• lexInput :: String

  Current input.

• lexPrevChar :: !Char

  Previously read character.

lensLexInput :: Lens' String AlexInput

A lens for lexInput.

alexInputPrevChar :: AlexInput -> Char

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)

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.

alexGetByte :: AlexInput -> Maybe (Word8, AlexInput)

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).

Lex actions

newtype LexAction r

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

Constructors

LexAction

Fields

• runLexAction :: PreviousInput -> CurrentInput -> TokenLength -> Parser r

Instances

Applicative LexAction

Defined in Agda.Syntax.Parser.Alex

Methods

pure :: a -> LexAction a

(<*>) :: LexAction (a -> b) -> LexAction a -> LexAction b

liftA2 :: (a -> b -> c) -> LexAction a -> LexAction b -> LexAction c

(*>) :: LexAction a -> LexAction b -> LexAction b

(<*) :: LexAction a -> LexAction b -> LexAction a

Functor LexAction

Defined in Agda.Syntax.Parser.Alex

Methods

fmap :: (a -> b) -> LexAction a -> LexAction b

(<$) :: a -> LexAction b -> LexAction a

Monad LexAction

Defined in Agda.Syntax.Parser.Alex

Methods

(>>=) :: LexAction a -> (a -> LexAction b) -> LexAction b

(>>) :: LexAction a -> LexAction b -> LexAction b

return :: a -> LexAction a

MonadState ParseState LexAction

Defined in Agda.Syntax.Parser.Alex

Methods

get :: LexAction ParseState

put :: ParseState -> LexAction ()

state :: (ParseState -> (a, ParseState)) -> LexAction a

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

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.

(.&&.) :: LexPredicate -> LexPredicate -> LexPredicate

Conjunction of LexPredicates.

(.||.) :: LexPredicate -> LexPredicate -> LexPredicate

Disjunction of LexPredicates.

not' :: LexPredicate -> LexPredicate

Negation of LexPredicates.

type PreviousInput = AlexInput

type CurrentInput = AlexInput

type TokenLength = Int

Monad operations

getLexInput :: Parser AlexInput

setLexInput :: AlexInput -> Parser ()