Agda.Benchmarking

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