Agda-2.6.2.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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 IO Source # 
Instance details

Defined in Agda.Benchmarking

Associated Types

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

Defined in Agda.Termination.Monad

Associated Types

type BenchPhase TerM 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, Monoid w) => MonadBench (WriterT w m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (WriterT w m) Source #

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

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (StateT r m) Source #

type family BenchPhase m Source #

Instances

Instances details
type BenchPhase IO Source # 
Instance details

Defined in Agda.Benchmarking

type BenchPhase TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type BenchPhase TerM Source # 
Instance details

Defined in Agda.Termination.Monad

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 (WriterT w m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

type BenchPhase (StateT r m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

updateBenchmarkingStatus :: TCM () Source #

When verbosity is set or changes, 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 profiling is not activated at level 2.