{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE MagicHash #-}

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

import Agda.Utils.StrictReader qualified as Strict
import Agda.Utils.StrictWriter qualified as Strict
import Agda.Utils.StrictState  qualified as Strict

---------------------------------------------------------------------------
-- * 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
    CheckLocalRewriteConstraint{} -> 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

  {-# INLINE traceCall #-}
  -- | 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

  {-# INLINE traceCallM #-}
  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

  {-# INLINE traceCallCPS #-}
  -- | 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.
    e <- m TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
    let mcall = TCEnv
e TCEnv
-> Getting (Maybe (Closure Call)) TCEnv (Maybe (Closure Call))
-> Maybe (Closure Call)
forall s a. s -> Getting a s a -> a
^. Getting (Maybe (Closure Call)) TCEnv (Maybe (Closure Call))
Lens' TCEnv (Maybe (Closure Call))
eCall
        r     = TCEnv
e TCEnv -> Getting Range TCEnv Range -> Range
forall s a. s -> Getting a s a -> a
^. Getting Range TCEnv Range
Lens' TCEnv Range
eRange
        hr    = TCEnv
e TCEnv -> Getting Range TCEnv Range -> Range
forall s a. s -> Getting a s a -> a
^. Getting Range TCEnv Range
Lens' TCEnv Range
eHighlightingRange

    -- 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 (ASetter TCEnv TCEnv (Maybe (Closure Call)) (Maybe (Closure Call))
-> Maybe (Closure Call) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv (Maybe (Closure Call)) (Maybe (Closure Call))
Lens' TCEnv (Maybe (Closure Call))
eCall Maybe (Closure Call)
mcall (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter TCEnv TCEnv Range Range -> Range -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Range Range
Lens' TCEnv Range
eRange Range
r (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter TCEnv TCEnv Range Range -> Range -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Range Range
Lens' TCEnv Range
eHighlightingRange Range
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 (Strict.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
Strict.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
Strict.runReaderT ReaderT r m a
f r
r

instance MonadTrace m => MonadTrace (Strict.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 (Pair a s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (Pair a s)) -> StateT s m a
Strict.StateT (Closure Call -> m (Pair a s) -> m (Pair 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 (Pair a s) -> m (Pair a s))
-> (s -> m (Pair a s)) -> s -> m (Pair a s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT s m a -> s -> m (Pair a s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (Pair a s)
Strict.runStateT# StateT s m a
f)

instance (MonadTrace m, Monoid w) => MonadTrace (Strict.WriterT w m) where
  traceClosureCall :: forall a. Closure Call -> WriterT w m a -> WriterT w m a
traceClosureCall Closure Call
c (Strict.WriterT StateT w m a
f) = StateT w m a -> WriterT w m a
forall w (m :: * -> *) a. StateT w m a -> WriterT w m a
Strict.WriterT (StateT w m a -> WriterT w m a) -> StateT w m a -> WriterT w m a
forall a b. (a -> b) -> a -> b
$ Closure Call -> StateT w m a -> StateT w m a
forall a. Closure Call -> StateT w m a -> StateT w m a
forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
traceClosureCall Closure Call
c StateT 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
$
          [ [ ASetter TCEnv TCEnv (Maybe (Closure Call)) (Maybe (Closure Call))
-> Maybe (Closure Call) -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv (Maybe (Closure Call)) (Maybe (Closure Call))
Lens' TCEnv (Maybe (Closure Call))
eCall (Closure Call -> Maybe (Closure Call)
forall a. a -> Maybe a
Just Closure Call
cl) | Call -> Bool
interestingCall Call
call ]
          , [ ASetter TCEnv TCEnv Range Range -> Range -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Range Range
Lens' TCEnv Range
eHighlightingRange Range
callRange | Bool
callHasRange Bool -> Bool -> Bool
&& Bool
highlightCall Bool -> Bool -> Bool
|| Bool
isNoHighlighting ]
          , [ ASetter TCEnv TCEnv Range Range -> Range -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Range Range
Lens' TCEnv Range
eRange Range
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 -> HighlightingLevel -> Bool
forall a. a -> HighlightingLevel -> a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
highlightCall (HighlightingLevel -> Bool)
-> (HighlightingLevel -> Bool) -> HighlightingLevel -> Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` (HighlightingLevel
Interactive HighlightingLevel -> HighlightingLevel -> Bool
forall a. Eq a => a -> a -> Bool
==) (HighlightingLevel -> Bool)
-> TCMT IO HighlightingLevel -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv HighlightingLevel -> TCMT IO HighlightingLevel
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (HighlightingLevel -> f HighlightingLevel) -> TCEnv -> f TCEnv
Lens' TCEnv HighlightingLevel
eHighlightingLevel)
      {-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 <- Lens' TCEnv Range -> TCMT IO Range
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Range -> f Range) -> TCEnv -> f TCEnv
Lens' TCEnv Range
eHighlightingRange
        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
_ Bool
h     -> Bool
h
      CheckPragma{}             -> Bool
True
      CheckPrimitive{}          -> Bool
True
      CheckIsEmpty{}            -> Bool
True
      CheckConfluence{}         -> Bool
False
      CheckIApplyConfluence{}   -> Bool
False
      CheckLocalRewriteConstraint{} -> 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' SessionState ModuleToSource -> TCMT IO ModuleToSource
forall (m :: * -> *) a.
ReadTCState m =>
Lens' SessionState a -> m a
useSession (ModuleToSource -> f ModuleToSource)
-> SessionState -> f SessionState
Lens' SessionState ModuleToSource
lensModuleToSource
    method   <- viewTC eHighlightingMethod
    reportSDoc "highlighting" 90 $ 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 = Lens' TCEnv Range -> m Range
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Range -> f Range) -> TCEnv -> f TCEnv
Lens' TCEnv Range
eRange

-- | 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. Range' a -> Range' a
P.continuousPerLine Range
rPre)
  r' :: Ranges
r'        = Range -> Ranges
rToR (Range -> Range
forall 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