Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Monad.Benchmark

Description

Measure CPU time for individual phases of the Agda pipeline.

Synopsis

module Agda.Benchmarking
class (Ord (BenchPhase m), Functor m, MonadIO m) => MonadBench m
type family BenchPhase m
getBenchmark :: MonadBench m => m (Benchmark (BenchPhase m))
updateBenchmarkingStatus :: TCM ()
billTo :: MonadBench m => Account (BenchPhase m) -> m c -> m c
billPureTo :: MonadBench m => Account (BenchPhase m) -> c -> m c
billToCPS :: MonadBench m => Account (BenchPhase m) -> ((b -> m c) -> m c) -> (b -> m c) -> m c
reset :: MonadBench m => m ()
print :: MonadTCM tcm => tcm ()

Documentation

module Agda.Benchmarking

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 # Methods getBenchmark :: TerM (Benchmark (BenchPhase TerM)) Source # putBenchmark :: Benchmark (BenchPhase TerM) -> TerM () Source # modifyBenchmark :: (Benchmark (BenchPhase TerM) -> Benchmark (BenchPhase TerM)) -> TerM () Source # finally :: TerM b -> TerM c -> TerM b 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 # Methods getBenchmark :: TCM (Benchmark (BenchPhase TCM)) Source # putBenchmark :: Benchmark (BenchPhase TCM) -> TCM () Source # modifyBenchmark :: (Benchmark (BenchPhase TCM) -> Benchmark (BenchPhase TCM)) -> TCM () Source # finally :: TCM b -> TCM c -> TCM b Source #
MonadBench IO Source #
Instance details Defined in Agda.Benchmarking Associated Types type BenchPhase IO Source # Methods getBenchmark :: IO (Benchmark (BenchPhase IO)) Source # putBenchmark :: Benchmark (BenchPhase IO) -> IO () Source # modifyBenchmark :: (Benchmark (BenchPhase IO) -> Benchmark (BenchPhase IO)) -> IO () Source # finally :: IO b -> IO c -> IO b Source #
MonadBench m => MonadBench (ListT m) Source #
Instance details Defined in Agda.Utils.Benchmark Associated Types type BenchPhase (ListT m) Source # Methods getBenchmark :: ListT m (Benchmark (BenchPhase (ListT m))) Source # putBenchmark :: Benchmark (BenchPhase (ListT m)) -> ListT m () Source # modifyBenchmark :: (Benchmark (BenchPhase (ListT m)) -> Benchmark (BenchPhase (ListT m))) -> ListT m () Source # finally :: ListT m b -> ListT m c -> ListT m b Source #
MonadBench m => MonadBench (ExceptT e m) Source #
Instance details Defined in Agda.Utils.Benchmark Associated Types type BenchPhase (ExceptT e m) Source # Methods getBenchmark :: ExceptT e m (Benchmark (BenchPhase (ExceptT e m))) Source # putBenchmark :: Benchmark (BenchPhase (ExceptT e m)) -> ExceptT e m () Source # modifyBenchmark :: (Benchmark (BenchPhase (ExceptT e m)) -> Benchmark (BenchPhase (ExceptT e m))) -> ExceptT e m () Source # finally :: ExceptT e m b -> ExceptT e m c -> ExceptT e m b Source #
MonadBench m => MonadBench (ReaderT r m) Source #
Instance details Defined in Agda.Utils.Benchmark Associated Types type BenchPhase (ReaderT r m) Source # Methods getBenchmark :: ReaderT r m (Benchmark (BenchPhase (ReaderT r m))) Source # putBenchmark :: Benchmark (BenchPhase (ReaderT r m)) -> ReaderT r m () Source # modifyBenchmark :: (Benchmark (BenchPhase (ReaderT r m)) -> Benchmark (BenchPhase (ReaderT r m))) -> ReaderT r m () Source # finally :: ReaderT r m b -> ReaderT r m c -> ReaderT r m b Source #
MonadBench m => MonadBench (StateT r m) Source #
Instance details Defined in Agda.Utils.Benchmark Associated Types type BenchPhase (StateT r m) Source # Methods getBenchmark :: StateT r m (Benchmark (BenchPhase (StateT r m))) Source # putBenchmark :: Benchmark (BenchPhase (StateT r m)) -> StateT r m () Source # modifyBenchmark :: (Benchmark (BenchPhase (StateT r m)) -> Benchmark (BenchPhase (StateT r m))) -> StateT r m () Source # finally :: StateT r m b -> StateT r m c -> StateT r m b 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 # Methods getBenchmark :: WriterT w m (Benchmark (BenchPhase (WriterT w m))) Source # putBenchmark :: Benchmark (BenchPhase (WriterT w m)) -> WriterT w m () Source # modifyBenchmark :: (Benchmark (BenchPhase (WriterT w m)) -> Benchmark (BenchPhase (WriterT w m))) -> WriterT w m () Source # finally :: WriterT w m b -> WriterT w m c -> WriterT w m b Source #

type family BenchPhase m Source #

Instances

Instances details

type BenchPhase TerM Source #
Instance details Defined in Agda.Termination.Monad type BenchPhase TerM = Phase
type BenchPhase TCM Source #
Instance details Defined in Agda.TypeChecking.Monad.Base type BenchPhase TCM = Phase
type BenchPhase IO Source #
Instance details Defined in Agda.Benchmarking type BenchPhase IO = Phase
type BenchPhase (ListT m) Source #
Instance details Defined in Agda.Utils.Benchmark type BenchPhase (ListT m) = BenchPhase m
type BenchPhase (ExceptT e m) Source #
Instance details Defined in Agda.Utils.Benchmark type BenchPhase (ExceptT e m) = BenchPhase m
type BenchPhase (ReaderT r m) Source #
Instance details Defined in Agda.Utils.Benchmark type BenchPhase (ReaderT r m) = BenchPhase m
type BenchPhase (StateT r m) Source #
Instance details Defined in Agda.Utils.Benchmark type BenchPhase (StateT r m) = BenchPhase m
type BenchPhase (WriterT w m) Source #
Instance details Defined in Agda.Utils.Benchmark type BenchPhase (WriterT w m) = BenchPhase m

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

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.