{-# 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.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 = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 = 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 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
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 = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity

  default getProfileOptions
    :: (MonadTrans t, MonadDebug n, m ~ t n)
    => m ProfileOptions
  getProfileOptions = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadDebug m => m ProfileOptions
getProfileOptions

  default isDebugPrinting
    :: (MonadTrans t, MonadDebug n, m ~ t n)
    => m Bool
  isDebugPrinting = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadDebug m => m Bool
isDebugPrinting

  default nowDebugPrinting
    :: (MonadTransControl t, MonadDebug n, m ~ t n)
    => m a -> m a
  nowDebugPrinting = 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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

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

defaultIsDebugPrinting :: MonadTCEnv m => m Bool
defaultIsDebugPrinting :: forall (m :: * -> *). MonadTCEnv m => m Bool
defaultIsDebugPrinting = 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 = forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC Lens' TCEnv Bool
eIsDebugPrinting forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n VerboseKey
s forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) b a.
CatchImpossible m =>
(Impossible -> Maybe b) -> m a -> (b -> m a) -> m a
catchImpossibleJust Impossible -> Maybe Impossible
catchMe m VerboseKey
m forall a b. (a -> b) -> a -> b
$ \ Impossible
imposs -> do
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Doc a -> VerboseKey
render forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
    [ forall a. VerboseKey -> Doc a
text forall a b. (a -> b) -> a -> b
$ VerboseKey
"Debug printing " forall a. [a] -> [a] -> [a]
++ VerboseKey
k forall a. [a] -> [a] -> [a]
++ VerboseKey
":" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> VerboseKey
show VerboseLevel
n forall a. [a] -> [a] -> [a]
++ VerboseKey
" failed due to exception:"
    , forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. VerboseLevel -> Doc a -> Doc a
nest VerboseLevel
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. VerboseKey -> Doc a
text) forall a b. (a -> b) -> a -> b
$ VerboseKey -> [VerboseKey]
lines forall a b. (a -> b) -> a -> b
$ 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 = forall a. (a -> Bool) -> a -> Maybe a
filterMaybe 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  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
(CatchImpossible m, Monad m) =>
VerboseKey -> VerboseLevel -> m VerboseKey -> m VerboseKey
catchAndPrintImpossible VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> IO a
E.evaluate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NFData a => a -> a
DeepSeq.force forall a b. (a -> b) -> a -> b
$ VerboseKey
s
    InteractionOutputCallback
cb <- forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC forall a b. (a -> b) -> a -> b
$ PersistentTCState -> InteractionOutputCallback
stInteractionOutputCallback 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 <- forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
"debug.time" VerboseLevel
100) {-then-} (forall (m :: * -> *) a. Monad m => a -> m a
return VerboseKey
s) {-else-} forall a b. (a -> b) -> a -> b
$ do
      VerboseKey
now <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseKey
trailingZeros forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. ISO8601 t => t -> VerboseKey
iso8601Show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ VerboseKey
now, VerboseKey
": ", VerboseKey
s ]

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

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

#ifdef DEBUG
  verboseBracket 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
  verboseBracket :: forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s TCM a
