Agda-2.6.2.2.20230105: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Monad.Benchmark

Description

Measure CPU time for individual phases of the Agda pipeline.

Synopsis

Documentation

class (Ord (BenchPhase m), Functor m, MonadIO m) => MonadBench m Source #

Monad with access to benchmarking data.

Minimal complete definition

getBenchmark, finally

Instances

Instances details
MonadBench TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Associated Types

type BenchPhase TerM 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 Source #

MonadBench IO Source # 
Instance details

Defined in Agda.Benchmarking

Associated Types

type BenchPhase IO Source #

MonadBench m => MonadBench (ListT m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (ListT m) Source #

MonadBench m => MonadBench (ExceptT e m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (ExceptT e m) Source #

MonadBench m => MonadBench (ReaderT r m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (ReaderT r m) Source #

MonadBench m => MonadBench (StateT r m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (StateT r m) Source #

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

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (WriterT w m) Source #

type family BenchPhase m Source #

Instances

Instances details
type BenchPhase TerM Source # 
Instance details

Defined in Agda.Termination.Monad

type BenchPhase TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type BenchPhase IO Source # 
Instance details

Defined in Agda.Benchmarking

type BenchPhase (ListT m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

type BenchPhase (ExceptT e m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

type BenchPhase (ReaderT r m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

type BenchPhase (StateT r m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

type BenchPhase (WriterT w m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

updateBenchmarkingStatus :: TCM () Source #

When profile options are set or changed, we need to turn benchmarking on or off.

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.

billPureTo :: MonadBench m => Account (BenchPhase m) -> c -> m c Source #

Bill a pure computation to a specific account.

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.

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

Resets the account and the timing information.

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

Prints the accumulated benchmark results. Does nothing if no benchmark profiling is enabled.