Agda-2.6.3.20230805: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Parser.Alex

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

alexInputPrevChar :: AlexInput -> Char Source #

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 #

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) Source #

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 Source #

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

Instances

Instances details
Applicative LexAction Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Parser.Alex

Methods

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

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

Monad LexAction Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Parser.Alex

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

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