ma = TCM a
ma
  {-# INLINE verboseBracket #-}
#endif

  getVerbosity :: TCM Verbosity
getVerbosity      = forall (m :: * -> *). HasOptions m => m Verbosity
defaultGetVerbosity
  getProfileOptions :: TCM ProfileOptions
getProfileOptions = forall (m :: * -> *). HasOptions m => m ProfileOptions
defaultGetProfileOptions
  isDebugPrinting :: TCM Bool
isDebugPrinting   = forall (m :: * -> *). MonadTCEnv m => m Bool
defaultIsDebugPrinting
  nowDebugPrinting :: forall a. TCM a -> TCM a
nowDebugPrinting  = 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 (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT forall a b. (a -> b) -> a -> b
$ 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 (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT forall a b. (a -> b) -> a -> b
$ 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 (m :: * -> *) (m' :: * -> *) a.
(Monad m, Monad m') =>
(forall a1. m a1 -> m' a1) -> ListT m a -> ListT m' a
liftListT 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 = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc
instance ReportS String    where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportS = 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 = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
instance ReportS [String]  where reportS :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> [VerboseKey] -> m ()
reportS VerboseKey
k VerboseLevel
n = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
k VerboseLevel
n 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 = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> VerboseKey
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> VerboseKey
render

#ifdef DEBUG

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

#else

{-# INLINE reportSLn #-}
reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
reportSLn :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
_ VerboseLevel
_ VerboseKey
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

#endif

-- | Conditionally println debug string. Works regardless of the debug flag.
{-# SPECIALIZE reportSLn :: 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 = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ VerboseKey
s 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
  forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ VerboseKey
s forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n"

  forall a. Impossible -> a
throwImpossible Impossible
err
  where
    -- Create the "Impossible" error using *our* caller as the call site.
    err :: Impossible
err = forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Impossible
Impossible

#ifdef DEBUG

-- | Conditionally render debug 'Doc' and print it.
{-# SPECIALIZE reportSDoc :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM () #-}
reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc k n d = verboseS k n $ do
  displayDebugMessage k n . (++ "\n") =<< formatDebugMessage k n (locallyTC eIsDebugPrinting (const True) d)

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

#else

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

-- | Debug print the result of a computation.
{-# INLINE reportResult #-}
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
_ VerboseLevel
_ a -> TCM Doc
_ m a
action = m a
action

#endif

-- | Conditionally render debug 'Doc' and print it. Works regardless of the debug flag.
{-# SPECIALIZE reportSDoc :: 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 = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n") forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n (forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC Lens' TCEnv Bool
eIsDebugPrinting (forall a b. a -> b -> a
const Bool
True) TCM Doc
d)

unlessDebugPrinting :: MonadDebug m => m () -> m ()
unlessDebugPrinting :: forall (m :: * -> *). MonadDebug m => m () -> m ()
unlessDebugPrinting = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM 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 = 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 = 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 = forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c
traceSDoc VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
instance TraceS [String]  where traceS :: forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> [VerboseKey] -> m c -> m c
traceS VerboseKey
k VerboseLevel
n = forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn  VerboseKey
k VerboseLevel
n 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 = forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn  VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> VerboseKey
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (m :: * -> *) c.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m c -> m c
traceSLn  VerboseKey
k VerboseLevel
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Doc a -> VerboseKey
render


#ifdef DEBUG

traceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a
traceSLn k n s = applyWhenVerboseS k n $ traceDebugMessage k n $ s ++ "\n"

-- | Conditionally render debug 'Doc', print it, and then continue.
traceSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSDoc k n d = applyWhenVerboseS k n $ \cont -> do
  s <- formatDebugMessage k n $ locallyTC eIsDebugPrinting (const True) d
  traceDebugMessage k n (s ++ "\n") cont

#else

{-# INLINE traceSLn #-}
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
_ VerboseLevel
_ VerboseKey
_ m a
action = m a
action

-- | Conditionally render debug 'Doc', print it, and then continue.
{-# INLINE traceSDoc #-}
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
_ VerboseLevel
_ TCM Doc
_ m a
action = m a
action

#endif


openVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
openVerboseBracket :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
openVerboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
displayDebugMessage VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ VerboseKey
"{ " forall a. [a] -> [a] -> [a]
++ VerboseKey
s 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 = 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 = 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 <- forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Verbosity
t of
    Verbosity
Strict.Nothing -> VerboseLevel
n 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 forall a. Eq a => a -> a -> Bool
== forall k v. [k] -> v -> Trie k v
Trie.singleton [] VerboseLevel
0 ->
        -- A special case for "-v0".
        VerboseLevel
n forall a. Ord a => a -> a -> Bool
<= VerboseLevel
0
      | Bool
otherwise ->
        let ks :: [VerboseKeyItem]
ks = VerboseKey -> [VerboseKeyItem]
parseVerboseKey VerboseKey
k
            m :: VerboseLevel
m  = forall a. a -> [a] -> a
lastWithDefault VerboseLevel
0 forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => [k] -> Trie k v -> [v]
Trie.lookupPath [VerboseKeyItem]
ks Trie VerboseKeyItem VerboseLevel
t
        in VerboseLevel
n 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 <- forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Verbosity
t of
    Verbosity
Strict.Nothing -> VerboseLevel
n 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 forall a. Eq a => a -> a -> Bool
== forall k v. [k] -> v -> Trie k v
Trie.singleton [] VerboseLevel
0 ->
        -- A special case for "-v0".
        VerboseLevel
n forall a. Eq a => a -> a -> Bool
== VerboseLevel
0
      | Bool
otherwise ->
        forall a. a -> Maybe a
Just VerboseLevel
n forall a. Eq a => a -> a -> Bool
== 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 = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
whenExactVerbosity VerboseKey
k VerboseLevel
n (forall a. Impossible -> a
throwImpossible Impossible
err)
  where
    -- Create the "Unreachable" error using *our* caller as the call site.
    err :: Impossible
err = 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 = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
k VerboseLevel
n) forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
hasProfileOption ProfileOption
opt)