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



This module contains the lex actions that handle the layout rules. The way it works is that the Parser monad keeps track of a stack of LayoutContexts specifying the indentation of the layout blocks in scope. For instance, consider the following incomplete (Haskell) program:

 f x = x'
     x' = case x of { True -> False; False -> ...

At the ... the layout context would be

 [NoLayout, Layout 4, Layout 0]

The closest layout block is the one containing the case branches. This block starts with an open brace ('{') and so doesn't use layout. The second closest block is the where clause. Here, there is no open brace so the block is started by the x' token which has indentation 4. Finally there is a top-level layout block with indentation 0.



openBrace :: LexAction TokenSource

Executed upon lexing an open brace ('{'). Enters the NoLayout context.

closeBrace :: LexAction TokenSource

Executed upon lexing a close brace ('}'). Exits the current layout context. This might look a bit funny--the lexer will happily use a close brace to close a context open by a virtual brace. This is not a problem since the parser will make sure the braces are appropriately matched.

withLayout :: LexAction r -> LexAction rSource

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

offsideRule :: LexAction TokenSource

Executed for the first token in each line (see bol). Checks the position of the token relative to the current layout context. If the token is

  • to the left : Exit the current context and a return virtual close brace (stay in the bol state).
  • same column : Exit the bol state and return a virtual semi colon.
  • to the right : Exit the bol state and continue lexing.

If the current block doesn't use layout (i.e. it was started by openBrace) all positions are considered to be to the right.

newLayoutContext :: LexAction TokenSource

Start a new layout context. This is one of two ways to get out of the layout state (the other is openBrace). There are two possibilities:

  • The current token is to the right of the current layout context (or we're in a no layout context).
  • The current token is to the left of or in the same column as the current context.

In the first case everything is fine and we enter a new layout context at the column of the current token. In the second case we have an empty layout block so we enter the empty_layout state. In both cases we return a virtual open brace without consuming any input.

Entering a new state when we know we want to generate a virtual {} may seem a bit roundabout. The thing is that we can only generate one token at a time, so the way to generate two tokens is to generate the first one and then enter a state in which the only thing you can do is generate the second one.

emptyLayout :: LexAction TokenSource

This action is only executed from the empty_layout state. It will exit this state, enter the bol state, and return a virtual close brace (closing the empty layout block started by newLayoutContext).