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




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


Main function

lexToken :: Parser TokenSource

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 tokSource

The most general way of parsing a token.

withInterval :: ((Interval, String) -> tok) -> LexAction tokSource

Parse a token from an Interval and the lexed string.

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

Like withInterval, but applies a function to the string.

withInterval_ :: (Interval -> r) -> LexAction rSource

Return a token without looking at the lexed string.

withLayout :: LexAction r -> LexAction rSource

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

begin :: LexState -> LexAction TokenSource

Enter a new state without consuming any input.

end :: LexAction TokenSource

Exit the current state without consuming any input

endWith :: LexAction a -> LexAction aSource

Exit the current state and perform the given action.

begin_ :: LexState -> LexAction TokenSource

Enter a new state throwing away the current lexeme.

end_ :: LexAction TokenSource

Exit the current state throwing away the current lexeme.

lexError :: String -> Parser aSource

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 TokenSource

Parse a Keyword token, triggers layout for layoutKeywords.

identifier :: LexAction TokenSource

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

literal :: Read a => (Range -> a -> Literal) -> LexAction TokenSource

Parse a literal.

Lex predicates

followedBy :: Char -> LexPredicateSource

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

eof :: LexPredicateSource

True if we are at the end of the file.

inState :: LexState -> LexPredicateSource

True if the given state appears somewhere on the state stack