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 BenchmarkOn a

Constructors

BenchmarkOff

BenchmarkOn

BenchmarkSome (Account a -> Bool)

isBenchmarkOn :: Account a -> BenchmarkOn a -> Bool

data Benchmark a

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

Constructors

Benchmark

Fields

• benchmarkOn :: !(BenchmarkOn a)

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

Defined in Agda.Utils.Benchmark

Methods

empty :: Benchmark a

null :: Benchmark a -> Bool

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

Print benchmark as three-column table with totals.

Defined in Agda.Utils.Benchmark

Methods

pretty :: Benchmark a -> Doc

prettyPrec :: Int -> Benchmark a -> Doc

prettyList :: [Benchmark a] -> Doc

mapBenchmarkOn :: (BenchmarkOn a -> BenchmarkOn a) -> 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 IO

Defined in Agda.Benchmarking

Methods

getBenchmark :: IO (Benchmark Phase)

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

putBenchmark :: Benchmark Phase -> IO ()

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

finally :: IO b -> IO c -> IO b

MonadBench Phase TCM

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.Termination.Monad

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)

Defined in Agda.Utils.Benchmark

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)

Defined in Agda.Utils.Benchmark

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 => BenchmarkOn a -> 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.