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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Benchmark

Description

Measure CPU time for individual phases of the Agda pipeline.

Synopsis

- module Agda.Benchmarking
- class (Ord a, Functor m, MonadIO m) => MonadBench a m | m -> a
- getBenchmark :: MonadBench a m => m (Benchmark a)
- updateBenchmarkingStatus :: TCM ()
- billTo :: MonadBench a m => Account a -> m c -> m c
- billPureTo :: MonadBench a m => Account a -> c -> m c
- billToCPS :: MonadBench a m => Account a -> ((b -> m c) -> m c) -> (b -> m c) -> m c
- reset :: MonadBench a m => m ()
- print :: MonadTCM tcm => tcm ()

# Documentation

module Agda.Benchmarking

class (Ord a, Functor m, MonadIO m) => MonadBench a m | m -> a Source #

Monad with access to benchmarking data.

Minimal complete definition

getBenchmark, finally

Instances

MonadBench Phase IO Source # |
Instance details Defined in Agda.Benchmarking Methods getBenchmark :: IO (Benchmark Phase) Source # getsBenchmark :: (Benchmark Phase -> c) -> IO c Source # putBenchmark :: Benchmark Phase -> IO () Source # modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> IO () Source # finally :: IO b -> IO c -> IO b Source #
MonadBench Phase 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 Methods getBenchmark :: TCM (Benchmark Phase) Source # getsBenchmark :: (Benchmark Phase -> c) -> TCM c Source # putBenchmark :: Benchmark Phase -> TCM () Source # modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> TCM () Source # finally :: TCM b -> TCM c -> TCM b Source #
MonadBench Phase TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods getBenchmark :: TerM (Benchmark Phase) Source # getsBenchmark :: (Benchmark Phase -> c) -> TerM c Source # putBenchmark :: Benchmark Phase -> TerM () Source # modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> TerM () Source # finally :: TerM b -> TerM c -> TerM b Source #
MonadBench a m => MonadBench a (StateT r m) Source # |
Instance details Defined in Agda.Utils.Benchmark Methods getBenchmark :: StateT r m (Benchmark a) Source # getsBenchmark :: (Benchmark a -> c) -> StateT r m c Source # putBenchmark :: Benchmark a -> StateT r m () Source # modifyBenchmark :: (Benchmark a -> Benchmark a) -> StateT r m () Source # finally :: StateT r m b -> StateT r m c -> StateT r m b Source #
MonadBench a m => MonadBench a (ReaderT r m) Source # |
Instance details Defined in Agda.Utils.Benchmark Methods getBenchmark :: ReaderT r m (Benchmark a) Source # getsBenchmark :: (Benchmark a -> c) -> ReaderT r m c Source # putBenchmark :: Benchmark a -> ReaderT r m () Source # modifyBenchmark :: (Benchmark a -> Benchmark a) -> ReaderT r m () Source # finally :: ReaderT r m b -> ReaderT r m c -> ReaderT r m b Source #

getBenchmark :: MonadBench a m => m (Benchmark a) Source #

updateBenchmarkingStatus :: TCM () Source #

When verbosity is set or changes, we need to turn benchmarking on or off.

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.

billToCPS :: MonadBench a m => Account a -> ((b -> m c) -> m c) -> (b -> m c) -> m c Source #

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

reset :: MonadBench a m => m () Source #

Resets the account and the timing information.

print :: MonadTCM tcm => tcm () Source #

Prints the accumulated benchmark results. Does nothing if profiling is not activated at level 7.