Mikan

Safe Haskell	None
Language	Haskell2010

Mikan.TypeChecking.Monad.Benchmark

Description

Measure CPU time for individual phases of the Agda pipeline.

Synopsis

module Mikan.Benchmarking
class (Ord (BenchPhase m), Functor m, MonadIO m) => MonadBench (m :: Type -> Type)
type family BenchPhase (m :: Type -> Type)
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 Mikan.Benchmarking

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

Monad with access to benchmarking data.

Minimal complete definition

getBenchmark, (putBenchmark | modifyBenchmark), finally

Instances

Instances details

MonadBench TerM Source #

Instance details

Defined in Mikan.Termination.Monad

Associated Types

type BenchPhase TerM
Instance details Defined in Mikan.Termination.Monad type BenchPhase TerM = Phase

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 Mikan.TypeChecking.Monad.Base

Associated Types

type BenchPhase TCM
Instance details Defined in Mikan.TypeChecking.Monad.Base type BenchPhase TCM = Phase

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 Mikan.Benchmarking

Associated Types

type BenchPhase IO
Instance details Defined in Mikan.Benchmarking type BenchPhase IO = Phase

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 Mikan.Utils.Benchmark

Associated Types

type BenchPhase (ListT m)
Instance details Defined in Mikan.Utils.Benchmark type BenchPhase (ListT m) = BenchPhase m

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 (ReaderT r m) Source #

Instance details

Defined in Mikan.Utils.Benchmark

Associated Types

type BenchPhase (ReaderT r m)
Instance details Defined in Mikan.Utils.Benchmark type BenchPhase (ReaderT r m) = BenchPhase m

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 (ExceptT e m) Source #

Instance details

Defined in Mikan.Utils.Benchmark

Associated Types

type BenchPhase (ExceptT e m)
Instance details Defined in Mikan.Utils.Benchmark type BenchPhase (ExceptT e m) = BenchPhase m

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 Mikan.Utils.Benchmark

Associated Types

type BenchPhase (ReaderT r m)
Instance details Defined in Mikan.Utils.Benchmark type BenchPhase (ReaderT r m) = BenchPhase m

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 Mikan.Utils.Benchmark

Associated Types

type BenchPhase (StateT r m)
Instance details Defined in Mikan.Utils.Benchmark type BenchPhase (StateT r m) = BenchPhase m

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 Mikan.Utils.Benchmark

Associated Types

type BenchPhase (WriterT w m)
Instance details Defined in Mikan.Utils.Benchmark type BenchPhase (WriterT w m) = BenchPhase m

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 :: Type -> Type) Source #

Instances

Instances details

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

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

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.