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

Monad with access to benchmarking data.

Minimal complete definition

getBenchmark, finally

Instances

MonadBench Phase IO

Defined in Agda.Benchmarking

Methods

getBenchmark :: IO (Benchmark Phase)

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

putBenchmark :: Benchmark Phase -> IO ()

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

finally :: IO b -> IO c -> IO b

MonadBench Phase TCM

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.Termination.Monad

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)

Defined in Agda.Utils.Benchmark

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)

Defined in Agda.Utils.Benchmark

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 2.