Agda-2.6.4.1: A dependently typed functional programming language and proof assistant

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
- | DeadCodeInstantiateFull
- | DeadCodeReachable
- | 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	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 `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

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

Instance details

Defined in Agda.Benchmarking

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

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