Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Debug

Synopsis

Documentation

class (Functor m, Applicative m, Monad m) => MonadDebug (m :: Type -> Type) where Source #

Minimal complete definition

Nothing

Methods

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

Instances details
MonadDebug AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadDebug TerM Source # 
Instance details

Defined in Agda.Termination.Monad

MonadDebug ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

MonadDebug TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadDebug NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

MonadDebug m => MonadDebug (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadDebug m => MonadDebug (BlockT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadDebug m => MonadDebug (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

MonadDebug m => MonadDebug (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadDebug m => MonadDebug (ChangeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadDebug m => MonadDebug (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> MaybeT m String Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> MaybeT m a -> MaybeT m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> MaybeT m a -> MaybeT m a Source #

getVerbosity :: MaybeT m Verbosity Source #

getProfileOptions :: MaybeT m ProfileOptions Source #

isDebugPrinting :: MaybeT m Bool Source #

nowDebugPrinting :: MaybeT m a -> MaybeT m a Source #

MonadDebug m => MonadDebug (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ExceptT e m String Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ExceptT e m a -> ExceptT e m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> ExceptT e m a -> ExceptT e m a Source #

getVerbosity :: ExceptT e m Verbosity Source #

getProfileOptions :: ExceptT e m ProfileOptions Source #

isDebugPrinting :: ExceptT e m Bool Source #

nowDebugPrinting :: ExceptT e m a -> ExceptT e m a Source #

MonadDebug m => MonadDebug (IdentityT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> IdentityT m String Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> IdentityT m a -> IdentityT m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> IdentityT m a -> IdentityT m a Source #

getVerbosity :: IdentityT m Verbosity Source #

getProfileOptions :: IdentityT m ProfileOptions Source #

isDebugPrinting :: IdentityT m Bool Source #

nowDebugPrinting :: IdentityT m a -> IdentityT m a Source #

MonadDebug m => MonadDebug (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ReaderT r m String Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ReaderT r m a -> ReaderT r m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> ReaderT r m a -> ReaderT r m a Source #

getVerbosity :: ReaderT r m Verbosity Source #

getProfileOptions :: ReaderT r m ProfileOptions Source #

isDebugPrinting :: ReaderT r m Bool Source #

nowDebugPrinting :: ReaderT r m a -> ReaderT r m a Source #

MonadDebug m => MonadDebug (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> StateT s m String Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> StateT s m a -> StateT s m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> StateT s m a -> StateT s m a Source #

getVerbosity :: StateT s m Verbosity Source #

getProfileOptions :: StateT s m ProfileOptions Source #

isDebugPrinting :: StateT s m Bool Source #

nowDebugPrinting :: StateT s m a -> StateT s m a Source #

(MonadDebug m, Monoid w) => MonadDebug (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> WriterT w m String Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> WriterT w m a -> WriterT w m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> WriterT w m a -> WriterT w m a Source #

getVerbosity :: WriterT w m Verbosity Source #

getProfileOptions :: WriterT w m ProfileOptions Source #

isDebugPrinting :: WriterT w m Bool Source #

nowDebugPrinting :: WriterT w m a -> WriterT w 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.

Methods

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

Instances

Instances details
ReportS Doc Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m () Source #

ReportS String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m () Source #

ReportS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS [Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m () Source #

ReportS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m () Source #

ReportS [String] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [String] -> m () 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 #

class TraceS 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 @ traceS key level "Literate string" gives an Ambiguous 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 Source #

Instances

Instances details
TraceS Doc Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m c -> m c Source #

TraceS String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m c -> m c Source #

TraceS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c Source #

TraceS [Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c Source #

TraceS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c Source #

TraceS [String] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

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 #

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).

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 Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel) Source #

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.

type VerboseKey = String Source #

type VerboseLevel = Int Source #