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.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 {-# 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 Agda.Utils.Monad
import Agda.Utils.Pretty
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
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 = 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
default verboseBracket
:: (MonadTransControl t, MonadDebug n, m ~ t n)
=> VerboseKey -> VerboseLevel -> String -> m a -> m a
verboseBracket 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
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s
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 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
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
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' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eIsDebugPrinting forall a b. (a -> b) -> a -> b
$ 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 = 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 ()
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
$ Doc -> VerboseKey
render forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
[ VerboseKey -> Doc
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 (VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> Doc
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
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
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
InteractionOutputCallback
cb (VerboseLevel -> VerboseKey -> Response
Resp_RunningInfo VerboseLevel
n VerboseKey
s)
TCM a
cont
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
Doc -> 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
prettyError TCErr
err forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 VerboseKey -> Doc
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:"
]
, VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ VerboseKey -> Doc
text VerboseKey
s
]
verboseBracket :: forall a.
VerboseKey -> VerboseLevel -> VerboseKey -> TCM a -> TCM a
verboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s = forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ \ TCMT IO a
m -> do
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
openVerboseBracket VerboseKey
k VerboseLevel
n VerboseKey
s
(TCMT IO a
m forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracket VerboseKey
k VerboseLevel
n) forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
e -> do
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m ()
closeVerboseBracketException VerboseKey
k VerboseLevel
n
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
e
getVerbosity :: TCM Verbosity
getVerbosity = forall (m :: * -> *). HasOptions m => m Verbosity
defaultGetVerbosity
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
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 (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
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
. Doc -> 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
. Doc -> VerboseKey
render
{-# 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 = 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 { forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"impossible" VerboseLevel
10 VerboseKey
s ; forall a. Impossible -> a
throwImpossible Impossible
err }
where
err :: Impossible
err = forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack CallStack -> Impossible
Impossible
{-# 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 = 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' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eIsDebugPrinting (forall a b. a -> b -> a
const Bool
True) TCM Doc
d)
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 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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 = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM 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 = 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
. Doc -> 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
. Doc -> 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 = forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ VerboseKey
s forall a. [a] -> [a] -> [a]
++ VerboseKey
"\n"
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 = forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ \m a
cont -> do
VerboseKey
s <- forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m VerboseKey
formatDebugMessage VerboseKey
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eIsDebugPrinting (forall a b. a -> b -> a
const Bool
True) TCM Doc
d
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
traceDebugMessage VerboseKey
k VerboseLevel
n (VerboseKey
s 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 = 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"
parseVerboseKey :: VerboseKey -> [String]
parseVerboseKey :: VerboseKey -> [VerboseKey]
parseVerboseKey = forall a. (a -> Bool) -> [a] -> [[a]]
wordsBy (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (VerboseKey
".:" :: String))
{-# SPECIALIZE hasVerbosity :: VerboseKey -> VerboseLevel -> TCM Bool #-}
hasVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
hasVerbosity :: forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m Bool
hasVerbosity VerboseKey
k VerboseLevel
n | VerboseLevel
n forall a. Ord a => a -> a -> Bool
< VerboseLevel
0 = forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
otherwise = do
Verbosity
t <- forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
let ks :: [VerboseKey]
ks = VerboseKey -> [VerboseKey]
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 [VerboseKey]
ks Verbosity
t
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseLevel
n 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 =
(forall a. a -> Maybe a
Just VerboseLevel
n forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => [k] -> Trie k v -> Maybe v
Trie.lookup (VerboseKey -> [VerboseKey]
parseVerboseKey VerboseKey
k) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
{-# 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
err :: Impossible
err = 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 = 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
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
verbosity :: VerboseKey -> Lens' VerboseLevel TCState
verbosity :: VerboseKey -> Lens' VerboseLevel TCState
verbosity VerboseKey
k = Lens' PragmaOptions TCState
stPragmaOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Verbosity PragmaOptions
verbOpt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => [k] -> Lens' (Maybe v) (Trie k v)
Trie.valueAt (VerboseKey -> [VerboseKey]
parseVerboseKey VerboseKey
k) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => a -> Lens' a (Maybe a)
defaultTo VerboseLevel
0
where
verbOpt :: Lens' Verbosity PragmaOptions
verbOpt :: Lens' Verbosity PragmaOptions
verbOpt Verbosity -> f Verbosity
f PragmaOptions
opts = Verbosity -> f Verbosity
f (PragmaOptions -> Verbosity
optVerbose PragmaOptions
opts) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Verbosity
v -> PragmaOptions
opts { optVerbose :: Verbosity
optVerbose = Verbosity
v }
defaultTo :: Eq a => a -> Lens' a (Maybe a)
defaultTo :: forall a. Eq a => a -> Lens' a (Maybe a)
defaultTo a
x a -> f a
f Maybe a
m = forall a. (a -> Bool) -> a -> Maybe a
filterMaybe (forall a. Eq a => a -> a -> Bool
== a
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f (forall a. a -> Maybe a -> a
fromMaybe a
x Maybe a
m)