Safe Haskell | None |
---|---|
Language | Haskell98 |
Tools for benchmarking and accumulating results. Nothing Agda-specific in here.
- type Account a = [a]
- type CurrentAccount a = Maybe (Account a, CPUTime)
- type Timings a = Trie a CPUTime
- data Benchmark a = Benchmark {
- benchmarkOn :: !Bool
- currentAccount :: !(CurrentAccount a)
- timings :: !(Timings a)
- mapBenchmarkOn :: (Bool -> Bool) -> Benchmark a -> Benchmark a
- mapCurrentAccount :: (CurrentAccount a -> CurrentAccount a) -> Benchmark a -> Benchmark a
- mapTimings :: (Timings a -> Timings a) -> Benchmark a -> Benchmark a
- addCPUTime :: Ord a => Account a -> CPUTime -> Benchmark a -> Benchmark a
- class (Ord a, Functor m, MonadIO m) => MonadBench a m | m -> a where
- getBenchmark :: m (Benchmark a)
- getsBenchmark :: (Benchmark a -> c) -> m c
- putBenchmark :: Benchmark a -> m ()
- modifyBenchmark :: (Benchmark a -> Benchmark a) -> m ()
- finally :: m b -> m c -> m b
- setBenchmarking :: MonadBench a m => Bool -> m ()
- switchBenchmarking :: MonadBench a m => Maybe (Account a) -> m (Maybe (Account a))
- reset :: MonadBench a m => m ()
- billTo :: MonadBench a m => Account a -> m c -> m c
- billPureTo :: MonadBench a m => Account a -> c -> m c
Benchmark trie
type CurrentAccount a = Maybe (Account a, CPUTime) Source
Record when we started billing the current account.
Benchmark structure is a trie, mapping accounts (phases and subphases) to CPU time spent on their performance.
Benchmark | |
|
mapCurrentAccount :: (CurrentAccount a -> CurrentAccount a) -> Benchmark a -> Benchmark a Source
Semantic editor combinator.
mapTimings :: (Timings a -> Timings a) -> Benchmark a -> Benchmark a Source
Semantic editor combinator.
addCPUTime :: Ord a => Account a -> CPUTime -> Benchmark a -> Benchmark a Source
Add to specified CPU time account.
Benchmarking monad.
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
getsBenchmark :: (Benchmark a -> c) -> m c Source
putBenchmark :: Benchmark a -> m () Source
modifyBenchmark :: (Benchmark a -> Benchmark a) -> m () Source
finally :: m b -> m c -> m b Source
We need to be able to terminate benchmarking in case of an exception.
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 (StateT r m) Source | |
MonadBench a m => MonadBench a (ReaderT r m) Source |
setBenchmarking :: MonadBench a m => Bool -> m () Source
Turn benchmarking on/off.
:: MonadBench a m | |
=> Maybe (Account a) | Maybe new account. |
-> m (Maybe (Account a)) | Maybe old account. |
Bill current account with time up to now. Switch to new account. Return old account (if any).
reset :: MonadBench a m => m () Source
Resets the account and the timing information.
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.