| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Monad.Base.Benchmark
Description
Data structures for collecting CPU usage.
- data Phase
- type Account = [Phase]
- data Benchmark = Benchmark {}
- modifyCurrentAccount :: (Maybe Account -> Maybe Account) -> Benchmark -> Benchmark
- modifyTimings :: (Trie Phase CPUTime -> Trie Phase CPUTime) -> Benchmark -> Benchmark
- empty :: Benchmark
- addCPUTime :: Account -> CPUTime -> Benchmark -> Benchmark
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 |
| RecCheck | Subphase for |
| Reduce | Subphase for |
| Level | Subphase for |
| Compare | Subphase for |
| With | Subphase for |
| ModuleName | Subphase for |
| Sort | Subphase for |
| BinaryEncode | Subphase for |
| Compress | Subphase for |
| Operators | Subphase for |
Benchmark structure is a trie, mapping accounts (phases and subphases) to CPU time spent on their performance.
modifyCurrentAccount :: (Maybe Account -> Maybe Account) -> Benchmark -> Benchmark Source
Semantic editor combinator.