ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Monad.Benchmark

Measure CPU time for individual phases of the Agda pipeline.

module Agda.Benchmarking

classclass (Ord (BenchPhase m), Functor m, MonadIO m) => MonadBench (m :: Type -> Type) where

Monad with access to benchmarking data.

Instances8MonadBench, …

MonadBench TerMDefined in Agda-2.7.0.1 · Agda.Termination.Monad
MonadBench TCMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.
MonadBench IODefined in Agda-2.7.0.1 · Agda.Benchmarking · orphan
MonadBench m => MonadBench (ListT m)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
MonadBench m => MonadBench (ExceptT e m)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
MonadBench m => MonadBench (ReaderT r m)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
MonadBench m => MonadBench (StateT r m)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark
(MonadBench m, Monoid w) => MonadBench (WriterT w m)Defined in Agda-2.7.0.1 · Agda.Utils.Benchmark

familytype family BenchPhase (m :: Type -> Type)

Instances8BenchPhase, …

type BenchPhase TerM = PhaseDefined in Agda-2.7.0.1 · Agda.Termination.Monad
type BenchPhase TCM = PhaseDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base
type BenchPhase IO = PhaseDefined in Agda-2.7.0.1 · Agda.Benchmarking · orphan
type BenchPhase (ListT m) = BenchPhase mDefined in Agda-2.7.0.1 · Agda.Utils.Benchmark
type BenchPhase (ExceptT e m) = BenchPhase mDefined in Agda-2.7.0.1 · Agda.Utils.Benchmark
type BenchPhase (ReaderT r m) = BenchPhase mDefined in Agda-2.7.0.1 · Agda.Utils.Benchmark
type BenchPhase (StateT r m) = BenchPhase mDefined in Agda-2.7.0.1 · Agda.Utils.Benchmark
type BenchPhase (WriterT w m) = BenchPhase mDefined in Agda-2.7.0.1 · Agda.Utils.Benchmark

methodgetBenchmark :: m (Benchmark (BenchPhase m))

valueupdateBenchmarkingStatus :: TCM ()

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

valuebillTo :: MonadBench m => Account (BenchPhase m) -> m c -> m c

Bill a computation to a specific account. Works even if the computation is aborted by an exception.

valuebillPureTo :: MonadBench m => Account (BenchPhase m) -> c -> m c

Bill a pure computation to a specific account.

valuebillToCPS

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

valuereset :: MonadBench m => m ()

Resets the account and the timing information.

valueprint :: MonadTCM tcm => tcm ()

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