Agda.Utils.Benchmark

Tools for benchmarking and accumulating results. Nothing Agda-specific in here.

Benchmark trie

type Account a = [a]

Account we can bill computation time to.

type CurrentAccount a = Maybe (Account a, CPUTime)

Record when we started billing the current account.

type Timings a = Trie a CPUTime

data Benchmark a

Benchmark structure is a trie, mapping accounts (phases and subphases) to CPU time spent on their performance.

Constructors

Benchmark

Fields

benchmarkOn :: !Bool

Are we benchmarking at all?

currentAccount :: !(CurrentAccount a)

What are we billing to currently?

timings :: !(Timings a)

The accounts and their accumulated timing bill.

Instances

Null (Benchmark a)

Initial benchmark structure (empty).

(Ord a, Pretty a) => Pretty (Benchmark a)

Print benchmark as two-column table with totals.

mapBenchmarkOn :: (Bool -> Bool) -> Benchmark a -> Benchmark a

Semantic editor combinator.

mapCurrentAccount :: (CurrentAccount a -> CurrentAccount a) -> Benchmark a -> Benchmark a

Semantic editor combinator.

mapTimings :: (Timings a -> Timings a) -> Benchmark a -> Benchmark a

Semantic editor combinator.

addCPUTime :: Ord a => Account a -> CPUTime -> Benchmark a -> Benchmark a

Add to specified CPU time account.

Benchmarking monad.

class (Ord a, Functor m, MonadIO m) => MonadBench a m | m -> a where

Monad with access to benchmarking data.

Minimal complete definition

getBenchmark, finally

Methods

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

We need to be able to terminate benchmarking in case of an exception.

Instances

MonadBench Phase TCM

We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.

MonadBench Phase TerM

MonadBench a m => MonadBench a (ReaderT r m)

setBenchmarking :: MonadBench a m => Bool -> m ()

Turn benchmarking on/off.

switchBenchmarking

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).

billTo :: MonadBench a m => Account a -> m c -> m c

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

Bill a pure computation to a specific account.