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.Compat ( iso8601Show )
  -- This is also exported from Data.Time.Format.ISO8601, but only from time >= 1.9

import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.Base

import Agda.Interaction.Options
import {-# SOURCE #-} Agda.Interaction.Response (Response(..))

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.Utils.ProfileOptions
import Agda.Utils.Update
import qualified Agda.Utils.Trie as Trie

import Agda.Utils.Impossible

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

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

  default traceDebugMessage
    :: (MonadTransControl t, MonadDebug n, m ~ t n)
    => VerboseKey -> VerboseLevel -> String -> m a -> m a
  traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
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 -> VerboseKey -> n (StT t a) -> n (StT t a)
forall a. VerboseKey -> VerboseLevel -> VerboseKey -> n a -> n a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s

  default verboseBracket
    :: (MonadTransControl t, MonadDebug n, m ~ t n)
    => VerboseKey -> VerboseLevel -> String -> m a -> m a
  verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
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 -> VerboseKey -> n (StT t a) -> n (StT t a)
forall a. VerboseKey -> VerboseLevel -> VerboseKey -> n a -> n a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s

  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 -> String -> m ()
displayDebugMessage :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s = VerboseKey -> VerboseLevel -> VerboseKey -> m () -> m ()
forall a. VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
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 String -> m String
catchAndPrintImpossible :: forall (m :: * -> *).
(CatchImpossible m, Monad m) =>
VerboseKey -> VerboseLevel -> m VerboseKey -> m VerboseKey
catchAndPrintImpossible VerboseKey
k VerboseLevel
n m VerboseKey
m = (Impossible -> Maybe Impossible)
-> m VerboseKey -> (Impossible -> m VerboseKey) -> m VerboseKey
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 VerboseKey
m ((Impossible -> m VerboseKey) -> m VerboseKey)
-> (Impossible -> m VerboseKey) -> m VerboseKey
forall a b. (a -> b) -> a -> b
$ \ Impossible
imposs -> do
  VerboseKey -> m VerboseKey
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseKey -> m VerboseKey) -> VerboseKey -> m VerboseKey
forall a b. (a -> b) -> a -> b
$ Doc -> VerboseKey
forall a. Doc a -> VerboseKey
render (Doc -> VerboseKey) -> Doc -> VerboseKey
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

instance MonadDebug TCM where

  traceDebugMessage :: forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s TCM a
cont = do
    -- Andreas, 2019-08-20, issue #4016:
    -- Force any lazy 'Impossible' exceptions to the surface and handle them.
    VerboseKey
s  <- IO VerboseKey -> TCM VerboseKey
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO VerboseKey -> TCM VerboseKey)
-> (VerboseKey -> IO VerboseKey) -> VerboseKey -> TCM VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> VerboseLevel -> IO VerboseKey -> IO VerboseKey
forall (m :: * -> *).
(CatchImpossible m, Monad m) =>
VerboseKey -> VerboseLevel -> m VerboseKey -> m VerboseKey
catchAndPrintImpossible VerboseKey
k VerboseLevel
n (IO VerboseKey -> IO VerboseKey)
-> (VerboseKey -> IO VerboseKey) -> VerboseKey -> IO VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> IO VerboseKey
forall a. a -> IO a
E.evaluate (VerboseKey -> IO VerboseKey)
-> (VerboseKey -> VerboseKey) -> VerboseKey -> IO VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> VerboseKey
forall a. NFData a => a -> a
DeepSeq.force (VerboseKey -> TCM VerboseKey) -> VerboseKey -> TCM VerboseKey
forall a b. (a -> b) -> a -> b
$ VerboseKey
s
    InteractionOutputCallback
cb <- (TCState -> InteractionOutputCallback)
-> TCMT IO InteractionOutputCallback
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC ((TCState -> InteractionOutputCallback)
 -> TCMT IO InteractionOutputCallback)
-> (TCState -> InteractionOutputCallback)
-> TCMT IO InteractionOutputCallback
forall a b. (a -> b) -> a -> b
$ PersistentTCState -> InteractionOutputCallback
stInteractionOutputCallback (PersistentTCState -> InteractionOutputCallback)
-> (TCState -> PersistentTCState)
-> TCState
-> InteractionOutputCallback
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState

    -- Andreas, 2022-06-15, prefix with time stamp if `-v debug.time:100`:
    VerboseKey
