Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Benchmarking

Description

Agda-specific benchmarking structure.

Synopsis

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 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

Instances details
Pretty Phase Source # 
Instance details

Defined in Agda.Benchmarking

NFData Phase Source # 
Instance details

Defined in Agda.Benchmarking

Methods

rnf :: Phase -> ()

Generic Phase Source # 
Instance details

Defined in Agda.Benchmarking

Associated Types

type Rep Phase 
Instance details

Defined in Agda.Benchmarking

type Rep Phase = D1 ('MetaData "Phase" "Agda.Benchmarking" "Agda-2.6.20240714-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 Source # 
Instance details

Defined in Agda.Benchmarking

Methods

showsPrec :: Int -> Phase -> ShowS

show :: Phase -> String

showList :: [Phase] -> ShowS

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.6.20240714-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))))))))

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 
Instance details

Defined in Agda.Benchmarking

type BenchPhase IO = Phase

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 #