Agda.Syntax.Parser.Lexer

The lexer is generated by Alex (http://www.haskell.org/alex) and is an adaptation of GHC's lexer. The main lexing function lexer is called by the Agda.Syntax.Parser.Parser to get the next token from the input.

The main function

lexer :: (Token -> Parser a) -> Parser a

Return the next token. This is the function used by Happy in the parser.

lexer k = lexToken >>= k

Lex states

normal :: LexState

This is the initial state for parsing a regular, non-literate file.

code :: Int

layout :: LexState

The layout state. Entered when we see a layout keyword (withLayout) and exited at the next token (newLayoutBlock).

empty_layout :: LexState

We enter this state from newLayoutBlock when the token following a layout keyword is to the left of (or at the same column as) the current layout context. Example:

data Empty : Set where
foo : Empty -> Nat

Here the second line is not part of the where clause since it is has the same indentation as the data definition. What we have to do is insert an empty layout block {} after the where. The only thing that can happen in this state is that emptyLayout is executed, generating the closing brace. The open brace is generated when entering by newLayoutBlock.

bol :: LexState

This state is entered at the beginning of each line. You can't lex anything in this state, and to exit you have to check the layout rule. Done with offsideRule.

imp_dir :: LexState

This state can only be entered by the parser. In this state you can only lex the keywords using, hiding, renaming and to. Moreover they are only keywords in this particular state. The lexer will never enter this state by itself, that has to be done in the parser.

Alex generated functions

data AlexReturn a

Constructors

AlexEOF

AlexError !AlexInput

AlexSkip !AlexInput !Int

AlexToken !AlexInput !Int a

alexScanUser :: ([LexState], ParseFlags) -> AlexInput -> Int -> AlexReturn (LexAction Token)

This is the main lexing function generated by Alex.