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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Parser.Alex

Contents

- Alex requirements
- Lex actions
- Monad operations

Description

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

Synopsis

- data AlexInput = AlexInput {
  - lexSrcFile :: !SrcFile
  - lexPos :: !PositionWithoutFile
  - lexInput :: String
  - lexPrevChar :: !Char
  }
- lensLexInput :: Lens' AlexInput String
- alexInputPrevChar :: AlexInput -> Char
- alexGetChar :: AlexInput -> Maybe (Char, AlexInput)
- alexGetByte :: AlexInput -> Maybe (Word8, AlexInput)
- newtype LexAction r = LexAction {
  - runLexAction :: PreviousInput -> CurrentInput -> TokenLength -> Parser r
  }
- type LexPredicate = ([LexState], ParseFlags) -> PreviousInput -> TokenLength -> CurrentInput -> Bool
- (.&&.) :: LexPredicate -> LexPredicate -> LexPredicate
- (.||.) :: LexPredicate -> LexPredicate -> LexPredicate
- not' :: LexPredicate -> LexPredicate
- type PreviousInput = AlexInput
- type CurrentInput = AlexInput
- type TokenLength = Int
- getLexInput :: Parser AlexInput
- setLexInput :: AlexInput -> Parser ()

# Alex requirements

data AlexInput Source #

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' AlexInput String Source #

A lens for `lexInput`.

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.

Constructors

LexAction |

Fields

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

#### Instances

Instances details

Applicative LexAction Source # |
Instance details Defined in Agda.Syntax.Parser.Alex Methods pure :: a -> LexAction a Source # (<*>) :: LexAction (a -> b) -> LexAction a -> LexAction b Source # liftA2 :: (a -> b -> c) -> LexAction a -> LexAction b -> LexAction c Source # (*>) :: LexAction a -> LexAction b -> LexAction b Source # (<*) :: LexAction a -> LexAction b -> LexAction a Source #
Functor LexAction Source # |
Instance details Defined in Agda.Syntax.Parser.Alex Methods fmap :: (a -> b) -> LexAction a -> LexAction b Source # (<$) :: a -> LexAction b -> LexAction a Source #
Monad LexAction Source # |
Instance details Defined in Agda.Syntax.Parser.Alex Methods (>>=) :: LexAction a -> (a -> LexAction b) -> LexAction b Source # (>>) :: LexAction a -> LexAction b -> LexAction b Source # return :: a -> LexAction a Source #
MonadState ParseState LexAction Source # |
Instance details Defined in Agda.Syntax.Parser.Alex Methods get :: LexAction ParseState Source # put :: ParseState -> LexAction () Source # state :: (ParseState -> (a, ParseState)) -> LexAction a Source #

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.

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

Conjunction of `LexPredicate`s.

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

Disjunction of `LexPredicate`s.

not' :: LexPredicate -> LexPredicate Source #

Negation of `LexPredicate`s.

type PreviousInput = AlexInput Source #

type CurrentInput = AlexInput Source #

type TokenLength = Int Source #

# Monad operations

getLexInput :: Parser AlexInput Source #

setLexInput :: AlexInput -> Parser () Source #