Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Monad.Base.Benchmark

Description

Data structures for collecting CPU usage.

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`.
Operators	Subphase for `Parsing`.
BuildParser	Subphase for `Operators`.

Instances

Account we can bill computation time to.

We measure CPU time spent on certain tasks.

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

Initial benchmark structure (empty).

Add to specified CPU time account.