msg <- TCM Bool -> TCM VerboseKey -> TCM VerboseKey -> TCM VerboseKey
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (VerboseKey -> VerboseLevel -> TCM Bool
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
"debug.time" VerboseLevel
100) {-then-} (VerboseKey -> TCM VerboseKey
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return VerboseKey
s) {-else-} (TCM VerboseKey -> TCM VerboseKey)
-> TCM VerboseKey -> TCM VerboseKey
forall a b. (a -> b) -> a -> b
$ do
      VerboseKey
now <- IO VerboseKey -> TCM VerboseKey
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO VerboseKey -> TCM VerboseKey)
-> IO VerboseKey -> TCM 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
      VerboseKey -> TCM VerboseKey
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseKey -> TCM VerboseKey) -> VerboseKey -> TCM VerboseKey
forall a b. (a -> b) -> a -> b
$ [VerboseKey] -> VerboseKey
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ VerboseKey
now, VerboseKey
": ", VerboseKey
s ]

    InteractionOutputCallback
cb InteractionOutputCallback -> InteractionOutputCallback
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> VerboseKey -> Response
Resp_RunningInfo VerboseLevel
n VerboseKey
msg
    TCM a
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 = VerboseLevel -> VerboseKey -> VerboseKey
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
26 (VerboseKey -> VerboseKey)
-> (VerboseKey -> VerboseKey) -> VerboseKey -> VerboseKey
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Char -> VerboseKey
forall a. a -> [a]
repeat Char
'0')

  formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n TCM Doc
d = VerboseKey -> VerboseLevel -> TCM VerboseKey -> TCM VerboseKey
forall (m :: * -> *).
(CatchImpossible m, Monad m) =>
VerboseKey -> VerboseLevel -> m VerboseKey -> m VerboseKey
catchAndPrintImpossible VerboseKey
k VerboseLevel
n (TCM VerboseKey -> TCM VerboseKey)
-> TCM VerboseKey -> TCM VerboseKey
forall a b. (a -> b) -> a -> b
$ do
    Doc -> VerboseKey
forall a. Doc a -> VerboseKey
render (Doc -> VerboseKey) -> TCM Doc -> TCM VerboseKey
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Doc
d TCM Doc -> (TCErr -> TCM Doc) -> TCM Doc
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err -> do
      TCErr -> TCM VerboseKey
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm VerboseKey
renderError TCErr
err TCM VerboseKey -> (VerboseKey -> Doc) -> TCM Doc
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ VerboseKey
s -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
        [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (VerboseKey -> Doc) -> [VerboseKey] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map VerboseKey -> Doc
forall a. VerboseKey -> Doc a
text
          [ VerboseKey
"Printing debug message"
          , 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
"failed due to error:"
          ]
        , VerboseLevel -> Doc -> Doc
forall a. VerboseLevel -> Doc a -> Doc a
nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Doc
forall a. VerboseKey -> Doc a
text VerboseKey
s
        ]

  verboseBracket :: forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = VerboseKey
