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.
ModuleAgda-2.8.0.2Haskell2010
Agda.Syntax.Parser.LexActions
This module contains the building blocks used to construct the lexer.
Synopsis
- value lexToken
- value token
- value withInterval
- value withInterval'
- value withInterval_
- value withLayout
- value andThen
- value skip
- value begin
- value end
- value beginWith
- value endWith
- value begin_
- value end_
- value lexError
- value keyword
- value symbol
- value identifier
- value literal
- value literal'
- value integer
- value followedBy
- value eof
- value inState
- PackageAgda-2.8.0.2
- Exports24
- LanguageHaskell2010
- LicenceMIT
- SourceLexActions.hs
Main function
Lex actions
General actions
The most general way of parsing a token.
Parse a token from an Interval and the lexed string.
Like withInterval, but applies a function to the string.
Return a token without looking at the lexed string.
Executed for layout keywords. Enters the layout state and performs the given action.
Prepend some parser manipulation to an action.
Throw away the current lexeme.
Enter a new state without consuming any input.
Exit the current state without consuming any input.
Enter a new state and perform the given action.
Exit the current state and perform the given action.
Enter a new state throwing away the current lexeme.
Exit the current state throwing away the current lexeme.
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
Parse a Keyword token, triggers layout for layoutKeywords.
Parse a Symbol token.
Parse an identifier. Identifiers can be qualified (see Name).
Example: Foo.Bar.f
Parse a literal.
Lex predicates
True when the given character is the next character of the input string.
True if we are at the end of the file.
True if the given state appears somewhere on the state stack