Agda-2.6.4.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Benchmark

Description

Tools for benchmarking and accumulating results. Nothing Agda-specific in here.

Synopsis

Benchmark trie

type Account a = [a] Source #

Account we can bill computation time to.

type CurrentAccount a = Maybe (Account a, CPUTime) Source #

Record when we started billing the current account.

type Timings a = Trie a CPUTime Source #

data BenchmarkOn a Source #

Constructors

BenchmarkOff 
BenchmarkOn 
BenchmarkSome (Account a -> Bool) 

Instances

Instances details
Generic (BenchmarkOn a) Source # 
Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type Rep (BenchmarkOn a) 
Instance details

Defined in Agda.Utils.Benchmark

type Rep (BenchmarkOn a) = D1 ('MetaData "BenchmarkOn" "Agda.Utils.Benchmark" "Agda-2.6.4.1-inplace" 'False) (C1 ('MetaCons "BenchmarkOff" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BenchmarkOn" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BenchmarkSome" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Account a -> Bool)))))

Methods

from :: BenchmarkOn a -> Rep (BenchmarkOn a) x #

to :: Rep (BenchmarkOn a) x -> BenchmarkOn a #

NFData a => NFData (BenchmarkOn a) Source # 
Instance details

Defined in Agda.Utils.Benchmark

Methods

rnf :: BenchmarkOn a -> () #

type Rep (BenchmarkOn a) Source # 
Instance details

Defined in Agda.Utils.Benchmark

type Rep (BenchmarkOn a) = D1 ('MetaData "BenchmarkOn" "Agda.Utils.Benchmark" "Agda-2.6.4.1-inplace" 'False) (C1 ('MetaCons "BenchmarkOff" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BenchmarkOn" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BenchmarkSome" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Account a -> Bool)))))

isBenchmarkOn :: Account a -> BenchmarkOn a -> Bool Source #

data Benchmark a Source #

Benchmark structure is a trie, mapping accounts (phases and subphases) to CPU time spent on their performance.

Constructors

Benchmark 

Fields

Instances

Instances details
(Ord a, Pretty a) => Pretty (Benchmark a) Source #

Print benchmark as three-column table with totals.

Instance details

Defined in Agda.Utils.Benchmark

Methods

pretty :: Benchmark a -> Doc Source #

prettyPrec :: Int -> Benchmark a -> Doc Source #

prettyList :: [Benchmark a] -> Doc Source #

Null (Benchmark a) Source #

Initial benchmark structure (empty).

Instance details

Defined in Agda.Utils.Benchmark

Methods

empty :: Benchmark a Source #

null :: Benchmark a -> Bool Source #

Generic (Benchmark a) Source # 
Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type Rep (Benchmark a) 
Instance details

Defined in Agda.Utils.Benchmark

type Rep (Benchmark a) = D1 ('MetaData "Benchmark" "Agda.Utils.Benchmark" "Agda-2.6.4.1-inplace" 'False) (C1 ('MetaCons "Benchmark" 'PrefixI 'True) (S1 ('MetaSel ('Just "benchmarkOn") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (BenchmarkOn a)) :*: (S1 ('MetaSel ('Just "currentAccount") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (CurrentAccount a)) :*: S1 ('MetaSel ('Just "timings") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Timings a)))))

Methods

from :: Benchmark a -> Rep (Benchmark a) x #

to :: Rep (Benchmark a) x -> Benchmark a #

NFData a => NFData (Benchmark a) Source # 
Instance details

Defined in Agda.Utils.Benchmark

Methods

rnf :: Benchmark a -> () #

type Rep (Benchmark a) Source # 
Instance details

Defined in Agda.Utils.Benchmark

type Rep (Benchmark a) = D1 ('MetaData "Benchmark" "Agda.Utils.Benchmark" "Agda-2.6.4.1-inplace" 'False) (C1 ('MetaCons "Benchmark" 'PrefixI 'True) (S1 ('MetaSel ('Just "benchmarkOn") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (BenchmarkOn a)) :*: (S1 ('MetaSel ('Just "currentAccount") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (CurrentAccount a)) :*: S1 ('MetaSel ('Just "timings") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Timings a)))))

mapBenchmarkOn :: (BenchmarkOn a -> BenchmarkOn a) -> Benchmark a -> Benchmark a Source #

Semantic editor combinator.

mapCurrentAccount :: (CurrentAccount a -> CurrentAccount a) -> Benchmark a -> Benchmark a Source #

Semantic editor combinator.

mapTimings :: (Timings a -> Timings a) -> Benchmark a -> Benchmark a Source #

Semantic editor combinator.

addCPUTime :: Ord a => Account a -> CPUTime -> Benchmark a -> Benchmark a Source #

Add to specified CPU time account.

Benchmarking monad.

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

Monad with access to benchmarking data.

Minimal complete definition

getBenchmark, finally

Associated Types

type BenchPhase (m :: Type -> Type) Source #

Methods

getBenchmark :: m (Benchmark (BenchPhase m)) Source #

putBenchmark :: Benchmark (BenchPhase m) -> m () Source #

modifyBenchmark :: (Benchmark (BenchPhase m) -> Benchmark (BenchPhase m)) -> m () Source #

finally :: m b -> m c -> m b Source #

We need to be able to terminate benchmarking in case of an exception.

Instances

Instances details
MonadBench TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Associated Types

type BenchPhase TerM 
Instance details

Defined in Agda.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 Agda.TypeChecking.Monad.Base

Associated Types

type BenchPhase TCM 
Instance details

Defined in Agda.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 Agda.Benchmarking

Associated Types

type BenchPhase IO 
Instance details

Defined in Agda.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 Agda.Utils.Benchmark

Associated Types

type BenchPhase (ListT m) 
Instance details

Defined in Agda.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 (ExceptT e m) Source # 
Instance details

Defined in Agda.Utils.Benchmark

Associated Types

type BenchPhase (ExceptT e m) 
Instance details

Defined in Agda.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 Agda.Utils.Benchmark

Associated Types

type BenchPhase (ReaderT r m) 
Instance details

Defined in Agda.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 Agda.Utils.Benchmark

Associated Types

type BenchPhase (StateT r m) 
Instance details

Defined in Agda.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 Agda.Utils.Benchmark

Associated Types

type BenchPhase (WriterT w m) 
Instance details

Defined in Agda.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 #

getsBenchmark :: MonadBench m => (Benchmark (BenchPhase m) -> c) -> m c Source #

setBenchmarking :: MonadBench m => BenchmarkOn (BenchPhase m) -> m () Source #

Turn benchmarking on/off.

switchBenchmarking Source #

Arguments

:: MonadBench m 
=> Maybe (Account (BenchPhase m))

Maybe new account.

-> m (Maybe (Account (BenchPhase m)))

Maybe old account.

Bill current account with time up to now. Switch to new account. Return old account (if any).

reset :: MonadBench m => m () Source #

Resets the account and the timing information.

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.

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.

billPureTo :: MonadBench m => Account (BenchPhase m) -> c -> m c Source #

Bill a pure computation to a specific account.