Agda.TypeChecking.Monad.Debug

Documentation

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

Minimal complete definition

Nothing

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> m String

default formatDebugMessage :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadDebug n, m ~ t n) => VerboseKey -> VerboseLevel -> TCM Doc -> m String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> m a -> m a

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

verboseBracket :: VerboseKey -> VerboseLevel -> String -> m a -> m a

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

getVerbosity :: m Verbosity

default getVerbosity :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadDebug n, m ~ t n) => m Verbosity

getProfileOptions :: m ProfileOptions

default getProfileOptions :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadDebug n, m ~ t n) => m ProfileOptions

isDebugPrinting :: m Bool

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

nowDebugPrinting :: m a -> m a

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

Instances

MonadDebug AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> AbsToCon String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> AbsToCon a -> AbsToCon a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> AbsToCon a -> AbsToCon a

getVerbosity :: AbsToCon Verbosity

getProfileOptions :: AbsToCon ProfileOptions

isDebugPrinting :: AbsToCon Bool

nowDebugPrinting :: AbsToCon a -> AbsToCon a

MonadDebug TerM

Defined in Agda.Termination.Monad

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> TerM String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> TerM a -> TerM a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> TerM a -> TerM a

getVerbosity :: TerM Verbosity

getProfileOptions :: TerM ProfileOptions

isDebugPrinting :: TerM Bool

nowDebugPrinting :: TerM a -> TerM a

MonadDebug ReduceM

Defined in Agda.TypeChecking.Reduce.Monad

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ReduceM String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ReduceM a -> ReduceM a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> ReduceM a -> ReduceM a

getVerbosity :: ReduceM Verbosity

getProfileOptions :: ReduceM ProfileOptions

isDebugPrinting :: ReduceM Bool

nowDebugPrinting :: ReduceM a -> ReduceM a

MonadDebug TCM

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> TCM a -> TCM a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> TCM a -> TCM a

getVerbosity :: TCM Verbosity

getProfileOptions :: TCM ProfileOptions

isDebugPrinting :: TCM Bool

nowDebugPrinting :: TCM a -> TCM a

MonadDebug NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> NLM String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> NLM a -> NLM a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> NLM a -> NLM a

getVerbosity :: NLM Verbosity

getProfileOptions :: NLM ProfileOptions

isDebugPrinting :: NLM Bool

nowDebugPrinting :: NLM a -> NLM a

MonadDebug m => MonadDebug (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> PureConversionT m String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> PureConversionT m a -> PureConversionT m a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> PureConversionT m a -> PureConversionT m a

getVerbosity :: PureConversionT m Verbosity

getProfileOptions :: PureConversionT m ProfileOptions

isDebugPrinting :: PureConversionT m Bool

nowDebugPrinting :: PureConversionT m a -> PureConversionT m a

MonadDebug m => MonadDebug (BlockT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> BlockT m String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> BlockT m a -> BlockT m a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> BlockT m a -> BlockT m a

getVerbosity :: BlockT m Verbosity

getProfileOptions :: BlockT m ProfileOptions

isDebugPrinting :: BlockT m Bool

nowDebugPrinting :: BlockT m a -> BlockT m a

MonadDebug m => MonadDebug (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> NamesT m a -> NamesT m a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> NamesT m a -> NamesT m a

getVerbosity :: NamesT m Verbosity

getProfileOptions :: NamesT m ProfileOptions

isDebugPrinting :: NamesT m Bool

nowDebugPrinting :: NamesT m a -> NamesT m a

MonadDebug m => MonadDebug (ListT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ListT m String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ListT m a -> ListT m a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> ListT m a -> ListT m a

getVerbosity :: ListT m Verbosity

getProfileOptions :: ListT m ProfileOptions

isDebugPrinting :: ListT m Bool

nowDebugPrinting :: ListT m a -> ListT m a

MonadDebug m => MonadDebug (ChangeT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ChangeT m String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ChangeT m a -> ChangeT m a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> ChangeT m a -> ChangeT m a

getVerbosity :: ChangeT m Verbosity

getProfileOptions :: ChangeT m ProfileOptions

isDebugPrinting :: ChangeT m Bool

nowDebugPrinting :: ChangeT m a -> ChangeT m a

MonadDebug m => MonadDebug (MaybeT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

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

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

getVerbosity :: MaybeT m Verbosity

getProfileOptions :: MaybeT m ProfileOptions

isDebugPrinting :: MaybeT m Bool

nowDebugPrinting :: MaybeT m a -> MaybeT m a

MonadDebug m => MonadDebug (ExceptT e m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

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

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

getVerbosity :: ExceptT e m Verbosity

getProfileOptions :: ExceptT e m ProfileOptions

isDebugPrinting :: ExceptT e m Bool

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

MonadDebug m => MonadDebug (IdentityT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

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

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

getVerbosity :: IdentityT m Verbosity

getProfileOptions :: IdentityT m ProfileOptions

isDebugPrinting :: IdentityT m Bool

nowDebugPrinting :: IdentityT m a -> IdentityT m a

MonadDebug m => MonadDebug (ReaderT r m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

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

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

getVerbosity :: ReaderT r m Verbosity

getProfileOptions :: ReaderT r m ProfileOptions

isDebugPrinting :: ReaderT r m Bool

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

MonadDebug m => MonadDebug (StateT s m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

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

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

getVerbosity :: StateT s m Verbosity

getProfileOptions :: StateT s m ProfileOptions

isDebugPrinting :: StateT s m Bool

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

(MonadDebug m, Monoid w) => MonadDebug (WriterT w m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

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

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

getVerbosity :: WriterT w m Verbosity

getProfileOptions :: WriterT w m ProfileOptions

isDebugPrinting :: WriterT w m Bool

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

Conditionally render debug Doc and print it.

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

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

Apply a function if a certain verbosity level is activated.

Precondition: The level must be non-negative.

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

Methods

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

Instances

ReportS Doc

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS String

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS (TCM Doc)

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS [Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS [TCM Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

ReportS [String]

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

Print a debug message if switched on.

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

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

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

Check whether a certain verbosity level is activated.

Precondition: The level must be non-negative.

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

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

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

Debug print the result of a computation.

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

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

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

class 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 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

Instances

TraceS Doc

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS String

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS (TCM Doc)

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS [Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS [TCM Doc]

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

TraceS [String]

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [String] -> m c -> m c

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

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

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

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

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

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

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

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

Check whether a certain profile option is activated.

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

Run some code when the given profiling option is active.

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

type VerboseKey = String

type VerboseLevel = Int