-- {-# LANGUAGE CPP #-}

{-| 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 = token $ \_ ->
    do  pushContext NoLayout
        i <- getParseInterval
        return (TokSymbol SymOpenBrace 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 = token $ \_ ->
    do  popContext
        i <- getParseInterval
        return (TokSymbol SymCloseBrace 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 inp _ _ =
    do  offs <- getOffside p
        case offs of
            LT  -> do   popContext
                        return (TokSymbol SymCloseVirtualBrace i)
            EQ  -> do   popLexState
                        return (TokSymbol SymVirtualSemi i)
            GT  -> do   popLexState
                        lexToken
    where
        p = lexPos inp
        i = posToInterval (lexSrcFile inp) p 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 inp _ _ =
    do  popLexState
        pushLexState bol
        return (TokSymbol SymCloseVirtualBrace i)
    where
        p = lexPos inp
        i = posToInterval (lexSrcFile inp) p 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 inp _ _ =
    do  let offset = posCol p
        ctx <- topContext
        case ctx of
            Layout prevOffs | prevOffs >= offset ->
                do  pushLexState empty_layout
                    return (TokSymbol SymOpenVirtualBrace i)
            _ ->
                do  pushContext (Layout offset)
                    return (TokSymbol SymOpenVirtualBrace i)
    where
        p = lexPos inp
        i = posToInterval (lexSrcFile inp) p p


-- | Compute the relative position of a location to the
--   current layout context.
getOffside :: Position' a -> Parser Ordering
getOffside loc =
    do  ctx <- topContext
        return $ case ctx of
            Layout n    -> compare (posCol loc) n
            _           -> GT