Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Debug

Synopsis

- class (Functor m, Applicative m, Monad m) => MonadDebug m where
  - displayDebugMessage :: Int -> String -> m ()
  - traceDebugMessage :: Int -> String -> m a -> m a
  - formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> m String
- reportS :: (HasOptions m, MonadDebug m, MonadTCEnv m) => VerboseKey -> Int -> String -> m ()
- reportSLn :: (HasOptions m, MonadDebug m, MonadTCEnv m) => VerboseKey -> Int -> String -> m ()
- reportSDoc :: (HasOptions m, MonadDebug m, MonadTCEnv m) => VerboseKey -> Int -> TCM Doc -> m ()
- 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
- verboseBracket :: (HasOptions m, MonadDebug m, MonadError err m) => VerboseKey -> Int -> String -> m a -> m a

# Documentation

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

Minimal complete definition

formatDebugMessage

Methods

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

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

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

Instances

MonadDebug ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods displayDebugMessage :: Int -> String -> ReduceM () Source # traceDebugMessage :: Int -> String -> ReduceM a -> ReduceM a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> ReduceM String Source #
MonadDebug TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods displayDebugMessage :: Int -> String -> TerM () Source # traceDebugMessage :: Int -> String -> TerM a -> TerM a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> TerM String Source #
MonadDebug m => MonadDebug (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods displayDebugMessage :: Int -> String -> MaybeT m () Source # traceDebugMessage :: Int -> String -> MaybeT m a -> MaybeT m a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> MaybeT m String Source #
MonadDebug m => MonadDebug (ListT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods displayDebugMessage :: Int -> String -> ListT m () Source # traceDebugMessage :: Int -> String -> ListT m a -> ListT m a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> ListT m String Source #
MonadIO m => MonadDebug (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods displayDebugMessage :: Int -> String -> TCMT m () Source # traceDebugMessage :: Int -> String -> TCMT m a -> TCMT m a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> TCMT m String Source #
MonadDebug m => MonadDebug (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods displayDebugMessage :: Int -> String -> NamesT m () Source # traceDebugMessage :: Int -> String -> NamesT m a -> NamesT m a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> NamesT m String Source #
MonadDebug m => MonadDebug (ExceptT e m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods displayDebugMessage :: Int -> String -> ExceptT e m () Source # traceDebugMessage :: Int -> String -> ExceptT e m a -> ExceptT e m a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> ExceptT e m String Source #
MonadDebug m => MonadDebug (ReaderT r m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods displayDebugMessage :: Int -> String -> ReaderT r m () Source # traceDebugMessage :: Int -> String -> ReaderT r m a -> ReaderT r m a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> ReaderT r m String Source #
MonadDebug m => MonadDebug (StateT s m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods displayDebugMessage :: Int -> String -> StateT s m () Source # traceDebugMessage :: Int -> String -> StateT s m a -> StateT s m a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> StateT s m String Source #
(MonadDebug m, Monoid w) => MonadDebug (WriterT w m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods displayDebugMessage :: Int -> String -> WriterT w m () Source # traceDebugMessage :: Int -> String -> WriterT w m a -> WriterT w m a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> WriterT w m String Source #

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

Conditionally print debug string.

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

Conditionally println debug string.

reportSDoc :: (HasOptions m, MonadDebug m, MonadTCEnv 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.