{-| 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 -> TokenLength -> Parser Token)
-> LexAction Token
forall r.
(PreviousInput -> PreviousInput -> TokenLength -> Parser r)
-> LexAction r
LexAction ((PreviousInput -> PreviousInput -> TokenLength -> Parser Token)
 -> LexAction Token)
-> (PreviousInput -> PreviousInput -> TokenLength -> Parser Token)
-> LexAction Token
forall a b. (a -> b) -> a -> b
$ \ PreviousInput
inp PreviousInput
_ TokenLength
_ -> 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 -> TokenLength -> Parser Token)
-> LexAction Token
forall r.
(PreviousInput -> PreviousInput -> TokenLength -> Parser r)
-> LexAction r
LexAction ((PreviousInput -> PreviousInput -> TokenLength -> Parser Token)
 -> LexAction Token)
-> (PreviousInput -> PreviousInput -> TokenLength -> Parser Token)
-> LexAction Token
forall a b. (a -> b) -> a -> b
$ \ PreviousInput
inp PreviousInput
_ TokenLength
_ -> 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
    TokenLength -> Parser ()
pushLexState TokenLength
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 -> TokenLength -> Parser Token)
-> LexAction Token
forall r.
(PreviousInput -> PreviousInput -> TokenLength -> Parser r)
-> LexAction r
LexAction ((PreviousInput -> PreviousInput -> TokenLength -> Parser Token)
 -> LexAction Token)
-> (PreviousInput -> PreviousInput -> TokenLength -> Parser Token)
-> LexAction Token
forall a b. (a -> b) -> a -> b
$ \ PreviousInput
inp PreviousInput
_ TokenLength
_ -> 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 :: Int32
offset = PositionWithoutFile -> Int32
forall a. Position' a -> Int32
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
    Int32
prevOffs <- LayoutContext -> Int32
confirmedLayoutColumn (LayoutContext -> Int32) -> Parser LayoutContext -> Parser Int32
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LayoutContext
forall (m :: * -> *). MonadState ParseState m => m LayoutContext
getContext
    if Int32
prevOffs Int32 -> Int32 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int32
offset
        then TokenLength -> Parser ()
pushLexState TokenLength
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 Int32 -> LayoutContext -> LayoutContext
confirmTentativeBlocks (Maybe Int32 -> LayoutContext -> LayoutContext)
-> Maybe Int32 -> LayoutContext -> LayoutContext
forall a b. (a -> b) -> a -> b
$ Int32 -> Maybe Int32
forall a. a -> Maybe a
Just Int32
offset
            LayoutBlock -> Parser ()
pushBlock (LayoutBlock -> Parser ()) -> LayoutBlock -> Parser ()
forall a b. (a -> b) -> a -> b
$ Keyword -> LayoutStatus -> Int32 -> LayoutBlock
Layout Keyword
kw LayoutStatus
status Int32
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 -> Int32
confirmedLayoutColumn = \case
       Layout Keyword
_ LayoutStatus
Confirmed Int32
c : LayoutContext
_   -> Int32
c
       Layout Keyword
_ LayoutStatus
Tentative Int32
_ : LayoutContext
cxt -> LayoutContext -> Int32
confirmedLayoutColumn LayoutContext
cxt
       [] -> Int32
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 :: 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
_ Int32
n : LayoutContext
_ -> Int32 -> Int32 -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Position' a -> Int32
forall a. Position' a -> Int32
posCol Position' a
loc) Int32
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 [TokenLength]
getLexState Parser [TokenLength] -> ([TokenLength] -> Parser ()) -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
  TokenLength
s : [TokenLength]
_ | TokenLength
s TokenLength -> TokenLength -> Bool
forall a. Eq a => a -> a -> Bool
== TokenLength
layout -> Parser ()
confirmedLayoutComing
  [TokenLength]
_                   -> 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 Int32 -> LayoutContext -> LayoutContext
confirmTentativeBlocks Maybe Int32
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 Int32 -> LayoutContext -> LayoutContext
confirmTentativeBlocks Maybe Int32
mcol = \case
    Layout Keyword
kw LayoutStatus
Tentative Int32
col : LayoutContext
cxt | Bool -> (Int32 -> Bool) -> Maybe Int32 -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (Int32
col Int32 -> Int32 -> Bool
forall a. Ord a => a -> a -> Bool
<) Maybe Int32
mcol
            -> Keyword -> LayoutStatus -> Int32 -> LayoutBlock
Layout Keyword
kw LayoutStatus
Confirmed Int32
col LayoutBlock -> LayoutContext -> LayoutContext
forall a. a -> [a] -> [a]
: Maybe Int32 -> LayoutContext -> LayoutContext
confirmTentativeBlocks (Int32 -> Maybe Int32
forall a. a -> Maybe a
Just Int32
col) LayoutContext
cxt
    LayoutContext
cxt  -> LayoutContext
cxt