    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.Monad.Trace where

    import Prelude hiding (null)

    import Control.Monad.Except         ( ExceptT  (ExceptT  ), runExceptT   , throwError )
    import Control.Monad.Reader         ( ReaderT  (ReaderT  ), runReaderT   )
    import Control.Monad.State          ( StateT   (StateT   ), runStateT    )
    import Control.Monad.Trans.Identity ( IdentityT(IdentityT), runIdentityT )
    import Control.Monad.Trans.Maybe    ( MaybeT   (MaybeT   ), runMaybeT    )
    import Control.Monad.Writer         ( WriterT  (WriterT  ), runWriterT   )

    import qualified Data.Set as Set

    import Agda.Syntax.Common.Pretty
    import Agda.Syntax.Parser (PM, runPMIO)
    import Agda.Syntax.Position
    import qualified Agda.Syntax.Position as P

    import Agda.Interaction.Response
    import Agda.Interaction.Highlighting.Precise
    import Agda.Interaction.Highlighting.Range (rToR, minus)

    import Agda.TypeChecking.Monad.Base
      hiding (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype)
    import Agda.TypeChecking.Monad.Debug
    import Agda.TypeChecking.Monad.State
    import Agda.TypeChecking.Warnings (warning)

    import Agda.Utils.Function
    import Agda.Utils.Monad
    import Agda.Utils.Null

    ---------------------------------------------------------------------------
    -- * Trace
    ---------------------------------------------------------------------------

    interestingCall :: Call -> Bool
    interestingCall :: Call -> Bool
    interestingCall = \case
        InferVar{}              -> Bool
    False
        InferDef{}              -> Bool
    False
        CheckArguments Expr
    _ [] Type
    _ Maybe Type
    _ -> Bool
    False
        SetRange{}              -> Bool
    False
        NoHighlighting{}        -> Bool
    False
        -- Andreas, 2019-08-07, expanded catch-all pattern.
        -- The previous presence of a catch-all raises the following question:
        -- are all of the following really interesting?
        CheckClause{}             -> Bool
    True
        CheckLHS{}                -> Bool
    True
        CheckPattern{}            -> Bool
    True
        CheckPatternLinearityType{}  -> Bool
    True
        CheckPatternLinearityValue{} -> Bool
    True
        CheckLetBinding{}         -> Bool
    True
        InferExpr{}               -> Bool
    True
        CheckExprCall{}           -> Bool
    True
        CheckDotPattern{}         -> Bool
    True
        IsTypeCall{}              -> Bool
    True
        IsType_{}                 -> Bool
    True
        CheckArguments{}          -> Bool
    True
        CheckMetaSolution{}       -> Bool
    True
        CheckTargetType{}         -> Bool
    True
        CheckDataDef{}            -> Bool
    True
        CheckRecDef{}             -> Bool
    True
        CheckConstructor{}        -> Bool
    True
        CheckIApplyConfluence{}   -> Bool
    True
        CheckConArgFitsIn{}       -> Bool
    True
        CheckFunDefCall{}         -> Bool
    True
        CheckPragma{}             -> Bool
    True
        CheckPrimitive{}          -> Bool
    True
        CheckIsEmpty{}            -> Bool
    True
        CheckConfluence{}         -> Bool
    True
        CheckModuleParameters{}   -> Bool
    True
        CheckWithFunctionType{}   -> Bool
    True
        CheckSectionApplication{} -> Bool
    True
        CheckNamedWhere{}         -> Bool
    True
        ScopeCheckExpr{}          -> Bool
    True
        ScopeCheckDeclaration{}   -> Bool
    True
        ScopeCheckLHS{}           -> Bool
    True
        CheckProjection{}         -> Bool
    True
        ModuleContents{}          -> Bool
    True

    class (MonadTCEnv m, ReadTCState m) => MonadTrace m where

      -- | Record a function call in the trace.
      traceCall :: Call -> m a -> m a
      traceCall Call
    call m a
    m = do
        cl <- Call -> m (Closure Call)
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m) =>
    a -> m (Closure a)
    buildClosure Call
    call
        traceClosureCall cl m

      traceCallM :: m Call -> m a -> m a
      traceCallM m Call
    call m a
    m = (Call -> m a -> m a) -> m a -> Call -> m a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Call -> m a -> m a
    forall a. Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall m a
    m (Call -> m a) -> m Call -> m a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m Call
    call

      -- | Like 'traceCall', but resets 'envCall' and the current ranges to the
      --   previous values in the continuation.
      --
      traceCallCPS :: Call -> ((a -> m b) -> m b) -> ((a -> m b) -> m b)
      traceCallCPS Call
    call (a -> m b) -> m b
    k a -> m b
    ret = do

        -- Save current call and ranges.
        TCEnv{ envCall = mcall, envRange = r, envHighlightingRange = hr } <- m TCEnv
    forall (m :: * -> *). MonadTCEnv m => m TCEnv
    askTC

        -- Run given computation under given call.
        traceCall call $ k $ \ a
    a -> do

          -- Restore previous call and ranges for the continuation.
          (TCEnv -> TCEnv) -> m b -> m b
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    e -> TCEnv
    e{ envCall = mcall, envRange = r, envHighlightingRange = hr }) (m b -> m b) -> m b -> m b
    forall a b. (a -> b) -> a -> b
    $
            a -> m b
    ret a
    a

      traceClosureCall :: Closure Call -> m a -> m a

      -- | Lispify and print the given highlighting information.
      printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()

      default printHighlightingInfo
        :: (MonadTrans t, MonadTrace n, t n ~ m)
        => RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
      printHighlightingInfo RemoveTokenBasedHighlighting
    r HighlightingInfo
    i = n () -> t n ()
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n () -> t n ()) -> n () -> t n ()
    forall a b. (a -> b) -> a -> b
    $ RemoveTokenBasedHighlighting -> HighlightingInfo -> n ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    r HighlightingInfo
    i

    traceCallCPS' :: MonadTrace m => Call -> (m b -> m b) -> m b -> m b
    traceCallCPS' :: forall (m :: * -> *) b.
    MonadTrace m =>
    Call -> (m b -> m b) -> m b -> m b
    traceCallCPS' Call
    c m b -> m b
    k m b
    ret = Call -> ((() -> m b) -> m b) -> (() -> m b) -> m b
    forall a b. Call -> ((a -> m b) -> m b) -> (a -> m b) -> m b
    forall (m :: * -> *) a b.
    MonadTrace m =>
    Call -> ((a -> m b) -> m b) -> (a -> m b) -> m b
    traceCallCPS Call
    c (\() -> m b
    ret -> m b -> m b
    k (() -> m b
    ret ())) (\() -> m b
    ret)

    instance MonadTrace m => MonadTrace (IdentityT m) where
      traceClosureCall :: forall a. Closure Call -> IdentityT m a -> IdentityT m a
    traceClosureCall Closure Call
    c IdentityT m a
    f = m a -> IdentityT m a
    forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
    IdentityT (m a -> IdentityT m a) -> m a -> IdentityT m a
    forall a b. (a -> b) -> a -> b
    $ Closure Call -> m a -> m a
    forall a. Closure Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Closure Call
    c (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ IdentityT m a -> m a
    forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
    runIdentityT IdentityT m a
    f

    instance MonadTrace m => MonadTrace (MaybeT m) where
      traceClosureCall :: forall a. Closure Call -> MaybeT m a -> MaybeT m a
    traceClosureCall Closure Call
    c MaybeT m a
    f = m (Maybe a) -> MaybeT m a
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (m (Maybe a) -> MaybeT m a) -> m (Maybe a) -> MaybeT m a
    forall a b. (a -> b) -> a -> b
    $ Closure Call -> m (Maybe a) -> m (Maybe a)
    forall a. Closure Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Closure Call
    c (m (Maybe a) -> m (Maybe a)) -> m (Maybe a) -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ MaybeT m a -> m (Maybe a)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT MaybeT m a
    f

    instance MonadTrace m => MonadTrace (ReaderT r m) where
      traceClosureCall :: forall a. Closure Call -> ReaderT r m a -> ReaderT r m a
    traceClosureCall Closure Call
    c ReaderT r m a
    f = (r -> m a) -> ReaderT r m a
    forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
    ReaderT ((r -> m a) -> ReaderT r m a) -> (r -> m a) -> ReaderT r m a
    forall a b. (a -> b) -> a -> b
    $ \r
    r -> Closure Call -> m a -> m a
    forall a. Closure Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Closure Call
    c (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ ReaderT r m a -> r -> m a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT r m a
    f r
    r

    instance MonadTrace m => MonadTrace (StateT s m) where
      traceClosureCall :: forall a. Closure Call -> StateT s m a -> StateT s m a
    traceClosureCall Closure Call
    c StateT s m a
    f = (s -> m (a, s)) -> StateT s m a
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StateT (Closure Call -> m (a, s) -> m (a, s)
    forall a. Closure Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Closure Call
    c (m (a, s) -> m (a, s)) -> (s -> m (a, s)) -> s -> m (a, s)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT StateT s m a
    f)

    instance (MonadTrace m, Monoid w) => MonadTrace (WriterT w m) where
      traceClosureCall :: forall a. Closure Call -> WriterT w m a -> WriterT w m a
    traceClosureCall Closure Call
    c WriterT w m a
    f = m (a, w) -> WriterT w m a
    forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
    WriterT (m (a, w) -> WriterT w m a) -> m (a, w) -> WriterT w m a
    forall a b. (a -> b) -> a -> b
    $ Closure Call -> m (a, w) -> m (a, w)
    forall a. Closure Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Closure Call
    c (m (a, w) -> m (a, w)) -> m (a, w) -> m (a, w)
    forall a b. (a -> b) -> a -> b
    $ WriterT w m a -> m (a, w)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT WriterT w m a
    f

    instance MonadTrace m => MonadTrace (ExceptT e m) where
      traceClosureCall :: forall a. Closure Call -> ExceptT e m a -> ExceptT e m a
    traceClosureCall Closure Call
    c ExceptT e m a
    f = m (Either e a) -> ExceptT e m a
    forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
    ExceptT (m (Either e a) -> ExceptT e m a)
    -> m (Either e a) -> ExceptT e m a
    forall a b. (a -> b) -> a -> b
    $ Closure Call -> m (Either e a) -> m (Either e a)
    forall a. Closure Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Closure Call
    c (m (Either e a) -> m (Either e a))
    -> m (Either e a) -> m (Either e a)
    forall a b. (a -> b) -> a -> b
    $ ExceptT e m a -> m (Either e a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT ExceptT e m a
    f

    instance MonadTrace TCM where
      traceClosureCall :: forall a. Closure Call -> TCM a -> TCM a
    traceClosureCall Closure Call
    cl TCM a
    m = do
        -- Andreas, 2016-09-13 issue #2177
        -- Since the fix of #2092 we may report an error outside the current file.
        -- (For instance, if we import a module which then happens to have the
        -- wrong name.)

        -- Compute update to 'Range' and 'Call' components of 'TCEnv'.
        let withCall :: TCM a -> TCM a
    withCall = (TCEnv -> TCEnv) -> TCM a -> TCM a
    forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCM a -> TCM a)
    -> (TCEnv -> TCEnv) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ ((TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv)
    -> (TCEnv -> TCEnv) -> [TCEnv -> TCEnv] -> TCEnv -> TCEnv
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.) TCEnv -> TCEnv
    forall a. a -> a
    id ([TCEnv -> TCEnv] -> TCEnv -> TCEnv)
    -> [TCEnv -> TCEnv] -> TCEnv -> TCEnv
    forall a b. (a -> b) -> a -> b
    $ [[TCEnv -> TCEnv]] -> [TCEnv -> TCEnv]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[TCEnv -> TCEnv]] -> [TCEnv -> TCEnv])
    -> [[TCEnv -> TCEnv]] -> [TCEnv -> TCEnv]
    forall a b. (a -> b) -> a -> b
    $
              [ [ \TCEnv
    e -> TCEnv
    e { envCall = Just cl } | Call -> Bool
    interestingCall Call
    call ]
              , [ \TCEnv
    e -> TCEnv
    e { envHighlightingRange = callRange }
                | Bool
    callHasRange Bool -> Bool -> Bool
    && Bool
    highlightCall
                  Bool -> Bool -> Bool
    || Bool
    isNoHighlighting
                ]
              , [ \TCEnv
    e -> TCEnv
    e { envRange = callRange } | Bool
    callHasRange ]
              ]

        -- For interactive highlighting, also wrap computation @m@ in 'highlightAsTypeChecked':
        TCMT IO Bool -> TCM a -> TCM a -> TCM a
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    highlightCall TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` do (HighlightingLevel
    Interactive HighlightingLevel -> HighlightingLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (HighlightingLevel -> Bool)
    -> (TCEnv -> HighlightingLevel) -> TCEnv -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCEnv -> HighlightingLevel
    envHighlightingLevel (TCEnv -> Bool) -> TCMT IO TCEnv -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO TCEnv
    forall (m :: * -> *). MonadTCEnv m => m TCEnv
    askTC)
          {-then-} (TCM a -> TCM a
    withCall TCM a
    m)
          {-else-} (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ do
            oldRange <- TCEnv -> Range
    envHighlightingRange (TCEnv -> Range) -> TCMT IO TCEnv -> TCMT IO Range
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO TCEnv
    forall (m :: * -> *). MonadTCEnv m => m TCEnv
    askTC
            highlightAsTypeChecked oldRange callRange $
              withCall m
        where
        call :: Call
    call = Closure Call -> Call
    forall a. Closure a -> a
    clValue Closure Call
    cl
        callRange :: Range
    callRange = Call -> Range
    forall a. HasRange a => a -> Range
    getRange Call
    call
        callHasRange :: Bool
    callHasRange = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Range -> Bool
    forall a. Null a => a -> Bool
    null Range
    callRange

        -- Should the given call trigger interactive highlighting?
        highlightCall :: Bool
    highlightCall = case Call
    call of
          CheckClause{}             -> Bool
    True
          CheckLHS{}                -> Bool
    True
          CheckPattern{}            -> Bool
    True
          CheckPatternLinearityType{}  -> Bool
    False
          CheckPatternLinearityValue{} -> Bool
    False
          CheckLetBinding{}         -> Bool
    True
          InferExpr{}               -> Bool
    True
          CheckExprCall{}           -> Bool
    True
          CheckDotPattern{}         -> Bool
    True
          IsTypeCall{}              -> Bool
    True
          IsType_{}                 -> Bool
    True
          InferVar{}                -> Bool
    True
          InferDef{}                -> Bool
    True
          CheckArguments{}          -> Bool
    True
          CheckMetaSolution{}       -> Bool
    False
          CheckTargetType{}         -> Bool
    False
          CheckDataDef{}            -> Bool
    True
          CheckRecDef{}             -> Bool
    True
          CheckConstructor{}        -> Bool
    True
          CheckConArgFitsIn{}       -> Bool
    False
          CheckFunDefCall Range
    _ QName
    _ [Clause]
    _ Bool
    h   -> Bool
    h
          CheckPragma{}             -> Bool
    True
          CheckPrimitive{}          -> Bool
    True
          CheckIsEmpty{}            -> Bool
    True
          CheckConfluence{}         -> Bool
    False
          CheckIApplyConfluence{}   -> Bool
    False
          CheckModuleParameters{}   -> Bool
    False
          CheckWithFunctionType{}   -> Bool
    True
          CheckSectionApplication{} -> Bool
    True
          CheckNamedWhere{}         -> Bool
    False
          ScopeCheckExpr{}          -> Bool
    False
          ScopeCheckDeclaration{}   -> Bool
    False
          ScopeCheckLHS{}           -> Bool
    False
          NoHighlighting{}          -> Bool
    True
          CheckProjection{}         -> Bool
    False
          SetRange{}                -> Bool
    False
          ModuleContents{}          -> Bool
    False

        isNoHighlighting :: Bool
    isNoHighlighting = case Call
    call of
          NoHighlighting{} -> Bool
    True
          Call
    _ -> Bool
    False

      printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    remove HighlightingInfo
    info = do
        modToSrc <- Lens' TCState ModuleToSource -> TCMT IO ModuleToSource
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (ModuleToSource -> f ModuleToSource) -> TCState -> f TCState
    Lens' TCState ModuleToSource
    stModuleToSource
        method   <- viewTC eHighlightingMethod
        reportSDoc "highlighting" 50 $ pure $ vcat
          [ "Printing highlighting info:"
          , nest 2 $ (text . show) info
          , "File modules:"
          , nest 2 $ pretty modToSrc
          ]
        unless (null info) $ do
          appInteractionOutputCallback $
              Resp_HighlightingInfo info remove method modToSrc

    getCurrentRange :: MonadTCEnv m => m Range
    getCurrentRange :: forall (m :: * -> *). MonadTCEnv m => m Range
    getCurrentRange = (TCEnv -> Range) -> m Range
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Range
    envRange

    -- | Sets the current range (for error messages etc.) to the range
    --   of the given object, if it has a range (i.e., its range is not 'noRange').
    setCurrentRange :: (MonadTrace m, HasRange x) => x -> m a -> m a
    setCurrentRange :: forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange x
    x = Bool -> (m a -> m a) -> m a -> m a
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyUnless (Range -> Bool
    forall a. Null a => a -> Bool
    null Range
    r) ((m a -> m a) -> m a -> m a) -> (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Call -> m a -> m a
    forall a. Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Call -> m a -> m a) -> Call -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Range -> Call
    SetRange Range
    r
      where r :: Range
    r = x -> Range
    forall a. HasRange a => a -> Range
    getRange x
    x

    -- | @highlightAsTypeChecked rPre r m@ runs @m@ and returns its
    --   result. Additionally, some code may be highlighted:
    --
    -- * If @r@ is non-empty and not a sub-range of @rPre@ (after
    --   'P.continuousPerLine' has been applied to both): @r@ is
    --   highlighted as being type-checked while @m@ is running (this
    --   highlighting is removed if @m@ completes /successfully/).
    --
    -- * Otherwise: Highlighting is removed for @rPre - r@ before @m@
    --   runs, and if @m@ completes successfully, then @rPre - r@ is
    --   highlighted as being type-checked.

    highlightAsTypeChecked
      :: (MonadTrace m)
      => Range   -- ^ @rPre@
      -> Range   -- ^ @r@
      -> m a
      -> m a
    highlightAsTypeChecked :: forall (m :: * -> *) a.
    MonadTrace m =>
    Range -> Range -> m a -> m a
    highlightAsTypeChecked Range
    rPre Range
    r m a
    m
      | Range
    r Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Range
    forall a. Range' a
    noRange Bool -> Bool -> Bool
    && Ranges
    delta Ranges -> Ranges -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ranges
    rPre' = Ranges -> Aspects -> Aspects -> m a
    wrap Ranges
    r'    Aspects
    highlight Aspects
    clear
      | Bool
    otherwise                      = Ranges -> Aspects -> Aspects -> m a
    wrap Ranges
    delta Aspects
    clear     Aspects
    highlight
      where
      rPre' :: Ranges
    rPre'     = Range -> Ranges
    rToR (Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine Range
    rPre)
      r' :: Ranges
    r'        = Range -> Ranges
    rToR (Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine Range
    r)
      delta :: Ranges
    delta     = Ranges
    rPre' Ranges -> Ranges -> Ranges
    `minus` Ranges
    r'
      clear :: Aspects
    clear     = Aspects
    forall a. Monoid a => a
    mempty
      highlight :: Aspects
    highlight = Aspects
    parserBased { otherAspects = Set.singleton TypeChecks }

      wrap :: Ranges -> Aspects -> Aspects -> m a
    wrap Ranges
    rs Aspects
    x Aspects
    y = do
        Ranges -> Aspects -> m ()
    forall {m :: * -> *}. MonadTrace m => Ranges -> Aspects -> m ()
    p Ranges
    rs Aspects
    x
        v <- m a
    m
        p rs y
        return v
        where
        p :: Ranges -> Aspects -> m ()
    p Ranges
    rs Aspects
    x = RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting (Ranges -> Aspects -> HighlightingInfo
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    singleton Ranges
    rs Aspects
    x)

    ---------------------------------------------------------------------------
    -- * Warnings in the parser
    ---------------------------------------------------------------------------

    -- | Running the Parse monad, raising parser warnings.

    runPM :: PM a -> TCM a
    runPM :: forall a. PM a -> TCM a
    runPM PM a
    m = do
      (res, ws) <- PM a -> TCMT IO (Either ParseError a, [ParseWarning])
    forall (m :: * -> *) a.
    MonadIO m =>
    PM a -> m (Either ParseError a, [ParseWarning])
    runPMIO PM a
    m
      forM_ ws \ ParseWarning
    w -> ParseWarning -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange ParseWarning
    w (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ParseWarning -> Warning
    ParseWarning ParseWarning
    w
      case res of
        Left  ParseError
    e -> TCErr -> TCMT IO a
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (TCErr -> TCMT IO a) -> TCErr -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ ParseError -> TCErr
    ParserError ParseError
    e
        Right a
    a -> a -> TCMT IO a
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

    -- | Running the Parse monad, dropping parser warnings.

    runPMDropWarnings :: PM a -> TCM a
    runPMDropWarnings :: forall a. PM a -> TCM a
    runPMDropWarnings PM a
    m = do
      (res, _ws) <- PM a -> TCMT IO (Either ParseError a, [ParseWarning])
    forall (m :: * -> *) a.
    MonadIO m =>
    PM a -> m (Either ParseError a, [ParseWarning])
    runPMIO PM a
    m
      case res of
        Left  ParseError
    e -> TCErr -> TCMT IO a
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (TCErr -> TCMT IO a) -> TCErr -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ ParseError -> TCErr
    ParserError ParseError
    e
        Right a
    a -> a -> TCMT IO a
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a