Agda.TypeChecking.Monad.Base.Benchmark

Data structures for collecting CPU usage.

Documentation

data Phase

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

Bounded Phase

Enum Phase

Eq Phase

Ord Phase

Show Phase

type Account = [Phase]

Account we can bill computation time to.

type CPUTime = Integer

We measure CPU time spent on certain tasks.

type Benchmark = Trie Phase CPUTime

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

empty :: Benchmark

Initial benchmark structure (empty).

addCPUTime :: Account -> CPUTime -> Benchmark -> Benchmark

Add to specified CPU time account.