{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
-}

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}

module GHC.Core.Map.Type (
     -- * Re-export generic interface
   TrieMap(..), XT,

     -- * Maps over 'Type's
   TypeMap, emptyTypeMap, extendTypeMap, lookupTypeMap, foldTypeMap,
   LooseTypeMap,
   -- ** With explicit scoping
   CmEnv, lookupCME, extendTypeMapWithScope, lookupTypeMapWithScope,
   mkDeBruijnContext, extendCME, extendCMEs, emptyCME,

   -- * Utilities for use by friends only
   TypeMapG, CoercionMapG,

   DeBruijn(..), deBruijnize, eqDeBruijnType, eqDeBruijnVar,

   BndrMap, xtBndr, lkBndr,
   VarMap, xtVar, lkVar, lkDFreeVar, xtDFreeVar,

   xtDNamed, lkDNamed

   ) where

-- This module is separate from GHC.Core.Map.Expr to avoid a module loop
-- between GHC.Core.Unify (which depends on this module) and GHC.Core

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 ( (>=>) )

-- NB: Be careful about RULES and type families (#5821).  So we should make sure
-- to specify @Key TypeMapX@ (and not @DeBruijn Type@, the reduced form)

{-# 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 #-}

{-
************************************************************************
*                                                                      *
                   Coercions
*                                                                      *
************************************************************************
-}

-- We should really never care about the contents of a coercion. Instead,
-- just look up the coercion's type.
newtype CoercionMap a = CoercionMap (CoercionMapG a)

-- TODO(22292): derive
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)

-- TODO(22292): derive
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)

{-
************************************************************************
*                                                                      *
                   Types
*                                                                      *
************************************************************************
-}

-- | @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 TypeMapG = GenMap TypeMapX

-- | @TypeMapX a@ is the base map from @DeBruijn Type@ to @a@, but without the
-- 'GenMap' optimization. See Note [Computing equality on types] in GHC.Core.Type.
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)  -- Note [Equality on AppTys] in GHC.Core.Type
       , forall a. TypeMapX a -> DNameEnv a
tm_tycon  :: DNameEnv a
       , forall a. TypeMapX a -> TypeMapG (BndrMap a)
tm_forall :: TypeMapG (BndrMap a) -- See Note [Binders] in GHC.Core.Map.Expr
       , forall a. TypeMapX a -> TyLitMap a
tm_tylit  :: TyLitMap a
       , forall a. TypeMapX a -> Maybe a
tm_coerce :: Maybe a
       }
    -- Note that there is no tyconapp case; see Note [Equality on AppTys] in GHC.Core.Type

-- | Squeeze out any synonyms, and change TyConApps to nested AppTys. Why the
-- last one? See Note [Equality on AppTys] in GHC.Core.Type
--
-- We also keep (Eq a => a) as a FunTy, distinct from ((->) (Eq a) a).
trieMapView :: Type -> Maybe Type
trieMapView :: Type -> Maybe Type
trieMapView Type
ty
  -- First check for TyConApps that need to be expanded to
  -- AppTy chains.  This includes eliminating FunTy entirely.
  | 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

  -- Then resolve any remaining nullary synonyms.
  | 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

-- TODO(22292): derive
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

-- | An equality relation between two 'Type's (known below as @t1 :: k2@
-- and @t2 :: k2@)
data TypeEquality = TNEQ -- ^ @t1 /= t2@
                  | TEQ  -- ^ @t1 ~ t2@ and there are not casts in either,
                         -- therefore we can conclude @k1 ~ k2@
                  | TEQX -- ^ @t1 ~ t2@ yet one of the types contains a cast so
                         -- they may differ in kind

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) =
    -- See Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep
    -- See Note [Computing equality on types]
    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

    -- See Note [Comparing nullary type synonyms] in GHC.Core.Type
    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
          -- See Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep
          (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')
          -- See Note [Equality on AppTys] in GHC.Core.Type
          (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`
                 -- NB: eqDeBruijnType does the kind check requested by
                 -- Note [Equality on FunTys] in GHC.Core.TyCo.Rep
                 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`
                 -- Comparing multiplicities last because the test is usually true
                 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')
              -> -- See Note [ForAllTy and type equality] in
                 -- GHC.Core.TyCo.Compare for why we use `eqForAllVis` here
                 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

    -- These bangs make 'gos' strict in the CMEnv, which in turn
    -- keeps the CMEnv unboxed across the go/gos mutual recursion
    -- (If you want a test case, T9872c really exercises this code.)
    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

    -- trieMapView has eliminated non-nullary TyConApp
    -- and FunTy into an AppTy chain
    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 }

-- trieMapView has eliminated non-nullary TyConApp
-- and FunTy into an AppTy chain
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
                      }

-- TODO(22292): derive
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 }

-------------------------------------------------
-- | @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.
newtype TypeMap a = TypeMap (TypeMapG (TypeMapG a))

-- TODO(22292): derive
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)

-- Below are some client-oriented functions which operate on 'TypeMap'.

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

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

-- | Construct a deBruijn environment with the given variables in scope.
-- e.g. @mkDeBruijnEnv [a,b,c]@ constructs a context @forall a b c.@
mkDeBruijnContext :: [Var] -> CmEnv
mkDeBruijnContext :: [Var] -> CmEnv
mkDeBruijnContext = CmEnv -> [Var] -> CmEnv
extendCMEs CmEnv
emptyCME

-- | 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.
newtype LooseTypeMap a = LooseTypeMap (TypeMapG a)

-- TODO(22292): derive
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)

{-
************************************************************************
*                                                                      *
                   Variables
*                                                                      *
************************************************************************
-}

type BoundVar = Int  -- Bound variables are deBruijn numbered
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

-- | @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.
data DeBruijn a = D CmEnv a

-- | Synthesizes a @DeBruijn a@ from an @a@, by assuming that there are no
-- bound binders (an empty 'CmEnv').  This is usually what you want if there
-- isn't already a 'CmEnv' in scope.
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

--------- Variable binders -------------

-- | 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.
data BndrMap a = BndrMap (TypeMapG (MaybeMap TypeMapG a))

-- TODO(22292): derive
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


-- We need to use 'BndrMap' for 'Coercion', 'CoreExpr' AND 'Type', since all
-- of these data types have binding forms.

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)

--------- Variable occurrence -------------
data VarMap a = VM { forall a. VarMap a -> BoundVarMap a
vm_bvar   :: BoundVarMap a  -- Bound variable
                   , forall a. VarMap a -> DVarEnv a
vm_fvar   :: DVarEnv a }      -- Free variable

-- TODO(22292): derive
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)