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'
  where
    x' = do y <- foo x; bar ...

At the ... the layout context would be

[Layout 12, Layout 4, Layout 0]

The closest layout block is the one following do which is started by token foo at column 12. The second closest block is the where clause started by the x' token which has indentation 4. Finally, there is a top-level layout block with indentation 0.

In April 2021 we changed layout handling in the lexer to allow stacking of layout keywords on the same line, e.g.:

private module M where
   postulate A : Set
             private
               B : Set

The layout columns in the layout context (stack of layout blocks) can have LayoutStatus either Tentative or Confirmed. New layout columns following a layout keyword are tentative until we see a new line. E.g.

• The first private block (column 8) is Tentative when we encounter the layout keyword where.
• The postulate block (column 12) is Tentative until the newline after A : Set.

In contrast,

• The module block (column 2) is Confirmed from the beginning since the first token (postulate) after the layout keyword where is on a new line.
• The second private block (column 14) is also Confirmed from the beginning (for the same reason).

A new layout column has to be strictly above the last confirmed column only. E.g., when encountering postulate at column 2 after where, the confirmed column is still 0, so this is a valid start of the block following where.

The column 8 of the private block never enters the Confirmed status but remains Tentative. Also, this block can never get more than the one declaration it has (module...), because when the module block closes due to a column < 2, it closes as well. One could say that tentative blocks buried under confirmed blocks are passive, the only wait for their closing.

To implement the process of block confirmation (function confirmLayout), the lexer has to act on newline characters (except for those in a block comment).

• In ordinary mode, when encountering a newline, we confirm the top unconfirmed blocks. Example: The newline after A : Set confirms the column 12 after postulate. Function: confirmLayoutAtNewLine, state bol.
• In the layout state following a layout keyword, a newline does not confirm any block, but announces that the next block should be confirmed from the start. Function: confirmedLayoutComing.

In order to implement confirmedLayoutComing we have a LayoutStatus flag in the parse state (field stateLayStatus). By default, for a new layout block, the status is Tentative (unless we saw a newline).

New layout blocks are created as follows. When a layout keyword is encountered, we enter lexer state layout via function withLayout. When we exit the layout state via newLayoutBlock with a token that marks the new layout column, we push a new LayoutBlock onto the LayoutContext using the given column and the current parseLayStatus which is then reset to Tentative.

The new block is actually only pushed if the column is above the last confirmed layout column (confirmedLayoutColumn). If this check fails, we instead enter the empty_layout state. This state produces the closing brace and is immediately left for bol (beginning of line).

(Remark: In bol we might confirm some tentative top blocks, but this is irrelevant, since they will be closed immediately, given that the current token is left of the confirmed column, and tentative columns above it must be to the right of this column.)

The offsideRule (state bol) is unchanged. It checks how the first token on a new line relates to the top layout column, be it tentative or confirmed. (Since we are on a new line, Tentative can only happen when we popped some Confirmed columns and continue popping the top Tentative columns here.) While the token is to the left of the layout column, we keep closing blocks.