Agda-2.8.0: 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
  - | 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 #
NFData Phase Source # |
Instance details Defined in Agda.Benchmarking Methods rnf :: Phase -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep Phase x -> Phase Source #

Show Phase Source # |
Instance details Defined in Agda.Benchmarking Methods showsPrec :: Int -> Phase -> ShowS Source # show :: Phase -> String Source # showList :: [Phase] -> ShowS Source #
Eq Phase Source # |
Instance details Defined in Agda.Benchmarking Methods (==) :: Phase -> Phase -> Bool Source # (/=) :: Phase -> Phase -> Bool Source #
Ord Phase Source # |
Instance details Defined in Agda.Benchmarking Methods compare :: Phase -> Phase -> Ordering Source # (<) :: Phase -> Phase -> Bool Source # (<=) :: Phase -> Phase -> Bool Source # (>) :: Phase -> Phase -> Bool Source # (>=) :: Phase -> Phase -> Bool Source # max :: Phase -> Phase -> Phase Source # min :: Phase -> Phase -> Phase Source #
type Rep Phase Source # |

Instance details

Defined in Agda.Benchmarking

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