Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Monad.Debug

Synopsis

class (Functor m, Applicative m, Monad m) => MonadDebug (m :: Type -> Type) where
- formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> m String
- traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> m a -> m a
- verboseBracket :: VerboseKey -> VerboseLevel -> String -> m a -> m a
- getVerbosity :: m Verbosity
- getProfileOptions :: m ProfileOptions
- isDebugPrinting :: m Bool
- nowDebugPrinting :: m a -> m a
__IMPOSSIBLE_VERBOSE__ :: (HasCallStack, MonadDebug m) => String -> m a
reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
verboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
class ReportS a where
- reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m ()
defaultGetVerbosity :: HasOptions m => m Verbosity
defaultGetProfileOptions :: HasOptions m => m ProfileOptions
defaultIsDebugPrinting :: MonadTCEnv m => m Bool
defaultNowDebugPrinting :: MonadTCEnv m => m a -> m a
displayDebugMessage :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
catchAndPrintImpossible :: (CatchImpossible m, Monad m) => VerboseKey -> VerboseLevel -> m String -> m String
hasVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
alwaysReportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
reportResult :: MonadDebug m => VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
alwaysReportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
unlessDebugPrinting :: MonadDebug m => m () -> m ()
class TraceS a where
- traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m c -> m c
traceSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
traceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a
openVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
closeVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> m ()
closeVerboseBracketException :: MonadDebug m => VerboseKey -> VerboseLevel -> m ()
hasExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
whenExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
__CRASH_WHEN__ :: (HasCallStack, MonadTCM m, MonadDebug m) => VerboseKey -> VerboseLevel -> m ()
hasProfileOption :: MonadDebug m => ProfileOption -> m Bool
whenProfile :: MonadDebug m => ProfileOption -> m () -> m ()
type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel)
type VerboseKey = String
type VerboseLevel = Int

Documentation

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

Minimal complete definition

Nothing

Methods

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

default formatDebugMessage :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadDebug n, m ~ t n) => VerboseKey -> VerboseLevel -> TCM Doc -> m String Source #

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

default traceDebugMessage :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type) a. (MonadTransControl t, MonadDebug n, m ~ t n) => VerboseKey -> VerboseLevel -> String -> m a -> m a Source #

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

Print brackets around debug messages issued by a computation.

default verboseBracket :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type) a. (MonadTransControl t, MonadDebug n, m ~ t n) => VerboseKey -> VerboseLevel -> String -> m a -> m a Source #

getVerbosity :: m Verbosity Source #

default getVerbosity :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadDebug n, m ~ t n) => m Verbosity Source #

getProfileOptions :: m ProfileOptions Source #

default getProfileOptions :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadDebug n, m ~ t n) => m ProfileOptions Source #

isDebugPrinting :: m Bool Source #

Check whether we are currently debug printing.

default isDebugPrinting :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadDebug n, m ~ t n) => m Bool Source #

nowDebugPrinting :: m a -> m a Source #

Flag in a computation that we are currently debug printing.

default nowDebugPrinting :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type) a. (MonadTransControl t, MonadDebug n, m ~ t n) => m a -> m a Source #

Instances

Instances details

