Agda.TypeChecking.Monad.Statistics

Collect statistics.

Documentation

class ReadTCState m => MonadStatistics m where

Minimal complete definition

Nothing

Methods

modifyCounter :: String -> (Integer -> Integer) -> m ()

default modifyCounter :: (MonadStatistics n, MonadTrans t, t n ~ m) => String -> (Integer -> Integer) -> m ()

Instances

MonadStatistics TerM

Defined in Agda.Termination.Monad

Methods

modifyCounter :: String -> (Integer -> Integer) -> TerM ()

MonadStatistics TCM

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> TCM ()

ReadTCState m => MonadStatistics (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

modifyCounter :: String -> (Integer -> Integer) -> PureConversionT m ()

MonadStatistics m => MonadStatistics (MaybeT m)

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> MaybeT m ()

MonadStatistics m => MonadStatistics (ExceptT e m)

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> ExceptT e m ()

MonadStatistics m => MonadStatistics (ReaderT r m)

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> ReaderT r m ()

MonadStatistics m => MonadStatistics (StateT s m)

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> StateT s m ()

(MonadStatistics m, Monoid w) => MonadStatistics (WriterT w m)

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> WriterT w m ()

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

Increase specified counter by 1.

tickN :: MonadStatistics m => String -> Integer -> m ()

Increase specified counter by n.

tickMax :: MonadStatistics m => String -> Integer -> m ()

Set the specified counter to the maximum of its current value and n.

getStatistics :: ReadTCState m => m Statistics

Get the statistics.

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

Modify the statistics via given function.

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

Print the given statistics if verbosity "profile.ticks" is given.