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

Safe Haskell | None

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

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.

literate :: LexState

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

code :: Int

layout :: LexState

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

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

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.