| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Benchmarking
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
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 |
| RecCheck | Subphase for |
| Reduce | Subphase for |
| Level | Subphase for |
| Compare | Subphase for |
| With | Subphase for |
| ModuleName | Subphase for |
| Compaction | Subphase for |
| BuildInterface | Subphase for |
| Sort | Subphase for |
| BinaryEncode | Subphase for |
| Compress | Subphase for |
| OperatorsExpr | Subphase for |
| OperatorsPattern | Subphase for |
| Free | Subphase for |
| OccursCheck | Subphase for |
| CheckLHS | Subphase for |
| CheckRHS | Subphase for |
| TypeSig | Subphase for |
| Generalize | Subphase for |
| InstanceSearch | Subphase for |
| Reflection | Subphase for |
| InitialCandidates | Subphase for |
| FilterCandidates | Subphase for |
| OrderCandidates | Subphase for |
| CheckOverlap | Subphase for |
| UnifyIndices | Subphase for |
| InverseScopeLookup | Pretty printing names. |
| TopModule TopLevelModuleName | |
| Typeclass QName | |
| Definition QName |
Instances
| Pretty Phase Source # | |||||
| NFData Phase Source # | |||||
Defined in Agda.Benchmarking | |||||
| Generic Phase Source # | |||||
Defined in Agda.Benchmarking Associated Types
| |||||
| Show Phase Source # | |||||
| Eq Phase Source # | |||||
| Ord Phase Source # | |||||
| type Rep Phase Source # | |||||
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)))))))) | |||||
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 # | |||||
Associated Types
Methods getBenchmark :: IO (Benchmark (BenchPhase IO)) Source # putBenchmark :: Benchmark (BenchPhase IO) -> IO () Source # modifyBenchmark :: (Benchmark (BenchPhase IO) -> Benchmark (BenchPhase IO)) -> IO () Source # | |||||