Safe Haskell | None |
---|---|
Language | Haskell98 |
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 Bool Source
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 a Source
Bill a pure computation to a specific account.
reimburse :: MonadTCM tcm => Account -> tcm a -> tcm a Source
Reimburse a specific account for computation costs.
reimburseTop :: MonadTCM tcm => Phase -> tcm a -> tcm a Source
Reimburse a top account.