Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data Key
- data DiscrimTree a
- = EmptyDT
- | DoneDT (Set a)
- | CaseDT !Int (Map Key (DiscrimTree a)) (DiscrimTree a)
- mergeDT :: Ord a => DiscrimTree a -> DiscrimTree a -> DiscrimTree a
- singletonDT :: [Key] -> a -> DiscrimTree a
Documentation
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
PrettyTCM Key Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
EmbPrj Key Source # | |||||
NFData Key Source # | |||||
Defined in Agda.TypeChecking.DiscrimTree.Types | |||||
Generic Key Source # | |||||
Defined in Agda.TypeChecking.DiscrimTree.Types
| |||||
Show Key Source # | |||||
Eq Key Source # | |||||
Ord Key Source # | |||||
type Rep Key Source # | |||||
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.
EmptyDT | The empty discrimination tree. |
DoneDT (Set a) | Succeed with a given set of values. |
CaseDT | Do case analysis on a term. |
|
Instances
(KillRange a, Ord a) => KillRange (DiscrimTree a) Source # | |||||
Defined in Agda.TypeChecking.DiscrimTree.Types killRange :: KillRangeT (DiscrimTree a) Source # | |||||
PrettyTCM a => PrettyTCM (DiscrimTree a) Source # | |||||
Defined in Agda.TypeChecking.Pretty prettyTCM :: MonadPretty m => DiscrimTree a -> m Doc Source # | |||||
(EmbPrj a, Ord a) => EmbPrj (DiscrimTree a) Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Internal icode :: DiscrimTree a -> S Int32 Source # icod_ :: DiscrimTree a -> S Int32 Source # value :: Int32 -> R (DiscrimTree a) Source # | |||||
Null (DiscrimTree a) Source # | |||||
Defined in Agda.TypeChecking.DiscrimTree.Types empty :: DiscrimTree a Source # null :: DiscrimTree a -> Bool Source # | |||||
NFData a => NFData (DiscrimTree a) Source # | |||||
Defined in Agda.TypeChecking.DiscrimTree.Types rnf :: DiscrimTree a -> () | |||||
Ord a => Monoid (DiscrimTree a) Source # | |||||
Defined in Agda.TypeChecking.DiscrimTree.Types mempty :: DiscrimTree a mappend :: DiscrimTree a -> DiscrimTree a -> DiscrimTree a mconcat :: [DiscrimTree a] -> DiscrimTree a | |||||
Ord a => Semigroup (DiscrimTree a) Source # | |||||
Defined in Agda.TypeChecking.DiscrimTree.Types (<>) :: DiscrimTree a -> DiscrimTree a -> DiscrimTree a # sconcat :: NonEmpty (DiscrimTree a) -> DiscrimTree a stimes :: Integral b => b -> DiscrimTree a -> DiscrimTree a | |||||
Generic (DiscrimTree a) Source # | |||||
Defined in Agda.TypeChecking.DiscrimTree.Types
from :: DiscrimTree a -> Rep (DiscrimTree a) x to :: Rep (DiscrimTree a) x -> DiscrimTree a | |||||
Show a => Show (DiscrimTree a) Source # | |||||
Defined in Agda.TypeChecking.DiscrimTree.Types showsPrec :: Int -> DiscrimTree a -> ShowS show :: DiscrimTree a -> String showList :: [DiscrimTree a] -> ShowS | |||||
Eq a => Eq (DiscrimTree a) Source # | |||||
Defined in Agda.TypeChecking.DiscrimTree.Types (==) :: DiscrimTree a -> DiscrimTree a -> Bool (/=) :: DiscrimTree a -> DiscrimTree a -> Bool | |||||
type Rep (DiscrimTree a) Source # | |||||
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 #
singletonDT :: [Key] -> a -> DiscrimTree a Source #