{-# LANGUAGE CPP #-}

module Agda.TypeChecking.Monad.Debug
  ( module Agda.TypeChecking.Monad.Debug
  , Verbosity, VerboseKey, VerboseLevel
  ) where

import qualified Control.Exception as E
import qualified Control.DeepSeq as DeepSeq (force)

import Control.Applicative          ( liftA2 )
import Control.Monad.IO.Class       ( MonadIO(..) )
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Control  ( MonadTransControl(..), liftThrough )
import Control.Monad.Trans.Maybe
import Control.Monad.Trans.Identity
import Control.Monad.Writer

import Data.Maybe
import Data.Time                    ( getCurrentTime, getCurrentTimeZone, utcToLocalTime )
import Data.Time.Format.ISO8601     ( iso8601Show )

import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.Base
-- import Agda.TypeChecking.Monad.State ( appInteractionOutputCallback )  -- import cycle

import Agda.Interaction.Options
import Agda.Interaction.Response.Base (Response_boot(..))

import Agda.Utils.CallStack ( HasCallStack, withCallerCallStack )
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Syntax.Common.Pretty
import Agda.Interaction.Options.ProfileOptions
import Agda.Utils.Update
import qualified Agda.Utils.Trie as Trie

import Agda.Utils.Impossible
import Agda.Utils.DocTree (renderToTree)

class (Functor m, Applicative m, Monad m) => MonadDebug m where

  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> m Doc
  traceDebugMessage  :: VerboseKey -> VerboseLevel -> Doc -> m a -> m a

  -- | Print brackets around debug messages issued by a computation.
  verboseBracket     :: VerboseKey -> VerboseLevel -> String -> m a -> m a

  getVerbosity       :: m Verbosity
  getProfileOptions  :: m ProfileOptions

  -- | Check whether we are currently debug printing.
  isDebugPrinting    :: m Bool

  -- | Flag in a computation that we are currently debug printing.
  nowDebugPrinting   :: m a -> m a

  -- default implementation of transformed debug monad

  default formatDebugMessage
    :: (MonadTrans t, MonadDebug n, m ~ t n)
    => VerboseKey -> VerboseLevel -> TCM Doc -> m Doc
  formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d = n Doc -> t n Doc
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 Doc -> t n Doc) -> n Doc -> t n Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> n Doc
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m Doc
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d

  default traceDebugMessage
    :: (MonadTransControl t, MonadDebug n, m ~ t n)
    => VerboseKey -> VerboseLevel -> Doc -> m a -> m a
  traceDebugMessage VerboseKey
