{-# 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