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
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
$ \_ ->
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)
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
$ \_ ->
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)
offsideRule :: LexAction Token
offsideRule :: LexAction Token
offsideRule inp :: PreviousInput
inp _ _ =
do Ordering
offs <- Position' () -> Parser Ordering
forall a. Position' a -> Parser Ordering
getOffside Position' ()
p
case Ordering
offs of
LT -> do Parser ()
popContext
Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Interval -> Token
TokSymbol Symbol
SymCloseVirtualBrace Interval
i)
EQ -> do Parser ()
popLexState
Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Interval -> Token
TokSymbol Symbol
SymVirtualSemi Interval
i)
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
emptyLayout :: LexAction Token
emptyLayout :: LexAction Token
emptyLayout inp :: PreviousInput
inp _ _ =
do Parser ()
popLexState
LexState -> Parser ()
pushLexState LexState
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
newLayoutContext :: LexAction Token
newLayoutContext :: LexAction Token
newLayoutContext inp :: PreviousInput
inp _ _ =
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 prevOffs :: Int32
prevOffs | Int32
prevOffs Int32 -> Int32 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int32
offset ->
do LexState -> Parser ()
pushLexState LexState
empty_layout
Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Interval -> Token
TokSymbol Symbol
SymOpenVirtualBrace Interval
i)
_ ->
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
getOffside :: Position' a -> Parser Ordering
getOffside :: Position' a -> Parser Ordering
getOffside loc :: 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 n :: 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
_ -> Ordering
GT