    {-| 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.

    -}
    module Agda.Syntax.Parser.Layout
        ( withLayout
        , offsideRule
        , newLayoutBlock
        , emptyLayout
        , confirmLayout
        ) where

    import Control.Monad        ( when )
    import Control.Monad.State  ( gets, modify )

    import Agda.Syntax.Parser.Lexer
    import Agda.Syntax.Parser.Alex
    import Agda.Syntax.Parser.Monad
    import Agda.Syntax.Parser.Tokens
    import Agda.Syntax.Parser.LexActions
    import Agda.Syntax.Position

    import Agda.Utils.Functor ((<&>))

    import Agda.Utils.Impossible

    {-| Executed for the first token in each line (see 'Agda.Syntax.Parser.Lexer.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
            'Agda.Syntax.Parser.Lexer.bol' state).

        - /same column/ :
            Exit the 'Agda.Syntax.Parser.Lexer.bol' state and return a virtual semi
            colon.

        - /to the right/ :
            Exit the 'Agda.Syntax.Parser.Lexer.bol' state and continue lexing.

    -}
    offsideRule :: LexAction Token
    offsideRule :: LexAction Token
    offsideRule = (PreviousInput -> PreviousInput -> LexState -> Parser Token)
    -> LexAction Token
    forall r.
    (PreviousInput -> PreviousInput -> LexState -> Parser r)
    -> LexAction r
    LexAction ((PreviousInput -> PreviousInput -> LexState -> Parser Token)
     -> LexAction Token)
    -> (PreviousInput -> PreviousInput -> LexState -> Parser Token)
    -> LexAction Token
    forall a b. (a -> b) -> a -> b
    $ \ PreviousInput
    inp PreviousInput
    _ LexState
    _ -> do
        let p :: PositionWithoutFile
    p = PreviousInput -> PositionWithoutFile
    lexPos PreviousInput
    inp
            i :: Interval' SrcFile
    i = SrcFile
    -> PositionWithoutFile -> PositionWithoutFile -> Interval' SrcFile
    forall a.
    a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
    posToInterval (PreviousInput -> SrcFile
    lexSrcFile PreviousInput
    inp) PositionWithoutFile
    p PositionWithoutFile
    p
        PositionWithoutFile -> Parser Ordering
    forall a. Position' a -> Parser Ordering
    getOffside PositionWithoutFile
    p Parser Ordering -> (Ordering -> Parser Token) -> Parser Token
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Ordering
    LT  -> do   Parser ()
    popBlock
                        Token -> Parser Token
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Symbol -> Interval' SrcFile -> Token
    TokSymbol Symbol
    SymCloseVirtualBrace Interval' SrcFile
    i)
            Ordering
    EQ  -> do   Parser ()
    popLexState
                        Token -> Parser Token
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Symbol -> Interval' SrcFile -> Token
    TokSymbol Symbol
    SymVirtualSemi Interval' SrcFile
    i)
            Ordering
    GT  -> do   Parser ()
    popLexState
                        Parser Token
    lexToken

    {-| This action is only executed from the 'Agda.Syntax.Parser.Lexer.empty_layout'
        state. It will exit this state, enter the 'Agda.Syntax.Parser.Lexer.bol' state,
        and return a virtual close brace (closing the empty layout block started
        by 'newLayoutBlock').
    -}
    emptyLayout :: LexAction Token
    emptyLayout :: LexAction Token
    emptyLayout = (PreviousInput -> PreviousInput -> LexState -> Parser Token)
    -> LexAction Token
    forall r.
    (PreviousInput -> PreviousInput -> LexState -> Parser r)
    -> LexAction r
    LexAction ((PreviousInput -> PreviousInput -> LexState -> Parser Token)
     -> LexAction Token)
    -> (PreviousInput -> PreviousInput -> LexState -> Parser Token)
    -> LexAction Token
    forall a b. (a -> b) -> a -> b
    $ \ PreviousInput
    inp PreviousInput
    _ LexState
    _ -> do
        let p :: PositionWithoutFile
    p = PreviousInput -> PositionWithoutFile
    lexPos PreviousInput
    inp
            i :: Interval' SrcFile
    i = SrcFile
    -> PositionWithoutFile -> PositionWithoutFile -> Interval' SrcFile
    forall a.
    a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
    posToInterval (PreviousInput -> SrcFile
    lexSrcFile PreviousInput
    inp) PositionWithoutFile
    p PositionWithoutFile
    p
        Parser ()
    popLexState
        LexState -> Parser ()
    pushLexState LexState
    bol
        Token -> Parser Token
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Symbol -> Interval' SrcFile -> Token
    TokSymbol Symbol
    SymCloseVirtualBrace Interval' SrcFile
    i)

    {-| Start a new layout block. This is how to get out of the
        'Agda.Syntax.Parser.Lexer.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 'Agda.Syntax.Parser.Lexer.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.
    -}
    newLayoutBlock :: LexAction Token
    newLayoutBlock :: LexAction Token
    newLayoutBlock = (PreviousInput -> PreviousInput -> LexState -> Parser Token)
    -> LexAction Token
    forall r.
    (PreviousInput -> PreviousInput -> LexState -> Parser r)
    -> LexAction r
    LexAction ((PreviousInput -> PreviousInput -> LexState -> Parser Token)
     -> LexAction Token)
    -> (PreviousInput -> PreviousInput -> LexState -> Parser Token)
    -> LexAction Token
    forall a b. (a -> b) -> a -> b
    $ \ PreviousInput
    inp PreviousInput
    _ LexState
    _ -> do
        let p :: PositionWithoutFile
    p = PreviousInput -> PositionWithoutFile
    lexPos PreviousInput
    inp
            i :: Interval' SrcFile
    i = SrcFile
    -> PositionWithoutFile -> PositionWithoutFile -> Interval' SrcFile
    forall a.
    a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
    posToInterval (PreviousInput -> SrcFile
    lexSrcFile PreviousInput
    inp) PositionWithoutFile
    p PositionWithoutFile
    p
            offset :: Column
    offset = PositionWithoutFile -> Column
    forall a. Position' a -> Column
    posCol PositionWithoutFile
    p
        LayoutStatus
    status   <- Parser LayoutStatus
    popPendingLayout
        Keyword
    kw       <- (ParseState -> Keyword) -> Parser Keyword
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ParseState -> Keyword
    parseLayKw
        Column
    prevOffs <- LayoutContext -> Column
    confirmedLayoutColumn (LayoutContext -> Column) -> Parser LayoutContext -> Parser Column
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser LayoutContext
    forall (m :: * -> *). MonadState ParseState m => m LayoutContext
    getContext
        if Column
    prevOffs Column -> Column -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Column
    offset
            then LexState -> Parser ()
    pushLexState LexState
    empty_layout
            else do
                Bool -> Parser () -> Parser ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (LayoutStatus
    status LayoutStatus -> LayoutStatus -> Bool
    forall a. Eq a => a -> a -> Bool
    == LayoutStatus
    Confirmed) (Parser () -> Parser ()) -> Parser () -> Parser ()
    forall a b. (a -> b) -> a -> b
    $
                  (LayoutContext -> LayoutContext) -> Parser ()
    modifyContext ((LayoutContext -> LayoutContext) -> Parser ())
    -> (LayoutContext -> LayoutContext) -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ Maybe Column -> LayoutContext -> LayoutContext
    confirmTentativeBlocks (Maybe Column -> LayoutContext -> LayoutContext)
    -> Maybe Column -> LayoutContext -> LayoutContext
    forall a b. (a -> b) -> a -> b
    $ Column -> Maybe Column
    forall a. a -> Maybe a
    Just Column
    offset
                LayoutBlock -> Parser ()
    pushBlock (LayoutBlock -> Parser ()) -> LayoutBlock -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ Keyword -> LayoutStatus -> Column -> LayoutBlock
    Layout Keyword
    kw LayoutStatus
    status Column
    offset
        Token -> Parser Token
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Token -> Parser Token) -> Token -> Parser Token
    forall a b. (a -> b) -> a -> b
    $ Symbol -> Interval' SrcFile -> Token
    TokSymbol Symbol
    SymOpenVirtualBrace Interval' SrcFile
    i
      where

        -- Get and reset the status of the coming layout block.
        popPendingLayout :: Parser LayoutStatus
        popPendingLayout :: Parser LayoutStatus
    popPendingLayout = do
            LayoutStatus
    status <- (ParseState -> LayoutStatus) -> Parser LayoutStatus
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ParseState -> LayoutStatus
    parseLayStatus
            Parser ()
    resetLayoutStatus
            LayoutStatus -> Parser LayoutStatus
    forall (m :: * -> *) a. Monad m => a -> m a
    return LayoutStatus
    status

        -- The confirmed layout column, or 0 if there is none.
        confirmedLayoutColumn :: LayoutContext -> Column
        confirmedLayoutColumn :: LayoutContext -> Column
    confirmedLayoutColumn = \case
           Layout Keyword
    _ LayoutStatus
    Confirmed Column
    c : LayoutContext
    _   -> Column
    c
           Layout Keyword
    _ LayoutStatus
    Tentative Column
    _ : LayoutContext
    cxt -> LayoutContext -> Column
    confirmedLayoutColumn LayoutContext
    cxt
           [] -> Column
    0 -- should only happen when looking at the first token (top-level layout)

    -- | Compute the relative position of a location to the
    --   current layout context.
    getOffside :: Position' a -> Parser Ordering
    getOffside :: forall a. Position' a -> Parser Ordering
    getOffside Position' a
    loc =
        Parser LayoutContext
    forall (m :: * -> *). MonadState ParseState m => m LayoutContext
    getContext Parser LayoutContext
    -> (LayoutContext -> Ordering) -> Parser Ordering
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
            Layout Keyword
    _ LayoutStatus
    _ Column
    n : LayoutContext
    _ -> Column -> Column -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Position' a -> Column
    forall a. Position' a -> Column
    posCol Position' a
    loc) Column
    n
            LayoutContext
    _                -> Ordering
    GT

    -- | 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.
    confirmLayout :: Parser ()
    confirmLayout :: Parser ()
    confirmLayout = Parser [LexState]
    getLexState Parser [LexState] -> ([LexState] -> Parser ()) -> Parser ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ case
      LexState
    s : [LexState]
    _ | LexState
    s LexState -> LexState -> Bool
    forall a. Eq a => a -> a -> Bool
    == LexState
    layout -> Parser ()
    confirmedLayoutComing
      [LexState]
    _                   -> Parser ()
    confirmLayoutAtNewLine
      where

      -- Mark the pending layout block as 'Confirmed'.
      confirmedLayoutComing :: Parser ()
      confirmedLayoutComing :: Parser ()
    confirmedLayoutComing = (ParseState -> ParseState) -> Parser ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((ParseState -> ParseState) -> Parser ())
    -> (ParseState -> ParseState) -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ \ ParseState
    s -> ParseState
    s { parseLayStatus :: LayoutStatus
    parseLayStatus = LayoutStatus
    Confirmed }

      -- Encountering a newline outside of a 'layout' state we confirm top
      -- tentative layout columns.
      confirmLayoutAtNewLine :: Parser ()
      confirmLayoutAtNewLine :: Parser ()
    confirmLayoutAtNewLine = (LayoutContext -> LayoutContext) -> Parser ()
    modifyContext ((LayoutContext -> LayoutContext) -> Parser ())
    -> (LayoutContext -> LayoutContext) -> Parser ()
    forall a b. (a -> b) -> a -> b
    $ Maybe Column -> LayoutContext -> LayoutContext
    confirmTentativeBlocks Maybe Column
    forall a. Maybe a
    Nothing

    -- | Confirm all top 'Tentative' layout columns.
    -- If a column is given, only those below the given column.
    --
    -- The code ensures that the newly created 'Definitive' columns
    -- are strictly decreasing.
    --
    confirmTentativeBlocks :: Maybe Column -> LayoutContext -> LayoutContext
    confirmTentativeBlocks :: Maybe Column -> LayoutContext -> LayoutContext
    confirmTentativeBlocks Maybe Column
    mcol = \case
        Layout Keyword
    kw LayoutStatus
    Tentative Column
    col : LayoutContext
    cxt | Bool -> (Column -> Bool) -> Maybe Column -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True (Column
    col Column -> Column -> Bool
    forall a. Ord a => a -> a -> Bool
    <) Maybe Column
    mcol
                -> Keyword -> LayoutStatus -> Column -> LayoutBlock
    Layout Keyword
    kw LayoutStatus
    Confirmed Column
    col LayoutBlock -> LayoutContext -> LayoutContext
    forall a. a -> [a] -> [a]
    : Maybe Column -> LayoutContext -> LayoutContext
    confirmTentativeBlocks (Column -> Maybe Column
    forall a. a -> Maybe a
    Just Column
    col) LayoutContext
    cxt
        LayoutContext
    cxt  -> LayoutContext
    cxt