X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FCoercion.lhs;h=a51ea266bb6f0761a9cf4a329f808717c12bc436;hb=8897e76874e10daa4dc695342e68b15e114a6de0;hp=d6b92fa29cfa3ae243aaf54fe0caf13dcbb3fc4c;hpb=1fa25d26f6bc9ab6def35b272405bad5bd23f6bf;p=ghc-hetmet.git diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index d6b92fa..a51ea26 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -22,7 +22,7 @@ module Coercion ( Coercion, mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind, - coercionKind, coercionKinds, coercionKindPredTy, + coercionKind, coercionKinds, coercionKindPredTy, isIdentityCoercion, -- ** Equality predicates isEqPred, mkEqPred, getEqPredTys, isEqPredTy, @@ -31,8 +31,8 @@ module Coercion ( mkCoercion, mkSymCoercion, mkTransCoercion, mkLeftCoercion, mkRightCoercion, mkRightCoercions, - mkInstCoercion, mkAppCoercion, - mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion, + mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion, + mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion, mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion, splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo, @@ -46,7 +46,7 @@ module Coercion ( -- * CoercionI CoercionI(..), - isIdentityCoercion, + isIdentityCoI, mkSymCoI, mkTransCoI, mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI, mkForAllTyCoI, @@ -74,14 +74,14 @@ import FastString -- | A 'Coercion' represents a 'Type' something should be coerced to. type Coercion = Type --- | A 'CoercionKind' is always of form @ty1 :=: ty2@ and indicates the +-- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the -- types that a 'Coercion' will work on. type CoercionKind = Kind ------------------------------ --- | This breaks a 'Coercion' with 'CoercionKind' @T A B C :=: T D E F@ into --- a list of 'Coercion's of kinds @A :=: D@, @B :=: E@ and @E :=: F@. Hence: +-- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into +-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence: -- -- > decomposeCo 3 c = [right (left (left c)), right (left c), right c] decomposeCo :: Arity -> Coercion -> [Coercion] @@ -134,7 +134,7 @@ splitCoercionKind_maybe _ = Nothing -- | If it is the case that -- --- > c :: (t1 :=: t2) +-- > c :: (t1 ~ t2) -- -- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@. -- See also 'coercionKindPredTy' @@ -184,6 +184,12 @@ coercionKinds :: [Coercion] -> ([Type], [Type]) coercionKinds tys = unzip $ map coercionKind tys ------------------------------------- +isIdentityCoercion :: Coercion -> Bool +isIdentityCoercion co + = case coercionKind co of + (t1,t2) -> t1 `coreEqType` t2 + +------------------------------------- -- Coercion kind and type mk's -- (make saturated TyConApp CoercionTyCon{...} args) @@ -194,36 +200,40 @@ mkCoercion :: TyCon -> [Type] -> Coercion mkCoercion coCon args = ASSERT( tyConArity coCon == length args ) TyConApp coCon args --- | Apply a 'Coercion' to another 'Coercion', which is presumably a 'Coercion' constructor of some --- kind +-- | Apply a 'Coercion' to another 'Coercion', which is presumably a +-- 'Coercion' constructor of some kind mkAppCoercion :: Coercion -> Coercion -> Coercion -mkAppCoercion co1 co2 = mkAppTy co1 co2 +mkAppCoercion co1 co2 = mkAppTy co1 co2 -- | Applies multiple 'Coercion's to another 'Coercion', from left to right. -- See also 'mkAppCoercion' mkAppsCoercion :: Coercion -> [Coercion] -> Coercion -mkAppsCoercion co1 tys = foldl mkAppTy co1 tys +mkAppsCoercion co1 tys = foldl mkAppTy co1 tys + +-- | Apply a type constructor to a list of coercions. +mkTyConCoercion :: TyCon -> [Coercion] -> Coercion +mkTyConCoercion con cos = mkTyConApp con cos + +-- | Make a function 'Coercion' between two other 'Coercion's +mkFunCoercion :: Coercion -> Coercion -> Coercion +mkFunCoercion co1 co2 = mkFunTy co1 co2 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion' mkForAllCoercion :: Var -> Coercion -> Coercion -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar) mkForAllCoercion tv co = ASSERT ( isTyVar tv ) mkForAllTy tv co --- | Make a function 'Coercion' between two other 'Coercion's -mkFunCoercion :: Coercion -> Coercion -> Coercion -mkFunCoercion co1 co2 = mkFunTy co1 co2 - ------------------------------- mkSymCoercion :: Coercion -> Coercion --- ^ Create a symmetric version of the given 'Coercion' that asserts equality between --- the same types but in the other "direction", so a kind of @t1 :=: t2@ becomes the --- kind @t2 :=: t1@. +-- ^ Create a symmetric version of the given 'Coercion' that asserts equality +-- between the same types but in the other "direction", so a kind of @t1 ~ t2@ +-- becomes the kind @t2 ~ t1@. -- --- This function attempts to simplify the generated 'Coercion' by removing redundant applications --- of @sym@. This is done by pushing this new @sym@ down into the 'Coercion' and exploiting the fact that --- @sym (sym co) = co@. +-- This function attempts to simplify the generated 'Coercion' by removing +-- redundant applications of @sym@. This is done by pushing this new @sym@ +-- down into the 'Coercion' and exploiting the fact that @sym (sym co) = co@. mkSymCoercion co | Just co' <- coreView co = mkSymCoercion co' @@ -405,7 +415,7 @@ mkNewTypeCoercion name tycon tvs rhs_ty (TyConApp tycon args, substTyWith tvs args rhs_ty) -- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type --- and its family instance. It has the form @Co tvs :: F ts :=: R tvs@, where @Co@ is +-- and its family instance. It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is -- the coercion tycon built here, @F@ the family tycon and @R@ the (derived) -- representation tycon. mkFamInstCoercion :: Name -- ^ Unique name for the coercion tycon @@ -420,7 +430,7 @@ mkFamInstCoercion name tvs family instTys rep_tycon coArity = length tvs rule args = (substTyWith tvs args $ -- with sigma = [tys/tvs], TyConApp family instTys, -- sigma (F ts) - TyConApp rep_tycon args) -- :=: R tys + TyConApp rep_tycon args) -- ~ R tys -------------------------------------- -- Coercion Type Constructors... @@ -478,7 +488,7 @@ splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type)) -- Helper for left and right. Finds coercion kind of its input and -- returns the left and right projections of the coercion... -- --- if c :: t1 s1 :=: t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2)) +-- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2)) splitCoercionKindOf co | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co) , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1 @@ -576,13 +586,17 @@ coreEqCoercion = coreEqType -- 2. The identity coercion data CoercionI = IdCo | ACo Coercion -isIdentityCoercion :: CoercionI -> Bool -isIdentityCoercion IdCo = True -isIdentityCoercion _ = False +instance Outputable CoercionI where + ppr IdCo = ptext (sLit "IdCo") + ppr (ACo co) = ppr co + +isIdentityCoI :: CoercionI -> Bool +isIdentityCoI IdCo = True +isIdentityCoI _ = False -- | Tests whether all the given 'CoercionI's represent the identity coercion -allIdCos :: [CoercionI] -> Bool -allIdCos = all isIdentityCoercion +allIdCoIs :: [CoercionI] -> Bool +allIdCoIs = all isIdentityCoI -- | For each 'CoercionI' in the input list, return either the 'Coercion' it -- contains or the corresponding 'Type' from the other list @@ -611,8 +625,8 @@ mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2 -- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion' mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI mkTyConAppCoI tyCon tys cois - | allIdCos cois = IdCo - | otherwise = ACo (TyConApp tyCon (zipCoArgs cois tys)) + | allIdCoIs cois = IdCo + | otherwise = ACo (TyConApp tyCon (zipCoArgs cois tys)) -- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion' mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI @@ -641,8 +655,8 @@ fromACo (ACo co) = co -- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois)) mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI mkClassPPredCoI cls tys cois - | allIdCos cois = IdCo - | otherwise = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys) + | allIdCoIs cois = IdCo + | otherwise = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys) -- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI' mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI