{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
module GHC.Core.Map.Type (
TrieMap(..), XT,
TypeMap, emptyTypeMap, extendTypeMap, lookupTypeMap, foldTypeMap,
LooseTypeMap,
CmEnv, lookupCME, extendTypeMapWithScope, lookupTypeMapWithScope,
mkDeBruijnContext, extendCME, extendCMEs, emptyCME,
TypeMapG, CoercionMapG,
DeBruijn(..), deBruijnize, eqDeBruijnType, eqDeBruijnVar,
BndrMap, xtBndr, lkBndr,
VarMap, xtVar, lkVar, lkDFreeVar, xtDFreeVar,
xtDNamed, lkDNamed
) where
import GHC.Prelude
import GHC.Core.Type
import GHC.Core.Coercion
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Compare( eqForAllVis )
import GHC.Data.TrieMap
import GHC.Data.FastString
import GHC.Types.Name
import GHC.Types.Name.Env
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Unique.FM
import GHC.Utils.Outputable
import GHC.Utils.Panic
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import Control.Monad ( (>=>) )
{-# SPECIALIZE lkG :: Key TypeMapX -> TypeMapG a -> Maybe a #-}
{-# SPECIALIZE lkG :: Key CoercionMapX -> CoercionMapG a -> Maybe a #-}
{-# SPECIALIZE xtG :: Key TypeMapX -> XT a -> TypeMapG a -> TypeMapG a #-}
{-# SPECIALIZE xtG :: Key CoercionMapX -> XT a -> CoercionMapG a -> CoercionMapG a #-}
{-# SPECIALIZE mapG :: (a -> b) -> TypeMapG a -> TypeMapG b #-}
{-# SPECIALIZE mapG :: (a -> b) -> CoercionMapG a -> CoercionMapG b #-}
{-# SPECIALIZE fdG :: (a -> b -> b) -> TypeMapG a -> b -> b #-}
{-# SPECIALIZE fdG :: (a -> b -> b) -> CoercionMapG a -> b -> b #-}
newtype CoercionMap a = CoercionMap (CoercionMapG a)
instance Functor CoercionMap where
fmap :: forall a b. (a -> b) -> CoercionMap a -> CoercionMap b
fmap a -> b
f = \ (CoercionMap CoercionMapG a
m) -> CoercionMapG b -> CoercionMap b
forall a. CoercionMapG a -> CoercionMap a
CoercionMap ((a -> b) -> CoercionMapG a -> CoercionMapG b
forall a b.
(a -> b) -> GenMap CoercionMapX a -> GenMap CoercionMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f CoercionMapG a
m)
{-# INLINE fmap #-}
instance TrieMap CoercionMap where
type Key CoercionMap = Coercion
emptyTM :: forall a. CoercionMap a
emptyTM = CoercionMapG a -> CoercionMap a
forall a. CoercionMapG a -> CoercionMap a
CoercionMap CoercionMapG a
forall a. GenMap CoercionMapX a
forall (m :: * -> *) a. TrieMap m => m a
emptyTM
lookupTM :: forall b. Key CoercionMap -> CoercionMap b -> Maybe b
lookupTM Key CoercionMap
k (CoercionMap CoercionMapG b
m) = Key (GenMap CoercionMapX) -> CoercionMapG b -> Maybe b
forall b.
Key (GenMap CoercionMapX) -> GenMap CoercionMapX b -> Maybe b
forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM (Coercion -> DeBruijn Coercion
forall a. a -> DeBruijn a
deBruijnize Coercion
Key CoercionMap
k) CoercionMapG b
m
alterTM :: forall b. Key CoercionMap -> XT b -> CoercionMap b -> CoercionMap b
alterTM Key CoercionMap
k XT b
f (CoercionMap CoercionMapG b
m) = CoercionMapG b -> CoercionMap b
forall a. CoercionMapG a -> CoercionMap a
CoercionMap (Key (GenMap CoercionMapX)
-> XT b -> CoercionMapG b -> CoercionMapG b
forall b.
Key (GenMap CoercionMapX)
-> XT b -> GenMap CoercionMapX b -> GenMap CoercionMapX b
forall (m :: * -> *) b. TrieMap m => Key m -> XT b -> m b -> m b
alterTM (Coercion -> DeBruijn Coercion
forall a. a -> DeBruijn a
deBruijnize Coercion
Key CoercionMap
k) XT b
f CoercionMapG b
m)
foldTM :: forall a b. (a -> b -> b) -> CoercionMap a -> b -> b
foldTM a -> b -> b
k (CoercionMap CoercionMapG a
m) = (a -> b -> b) -> CoercionMapG a -> b -> b
forall a b. (a -> b -> b) -> GenMap CoercionMapX a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k CoercionMapG a
m
filterTM :: forall a. (a -> Bool) -> CoercionMap a -> CoercionMap a
filterTM a -> Bool
f (CoercionMap CoercionMapG a
m) = CoercionMapG a -> CoercionMap a
forall a. CoercionMapG a -> CoercionMap a
CoercionMap ((a -> Bool) -> CoercionMapG a -> CoercionMapG a
forall a.
(a -> Bool) -> GenMap CoercionMapX a -> GenMap CoercionMapX a
forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f CoercionMapG a
m)
type CoercionMapG = GenMap CoercionMapX
newtype CoercionMapX a = CoercionMapX (TypeMapX a)
instance Functor CoercionMapX where
fmap :: forall a b. (a -> b) -> CoercionMapX a -> CoercionMapX b
fmap a -> b
f = \ (CoercionMapX TypeMapX a
core_tm) -> TypeMapX b -> CoercionMapX b
forall a. TypeMapX a -> CoercionMapX a
CoercionMapX ((a -> b) -> TypeMapX a -> TypeMapX b
forall a b. (a -> b) -> TypeMapX a -> TypeMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f TypeMapX a
core_tm)
{-# INLINE fmap #-}
instance TrieMap CoercionMapX where
type Key CoercionMapX = DeBruijn Coercion
emptyTM :: forall a. CoercionMapX a
emptyTM = TypeMapX a -> CoercionMapX a
forall a. TypeMapX a -> CoercionMapX a
CoercionMapX TypeMapX a
forall a. TypeMapX a
forall (m :: * -> *) a. TrieMap m => m a
emptyTM
lookupTM :: forall b. Key CoercionMapX -> CoercionMapX b -> Maybe b
lookupTM = Key CoercionMapX -> CoercionMapX b -> Maybe b
DeBruijn Coercion -> CoercionMapX b -> Maybe b
forall a. DeBruijn Coercion -> CoercionMapX a -> Maybe a
lkC
alterTM :: forall b.
Key CoercionMapX -> XT b -> CoercionMapX b -> CoercionMapX b
alterTM = Key CoercionMapX
-> (Maybe b -> Maybe b) -> CoercionMapX b -> CoercionMapX b
DeBruijn Coercion
-> (Maybe b -> Maybe b) -> CoercionMapX b -> CoercionMapX b
forall a.
DeBruijn Coercion -> XT a -> CoercionMapX a -> CoercionMapX a
xtC
foldTM :: forall a b. (a -> b -> b) -> CoercionMapX a -> b -> b
foldTM a -> b -> b
f (CoercionMapX TypeMapX a
core_tm) = (a -> b -> b) -> TypeMapX a -> b -> b
forall a b. (a -> b -> b) -> TypeMapX a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
f TypeMapX a
core_tm
filterTM :: forall a. (a -> Bool) -> CoercionMapX a -> CoercionMapX a
filterTM a -> Bool
f (CoercionMapX TypeMapX a
core_tm) = TypeMapX a -> CoercionMapX a
forall a. TypeMapX a -> CoercionMapX a
CoercionMapX ((a -> Bool) -> TypeMapX a -> TypeMapX a
forall a. (a -> Bool) -> TypeMapX a -> TypeMapX a
forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f TypeMapX a
core_tm)
instance Eq (DeBruijn Coercion) where
D CmEnv
env1 Coercion
co1 == :: DeBruijn Coercion -> DeBruijn Coercion -> Bool
== D CmEnv
env2 Coercion
co2
= CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env1 (Coercion -> Type
coercionType Coercion
co1) DeBruijn Type -> DeBruijn Type -> Bool
forall a. Eq a => a -> a -> Bool
==
CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env2 (Coercion -> Type
coercionType Coercion
co2)
lkC :: DeBruijn Coercion -> CoercionMapX a -> Maybe a
lkC :: forall a. DeBruijn Coercion -> CoercionMapX a -> Maybe a
lkC (D CmEnv
env Coercion
co) (CoercionMapX TypeMapX a
core_tm) = DeBruijn Type -> TypeMapX a -> Maybe a
forall a. DeBruijn Type -> TypeMapX a -> Maybe a
lkT (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env (Type -> DeBruijn Type) -> Type -> DeBruijn Type
forall a b. (a -> b) -> a -> b
$ Coercion -> Type
coercionType Coercion
co)
TypeMapX a
core_tm
xtC :: DeBruijn Coercion -> XT a -> CoercionMapX a -> CoercionMapX a
xtC :: forall a.
DeBruijn Coercion -> XT a -> CoercionMapX a -> CoercionMapX a
xtC (D CmEnv
env Coercion
co) XT a
f (CoercionMapX TypeMapX a
m)
= TypeMapX a -> CoercionMapX a
forall a. TypeMapX a -> CoercionMapX a
CoercionMapX (DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
forall a. DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
xtT (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env (Type -> DeBruijn Type) -> Type -> DeBruijn Type
forall a b. (a -> b) -> a -> b
$ Coercion -> Type
coercionType Coercion
co) XT a
f TypeMapX a
m)
type TypeMapG = GenMap TypeMapX
data TypeMapX a
= TM { forall a. TypeMapX a -> VarMap a
tm_var :: VarMap a
, forall a. TypeMapX a -> TypeMapG (TypeMapG a)
tm_app :: TypeMapG (TypeMapG a)
, forall a. TypeMapX a -> DNameEnv a
tm_tycon :: DNameEnv a
, forall a. TypeMapX a -> TypeMapG (BndrMap a)
tm_forall :: TypeMapG (BndrMap a)
, forall a. TypeMapX a -> TyLitMap a
tm_tylit :: TyLitMap a
, forall a. TypeMapX a -> Maybe a
tm_coerce :: Maybe a
}
trieMapView :: Type -> Maybe Type
trieMapView :: Type -> Maybe Type
trieMapView Type
ty
| Just (TyCon
tc, tys :: [Type]
tys@(Type
_:[Type]
_)) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
= Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type) -> Type -> [Type] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
AppTy (TyCon -> Type
mkTyConTy TyCon
tc) [Type]
tys
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
= Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty'
trieMapView Type
_ = Maybe Type
forall a. Maybe a
Nothing
instance Functor TypeMapX where
fmap :: forall a b. (a -> b) -> TypeMapX a -> TypeMapX b
fmap a -> b
f TM
{ tm_var :: forall a. TypeMapX a -> VarMap a
tm_var = VarMap a
tvar, tm_app :: forall a. TypeMapX a -> TypeMapG (TypeMapG a)
tm_app = TypeMapG (TypeMapG a)
tapp, tm_tycon :: forall a. TypeMapX a -> DNameEnv a
tm_tycon = DNameEnv a
ttycon, tm_forall :: forall a. TypeMapX a -> TypeMapG (BndrMap a)
tm_forall = TypeMapG (BndrMap a)
tforall
, tm_tylit :: forall a. TypeMapX a -> TyLitMap a
tm_tylit = TyLitMap a
tlit, tm_coerce :: forall a. TypeMapX a -> Maybe a
tm_coerce = Maybe a
tcoerce } = TM
{ tm_var :: VarMap b
tm_var = (a -> b) -> VarMap a -> VarMap b
forall a b. (a -> b) -> VarMap a -> VarMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f VarMap a
tvar, tm_app :: TypeMapG (TypeMapG b)
tm_app = (TypeMapG a -> TypeMapG b)
-> TypeMapG (TypeMapG a) -> TypeMapG (TypeMapG b)
forall a b. (a -> b) -> GenMap TypeMapX a -> GenMap TypeMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> TypeMapG a -> TypeMapG b
forall a b. (a -> b) -> GenMap TypeMapX a -> GenMap TypeMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) TypeMapG (TypeMapG a)
tapp, tm_tycon :: DNameEnv b
tm_tycon = (a -> b) -> DNameEnv a -> DNameEnv b
forall a b. (a -> b) -> UniqDFM Name a -> UniqDFM Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f DNameEnv a
ttycon
, tm_forall :: TypeMapG (BndrMap b)
tm_forall = (BndrMap a -> BndrMap b)
-> TypeMapG (BndrMap a) -> TypeMapG (BndrMap b)
forall a b. (a -> b) -> GenMap TypeMapX a -> GenMap TypeMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> BndrMap a -> BndrMap b
forall a b. (a -> b) -> BndrMap a -> BndrMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) TypeMapG (BndrMap a)
tforall
, tm_tylit :: TyLitMap b
tm_tylit = (a -> b) -> TyLitMap a -> TyLitMap b
forall a b. (a -> b) -> TyLitMap a -> TyLitMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f TyLitMap a
tlit, tm_coerce :: Maybe b
tm_coerce = (a -> b) -> Maybe a -> Maybe b
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Maybe a
tcoerce }
instance TrieMap TypeMapX where
type Key TypeMapX = DeBruijn Type
emptyTM :: forall a. TypeMapX a
emptyTM = TypeMapX a
forall a. TypeMapX a
emptyT
lookupTM :: forall b. Key TypeMapX -> TypeMapX b -> Maybe b
lookupTM = Key TypeMapX -> TypeMapX b -> Maybe b
DeBruijn Type -> TypeMapX b -> Maybe b
forall a. DeBruijn Type -> TypeMapX a -> Maybe a
lkT
alterTM :: forall b. Key TypeMapX -> XT b -> TypeMapX b -> TypeMapX b
alterTM = Key TypeMapX -> (Maybe b -> Maybe b) -> TypeMapX b -> TypeMapX b
DeBruijn Type -> (Maybe b -> Maybe b) -> TypeMapX b -> TypeMapX b
forall a. DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
xtT
foldTM :: forall a b. (a -> b -> b) -> TypeMapX a -> b -> b
foldTM = (a -> b -> b) -> TypeMapX a -> b -> b
forall a b. (a -> b -> b) -> TypeMapX a -> b -> b
fdT
filterTM :: forall a. (a -> Bool) -> TypeMapX a -> TypeMapX a
filterTM = (a -> Bool) -> TypeMapX a -> TypeMapX a
forall a. (a -> Bool) -> TypeMapX a -> TypeMapX a
filterT
instance Eq (DeBruijn Type) where
== :: DeBruijn Type -> DeBruijn Type -> Bool
(==) = DeBruijn Type -> DeBruijn Type -> Bool
eqDeBruijnType
data TypeEquality = TNEQ
| TEQ
| TEQX
eqDeBruijnType :: DeBruijn Type -> DeBruijn Type -> Bool
eqDeBruijnType :: DeBruijn Type -> DeBruijn Type -> Bool
eqDeBruijnType env_t1 :: DeBruijn Type
env_t1@(D CmEnv
env1 Type
t1) env_t2 :: DeBruijn Type
env_t2@(D CmEnv
env2 Type
t2) =
case DeBruijn Type -> DeBruijn Type -> TypeEquality
go DeBruijn Type
env_t1 DeBruijn Type
env_t2 of
TypeEquality
TEQX -> TypeEquality -> Bool
toBool (DeBruijn Type -> DeBruijn Type -> TypeEquality
go (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env1 Type
k1) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env2 Type
k2))
TypeEquality
ty_eq -> TypeEquality -> Bool
toBool TypeEquality
ty_eq
where
k1 :: Type
k1 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
t1
k2 :: Type
k2 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
t2
toBool :: TypeEquality -> Bool
toBool :: TypeEquality -> Bool
toBool TypeEquality
TNEQ = Bool
False
toBool TypeEquality
_ = Bool
True
liftEquality :: Bool -> TypeEquality
liftEquality :: Bool -> TypeEquality
liftEquality Bool
False = TypeEquality
TNEQ
liftEquality Bool
_ = TypeEquality
TEQ
hasCast :: TypeEquality -> TypeEquality
hasCast :: TypeEquality -> TypeEquality
hasCast TypeEquality
TEQ = TypeEquality
TEQX
hasCast TypeEquality
eq = TypeEquality
eq
andEq :: TypeEquality -> TypeEquality -> TypeEquality
andEq :: TypeEquality -> TypeEquality -> TypeEquality
andEq TypeEquality
TNEQ TypeEquality
_ = TypeEquality
TNEQ
andEq TypeEquality
TEQX TypeEquality
e = TypeEquality -> TypeEquality
hasCast TypeEquality
e
andEq TypeEquality
TEQ TypeEquality
e = TypeEquality
e
go :: DeBruijn Type -> DeBruijn Type -> TypeEquality
go (D CmEnv
_ (TyConApp TyCon
tc1 [])) (D CmEnv
_ (TyConApp TyCon
tc2 []))
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= TypeEquality
TEQ
go env_t :: DeBruijn Type
env_t@(D CmEnv
env Type
t) env_t' :: DeBruijn Type
env_t'@(D CmEnv
env' Type
t')
| Just Type
new_t <- Type -> Maybe Type
coreView Type
t = DeBruijn Type -> DeBruijn Type -> TypeEquality
go (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
new_t) DeBruijn Type
env_t'
| Just Type
new_t' <- Type -> Maybe Type
coreView Type
t' = DeBruijn Type -> DeBruijn Type -> TypeEquality
go DeBruijn Type
env_t (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' Type
new_t')
| Bool
otherwise
= case (Type
t, Type
t') of
(CastTy Type
t1 Coercion
_, Type
_) -> TypeEquality -> TypeEquality
hasCast (DeBruijn Type -> DeBruijn Type -> TypeEquality
go (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t'))
(Type
_, CastTy Type
t1' Coercion
_) -> TypeEquality -> TypeEquality
hasCast (DeBruijn Type -> DeBruijn Type -> TypeEquality
go (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1'))
(TyVarTy Var
v, TyVarTy Var
v')
-> Bool -> TypeEquality
liftEquality (Bool -> TypeEquality) -> Bool -> TypeEquality
forall a b. (a -> b) -> a -> b
$ DeBruijn Var -> DeBruijn Var -> Bool
eqDeBruijnVar (CmEnv -> Var -> DeBruijn Var
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Var
v) (CmEnv -> Var -> DeBruijn Var
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' Var
v')
(AppTy Type
t1 Type
t2, Type
s) | Just (Type
t1', Type
t2') <- (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
s
-> DeBruijn Type -> DeBruijn Type -> TypeEquality
go (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' Type
t1') TypeEquality -> TypeEquality -> TypeEquality
`andEq` DeBruijn Type -> DeBruijn Type -> TypeEquality
go (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t2) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' Type
t2')
(Type
s, AppTy Type
t1' Type
t2') | Just (Type
t1, Type
t2) <- (() :: Constraint) => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
s
-> DeBruijn Type -> DeBruijn Type -> TypeEquality
go (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' Type
t1') TypeEquality -> TypeEquality -> TypeEquality
`andEq` DeBruijn Type -> DeBruijn Type -> TypeEquality
go (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t2) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' Type
t2')
(FunTy FunTyFlag
v1 Type
w1 Type
t1 Type
t2, FunTy FunTyFlag
v1' Type
w1' Type
t1' Type
t2')
-> Bool -> TypeEquality
liftEquality (FunTyFlag
v1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== FunTyFlag
v1') TypeEquality -> TypeEquality -> TypeEquality
`andEq`
Bool -> TypeEquality
liftEquality (DeBruijn Type -> DeBruijn Type -> Bool
eqDeBruijnType (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' Type
t1')) TypeEquality -> TypeEquality -> TypeEquality
`andEq`
Bool -> TypeEquality
liftEquality (DeBruijn Type -> DeBruijn Type -> Bool
eqDeBruijnType (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t2) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' Type
t2')) TypeEquality -> TypeEquality -> TypeEquality
`andEq`
DeBruijn Type -> DeBruijn Type -> TypeEquality
go (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
w1) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
w1')
(TyConApp TyCon
tc [Type]
tys, TyConApp TyCon
tc' [Type]
tys')
-> Bool -> TypeEquality
liftEquality (TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc') TypeEquality -> TypeEquality -> TypeEquality
`andEq` CmEnv -> CmEnv -> [Type] -> [Type] -> TypeEquality
gos CmEnv
env CmEnv
env' [Type]
tys [Type]
tys'
(LitTy TyLit
l, LitTy TyLit
l')
-> Bool -> TypeEquality
liftEquality (TyLit
l TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
l')
(ForAllTy (Bndr Var
tv ForAllTyFlag
vis) Type
ty, ForAllTy (Bndr Var
tv' ForAllTyFlag
vis') Type
ty')
->
Bool -> TypeEquality
liftEquality (ForAllTyFlag
vis ForAllTyFlag -> ForAllTyFlag -> Bool
`eqForAllVis` ForAllTyFlag
vis') TypeEquality -> TypeEquality -> TypeEquality
`andEq`
DeBruijn Type -> DeBruijn Type -> TypeEquality
go (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env (Var -> Type
varType Var
tv)) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' (Var -> Type
varType Var
tv')) TypeEquality -> TypeEquality -> TypeEquality
`andEq`
DeBruijn Type -> DeBruijn Type -> TypeEquality
go (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D (CmEnv -> Var -> CmEnv
extendCME CmEnv
env Var
tv) Type
ty) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D (CmEnv -> Var -> CmEnv
extendCME CmEnv
env' Var
tv') Type
ty')
(CoercionTy {}, CoercionTy {})
-> TypeEquality
TEQ
(Type, Type)
_ -> TypeEquality
TNEQ
gos :: CmEnv -> CmEnv -> [Type] -> [Type] -> TypeEquality
gos !CmEnv
_ !CmEnv
_ [] [] = TypeEquality
TEQ
gos CmEnv
e1 CmEnv
e2 (Type
ty1:[Type]
tys1) (Type
ty2:[Type]
tys2) = DeBruijn Type -> DeBruijn Type -> TypeEquality
go (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
e1 Type
ty1) (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
e2 Type
ty2) TypeEquality -> TypeEquality -> TypeEquality
`andEq`
CmEnv -> CmEnv -> [Type] -> [Type] -> TypeEquality
gos CmEnv
e1 CmEnv
e2 [Type]
tys1 [Type]
tys2
gos CmEnv
_ CmEnv
_ [Type]
_ [Type]
_ = TypeEquality
TNEQ
instance Eq (DeBruijn Var) where
== :: DeBruijn Var -> DeBruijn Var -> Bool
(==) = DeBruijn Var -> DeBruijn Var -> Bool
eqDeBruijnVar
eqDeBruijnVar :: DeBruijn Var -> DeBruijn Var -> Bool
eqDeBruijnVar :: DeBruijn Var -> DeBruijn Var -> Bool
eqDeBruijnVar (D CmEnv
env1 Var
v1) (D CmEnv
env2 Var
v2) =
case (CmEnv -> Var -> Maybe BoundVar
lookupCME CmEnv
env1 Var
v1, CmEnv -> Var -> Maybe BoundVar
lookupCME CmEnv
env2 Var
v2) of
(Just BoundVar
b1, Just BoundVar
b2) -> BoundVar
b1 BoundVar -> BoundVar -> Bool
forall a. Eq a => a -> a -> Bool
== BoundVar
b2
(Maybe BoundVar
Nothing, Maybe BoundVar
Nothing) -> Var
v1 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v2
(Maybe BoundVar, Maybe BoundVar)
_ -> Bool
False
instance {-# OVERLAPPING #-}
Outputable a => Outputable (TypeMapG a) where
ppr :: TypeMapG a -> SDoc
ppr TypeMapG a
m = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"TypeMap elts" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [a] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((a -> [a] -> [a]) -> TypeMapG a -> [a] -> [a]
forall a b. (a -> b -> b) -> GenMap TypeMapX a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM (:) TypeMapG a
m [])
emptyT :: TypeMapX a
emptyT :: forall a. TypeMapX a
emptyT = TM { tm_var :: VarMap a
tm_var = VarMap a
forall a. VarMap a
forall (m :: * -> *) a. TrieMap m => m a
emptyTM
, tm_app :: TypeMapG (TypeMapG a)
tm_app = TypeMapG (TypeMapG a)
forall a. GenMap TypeMapX a
forall (m :: * -> *) a. TrieMap m => m a
emptyTM
, tm_tycon :: DNameEnv a
tm_tycon = DNameEnv a
forall a. DNameEnv a
emptyDNameEnv
, tm_forall :: TypeMapG (BndrMap a)
tm_forall = TypeMapG (BndrMap a)
forall a. GenMap TypeMapX a
forall (m :: * -> *) a. TrieMap m => m a
emptyTM
, tm_tylit :: TyLitMap a
tm_tylit = TyLitMap a
forall a. TyLitMap a
emptyTyLitMap
, tm_coerce :: Maybe a
tm_coerce = Maybe a
forall a. Maybe a
Nothing }
lkT :: DeBruijn Type -> TypeMapX a -> Maybe a
lkT :: forall a. DeBruijn Type -> TypeMapX a -> Maybe a
lkT (D CmEnv
env Type
ty) TypeMapX a
m = Type -> TypeMapX a -> Maybe a
go Type
ty TypeMapX a
m
where
go :: Type -> TypeMapX a -> Maybe a
go Type
ty | Just Type
ty' <- Type -> Maybe Type
trieMapView Type
ty = Type -> TypeMapX a -> Maybe a
go Type
ty'
go (TyVarTy Var
v) = TypeMapX a -> VarMap a
forall a. TypeMapX a -> VarMap a
tm_var (TypeMapX a -> VarMap a)
-> (VarMap a -> Maybe a) -> TypeMapX a -> Maybe a
forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> CmEnv -> Var -> VarMap a -> Maybe a
forall a. CmEnv -> Var -> VarMap a -> Maybe a
lkVar CmEnv
env Var
v
go (AppTy Type
t1 Type
t2) = TypeMapX a -> TypeMapG (TypeMapG a)
forall a. TypeMapX a -> TypeMapG (TypeMapG a)
tm_app (TypeMapX a -> TypeMapG (TypeMapG a))
-> (TypeMapG (TypeMapG a) -> Maybe a) -> TypeMapX a -> Maybe a
forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> Key TypeMapX -> TypeMapG (TypeMapG a) -> Maybe (TypeMapG a)
forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> GenMap m a -> Maybe a
lkG (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1)
(TypeMapG (TypeMapG a) -> Maybe (TypeMapG a))
-> (TypeMapG a -> Maybe a) -> TypeMapG (TypeMapG a) -> Maybe a
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Key TypeMapX -> TypeMapG a -> Maybe a
forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> GenMap m a -> Maybe a
lkG (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t2)
go (TyConApp TyCon
tc []) = TypeMapX a -> DNameEnv a
forall a. TypeMapX a -> DNameEnv a
tm_tycon (TypeMapX a -> DNameEnv a)
-> (DNameEnv a -> Maybe a) -> TypeMapX a -> Maybe a
forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> TyCon -> DNameEnv a -> Maybe a
forall n a. NamedThing n => n -> DNameEnv a -> Maybe a
lkDNamed TyCon
tc
go (LitTy TyLit
l) = TypeMapX a -> TyLitMap a
forall a. TypeMapX a -> TyLitMap a
tm_tylit (TypeMapX a -> TyLitMap a)
-> (TyLitMap a -> Maybe a) -> TypeMapX a -> Maybe a
forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> TyLit -> TyLitMap a -> Maybe a
forall a. TyLit -> TyLitMap a -> Maybe a
lkTyLit TyLit
l
go (ForAllTy (Bndr Var
tv ForAllTyFlag
_) Type
ty) = TypeMapX a -> TypeMapG (BndrMap a)
forall a. TypeMapX a -> TypeMapG (BndrMap a)
tm_forall (TypeMapX a -> TypeMapG (BndrMap a))
-> (TypeMapG (BndrMap a) -> Maybe a) -> TypeMapX a -> Maybe a
forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> Key TypeMapX -> TypeMapG (BndrMap a) -> Maybe (BndrMap a)
forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> GenMap m a -> Maybe a
lkG (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D (CmEnv -> Var -> CmEnv
extendCME CmEnv
env Var
tv) Type
ty)
(TypeMapG (BndrMap a) -> Maybe (BndrMap a))
-> (BndrMap a -> Maybe a) -> TypeMapG (BndrMap a) -> Maybe a
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> CmEnv -> Var -> BndrMap a -> Maybe a
forall a. CmEnv -> Var -> BndrMap a -> Maybe a
lkBndr CmEnv
env Var
tv
go (CastTy Type
t Coercion
_) = Type -> TypeMapX a -> Maybe a
go Type
t
go (CoercionTy {}) = TypeMapX a -> Maybe a
forall a. TypeMapX a -> Maybe a
tm_coerce
go ty :: Type
ty@(TyConApp TyCon
_ (Type
_:[Type]
_)) = String -> SDoc -> TypeMapX a -> Maybe a
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"lkT TyConApp" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
go ty :: Type
ty@(FunTy {}) = String -> SDoc -> TypeMapX a -> Maybe a
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"lkT FunTy" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
xtT :: DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
xtT :: forall a. DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
xtT (D CmEnv
env Type
ty) XT a
f TypeMapX a
m | Just Type
ty' <- Type -> Maybe Type
trieMapView Type
ty = DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
forall a. DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
xtT (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
ty') XT a
f TypeMapX a
m
xtT (D CmEnv
env (TyVarTy Var
v)) XT a
f TypeMapX a
m = TypeMapX a
m { tm_var = tm_var m |> xtVar env v f }
xtT (D CmEnv
env (AppTy Type
t1 Type
t2)) XT a
f TypeMapX a
m = TypeMapX a
m { tm_app = tm_app m |> xtG (D env t1)
|>> xtG (D env t2) f }
xtT (D CmEnv
_ (TyConApp TyCon
tc [])) XT a
f TypeMapX a
m = TypeMapX a
m { tm_tycon = tm_tycon m |> xtDNamed tc f }
xtT (D CmEnv
_ (LitTy TyLit
l)) XT a
f TypeMapX a
m = TypeMapX a
m { tm_tylit = tm_tylit m |> xtTyLit l f }
xtT (D CmEnv
env (CastTy Type
t Coercion
_)) XT a
f TypeMapX a
m = DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
forall a. DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
xtT (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t) XT a
f TypeMapX a
m
xtT (D CmEnv
_ (CoercionTy {})) XT a
f TypeMapX a
m = TypeMapX a
m { tm_coerce = tm_coerce m |> f }
xtT (D CmEnv
env (ForAllTy (Bndr Var
tv ForAllTyFlag
_) Type
ty)) XT a
f TypeMapX a
m
= TypeMapX a
m { tm_forall = tm_forall m |> xtG (D (extendCME env tv) ty)
|>> xtBndr env tv f }
xtT (D CmEnv
_ ty :: Type
ty@(TyConApp TyCon
_ (Type
_:[Type]
_))) XT a
_ TypeMapX a
_ = String -> SDoc -> TypeMapX a
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"xtT TyConApp" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
xtT (D CmEnv
_ ty :: Type
ty@(FunTy {})) XT a
_ TypeMapX a
_ = String -> SDoc -> TypeMapX a
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"xtT FunTy" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
fdT :: (a -> b -> b) -> TypeMapX a -> b -> b
fdT :: forall a b. (a -> b -> b) -> TypeMapX a -> b -> b
fdT a -> b -> b
k TypeMapX a
m = (a -> b -> b) -> VarMap a -> b -> b
forall a b. (a -> b -> b) -> VarMap a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k (TypeMapX a -> VarMap a
forall a. TypeMapX a -> VarMap a
tm_var TypeMapX a
m)
(b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenMap TypeMapX a -> b -> b)
-> GenMap TypeMapX (GenMap TypeMapX a) -> b -> b
forall a b. (a -> b -> b) -> GenMap TypeMapX a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM ((a -> b -> b) -> GenMap TypeMapX a -> b -> b
forall a b. (a -> b -> b) -> GenMap TypeMapX a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k) (TypeMapX a -> GenMap TypeMapX (GenMap TypeMapX a)
forall a. TypeMapX a -> TypeMapG (TypeMapG a)
tm_app TypeMapX a
m)
(b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b -> b) -> UniqDFM Name a -> b -> b
forall a b. (a -> b -> b) -> UniqDFM Name a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k (TypeMapX a -> UniqDFM Name a
forall a. TypeMapX a -> DNameEnv a
tm_tycon TypeMapX a
m)
(b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BndrMap a -> b -> b) -> GenMap TypeMapX (BndrMap a) -> b -> b
forall a b. (a -> b -> b) -> GenMap TypeMapX a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM ((a -> b -> b) -> BndrMap a -> b -> b
forall a b. (a -> b -> b) -> BndrMap a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k) (TypeMapX a -> GenMap TypeMapX (BndrMap a)
forall a. TypeMapX a -> TypeMapG (BndrMap a)
tm_forall TypeMapX a
m)
(b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b -> b) -> TyLitMap a -> b -> b
forall a b. (a -> b -> b) -> TyLitMap a -> b -> b
foldTyLit a -> b -> b
k (TypeMapX a -> TyLitMap a
forall a. TypeMapX a -> TyLitMap a
tm_tylit TypeMapX a
m)
(b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b -> b) -> Maybe a -> b -> b
forall a b. (a -> b -> b) -> Maybe a -> b -> b
foldMaybe a -> b -> b
k (TypeMapX a -> Maybe a
forall a. TypeMapX a -> Maybe a
tm_coerce TypeMapX a
m)
filterT :: (a -> Bool) -> TypeMapX a -> TypeMapX a
filterT :: forall a. (a -> Bool) -> TypeMapX a -> TypeMapX a
filterT a -> Bool
f (TM { tm_var :: forall a. TypeMapX a -> VarMap a
tm_var = VarMap a
tvar, tm_app :: forall a. TypeMapX a -> TypeMapG (TypeMapG a)
tm_app = TypeMapG (TypeMapG a)
tapp, tm_tycon :: forall a. TypeMapX a -> DNameEnv a
tm_tycon = DNameEnv a
ttycon
, tm_forall :: forall a. TypeMapX a -> TypeMapG (BndrMap a)
tm_forall = TypeMapG (BndrMap a)
tforall, tm_tylit :: forall a. TypeMapX a -> TyLitMap a
tm_tylit = TyLitMap a
tlit
, tm_coerce :: forall a. TypeMapX a -> Maybe a
tm_coerce = Maybe a
tcoerce })
= TM { tm_var :: VarMap a
tm_var = (a -> Bool) -> VarMap a -> VarMap a
forall a. (a -> Bool) -> VarMap a -> VarMap a
forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f VarMap a
tvar
, tm_app :: TypeMapG (TypeMapG a)
tm_app = (TypeMapG a -> TypeMapG a)
-> TypeMapG (TypeMapG a) -> TypeMapG (TypeMapG a)
forall a b. (a -> b) -> GenMap TypeMapX a -> GenMap TypeMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Bool) -> TypeMapG a -> TypeMapG a
forall a. (a -> Bool) -> GenMap TypeMapX a -> GenMap TypeMapX a
forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f) TypeMapG (TypeMapG a)
tapp
, tm_tycon :: DNameEnv a
tm_tycon = (a -> Bool) -> DNameEnv a -> DNameEnv a
forall a. (a -> Bool) -> UniqDFM Name a -> UniqDFM Name a
forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f DNameEnv a
ttycon
, tm_forall :: TypeMapG (BndrMap a)
tm_forall = (BndrMap a -> BndrMap a)
-> TypeMapG (BndrMap a) -> TypeMapG (BndrMap a)
forall a b. (a -> b) -> GenMap TypeMapX a -> GenMap TypeMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Bool) -> BndrMap a -> BndrMap a
forall a. (a -> Bool) -> BndrMap a -> BndrMap a
forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f) TypeMapG (BndrMap a)
tforall
, tm_tylit :: TyLitMap a
tm_tylit = (a -> Bool) -> TyLitMap a -> TyLitMap a
forall a. (a -> Bool) -> TyLitMap a -> TyLitMap a
forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f TyLitMap a
tlit
, tm_coerce :: Maybe a
tm_coerce = (a -> Bool) -> Maybe a -> Maybe a
forall a. (a -> Bool) -> Maybe a -> Maybe a
filterMaybe a -> Bool
f Maybe a
tcoerce }
data TyLitMap a = TLM { forall a. TyLitMap a -> Map Integer a
tlm_number :: Map.Map Integer a
, forall a. TyLitMap a -> UniqFM FastString a
tlm_string :: UniqFM FastString a
, forall a. TyLitMap a -> Map Char a
tlm_char :: Map.Map Char a
}
instance Functor TyLitMap where
fmap :: forall a b. (a -> b) -> TyLitMap a -> TyLitMap b
fmap a -> b
f TLM { tlm_number :: forall a. TyLitMap a -> Map Integer a
tlm_number = Map Integer a
tn, tlm_string :: forall a. TyLitMap a -> UniqFM FastString a
tlm_string = UniqFM FastString a
ts, tlm_char :: forall a. TyLitMap a -> Map Char a
tlm_char = Map Char a
tc } = TLM
{ tlm_number :: Map Integer b
tlm_number = (a -> b) -> Map Integer a -> Map Integer b
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map a -> b
f Map Integer a
tn, tlm_string :: UniqFM FastString b
tlm_string = (a -> b) -> UniqFM FastString a -> UniqFM FastString b
forall elt1 elt2 key.
(elt1 -> elt2) -> UniqFM key elt1 -> UniqFM key elt2
mapUFM a -> b
f UniqFM FastString a
ts, tlm_char :: Map Char b
tlm_char = (a -> b) -> Map Char a -> Map Char b
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map a -> b
f Map Char a
tc }
instance TrieMap TyLitMap where
type Key TyLitMap = TyLit
emptyTM :: forall a. TyLitMap a
emptyTM = TyLitMap a
forall a. TyLitMap a
emptyTyLitMap
lookupTM :: forall b. Key TyLitMap -> TyLitMap b -> Maybe b
lookupTM = TyLit -> TyLitMap b -> Maybe b
Key TyLitMap -> TyLitMap b -> Maybe b
forall a. TyLit -> TyLitMap a -> Maybe a
lkTyLit
alterTM :: forall b. Key TyLitMap -> XT b -> TyLitMap b -> TyLitMap b
alterTM = TyLit -> XT b -> TyLitMap b -> TyLitMap b
Key TyLitMap -> XT b -> TyLitMap b -> TyLitMap b
forall a. TyLit -> XT a -> TyLitMap a -> TyLitMap a
xtTyLit
foldTM :: forall a b. (a -> b -> b) -> TyLitMap a -> b -> b
foldTM = (a -> b -> b) -> TyLitMap a -> b -> b
forall a b. (a -> b -> b) -> TyLitMap a -> b -> b
foldTyLit
filterTM :: forall a. (a -> Bool) -> TyLitMap a -> TyLitMap a
filterTM = (a -> Bool) -> TyLitMap a -> TyLitMap a
forall a. (a -> Bool) -> TyLitMap a -> TyLitMap a
filterTyLit
emptyTyLitMap :: TyLitMap a
emptyTyLitMap :: forall a. TyLitMap a
emptyTyLitMap = TLM { tlm_number :: Map Integer a
tlm_number = Map Integer a
forall k a. Map k a
Map.empty, tlm_string :: UniqFM FastString a
tlm_string = UniqFM FastString a
forall key elt. UniqFM key elt
emptyUFM, tlm_char :: Map Char a
tlm_char = Map Char a
forall k a. Map k a
Map.empty }
lkTyLit :: TyLit -> TyLitMap a -> Maybe a
lkTyLit :: forall a. TyLit -> TyLitMap a -> Maybe a
lkTyLit TyLit
l =
case TyLit
l of
NumTyLit Integer
n -> TyLitMap a -> Map Integer a
forall a. TyLitMap a -> Map Integer a
tlm_number (TyLitMap a -> Map Integer a)
-> (Map Integer a -> Maybe a) -> TyLitMap a -> Maybe a
forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> Integer -> Map Integer a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Integer
n
StrTyLit FastString
n -> TyLitMap a -> UniqFM FastString a
forall a. TyLitMap a -> UniqFM FastString a
tlm_string (TyLitMap a -> UniqFM FastString a)
-> (UniqFM FastString a -> Maybe a) -> TyLitMap a -> Maybe a
forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> (UniqFM FastString a -> FastString -> Maybe a
forall key elt. Uniquable key => UniqFM key elt -> key -> Maybe elt
`lookupUFM` FastString
n)
CharTyLit Char
n -> TyLitMap a -> Map Char a
forall a. TyLitMap a -> Map Char a
tlm_char (TyLitMap a -> Map Char a)
-> (Map Char a -> Maybe a) -> TyLitMap a -> Maybe a
forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> Char -> Map Char a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Char
n
xtTyLit :: TyLit -> XT a -> TyLitMap a -> TyLitMap a
xtTyLit :: forall a. TyLit -> XT a -> TyLitMap a -> TyLitMap a
xtTyLit TyLit
l XT a
f TyLitMap a
m =
case TyLit
l of
NumTyLit Integer
n -> TyLitMap a
m { tlm_number = Map.alter f n (tlm_number m) }
StrTyLit FastString
n -> TyLitMap a
m { tlm_string = alterUFM f (tlm_string m) n }
CharTyLit Char
n -> TyLitMap a
m { tlm_char = Map.alter f n (tlm_char m) }
foldTyLit :: (a -> b -> b) -> TyLitMap a -> b -> b
foldTyLit :: forall a b. (a -> b -> b) -> TyLitMap a -> b -> b
foldTyLit a -> b -> b
l TyLitMap a
m = (b -> UniqFM FastString a -> b) -> UniqFM FastString a -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> b -> b) -> b -> UniqFM FastString a -> b
forall elt a key. (elt -> a -> a) -> a -> UniqFM key elt -> a
foldUFM a -> b -> b
l) (TyLitMap a -> UniqFM FastString a
forall a. TyLitMap a -> UniqFM FastString a
tlm_string TyLitMap a
m)
(b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Map Integer a -> b) -> Map Integer a -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> b -> b) -> b -> Map Integer a -> b
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr a -> b -> b
l) (TyLitMap a -> Map Integer a
forall a. TyLitMap a -> Map Integer a
tlm_number TyLitMap a
m)
(b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Map Char a -> b) -> Map Char a -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> b -> b) -> b -> Map Char a -> b
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr a -> b -> b
l) (TyLitMap a -> Map Char a
forall a. TyLitMap a -> Map Char a
tlm_char TyLitMap a
m)
filterTyLit :: (a -> Bool) -> TyLitMap a -> TyLitMap a
filterTyLit :: forall a. (a -> Bool) -> TyLitMap a -> TyLitMap a
filterTyLit a -> Bool
f (TLM { tlm_number :: forall a. TyLitMap a -> Map Integer a
tlm_number = Map Integer a
tn, tlm_string :: forall a. TyLitMap a -> UniqFM FastString a
tlm_string = UniqFM FastString a
ts, tlm_char :: forall a. TyLitMap a -> Map Char a
tlm_char = Map Char a
tc })
= TLM { tlm_number :: Map Integer a
tlm_number = (a -> Bool) -> Map Integer a -> Map Integer a
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter a -> Bool
f Map Integer a
tn, tlm_string :: UniqFM FastString a
tlm_string = (a -> Bool) -> UniqFM FastString a -> UniqFM FastString a
forall elt key. (elt -> Bool) -> UniqFM key elt -> UniqFM key elt
filterUFM a -> Bool
f UniqFM FastString a
ts, tlm_char :: Map Char a
tlm_char = (a -> Bool) -> Map Char a -> Map Char a
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter a -> Bool
f Map Char a
tc }
newtype TypeMap a = TypeMap (TypeMapG (TypeMapG a))
instance Functor TypeMap where
fmap :: forall a b. (a -> b) -> TypeMap a -> TypeMap b
fmap a -> b
f = \ (TypeMap TypeMapG (TypeMapG a)
m) -> TypeMapG (TypeMapG b) -> TypeMap b
forall a. TypeMapG (TypeMapG a) -> TypeMap a
TypeMap ((TypeMapG a -> TypeMapG b)
-> TypeMapG (TypeMapG a) -> TypeMapG (TypeMapG b)
forall a b. (a -> b) -> GenMap TypeMapX a -> GenMap TypeMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> TypeMapG a -> TypeMapG b
forall a b. (a -> b) -> GenMap TypeMapX a -> GenMap TypeMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) TypeMapG (TypeMapG a)
m)
{-# INLINE fmap #-}
lkTT :: DeBruijn Type -> TypeMap a -> Maybe a
lkTT :: forall a. DeBruijn Type -> TypeMap a -> Maybe a
lkTT (D CmEnv
env Type
ty) (TypeMap TypeMapG (TypeMapG a)
m) = Key TypeMapX -> TypeMapG (TypeMapG a) -> Maybe (TypeMapG a)
forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> GenMap m a -> Maybe a
lkG (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env (Type -> DeBruijn Type) -> Type -> DeBruijn Type
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty) TypeMapG (TypeMapG a)
m
Maybe (TypeMapG a) -> (TypeMapG a -> Maybe a) -> Maybe a
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Key TypeMapX -> TypeMapG a -> Maybe a
forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> GenMap m a -> Maybe a
lkG (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
ty)
xtTT :: DeBruijn Type -> XT a -> TypeMap a -> TypeMap a
xtTT :: forall a. DeBruijn Type -> XT a -> TypeMap a -> TypeMap a
xtTT (D CmEnv
env Type
ty) XT a
f (TypeMap TypeMapG (TypeMapG a)
m)
= TypeMapG (TypeMapG a) -> TypeMap a
forall a. TypeMapG (TypeMapG a) -> TypeMap a
TypeMap (TypeMapG (TypeMapG a)
m TypeMapG (TypeMapG a)
-> (TypeMapG (TypeMapG a) -> TypeMapG (TypeMapG a))
-> TypeMapG (TypeMapG a)
forall a b. a -> (a -> b) -> b
|> Key TypeMapX
-> XT (TypeMapG a)
-> TypeMapG (TypeMapG a)
-> TypeMapG (TypeMapG a)
forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> XT a -> GenMap m a -> GenMap m a
xtG (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env (Type -> DeBruijn Type) -> Type -> DeBruijn Type
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty)
(XT (TypeMapG a) -> TypeMapG (TypeMapG a) -> TypeMapG (TypeMapG a))
-> (TypeMapG a -> TypeMapG a)
-> TypeMapG (TypeMapG a)
-> TypeMapG (TypeMapG a)
forall (m2 :: * -> *) a (m1 :: * -> *).
TrieMap m2 =>
(XT (m2 a) -> m1 (m2 a) -> m1 (m2 a))
-> (m2 a -> m2 a) -> m1 (m2 a) -> m1 (m2 a)
|>> Key TypeMapX -> XT a -> TypeMapG a -> TypeMapG a
forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> XT a -> GenMap m a -> GenMap m a
xtG (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
ty) XT a
f)
instance TrieMap TypeMap where
type Key TypeMap = Type
emptyTM :: forall a. TypeMap a
emptyTM = TypeMapG (TypeMapG a) -> TypeMap a
forall a. TypeMapG (TypeMapG a) -> TypeMap a
TypeMap TypeMapG (TypeMapG a)
forall a. GenMap TypeMapX a
forall (m :: * -> *) a. TrieMap m => m a
emptyTM
lookupTM :: forall b. Key TypeMap -> TypeMap b -> Maybe b
lookupTM Key TypeMap
k TypeMap b
m = DeBruijn Type -> TypeMap b -> Maybe b
forall a. DeBruijn Type -> TypeMap a -> Maybe a
lkTT (Type -> DeBruijn Type
forall a. a -> DeBruijn a
deBruijnize Type
Key TypeMap
k) TypeMap b
m
alterTM :: forall b. Key TypeMap -> XT b -> TypeMap b -> TypeMap b
alterTM Key TypeMap
k XT b
f TypeMap b
m = DeBruijn Type -> XT b -> TypeMap b -> TypeMap b
forall a. DeBruijn Type -> XT a -> TypeMap a -> TypeMap a
xtTT (Type -> DeBruijn Type
forall a. a -> DeBruijn a
deBruijnize Type
Key TypeMap
k) XT b
f TypeMap b
m
foldTM :: forall a b. (a -> b -> b) -> TypeMap a -> b -> b
foldTM a -> b -> b
k (TypeMap TypeMapG (TypeMapG a)
m) = (TypeMapG a -> b -> b) -> TypeMapG (TypeMapG a) -> b -> b
forall a b. (a -> b -> b) -> GenMap TypeMapX a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM ((a -> b -> b) -> TypeMapG a -> b -> b
forall a b. (a -> b -> b) -> GenMap TypeMapX a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k) TypeMapG (TypeMapG a)
m
filterTM :: forall a. (a -> Bool) -> TypeMap a -> TypeMap a
filterTM a -> Bool
f (TypeMap TypeMapG (TypeMapG a)
m) = TypeMapG (TypeMapG a) -> TypeMap a
forall a. TypeMapG (TypeMapG a) -> TypeMap a
TypeMap ((TypeMapG a -> TypeMapG a)
-> TypeMapG (TypeMapG a) -> TypeMapG (TypeMapG a)
forall a b. (a -> b) -> GenMap TypeMapX a -> GenMap TypeMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Bool) -> TypeMapG a -> TypeMapG a
forall a. (a -> Bool) -> GenMap TypeMapX a -> GenMap TypeMapX a
forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f) TypeMapG (TypeMapG a)
m)
foldTypeMap :: (a -> b -> b) -> b -> TypeMap a -> b
foldTypeMap :: forall a b. (a -> b -> b) -> b -> TypeMap a -> b
foldTypeMap a -> b -> b
k b
z TypeMap a
m = (a -> b -> b) -> TypeMap a -> b -> b
forall a b. (a -> b -> b) -> TypeMap a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k TypeMap a
m b
z
emptyTypeMap :: TypeMap a
emptyTypeMap :: forall a. TypeMap a
emptyTypeMap = TypeMap a
forall a. TypeMap a
forall (m :: * -> *) a. TrieMap m => m a
emptyTM
lookupTypeMap :: TypeMap a -> Type -> Maybe a
lookupTypeMap :: forall a. TypeMap a -> Type -> Maybe a
lookupTypeMap TypeMap a
cm Type
t = Key TypeMap -> TypeMap a -> Maybe a
forall b. Key TypeMap -> TypeMap b -> Maybe b
forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM Type
Key TypeMap
t TypeMap a
cm
extendTypeMap :: TypeMap a -> Type -> a -> TypeMap a
extendTypeMap :: forall a. TypeMap a -> Type -> a -> TypeMap a
extendTypeMap TypeMap a
m Type
t a
v = Key TypeMap -> XT a -> TypeMap a -> TypeMap a
forall b. Key TypeMap -> XT b -> TypeMap b -> TypeMap b
forall (m :: * -> *) b. TrieMap m => Key m -> XT b -> m b -> m b
alterTM Type
Key TypeMap
t (Maybe a -> XT a
forall a b. a -> b -> a
const (a -> Maybe a
forall a. a -> Maybe a
Just a
v)) TypeMap a
m
lookupTypeMapWithScope :: TypeMap a -> CmEnv -> Type -> Maybe a
lookupTypeMapWithScope :: forall a. TypeMap a -> CmEnv -> Type -> Maybe a
lookupTypeMapWithScope TypeMap a
m CmEnv
cm Type
t = DeBruijn Type -> TypeMap a -> Maybe a
forall a. DeBruijn Type -> TypeMap a -> Maybe a
lkTT (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
cm Type
t) TypeMap a
m
extendTypeMapWithScope :: TypeMap a -> CmEnv -> Type -> a -> TypeMap a
extendTypeMapWithScope :: forall a. TypeMap a -> CmEnv -> Type -> a -> TypeMap a
extendTypeMapWithScope TypeMap a
m CmEnv
cm Type
t a
v = DeBruijn Type -> XT a -> TypeMap a -> TypeMap a
forall a. DeBruijn Type -> XT a -> TypeMap a -> TypeMap a
xtTT (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
cm Type
t) (Maybe a -> XT a
forall a b. a -> b -> a
const (a -> Maybe a
forall a. a -> Maybe a
Just a
v)) TypeMap a
m
mkDeBruijnContext :: [Var] -> CmEnv
mkDeBruijnContext :: [Var] -> CmEnv
mkDeBruijnContext = CmEnv -> [Var] -> CmEnv
extendCMEs CmEnv
emptyCME
newtype LooseTypeMap a = LooseTypeMap (TypeMapG a)
instance Functor LooseTypeMap where
fmap :: forall a b. (a -> b) -> LooseTypeMap a -> LooseTypeMap b
fmap a -> b
f = \ (LooseTypeMap TypeMapG a
m) -> TypeMapG b -> LooseTypeMap b
forall a. TypeMapG a -> LooseTypeMap a
LooseTypeMap ((a -> b) -> TypeMapG a -> TypeMapG b
forall a b. (a -> b) -> GenMap TypeMapX a -> GenMap TypeMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f TypeMapG a
m)
{-# INLINE fmap #-}
instance TrieMap LooseTypeMap where
type Key LooseTypeMap = Type
emptyTM :: forall a. LooseTypeMap a
emptyTM = TypeMapG a -> LooseTypeMap a
forall a. TypeMapG a -> LooseTypeMap a
LooseTypeMap TypeMapG a
forall a. GenMap TypeMapX a
forall (m :: * -> *) a. TrieMap m => m a
emptyTM
lookupTM :: forall b. Key LooseTypeMap -> LooseTypeMap b -> Maybe b
lookupTM Key LooseTypeMap
k (LooseTypeMap TypeMapG b
m) = Key (GenMap TypeMapX) -> TypeMapG b -> Maybe b
forall b. Key (GenMap TypeMapX) -> GenMap TypeMapX b -> Maybe b
forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM (Type -> DeBruijn Type
forall a. a -> DeBruijn a
deBruijnize Type
Key LooseTypeMap
k) TypeMapG b
m
alterTM :: forall b.
Key LooseTypeMap -> XT b -> LooseTypeMap b -> LooseTypeMap b
alterTM Key LooseTypeMap
k XT b
f (LooseTypeMap TypeMapG b
m) = TypeMapG b -> LooseTypeMap b
forall a. TypeMapG a -> LooseTypeMap a
LooseTypeMap (Key (GenMap TypeMapX) -> XT b -> TypeMapG b -> TypeMapG b
forall b.
Key (GenMap TypeMapX)
-> XT b -> GenMap TypeMapX b -> GenMap TypeMapX b
forall (m :: * -> *) b. TrieMap m => Key m -> XT b -> m b -> m b
alterTM (Type -> DeBruijn Type
forall a. a -> DeBruijn a
deBruijnize Type
Key LooseTypeMap
k) XT b
f TypeMapG b
m)
foldTM :: forall a b. (a -> b -> b) -> LooseTypeMap a -> b -> b
foldTM a -> b -> b
f (LooseTypeMap TypeMapG a
m) = (a -> b -> b) -> TypeMapG a -> b -> b
forall a b. (a -> b -> b) -> GenMap TypeMapX a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
f TypeMapG a
m
filterTM :: forall a. (a -> Bool) -> LooseTypeMap a -> LooseTypeMap a
filterTM a -> Bool
f (LooseTypeMap TypeMapG a
m) = TypeMapG a -> LooseTypeMap a
forall a. TypeMapG a -> LooseTypeMap a
LooseTypeMap ((a -> Bool) -> TypeMapG a -> TypeMapG a
forall a. (a -> Bool) -> GenMap TypeMapX a -> GenMap TypeMapX a
forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f TypeMapG a
m)
type BoundVar = Int
type BoundVarMap a = IntMap.IntMap a
data CmEnv = CME { CmEnv -> BoundVar
cme_next :: !BoundVar
, CmEnv -> VarEnv BoundVar
cme_env :: VarEnv BoundVar }
emptyCME :: CmEnv
emptyCME :: CmEnv
emptyCME = CME { cme_next :: BoundVar
cme_next = BoundVar
0, cme_env :: VarEnv BoundVar
cme_env = VarEnv BoundVar
forall a. VarEnv a
emptyVarEnv }
extendCME :: CmEnv -> Var -> CmEnv
extendCME :: CmEnv -> Var -> CmEnv
extendCME (CME { cme_next :: CmEnv -> BoundVar
cme_next = BoundVar
bv, cme_env :: CmEnv -> VarEnv BoundVar
cme_env = VarEnv BoundVar
env }) Var
v
= CME { cme_next :: BoundVar
cme_next = BoundVar
bvBoundVar -> BoundVar -> BoundVar
forall a. Num a => a -> a -> a
+BoundVar
1, cme_env :: VarEnv BoundVar
cme_env = VarEnv BoundVar -> Var -> BoundVar -> VarEnv BoundVar
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv VarEnv BoundVar
env Var
v BoundVar
bv }
extendCMEs :: CmEnv -> [Var] -> CmEnv
extendCMEs :: CmEnv -> [Var] -> CmEnv
extendCMEs CmEnv
env [Var]
vs = (CmEnv -> Var -> CmEnv) -> CmEnv -> [Var] -> CmEnv
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' CmEnv -> Var -> CmEnv
extendCME CmEnv
env [Var]
vs
lookupCME :: CmEnv -> Var -> Maybe BoundVar
lookupCME :: CmEnv -> Var -> Maybe BoundVar
lookupCME (CME { cme_env :: CmEnv -> VarEnv BoundVar
cme_env = VarEnv BoundVar
env }) Var
v = VarEnv BoundVar -> Var -> Maybe BoundVar
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv VarEnv BoundVar
env Var
v
data DeBruijn a = D CmEnv a
deBruijnize :: a -> DeBruijn a
deBruijnize :: forall a. a -> DeBruijn a
deBruijnize = CmEnv -> a -> DeBruijn a
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
emptyCME
instance Eq (DeBruijn a) => Eq (DeBruijn [a]) where
D CmEnv
_ [] == :: DeBruijn [a] -> DeBruijn [a] -> Bool
== D CmEnv
_ [] = Bool
True
D CmEnv
env (a
x:[a]
xs) == D CmEnv
env' (a
x':[a]
xs') = CmEnv -> a -> DeBruijn a
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env a
x DeBruijn a -> DeBruijn a -> Bool
forall a. Eq a => a -> a -> Bool
== CmEnv -> a -> DeBruijn a
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' a
x' Bool -> Bool -> Bool
&&
CmEnv -> [a] -> DeBruijn [a]
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env [a]
xs DeBruijn [a] -> DeBruijn [a] -> Bool
forall a. Eq a => a -> a -> Bool
== CmEnv -> [a] -> DeBruijn [a]
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' [a]
xs'
DeBruijn [a]
_ == DeBruijn [a]
_ = Bool
False
instance Eq (DeBruijn a) => Eq (DeBruijn (Maybe a)) where
D CmEnv
_ Maybe a
Nothing == :: DeBruijn (Maybe a) -> DeBruijn (Maybe a) -> Bool
== D CmEnv
_ Maybe a
Nothing = Bool
True
D CmEnv
env (Just a
x) == D CmEnv
env' (Just a
x') = CmEnv -> a -> DeBruijn a
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env a
x DeBruijn a -> DeBruijn a -> Bool
forall a. Eq a => a -> a -> Bool
== CmEnv -> a -> DeBruijn a
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' a
x'
DeBruijn (Maybe a)
_ == DeBruijn (Maybe a)
_ = Bool
False
data BndrMap a = BndrMap (TypeMapG (MaybeMap TypeMapG a))
instance Functor BndrMap where
fmap :: forall a b. (a -> b) -> BndrMap a -> BndrMap b
fmap a -> b
f = \ (BndrMap TypeMapG (MaybeMap (GenMap TypeMapX) a)
tm) -> TypeMapG (MaybeMap (GenMap TypeMapX) b) -> BndrMap b
forall a. TypeMapG (MaybeMap (GenMap TypeMapX) a) -> BndrMap a
BndrMap ((MaybeMap (GenMap TypeMapX) a -> MaybeMap (GenMap TypeMapX) b)
-> TypeMapG (MaybeMap (GenMap TypeMapX) a)
-> TypeMapG (MaybeMap (GenMap TypeMapX) b)
forall a b. (a -> b) -> GenMap TypeMapX a -> GenMap TypeMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b)
-> MaybeMap (GenMap TypeMapX) a -> MaybeMap (GenMap TypeMapX) b
forall a b.
(a -> b)
-> MaybeMap (GenMap TypeMapX) a -> MaybeMap (GenMap TypeMapX) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) TypeMapG (MaybeMap (GenMap TypeMapX) a)
tm)
{-# INLINE fmap #-}
instance TrieMap BndrMap where
type Key BndrMap = Var
emptyTM :: forall a. BndrMap a
emptyTM = TypeMapG (MaybeMap (GenMap TypeMapX) a) -> BndrMap a
forall a. TypeMapG (MaybeMap (GenMap TypeMapX) a) -> BndrMap a
BndrMap TypeMapG (MaybeMap (GenMap TypeMapX) a)
forall a. GenMap TypeMapX a
forall (m :: * -> *) a. TrieMap m => m a
emptyTM
lookupTM :: forall b. Key BndrMap -> BndrMap b -> Maybe b
lookupTM = CmEnv -> Var -> BndrMap b -> Maybe b
forall a. CmEnv -> Var -> BndrMap a -> Maybe a
lkBndr CmEnv
emptyCME
alterTM :: forall b. Key BndrMap -> XT b -> BndrMap b -> BndrMap b
alterTM = CmEnv -> Var -> (Maybe b -> Maybe b) -> BndrMap b -> BndrMap b
forall a. CmEnv -> Var -> XT a -> BndrMap a -> BndrMap a
xtBndr CmEnv
emptyCME
foldTM :: forall a b. (a -> b -> b) -> BndrMap a -> b -> b
foldTM = (a -> b -> b) -> BndrMap a -> b -> b
forall a b. (a -> b -> b) -> BndrMap a -> b -> b
fdBndrMap
filterTM :: forall a. (a -> Bool) -> BndrMap a -> BndrMap a
filterTM = (a -> Bool) -> BndrMap a -> BndrMap a
forall a. (a -> Bool) -> BndrMap a -> BndrMap a
ftBndrMap
fdBndrMap :: (a -> b -> b) -> BndrMap a -> b -> b
fdBndrMap :: forall a b. (a -> b -> b) -> BndrMap a -> b -> b
fdBndrMap a -> b -> b
f (BndrMap TypeMapG (MaybeMap (GenMap TypeMapX) a)
tm) = (MaybeMap (GenMap TypeMapX) a -> b -> b)
-> TypeMapG (MaybeMap (GenMap TypeMapX) a) -> b -> b
forall a b. (a -> b -> b) -> GenMap TypeMapX a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM ((a -> b -> b) -> MaybeMap (GenMap TypeMapX) a -> b -> b
forall a b. (a -> b -> b) -> MaybeMap (GenMap TypeMapX) a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
f) TypeMapG (MaybeMap (GenMap TypeMapX) a)
tm
lkBndr :: CmEnv -> Var -> BndrMap a -> Maybe a
lkBndr :: forall a. CmEnv -> Var -> BndrMap a -> Maybe a
lkBndr CmEnv
env Var
v (BndrMap TypeMapG (MaybeMap (GenMap TypeMapX) a)
tymap) = do
MaybeMap (GenMap TypeMapX) a
multmap <- Key TypeMapX
-> TypeMapG (MaybeMap (GenMap TypeMapX) a)
-> Maybe (MaybeMap (GenMap TypeMapX) a)
forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> GenMap m a -> Maybe a
lkG (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env (Var -> Type
varType Var
v)) TypeMapG (MaybeMap (GenMap TypeMapX) a)
tymap
Key (MaybeMap (GenMap TypeMapX))
-> MaybeMap (GenMap TypeMapX) a -> Maybe a
forall b.
Key (MaybeMap (GenMap TypeMapX))
-> MaybeMap (GenMap TypeMapX) b -> Maybe b
forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env (Type -> DeBruijn Type) -> Maybe Type -> Maybe (DeBruijn Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> Maybe Type
varMultMaybe Var
v) MaybeMap (GenMap TypeMapX) a
multmap
xtBndr :: forall a . CmEnv -> Var -> XT a -> BndrMap a -> BndrMap a
xtBndr :: forall a. CmEnv -> Var -> XT a -> BndrMap a -> BndrMap a
xtBndr CmEnv
env Var
v XT a
xt (BndrMap TypeMapG (MaybeMap (GenMap TypeMapX) a)
tymap) =
TypeMapG (MaybeMap (GenMap TypeMapX) a) -> BndrMap a
forall a. TypeMapG (MaybeMap (GenMap TypeMapX) a) -> BndrMap a
BndrMap (TypeMapG (MaybeMap (GenMap TypeMapX) a)
tymap TypeMapG (MaybeMap (GenMap TypeMapX) a)
-> (TypeMapG (MaybeMap (GenMap TypeMapX) a)
-> TypeMapG (MaybeMap (GenMap TypeMapX) a))
-> TypeMapG (MaybeMap (GenMap TypeMapX) a)
forall a b. a -> (a -> b) -> b
|> Key TypeMapX
-> XT (MaybeMap (GenMap TypeMapX) a)
-> TypeMapG (MaybeMap (GenMap TypeMapX) a)
-> TypeMapG (MaybeMap (GenMap TypeMapX) a)
forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> XT a -> GenMap m a -> GenMap m a
xtG (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env (Var -> Type
varType Var
v)) (XT (MaybeMap (GenMap TypeMapX) a)
-> TypeMapG (MaybeMap (GenMap TypeMapX) a)
-> TypeMapG (MaybeMap (GenMap TypeMapX) a))
-> (MaybeMap (GenMap TypeMapX) a -> MaybeMap (GenMap TypeMapX) a)
-> TypeMapG (MaybeMap (GenMap TypeMapX) a)
-> TypeMapG (MaybeMap (GenMap TypeMapX) a)
forall (m2 :: * -> *) a (m1 :: * -> *).
TrieMap m2 =>
(XT (m2 a) -> m1 (m2 a) -> m1 (m2 a))
-> (m2 a -> m2 a) -> m1 (m2 a) -> m1 (m2 a)
|>> (Key (MaybeMap (GenMap TypeMapX))
-> XT a
-> MaybeMap (GenMap TypeMapX) a
-> MaybeMap (GenMap TypeMapX) a
forall b.
Key (MaybeMap (GenMap TypeMapX))
-> XT b
-> MaybeMap (GenMap TypeMapX) b
-> MaybeMap (GenMap TypeMapX) b
forall (m :: * -> *) b. TrieMap m => Key m -> XT b -> m b -> m b
alterTM (CmEnv -> Type -> DeBruijn Type
forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env (Type -> DeBruijn Type) -> Maybe Type -> Maybe (DeBruijn Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> Maybe Type
varMultMaybe Var
v) XT a
xt))
ftBndrMap :: (a -> Bool) -> BndrMap a -> BndrMap a
ftBndrMap :: forall a. (a -> Bool) -> BndrMap a -> BndrMap a
ftBndrMap a -> Bool
f (BndrMap TypeMapG (MaybeMap (GenMap TypeMapX) a)
tm) = TypeMapG (MaybeMap (GenMap TypeMapX) a) -> BndrMap a
forall a. TypeMapG (MaybeMap (GenMap TypeMapX) a) -> BndrMap a
BndrMap ((MaybeMap (GenMap TypeMapX) a -> MaybeMap (GenMap TypeMapX) a)
-> TypeMapG (MaybeMap (GenMap TypeMapX) a)
-> TypeMapG (MaybeMap (GenMap TypeMapX) a)
forall a b. (a -> b) -> GenMap TypeMapX a -> GenMap TypeMapX b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Bool)
-> MaybeMap (GenMap TypeMapX) a -> MaybeMap (GenMap TypeMapX) a
forall a.
(a -> Bool)
-> MaybeMap (GenMap TypeMapX) a -> MaybeMap (GenMap TypeMapX) a
forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f) TypeMapG (MaybeMap (GenMap TypeMapX) a)
tm)
data VarMap a = VM { forall a. VarMap a -> BoundVarMap a
vm_bvar :: BoundVarMap a
, forall a. VarMap a -> DVarEnv a
vm_fvar :: DVarEnv a }
instance Functor VarMap where
fmap :: forall a b. (a -> b) -> VarMap a -> VarMap b
fmap a -> b
f VM { vm_bvar :: forall a. VarMap a -> BoundVarMap a
vm_bvar = BoundVarMap a
bv, vm_fvar :: forall a. VarMap a -> DVarEnv a
vm_fvar = DVarEnv a
fv } = VM { vm_bvar :: BoundVarMap b
vm_bvar = (a -> b) -> BoundVarMap a -> BoundVarMap b
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f BoundVarMap a
bv, vm_fvar :: DVarEnv b
vm_fvar = (a -> b) -> DVarEnv a -> DVarEnv b
forall a b. (a -> b) -> UniqDFM Var a -> UniqDFM Var b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f DVarEnv a
fv }
instance TrieMap VarMap where
type Key VarMap = Var
emptyTM :: forall a. VarMap a
emptyTM = VM { vm_bvar :: BoundVarMap a
vm_bvar = BoundVarMap a
forall a. IntMap a
IntMap.empty, vm_fvar :: DVarEnv a
vm_fvar = DVarEnv a
forall a. DVarEnv a
emptyDVarEnv }
lookupTM :: forall b. Key VarMap -> VarMap b -> Maybe b
lookupTM = CmEnv -> Var -> VarMap b -> Maybe b
forall a. CmEnv -> Var -> VarMap a -> Maybe a
lkVar CmEnv
emptyCME
alterTM :: forall b. Key VarMap -> XT b -> VarMap b -> VarMap b
alterTM = CmEnv -> Var -> (Maybe b -> Maybe b) -> VarMap b -> VarMap b
forall a. CmEnv -> Var -> XT a -> VarMap a -> VarMap a
xtVar CmEnv
emptyCME
foldTM :: forall a b. (a -> b -> b) -> VarMap a -> b -> b
foldTM = (a -> b -> b) -> VarMap a -> b -> b
forall a b. (a -> b -> b) -> VarMap a -> b -> b
fdVar
filterTM :: forall a. (a -> Bool) -> VarMap a -> VarMap a
filterTM = (a -> Bool) -> VarMap a -> VarMap a
forall a. (a -> Bool) -> VarMap a -> VarMap a
ftVar
lkVar :: CmEnv -> Var -> VarMap a -> Maybe a
lkVar :: forall a. CmEnv -> Var -> VarMap a -> Maybe a
lkVar CmEnv
env Var
v
| Just BoundVar
bv <- CmEnv -> Var -> Maybe BoundVar
lookupCME CmEnv
env Var
v = VarMap a -> BoundVarMap a
forall a. VarMap a -> BoundVarMap a
vm_bvar (VarMap a -> BoundVarMap a)
-> (BoundVarMap a -> Maybe a) -> VarMap a -> Maybe a
forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> Key IntMap -> BoundVarMap a -> Maybe a
forall b. Key IntMap -> IntMap b -> Maybe b
forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM BoundVar
Key IntMap
bv
| Bool
otherwise = VarMap a -> DVarEnv a
forall a. VarMap a -> DVarEnv a
vm_fvar (VarMap a -> DVarEnv a)
-> (DVarEnv a -> Maybe a) -> VarMap a -> Maybe a
forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> Var -> DVarEnv a -> Maybe a
forall a. Var -> DVarEnv a -> Maybe a
lkDFreeVar Var
v
xtVar :: CmEnv -> Var -> XT a -> VarMap a -> VarMap a
xtVar :: forall a. CmEnv -> Var -> XT a -> VarMap a -> VarMap a
xtVar CmEnv
env Var
v XT a
f VarMap a
m
| Just BoundVar
bv <- CmEnv -> Var -> Maybe BoundVar
lookupCME CmEnv
env Var
v = VarMap a
m { vm_bvar = vm_bvar m |> alterTM bv f }
| Bool
otherwise = VarMap a
m { vm_fvar = vm_fvar m |> xtDFreeVar v f }
fdVar :: (a -> b -> b) -> VarMap a -> b -> b
fdVar :: forall a b. (a -> b -> b) -> VarMap a -> b -> b
fdVar a -> b -> b
k VarMap a
m = (a -> b -> b) -> IntMap a -> b -> b
forall a b. (a -> b -> b) -> IntMap a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k (VarMap a -> IntMap a
forall a. VarMap a -> BoundVarMap a
vm_bvar VarMap a
m)
(b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b -> b) -> UniqDFM Var a -> b -> b
forall a b. (a -> b -> b) -> UniqDFM Var a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k (VarMap a -> UniqDFM Var a
forall a. VarMap a -> DVarEnv a
vm_fvar VarMap a
m)
lkDFreeVar :: Var -> DVarEnv a -> Maybe a
lkDFreeVar :: forall a. Var -> DVarEnv a -> Maybe a
lkDFreeVar Var
var DVarEnv a
env = DVarEnv a -> Var -> Maybe a
forall a. DVarEnv a -> Var -> Maybe a
lookupDVarEnv DVarEnv a
env Var
var
xtDFreeVar :: Var -> XT a -> DVarEnv a -> DVarEnv a
xtDFreeVar :: forall a. Var -> XT a -> DVarEnv a -> DVarEnv a
xtDFreeVar Var
v XT a
f DVarEnv a
m = XT a -> DVarEnv a -> Var -> DVarEnv a
forall a. (Maybe a -> Maybe a) -> DVarEnv a -> Var -> DVarEnv a
alterDVarEnv XT a
f DVarEnv a
m Var
v
ftVar :: (a -> Bool) -> VarMap a -> VarMap a
ftVar :: forall a. (a -> Bool) -> VarMap a -> VarMap a
ftVar a -> Bool
f (VM { vm_bvar :: forall a. VarMap a -> BoundVarMap a
vm_bvar = BoundVarMap a
bv, vm_fvar :: forall a. VarMap a -> DVarEnv a
vm_fvar = DVarEnv a
fv })
= VM { vm_bvar :: BoundVarMap a
vm_bvar = (a -> Bool) -> BoundVarMap a -> BoundVarMap a
forall a. (a -> Bool) -> IntMap a -> IntMap a
forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f BoundVarMap a
bv, vm_fvar :: DVarEnv a
vm_fvar = (a -> Bool) -> DVarEnv a -> DVarEnv a
forall a. (a -> Bool) -> UniqDFM Var a -> UniqDFM Var a
forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f DVarEnv a
fv }
lkDNamed :: NamedThing n => n -> DNameEnv a -> Maybe a
lkDNamed :: forall n a. NamedThing n => n -> DNameEnv a -> Maybe a
lkDNamed n
n DNameEnv a
env = DNameEnv a -> Name -> Maybe a
forall a. DNameEnv a -> Name -> Maybe a
lookupDNameEnv DNameEnv a
env (n -> Name
forall a. NamedThing a => a -> Name
getName n
n)
xtDNamed :: NamedThing n => n -> XT a -> DNameEnv a -> DNameEnv a
xtDNamed :: forall n a. NamedThing n => n -> XT a -> DNameEnv a -> DNameEnv a
xtDNamed n
tc XT a
f DNameEnv a
m = XT a -> DNameEnv a -> Name -> DNameEnv a
forall a. (Maybe a -> Maybe a) -> DNameEnv a -> Name -> DNameEnv a
alterDNameEnv XT a
f DNameEnv a
m (n -> Name
forall a. NamedThing a => a -> Name
getName n
tc)