Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 #
lookupTM :: Key m -> m b -> Maybe b Source #
alterTM :: Key m -> XT b -> m b -> m b Source #
Instances
Maps over Type
s
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
Functor LooseTypeMap Source # | |||||
Defined in GHC.Core.Map.Type fmap :: (a -> b) -> LooseTypeMap a -> LooseTypeMap b Source # (<$) :: a -> LooseTypeMap b -> LooseTypeMap a Source # | |||||
TrieMap LooseTypeMap Source # | |||||
Defined in GHC.Core.Map.Type
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 # | |||||
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.