Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- class (Functor m, Applicative m, Monad m) => MonadDebug (m :: Type -> Type) 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
- __IMPOSSIBLE_VERBOSE__ :: (HasCallStack, MonadDebug m) => String -> m a
- reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
- reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
- verboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
- applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
- class ReportS a where
- reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m ()
- defaultGetVerbosity :: HasOptions m => m Verbosity
- defaultGetProfileOptions :: HasOptions m => m ProfileOptions
- defaultIsDebugPrinting :: MonadTCEnv m => m Bool
- defaultNowDebugPrinting :: MonadTCEnv m => m a -> m a
- displayDebugMessage :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
- catchAndPrintImpossible :: (CatchImpossible m, Monad m) => VerboseKey -> VerboseLevel -> m String -> m String
- hasVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
- alwaysReportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
- reportResult :: MonadDebug m => VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
- alwaysReportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
- unlessDebugPrinting :: MonadDebug m => m () -> m ()
- class TraceS a where
- traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m c -> m c
- traceSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
- traceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a
- openVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
- closeVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> m ()
- closeVerboseBracketException :: MonadDebug m => VerboseKey -> VerboseLevel -> m ()
- hasExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
- whenExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
- __CRASH_WHEN__ :: (HasCallStack, MonadTCM m, MonadDebug m) => VerboseKey -> VerboseLevel -> m ()
- hasProfileOption :: MonadDebug m => ProfileOption -> m Bool
- whenProfile :: MonadDebug m => ProfileOption -> m () -> m ()
- type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel)
- type VerboseKey = String
- type VerboseLevel = Int
Documentation
class (Functor m, Applicative m, Monad m) => MonadDebug (m :: Type -> Type) where Source #
Nothing
formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> m String Source #
default formatDebugMessage :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadDebug n, m ~ t n) => VerboseKey -> VerboseLevel -> TCM Doc -> m String Source #
traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> m a -> m a Source #
default traceDebugMessage :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type) a. (MonadTransControl t, MonadDebug n, m ~ t n) => VerboseKey -> VerboseLevel -> String -> m a -> m a Source #
verboseBracket :: VerboseKey -> VerboseLevel -> String -> m a -> m a Source #
Print brackets around debug messages issued by a computation.
default verboseBracket :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type) a. (MonadTransControl t, MonadDebug n, m ~ t n) => VerboseKey -> VerboseLevel -> String -> m a -> m a Source #
getVerbosity :: m Verbosity Source #
default getVerbosity :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadDebug n, m ~ t n) => m Verbosity Source #
getProfileOptions :: m ProfileOptions Source #
default getProfileOptions :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadDebug n, m ~ t n) => m ProfileOptions Source #
isDebugPrinting :: m Bool Source #
Check whether we are currently debug printing.
default isDebugPrinting :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadDebug n, m ~ t n) => m Bool Source #
nowDebugPrinting :: m a -> m a Source #
Flag in a computation that we are currently debug printing.
default nowDebugPrinting :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type) a. (MonadTransControl t, MonadDebug n, m ~ t n) => m a -> m a Source #
Instances
__IMPOSSIBLE_VERBOSE__ :: (HasCallStack, MonadDebug m) => String -> m a Source #
reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m () Source #
reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #
Conditionally render debug Doc
and print it.
verboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m () Source #
Run a computation 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 Source #
Apply a function if a certain verbosity level is activated.
Precondition: The level must be non-negative.
class ReportS a where Source #
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.
reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m () Source #
Instances
ReportS Doc Source # | |
Defined in Agda.TypeChecking.Monad.Debug reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m () Source # | |
ReportS String Source # | |
Defined in Agda.TypeChecking.Monad.Debug reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m () Source # | |
ReportS (TCM Doc) Source # | |
Defined in Agda.TypeChecking.Monad.Debug reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source # | |
ReportS [Doc] Source # | |
Defined in Agda.TypeChecking.Monad.Debug reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m () Source # | |
ReportS [TCM Doc] Source # | |
Defined in Agda.TypeChecking.Monad.Debug reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m () Source # | |
ReportS [String] Source # | |
Defined in Agda.TypeChecking.Monad.Debug reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [String] -> m () Source # |
defaultGetVerbosity :: HasOptions m => m Verbosity Source #
defaultGetProfileOptions :: HasOptions m => m ProfileOptions Source #
defaultIsDebugPrinting :: MonadTCEnv m => m Bool Source #
defaultNowDebugPrinting :: MonadTCEnv m => m a -> m a Source #
displayDebugMessage :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m () Source #
Print a debug message if switched on.
catchAndPrintImpossible :: (CatchImpossible m, Monad m) => VerboseKey -> VerboseLevel -> m String -> m String Source #
During printing, catch internal errors of kind Impossible
and print them.
hasVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool Source #
Check whether a certain verbosity level is activated.
Precondition: The level must be non-negative.
alwaysReportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m () Source #
Conditionally println debug string. Works regardless of the debug flag.
reportResult :: MonadDebug m => VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a Source #
Debug print the result of a computation.
alwaysReportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #
Conditionally render debug Doc
and print it. Works regardless of the debug flag.
unlessDebugPrinting :: MonadDebug m => m () -> m () Source #
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.
traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m c -> m c Source #
Instances
TraceS Doc Source # | |
Defined in Agda.TypeChecking.Monad.Debug traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m c -> m c Source # | |
TraceS String Source # | |
Defined in Agda.TypeChecking.Monad.Debug traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m c -> m c Source # | |
TraceS (TCM Doc) Source # | |
Defined in Agda.TypeChecking.Monad.Debug traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c Source # | |
TraceS [Doc] Source # | |
Defined in Agda.TypeChecking.Monad.Debug traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c Source # | |
TraceS [TCM Doc] Source # | |
Defined in Agda.TypeChecking.Monad.Debug traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c Source # | |
TraceS [String] Source # | |
Defined in Agda.TypeChecking.Monad.Debug traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [String] -> m c -> m c Source # |
traceSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a Source #
Conditionally render debug Doc
, print it, and then continue.
traceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a Source #
openVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m () Source #
closeVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> m () Source #
closeVerboseBracketException :: MonadDebug m => VerboseKey -> VerboseLevel -> m () Source #
hasExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool Source #
Check whether a certain verbosity level is activated (exact match).
whenExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m () Source #
Run a computation if a certain verbosity level is activated (exact match).
__CRASH_WHEN__ :: (HasCallStack, MonadTCM m, MonadDebug m) => VerboseKey -> VerboseLevel -> m () Source #
hasProfileOption :: MonadDebug m => ProfileOption -> m Bool Source #
Check whether a certain profile option is activated.
whenProfile :: MonadDebug m => ProfileOption -> m () -> m () Source #
Run some code when the given profiling option is active.
type VerboseKey = String Source #
type VerboseLevel = Int Source #