Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.DiscrimTree.Types

Synopsis

Documentation

data Key Source #

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.

Instances

Instances details
PrettyTCM Key Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Key -> m Doc Source #

EmbPrj Key Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Key -> S Int32 Source #

icod_ :: Key -> S Int32 Source #

value :: Int32 -> R Key Source #

NFData Key Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Methods

rnf :: Key -> ()

Generic Key Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Associated Types

type Rep Key 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

type Rep Key = D1 ('MetaData "Key" "Agda.TypeChecking.DiscrimTree.Types" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "RigidK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int)) :+: (C1 ('MetaCons "LocalK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int)) :+: C1 ('MetaCons "PiK" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "ConstK" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SortK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FlexK" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: Key -> Rep Key x

to :: Rep Key x -> Key

Show Key Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Methods

showsPrec :: Int -> Key -> ShowS

show :: Key -> String

showList :: [Key] -> ShowS

Eq Key Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Methods

(==) :: Key -> Key -> Bool

(/=) :: Key -> Key -> Bool

Ord Key Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Methods

compare :: Key -> Key -> Ordering

(<) :: Key -> Key -> Bool

(<=) :: Key -> Key -> Bool

(>) :: Key -> Key -> Bool

(>=) :: Key -> Key -> Bool

max :: Key -> Key -> Key

min :: Key -> Key -> Key

type Rep Key Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

type Rep Key = D1 ('MetaData "Key" "Agda.TypeChecking.DiscrimTree.Types" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "RigidK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int)) :+: (C1 ('MetaCons "LocalK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int)) :+: C1 ('MetaCons "PiK" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "ConstK" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SortK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FlexK" 'PrefixI 'False) (U1 :: Type -> Type))))

data DiscrimTree a Source #

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

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.

Fields

  • !Int

    The variable to case on.

  • (Map Key (DiscrimTree a))

    The proper branches.

  • (DiscrimTree a)

    A further tree, which should always be explored.

Instances

Instances details
(KillRange a, Ord a) => KillRange (DiscrimTree a) Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

PrettyTCM a => PrettyTCM (DiscrimTree a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

(EmbPrj a, Ord a) => EmbPrj (DiscrimTree a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DiscrimTree a -> S Int32 Source #

icod_ :: DiscrimTree a -> S Int32 Source #

value :: Int32 -> R (DiscrimTree a) Source #

Null (DiscrimTree a) Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Methods

empty :: DiscrimTree a Source #

null :: DiscrimTree a -> Bool Source #

NFData a => NFData (DiscrimTree a) Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Methods

rnf :: DiscrimTree a -> ()

Ord a => Monoid (DiscrimTree a) Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Ord a => Semigroup (DiscrimTree a) Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Methods

(<>) :: DiscrimTree a -> DiscrimTree a -> DiscrimTree a #

sconcat :: NonEmpty (DiscrimTree a) -> DiscrimTree a

stimes :: Integral b => b -> DiscrimTree a -> DiscrimTree a

Generic (DiscrimTree a) Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Associated Types

type Rep (DiscrimTree a) 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

type Rep (DiscrimTree a) = D1 ('MetaData "DiscrimTree" "Agda.TypeChecking.DiscrimTree.Types" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "EmptyDT" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DoneDT" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set a))) :+: C1 ('MetaCons "CaseDT" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Key (DiscrimTree a))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (DiscrimTree a))))))

Methods

from :: DiscrimTree a -> Rep (DiscrimTree a) x

to :: Rep (DiscrimTree a) x -> DiscrimTree a

Show a => Show (DiscrimTree a) Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Methods

showsPrec :: Int -> DiscrimTree a -> ShowS

show :: DiscrimTree a -> String

showList :: [DiscrimTree a] -> ShowS

Eq a => Eq (DiscrimTree a) Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

Methods

(==) :: DiscrimTree a -> DiscrimTree a -> Bool

(/=) :: DiscrimTree a -> DiscrimTree a -> Bool

type Rep (DiscrimTree a) Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree.Types

type Rep (DiscrimTree a) = D1 ('MetaData "DiscrimTree" "Agda.TypeChecking.DiscrimTree.Types" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "EmptyDT" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "DoneDT" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set a))) :+: C1 ('MetaCons "CaseDT" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Key (DiscrimTree a))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (DiscrimTree a))))))

mergeDT :: Ord a => DiscrimTree a -> DiscrimTree a -> DiscrimTree a Source #

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).

singletonDT :: [Key] -> a -> DiscrimTree a Source #

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.