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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Syntax.Parser.LexActions

Contents

- Main function
- Lex actions
  - General actions
  - Specialized actions
- Lex predicates

Description

This module contains the building blocks used to construct the lexer.

Synopsis

- lexToken :: Parser Token
- token :: (String -> Parser tok) -> LexAction tok
- withInterval :: ((Interval, String) -> tok) -> LexAction tok
- withInterval' :: (String -> a) -> ((Interval, a) -> tok) -> LexAction tok
- withInterval_ :: (Interval -> r) -> LexAction r
- withLayout :: Keyword -> LexAction r -> LexAction r
- andThen :: Parser () -> LexAction r -> LexAction r
- skip :: LexAction Token
- begin :: LexState -> LexAction Token
- end :: LexAction Token
- beginWith :: LexState -> LexAction a -> LexAction a
- endWith :: LexAction a -> LexAction a
- begin_ :: LexState -> LexAction Token
- end_ :: LexAction Token
- lexError :: String -> Parser a
- keyword :: Keyword -> LexAction Token
- symbol :: Symbol -> LexAction Token
- identifier :: LexAction Token
- literal :: Read a => (a -> Literal) -> LexAction Token
- literal' :: (String -> a) -> (a -> Literal) -> LexAction Token
- integer :: String -> Integer
- followedBy :: Char -> LexPredicate
- eof :: LexPredicate
- inState :: LexState -> LexPredicate

# Main function

lexToken :: Parser Token Source #

Scan the input to find the next token. Calls `alexScanUser`. This is the main lexing function where all the work happens. The function `lexer`, used by the parser is the continuation version of this function.

# Lex actions

## General actions

token :: (String -> Parser tok) -> LexAction tok Source #

The most general way of parsing a token.

withInterval :: ((Interval, String) -> tok) -> LexAction tok Source #

Parse a token from an `Interval` and the lexed string.

withInterval' :: (String -> a) -> ((Interval, a) -> tok) -> LexAction tok Source #

Like `withInterval`, but applies a function to the string.

withInterval_ :: (Interval -> r) -> LexAction r Source #

Return a token without looking at the lexed string.

withLayout :: Keyword -> LexAction r -> LexAction r Source #

Executed for layout keywords. Enters the `layout` state and performs the given action.

andThen :: Parser () -> LexAction r -> LexAction r infixr 1 Source #

Prepend some parser manipulation to an action.

skip :: LexAction Token Source #

Throw away the current lexeme.

begin :: LexState -> LexAction Token Source #

Enter a new state without consuming any input.

end :: LexAction Token Source #

Exit the current state without consuming any input.

beginWith :: LexState -> LexAction a -> LexAction a Source #

Enter a new state and perform the given action.

endWith :: LexAction a -> LexAction a Source #

Exit the current state and perform the given action.

begin_ :: LexState -> LexAction Token Source #

Enter a new state throwing away the current lexeme.

end_ :: LexAction Token Source #

Exit the current state throwing away the current lexeme.

lexError :: String -> Parser a Source #

For lexical errors we want to report the current position as the site of the error, whereas for parse errors the previous position is the one we're interested in (since this will be the position of the token we just lexed). This function does `parseErrorAt` the current position.

## Specialized actions

keyword :: Keyword -> LexAction Token Source #

Parse a `Keyword` token, triggers layout for `layoutKeywords`.

symbol :: Symbol -> LexAction Token Source #

Parse a `Symbol` token.

identifier :: LexAction Token Source #

Parse an identifier. Identifiers can be qualified (see `Name`). Example: `Foo.Bar.f`

literal :: Read a => (a -> Literal) -> LexAction Token Source #

literal' :: (String -> a) -> (a -> Literal) -> LexAction Token Source #

Parse a literal.

integer :: String -> Integer Source #

# Lex predicates

followedBy :: Char -> LexPredicate Source #

True when the given character is the next character of the input string.

eof :: LexPredicate Source #

True if we are at the end of the file.

inState :: LexState -> LexPredicate Source #

True if the given state appears somewhere on the state stack