Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda-specific benchmarking structure.
Documentation
Phases to allocate CPU time to.
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 |
Free | Subphase for |
OccursCheck | Subphase for |
InverseScopeLookup | Pretty printing names. |
Benchmarking in the IO monad.
benchmarks :: IORef Benchmark Source
Global variable to store benchmark statistics.
billToIO :: Account -> IO a -> IO a Source
Benchmark an IO computation and bill it to the given account.
billToPure :: Account -> a -> a Source
Benchmark a pure computation and bill it to the given account.