Agda.Benchmarking

Agda-specific benchmarking structure.

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.

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 variables

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

Pretty Phase

Defined in Agda.Benchmarking

Methods

pretty :: Phase -> Doc

prettyPrec :: Int -> Phase -> Doc

prettyList :: [Phase] -> Doc

NFData Phase

Defined in Agda.Benchmarking

Methods

rnf :: Phase -> ()

Generic Phase

Defined in Agda.Benchmarking

Associated Types

type Rep Phase

Defined in Agda.Benchmarking

type Rep Phase = D1 ('MetaData "Phase" "Agda.Benchmarking" "Agda-2.6.20240731-inplace" '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))))))))

Methods

from :: Phase -> Rep Phase x

to :: Rep Phase x -> Phase

Show Phase

Defined in Agda.Benchmarking

Methods

showsPrec :: Int -> Phase -> ShowS

show :: Phase -> String

showList :: [Phase] -> ShowS

Eq Phase

Defined in Agda.Benchmarking

Methods

(==) :: Phase -> Phase -> Bool

(/=) :: Phase -> Phase -> Bool

Ord Phase

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

Defined in Agda.Benchmarking

type Rep Phase = D1 ('MetaData "Phase" "Agda.Benchmarking" "Agda-2.6.20240731-inplace" '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

type Account = Account Phase

isModuleAccount :: Account -> Bool

isDefAccount :: Account -> Bool

isInternalAccount :: Account -> Bool

Benchmarking in the IO monad.

benchmarks :: IORef Benchmark

Global variable to store benchmark statistics.

billToIO :: Account -> IO a -> IO a

Benchmark an IO computation and bill it to the given account.

billToPure :: Account -> a -> a

Benchmark a pure computation and bill it to the given account.

Orphan instances

MonadBench IO

Associated Types

type BenchPhase IO

Defined in Agda.Benchmarking

type BenchPhase IO = Phase

Methods

getBenchmark :: IO (Benchmark (BenchPhase IO))

putBenchmark :: Benchmark (BenchPhase IO) -> IO ()

modifyBenchmark :: (Benchmark (BenchPhase IO) -> Benchmark (BenchPhase IO)) -> IO ()

finally :: IO b -> IO c -> IO b