Coercion,
mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind,
- coercionKind, coercionKinds, coercionKindPredTy,
+ coercionKind, coercionKinds, coercionKindPredTy, isIdentityCoercion,
-- ** Equality predicates
isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
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,
transCoercionTyCon, leftCoercionTyCon,
rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
+ -- ** Optimisation
+ optCoercion,
+
-- ** Comparison
coreEqCoercion,
-- * CoercionI
CoercionI(..),
- isIdentityCoercion,
+ isIdentityCoI,
mkSymCoI, mkTransCoI,
mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
mkForAllTyCoI,
import Class
import Var
import Name
-import OccName
import PrelNames
import Util
-import Unique
import BasicTypes
import Outputable
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]
-- | 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'
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)
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'
(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
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...
-- 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
-- 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
-- | 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
-- > 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
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}
projects / ghc-hetmet.git / blobdiff