Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Monad.Statistics

Description

Collect statistics.

Synopsis

class ReadTCState m => MonadStatistics (m :: Type -> Type) where
- tickN :: String -> Word64 -> m ()
- tickMax :: String -> Word64 -> m ()
tick :: MonadStatistics m => String -> m ()
getStatistics :: ReadTCState m => m Statistics
modifyStatistics :: (Statistics -> Statistics) -> TCM ()
printStatistics :: (MonadDebug m, MonadTCEnv m, HasOptions m) => Maybe TopLevelModuleName -> Statistics -> m ()

Documentation

class ReadTCState m => MonadStatistics (m :: Type -> Type) where Source #

Minimal complete definition

Nothing

Methods

tickN :: String -> Word64 -> m () Source #

default tickN :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type). (MonadStatistics n, MonadTrans t, t n ~ m) => String -> Word64 -> m () Source #

tickMax :: String -> Word64 -> m () Source #

default tickMax :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type). (MonadStatistics n, MonadTrans t, t n ~ m) => String -> Word64 -> m () Source #

Instances

Instances details

MonadStatistics TerM Source #
Instance details Defined in Agda.Termination.Monad Methods tickN :: String -> Word64 -> TerM () Source # tickMax :: String -> Word64 -> TerM () Source #
MonadStatistics TCM Source #
Instance details Defined in Agda.TypeChecking.Monad.Statistics Methods tickN :: String -> Word64 -> TCM () Source # tickMax :: String -> Word64 -> TCM () Source #
ReadTCState m => MonadStatistics (PureConversionT m) Source #
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods tickN :: String -> Word64 -> PureConversionT m () Source # tickMax :: String -> Word64 -> PureConversionT m () Source #
MonadStatistics m => MonadStatistics (MaybeT m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Statistics Methods tickN :: String -> Word64 -> MaybeT m () Source # tickMax :: String -> Word64 -> MaybeT m () Source #
MonadStatistics m => MonadStatistics (ExceptT e m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Statistics Methods tickN :: String -> Word64 -> ExceptT e m () Source # tickMax :: String -> Word64 -> ExceptT e m () Source #
MonadStatistics m => MonadStatistics (ReaderT r m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Statistics Methods tickN :: String -> Word64 -> ReaderT r m () Source # tickMax :: String -> Word64 -> ReaderT r m () Source #
MonadStatistics m => MonadStatistics (StateT s m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Statistics Methods tickN :: String -> Word64 -> StateT s m () Source # tickMax :: String -> Word64 -> StateT s m () Source #
(MonadStatistics m, Monoid w) => MonadStatistics (WriterT w m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Statistics Methods tickN :: String -> Word64 -> WriterT w m () Source # tickMax :: String -> Word64 -> WriterT w m () Source #

tick :: MonadStatistics m => String -> m () Source #

Increase specified counter by 1.

getStatistics :: ReadTCState m => m Statistics Source #

Get the statistics.

modifyStatistics :: (Statistics -> Statistics) -> TCM () Source #

Modify the statistics via given function.

printStatistics :: (MonadDebug m, MonadTCEnv m, HasOptions m) => Maybe TopLevelModuleName -> Statistics -> m () Source #

Print the given statistics.