{-| 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' = 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.
-}
module Agda.Syntax.Parser.Layout
    ( openBrace, closeBrace
    , withLayout
    , offsideRule
    , newLayoutContext
    , emptyLayout
    ) where

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


-- | Executed upon lexing an open brace (@\'{\'@). Enters the 'NoLayout'
--   context.
openBrace :: LexAction Token
openBrace :: LexAction Token
openBrace = (String -> Parser Token) -> LexAction Token
forall tok. (String -> Parser tok) -> LexAction tok
token ((String -> Parser Token) -> LexAction Token)
-> (String -> Parser Token) -> LexAction Token
forall a b. (a -> b) -> a -> b
$ \String
_ ->
    do  LayoutContext -> Parser ()
pushContext LayoutContext
NoLayout
        Interval
i <- Parser Interval
getParseInterval
        Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Interval -> Token
TokSymbol Symbol
SymOpenBrace Interval
i)


{-| 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.
-}
closeBrace :: LexAction Token
closeBrace :: LexAction Token
closeBrace = (String -> Parser Token) -> LexAction Token
forall tok. (String -> Parser tok) -> LexAction tok
token ((String -> Parser Token) -> LexAction Token)
-> (String -> Parser Token) -> LexAction Token
forall a b. (a -> b) -> a -> b
$ \String
_ ->
    do  Parser ()
popContext
        Interval
i <- Parser Interval
getParseInterval
        Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Interval -> Token
TokSymbol Symbol
SymCloseBrace Interval
i)


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

    If the current block doesn't use layout (i.e. it was started by
    'openBrace') all positions are considered to be /to the right/.
-}
offsideRule :: LexAction Token
offsideRule :: LexAction Token
offsideRule PreviousInput
inp PreviousInput
_ TokenLength
_ =
    do  Ordering
offs <- Position' () -> Parser Ordering
forall a. Position' a -> Parser Ordering
getOffside Position' ()
p
        case Ordering
offs of
            Ordering
LT  -> do   Parser ()
popContext
                        Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Interval -> Token
TokSymbol Symbol
SymCloseVirtualBrace Interval
i)
            Ordering
EQ  -> do   Parser ()
popLexState
                        Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Interval -> Token
TokSymbol Symbol
SymVirtualSemi Interval
i)
            Ordering
GT  -> do   Parser ()
popLexState
                        Parser Token
lexToken
    where
        p :: Position' ()
p = PreviousInput -> Position' ()
lexPos PreviousInput
inp
        i :: Interval
i = SrcFile -> Position' () -> Position' () -> Interval
forall a. a -> Position' () -> Position' () -> Interval' a
posToInterval (PreviousInput -> SrcFile
lexSrcFile PreviousInput
inp) Position' ()
p Position' ()
p


{-| 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 'newLayoutContext').
-}
emptyLayout :: LexAction Token
emptyLayout :: LexAction Token
emptyLayout PreviousInput
inp PreviousInput
_ TokenLength
_ =
    do  Parser ()
popLexState
        TokenLength -> Parser ()
pushLexState TokenLength
bol
        Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Interval -> Token
TokSymbol Symbol
SymCloseVirtualBrace Interval
i)
    where
        p :: Position' ()
p = PreviousInput -> Position' ()
lexPos PreviousInput
inp
        i :: Interval
i = SrcFile -> Position' () -> Position' () -> Interval
forall a. a -> Position' () -> Position' () -> Interval' a
posToInterval (PreviousInput -> SrcFile
lexSrcFile PreviousInput
inp) Position' ()
p Position' ()
p


{-| Start a new layout context. This is one of two ways to get out of the
    'Agda.Syntax.Parser.Lexer.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 '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.
-}
newLayoutContext :: LexAction Token
newLayoutContext :: LexAction Token
newLayoutContext PreviousInput
inp PreviousInput
_ TokenLength
_ =
    do  let offset :: Int32
offset = Position' () -> Int32
forall a. Position' a -> Int32
posCol Position' ()
p
        LayoutContext
ctx <- Parser LayoutContext
topContext
        case LayoutContext
ctx of
            Layout Int32
prevOffs | Int32
prevOffs Int32 -> Int32 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int32
offset ->
                do  TokenLength -> Parser ()
pushLexState TokenLength
empty_layout
                    Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Interval -> Token
TokSymbol Symbol
SymOpenVirtualBrace Interval
i)
            LayoutContext
_ ->
                do  LayoutContext -> Parser ()
pushContext (Int32 -> LayoutContext
Layout Int32
offset)
                    Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Interval -> Token
TokSymbol Symbol
SymOpenVirtualBrace Interval
i)
    where
        p :: Position' ()
p = PreviousInput -> Position' ()
lexPos PreviousInput
inp
        i :: Interval
i = SrcFile -> Position' () -> Position' () -> Interval
forall a. a -> Position' () -> Position' () -> Interval' a
posToInterval (PreviousInput -> SrcFile
lexSrcFile PreviousInput
inp) Position' ()
p Position' ()
p


-- | 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 =
    do  LayoutContext
ctx <- Parser LayoutContext
topContext
        Ordering -> Parser Ordering
forall (m :: * -> *) a. Monad m => a -> m a
return (Ordering -> Parser Ordering) -> Ordering -> Parser Ordering
forall a b. (a -> b) -> a -> b
$ case LayoutContext
ctx of
            Layout Int32
n    -> 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