X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FCoercion.lhs;h=d78bc22f523cdb407dee0204abb2f425fe805759;hb=9f93fed1fafcf316f415cad5013acb18e41e9c29;hp=59a1a15c03607ebabbd3adf1f41df72ceed10903;hpb=5e5310b3cb4f78e30cc7b90879eb016e97c214cb;p=ghc-hetmet.git diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 59a1a15..d78bc22 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, @@ -41,12 +41,15 @@ module Coercion ( transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn + -- ** Optimisation + optCoercion, + -- ** Comparison coreEqCoercion, -- * CoercionI CoercionI(..), - isIdentityCoercion, + isIdentityCoI, mkSymCoI, mkTransCoI, mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI, mkForAllTyCoI, @@ -63,10 +66,8 @@ import TyCon import Class import Var import Name -import OccName import PrelNames import Util -import Unique import BasicTypes import Outputable import FastString @@ -184,6 +185,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 +201,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' @@ -576,13 +587,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 +626,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 +656,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 @@ -655,3 +670,97 @@ mkEqPredCoI _ IdCo _ IdCo = IdCo mkEqPredCoI ty1 IdCo _ (ACo co2) = ACo $ PredTy $ EqPred ty1 co2 mkEqPredCoI _ (ACo co1) ty2 coi2 = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2) \end{code} + +%************************************************************************ +%* * + Optimising coercions +%* * +%************************************************************************ + +\begin{code} +optCoercion :: Coercion -> Coercion +optCoercion co = co +{- + = pprTrace "optCoercion" (ppr co $$ ppr (coercionKind co)) $ + ASSERT2( coercionKind co `eq` coercionKind result, ppr co $$ ppr result ) + result + where + (s1,t1) `eq` (s2,t2) = s1 `coreEqType` s2 && t1 `coreEqType` t2 + + (result,_,_) = go co + -- optimized, changed?, identity? + go :: Coercion -> ( Coercion, Bool, Bool ) + -- traverse coercion term bottom up and return + -- + -- 1) equivalent coercion, in optimized form + -- + -- 2) whether the output coercion differs from + -- the input coercion + -- + -- 3) whether the coercion is an identity coercion + -- + -- Performs the following optimizations: + -- + -- sym id >-> id + -- trans id co >-> co + -- trans co id >-> co + -- + go ty@(TyVarTy a) | isCoVar a = let (ty1,ty2) = coercionKind ty + in (ty, False, ty1 `coreEqType` ty2) + | otherwise = (ty, False, True) + go ty@(AppTy ty1 ty2) + = let (ty1', chan1, id1) = go ty1 + (ty2', chan2, id2) = go ty2 + in if chan1 || chan2 + then (AppTy ty1' ty2', True, id1 && id2) + else (ty , False, id1 && id2) + go ty@(TyConApp tc args) + | tc == symCoercionTyCon, [ty1] <- args + = case go ty1 of + (ty1', _ , True) -> (ty1', True, True) + (ty1', True, _ ) -> (TyConApp tc [ty1'], True, False) + (_ , _ , _ ) -> (ty, False, False) + | tc == transCoercionTyCon, [ty1,ty2] <- args + = let (ty1', chan1, id1) = go ty1 + (ty2', chan2, id2) = go ty2 + in if id1 + then (ty2', True, id2) + else if id2 + then (ty1', True, False) + else if chan1 || chan2 + then (TyConApp tc [ty1',ty2'], True , False) + else (ty , False, False) + | otherwise + = let (args', chans, ids) = mapAndUnzip3 go args + in if or chans + then (TyConApp tc args', True , and ids) + else (ty , False, and ids) + go ty@(FunTy ty1 ty2) + = let (ty1',chan1,id1) = go ty1 + (ty2',chan2,id2) = go ty2 + in if chan1 || chan2 + then (FunTy ty1' ty2', True , id1 && id2) + else (ty , False, id1 && id2) + go ty@(ForAllTy tv ty1) + = let (ty1', chan1, id1) = go ty1 + in if chan1 + then (ForAllTy tv ty1', True , id1) + else (ty , False, id1) + go ty@(PredTy (EqPred ty1 ty2)) + = let (ty1', chan1, id1) = go ty1 + (ty2', chan2, id2) = go ty2 + in if chan1 || chan2 + then (PredTy (EqPred ty1' ty2'), True , id1 && id2) + else (ty , False, id1 && id2) + go ty@(PredTy (ClassP cl args)) + = let (args', chans, ids) = mapAndUnzip3 go args + in if or chans + then (PredTy (ClassP cl args'), True , and ids) + else (ty , False, and ids) + go ty@(PredTy (IParam name ty1)) + = let (ty1', chan1, id1) = go ty1 + in if chan1 + then (PredTy (IParam name ty1'), True , id1) + else (ty , False, id1) +-} +\end{code}