Agda-2.6.4.3: 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.

DeadCodeInstantiateFull

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

UnifyIndices

Subphase for CheckLHS: unification of the indices

InverseScopeLookup

Pretty printing names.

TopModule TopLevelModuleName 
Definition QName 

Instances

Instances details
Pretty Phase Source # 
Instance details

Defined in Agda.Benchmarking

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.4.3-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 "DeadCodeInstantiateFull" '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 "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 "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 #

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.6.4.3-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 "DeadCodeInstantiateFull" '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 "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 "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