X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FCoercion.lhs;h=1e071ebd17c1e233c8ee188df74a5c4ac21f6694;hb=87b3c589498941332029a8a9da35e94a6139f0eb;hp=b9c6ea7fae77733d6c7c9b14454615e8ec1ee315;hpb=77241a03e4c0c56b35c63a303b96933232ecd083;p=ghc-hetmet.git diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index b9c6ea7..1e071eb 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -25,13 +25,23 @@ module Coercion ( mkSymCoercion, mkTransCoercion, mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion, mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion, - mkNewTypeCoercion, mkDataInstCoercion, mkAppsCoercion, + mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion, splitNewTypeRepCo_maybe, decomposeCo, unsafeCoercionTyCon, symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, - rightCoercionTyCon, instCoercionTyCon -- needed by TysWiredIn + rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn + + -- CoercionI + CoercionI(..), + isIdentityCoercion, + mkSymCoI, mkTransCoI, + mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI, + mkNoteTyCoI, mkForAllTyCoI, + fromCoI, + mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI, + ) where #include "HsVersions.h" @@ -39,6 +49,7 @@ module Coercion ( import TypeRep import Type import TyCon +import Class import Var import Name import OccName @@ -294,18 +305,18 @@ mkNewTypeCoercion name tycon tvs rhs_ty rule args = ASSERT( co_con_arity == length args ) (TyConApp tycon args, substTyWith tvs args rhs_ty) --- Coercion identifying a data/newtype representation type 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) +-- Coercion identifying a data/newtype/synonym representation type 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. -- -mkDataInstCoercion :: Name -- unique name for the coercion tycon - -> [TyVar] -- type parameters of the coercion (`tvs') - -> TyCon -- family tycon (`F') - -> [Type] -- type instance (`ts') - -> TyCon -- representation tycon (`R') - -> TyCon -- => coercion tycon (`Co') -mkDataInstCoercion name tvs family instTys rep_tycon +mkFamInstCoercion :: Name -- unique name for the coercion tycon + -> [TyVar] -- type parameters of the coercion (`tvs') + -> TyCon -- family tycon (`F') + -> [Type] -- type instance (`ts') + -> TyCon -- representation tycon (`R') + -> TyCon -- => coercion tycon (`Co') +mkFamInstCoercion name tvs family instTys rep_tycon = mkCoercionTyCon name coArity rule where coArity = length tvs @@ -421,3 +432,92 @@ splitNewTypeRepCo_maybe (TyConApp tc tys) co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo_maybe tc) splitNewTypeRepCo_maybe other = Nothing \end{code} + + +-------------------------------------- +-- CoercionI smart constructors +-- lifted smart constructors of ordinary coercions + + +\begin{code} + + -- CoercionI is either + -- (a) proper coercion + -- (b) the identity coercion +data CoercionI = IdCo | ACo Coercion + +isIdentityCoercion :: CoercionI -> Bool +isIdentityCoercion IdCo = True +isIdentityCoercion _ = False + +mkSymCoI :: CoercionI -> CoercionI +mkSymCoI IdCo = IdCo +mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co] + -- the smart constructor + -- is too smart with tyvars + +mkTransCoI :: CoercionI -> CoercionI -> CoercionI +mkTransCoI IdCo aco = aco +mkTransCoI aco IdCo = aco +mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2 + +mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI +mkTyConAppCoI tyCon tys cois = + let (anyAcon,co_args) = f tys cois + in if anyAcon + then ACo (TyConApp tyCon co_args) + else IdCo + where + f [] [] = (False,[]) + f (x:xs) (y:ys) = + let (b,cos) = f xs ys + in case y of + IdCo -> (b,x:cos) + ACo co -> (True,co:cos) + +mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI +mkAppTyCoI ty1 IdCo ty2 IdCo = IdCo +mkAppTyCoI ty1 coi1 ty2 coi2 = + ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2) + +mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI +mkFunTyCoI ty1 IdCo ty2 IdCo = IdCo +mkFunTyCoI ty1 coi1 ty2 coi2 = + ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2) + +mkNoteTyCoI :: TyNote -> CoercionI -> CoercionI +mkNoteTyCoI _ IdCo = IdCo +mkNoteTyCoI note (ACo co) = ACo $ NoteTy note co + +mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI +mkForAllTyCoI _ IdCo = IdCo +mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co + +fromCoI IdCo ty = ty +fromCoI (ACo co) ty = co + +mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI +mkClassPPredCoI cls tys cois = + let (anyAcon,co_args) = f tys cois + in if anyAcon + then ACo $ PredTy $ ClassP cls co_args + else IdCo + where + f [] [] = (False,[]) + f (x:xs) (y:ys) = + let (b,cos) = f xs ys + in case y of + IdCo -> (b,x:cos) + ACo co -> (True,co:cos) + +mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI +mkIParamPredCoI ipn IdCo = IdCo +mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co + +mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI +mkEqPredCoI _ IdCo _ IdCo = IdCo +mkEqPredCoI ty1 IdCo _ (ACo co2) = ACo $ PredTy $ EqPred ty1 co2 +mkEqPredCoI ty1 (ACo co1) ty2 coi2 = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2) + +\end{code} +