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.

reportBenchmarkingLn :: String -> TCM ()

Report benchmarking results.

reportBenchmarkingDoc :: TCM Doc -> TCM ()

Report benchmarking results.

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

Bill a computation to a specific account.

billTop :: MonadTCM tcm => Phase -> tcm a -> tcm a

Bill a top account.

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

Bill a pure computation to a specific account.

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

Bill a sub account.

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

Reimburse a specific account for computation costs.

reimburseTop :: MonadTCM tcm => Phase -> tcm a -> tcm a

Reimburse a top account.