Agda.TypeChecking.Monad.Debug

Documentation

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 String

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

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 [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 (TCM Doc)

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

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 String

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

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 [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 (TCM Doc)

Defined in Agda.TypeChecking.Monad.Debug

Methods

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

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

Minimal complete definition

formatDebugMessage, verboseBracket

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> m ()

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

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

getVerbosity :: m Verbosity

default getVerbosity :: HasOptions m => m Verbosity

isDebugPrinting :: m Bool

default isDebugPrinting :: MonadTCEnv m => m Bool

nowDebugPrinting :: m a -> m a

default nowDebugPrinting :: MonadTCEnv m => m a -> m a

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

Print brackets around debug messages issued by a computation.

Instances

MonadDebug TCM

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> TCM ()

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

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

getVerbosity :: TCM Verbosity

isDebugPrinting :: TCM Bool

nowDebugPrinting :: TCM a -> TCM a

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

MonadDebug ReduceM

Defined in Agda.TypeChecking.Reduce.Monad

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> ReduceM ()

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

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

getVerbosity :: ReduceM Verbosity

isDebugPrinting :: ReduceM Bool

nowDebugPrinting :: ReduceM a -> ReduceM a

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

MonadDebug AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> AbsToCon ()

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

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

getVerbosity :: AbsToCon Verbosity

isDebugPrinting :: AbsToCon Bool

nowDebugPrinting :: AbsToCon a -> AbsToCon a

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

MonadDebug TerM

Defined in Agda.Termination.Monad

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> TerM ()

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

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

getVerbosity :: TerM Verbosity

isDebugPrinting :: TerM Bool

nowDebugPrinting :: TerM a -> TerM a

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

MonadDebug m => MonadDebug (MaybeT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> MaybeT m ()

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

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

getVerbosity :: MaybeT m Verbosity

isDebugPrinting :: MaybeT m Bool

nowDebugPrinting :: MaybeT m a -> MaybeT m a

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

MonadDebug m => MonadDebug (ListT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> ListT m ()

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

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

getVerbosity :: ListT m Verbosity

isDebugPrinting :: ListT m Bool

nowDebugPrinting :: ListT m a -> ListT m a

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

MonadDebug m => MonadDebug (ChangeT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> ChangeT m ()

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

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

getVerbosity :: ChangeT m Verbosity

isDebugPrinting :: ChangeT m Bool

nowDebugPrinting :: ChangeT m a -> ChangeT m a

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

MonadDebug m => MonadDebug (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> NamesT m ()

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

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

getVerbosity :: NamesT m Verbosity

isDebugPrinting :: NamesT m Bool

nowDebugPrinting :: NamesT m a -> NamesT m a

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

MonadDebug m => MonadDebug (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> PureConversionT m ()

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

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

getVerbosity :: PureConversionT m Verbosity

isDebugPrinting :: PureConversionT m Bool

nowDebugPrinting :: PureConversionT m a -> PureConversionT m a

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

MonadDebug m => MonadDebug (ExceptT e m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> ExceptT e m ()

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

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

getVerbosity :: ExceptT e m Verbosity

isDebugPrinting :: ExceptT e m Bool

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

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

MonadDebug m => MonadDebug (ReaderT r m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> ReaderT r m ()

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

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

getVerbosity :: ReaderT r m Verbosity

isDebugPrinting :: ReaderT r m Bool

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

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

MonadDebug m => MonadDebug (IdentityT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> IdentityT m ()

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

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

getVerbosity :: IdentityT m Verbosity

isDebugPrinting :: IdentityT m Bool

nowDebugPrinting :: IdentityT m a -> IdentityT m a

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

MonadDebug m => MonadDebug (StateT s m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> StateT s m ()

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

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

getVerbosity :: StateT s m Verbosity

isDebugPrinting :: StateT s m Bool

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

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

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

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> WriterT w m ()

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

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

getVerbosity :: WriterT w m Verbosity

isDebugPrinting :: WriterT w m Bool

nowDebugPrinting :: WriterT w m a -> WriterT w m a

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

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

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

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

Conditionally println debug string.

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

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

Conditionally render debug Doc and print it.

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

Debug print the result of a computation.

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

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

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

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

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

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

parseVerboseKey :: VerboseKey -> [String]

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

Check whether a certain verbosity level is activated.

Precondition: The level must be non-negative.

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

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.

verbosity :: VerboseKey -> Lens' VerboseLevel TCState

Verbosity lens.

type Verbosity = Trie VerboseKey VerboseLevel

type VerboseKey = String

type VerboseLevel = Int