ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Monad.Debug

3 types
3 classes
26 values

PackageAgda-2.7.0.1
Exports32
LanguageHaskell2010
LicenceMIT
SourceDebug.hs

classclass (Functor m, Applicative m, Monad m) => MonadDebug (m :: Type -> Type) where

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> m String
traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> m a -> m a
verboseBracket :: VerboseKey -> VerboseLevel -> String -> m a -> m a
Print brackets around debug messages issued by a computation.
getVerbosity :: m Verbosity
getProfileOptions :: m ProfileOptions
isDebugPrinting :: m Bool
Check whether we are currently debug printing.
nowDebugPrinting :: m a -> m a
Flag in a computation that we are currently debug printing.

Instances17MonadDebug, …

MonadDebug AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
MonadDebug TerMDefined in Agda-2.7.0.1 · Agda.Termination.Monad
MonadDebug ForcedVariableCollection'Defined in Agda-2.7.0.1 · Agda.TypeChecking.Forcing
MonadDebug ReduceMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce.Monad · orphan
MonadDebug TCMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
MonadDebug NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
MonadDebug m => MonadDebug (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure
MonadDebug m => MonadDebug (BlockT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
MonadDebug m => MonadDebug (NamesT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Names
MonadDebug m => MonadDebug (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
MonadDebug m => MonadDebug (ChangeT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
MonadDebug m => MonadDebug (MaybeT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
MonadDebug m => MonadDebug (ExceptT e m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
MonadDebug m => MonadDebug (IdentityT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
MonadDebug m => MonadDebug (ReaderT r m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
MonadDebug m => MonadDebug (StateT s m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
(MonadDebug m, Monoid w) => MonadDebug (WriterT w m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug

value__IMPOSSIBLE_VERBOSE__ :: (HasCallStack, MonadDebug m) => String -> m a

valuereportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()

valuereportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()

Conditionally render debug Doc and print it.

valueverboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()

Run a computation if a certain verbosity level is activated.

Precondition: The level must be non-negative.

valueapplyWhenVerboseS

:: MonadDebug m
=> VerboseKey
-> VerboseLevel
-> m a -> m a
-> m a
-> m a

Apply a function if a certain verbosity level is activated.

Precondition: The level must be non-negative.

classclass ReportS a where

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 anAmbiguous type variable error in GHC@. Use the legacy functions reportSLn and reportSDoc instead then.

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m ()

Instances6ReportS

ReportS DocDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
ReportS StringDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
ReportS (TCM Doc)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
ReportS [Doc]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
ReportS [TCM Doc]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
ReportS [String]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug

valuedefaultGetVerbosity :: HasOptions m => m Verbosity

valuedefaultGetProfileOptions :: HasOptions m => m ProfileOptions

valuedefaultIsDebugPrinting :: MonadTCEnv m => m Bool

valuedefaultNowDebugPrinting :: MonadTCEnv m => m a -> m a

valuedisplayDebugMessage

:: MonadDebug m
=> VerboseKey
-> VerboseLevel
-> String
-> m ()

Print a debug message if switched on.

valuecatchAndPrintImpossible

:: (CatchImpossible m, Monad m)
=> VerboseKey
-> VerboseLevel
-> m String
-> m String

During printing, catch internal errors of kind Impossible and print them.

valuehasVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool

Check whether a certain verbosity level is activated.

Precondition: The level must be non-negative.

valuealwaysReportSLn

:: MonadDebug m
=> VerboseKey
-> VerboseLevel
-> String
-> m ()

Conditionally println debug string. Works regardless of the debug flag.

valuereportResult

:: MonadDebug m
=> VerboseKey
-> VerboseLevel
-> a -> TCM Doc
-> m a
-> m a

Debug print the result of a computation.

valuealwaysReportSDoc

:: MonadDebug m
=> VerboseKey
-> VerboseLevel
-> TCM Doc
-> m ()

Conditionally render debug Doc and print it. Works regardless of the debug flag.

valueunlessDebugPrinting :: MonadDebug m => m () -> m ()

classclass TraceS a where

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 anAmbiguous type variable error in GHC@. Use the legacy functions traceSLn and traceSDoc instead then.

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m c -> m c

Instances6TraceS

TraceS DocDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
TraceS StringDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
TraceS (TCM Doc)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
TraceS [Doc]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
TraceS [TCM Doc]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug
TraceS [String]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Debug

valuetraceSDoc

:: MonadDebug m
=> VerboseKey
-> VerboseLevel
-> TCM Doc
-> m a
-> m a

Conditionally render debug Doc, print it, and then continue.

valuetraceSLn

:: MonadDebug m
=> VerboseKey
-> VerboseLevel
-> String
-> m a
-> m a

valueopenVerboseBracket

:: MonadDebug m
=> VerboseKey
-> VerboseLevel
-> String
-> m ()

valuecloseVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> m ()

valuecloseVerboseBracketException

:: MonadDebug m
=> VerboseKey
-> VerboseLevel
-> m ()

valuehasExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool

Check whether a certain verbosity level is activated (exact match).

valuewhenExactVerbosity

:: MonadDebug m
=> VerboseKey
-> VerboseLevel
-> m ()
-> m ()

Run a computation if a certain verbosity level is activated (exact match).

value__CRASH_WHEN__

:: (HasCallStack, MonadTCM m, MonadDebug m)
=> VerboseKey
-> VerboseLevel
-> m ()

valuehasProfileOption :: MonadDebug m => ProfileOption -> m Bool

Check whether a certain profile option is activated.

valuewhenProfile :: MonadDebug m => ProfileOption -> m () -> m ()

Run some code when the given profiling option is active.

typetype Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel)

Nothing is used if no verbosity options have been given, thus making it possible to handle the default case relatively quickly. Note that Nothing corresponds to a trie with verbosity level 1 for the empty path.

typetype VerboseKey = String

typetype VerboseLevel = Int