Safe Haskell | None |
---|---|

Language | Haskell98 |

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.

getBenchmark :: m (Benchmark a) Source

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.