Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



Measure CPU time for individual phases of the Agda pipeline.



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

Monad with access to benchmarking data.

Minimal complete definition

getBenchmark, finally


getBenchmark :: m (Benchmark a) Source


MonadBench Phase TCM Source

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

MonadBench Phase TerM Source 
MonadBench a m => MonadBench a (ReaderT r m) Source 

updateBenchmarkingStatus :: TCM () Source

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

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

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 Source

Bill a pure computation to a specific account.

print :: MonadTCM tcm => tcm () Source

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