| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 :: LexAction r -> LexAction r
begin :: LexState -> LexAction Token
end :: LexAction Token
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 => (Range -> a -> Literal) -> LexAction Token
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 :: LexAction r -> LexAction r | Source

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

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

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 => (Range -> a -> Literal) -> LexAction Token | Source

Parse a literal.
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
Produced by Haddock version 2.4.2