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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Syntax.Parser.Layout

Description

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 `LayoutContext`s 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.

Synopsis

- withLayout :: Keyword -> LexAction r -> LexAction r
- offsideRule :: LexAction Token
- newLayoutBlock :: LexAction Token
- emptyLayout :: LexAction Token
- confirmLayout :: Parser ()

# Documentation

withLayout :: Keyword -> LexAction r -> LexAction r Source #

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

offsideRule :: LexAction Token Source #

Executed for the first token in each line (see `bol`), except when the last token was a layout keyword.

Checks the position of the token relative to the current layout context. If the token is

- to the left : Exit the current block 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.

newLayoutBlock :: LexAction Token Source #

Start a new layout block. This is how to get out of the `layout` state. There are two possibilities:

- The current token is to the right of the confirmed layout column.
- The current token is to the left of or in the same column as the confirmed layout column.

In the first case everything is fine and we enter a new layout block 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 Token Source #

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 `newLayoutBlock`).

confirmLayout :: Parser () Source #

At a new line, we confirm either existing tentative layout columns, or, if the last token was a layout keyword, the expected new layout column.