{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.Monad.Trace where

import Prelude hiding (null)

import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Identity
import Control.Monad.Writer

import qualified Data.Set as Set

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.Utils.Function

import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty (prettyShow)

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

interestingCall :: Call -> Bool
interestingCall :: Call -> Bool
interestingCall = \case
    InferVar{}              -> Bool
False
    InferDef{}              -> Bool
False
    CheckArguments Range
_ [] 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
    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
    Closure Call
cl <- Call -> m (Closure Call)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Call
call
    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
cl m a
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

  -- | Reset 'envCall' to previous value in the continuation.
  --
  -- Caveat: if the last 'traceCall' did not set an 'interestingCall',
  -- for example, only set the 'Range' with 'SetRange',
  -- we will revert to the last interesting call.
  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
    Maybe (Closure Call)
mcall <- (TCEnv -> Maybe (Closure Call)) -> m (Maybe (Closure Call))
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe (Closure Call)
envCall
    Call -> m b -> m b
forall a. Call -> m a -> m a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall Call
call (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ (a -> m b) -> m b
k ((a -> m b) -> m b) -> (a -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \ a
a -> do
      (m b -> m b)
-> (Closure Call -> m b -> m b)
-> Maybe (Closure Call)
-> m b
-> m b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m b -> m b
forall a. a -> a
id Closure Call -> m b -> m b
forall a. Closure Call -> m a -> m a
forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Maybe (Closure Call)
mcall (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

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 (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.)
    -- Thus, we no longer crash, but just report the alien range.
    -- -- Andreas, 2015-02-09 Make sure we do not set a range
    -- -- outside the current file
    [Char] -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> m () -> m ()
verboseS [Char]
"check.ranges" VerboseLevel
90 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      Maybe RangeFile -> (RangeFile -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
Strict.whenJust (Range -> Maybe RangeFile
rangeFile Range
callRange) ((RangeFile -> TCM ()) -> TCM ())
-> (RangeFile -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \RangeFile
f -> do
        Maybe AbsolutePath
currentFile <- (TCEnv -> Maybe AbsolutePath) -> TCMT IO (Maybe AbsolutePath)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe AbsolutePath
envCurrentPath
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe AbsolutePath
currentFile Maybe AbsolutePath -> Maybe AbsolutePath -> Bool
forall a. Eq a => a -> a -> Bool
/= AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Just (RangeFile -> AbsolutePath
rangeFilePath RangeFile
f)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          [Char] -> VerboseLevel -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"check.ranges" VerboseLevel
90 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
            Call -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Call
call [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
            [Char]
" is setting the current range to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Range -> [Char]
forall a. Show a => a -> [Char]
show Range
callRange [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
            [Char]
" which is outside of the current file " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe AbsolutePath -> [Char]
forall a. Show a => a -> [Char]
show Maybe AbsolutePath
currentFile

    -- 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
        Range
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
        Range -> Range -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadTrace m =>
Range -> Range -> m a -> m a
highlightAsTypeChecked Range
oldRange Range
callRange (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$
          TCM a -> TCM a
withCall TCM a
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
      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
    Map TopLevelModuleName AbsolutePath
modToSrc <- Lens' TCState (Map TopLevelModuleName AbsolutePath)
-> TCMT IO (Map TopLevelModuleName AbsolutePath)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map TopLevelModuleName AbsolutePath
 -> f (Map TopLevelModuleName AbsolutePath))
-> TCState -> f TCState
Lens' TCState (Map TopLevelModuleName AbsolutePath)
stModuleToSource
    HighlightingMethod
method   <- Lens' TCEnv HighlightingMethod -> TCMT IO HighlightingMethod
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (HighlightingMethod -> f HighlightingMethod) -> TCEnv -> f TCEnv
Lens' TCEnv HighlightingMethod
eHighlightingMethod
    [Char] -> VerboseLevel -> [[Char]] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> VerboseLevel -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [[Char]] -> m ()
reportS [Char]
"highlighting" VerboseLevel
50
      [ [Char]
"Printing highlighting info:"
      , HighlightingInfo -> [Char]
forall a. Show a => a -> [Char]
show HighlightingInfo
info
      , [Char]
"  modToSrc = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Map TopLevelModuleName AbsolutePath -> [Char]
forall a. Show a => a -> [Char]
show Map TopLevelModuleName AbsolutePath
modToSrc
      ]
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (HighlightingInfo -> Bool
forall a. Null a => a -> Bool
null HighlightingInfo
info) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      Response -> TCM ()
appInteractionOutputCallback (Response -> TCM ()) -> Response -> TCM ()
forall a b. (a -> b) -> a -> b
$
          HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> Map TopLevelModuleName AbsolutePath
-> Response
Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method Map TopLevelModuleName AbsolutePath
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
    a
v <- m a
m
    Ranges -> Aspects -> m ()
forall {m :: * -> *}. MonadTrace m => Ranges -> Aspects -> m ()
p Ranges
rs Aspects
y
    a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
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)