    {-| 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 -> PreviousInput -> LexState -> Parser Token)
    -> LexAction Token
    forall r.
    (PreviousInput -> PreviousInput -> LexState -> Parser r)
    -> LexAction r
    LexAction ((PreviousInput -> PreviousInput -> LexState -> Parser Token)
     -> LexAction Token)
    -> (PreviousInput -> PreviousInput -> LexState -> Parser Token)
    -> LexAction Token
    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
    _ = 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 '{-'"
            (forall a. String -> LookAhead a) -> LookAhead () -> Parser ()
    forall a.
    (forall a. String -> LookAhead a) -> LookAhead a -> Parser a
    runLookAhead forall a. String -> 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

    -- | Lex a hole (@{! ... !}@). Holes can be nested.
    --   Returns @'TokSymbol' 'SymQuestionMark'@.
    hole :: LexAction Token
    hole :: LexAction Token
    hole = (PreviousInput -> PreviousInput -> LexState -> Parser Token)
    -> LexAction Token
    forall r.
    (PreviousInput -> PreviousInput -> LexState -> Parser r)
    -> LexAction r
    LexAction ((PreviousInput -> PreviousInput -> LexState -> Parser Token)
     -> LexAction Token)
    -> (PreviousInput -> PreviousInput -> LexState -> Parser Token)
    -> LexAction Token
    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
    _ = 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 '{!'"
            (forall a. String -> LookAhead a) -> LookAhead () -> Parser ()
    forall a.
    (forall a. String -> LookAhead a) -> LookAhead a -> Parser a
    runLookAhead forall a. String -> 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

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