HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.DiscrimTree.Types

  • 2 types
  • 2 values
  • PackageAgda-2.7.0.1
  • Exports4
  • LanguageHaskell2010
  • LicenceMIT
  • SourceTypes.hs
datadata Key
#

Constructors

  • RigidK !QName !Int

    Rigid symbols (constructors, data types, record types, postulates) identified by a QName.

  • LocalK !Int !Int

    Local variables.

  • PiK

    Dependent function types. The domain will be represented accurately, for the case of a genuine dependent function type, the codomain will be a dummy.

  • ConstK

    Constant lambdas.

  • SortK

    Universes.

  • FlexK

    Anything else.

Instances8Eq, Ord, Show, Generic, NFData, PrettyTCM, …
datadata DiscrimTree a
#

A Term-indexed associative data structure supporting approximate (conservative) lookup. Rather than using a Trie keyed by Key directly, a DiscrimTree is instead represented more like a case tree.

This allows us to exploit the fact that instance selection often focuses on a small part of the term: Only that critical chain is represented in the tree. As an example, level parameters are unlikely to contribute to narrowing a search problem, so it would be wasteful to have an indirection in the tree for every FlexK standing for a level parameter.

Constructors

  • EmptyDT

    The empty discrimination tree.

  • DoneDT (Set a)

    Succeed with a given set of values.

  • CaseDT !Int (Map Key (DiscrimTree a)) (DiscrimTree a)

    Do case analysis on a term. CaseDT is scoped in the same way as fast case trees for the abstract machine: When matching actually succeeds, the variable that was matched gets replaced by its arguments directly in the context.

Instances11Eq, Show, Generic, Semigroup, Monoid, NFData, …
valuemergeDT :: Ord a => DiscrimTree a -> DiscrimTree a -> DiscrimTree a
#

Merge a pair of discrimination trees. This function tries to build the minimal discrimination tree that yields the union of the inputs' results, though it does so slightly naïvely, without considerable optimisations (e.g. it does not turn single-alternative CaseDTs into DoneDTs).

valuesingletonDT :: [Key] -> a -> DiscrimTree a
#

Construct the case tree corresponding to only performing proper matches on the given key. In this context, a "proper match" is any Key that is not FlexK.