Agda.TypeChecking.Monad.Benchmark

Measure CPU time for individual phases of the Agda pipeline.

Documentation

module Agda.TypeChecking.Monad.Base.Benchmark

getBenchmark :: TCM Benchmark

Lens getter for Benchmark from TCM.

benchmarking :: MonadTCM tcm => tcm Bool

Check whether benchmarking is activated.

billTo :: MonadTCM tcm => Account -> tcm a -> tcm a

Bill a computation to a specific account.

billPureTo :: MonadTCM tcm => Account -> a -> tcm a

Bill a pure computation to a specific account.

print :: MonadTCM tcm => tcm ()

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