{-
(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) -> forall a. CoercionMapG a -> CoercionMap a
CoercionMap (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                     = forall a. CoercionMapG a -> CoercionMap a
CoercionMap 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) = forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM (forall a. a -> DeBruijn a
deBruijnize 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) = forall a. CoercionMapG a -> CoercionMap a
CoercionMap (forall (m :: * -> *) b. TrieMap m => Key m -> XT b -> m b -> m b
alterTM (forall a. a -> DeBruijn a
deBruijnize 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) = 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) = forall a. CoercionMapG a -> CoercionMap a
CoercionMap (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) -> forall a. TypeMapX a -> CoercionMapX a
CoercionMapX (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 = forall a. TypeMapX a -> CoercionMapX a
CoercionMapX forall (m :: * -> *) a. TrieMap m => m a
emptyTM
  lookupTM :: forall b. Key CoercionMapX -> CoercionMapX b -> Maybe b
lookupTM = forall a. DeBruijn Coercion -> CoercionMapX a -> Maybe a
lkC
  alterTM :: forall b.
Key CoercionMapX -> XT b -> CoercionMapX b -> CoercionMapX b
alterTM  = 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) = 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) = forall a. TypeMapX a -> CoercionMapX a
CoercionMapX (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
    = forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env1 (Coercion -> Type
coercionType Coercion
co1) forall a. Eq a => a -> a -> Bool
==
      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) = forall a. DeBruijn Type -> TypeMapX a -> Maybe a
lkT (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env 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)
  = forall a. TypeMapX a -> CoercionMapX a
CoercionMapX (forall a. DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
xtT (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env 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]
_)) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
  = forall a. a -> Maybe a
Just forall a b. (a -> 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
  = forall a. a -> Maybe a
Just Type
ty'

trieMapView 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 = 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 = 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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  = 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 = 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  = forall a. TypeMapX a
emptyT
   lookupTM :: forall b. Key TypeMapX -> TypeMapX b -> Maybe b
lookupTM = forall a. DeBruijn Type -> TypeMapX a -> Maybe a
lkT
   alterTM :: forall b. Key TypeMapX -> XT b -> TypeMapX b -> TypeMapX b
alterTM  = forall a. DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
xtT
   foldTM :: forall a b. (a -> b -> b) -> TypeMapX a -> b -> b
foldTM   = forall a b. (a -> b -> b) -> TypeMapX a -> b -> b
fdT
   filterTM :: forall a. (a -> Bool) -> TypeMapX a -> TypeMapX a
filterTM = 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 (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env1 Type
k1) (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env2 Type
k2))
      TypeEquality
ty_eq -> TypeEquality -> Bool
toBool TypeEquality
ty_eq
  where
    k1 :: Type
k1 = HasDebugCallStack => Type -> Type
typeKind Type
t1
    k2 :: Type
