ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.Benchmark

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

Contents

Benchmark trie
Benchmarking monad.

Synopsis

type Account
type CurrentAccount
type Timings
data BenchmarkOn
value isBenchmarkOn
data Benchmark
value mapBenchmarkOn
value mapCurrentAccount
value mapTimings
value addCPUTime
class MonadBench
value getsBenchmark
value setBenchmarking
value switchBenchmarking
value reset
value billTo
value billToCPS
value billPureTo

PackageAgda-2.8.0.2
Exports18
LanguageHaskell2010
LicenceMIT
SourceBenchmark.hs

Benchmark trie

typetype Account a = [a]

Source#

Account we can bill computation time to.

typetype CurrentAccount a = Maybe (Account a, CPUTime)

Source#

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.8.0.2 · Agda.Utils.Benchmark
NFData a => NFData (BenchmarkOn a)Defined in Agda-2.8.0.2 · Agda.Utils.Benchmark
type Rep (BenchmarkOn a) = D1 ('MetaData "BenchmarkOn" "Agda.Utils.Benchmark" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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.8.0.2 · Agda.Utils.Benchmark

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

datadata Benchmark a

Source#

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.8.0.2 · Agda.Utils.Benchmark
NFData a => NFData (Benchmark a)Defined in Agda-2.8.0.2 · Agda.Utils.Benchmark
(Ord a, Pretty a) => Pretty (Benchmark a)Defined in Agda-2.8.0.2 · Agda.Utils.Benchmark
Print benchmark as three-column table with totals.
Null (Benchmark a)Defined in Agda-2.8.0.2 · Agda.Utils.Benchmark
Initial benchmark structure (empty).
type Rep (Benchmark a) = D1 ('MetaData "Benchmark" "Agda.Utils.Benchmark" "Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP" '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.8.0.2 · Agda.Utils.Benchmark

valuemapBenchmarkOn

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

Source#

Semantic editor combinator.

valuemapCurrentAccount

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

Source#

Semantic editor combinator.

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

Source#

Semantic editor combinator.

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

Source#

Add to specified CPU time account.

Benchmarking monad.

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

Source#

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