Agda-2.4.2.3: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Monad.Base.Benchmark

Description

Data structures for collecting CPU usage.

Synopsis

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.

BinaryEncode

Subphase for Serialize.

Compress

Subphase for Serialize.

Operators

Subphase for Parsing.

type Account = [Phase]

Account we can bill computation time to. A word of Phases.

data Benchmark

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

Constructors

Benchmark 

modifyCurrentAccount :: (Maybe Account -> Maybe Account) -> Benchmark -> Benchmark

Semantic editor combinator.

modifyTimings :: (Trie Phase CPUTime -> Trie Phase CPUTime) -> Benchmark -> Benchmark

Semantic editor combinator.

empty :: Benchmark

Initial benchmark structure (empty).

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

Add to specified CPU time account.