Agda.TypeChecking.Monad.Debug

Documentation

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

Minimal complete definition

formatDebugMessage

Methods

displayDebugMessage :: Int -> String -> m ()

traceDebugMessage :: Int -> String -> m a -> m a

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

Instances

MonadDebug ReduceM

Defined in Agda.TypeChecking.Reduce.Monad

Methods

displayDebugMessage :: Int -> String -> ReduceM ()

traceDebugMessage :: Int -> String -> ReduceM a -> ReduceM a

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

MonadDebug TerM

Defined in Agda.Termination.Monad

Methods

displayDebugMessage :: Int -> String -> TerM ()

traceDebugMessage :: Int -> String -> TerM a -> TerM a

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

MonadDebug m => MonadDebug (MaybeT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: Int -> String -> MaybeT m ()

traceDebugMessage :: Int -> String -> MaybeT m a -> MaybeT m a

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

MonadDebug m => MonadDebug (ListT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: Int -> String -> ListT m ()

traceDebugMessage :: Int -> String -> ListT m a -> ListT m a

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

MonadIO m => MonadDebug (TCMT m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: Int -> String -> TCMT m ()

traceDebugMessage :: Int -> String -> TCMT m a -> TCMT m a

formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> TCMT m String

MonadDebug m => MonadDebug (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

displayDebugMessage :: Int -> String -> NamesT m ()

traceDebugMessage :: Int -> String -> NamesT m a -> NamesT m a

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

MonadDebug m => MonadDebug (ReaderT r m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: Int -> String -> ReaderT r m ()

traceDebugMessage :: Int -> String -> ReaderT r m a -> ReaderT r m a

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

MonadDebug m => MonadDebug (ExceptT e m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: Int -> String -> ExceptT e m ()

traceDebugMessage :: Int -> String -> ExceptT e m a -> ExceptT e m a

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

MonadDebug m => MonadDebug (StateT s m)

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: Int -> String -> StateT s m ()

traceDebugMessage :: Int -> String -> StateT s m a -> StateT s m a

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

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

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: Int -> String -> WriterT w m ()

traceDebugMessage :: Int -> String -> WriterT w m a -> WriterT w m a

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

reportS :: (HasOptions m, MonadDebug m, MonadTCEnv m) => VerboseKey -> Int -> String -> m ()

Conditionally print debug string.

reportSLn :: (HasOptions m, MonadDebug m, MonadTCEnv m) => VerboseKey -> Int -> String -> m ()

Conditionally println debug string.

reportSDoc :: (HasOptions m, MonadDebug m, MonadTCEnv m) => VerboseKey -> Int -> TCM Doc -> m ()

Conditionally render debug Doc and print it.

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

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

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

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

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

Print brackets around debug messages issued by a computation.