Agda.TypeChecking.Monad.Benchmark

Monad with access to benchmarking data.

When profile options are set or changed, we need to turn benchmarking on or off.

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

Bill a pure computation to a specific account.

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

Resets the account and the timing information.

Prints the accumulated benchmark results. Does nothing if no benchmark profiling is enabled.