{-| This module defines the lex action to lex nested comments. As is well-known
    this cannot be done by regular expressions (which, incidently, is probably
    the reason why C-comments don't nest).

    When scanning nested comments we simply keep track of the nesting level,
    counting up for /open comments/ and down for /close comments/.
-}
module Agda.Syntax.Parser.Comments
    where

import qualified Data.List as List

import {-# SOURCE #-} Agda.Syntax.Parser.LexActions
import Agda.Syntax.Parser.Monad
import Agda.Syntax.Parser.Tokens
import Agda.Syntax.Parser.Alex
import Agda.Syntax.Parser.LookAhead
import Agda.Syntax.Position

-- | Should comment tokens be output?

keepComments :: LexPredicate
keepComments :: LexPredicate
keepComments ([LexState]
_, ParseFlags
s) PreviousInput
_ LexState
_ PreviousInput
_ = ParseFlags -> Bool
parseKeepComments ParseFlags
s

-- | Should comment tokens be output?

keepCommentsM :: Parser Bool
keepCommentsM :: Parser Bool
keepCommentsM = (ParseFlags -> Bool) -> Parser ParseFlags -> Parser Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ParseFlags -> Bool
parseKeepComments Parser ParseFlags
getParseFlags

-- | Manually lexing a block comment. Assumes an /open comment/ has been lexed.
--   In the end the comment is discarded and 'lexToken' is called to lex a real
--   token.
nestedComment :: LexAction Token
nestedComment :: LexAction Token
nestedComment PreviousInput
inp PreviousInput
inp' LexState
_ =
    do  PreviousInput -> Parser ()
setLexInput PreviousInput
inp'
        (forall b. String -> LookAhead b) -> LookAhead () -> Parser ()
forall a.
(forall b. String -> LookAhead b) -> LookAhead a -> Parser a
runLookAhead forall b. String -> LookAhead b
forall p a. p -> LookAhead a
err (LookAhead () -> Parser ()) -> LookAhead () -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> String -> LookAhead ()
skipBlock String
"{-" String
"-}"
        Bool
keep <- Parser Bool
keepCommentsM
        if Bool
keep then do
          PreviousInput
inp'' <- Parser PreviousInput
getLexInput
          let p1 :: PositionWithoutFile
p1 = PreviousInput -> PositionWithoutFile
lexPos PreviousInput
inp; p2 :: PositionWithoutFile
p2 = PreviousInput -> PositionWithoutFile
lexPos PreviousInput
inp''
              i :: Interval' SrcFile
i = SrcFile
-> PositionWithoutFile -> PositionWithoutFile -> Interval' SrcFile
forall a.
a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
posToInterval (PreviousInput -> SrcFile
lexSrcFile PreviousInput
inp) PositionWithoutFile
p1 PositionWithoutFile
p2
              s :: String
s = case (PositionWithoutFile
p1, PositionWithoutFile
p2) of
                    (Pn { posPos :: forall a. Position' a -> Int32
posPos = Int32
p1 }, Pn { posPos :: forall a. Position' a -> Int32
posPos = Int32
p2 }) ->
                      Int32 -> String -> String
forall i a. Integral i => i -> [a] -> [a]
List.genericTake (Int32
p2 Int32 -> Int32 -> Int32
forall a. Num a => a -> a -> a
- Int32
p1) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ PreviousInput -> String
lexInput PreviousInput
inp
          Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Parser Token) -> Token -> Parser Token
forall a b. (a -> b) -> a -> b
$ (Interval' SrcFile, String) -> Token
TokComment (Interval' SrcFile
i, String
s)
         else
          Parser Token
lexToken
    where
        err :: p -> LookAhead a
err p
_ = Parser a -> LookAhead a
forall a. Parser a -> LookAhead a
liftP (Parser a -> LookAhead a) -> Parser a -> LookAhead a
forall a b. (a -> b) -> a -> b
$ PositionWithoutFile -> String -> Parser a
forall a. PositionWithoutFile -> String -> Parser a
parseErrorAt (PreviousInput -> PositionWithoutFile
lexPos PreviousInput
inp) String
"Unterminated '{-'"

-- | Lex a hole (@{! ... !}@). Holes can be nested.
--   Returns @'TokSymbol' 'SymQuestionMark'@.
hole :: LexAction Token
hole :: LexAction Token
hole PreviousInput
inp PreviousInput
inp' LexState
_ =
    do  PreviousInput -> Parser ()
setLexInput PreviousInput
inp'
        (forall b. String -> LookAhead b) -> LookAhead () -> Parser ()
forall a.
(forall b. String -> LookAhead b) -> LookAhead a -> Parser a
runLookAhead forall b. String -> LookAhead b
forall p a. p -> LookAhead a
err (LookAhead () -> Parser ()) -> LookAhead () -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> String -> LookAhead ()
skipBlock String
"{!" String
"!}"
        PositionWithoutFile
p <- PreviousInput -> PositionWithoutFile
lexPos (PreviousInput -> PositionWithoutFile)
-> Parser PreviousInput -> Parser PositionWithoutFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser PreviousInput
getLexInput
        Token -> Parser Token
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Parser Token) -> Token -> Parser Token
forall a b. (a -> b) -> a -> b
$
          Symbol -> Interval' SrcFile -> Token
TokSymbol Symbol
SymQuestionMark (Interval' SrcFile -> Token) -> Interval' SrcFile -> Token
forall a b. (a -> b) -> a -> b
$
          SrcFile
-> PositionWithoutFile -> PositionWithoutFile -> Interval' SrcFile
forall a.
a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
posToInterval (PreviousInput -> SrcFile
lexSrcFile PreviousInput
inp) (PreviousInput -> PositionWithoutFile
lexPos PreviousInput
inp) PositionWithoutFile
p
    where
        err :: p -> LookAhead a
err p
_ = Parser a -> LookAhead a
forall a. Parser a -> LookAhead a
liftP (Parser a -> LookAhead a) -> Parser a -> LookAhead a
forall a b. (a -> b) -> a -> b
$ PositionWithoutFile -> String -> Parser a
forall a. PositionWithoutFile -> String -> Parser a
parseErrorAt (PreviousInput -> PositionWithoutFile
lexPos PreviousInput
inp) String
"Unterminated '{!'"

-- | Skip a block of text enclosed by the given open and close strings. Assumes
--   the first open string has been consumed. Open-close pairs may be nested.
skipBlock :: String -> String -> LookAhead ()
skipBlock :: String -> String -> LookAhead ()
skipBlock String
open String
close = Integer -> LookAhead ()
forall a. (Eq a, Num a) => a -> LookAhead ()
scan Integer
1
    where
        scan :: a -> LookAhead ()
scan a
0 = LookAhead ()
sync
        scan a
n = [(String, LookAhead ())] -> LookAhead () -> LookAhead ()
forall a. [(String, LookAhead a)] -> LookAhead a -> LookAhead a
match [ String
open   String -> LookAhead () -> (String, LookAhead ())
forall a b. a -> b -> (a, b)
==>  a -> LookAhead ()
scan (a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)
                       , String
close  String -> LookAhead () -> (String, LookAhead ())
forall a b. a -> b -> (a, b)
==>  a -> LookAhead ()
scan (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1)
                       ] (LookAhead () -> LookAhead ()) -> LookAhead () -> LookAhead ()
forall a b. (a -> b) -> a -> b
`other` a -> LookAhead ()
scan a
n
            where
                ==> :: a -> b -> (a, b)
(==>) = (,)
                other :: (a -> b) -> a -> b
other = (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)