| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.Benchmark
Description
Tools for benchmarking and accumulating results. Nothing Agda-specific in here.
Synopsis
- type Account a = [a]
- type CurrentAccount a = Maybe (Account a, CPUTime)
- type Timings a = Trie a CPUTime
- data BenchmarkOn a
- = BenchmarkOff
- | BenchmarkOn
- | BenchmarkSome (Account a -> Bool)
- isBenchmarkOn :: Account a -> BenchmarkOn a -> Bool
- data Benchmark a = Benchmark {
- benchmarkOn :: !(BenchmarkOn a)
- currentAccount :: !(CurrentAccount a)
- timings :: !(Timings a)
- mapBenchmarkOn :: (BenchmarkOn a -> BenchmarkOn a) -> 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 (BenchPhase m), Functor m, MonadIO m) => MonadBench (m :: Type -> Type) where
- type BenchPhase (m :: Type -> Type)
- 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
- getsBenchmark :: MonadBench m => (Benchmark (BenchPhase m) -> c) -> m c
- setBenchmarking :: MonadBench m => BenchmarkOn (BenchPhase m) -> m ()
- switchBenchmarking :: MonadBench m => Maybe (Account (BenchPhase m)) -> m (Maybe (Account (BenchPhase m)))
- reset :: MonadBench m => m ()
- billTo :: MonadBench m => Account (BenchPhase m) -> m c -> m c
- billToCPS :: MonadBench m => Account (BenchPhase m) -> ((b -> m c) -> m c) -> (b -> m c) -> m c
- billPureTo :: MonadBench m => Account (BenchPhase m) -> c -> m c
Benchmark trie
type CurrentAccount a = Maybe (Account a, CPUTime) Source #
Record when we started billing the current account.
data BenchmarkOn a Source #
Constructors
| BenchmarkOff | |
| BenchmarkOn | |
| BenchmarkSome (Account a -> Bool) |
Instances
| NFData a => NFData (BenchmarkOn a) Source # | |||||
Defined in Agda.Utils.Benchmark Methods rnf :: BenchmarkOn a -> () | |||||
| Generic (BenchmarkOn a) Source # | |||||
Defined in Agda.Utils.Benchmark Associated Types
| |||||
| type Rep (BenchmarkOn a) Source # | |||||
Defined in Agda.Utils.Benchmark type Rep (BenchmarkOn a) = D1 ('MetaData "BenchmarkOn" "Agda.Utils.Benchmark" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "BenchmarkOff" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BenchmarkOn" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BenchmarkSome" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Account a -> Bool))))) | |||||
isBenchmarkOn :: Account a -> BenchmarkOn a -> Bool Source #
Benchmark structure is a trie, mapping accounts (phases and subphases) to CPU time spent on their performance.
Constructors
| Benchmark | |
Fields
| |
Instances
| (Ord a, Pretty a) => Pretty (Benchmark a) Source # | Print benchmark as three-column table with totals. | ||||
| Null (Benchmark a) Source # | Initial benchmark structure (empty). | ||||
| NFData a => NFData (Benchmark a) Source # | |||||
Defined in Agda.Utils.Benchmark | |||||
| Generic (Benchmark a) Source # | |||||
Defined in Agda.Utils.Benchmark Associated Types
| |||||
| type Rep (Benchmark a) Source # | |||||
Defined in Agda.Utils.Benchmark type Rep (Benchmark a) = D1 ('MetaData "Benchmark" "Agda.Utils.Benchmark" "Agda-2.6.20240714-inplace" '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))))) | |||||
mapBenchmarkOn :: (BenchmarkOn a -> BenchmarkOn a) -> Benchmark a -> Benchmark a Source #
Semantic editor combinator.
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 (BenchPhase m), Functor m, MonadIO m) => MonadBench (m :: Type -> Type) where Source #
Monad with access to benchmarking data.
Minimal complete definition
Associated Types
type BenchPhase (m :: Type -> Type) Source #
Methods
getBenchmark :: m (Benchmark (BenchPhase m)) Source #
putBenchmark :: Benchmark (BenchPhase m) -> m () Source #
modifyBenchmark :: (Benchmark (BenchPhase m) -> Benchmark (BenchPhase m)) -> m () Source #
finally :: m b -> m c -> m b Source #
We need to be able to terminate benchmarking in case of an exception.
Instances
getsBenchmark :: MonadBench m => (Benchmark (BenchPhase m) -> c) -> m c Source #
setBenchmarking :: MonadBench m => BenchmarkOn (BenchPhase m) -> m () Source #
Turn benchmarking on/off.
Arguments
| :: 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).
reset :: MonadBench m => m () Source #
Resets the account and the timing information.
billTo :: MonadBench m => Account (BenchPhase m) -> m c -> m c Source #
Bill a computation to a specific account. Works even if the computation is aborted by an exception.
billToCPS :: MonadBench m => Account (BenchPhase m) -> ((b -> m c) -> m c) -> (b -> m c) -> m c Source #
Bill a CPS function to an account. Can't handle exceptions.
billPureTo :: MonadBench m => Account (BenchPhase m) -> c -> m c Source #
Bill a pure computation to a specific account.