Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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.

type TokenLength = Int Source #

Monad operations