Safe Haskell	None
Language	Haskell2010

Agda.Benchmarking

Contents

Benchmarking in the IO monad.
Orphan instances

Description

Agda-specific benchmarking structure.

Synopsis

data Phase
- = Parsing
- | Import
- | Deserialization
- | Scoping
- | Typing
- | Termination
- | Positivity
- | Injectivity
- | ProjectionLikeness
- | Coverage
- | Highlighting
- | Serialization
- | DeadCode
- | Graph
- | RecCheck
- | Reduce
- | Level
- | Compare
- | With
- | ModuleName
- | Compaction
- | BuildInterface
- | Sort
- | BinaryEncode
- | Compress
- | OperatorsExpr
- | OperatorsPattern
- | Free
- | OccursCheck
- | CheckLHS
- | CheckRHS
- | TypeSig
- | Generalize
- | InstanceSearch
- | UnifyIndices
- | InverseScopeLookup
- | TopModule TopLevelModuleName
- | Definition QName
type Benchmark = Benchmark Phase
type Account = Account Phase
isModuleAccount :: Account -> Bool
isDefAccount :: Account -> Bool
isInternalAccount :: Account -> Bool
benchmarks :: IORef Benchmark
billToIO :: Account -> IO a -> IO a
billToPure :: Account -> a -> a

Documentation

data Phase Source #

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.
DeadCode	Deac code elimination.
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`.
Compaction	Subphase for `Deserialization`: compacting interfaces.
BuildInterface	Subphase for `Serialization`.
Sort	Subphase for `Serialization`.
BinaryEncode	Subphase for `Serialization`.
Compress	Subphase for `Serialization`.
OperatorsExpr	Subphase for `Parsing`.
OperatorsPattern	Subphase for `Parsing`.
Free	Subphase for `Typing`: free variable computation.
OccursCheck	Subphase for `Typing`: occurs check for solving metas.
CheckLHS	Subphase for `Typing`: checking the LHS
CheckRHS	Subphase for `Typing`: checking the RHS
TypeSig	Subphase for `Typing`: checking a type signature
Generalize	Subphase for `Typing`: generalizing over `variable`s
InstanceSearch	Subphase for `Typing`: solving instance goals
UnifyIndices	Subphase for `CheckLHS`: unification of the indices
InverseScopeLookup	Pretty printing names.
TopModule TopLevelModuleName
Definition QName

Instances

Instances details

Eq Phase Source #
Instance details Defined in Agda.Benchmarking Methods (==) :: Phase -> Phase -> Bool # (/=) :: Phase -> Phase -> Bool #
Ord Phase Source #
Instance details Defined in Agda.Benchmarking Methods compare :: Phase -> Phase -> Ordering # (<) :: Phase -> Phase -> Bool # (<=) :: Phase -> Phase -> Bool # (>) :: Phase -> Phase -> Bool # (>=) :: Phase -> Phase -> Bool # max :: Phase -> Phase -> Phase # min :: Phase -> Phase -> Phase #
Show Phase Source #
Instance details Defined in Agda.Benchmarking Methods showsPrec :: Int -> Phase -> ShowS # show :: Phase -> String # showList :: [Phase] -> ShowS #
Pretty Phase Source #
Instance details Defined in Agda.Benchmarking Methods pretty :: Phase -> Doc Source # prettyPrec :: Int -> Phase -> Doc Source # prettyList :: [Phase] -> Doc Source #
MonadBench Phase IO Source #
Instance details Defined in Agda.Benchmarking Methods getBenchmark :: IO (Benchmark Phase) Source # getsBenchmark :: (Benchmark Phase -> c) -> IO c Source # putBenchmark :: Benchmark Phase -> IO () Source # modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> IO () Source # finally :: IO b -> IO c -> IO b Source #
MonadBench Phase TCM Source #	We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getBenchmark :: TCM (Benchmark Phase) Source # getsBenchmark :: (Benchmark Phase -> c) -> TCM c Source # putBenchmark :: Benchmark Phase -> TCM () Source # modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> TCM () Source # finally :: TCM b -> TCM c -> TCM b Source #
MonadBench Phase TerM Source #
Instance details Defined in Agda.Termination.Monad Methods getBenchmark :: TerM (Benchmark Phase) Source # getsBenchmark :: (Benchmark Phase -> c) -> TerM c Source # putBenchmark :: Benchmark Phase -> TerM () Source # modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> TerM () Source # finally :: TerM b -> TerM c -> TerM b Source #

type Benchmark = Benchmark Phase Source #

type Account = Account Phase Source #

isModuleAccount :: Account -> Bool Source #

isDefAccount :: Account -> Bool Source #

isInternalAccount :: Account -> Bool Source #

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.

Orphan instances

MonadBench Phase IO Source #
Instance details Methods getBenchmark :: IO (Benchmark Phase) Source # getsBenchmark :: (Benchmark Phase -> c) -> IO c Source # putBenchmark :: Benchmark Phase -> IO () Source # modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> IO () Source # finally :: IO b -> IO c -> IO b Source #