Safe Haskell  None 

Language  Haskell98 
Tools for benchmarking and accumulating results. Nothing Agdaspecific 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))
 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 (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).
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.