module Predicate (
Pred(..), classifyPredType,
isPredTy, isEvVarType,
EqRel(..), eqRelRole,
isEqPrimPred, isEqPred,
getEqPredTys, getEqPredTys_maybe, getEqPredRole,
predTypeEqRel,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
mkClassPred, isDictTy,
isClassPred, isEqPredClass, isCTupleClass,
getClassPredTys, getClassPredTys_maybe,
isIPPred, isIPPred_maybe, isIPTyCon, isIPClass, hasIPPred,
DictId, isEvVar, isDictId
) where
import GhcPrelude
import Type
import Class
import TyCon
import Var
import Coercion
import PrelNames
import FastString
import Outputable
import Util
import Control.Monad ( guard )
data Pred
= ClassPred Class [Type]
| EqPred EqRel Type Type
| IrredPred PredType
| ForAllPred [TyCoVarBinder] [PredType] PredType
classifyPredType :: PredType -> Pred
classifyPredType :: PredType -> Pred
classifyPredType ev_ty :: PredType
ev_ty = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ev_ty of
Just (tc :: TyCon
tc, [_, _, ty1 :: PredType
ty1, ty2 :: PredType
ty2])
| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey -> EqRel -> PredType -> PredType -> Pred
EqPred EqRel
ReprEq PredType
ty1 PredType
ty2
| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey -> EqRel -> PredType -> PredType -> Pred
EqPred EqRel
NomEq PredType
ty1 PredType
ty2
Just (tc :: TyCon
tc, tys :: [PredType]
tys)
| Just clas :: Class
clas <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
-> Class -> [PredType] -> Pred
ClassPred Class
clas [PredType]
tys
_ | (tvs :: [TyCoVarBinder]
tvs, rho :: PredType
rho) <- PredType -> ([TyCoVarBinder], PredType)
splitForAllVarBndrs PredType
ev_ty
, (theta :: [PredType]
theta, pred :: PredType
pred) <- PredType -> ([PredType], PredType)
splitFunTys PredType
rho
, Bool -> Bool
not ([TyCoVarBinder] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVarBinder]
tvs Bool -> Bool -> Bool
&& [PredType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PredType]
theta)
-> [TyCoVarBinder] -> [PredType] -> PredType -> Pred
ForAllPred [TyCoVarBinder]
tvs [PredType]
theta PredType
pred
| Bool
otherwise
-> PredType -> Pred
IrredPred PredType
ev_ty
mkClassPred :: Class -> [Type] -> PredType
mkClassPred :: Class -> [PredType] -> PredType
mkClassPred clas :: Class
clas tys :: [PredType]
tys = TyCon -> [PredType] -> PredType
mkTyConApp (Class -> TyCon
classTyCon Class
clas) [PredType]
tys
isDictTy :: Type -> Bool
isDictTy :: PredType -> Bool
isDictTy = PredType -> Bool
isClassPred
getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])
getClassPredTys :: PredType -> (Class, [PredType])
getClassPredTys ty :: PredType
ty = case PredType -> Maybe (Class, [PredType])
getClassPredTys_maybe PredType
ty of
Just (clas :: Class
clas, tys :: [PredType]
tys) -> (Class
clas, [PredType]
tys)
Nothing -> String -> SDoc -> (Class, [PredType])
forall a. HasCallStack => String -> SDoc -> a
pprPanic "getClassPredTys" (PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr PredType
ty)
getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
getClassPredTys_maybe :: PredType -> Maybe (Class, [PredType])
getClassPredTys_maybe ty :: PredType
ty = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty of
Just (tc :: TyCon
tc, tys :: [PredType]
tys) | Just clas :: Class
clas <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc -> (Class, [PredType]) -> Maybe (Class, [PredType])
forall a. a -> Maybe a
Just (Class
clas, [PredType]
tys)
_ -> Maybe (Class, [PredType])
forall a. Maybe a
Nothing
data EqRel = NomEq | ReprEq
deriving (EqRel -> EqRel -> Bool
(EqRel -> EqRel -> Bool) -> (EqRel -> EqRel -> Bool) -> Eq EqRel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EqRel -> EqRel -> Bool
$c/= :: EqRel -> EqRel -> Bool
== :: EqRel -> EqRel -> Bool
$c== :: EqRel -> EqRel -> Bool
Eq, Eq EqRel
Eq EqRel =>
(EqRel -> EqRel -> Ordering)
-> (EqRel -> EqRel -> Bool)
-> (EqRel -> EqRel -> Bool)
-> (EqRel -> EqRel -> Bool)
-> (EqRel -> EqRel -> Bool)
-> (EqRel -> EqRel -> EqRel)
-> (EqRel -> EqRel -> EqRel)
-> Ord EqRel
EqRel -> EqRel -> Bool
EqRel -> EqRel -> Ordering
EqRel -> EqRel -> EqRel
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: EqRel -> EqRel -> EqRel
$cmin :: EqRel -> EqRel -> EqRel
max :: EqRel -> EqRel -> EqRel
$cmax :: EqRel -> EqRel -> EqRel
>= :: EqRel -> EqRel -> Bool
$c>= :: EqRel -> EqRel -> Bool
> :: EqRel -> EqRel -> Bool
$c> :: EqRel -> EqRel -> Bool
<= :: EqRel -> EqRel -> Bool
$c<= :: EqRel -> EqRel -> Bool
< :: EqRel -> EqRel -> Bool
$c< :: EqRel -> EqRel -> Bool
compare :: EqRel -> EqRel -> Ordering
$ccompare :: EqRel -> EqRel -> Ordering
$cp1Ord :: Eq EqRel
Ord)
instance Outputable EqRel where
ppr :: EqRel -> SDoc
ppr NomEq = String -> SDoc
text "nominal equality"
ppr ReprEq = String -> SDoc
text "representational equality"
eqRelRole :: EqRel -> Role
eqRelRole :: EqRel -> Role
eqRelRole NomEq = Role
Nominal
eqRelRole ReprEq = Role
Representational
getEqPredTys :: PredType -> (Type, Type)
getEqPredTys :: PredType -> (PredType, PredType)
getEqPredTys ty :: PredType
ty
= case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty of
Just (tc :: TyCon
tc, [_, _, ty1 :: PredType
ty1, ty2 :: PredType
ty2])
| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey
Bool -> Bool -> Bool
|| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey
-> (PredType
ty1, PredType
ty2)
_ -> String -> SDoc -> (PredType, PredType)
forall a. HasCallStack => String -> SDoc -> a
pprPanic "getEqPredTys" (PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr PredType
ty)
getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
getEqPredTys_maybe :: PredType -> Maybe (Role, PredType, PredType)
getEqPredTys_maybe ty :: PredType
ty
= case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty of
Just (tc :: TyCon
tc, [_, _, ty1 :: PredType
ty1, ty2 :: PredType
ty2])
| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey -> (Role, PredType, PredType) -> Maybe (Role, PredType, PredType)
forall a. a -> Maybe a
Just (Role
Nominal, PredType
ty1, PredType
ty2)
| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey -> (Role, PredType, PredType) -> Maybe (Role, PredType, PredType)
forall a. a -> Maybe a
Just (Role
Representational, PredType
ty1, PredType
ty2)
_ -> Maybe (Role, PredType, PredType)
forall a. Maybe a
Nothing
getEqPredRole :: PredType -> Role
getEqPredRole :: PredType -> Role
getEqPredRole ty :: PredType
ty = EqRel -> Role
eqRelRole (PredType -> EqRel
predTypeEqRel PredType
ty)
predTypeEqRel :: PredType -> EqRel
predTypeEqRel :: PredType -> EqRel
predTypeEqRel ty :: PredType
ty
| Just (tc :: TyCon
tc, _) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty
, TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey
= EqRel
ReprEq
| Bool
otherwise
= EqRel
NomEq
isEvVarType :: Type -> Bool
isEvVarType :: PredType -> Bool
isEvVarType ty :: PredType
ty = PredType -> Bool
isCoVarType PredType
ty Bool -> Bool -> Bool
|| HasDebugCallStack => PredType -> Bool
PredType -> Bool
isPredTy PredType
ty
isEqPredClass :: Class -> Bool
isEqPredClass :: Class -> Bool
isEqPredClass cls :: Class
cls = Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey
Bool -> Bool -> Bool
|| Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
isClassPred, isEqPred, isEqPrimPred, isIPPred :: PredType -> Bool
isClassPred :: PredType -> Bool
isClassPred ty :: PredType
ty = case PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty of
Just tyCon :: TyCon
tyCon | TyCon -> Bool
isClassTyCon TyCon
tyCon -> Bool
True
_ -> Bool
False
isEqPred :: PredType -> Bool
isEqPred ty :: PredType
ty
| Just tc :: TyCon
tc <- PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty
, Just cls :: Class
cls <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
= Class -> Bool
isEqPredClass Class
cls
| Bool
otherwise
= Bool
False
isEqPrimPred :: PredType -> Bool
isEqPrimPred ty :: PredType
ty = PredType -> Bool
isCoVarType PredType
ty
isIPPred :: PredType -> Bool
isIPPred ty :: PredType
ty = case PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty of
Just tc :: TyCon
tc -> TyCon -> Bool
isIPTyCon TyCon
tc
_ -> Bool
False
isIPTyCon :: TyCon -> Bool
isIPTyCon :: TyCon -> Bool
isIPTyCon tc :: TyCon
tc = TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
ipClassKey
isIPClass :: Class -> Bool
isIPClass :: Class -> Bool
isIPClass cls :: Class
cls = Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
ipClassKey
isCTupleClass :: Class -> Bool
isCTupleClass :: Class -> Bool
isCTupleClass cls :: Class
cls = TyCon -> Bool
isTupleTyCon (Class -> TyCon
classTyCon Class
cls)
isIPPred_maybe :: Type -> Maybe (FastString, Type)
isIPPred_maybe :: PredType -> Maybe (FastString, PredType)
isIPPred_maybe ty :: PredType
ty =
do (tc :: TyCon
tc,[t1 :: PredType
t1,t2 :: PredType
t2]) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TyCon -> Bool
isIPTyCon TyCon
tc)
FastString
x <- PredType -> Maybe FastString
isStrLitTy PredType
t1
(FastString, PredType) -> Maybe (FastString, PredType)
forall (m :: * -> *) a. Monad m => a -> m a
return (FastString
x,PredType
t2)
hasIPPred :: PredType -> Bool
hasIPPred :: PredType -> Bool
hasIPPred pred :: PredType
pred
= case PredType -> Pred
classifyPredType PredType
pred of
ClassPred cls :: Class
cls tys :: [PredType]
tys
| Class -> Bool
isIPClass Class
cls -> Bool
True
| Class -> Bool
isCTupleClass Class
cls -> (PredType -> Bool) -> [PredType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any PredType -> Bool
hasIPPred [PredType]
tys
_other :: Pred
_other -> Bool
False
isEvVar :: Var -> Bool
isEvVar :: Var -> Bool
isEvVar var :: Var
var = PredType -> Bool
isEvVarType (Var -> PredType
varType Var
var)
isDictId :: Id -> Bool
isDictId :: Var -> Bool
isDictId id :: Var
id = PredType -> Bool
isDictTy (Var -> PredType
varType Var
id)