Agda-2.8.0: 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 :: 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
- reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
- class ReportS a where
  - reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m ()
- reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
- verboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
- applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
- 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 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 #

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

Conditionally render debug `Doc` and print it.

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 an` Ambiguous 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 #

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

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.

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 an` Ambiguous 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 #