Layout.hs

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