Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Benchmark

Contents

- Benchmark trie
- Benchmarking monad.

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 Account a = [a] Source #

Account we can bill computation time to.

type CurrentAccount a = Maybe (Account a, CPUTime) Source #

Record when we started billing the current account.

type Timings a = Trie a CPUTime Source #

data BenchmarkOn a Source #

Constructors

BenchmarkOff |
BenchmarkOn |
BenchmarkSome (Account a -> Bool) |

#### Instances

Instances details

NFData a => NFData (BenchmarkOn a) Source # |
Instance details Defined in Agda.Utils.Benchmark Methods rnf :: BenchmarkOn a -> () Source #
Generic (BenchmarkOn a) Source # |

Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type Rep (BenchmarkOn a) |

Instance details

Defined in Agda.Utils.Benchmark

type Rep (BenchmarkOn a) = D1 ('MetaData "BenchmarkOn" "Agda.Utils.Benchmark" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))

Methods

from :: BenchmarkOn a -> Rep (BenchmarkOn a) x Source #

to :: Rep (BenchmarkOn a) x -> BenchmarkOn a Source #

type Rep (BenchmarkOn a) Source # |

Instance details

Defined in Agda.Utils.Benchmark

type Rep (BenchmarkOn a) = D1 ('MetaData "BenchmarkOn" "Agda.Utils.Benchmark" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 #

data Benchmark a Source #

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

Instances details

(Ord a, Pretty a) => Pretty (Benchmark a) Source # | Print benchmark as three-column table with totals.
Instance details Defined in Agda.Utils.Benchmark Methods pretty :: Benchmark a -> Doc Source # prettyPrec :: Int -> Benchmark a -> Doc Source # prettyList :: [Benchmark a] -> Doc Source #
Null (Benchmark a) Source # | Initial benchmark structure (empty).
Instance details Defined in Agda.Utils.Benchmark Methods empty :: Benchmark a Source # null :: Benchmark a -> Bool Source #
NFData a => NFData (Benchmark a) Source # |
Instance details Defined in Agda.Utils.Benchmark Methods rnf :: Benchmark a -> () Source #
Generic (Benchmark a) Source # |

Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type Rep (Benchmark a) |

Instance details

Defined in Agda.Utils.Benchmark

type Rep (Benchmark a) = D1 ('MetaData "Benchmark" "Agda.Utils.Benchmark" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))

Methods

from :: Benchmark a -> Rep (Benchmark a) x Source #

to :: Rep (Benchmark a) x -> Benchmark a Source #

type Rep (Benchmark a) Source # |

Instance details

Defined in Agda.Utils.Benchmark

type Rep (Benchmark a) = D1 ('MetaData "Benchmark" "Agda.Utils.Benchmark" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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

getBenchmark, (putBenchmark | modifyBenchmark), finally

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

Instances details

MonadBench TerM Source # |

Instance details

Defined in Agda.Termination.Monad

Associated Types

type BenchPhase TerM |
Instance details Defined in Agda.Termination.Monad type BenchPhase TerM = Phase

Methods

getBenchmark :: TerM (Benchmark (BenchPhase TerM)) Source #

putBenchmark :: Benchmark (BenchPhase TerM) -> TerM () Source #

modifyBenchmark :: (Benchmark (BenchPhase TerM) -> Benchmark (BenchPhase TerM)) -> TerM () Source #

finally :: TerM b -> TerM c -> TerM b Source #

MonadBench TCM Source # | We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Associated Types

type BenchPhase TCM |
Instance details Defined in Agda.TypeChecking.Monad.Base type BenchPhase TCM = Phase

Methods

getBenchmark :: TCM (Benchmark (BenchPhase TCM)) Source #

putBenchmark :: Benchmark (BenchPhase TCM) -> TCM () Source #

modifyBenchmark :: (Benchmark (BenchPhase TCM) -> Benchmark (BenchPhase TCM)) -> TCM () Source #

finally :: TCM b -> TCM c -> TCM b Source #

MonadBench IO Source # |

Instance details

Defined in Agda.Benchmarking

Associated Types

type BenchPhase IO |
Instance details Defined in Agda.Benchmarking type BenchPhase IO = Phase

Methods

getBenchmark :: IO (Benchmark (BenchPhase IO)) Source #

putBenchmark :: Benchmark (BenchPhase IO) -> IO () Source #

modifyBenchmark :: (Benchmark (BenchPhase IO) -> Benchmark (BenchPhase IO)) -> IO () Source #

finally :: IO b -> IO c -> IO b Source #

MonadBench m => MonadBench (ListT m) Source # |

Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (ListT m) |
Instance details Defined in Agda.Utils.Benchmark type BenchPhase (ListT m) = BenchPhase m

Methods

getBenchmark :: ListT m (Benchmark (BenchPhase (ListT m))) Source #

putBenchmark :: Benchmark (BenchPhase (ListT m)) -> ListT m () Source #

modifyBenchmark :: (Benchmark (BenchPhase (ListT m)) -> Benchmark (BenchPhase (ListT m))) -> ListT m () Source #

finally :: ListT m b -> ListT m c -> ListT m b Source #

MonadBench m => MonadBench (ExceptT e m) Source # |

Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (ExceptT e m) |
Instance details Defined in Agda.Utils.Benchmark type BenchPhase (ExceptT e m) = BenchPhase m

Methods

getBenchmark :: ExceptT e m (Benchmark (BenchPhase (ExceptT e m))) Source #

putBenchmark :: Benchmark (BenchPhase (ExceptT e m)) -> ExceptT e m () Source #

modifyBenchmark :: (Benchmark (BenchPhase (ExceptT e m)) -> Benchmark (BenchPhase (ExceptT e m))) -> ExceptT e m () Source #

finally :: ExceptT e m b -> ExceptT e m c -> ExceptT e m b Source #

MonadBench m => MonadBench (ReaderT r m) Source # |

Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (ReaderT r m) |
Instance details Defined in Agda.Utils.Benchmark type BenchPhase (ReaderT r m) = BenchPhase m

Methods

getBenchmark :: ReaderT r m (Benchmark (BenchPhase (ReaderT r m))) Source #

putBenchmark :: Benchmark (BenchPhase (ReaderT r m)) -> ReaderT r m () Source #

modifyBenchmark :: (Benchmark (BenchPhase (ReaderT r m)) -> Benchmark (BenchPhase (ReaderT r m))) -> ReaderT r m () Source #

finally :: ReaderT r m b -> ReaderT r m c -> ReaderT r m b Source #

MonadBench m => MonadBench (StateT r m) Source # |

Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (StateT r m) |
Instance details Defined in Agda.Utils.Benchmark type BenchPhase (StateT r m) = BenchPhase m

Methods

getBenchmark :: StateT r m (Benchmark (BenchPhase (StateT r m))) Source #

putBenchmark :: Benchmark (BenchPhase (StateT r m)) -> StateT r m () Source #

modifyBenchmark :: (Benchmark (BenchPhase (StateT r m)) -> Benchmark (BenchPhase (StateT r m))) -> StateT r m () Source #

finally :: StateT r m b -> StateT r m c -> StateT r m b Source #

(MonadBench m, Monoid w) => MonadBench (WriterT w m) Source # |

Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (WriterT w m) |
Instance details Defined in Agda.Utils.Benchmark type BenchPhase (WriterT w m) = BenchPhase m

Methods

getBenchmark :: WriterT w m (Benchmark (BenchPhase (WriterT w m))) Source #

putBenchmark :: Benchmark (BenchPhase (WriterT w m)) -> WriterT w m () Source #

modifyBenchmark :: (Benchmark (BenchPhase (WriterT w m)) -> Benchmark (BenchPhase (WriterT w m))) -> WriterT w m () Source #

finally :: WriterT w m b -> WriterT w m c -> WriterT w m b Source #

getsBenchmark :: MonadBench m => (Benchmark (BenchPhase m) -> c) -> m c Source #

setBenchmarking :: MonadBench m => BenchmarkOn (BenchPhase m) -> m () Source #

Turn benchmarking on/off.

switchBenchmarking Source #

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.