Agda.TypeChecking.Monad.Benchmark

Measure CPU time for individual phases of the Agda pipeline.

Documentation

module Agda.Benchmarking

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

Monad with access to benchmarking data.

Minimal complete definition

getBenchmark, finally

Instances

MonadBench TerM

Defined in Agda.Termination.Monad

Associated Types

type BenchPhase TerM

Defined in Agda.Termination.Monad

type BenchPhase TerM = Phase

Methods

getBenchmark :: TerM (Benchmark (BenchPhase TerM))

putBenchmark :: Benchmark (BenchPhase TerM) -> TerM ()

modifyBenchmark :: (Benchmark (BenchPhase TerM) -> Benchmark (BenchPhase TerM)) -> TerM ()

finally :: TerM b -> TerM c -> TerM b

MonadBench TCM

We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.

Defined in Agda.TypeChecking.Monad.Base

Associated Types

type BenchPhase TCM

Defined in Agda.TypeChecking.Monad.Base

type BenchPhase TCM = Phase

Methods

getBenchmark :: TCM (Benchmark (BenchPhase TCM))

putBenchmark :: Benchmark (BenchPhase TCM) -> TCM ()

modifyBenchmark :: (Benchmark (BenchPhase TCM) -> Benchmark (BenchPhase TCM)) -> TCM ()

finally :: TCM b -> TCM c -> TCM b

MonadBench IO

Defined in Agda.Benchmarking

Associated Types

type BenchPhase IO

Defined in Agda.Benchmarking

type BenchPhase IO = Phase

Methods

getBenchmark :: IO (Benchmark (BenchPhase IO))

putBenchmark :: Benchmark (BenchPhase IO) -> IO ()

modifyBenchmark :: (Benchmark (BenchPhase IO) -> Benchmark (BenchPhase IO)) -> IO ()

finally :: IO b -> IO c -> IO b

MonadBench m => MonadBench (ListT m)

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (ListT m)

Defined in Agda.Utils.Benchmark

type BenchPhase (ListT m) = BenchPhase m

Methods

getBenchmark :: ListT m (Benchmark (BenchPhase (ListT m)))

putBenchmark :: Benchmark (BenchPhase (ListT m)) -> ListT m ()

modifyBenchmark :: (Benchmark (BenchPhase (ListT m)) -> Benchmark (BenchPhase (ListT m))) -> ListT m ()

finally :: ListT m b -> ListT m c -> ListT m b

MonadBench m => MonadBench (ExceptT e m)

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (ExceptT e m)

Defined in Agda.Utils.Benchmark

type BenchPhase (ExceptT e m) = BenchPhase m

Methods

getBenchmark :: ExceptT e m (Benchmark (BenchPhase (ExceptT e m)))

putBenchmark :: Benchmark (BenchPhase (ExceptT e m)) -> ExceptT e m ()

modifyBenchmark :: (Benchmark (BenchPhase (ExceptT e m)) -> Benchmark (BenchPhase (ExceptT e m))) -> ExceptT e m ()

finally :: ExceptT e m b -> ExceptT e m c -> ExceptT e m b

MonadBench m => MonadBench (ReaderT r m)

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (ReaderT r m)

Defined in Agda.Utils.Benchmark

type BenchPhase (ReaderT r m) = BenchPhase m

Methods

getBenchmark :: ReaderT r m (Benchmark (BenchPhase (ReaderT r m)))

putBenchmark :: Benchmark (BenchPhase (ReaderT r m)) -> ReaderT r m ()

modifyBenchmark :: (Benchmark (BenchPhase (ReaderT r m)) -> Benchmark (BenchPhase (ReaderT r m))) -> ReaderT r m ()

finally :: ReaderT r m b -> ReaderT r m c -> ReaderT r m b

MonadBench m => MonadBench (StateT r m)

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (StateT r m)

Defined in Agda.Utils.Benchmark

type BenchPhase (StateT r m) = BenchPhase m

Methods

getBenchmark :: StateT r m (Benchmark (BenchPhase (StateT r m)))

putBenchmark :: Benchmark (BenchPhase (StateT r m)) -> StateT r m ()

modifyBenchmark :: (Benchmark (BenchPhase (StateT r m)) -> Benchmark (BenchPhase (StateT r m))) -> StateT r m ()

finally :: StateT r m b -> StateT r m c -> StateT r m b

(MonadBench m, Monoid w) => MonadBench (WriterT w m)

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (WriterT w m)

Defined in Agda.Utils.Benchmark

type BenchPhase (WriterT w m) = BenchPhase m

Methods

getBenchmark :: WriterT w m (Benchmark (BenchPhase (WriterT w m)))

putBenchmark :: Benchmark (BenchPhase (WriterT w m)) -> WriterT w m ()

modifyBenchmark :: (Benchmark (BenchPhase (WriterT w m)) -> Benchmark (BenchPhase (WriterT w m))) -> WriterT w m ()

finally :: WriterT w m b -> WriterT w m c -> WriterT w m b

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

Instances

type BenchPhase TerM

Defined in Agda.Termination.Monad

type BenchPhase TerM = Phase

type BenchPhase TCM

Defined in Agda.TypeChecking.Monad.Base

type BenchPhase TCM = Phase

type BenchPhase IO

Defined in Agda.Benchmarking

type BenchPhase IO = Phase

type BenchPhase (ListT m)

Defined in Agda.Utils.Benchmark

type BenchPhase (ListT m) = BenchPhase m

type BenchPhase (ExceptT e m)

Defined in Agda.Utils.Benchmark

type BenchPhase (ExceptT e m) = BenchPhase m

type BenchPhase (ReaderT r m)

Defined in Agda.Utils.Benchmark

type BenchPhase (ReaderT r m) = BenchPhase m

type BenchPhase (StateT r m)

Defined in Agda.Utils.Benchmark

type BenchPhase (StateT r m) = BenchPhase m

type BenchPhase (WriterT w m)

Defined in Agda.Utils.Benchmark

type BenchPhase (WriterT w m) = BenchPhase m

getBenchmark :: MonadBench m => m (Benchmark (BenchPhase m))

updateBenchmarkingStatus :: TCM ()

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

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

Bill a pure computation to a specific account.

billToCPS :: MonadBench m => Account (BenchPhase m) -> ((b -> m c) -> m c) -> (b -> m c) -> m c

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

reset :: MonadBench m => m ()

Resets the account and the timing information.

print :: MonadTCM tcm => tcm ()

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