Agda-2.5.4.2.20190111: 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 where Source #

Minimal complete definition

formatDebugMessage

Instances
MonadDebug ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

MonadDebug TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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

Defined in Agda.TypeChecking.Monad.Debug

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

Defined in Agda.TypeChecking.Monad.Debug

MonadIO m => MonadDebug (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

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

Defined in Agda.TypeChecking.Monad.Debug

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

Defined in Agda.TypeChecking.Monad.Debug

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

Defined in Agda.TypeChecking.Monad.Debug

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

Defined in Agda.TypeChecking.Monad.Debug

reportS :: (HasOptions m, MonadDebug m, MonadReader TCEnv m) => VerboseKey -> Int -> String -> m () Source #

Conditionally print debug string.

reportSLn :: (HasOptions m, MonadDebug m, MonadReader TCEnv m) => VerboseKey -> Int -> String -> m () Source #

Conditionally println debug string.

reportSDoc :: (HasOptions m, MonadDebug m, MonadReader TCEnv m) => VerboseKey -> Int -> TCM Doc -> m () Source #

Conditionally render debug Doc and print it.

unlessDebugPrinting :: MonadTCM m => m () -> m () Source #

traceSLn :: (HasOptions m, MonadDebug m) => VerboseKey -> Int -> String -> m a -> m a Source #

traceSDoc :: (HasOptions m, MonadDebug m) => VerboseKey -> Int -> TCM Doc -> m a -> m a Source #

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

verboseBracket :: (HasOptions m, MonadDebug m, MonadError err m) => VerboseKey -> Int -> String -> m a -> m a Source #

Print brackets around debug messages issued by a computation.