{-| 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 = 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 = forall r.
(PreviousInput -> PreviousInput -> LexState -> Parser r)
-> LexAction r
LexAction forall a b. (a -> b) -> a -> b
$ \ PreviousInput
inp PreviousInput
inp' LexState
_ ->
    do  PreviousInput -> Parser ()
setLexInput PreviousInput
inp'
        let err :: forall a. String -> LookAhead a
            err :: forall a. String -> LookAhead a
err String
_ = forall a. Parser a -> LookAhead a
liftP forall a b. (a -> b) -> a -> b
$ forall a. PositionWithoutFile -> String -> Parser a
parseErrorAt (PreviousInput -> PositionWithoutFile
lexPos PreviousInput
inp) String
"Unterminated '{-'"
        forall a.
(forall a. String -> LookAhead a) -> LookAhead a -> Parser a
runLookAhead forall a. String -> LookAhead a
err 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 = 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 }) ->
                      forall i a. Integral i => i -> [a] -> [a]
List.genericTake (Int32
p2 forall a. Num a => a -> a -> a
- Int32
p1) forall a b. (a -> b) -> a -> b
$ PreviousInput -> String
lexInput PreviousInput
inp
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Interval' SrcFile, String) -> Token
TokComment (Interval' SrcFile
i, String
s)
         else
          Parser Token
lexToken


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

-- | 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 ()
scan Integer
1
    where
        scan :: Integer -> LookAhead ()
scan Integer
0 = LookAhead ()
sync
        scan Integer
n = forall a. [(String, LookAhead a)] -> LookAhead a -> LookAhead a
match [ String
open   forall {a} {b}. a -> b -> (a, b)
==>  Integer -> LookAhead ()
scan (Integer
n forall a. Num a => a -> a -> a
+ Integer
1)
                       , String
close  forall {a} {b}. a -> b -> (a, b)
==>  Integer -> LookAhead ()
scan (Integer
n forall a. Num a => a -> a -> a
- Integer
1)
                       ] forall {a} {b}. (a -> b) -> a -> b
`other` Integer -> LookAhead ()
scan Integer
n
            where
                ==> :: a -> b -> (a, b)
(==>) = (,)
                other :: (a -> b) -> a -> b
other = forall a b. (a -> b) -> a -> b
($)