MonadDebug AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> AbsToCon String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> AbsToCon a -> AbsToCon a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> AbsToCon a -> AbsToCon a Source # getVerbosity :: AbsToCon Verbosity Source # getProfileOptions :: AbsToCon ProfileOptions Source # isDebugPrinting :: AbsToCon Bool Source # nowDebugPrinting :: AbsToCon a -> AbsToCon a Source #
MonadDebug TerM Source #
Instance details Defined in Agda.Termination.Monad Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> TerM String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> TerM a -> TerM a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> TerM a -> TerM a Source # getVerbosity :: TerM Verbosity Source # getProfileOptions :: TerM ProfileOptions Source # isDebugPrinting :: TerM Bool Source # nowDebugPrinting :: TerM a -> TerM a Source #
MonadDebug ReduceM Source #
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ReduceM String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ReduceM a -> ReduceM a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> ReduceM a -> ReduceM a Source # getVerbosity :: ReduceM Verbosity Source # getProfileOptions :: ReduceM ProfileOptions Source # isDebugPrinting :: ReduceM Bool Source # nowDebugPrinting :: ReduceM a -> ReduceM a Source #
MonadDebug TCM Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> TCM a -> TCM a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> TCM a -> TCM a Source # getVerbosity :: TCM Verbosity Source # getProfileOptions :: TCM ProfileOptions Source # isDebugPrinting :: TCM Bool Source # nowDebugPrinting :: TCM a -> TCM a Source #
MonadDebug NLM Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> NLM String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> NLM a -> NLM a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> NLM a -> NLM a Source # getVerbosity :: NLM Verbosity Source # getProfileOptions :: NLM ProfileOptions Source # isDebugPrinting :: NLM Bool Source # nowDebugPrinting :: NLM a -> NLM a Source #
MonadDebug m => MonadDebug (PureConversionT m) Source #
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> PureConversionT m String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> PureConversionT m a -> PureConversionT m a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> PureConversionT m a -> PureConversionT m a Source # getVerbosity :: PureConversionT m Verbosity Source # getProfileOptions :: PureConversionT m ProfileOptions Source # isDebugPrinting :: PureConversionT m Bool Source # nowDebugPrinting :: PureConversionT m a -> PureConversionT m a Source #
MonadDebug m => MonadDebug (BlockT m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> BlockT m String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> BlockT m a -> BlockT m a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> BlockT m a -> BlockT m a Source # getVerbosity :: BlockT m Verbosity Source # getProfileOptions :: BlockT m ProfileOptions Source # isDebugPrinting :: BlockT m Bool Source # nowDebugPrinting :: BlockT m a -> BlockT m a Source #
MonadDebug m => MonadDebug (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> NamesT m String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> NamesT m a -> NamesT m a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> NamesT m a -> NamesT m a Source # getVerbosity :: NamesT m Verbosity Source # getProfileOptions :: NamesT m ProfileOptions Source # isDebugPrinting :: NamesT m Bool Source # nowDebugPrinting :: NamesT m a -> NamesT m a Source #
MonadDebug m => MonadDebug (ListT m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ListT m String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ListT m a -> ListT m a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> ListT m a -> ListT m a Source # getVerbosity :: ListT m Verbosity Source # getProfileOptions :: ListT m ProfileOptions Source # isDebugPrinting :: ListT m Bool Source # nowDebugPrinting :: ListT m a -> ListT m a Source #
MonadDebug m => MonadDebug (ChangeT m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ChangeT m String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ChangeT m a -> ChangeT m a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> ChangeT m a -> ChangeT m a Source # getVerbosity :: ChangeT m Verbosity Source # getProfileOptions :: ChangeT m ProfileOptions Source # isDebugPrinting :: ChangeT m Bool Source # nowDebugPrinting :: ChangeT m a -> ChangeT m a Source #
MonadDebug m => MonadDebug (MaybeT m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> MaybeT m String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> MaybeT m a -> MaybeT m a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> MaybeT m a -> MaybeT m a Source # getVerbosity :: MaybeT m Verbosity Source # getProfileOptions :: MaybeT m ProfileOptions Source # isDebugPrinting :: MaybeT m Bool Source # nowDebugPrinting :: MaybeT m a -> MaybeT m a Source #
MonadDebug m => MonadDebug (ExceptT e m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ExceptT e m String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ExceptT e m a -> ExceptT e m a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> ExceptT e m a -> ExceptT e m a Source # getVerbosity :: ExceptT e m Verbosity Source # getProfileOptions :: ExceptT e m ProfileOptions Source # isDebugPrinting :: ExceptT e m Bool Source # nowDebugPrinting :: ExceptT e m a -> ExceptT e m a Source #
MonadDebug m => MonadDebug (IdentityT m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> IdentityT m String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> IdentityT m a -> IdentityT m a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> IdentityT m a -> IdentityT m a Source # getVerbosity :: IdentityT m Verbosity Source # getProfileOptions :: IdentityT m ProfileOptions Source # isDebugPrinting :: IdentityT m Bool Source # nowDebugPrinting :: IdentityT m a -> IdentityT m a Source #
MonadDebug m => MonadDebug (ReaderT r m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ReaderT r m String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ReaderT r m a -> ReaderT r m a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> ReaderT r m a -> ReaderT r m a Source # getVerbosity :: ReaderT r m Verbosity Source # getProfileOptions :: ReaderT r m ProfileOptions Source # isDebugPrinting :: ReaderT r m Bool Source # nowDebugPrinting :: ReaderT r m a -> ReaderT r m a Source #
MonadDebug m => MonadDebug (StateT s m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> StateT s m String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> StateT s m a -> StateT s m a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> StateT s m a -> StateT s m a Source # getVerbosity :: StateT s m Verbosity Source # getProfileOptions :: StateT s m ProfileOptions Source # isDebugPrinting :: StateT s m Bool Source # nowDebugPrinting :: StateT s m a -> StateT s m a Source #
(MonadDebug m, Monoid w) => MonadDebug (WriterT w m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> WriterT w m String Source # traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> WriterT w m a -> WriterT w m a Source # verboseBracket :: VerboseKey -> VerboseLevel -> String -> WriterT w m a -> WriterT w m a Source # getVerbosity :: WriterT w m Verbosity Source # getProfileOptions :: WriterT w m ProfileOptions Source # isDebugPrinting :: WriterT w m Bool Source # nowDebugPrinting :: WriterT w m a -> WriterT w m a Source #

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

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

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

Conditionally render debug Doc and print it.

verboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m () Source #

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 Source #

Apply a function if a certain verbosity level is activated.

Precondition: The level must be non-negative.

class ReportS a where Source #

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 anAmbiguous type variable error in GHC@. Use the legacy functions reportSLn and reportSDoc instead then.

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m () Source #

Instances

Instances details

ReportS Doc Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m () Source #
ReportS String Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m () Source #
ReportS (TCM Doc) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #
ReportS [Doc] Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m () Source #
ReportS [TCM Doc] Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m () Source #
ReportS [String] Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [String] -> m () Source #

defaultGetVerbosity :: HasOptions m => m Verbosity Source #

defaultGetProfileOptions :: HasOptions m => m ProfileOptions Source #

defaultIsDebugPrinting :: MonadTCEnv m => m Bool Source #

defaultNowDebugPrinting :: MonadTCEnv m => m a -> m a Source #

displayDebugMessage :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m () Source #

Print a debug message if switched on.

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

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

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

Check whether a certain verbosity level is activated.

Precondition: The level must be non-negative.

alwaysReportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m () Source #

Conditionally println debug string. Works regardless of the debug flag.

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

Debug print the result of a computation.

alwaysReportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #

Conditionally render debug Doc and print it. Works regardless of the debug flag.

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

class TraceS a where Source #

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 anAmbiguous 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 Source #

Instances

Instances details

TraceS Doc Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m c -> m c Source #
TraceS String Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m c -> m c Source #
TraceS (TCM Doc) Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c Source #
TraceS [Doc] Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c Source #
TraceS [TCM Doc] Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c Source #
TraceS [String] Source #
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [String] -> m c -> m c Source #

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

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

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

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

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

closeVerboseBracketException :: MonadDebug m => VerboseKey -> VerboseLevel -> m () Source #

hasExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool Source #

Check whether a certain verbosity level is activated (exact match).

whenExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m () Source #

Run a computation if a certain verbosity level is activated (exact match).

__CRASH_WHEN__ :: (HasCallStack, MonadTCM m, MonadDebug m) => VerboseKey -> VerboseLevel -> m () Source #

hasProfileOption :: MonadDebug m => ProfileOption -> m Bool Source #

Check whether a certain profile option is activated.

whenProfile :: MonadDebug m => ProfileOption -> m () -> m () Source #

Run some code when the given profiling option is active.

type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel) Source #

Nothing is used if no verbosity options have been given, thus making it possible to handle the default case relatively quickly. Note that Nothing corresponds to a trie with verbosity level 1 for the empty path.

type VerboseKey = String Source #

type VerboseLevel = Int Source #