Agda.TypeChecking.Monad.Benchmark

Measure CPU time for individual phases of the Agda pipeline.

Documentation

module Agda.Benchmarking

class (Ord a, Functor m, MonadIO m) => MonadBench a m | m -> a where

Monad with access to benchmarking data.

Minimal complete definition

getBenchmark, finally

Methods

getBenchmark :: m (Benchmark a)

Instances

MonadBench Phase TCM

We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.

Methods

getBenchmark :: TCM (Benchmark Phase)

getsBenchmark :: (Benchmark Phase -> c) -> TCM c

putBenchmark :: Benchmark Phase -> TCM ()

modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> TCM ()

finally :: TCM b -> TCM c -> TCM b

MonadBench Phase TerM

Methods

getBenchmark :: TerM (Benchmark Phase)

getsBenchmark :: (Benchmark Phase -> c) -> TerM c

putBenchmark :: Benchmark Phase -> TerM ()

modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> TerM ()

finally :: TerM b -> TerM c -> TerM b

MonadBench a m => MonadBench a (StateT r m)

Methods

getBenchmark :: StateT r m (Benchmark a)

getsBenchmark :: (Benchmark a -> c) -> StateT r m c

putBenchmark :: Benchmark a -> StateT r m ()

modifyBenchmark :: (Benchmark a -> Benchmark a) -> StateT r m ()

finally :: StateT r m b -> StateT r m c -> StateT r m b

MonadBench a m => MonadBench a (ReaderT * r m)

Methods

getBenchmark :: ReaderT * r m (Benchmark a)

getsBenchmark :: (Benchmark a -> c) -> ReaderT * r m c

putBenchmark :: Benchmark a -> ReaderT * r m ()

modifyBenchmark :: (Benchmark a -> Benchmark a) -> ReaderT * r m ()

finally :: ReaderT * r m b -> ReaderT * r m c -> ReaderT * r m b

getBenchmark :: MonadBench a m => m (Benchmark a)

updateBenchmarkingStatus :: TCM ()

When verbosity is set or changes, we need to turn benchmarking on or off.

billTo :: MonadBench a m => Account a -> m c -> m c

Bill a computation to a specific account. Works even if the computation is aborted by an exception.

billPureTo :: MonadBench a m => Account a -> c -> m c

Bill a pure computation to a specific account.

billToCPS :: MonadBench a m => Account a -> ((b -> m c) -> m c) -> (b -> m c) -> m c

Bill a CPS function to an account. Can't handle exceptions.

reset :: MonadBench a m => m ()

Resets the account and the timing information.

print :: MonadTCM tcm => tcm ()

Prints the accumulated benchmark results. Does nothing if profiling is not activated at level 7.