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

Instances details

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