k2 = HasDebugCallStack => 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 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 (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 (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 (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1) (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 (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t) (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1'))

          (TyVarTy Var
v, TyVarTy Var
v')
              -> Bool -> TypeEquality
liftEquality forall a b. (a -> b) -> a -> b
$ DeBruijn Var -> DeBruijn Var -> Bool
eqDeBruijnVar (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Var
v) (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') <- HasDebugCallStack => Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
s
              -> DeBruijn Type -> DeBruijn Type -> TypeEquality
go (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1) (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' Type
t1') TypeEquality -> TypeEquality -> TypeEquality
`andEq` DeBruijn Type -> DeBruijn Type -> TypeEquality
go (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t2) (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' Type
t2')
          (Type
s, AppTy Type
t1' Type
t2') | Just (Type
t1, Type
t2) <- HasDebugCallStack => Type -> Maybe (Type, Type)
splitAppTyNoView_maybe Type
s
              -> DeBruijn Type -> DeBruijn Type -> TypeEquality
go (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1) (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' Type
t1') TypeEquality -> TypeEquality -> TypeEquality
`andEq` DeBruijn Type -> DeBruijn Type -> TypeEquality
go (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t2) (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 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 (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1) (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' Type
t1')) TypeEquality -> TypeEquality -> TypeEquality
`andEq`
                 Bool -> TypeEquality
liftEquality (DeBruijn Type -> DeBruijn Type -> Bool
eqDeBruijnType (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t2) (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 (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
w1) (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 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 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 (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env (Var -> Type
varType Var
tv)) (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' (Var -> Type
varType Var
tv')) TypeEquality -> TypeEquality -> TypeEquality
`andEq`
                 DeBruijn Type -> DeBruijn Type -> TypeEquality
go (forall a. CmEnv -> a -> DeBruijn a
D (CmEnv -> Var -> CmEnv
extendCME CmEnv
env Var
tv) Type
ty) (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 (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
e1 Type
ty1) (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 forall a. Eq a => a -> a -> Bool
== BoundVar
b2
        (Maybe BoundVar
Nothing, Maybe BoundVar
Nothing) -> Var
v1 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 = forall doc. IsLine doc => String -> doc
text String
"TypeMap elts" forall doc. IsLine doc => doc -> doc -> doc
<+> forall a. Outputable a => a -> SDoc
ppr (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  = forall (m :: * -> *) a. TrieMap m => m a
emptyTM
            , tm_app :: TypeMapG (TypeMapG a)
tm_app  = forall (m :: * -> *) a. TrieMap m => m a
emptyTM
            , tm_tycon :: DNameEnv a
tm_tycon  = forall a. DNameEnv a
emptyDNameEnv
            , tm_forall :: TypeMapG (BndrMap a)
tm_forall = forall (m :: * -> *) a. TrieMap m => m a
emptyTM
            , tm_tylit :: TyLitMap a
tm_tylit  = forall a. TyLitMap a
emptyTyLitMap
            , tm_coerce :: Maybe a
tm_coerce = 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)                 = forall a. TypeMapX a -> VarMap a
tm_var    forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> forall a. CmEnv -> Var -> VarMap a -> Maybe a
lkVar CmEnv
env Var
v
    go (AppTy Type
t1 Type
t2)               = forall a. TypeMapX a -> TypeMapG (TypeMapG a)
tm_app    forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> GenMap m a -> Maybe a
lkG (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1)
                                               forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> GenMap m a -> Maybe a
lkG (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t2)
    go (TyConApp TyCon
tc [])            = forall a. TypeMapX a -> DNameEnv a
tm_tycon  forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> forall n a. NamedThing n => n -> DNameEnv a -> Maybe a
lkDNamed TyCon
tc
    go (LitTy TyLit
l)                   = forall a. TypeMapX a -> TyLitMap a
tm_tylit  forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> forall a. TyLit -> TyLitMap a -> Maybe a
lkTyLit TyLit
l
    go (ForAllTy (Bndr Var
tv ForAllTyFlag
_) Type
ty)   = forall a. TypeMapX a -> TypeMapG (BndrMap a)
tm_forall forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> GenMap m a -> Maybe a
lkG (forall a. CmEnv -> a -> DeBruijn a
D (CmEnv -> Var -> CmEnv
extendCME CmEnv
env Var
tv) Type
ty)
                                               forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> 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 {})             = 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]
_))       = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"lkT TyConApp" (forall a. Outputable a => a -> SDoc
ppr Type
ty)
    go ty :: Type
ty@(FunTy {})               = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"lkT FunTy" (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 = forall a. DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
xtT (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 :: VarMap a
tm_var    = forall a. TypeMapX a -> VarMap a
tm_var TypeMapX a
m forall a b. a -> (a -> b) -> b
|> forall a. CmEnv -> Var -> XT a -> VarMap a -> VarMap a
xtVar CmEnv
env Var
v XT a
f }
xtT (D CmEnv
env (AppTy Type
t1 Type
t2))     XT a
f TypeMapX a
m = TypeMapX a
m { tm_app :: TypeMapG (TypeMapG a)
tm_app    = forall a. TypeMapX a -> TypeMapG (TypeMapG a)
tm_app TypeMapX a
m forall a b. a -> (a -> b) -> b
|> forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> XT a -> GenMap m a -> GenMap m a
xtG (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t1)
                                                            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)
|>> forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> XT a -> GenMap m a -> GenMap m a
xtG (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env Type
t2) XT a
f }
xtT (D CmEnv
_   (TyConApp TyCon
tc []))  XT a
f TypeMapX a
m = TypeMapX a
m { tm_tycon :: DNameEnv a
tm_tycon  = forall a. TypeMapX a -> DNameEnv a
tm_tycon TypeMapX a
m forall a b. a -> (a -> b) -> b
|> forall n a. NamedThing n => n -> XT a -> DNameEnv a -> DNameEnv a
xtDNamed TyCon
tc XT a
f }
xtT (D CmEnv
_   (LitTy TyLit
l))         XT a
f TypeMapX a
m = TypeMapX a
m { tm_tylit :: TyLitMap a
tm_tylit  = forall a. TypeMapX a -> TyLitMap a
tm_tylit TypeMapX a
m forall a b. a -> (a -> b) -> b
|> forall a. TyLit -> XT a -> TyLitMap a -> TyLitMap a
xtTyLit TyLit
l XT a
f }
xtT (D CmEnv
env (CastTy Type
t Coercion
_))      XT a
f TypeMapX a
m = forall a. DeBruijn Type -> XT a -> TypeMapX a -> TypeMapX a
xtT (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 :: Maybe a
tm_coerce = forall a. TypeMapX a -> Maybe a
tm_coerce TypeMapX a
m forall a b. a -> (a -> b) -> b
|> XT a
f }
xtT (D CmEnv
env (ForAllTy (Bndr Var
tv ForAllTyFlag
_) Type
ty))  XT a
f TypeMapX a
m
  = TypeMapX a
m { tm_forall :: TypeMapG (BndrMap a)
tm_forall = forall a. TypeMapX a -> TypeMapG (BndrMap a)
tm_forall TypeMapX a
m forall a b. a -> (a -> b) -> b
|> forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> XT a -> GenMap m a -> GenMap m a
xtG (forall a. CmEnv -> a -> DeBruijn a
D (CmEnv -> Var -> CmEnv
extendCME CmEnv
env Var
tv) Type
ty)
                                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)
|>> forall a. CmEnv -> Var -> XT a -> BndrMap a -> BndrMap a
xtBndr CmEnv
env Var
tv XT a
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
_ = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"xtT TyConApp" (forall a. Outputable a => a -> SDoc
ppr Type
ty)
xtT (D CmEnv
_   ty :: Type
ty@(FunTy {}))         XT a
_ TypeMapX a
_ = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"xtT FunTy" (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 = forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k (forall a. TypeMapX a -> VarMap a
tm_var TypeMapX a
m)
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM (forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k) (forall a. TypeMapX a -> TypeMapG (TypeMapG a)
tm_app TypeMapX a
m)
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k (forall a. TypeMapX a -> DNameEnv a
tm_tycon TypeMapX a
m)
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM (forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k) (forall a. TypeMapX a -> TypeMapG (BndrMap a)
tm_forall TypeMapX a
m)
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b -> b) -> TyLitMap a -> b -> b
foldTyLit a -> b -> b
k (forall a. TypeMapX a -> TyLitMap a
tm_tylit TypeMapX a
m)
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b -> b) -> Maybe a -> b -> b
foldMaybe a -> b -> b
k (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    = 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    = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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  = 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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  = forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f TyLitMap a
tlit
       , tm_coerce :: Maybe a
tm_coerce = 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 = 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 = 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 = 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  = forall a. TyLitMap a
emptyTyLitMap
   lookupTM :: forall b. Key TyLitMap -> TyLitMap b -> Maybe b
lookupTM = forall a. TyLit -> TyLitMap a -> Maybe a
lkTyLit
   alterTM :: forall b. Key TyLitMap -> XT b -> TyLitMap b -> TyLitMap b
alterTM  = forall a. TyLit -> XT a -> TyLitMap a -> TyLitMap a
xtTyLit
   foldTM :: forall a b. (a -> b -> b) -> TyLitMap a -> b -> b
foldTM   = forall a b. (a -> b -> b) -> TyLitMap a -> b -> b
foldTyLit
   filterTM :: forall a. (a -> Bool) -> TyLitMap a -> TyLitMap a
filterTM = 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 = forall k a. Map k a
Map.empty, tlm_string :: UniqFM FastString a
tlm_string = forall key elt. UniqFM key elt
emptyUFM, tlm_char :: Map Char a
tlm_char = 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 -> forall a. TyLitMap a -> Map Integer a
tlm_number forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Integer
n
    StrTyLit FastString
n -> forall a. TyLitMap a -> UniqFM FastString a
tlm_string forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> (forall key elt. Uniquable key => UniqFM key elt -> key -> Maybe elt
`lookupUFM` FastString
n)
    CharTyLit Char
n -> forall a. TyLitMap a -> Map Char a
tlm_char forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> 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 Integer a
tlm_number = forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter XT a
f Integer
n (forall a. TyLitMap a -> Map Integer a
tlm_number TyLitMap a
m) }
    StrTyLit FastString
n ->  TyLitMap a
m { tlm_string :: UniqFM FastString a
tlm_string = forall key elt.
Uniquable key =>
(Maybe elt -> Maybe elt) -> UniqFM key elt -> key -> UniqFM key elt
alterUFM  XT a
f (forall a. TyLitMap a -> UniqFM FastString a
tlm_string TyLitMap a
m) FastString
n }
    CharTyLit Char
n -> TyLitMap a
m { tlm_char :: Map Char a
tlm_char = forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter XT a
f Char
n (forall a. TyLitMap a -> Map Char a
tlm_char TyLitMap a
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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall elt a key. (elt -> a -> a) -> a -> UniqFM key elt -> a
foldUFM a -> b -> b
l) (forall a. TyLitMap a -> UniqFM FastString a
tlm_string TyLitMap a
m)
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr a -> b -> b
l) (forall a. TyLitMap a -> Map Integer a
tlm_number TyLitMap a
m)
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr a -> b -> b
l) (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 = 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 = 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 = 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) -> forall a. TypeMapG (TypeMapG a) -> TypeMap a
TypeMap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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) = forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> GenMap m a -> Maybe a
lkG (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Type -> Type
typeKind Type
ty) TypeMapG (TypeMapG a)
m
                          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> GenMap m a -> Maybe a
lkG (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)
  = forall a. TypeMapG (TypeMapG a) -> TypeMap a
TypeMap (TypeMapG (TypeMapG a)
m forall a b. a -> (a -> b) -> b
|> forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> XT a -> GenMap m a -> GenMap m a
xtG (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Type -> Type
typeKind Type
ty)
               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)
|>> forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> XT a -> GenMap m a -> GenMap m a
xtG (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 = forall a. TypeMapG (TypeMapG a) -> TypeMap a
TypeMap forall (m :: * -> *) a. TrieMap m => m a
emptyTM
    lookupTM :: forall b. Key TypeMap -> TypeMap b -> Maybe b
lookupTM Key TypeMap
k TypeMap b
m = forall a. DeBruijn Type -> TypeMap a -> Maybe a
lkTT (forall a. a -> DeBruijn a
deBruijnize 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 = forall a. DeBruijn Type -> XT a -> TypeMap a -> TypeMap a
xtTT (forall a. a -> DeBruijn a
deBruijnize 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) = forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM (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) = forall a. TypeMapG (TypeMapG a) -> TypeMap a
TypeMap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 = 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 = 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 = forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM Type
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 = forall (m :: * -> *) b. TrieMap m => Key m -> XT b -> m b -> m b
alterTM Type
t (forall a b. a -> b -> a
const (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 = forall a. DeBruijn Type -> TypeMap a -> Maybe a
lkTT (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 = forall a. DeBruijn Type -> XT a -> TypeMap a -> TypeMap a
xtTT (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
cm Type
t) (forall a b. a -> b -> a
const (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) -> forall a. TypeMapG a -> LooseTypeMap a
LooseTypeMap (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 = forall a. TypeMapG a -> LooseTypeMap a
LooseTypeMap 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) = forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM (forall a. a -> DeBruijn a
deBruijnize 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) = forall a. TypeMapG a -> LooseTypeMap a
LooseTypeMap (forall (m :: * -> *) b. TrieMap m => Key m -> XT b -> m b -> m b
alterTM (forall a. a -> DeBruijn a
deBruijnize 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) = 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) = forall a. TypeMapG a -> LooseTypeMap a
LooseTypeMap (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 = 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
bvforall a. Num a => a -> a -> a
+BoundVar
1, cme_env :: VarEnv BoundVar
cme_env = 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 = 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 = 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 = 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') = forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env a
x  forall a. Eq a => a -> a -> Bool
== forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env' a
x' Bool -> Bool -> Bool
&&
                                      forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env [a]
xs forall a. Eq a => a -> a -> Bool
== 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') = forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env a
x  forall a. Eq a => a -> a -> Bool
== 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) -> forall a. TypeMapG (MaybeMap (GenMap TypeMapX) a) -> BndrMap a
BndrMap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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  = forall a. TypeMapG (MaybeMap (GenMap TypeMapX) a) -> BndrMap a
BndrMap forall (m :: * -> *) a. TrieMap m => m a
emptyTM
   lookupTM :: forall b. Key BndrMap -> BndrMap b -> Maybe b
lookupTM = forall a. CmEnv -> Var -> BndrMap a -> Maybe a
lkBndr CmEnv
emptyCME
   alterTM :: forall b. Key BndrMap -> XT b -> BndrMap b -> BndrMap b
alterTM  = 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   = forall a b. (a -> b -> b) -> BndrMap a -> b -> b
fdBndrMap
   filterTM :: forall a. (a -> Bool) -> BndrMap a -> BndrMap a
filterTM = 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) = forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM (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 <- forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> GenMap m a -> Maybe a
lkG (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env (Var -> Type
varType Var
v)) TypeMapG (MaybeMap (GenMap TypeMapX) a)
tymap
  forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env 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)  =
  forall a. TypeMapG (MaybeMap (GenMap TypeMapX) a) -> BndrMap a
BndrMap (TypeMapG (MaybeMap (GenMap TypeMapX) a)
tymap forall a b. a -> (a -> b) -> b
|> forall (m :: * -> *) a.
(Eq (Key m), TrieMap m) =>
Key m -> XT a -> GenMap m a -> GenMap m a
xtG (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env (Var -> Type
varType Var
v)) 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)
|>> (forall (m :: * -> *) b. TrieMap m => Key m -> XT b -> m b -> m b
alterTM (forall a. CmEnv -> a -> DeBruijn a
D CmEnv
env 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) = forall a. TypeMapG (MaybeMap (GenMap TypeMapX) a) -> BndrMap a
BndrMap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 = 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 = 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 = forall a. IntMap a
IntMap.empty, vm_fvar :: DVarEnv a
vm_fvar = forall a. DVarEnv a
emptyDVarEnv }
   lookupTM :: forall b. Key VarMap -> VarMap b -> Maybe b
lookupTM = forall a. CmEnv -> Var -> VarMap a -> Maybe a
lkVar CmEnv
emptyCME
   alterTM :: forall b. Key VarMap -> XT b -> VarMap b -> VarMap b
alterTM  = 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   = forall a b. (a -> b -> b) -> VarMap a -> b -> b
fdVar
   filterTM :: forall a. (a -> Bool) -> VarMap a -> VarMap a
filterTM = 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 = forall a. VarMap a -> BoundVarMap a
vm_bvar forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM BoundVar
bv
  | Bool
otherwise                  = forall a. VarMap a -> DVarEnv a
vm_fvar forall a b c. (a -> b) -> (b -> c) -> a -> c
>.> 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 :: BoundVarMap a
vm_bvar = forall a. VarMap a -> BoundVarMap a
vm_bvar VarMap a
m forall a b. a -> (a -> b) -> b
|> forall (m :: * -> *) b. TrieMap m => Key m -> XT b -> m b -> m b
alterTM BoundVar
bv XT a
f }
  | Bool
otherwise                  = VarMap a
m { vm_fvar :: DVarEnv a
vm_fvar = forall a. VarMap a -> DVarEnv a
vm_fvar VarMap a
m forall a b. a -> (a -> b) -> b
|> forall a. Var -> XT a -> DVarEnv a -> DVarEnv a
xtDFreeVar Var
v XT a
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 = forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k (forall a. VarMap a -> BoundVarMap a
vm_bvar VarMap a
m)
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k (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 = 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 = 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 = forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f BoundVarMap a
bv, vm_fvar :: DVarEnv a
vm_fvar = 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 = forall a. DNameEnv a -> Name -> Maybe a
lookupDNameEnv DNameEnv a
env (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 = forall a. (Maybe a -> Maybe a) -> DNameEnv a -> Name -> DNameEnv a
alterDNameEnv XT a
f DNameEnv a
m (forall a. NamedThing a => a -> Name
getName n
tc)