k VerboseLevel
n Doc
s = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTransControl t, Monad (t m), Monad m) =>
(m (StT t a) -> m (StT t b)) -> t m a -> t m b
liftThrough ((n (StT t a) -> n (StT t a)) -> t n a -> t n a)
-> (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> Doc -> n (StT t a) -> n (StT t a)
forall a. VerboseKey -> VerboseLevel -> Doc -> n a -> n a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n Doc
s

#ifdef DEBUG
  default verboseBracket
    :: (MonadTransControl t, MonadDebug n, m ~ t n)
    => VerboseKey -> VerboseLevel -> String -> m a -> m a
  verboseBracket k n s = liftThrough $ verboseBracket k n s
#else
  default verboseBracket
    :: (MonadTransControl t, MonadDebug n, m ~ t n)
    => VerboseKey -> VerboseLevel -> String -> m a -> m a
  verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s m a
ma = m a
ma
  {-# INLINE verboseBracket #-}
#endif

  default getVerbosity
    :: (MonadTrans t, MonadDebug n, m ~ t n)
    => m Verbosity
  getVerbosity = n Verbosity -> t n Verbosity
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 Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity

  default getProfileOptions
    :: (MonadTrans t, MonadDebug n, m ~ t n)
    => m ProfileOptions
  getProfileOptions = n ProfileOptions -> t n ProfileOptions
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 ProfileOptions
forall (m :: * -> *). MonadDebug m => m ProfileOptions
getProfileOptions

  default isDebugPrinting
    :: (MonadTrans t, MonadDebug n, m ~ t n)
    => m Bool
  isDebugPrinting = n Bool -> t n Bool
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 Bool
forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting

  default nowDebugPrinting
    :: (MonadTransControl t, MonadDebug n, m ~ t n)
    => m a -> m a
  nowDebugPrinting = (n (StT t a) -> n (StT t a)) -> t n a -> t n a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTransControl t, Monad (t m), Monad m) =>
(m (StT t a) -> m (StT t b)) -> t m a -> t m b
liftThrough n (StT t a) -> n (StT t a)
forall a. n a -> n a
forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting

-- Default implementations (working around the restriction to only
-- have one default signature).

defaultGetVerbosity :: HasOptions m => m Verbosity
defaultGetVerbosity :: forall (m :: * -> *). HasOptions m => m Verbosity
defaultGetVerbosity = PragmaOptions -> Verbosity
optVerbose (PragmaOptions -> Verbosity) -> m PragmaOptions -> m Verbosity
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

defaultGetProfileOptions :: HasOptions m => m ProfileOptions
defaultGetProfileOptions :: forall (m :: * -> *). HasOptions m => m ProfileOptions
defaultGetProfileOptions = PragmaOptions -> ProfileOptions
optProfiling (PragmaOptions -> ProfileOptions)
-> m PragmaOptions -> m ProfileOptions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

defaultIsDebugPrinting :: MonadTCEnv m => m Bool
defaultIsDebugPrinting :: forall (m :: * -> *). MonadTCEnv m => m Bool
defaultIsDebugPrinting = (TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envIsDebugPrinting

defaultNowDebugPrinting :: MonadTCEnv m => m a -> m a
defaultNowDebugPrinting :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
defaultNowDebugPrinting = Lens' TCEnv Bool -> (Bool -> Bool) -> m a -> m a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eIsDebugPrinting ((Bool -> Bool) -> m a -> m a) -> (Bool -> Bool) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True

-- | Print a debug message if switched on.
displayDebugMessage :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m ()
displayDebugMessage :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n Doc
s = VerboseKey -> VerboseLevel -> Doc -> m () -> m ()
forall a. VerboseKey -> VerboseLevel -> Doc -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n Doc
s (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | During printing, catch internal errors of kind 'Impossible' and print them.
catchAndPrintImpossible
  :: (CatchImpossible m, Monad m)
  => VerboseKey -> VerboseLevel -> m DocTree -> m DocTree
{-# SPECIALIZE catchAndPrintImpossible :: VerboseKey -> VerboseLevel -> TCM DocTree -> TCM DocTree #-}
catchAndPrintImpossible :: forall (m :: * -> *).
(CatchImpossible m, Monad m) =>
VerboseKey -> VerboseLevel -> m DocTree -> m DocTree
catchAndPrintImpossible VerboseKey
k VerboseLevel
n m DocTree
m = (Impossible -> Maybe Impossible)
-> m DocTree -> (Impossible -> m DocTree) -> m DocTree
forall b a. (Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
forall (m :: * -> *) b a.
CatchImpossible m =>
(Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
catchImpossibleJust Impossible -> Maybe Impossible
catchMe m DocTree
m ((Impossible -> m DocTree) -> m DocTree)
-> (Impossible -> m DocTree) -> m DocTree
forall a b. (a -> b) -> a -> b
$ \ Impossible
imposs -> do
  DocTree -> m DocTree
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DocTree -> m DocTree) -> DocTree -> m DocTree
forall a b. (a -> b) -> a -> b
$ Doc -> DocTree
forall ann. Null ann => Doc ann -> DocTree ann
renderToTree (Doc -> DocTree) -> Doc -> DocTree
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
    [ VerboseKey -> Doc
forall a. VerboseKey -> Doc a
text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Debug printing " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
k VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
":" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
n VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" failed due to exception:"
    , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (VerboseKey -> Doc) -> [VerboseKey] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> Doc -> Doc
forall a. VerboseLevel -> Doc a -> Doc a
nest VerboseLevel
2 (Doc -> Doc) -> (VerboseKey -> Doc) -> VerboseKey -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> Doc
forall a. VerboseKey -> Doc a
text) ([VerboseKey] -> [Doc]) -> [VerboseKey] -> [Doc]
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [VerboseKey]
lines (VerboseKey -> [VerboseKey]) -> VerboseKey -> [VerboseKey]
forall a b. (a -> b) -> a -> b
$ Impossible -> VerboseKey
forall a. Show a => a -> VerboseKey
show Impossible
imposs
    ]
  where
  -- Exception filter: Catch only the 'Impossible' exception during debug printing.
  catchMe :: Impossible -> Maybe Impossible
  catchMe :: Impossible -> Maybe Impossible
catchMe = (Impossible -> Bool) -> Impossible -> Maybe Impossible
forall a. (a -> Bool) -> a -> Maybe a
filterMaybe ((Impossible -> Bool) -> Impossible -> Maybe Impossible)
-> (Impossible -> Bool) -> Impossible -> Maybe Impossible
forall a b. (a -> b) -> a -> b
$ \case
    Impossible{}            -> Bool
True
    Unreachable{}           -> Bool
False
    ImpMissingDefinitions{} -> Bool
False

traceDebugMessageTCM :: VerboseKey -> VerboseLevel -> Doc -> TCM a -> TCM a
traceDebugMessageTCM :: forall a. VerboseKey -> VerboseLevel -> Doc -> TCM a -> TCM a
traceDebugMessageTCM VerboseKey
k VerboseLevel
n Doc
doc TCM a
cont = do
    -- Andreas, 2025-07-30, PR #8040:
    -- Forcing the @doc@ introduces a massive space leak,
    -- so for now we switch off the fix of #4016 which is just devx.
    -- This means that attempts to debug-print __IMPOSSIBLE__s will result in internal errors again.

    -- Andreas, 2022-06-15, prefix with time stamp if `-v debug.time:100`:
    doc <- TCMT IO Bool -> TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (VerboseKey -> VerboseLevel -> TCMT IO Bool
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
"debug.time" VerboseLevel
100) {-then-} (Doc -> TCM Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
doc) {-else-} (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ do
      now <- IO VerboseKey -> TCMT IO VerboseKey
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO VerboseKey -> TCMT IO VerboseKey)
-> IO VerboseKey -> TCMT IO VerboseKey
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseKey
trailingZeros (VerboseKey -> VerboseKey)
-> (LocalTime -> VerboseKey) -> LocalTime -> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalTime -> VerboseKey
forall t. ISO8601 t => t -> VerboseKey
iso8601Show (LocalTime -> VerboseKey) -> IO LocalTime -> IO VerboseKey
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TimeZone -> UTCTime -> LocalTime)
-> IO TimeZone -> IO UTCTime -> IO LocalTime
forall a b c. (a -> b -> c) -> IO a -> IO b -> IO c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 TimeZone -> UTCTime -> LocalTime
utcToLocalTime IO TimeZone
getCurrentTimeZone IO UTCTime
getCurrentTime
      pure $ (text now <> ":") <+> doc

    -- Andreas, 2019-08-20, issue #4016:
    -- Force any lazy 'Impossible' exceptions to the surface and handle them.
    msg :: DocTree <- liftIO . catchAndPrintImpossible k n . E.evaluate . DeepSeq.force . renderToTree $ doc
    cb <- useTC $ stInteractionOutputCallback
    cb $ Resp_RunningInfo n msg
    cont
    where
    -- Surprisingly, iso8601Show gives us _up to_ 6 fractional digits (microseconds),
    -- but not exactly 6.  https://github.com/haskell/time/issues/211
    -- So we need to do the padding ourselves.
    -- yyyy-mm-ddThh:mm:ss.ssssss
    -- 12345678901234567890123456
    trailingZeros :: VerboseKey -> VerboseKey
trailingZeros = Char -> Integer -> VerboseKey -> VerboseKey
forall a n. Integral n => a -> n -> [a] -> [a]
takeExactly Char
'0' Integer
26

formatDebugMessageTCM :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM Doc
formatDebugMessageTCM :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM Doc
formatDebugMessageTCM VerboseKey
_ VerboseLevel
_ = TCM Doc -> TCM Doc
forall a. a -> a
id

verboseBracketTCM :: VerboseKey -> VerboseLevel -> String -> TCM a -> TCM a
#ifdef DEBUG
verboseBracketTCM k n s =
  applyWhenVerboseS k n $ \ m -> do
    openVerboseBracket k n s
    (m <* closeVerboseBracket k n) `catchError` \ e -> do
      closeVerboseBracketException k n
      throwError e
#else
verboseBracketTCM :: forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
verboseBracketTCM VerboseKey
_ VerboseLevel
_ VerboseKey
_ = TCM a -> TCM a
forall a. a -> a
id
{-# INLINE verboseBracketTCM #-}
#endif

instance MonadDebug TCM where
  traceDebugMessage :: forall a. VerboseKey -> VerboseLevel -> Doc -> TCM a -> TCM a
traceDebugMessage = VerboseKey -> VerboseLevel -> Doc -> TCM a -> TCM a
forall a. VerboseKey -> VerboseLevel -> Doc -> TCM a -> TCM a
traceDebugMessageTCM
  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM Doc
formatDebugMessage= VerboseKey -> VerboseLevel -> TCM Doc -> TCM Doc
formatDebugMessageTCM
  verboseBracket :: forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
verboseBracket    = VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
verboseBracketTCM
  getVerbosity :: TCM Verbosity
getVerbosity      = TCM Verbosity
forall (m :: * -> *). HasOptions m => m Verbosity
defaultGetVerbosity
  getProfileOptions :: TCM ProfileOptions
getProfileOptions = TCM ProfileOptions
forall (m :: * -> *). HasOptions m => m ProfileOptions
defaultGetProfileOptions
  isDebugPrinting :: TCMT IO Bool
isDebugPrinting   = TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
defaultIsDebugPrinting
  nowDebugPrinting :: forall a. TCM a -> TCM a
nowDebugPrinting  = TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
defaultNowDebugPrinting

-- MonadTrans default instances

deriving instance MonadDebug m => MonadDebug (BlockT m)  -- ghc <= 8.0, GeneralizedNewtypeDeriving
instance MonadDebug m => MonadDebug (ChangeT m)
instance MonadDebug m => MonadDebug (ExceptT e m)
instance MonadDebug m => MonadDebug (MaybeT m)
instance MonadDebug m => MonadDebug (ReaderT r m)
instance MonadDebug m => MonadDebug (StateT s m)
instance (MonadDebug m, Monoid w) => MonadDebug (WriterT w m)
instance MonadDebug m => MonadDebug (IdentityT m)

-- We are lacking MonadTransControl ListT

instance MonadDebug m => MonadDebug (ListT m) where
  traceDebugMessage :: forall a.
VerboseKey -> VerboseLevel -> Doc -> ListT m a -> ListT m a
traceDebugMessage VerboseKey
k VerboseLevel
n Doc
s = (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT ((forall a1. m a1 -> m a1) -> ListT m a -> ListT m a)
-> (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> Doc -> m a1 -> m a1
forall a. VerboseKey -> VerboseLevel -> Doc -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n Doc
s
  verboseBracket :: forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> ListT m a -> ListT m a
verboseBracket    VerboseKey
k VerboseLevel
n VerboseKey
s = (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT ((forall a1. m a1 -> m a1) -> ListT m a -> ListT m a)
-> (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> m a1 -> m a1
forall a. VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s
  nowDebugPrinting :: forall a. ListT m a -> ListT m a
nowDebugPrinting        = (forall a1. m a1 -> m a1) -> ListT m a -> ListT m a
forall (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT m a1 -> m a1
forall a1. m a1 -> m a1
forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting

-- | Debug print some lines if the verbosity level for the given
--   'VerboseKey' is at least 'VerboseLevel'.
--
-- Note: In the presence of @OverloadedStrings@, just
-- @@
--   reportS key level "Literate string"
-- @@
-- gives an @Ambiguous type variable@ error in @GHC@.
-- Use the legacy functions 'reportSLn' and 'reportSDoc' instead then.
--
class ReportS a where
  reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m ()

instance ReportS (TCM Doc) where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportS = VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc
instance ReportS String    where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportS = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn

instance ReportS [TCM Doc] where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> [TCM Doc] -> m ()
reportS VerboseKey
k VerboseLevel
n = VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
k VerboseLevel
n (TCM Doc -> m ()) -> ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Doc] -> Doc) -> TCMT IO [Doc] -> TCM Doc
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (TCMT IO [Doc] -> TCM Doc)
-> ([TCM Doc] -> TCMT IO [Doc]) -> [TCM Doc] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCM Doc] -> TCMT IO [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
instance ReportS [String]  where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> [VerboseKey] -> m ()
reportS VerboseKey
k VerboseLevel
n = VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
k VerboseLevel
n (VerboseKey -> m ())
-> ([VerboseKey] -> VerboseKey) -> [VerboseKey] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VerboseKey] -> VerboseKey
unlines
instance ReportS [Doc]     where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> [Doc] -> m ()
reportS VerboseKey
k VerboseLevel
n = VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
k VerboseLevel
n (TCM Doc -> m ()) -> ([Doc] -> TCM Doc) -> [Doc] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TCM Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> TCM Doc) -> ([Doc] -> Doc) -> [Doc] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
instance ReportS Doc       where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> m ()
reportS VerboseKey
k VerboseLevel
n = VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
k VerboseLevel
n (TCM Doc -> m ()) -> (Doc -> TCM Doc) -> Doc -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TCM Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Conditionally println debug string. Works regardless of the debug flag.
{-# SPECIALIZE alwaysReportSLn :: VerboseKey -> VerboseLevel -> String -> TCM () #-}
alwaysReportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
alwaysReportSLn :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
alwaysReportSLn VerboseKey
k VerboseLevel
n VerboseKey
s = VerboseKey -> VerboseLevel -> VerboseKey -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
alwaysTraceSLn VerboseKey
k VerboseLevel
n VerboseKey
s (() -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

-- | Conditionally render debug 'Doc' and print it. Works regardless of the debug flag.
{-# SPECIALIZE alwaysReportSDoc :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM () #-}
alwaysReportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
alwaysReportSDoc :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
alwaysReportSDoc VerboseKey
k VerboseLevel
n TCM Doc
d = VerboseKey -> VerboseLevel -> TCM Doc -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
alwaysTraceSDoc VerboseKey
k VerboseLevel
n TCM Doc
d (() -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

-- | Conditionally println debug string.
--
reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
#ifdef DEBUG
reportSLn = alwaysReportSLn
#else
reportSLn :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
_ VerboseLevel
_ VerboseKey
_ = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
#endif
{-# INLINE reportSLn #-}

-- | Conditionally render debug 'Doc' and print it.
--
reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
#ifdef DEBUG
reportSDoc = alwaysReportSDoc
#else
reportSDoc :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
_ VerboseLevel
_ TCM Doc
_ = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
#endif
{-# INLINE reportSDoc #-}

-- | Raise internal error with extra information.
__IMPOSSIBLE_VERBOSE__ :: (HasCallStack, MonadDebug m) => String -> m a
__IMPOSSIBLE_VERBOSE__ :: forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
VerboseKey -> m a
__IMPOSSIBLE_VERBOSE__ VerboseKey
s = do
  -- Andreas, 2023-07-19, issue #6728 is fixed by manually inlining reportSLn here.
  -- reportSLn "impossible" 10 s
  -- It seems like GHC 9.6 optimization does otherwise something that throws
  -- away the debug message.
  -- let k = "impossible"
  -- let n = 10
  -- verboseS k n $ displayDebugMessage k n $ text s
  -- throwImpossible err
  -- Andreas, 2025-08-01: Does it work with traceSLn?
  VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceSLn VerboseKey
"impossible" VerboseLevel
10 VerboseKey
s (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ Impossible -> m a
forall a. Impossible -> a
throwImpossible Impossible
err
  where
    -- Create the "Impossible" error using *our* caller as the call site.
    err :: Impossible
err = (CallStack -> Impossible) -> Impossible
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Impossible
Impossible

-- | Debug print the result of a computation.
--
reportResult :: MonadDebug m => VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
#ifdef DEBUG
reportResult k n debug action = do
  x <- action
  x <$ reportSDoc k n (debug x)
#else
reportResult :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
reportResult VerboseKey
_ VerboseLevel
_ a -> TCM Doc
_ = m a -> m a
forall a. a -> a
id
{-# INLINE reportResult #-}
#endif

unlessDebugPrinting :: MonadDebug m => m () -> m ()
unlessDebugPrinting :: forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM m Bool
forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting
{-# INLINE unlessDebugPrinting #-}

-- | Debug print some lines if the verbosity level for the given
--   'VerboseKey' is at least 'VerboseLevel'.
--
-- Note: In the presence of @OverloadedStrings@, just
-- @@
--   traceS key level "Literate string"
-- @@
-- gives an @Ambiguous type variable@ error in @GHC@.
-- Use the legacy functions 'traceSLn' and 'traceSDoc' instead then.
--
class TraceS a where
  traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m c -> m c

instance TraceS (TCM Doc) where traceS :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceS = VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc
instance TraceS String    where traceS :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceS = VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceSLn

instance TraceS [TCM Doc] where traceS :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c
traceS VerboseKey
k VerboseLevel
n = VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
k VerboseLevel
n (TCM Doc -> m c -> m c)
-> ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> m c -> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Doc] -> Doc) -> TCMT IO [Doc] -> TCM Doc
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (TCMT IO [Doc] -> TCM Doc)
-> ([TCM Doc] -> TCMT IO [Doc]) -> [TCM Doc] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCM Doc] -> TCMT IO [Doc]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
instance TraceS [String]  where traceS :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> [VerboseKey] -> m c -> m c
traceS VerboseKey
k VerboseLevel
n = VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceSLn  VerboseKey
k VerboseLevel
n (VerboseKey -> m c -> m c)
-> ([VerboseKey] -> VerboseKey) -> [VerboseKey] -> m c -> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VerboseKey] -> VerboseKey
unlines
instance TraceS [Doc]     where traceS :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c
traceS VerboseKey
k VerboseLevel
n = VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
k VerboseLevel
n (TCM Doc -> m c -> m c)
-> ([Doc] -> TCM Doc) -> [Doc] -> m c -> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TCM Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> TCM Doc) -> ([Doc] -> Doc) -> [Doc] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
instance TraceS Doc       where traceS :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> m c -> m c
traceS VerboseKey
k VerboseLevel
n = VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
k VerboseLevel
n (TCM Doc -> m c -> m c) -> (Doc -> TCM Doc) -> Doc -> m c -> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TCM Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Conditionally debug print 'String', and then continue. Works regardless of the debug flag.
alwaysTraceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a
alwaysTraceSLn :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
alwaysTraceSLn VerboseKey
k VerboseLevel
n VerboseKey
s = VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n ((m a -> m a) -> m a -> m a) -> (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> Doc -> m a -> m a
forall a. VerboseKey -> VerboseLevel -> Doc -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n (Doc -> m a -> m a) -> Doc -> m a -> m a
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Doc
forall a. VerboseKey -> Doc a
text VerboseKey
s

-- | Conditionally render debug 'Doc', print it, and then continue. Works regardless of the debug flag.
alwaysTraceSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
alwaysTraceSDoc :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
alwaysTraceSDoc VerboseKey
k VerboseLevel
n TCM Doc
d = VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n ((m a -> m a) -> m a -> m a) -> (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ \m a
cont -> do
  doc <- VerboseKey -> VerboseLevel -> TCM Doc -> m Doc
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m Doc
formatDebugMessage VerboseKey
k VerboseLevel
n (TCM Doc -> m Doc) -> TCM Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Lens' TCEnv Bool -> (Bool -> Bool) -> TCM Doc -> TCM Doc
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eIsDebugPrinting (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) TCM Doc
d
  traceDebugMessage k n doc cont

-- | Conditionally debug print 'String', and then continue. Works regardless of the debug flag.
--
traceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a
#ifdef DEBUG
traceSLn = alwaysTraceSLn
#else
traceSLn :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceSLn VerboseKey
_ VerboseLevel
_ VerboseKey
_ = m a -> m a
forall a. a -> a
id
#endif
{-# INLINE traceSLn #-}

-- | Conditionally render debug 'Doc', print it, and then continue.
--
traceSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
#ifdef DEBUG
traceSDoc = alwaysTraceSDoc
#else
traceSDoc :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc VerboseKey
_ VerboseLevel
_ TCM Doc
_ = m a -> m a
forall a. a -> a
id
#endif
{-# INLINE traceSDoc #-}


openVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
openVerboseBracket :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
openVerboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = VerboseKey -> VerboseLevel -> Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n (Doc -> m ()) -> Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc
"{" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> VerboseKey -> Doc
forall a. VerboseKey -> Doc a
text VerboseKey
s

closeVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> m ()
closeVerboseBracket :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracket VerboseKey
k VerboseLevel
n = VerboseKey -> VerboseLevel -> Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n Doc
"}"

closeVerboseBracketException :: MonadDebug m => VerboseKey -> VerboseLevel -> m ()
closeVerboseBracketException :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracketException VerboseKey
k VerboseLevel
n = VerboseKey -> VerboseLevel -> Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> Doc -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n Doc
"} (exception)"


------------------------------------------------------------------------
-- Verbosity

-- Invariant (which we may or may not currently break): Debug
-- printouts use one of the following functions:
--
--   reportS
--   reportSLn
--   reportSDoc

-- | Get the verbosity level for a given key.
getVerbosityLevel :: MonadDebug m => VerboseKey -> m VerboseLevel
getVerbosityLevel :: forall (m :: * -> *). MonadDebug m => VerboseKey -> m VerboseLevel
getVerbosityLevel VerboseKey
k = do
  t <- m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  return $ case t of
    Verbosity
Strict.Nothing -> VerboseLevel
1
    Strict.Just Trie VerboseKeyItem VerboseLevel
t
      -- This code is not executed if no debug flags have been given.
      | Trie VerboseKeyItem VerboseLevel
t Trie VerboseKeyItem VerboseLevel
-> Trie VerboseKeyItem VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== [VerboseKeyItem]
-> VerboseLevel -> Trie VerboseKeyItem VerboseLevel
forall k v. [k] -> v -> Trie k v
Trie.singleton [] VerboseLevel
0 -> VerboseLevel
0 -- A special case for "-v0".
      | Bool
otherwise -> VerboseLevel -> [VerboseLevel] -> VerboseLevel
forall a. a -> [a] -> a
lastWithDefault VerboseLevel
0 ([VerboseLevel] -> VerboseLevel) -> [VerboseLevel] -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ [VerboseKeyItem]
-> Trie VerboseKeyItem VerboseLevel -> [VerboseLevel]
forall k v. Ord k => [k] -> Trie k v -> [v]
Trie.lookupPath [VerboseKeyItem]
ks Trie VerboseKeyItem VerboseLevel
t
  where ks :: [VerboseKeyItem]
ks = VerboseKey -> [VerboseKeyItem]
parseVerboseKey VerboseKey
k

-- | Check whether a certain verbosity level is activated.
--
--   Precondition: The level must be non-negative.
{-# SPECIALIZE hasVerbosity :: VerboseKey -> VerboseLevel -> TCM Bool #-}
hasVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
hasVerbosity :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
k VerboseLevel
n = (VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<=) (VerboseLevel -> Bool) -> m VerboseLevel -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseKey -> m VerboseLevel
forall (m :: * -> *). MonadDebug m => VerboseKey -> m VerboseLevel
getVerbosityLevel VerboseKey
k

-- | Check whether a certain verbosity level is activated (exact match).

{-# SPECIALIZE hasExactVerbosity :: VerboseKey -> VerboseLevel -> TCM Bool #-}
hasExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
hasExactVerbosity :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasExactVerbosity VerboseKey
k VerboseLevel
n = (VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
==) (VerboseLevel -> Bool) -> m VerboseLevel -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VerboseKey -> m VerboseLevel
forall (m :: * -> *). MonadDebug m => VerboseKey -> m VerboseLevel
getVerbosityLevel VerboseKey
k

-- | Run a computation if a certain verbosity level is activated (exact match).

{-# SPECIALIZE whenExactVerbosity :: VerboseKey -> VerboseLevel -> TCM () -> TCM () #-}
whenExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
whenExactVerbosity :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
whenExactVerbosity VerboseKey
k VerboseLevel
n = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (m Bool -> m () -> m ()) -> m Bool -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> m Bool
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasExactVerbosity VerboseKey
k VerboseLevel
n

__CRASH_WHEN__ :: (HasCallStack, MonadTCM m, MonadDebug m) => VerboseKey -> VerboseLevel -> m ()
__CRASH_WHEN__ :: forall (m :: * -> *).
(HasCallStack, MonadTCM m, MonadDebug m) =>
VerboseKey -> VerboseLevel -> m ()
__CRASH_WHEN__ VerboseKey
k VerboseLevel
n = VerboseKey -> VerboseLevel -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
whenExactVerbosity VerboseKey
k VerboseLevel
n (Impossible -> m ()
forall a. Impossible -> a
throwImpossible Impossible
err)
  where
    -- Create the "Unreachable" error using *our* caller as the call site.
    err :: Impossible
err = (CallStack -> Impossible) -> Impossible
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Impossible
Unreachable

-- | Run a computation if a certain verbosity level is activated.
--
--   Precondition: The level must be non-negative.
{-# SPECIALIZE verboseS :: VerboseKey -> VerboseLevel -> TCM () -> TCM () #-}
-- {-# SPECIALIZE verboseS :: MonadIO m => VerboseKey -> VerboseLevel -> TCMT m () -> TCMT m () #-} -- RULE left-hand side too complicated to desugar
-- {-# SPECIALIZE verboseS :: MonadTCM tcm => VerboseKey -> VerboseLevel -> tcm () -> tcm () #-}
verboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
verboseS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
k VerboseLevel
n m ()
action = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (VerboseKey -> VerboseLevel -> m Bool
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
k VerboseLevel
n) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ m () -> m ()
forall a. m a -> m a
forall (m :: * -> *) a. MonadDebug m => m a -> m a
nowDebugPrinting m ()
action

-- | Apply a function if a certain verbosity level is activated.
--
--   Precondition: The level must be non-negative.
applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n m a -> m a
f m a
a = m Bool -> m a -> m a -> m a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (VerboseKey -> VerboseLevel -> m Bool
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
k VerboseLevel
n) (m a -> m a
f m a
a) m a
a

-- | Check whether a certain profile option is activated.
{-# SPECIALIZE hasProfileOption :: ProfileOption -> TCM Bool #-}
hasProfileOption :: MonadDebug m => ProfileOption -> m Bool
hasProfileOption :: forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
hasProfileOption ProfileOption
opt = ProfileOption -> ProfileOptions -> Bool
containsProfileOption ProfileOption
opt (ProfileOptions -> Bool) -> m ProfileOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m ProfileOptions
forall (m :: * -> *). MonadDebug m => m ProfileOptions
getProfileOptions

-- | Run some code when the given profiling option is active.
whenProfile :: MonadDebug m => ProfileOption -> m () -> m ()
whenProfile :: forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
opt = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (ProfileOption -> m Bool
forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
hasProfileOption ProfileOption
opt)