Safe Haskell	None
Language	Haskell98

Agda.Benchmarking

Contents

Description

Agda-specific benchmarking structure.

Synopsis

Documentation

Phases to allocate CPU time to.

Constructors

Parsing	Happy parsing and operator parsing.
Import	Import chasing.
Deserialization	Reading interface files.
Scoping	Scope checking and translation to abstract syntax.
Typing	Type checking and translation to internal syntax.
Termination	Termination checking.
Positivity	Positivity checking and polarity computation.
Injectivity	Injectivity checking.
ProjectionLikeness	Checking for projection likeness.
Coverage	Coverage checking and compilation to case trees.
Highlighting	Generating highlighting info.
Serialization	Writing interface files.
Graph	Subphase for `Termination`.
RecCheck	Subphase for `Termination`.
Reduce	Subphase for `Termination`.
Level	Subphase for `Termination`.
Compare	Subphase for `Termination`.
With	Subphase for `Termination`.
ModuleName	Subphase for `Import`.
Sort	Subphase for `Serialize`.
BinaryEncode	Subphase for `Serialize`.
Compress	Subphase for `Serialize`.
Operators	Subphase for `Parsing`.
Free	Subphase for `Typing`: free variable computation.
OccursCheck	Subphase for `Typing`: occurs check for solving metas.
InverseScopeLookup	Pretty printing names.

Instances

Bounded Phase Source
Enum Phase Source
Eq Phase Source
Ord Phase Source
Show Phase Source
Pretty Phase Source
MonadBench Phase TCM Source	We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.
MonadBench Phase TerM Source

Benchmarking in the IO monad.

Global variable to store benchmark statistics.

Benchmark an IO computation and bill it to the given account.

Benchmark a pure computation and bill it to the given account.