-> VerboseLevel
-> (TCMT IO a -> TCMT IO a)
-> TCMT IO a
-> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n ((TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a)
-> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ \ TCMT IO a
m -> do
    VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
openVerboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s
    (TCMT IO a
m TCMT IO a -> TCMT IO () -> TCMT IO a
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* VerboseKey -> VerboseLevel -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracket VerboseKey
k VerboseLevel
n) TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
e -> do
      VerboseKey -> VerboseLevel -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracketException VerboseKey
k VerboseLevel
n
      TCErr -> TCMT IO a
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
e

  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 :: TCM Bool
isDebugPrinting   = TCM 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 -> VerboseKey -> ListT m a -> ListT m a
traceDebugMessage 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
traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
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 -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
k VerboseLevel
n (VerboseKey -> m ()) -> ([Doc] -> VerboseKey) -> [Doc] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> VerboseKey
forall a. Doc a -> VerboseKey
render (Doc -> VerboseKey) -> ([Doc] -> Doc) -> [Doc] -> VerboseKey
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 -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
k VerboseLevel
n (VerboseKey -> m ()) -> (Doc -> VerboseKey) -> Doc -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> VerboseKey
forall a. Doc a -> VerboseKey
render

-- | Conditionally println debug string.
{-# SPECIALIZE reportSLn :: VerboseKey -> VerboseLevel -> String -> TCM () #-}
reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
reportSLn :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
k VerboseLevel
n VerboseKey
s = VerboseKey -> VerboseLevel -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
k VerboseLevel
n (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
s VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n"

__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 :: VerboseKey
k = VerboseKey
"impossible"
  let n :: VerboseLevel
n = VerboseLevel
10
  VerboseKey -> VerboseLevel -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
k VerboseLevel
n (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
s VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n"

  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

-- | Conditionally render debug 'Doc' and print it.
{-# SPECIALIZE reportSDoc :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM () #-}
reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
k VerboseLevel
n TCM Doc
d = VerboseKey -> VerboseLevel -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
k VerboseLevel
n (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey -> VerboseLevel -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey -> m ())
-> (VerboseKey -> VerboseKey) -> VerboseKey -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n") (VerboseKey -> m ()) -> m VerboseKey -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n (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)

-- | Debug print the result of a computation.
reportResult :: MonadDebug m => VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
reportResult :: forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
reportResult VerboseKey
k VerboseLevel
n a -> TCM Doc
debug m a
action = do
  a
x <- m a
action
  a
x a -> m () -> m a
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
k VerboseLevel
n (a -> TCM Doc
debug a
x)

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

-- | 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 :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
traceS = VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
traceSDoc
instance TraceS String    where traceS :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceS = VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
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 :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
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 :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
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 -> VerboseKey -> m c -> m c
forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn  VerboseKey
k VerboseLevel
n (VerboseKey -> m c -> m c)
-> ([Doc] -> VerboseKey) -> [Doc] -> m c -> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> VerboseKey
forall a. Doc a -> VerboseKey
render (Doc -> VerboseKey) -> ([Doc] -> Doc) -> [Doc] -> VerboseKey
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 -> VerboseKey -> m c -> m c
forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn  VerboseKey
k VerboseLevel
n (VerboseKey -> m c -> m c)
-> (Doc -> VerboseKey) -> Doc -> m c -> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> VerboseKey
forall a. Doc a -> VerboseKey
render

traceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a
traceSLn :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn 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 -> VerboseKey -> m a -> m a
forall a. VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey -> m a -> m a) -> VerboseKey -> m a -> m a
forall a b. (a -> b) -> a -> b
$ VerboseKey
s VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n"

-- | Conditionally render debug 'Doc', print it, and then continue.
traceSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
traceSDoc 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
  VerboseKey
s <- VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n (TCM Doc -> m VerboseKey) -> TCM Doc -> m VerboseKey
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
  VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
forall a. VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey
s VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n") m a
cont

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 -> VerboseKey -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey -> m ()) -> VerboseKey -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"{ " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
s VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n"

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

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


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

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

-- | 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 = do
  Verbosity
t <- m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ case Verbosity
t of
    Verbosity
Strict.Nothing -> VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= 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 ->
        -- A special case for "-v0".
        VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
0
      | Bool
otherwise ->
        let ks :: [VerboseKeyItem]
ks = VerboseKey -> [VerboseKeyItem]
parseVerboseKey VerboseKey
k
            m :: VerboseLevel
m  = 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
        in VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
m

-- | 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 = do
  Verbosity
t <- m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ case Verbosity
t of
    Verbosity
Strict.Nothing -> VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== 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 ->
        -- A special case for "-v0".
        VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
0
      | Bool
otherwise ->
        VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
n Maybe VerboseLevel -> Maybe VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== [VerboseKeyItem]
-> Trie VerboseKeyItem VerboseLevel -> Maybe VerboseLevel
forall k v. Ord k => [k] -> Trie k v -> Maybe v
Trie.lookup (VerboseKey -> [VerboseKeyItem]
parseVerboseKey VerboseKey
k) Trie VerboseKeyItem VerboseLevel
t

-- | 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)