{-# 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.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.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
verboseBracket :: VerboseKey -> VerboseLevel -> String -> m a -> m a
getVerbosity :: m Verbosity
getProfileOptions :: m ProfileOptions
isDebugPrinting :: m Bool
nowDebugPrinting :: m a -> m a
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
#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
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
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 ()
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
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
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
cb <- getsTC $ stInteractionOutputCallback . stPersistentState
msg <- ifNotM (hasVerbosity "debug.time" 100) (return s) $ do
now <- liftIO $ trailingZeros . iso8601Show <$> liftA2 utcToLocalTime getCurrentTimeZone getCurrentTime
return $ concat [ now, ": ", s ]
cb $ Resp_RunningInfo n msg
cont
where
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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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
]
#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 = 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
deriving instance MonadDebug m => MonadDebug (BlockT m)
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)
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
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
#ifdef DEBUG
{-# 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
_ = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
#endif
{-# 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 = 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
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
err :: Impossible
err = (CallStack -> Impossible) -> Impossible
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Impossible
Impossible
#ifdef DEBUG
{-# 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)
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
{-# 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
_ = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
{-# 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
{-# 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 = 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)
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
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
#ifdef DEBUG
traceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a
traceSLn k n s = applyWhenVerboseS k n $ traceDebugMessage k n $ s ++ "\n"
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
{-# 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 = 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"
{-# 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
t <- m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
return $ case 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
| 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
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
{-# 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
t <- m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
return $ case 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
| 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
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
{-# 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
err :: Impossible
err = (CallStack -> Impossible) -> Impossible
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Impossible
Unreachable
{-# SPECIALIZE verboseS :: 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
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
{-# 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
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)