Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Monad.Debug

Synopsis

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 TerM #
Methods displayDebugMessage :: Int -> String -> TerM () # traceDebugMessage :: Int -> String -> TerM a -> TerM a # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> TerM String #
MonadDebug m => MonadDebug (MaybeT m) #
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) #
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) #
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 (ExceptT e m) #
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) #
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) #
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 #
MonadDebug m => MonadDebug (ReaderT * r m) #
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 #

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

Conditionally print debug string.

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

Conditionally println debug string.

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

Conditionally render debug Doc and print it.

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.