| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
GHC.Core.Map.Type
Synopsis
- class Functor m => TrieMap (m :: Type -> Type) where
- type XT a = Maybe a -> Maybe a
- data TypeMap a
- emptyTypeMap :: TypeMap a
- extendTypeMap :: TypeMap a -> Type -> a -> TypeMap a
- lookupTypeMap :: TypeMap a -> Type -> Maybe a
- foldTypeMap :: (a -> b -> b) -> b -> TypeMap a -> b
- data LooseTypeMap a
- data CmEnv
- lookupCME :: CmEnv -> Var -> Maybe BoundVar
- extendTypeMapWithScope :: TypeMap a -> CmEnv -> Type -> a -> TypeMap a
- lookupTypeMapWithScope :: TypeMap a -> CmEnv -> Type -> Maybe a
- mkDeBruijnContext :: [Var] -> CmEnv
- extendCME :: CmEnv -> Var -> CmEnv
- extendCMEs :: CmEnv -> [Var] -> CmEnv
- emptyCME :: CmEnv
- type TypeMapG = GenMap TypeMapX
- type CoercionMapG = GenMap CoercionMapX
- data DeBruijn a = D CmEnv a
- deBruijnize :: a -> DeBruijn a
- eqDeBruijnType :: DeBruijn Type -> DeBruijn Type -> Bool
- eqDeBruijnVar :: DeBruijn Var -> DeBruijn Var -> Bool
- data BndrMap a
- xtBndr :: CmEnv -> Var -> XT a -> BndrMap a -> BndrMap a
- lkBndr :: CmEnv -> Var -> BndrMap a -> Maybe a
- data VarMap a
- xtVar :: CmEnv -> Var -> XT a -> VarMap a -> VarMap a
- lkVar :: CmEnv -> Var -> VarMap a -> Maybe a
- lkDFreeVar :: Var -> DVarEnv a -> Maybe a
- xtDFreeVar :: Var -> XT a -> DVarEnv a -> DVarEnv a
- xtDNamed :: NamedThing n => n -> XT a -> DNameEnv a -> DNameEnv a
- lkDNamed :: NamedThing n => n -> DNameEnv a -> Maybe a
Re-export generic interface
class Functor m => TrieMap (m :: Type -> Type) where Source #
Methods
lookupTM :: Key m -> m b -> Maybe b Source #
alterTM :: Key m -> XT b -> m b -> m b Source #
Instances
Maps over Types
TypeMap a is a map from Type to a. If you are a client, this
is the type you want. The keys in this map may have different kinds.
emptyTypeMap :: TypeMap a Source #
foldTypeMap :: (a -> b -> b) -> b -> TypeMap a -> b Source #
data LooseTypeMap a Source #
A LooseTypeMap doesn't do a kind-check. Thus, when lookup up (t |> g),
you'll find entries inserted under (t), even if (g) is non-reflexive.
Instances
| TrieMap LooseTypeMap Source # | |||||
Defined in GHC.Core.Map.Type Associated Types
Methods emptyTM :: LooseTypeMap a Source # lookupTM :: Key LooseTypeMap -> LooseTypeMap b -> Maybe b Source # alterTM :: Key LooseTypeMap -> XT b -> LooseTypeMap b -> LooseTypeMap b Source # filterTM :: (a -> Bool) -> LooseTypeMap a -> LooseTypeMap a Source # foldTM :: (a -> b -> b) -> LooseTypeMap a -> b -> b Source # | |||||
| Functor LooseTypeMap Source # | |||||
Defined in GHC.Core.Map.Type Methods fmap :: (a -> b) -> LooseTypeMap a -> LooseTypeMap b # (<$) :: a -> LooseTypeMap b -> LooseTypeMap a # | |||||
| type Key LooseTypeMap Source # | |||||
Defined in GHC.Core.Map.Type | |||||
With explicit scoping
extendTypeMapWithScope :: TypeMap a -> CmEnv -> Type -> a -> TypeMap a Source #
Extend a TypeMap with a type in the given context.
extendTypeMapWithScope m (mkDeBruijnContext [a,b,c]) t v is equivalent to
extendTypeMap m (forall a b c. t) v, but allows reuse of the context over
multiple insertions.
mkDeBruijnContext :: [Var] -> CmEnv Source #
Construct a deBruijn environment with the given variables in scope.
e.g. mkDeBruijnEnv [a,b,c] constructs a context forall a b c.
Utilities for use by friends only
type TypeMapG = GenMap TypeMapX Source #
TypeMapG a is a map from DeBruijn Type to a. The extended
key makes it suitable for recursive traversal, since it can track binders,
but it is strictly internal to this module. If you are including a TypeMap
inside another TrieMap, this is the type you want. Note that this
lookup does not do a kind-check. Thus, all keys in this map must have
the same kind. Also note that this map respects the distinction between
Type and Constraint, despite the fact that they are equivalent type
synonyms in Core.
type CoercionMapG = GenMap CoercionMapX Source #
DeBruijn a represents a modulo alpha-renaming. This is achieved
by equipping the value with a CmEnv, which tracks an on-the-fly deBruijn
numbering. This allows us to define an Eq instance for DeBruijn a, even
if this was not (easily) possible for a. Note: we purposely don't
export the constructor. Make a helper function if you find yourself
needing it.
deBruijnize :: a -> DeBruijn a Source #
A BndrMap is a TypeMapG which allows us to distinguish between
binding forms whose binders have different types. For example,
if we are doing a TrieMap lookup on (x :: Int) -> (), we should
not pick up an entry in the TrieMap for (x :: Bool) -> ():
we can disambiguate this by matching on the type (or kind, if this
a binder in a type) of the binder.
We also need to do the same for multiplicity! Which, since multiplicities are
encoded simply as a Type, amounts to have a Trie for a pair of types. Tries
of pairs are composition.