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

Agda.Syntax.Parser.Lexer

Contents

The main function
Lex states
Alex generated functions

Description
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.
Synopsis

lexer :: (Token -> Parser a) -> Parser a
normal :: LexState
literate :: LexState
code :: Int
layout :: LexState
empty_layout :: LexState
bol :: LexState
imp_dir :: LexState

data AlexReturn a

= AlexEOF
| AlexError !AlexInput
| AlexSkip !AlexInput !Int
| AlexToken !AlexInput !Int a

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

The main function

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

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

    lexer k = lexToken >>= k

Lex states

normal :: LexState | Source

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

literate :: LexState | Source

This is the initial state for parsing a literate file. Code blocks should be enclosed in `\begin{code}` `\end{code}` pairs.

code :: Int | Source

layout :: LexState | Source

The layout state. Entered when we see a layout keyword (`withLayout`) and exited either when seeing an open brace (openBrace) or at the next token (`newLayoutContext`). Update: we don't use braces for layout anymore.

empty_layout :: LexState | Source

We enter this state from `newLayoutContext` 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 `newLayoutContext`.

bol :: LexState | Source

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 | Source

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 | Source

Constructors

AlexEOF |
AlexError !AlexInput |
AlexSkip !AlexInput !Int |
AlexToken !AlexInput !Int a |

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

This is the main lexing function generated by Alex.
Produced by Haddock version 2.4.2