Safe Haskell	Safe-Inferred
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
- | InterfaceInstantiateFull
- | DeadCodeReachable
- | Graph
- | RecCheck
- | Reduce
- | Level
- | Compare
- | With
- | ModuleName
- | Compaction
- | BuildInterface
- | Sort
- | BinaryEncode
- | Compress
- | OperatorsExpr
- | OperatorsPattern
- | Free
- | OccursCheck
- | CheckLHS
- | CheckRHS
- | TypeSig
- | Generalize
- | InstanceSearch
- | Reflection
- | InitialCandidates
- | FilterCandidates
- | OrderCandidates
- | CheckOverlap
- | UnifyIndices
- | InverseScopeLookup
- | TopModule TopLevelModuleName
- | Typeclass QName
- | 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	Dead code elimination.
InterfaceInstantiateFull	Unfolding all metas before serialization.
DeadCodeReachable	Dead code reachable definitions subphase.
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
Reflection	Subphase for `Typing`: evaluating elaborator reflection
InitialCandidates	Subphase for `InstanceSearch`: collecting initial candidates
FilterCandidates	Subphase for `InstanceSearch`: checking candidates for validity
OrderCandidates	Subphase for `InstanceSearch`: ordering candidates for specificity
CheckOverlap	Subphase for `InstanceSearch`: reducing overlapping instances
UnifyIndices	Subphase for `CheckLHS`: unification of the indices
InverseScopeLookup	Pretty printing names.
TopModule TopLevelModuleName
Typeclass QName
Definition QName

Instances

Instances details

Pretty Phase Source #
Instance details Defined in Agda.Benchmarking Methods pretty :: Phase -> Doc Source # prettyPrec :: Int -> Phase -> Doc Source # prettyList :: [Phase] -> Doc Source #
Generic Phase Source #
Instance details Defined in Agda.Benchmarking Associated Types type Rep Phase :: Type -> Type # Methods from :: Phase -> Rep Phase x # to :: Rep Phase x -> Phase #
Show Phase Source #
Instance details Defined in Agda.Benchmarking Methods showsPrec :: Int -> Phase -> ShowS # show :: Phase -> String # showList :: [Phase] -> ShowS #
NFData Phase Source #
Instance details Defined in Agda.Benchmarking Methods rnf :: Phase -> () #
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 #
type Rep Phase Source #
Instance details Defined in Agda.Benchmarking type Rep Phase = D1 ('MetaData "Phase" "Agda.Benchmarking" "Agda-2.7.0-GLfwtYnpcYgL7izVkqfuSR" 'False) (((((C1 ('MetaCons "Parsing" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Import" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Deserialization" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Scoping" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Typing" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Termination" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Positivity" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Injectivity" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "ProjectionLikeness" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Coverage" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Highlighting" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "Serialization" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DeadCode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InterfaceInstantiateFull" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "DeadCodeReachable" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Graph" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RecCheck" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Reduce" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Level" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Compare" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "With" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ModuleName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Compaction" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "BuildInterface" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Sort" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BinaryEncode" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Compress" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OperatorsExpr" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "OperatorsPattern" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Free" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OccursCheck" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "CheckLHS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CheckRHS" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeSig" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "Generalize" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "InstanceSearch" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Reflection" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "InitialCandidates" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FilterCandidates" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OrderCandidates" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "CheckOverlap" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UnifyIndices" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InverseScopeLookup" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TopModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName)) :+: (C1 ('MetaCons "Typeclass" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "Definition" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))))))

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 IO Source #
Instance details Associated Types type BenchPhase IO Source # Methods getBenchmark :: IO (Benchmark (BenchPhase IO)) Source # putBenchmark :: Benchmark (BenchPhase IO) -> IO () Source # modifyBenchmark :: (Benchmark (BenchPhase IO) -> Benchmark (BenchPhase IO)) -> IO () Source # finally :: IO b -> IO c -> IO b Source #