    {-# 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 (Interval p p))
    	    EQ	-> do	popLexState
    			return (TokSymbol SymVirtualSemi (Interval p p))
    	    GT	-> do	popLexState
    			lexToken
        where
    	p = lexPos inp

    {-| 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 (Interval p p))
        where
    	p = lexPos inp

    {-| 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 (Interval p p))
    	    _ ->
    		do  pushContext (Layout offset)
    		    return (TokSymbol SymOpenVirtualBrace (Interval p p))
        where
    	p = lexPos inp

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