| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Monad.Benchmark
Description
Measure CPU time for individual phases of the Agda pipeline.
- module Agda.Benchmarking
- class (Ord a, Functor m, MonadIO m) => MonadBench a m | m -> a where
- getBenchmark :: m (Benchmark a)
- updateBenchmarkingStatus :: TCM ()
- billTo :: MonadBench a m => Account a -> m c -> m c
- billPureTo :: MonadBench a m => Account a -> c -> m c
- print :: MonadTCM tcm => tcm ()
Documentation
module Agda.Benchmarking
class (Ord a, Functor m, MonadIO m) => MonadBench a m | m -> a where Source
Monad with access to benchmarking data.
Minimal complete definition
Methods
getBenchmark :: m (Benchmark a) Source
Instances
| MonadBench Phase TCM Source | We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking. |
| MonadBench Phase TerM Source | |
| MonadBench a m => MonadBench a (ReaderT r m) Source |
updateBenchmarkingStatus :: TCM () Source
When verbosity is set or changes, we need to turn benchmarking on or off.
billTo :: MonadBench a m => Account a -> m c -> m c Source
Bill a computation to a specific account. Works even if the computation is aborted by an exception.
billPureTo :: MonadBench a m => Account a -> c -> m c Source
Bill a pure computation to a specific account.