ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.Benchmark

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

5 types
1 class
12 values

PackageAgda-2.7.0.1
Exports18
LanguageHaskell2010
LicenceMIT
SourceBenchmark.hs

Benchmark trie

10 declarations

typetype Account a = [a]

Account we can bill computation time to.

typetype CurrentAccount a = Maybe (Account a, CPUTime)

Record when we started billing the current account.

typetype Timings a = Trie a CPUTime

datadata BenchmarkOn a

Instances3Generic, NFData, Rep

Generic (BenchmarkOn a)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
NFData a => NFData (BenchmarkOn a)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
type Rep (BenchmarkOn a) = D1 ('MetaData "BenchmarkOn" "Agda.Utils.Benchmark" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "BenchmarkOff" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "BenchmarkOn" 'PrefixI 'False) U1 :+: C1 ('MetaCons "BenchmarkSome" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Account a -> Bool)))))Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark

valueisBenchmarkOn :: Account a -> BenchmarkOn a -> Bool

datadata Benchmark a

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

Constructors

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

Instances5Generic, NFData, Pretty, Null, Rep

Generic (Benchmark a)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
NFData a => NFData (Benchmark a)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
(Ord a, Pretty a) => Pretty (Benchmark a)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
Print benchmark as three-column table with totals.
Null (Benchmark a)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
Initial benchmark structure (empty).
type Rep (Benchmark a) = D1 ('MetaData "Benchmark" "Agda.Utils.Benchmark" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "Benchmark" 'PrefixI 'True) (S1 ('MetaSel ('Just "benchmarkOn") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (BenchmarkOn a)) :*: (S1 ('MetaSel ('Just "currentAccount") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (CurrentAccount a)) :*: S1 ('MetaSel ('Just "timings") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Timings a)))))Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark

valuemapBenchmarkOn

:: BenchmarkOn a -> BenchmarkOn a
-> Benchmark a
-> Benchmark a

Semantic editor combinator.

valuemapCurrentAccount

:: CurrentAccount a -> CurrentAccount a
-> Benchmark a
-> Benchmark a

Semantic editor combinator.

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

Semantic editor combinator.

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

Add to specified CPU time account.

Benchmarking monad.

8 declarations

classclass (Ord (BenchPhase m), Functor m, MonadIO m) => MonadBench (m :: Type -> Type) where

Monad with access to benchmarking data.

Associated types

type family BenchPhase (m :: Type -> Type)

Methods

getBenchmark :: m (Benchmark (BenchPhase m))
putBenchmark :: Benchmark (BenchPhase m) -> m ()
modifyBenchmark :: (Benchmark (BenchPhase m) -> Benchmark (BenchPhase m)) -> m ()
finally :: m b -> m c -> m b
We need to be able to terminate benchmarking in case of an exception.

Instances8MonadBench, …

MonadBench TerMDefined in Agda-2.7.0.1 · Agda.Termination.Monad
MonadBench TCMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.
MonadBench IODefined in Agda-2.7.0.1 · Agda.Benchmarking · orphan
MonadBench m => MonadBench (ListT m)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
MonadBench m => MonadBench (ExceptT e m)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
MonadBench m => MonadBench (ReaderT r m)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
MonadBench m => MonadBench (StateT r m)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
(MonadBench m, Monoid w) => MonadBench (WriterT w m)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark

valuegetsBenchmark :: MonadBench m => (Benchmark (BenchPhase m) -> c) -> m c

valuesetBenchmarking :: MonadBench m => BenchmarkOn (BenchPhase m) -> m ()

Turn benchmarking on/off.

valueswitchBenchmarking

:: MonadBench m
=> Maybe (Account (BenchPhase m))
Maybe new account.
-> m (Maybe (Account (BenchPhase m)))
Maybe old account.

Bill current account with time up to now. Switch to new account. Return old account (if any).

valuereset :: MonadBench m => m ()

Resets the account and the timing information.

valuebillTo :: MonadBench m => Account (BenchPhase m) -> m c -> m c

Bill a computation to a specific account. Works even if the computation is aborted by an exception.

valuebillToCPS

:: MonadBench m
=> Account (BenchPhase m)
-> (b -> m c) -> m c
-> b -> m c
-> m c

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

valuebillPureTo :: MonadBench m => Account (BenchPhase m) -> c -> m c

Bill a pure computation to a specific account.