| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.Benchmark
Description
Tools for benchmarking and accumulating results. Nothing Agda-specific in here.
Synopsis
- type Account a = [a]
- type CurrentAccount a = Maybe (Account a, CPUTime)
- type Timings a = Trie a CPUTime
- data BenchmarkOn a
- = BenchmarkOff
- | BenchmarkOn
- | BenchmarkSome (Account a -> Bool)
- isBenchmarkOn :: Account a -> BenchmarkOn a -> Bool
- data Benchmark a = Benchmark {
- benchmarkOn :: !(BenchmarkOn a)
- currentAccount :: !(CurrentAccount a)
- timings :: !(Timings a)
- mapBenchmarkOn :: (BenchmarkOn a -> BenchmarkOn a) -> 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 => BenchmarkOn a -> 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
- billToCPS :: MonadBench a m => Account a -> ((b -> m c) -> m c) -> (b -> 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.
data BenchmarkOn a Source #
Constructors
| BenchmarkOff | |
| BenchmarkOn | |
| BenchmarkSome (Account a -> Bool) |
isBenchmarkOn :: Account a -> BenchmarkOn a -> Bool Source #
Benchmark structure is a trie, mapping accounts (phases and subphases) to CPU time spent on their performance.
Constructors
| Benchmark | |
Fields
| |
mapBenchmarkOn :: (BenchmarkOn a -> BenchmarkOn a) -> Benchmark a -> Benchmark a Source #
Semantic editor combinator.
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.
Minimal complete definition
Methods
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.
Instances
setBenchmarking :: MonadBench a m => BenchmarkOn a -> m () Source #
Turn benchmarking on/off.
Arguments
| :: 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.
billToCPS :: MonadBench a m => Account a -> ((b -> m c) -> m c) -> (b -> m c) -> m c Source #
Bill a CPS function to an account. Can't handle exceptions.
billPureTo :: MonadBench a m => Account a -> c -> m c Source #
Bill a pure computation to a specific account.