Safe Haskell | None |
---|
Measure CPU time for individual phases of the Agda pipeline.
- module Agda.TypeChecking.Monad.Base.Benchmark
- getBenchmark :: TCM Benchmark
- benchmarking :: MonadTCM tcm => tcm Bool
- reportBenchmarkingLn :: String -> TCM ()
- reportBenchmarkingDoc :: TCM Doc -> TCM ()
- billTo :: MonadTCM tcm => Account -> tcm a -> tcm a
- billTop :: MonadTCM tcm => Phase -> tcm a -> tcm a
- billPureTo :: MonadTCM tcm => Account -> a -> tcm a
- billSub :: MonadTCM tcm => Account -> tcm a -> tcm a
- reimburse :: MonadTCM tcm => Account -> tcm a -> tcm a
- reimburseTop :: MonadTCM tcm => Phase -> tcm a -> tcm a
Documentation
benchmarking :: MonadTCM tcm => tcm BoolSource
Check whether benchmarking is activated.
reportBenchmarkingLn :: String -> TCM ()Source
Report benchmarking results.
reportBenchmarkingDoc :: TCM Doc -> TCM ()Source
Report benchmarking results.
billPureTo :: MonadTCM tcm => Account -> a -> tcm aSource
Bill a pure computation to a specific account.
reimburse :: MonadTCM tcm => Account -> tcm a -> tcm aSource
Reimburse a specific account for computation costs.
reimburseTop :: MonadTCM tcm => Phase -> tcm a -> tcm aSource
Reimburse a top account.