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

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

Print benchmark as three-column table with totals.

Methods

pretty :: Benchmark a -> Doc

prettyPrec :: Int -> Benchmark a -> Doc

Null (Benchmark a)

Initial benchmark structure (empty).

Methods

empty :: Benchmark a

null :: Benchmark a -> Bool

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.

Methods

getBenchmark :: TCM (Benchmark Phase)

getsBenchmark :: (Benchmark Phase -> c) -> TCM c

putBenchmark :: Benchmark Phase -> TCM ()

modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> TCM ()

finally :: TCM b -> TCM c -> TCM b

MonadBench Phase TerM

Methods

getBenchmark :: TerM (Benchmark Phase)

getsBenchmark :: (Benchmark Phase -> c) -> TerM c

putBenchmark :: Benchmark Phase -> TerM ()

modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> TerM ()

finally :: TerM b -> TerM c -> TerM b

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

Methods

getBenchmark :: StateT r m (Benchmark a)

getsBenchmark :: (Benchmark a -> c) -> StateT r m c

putBenchmark :: Benchmark a -> StateT r m ()

modifyBenchmark :: (Benchmark a -> Benchmark a) -> StateT r m ()

finally :: StateT r m b -> StateT r m c -> StateT r m b

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

Methods

getBenchmark :: ReaderT * r m (Benchmark a)

getsBenchmark :: (Benchmark a -> c) -> ReaderT * r m c

putBenchmark :: Benchmark a -> ReaderT * r m ()

modifyBenchmark :: (Benchmark a -> Benchmark a) -> ReaderT * r m ()

finally :: ReaderT * r m b -> ReaderT * r m c -> ReaderT * r m b

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

reset :: MonadBench a m => m ()

Resets the account and the timing information.

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.

billToCPS :: MonadBench a m => Account a -> ((b -> m c) -> m c) -> (b -> m c) -> m c

Bill a CPS function to an account. Can't handle exceptions.

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

Bill a pure computation to a specific account.