From 701797c3f724090508e06ded276723edfa431ab4 Mon Sep 17 00:00:00 2001 From: Tom Schrijvers Date: Fri, 11 May 2007 17:09:28 +0000 Subject: [PATCH] type family normalisation --- compiler/types/Coercion.lhs | 102 ++++++++++++++++++++++++++++++++++++++- compiler/types/FamInstEnv.lhs | 105 ++++++++++++++++++++++++++++++++++++++++- 2 files changed, 205 insertions(+), 2 deletions(-) diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 49ae740..98b5a07 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -31,7 +31,17 @@ module Coercion ( 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 @@ -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} + diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs index b8c82f8..d1a3445 100644 --- a/compiler/types/FamInstEnv.lhs +++ b/compiler/types/FamInstEnv.lhs @@ -14,7 +14,10 @@ module FamInstEnv ( extendFamInstEnv, extendFamInstEnvList, famInstEnvElts, familyInstances, - lookupFamInstEnv, lookupFamInstEnvUnify + lookupFamInstEnv, lookupFamInstEnvUnify, + + -- Normalisation + toplevelNormaliseFamInst ) where #include "HsVersions.h" @@ -24,7 +27,9 @@ import Unify import TcGadt import TcType import Type +import TypeRep import TyCon +import Coercion import VarSet import Var import Name @@ -32,6 +37,8 @@ import OccName import SrcLoc import UniqFM import Outputable +import Maybes +import Util import Maybe \end{code} @@ -310,3 +317,99 @@ lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem | otherwise = BindMe \end{code} + +-------------------------------------- +-- Normalisation + +\begin{code} + -- get rid of TOPLEVEL type functions by rewriting them + -- i.e. treating their equations as a TRS +toplevelNormaliseFamInst :: FamInstEnvs -> + Type -> + (CoercionI,Type) +toplevelNormaliseFamInst env ty + | Just ty' <- tcView ty = normaliseFamInst env ty' +toplevelNormaliseFamInst env ty@(TyConApp tyCon tys) + | isOpenTyCon tyCon + = normaliseFamInst env ty +toplevelNormaliseFamInst env ty + = (IdCo,ty) + + + -- get rid of ALL type functions by rewriting them + -- i.e. treating their equations as a TRS +normaliseFamInst :: FamInstEnvs -> -- environment with family instances + Type -> -- old type + (CoercionI,Type) -- (coercion,new type) +normaliseFamInst env ty + | Just ty' <- tcView ty = normaliseFamInst env ty' +normaliseFamInst env ty@(TyConApp tyCon tys) = + let (cois,ntys) = mapAndUnzip (normaliseFamInst env) tys + tycon_coi = mkTyConAppCoI tyCon ntys cois + maybe_ty_co = lookupFamInst env tyCon ntys + in case maybe_ty_co of + -- a matching family instance exists + Just (ty',co) -> + let first_coi = mkTransCoI tycon_coi (ACo co) + (rest_coi,nty) = normaliseFamInst env ty' + fix_coi = mkTransCoI first_coi rest_coi + in (fix_coi,nty) + -- no matching family instance exists + -- we do not do anything + Nothing -> + (tycon_coi,TyConApp tyCon ntys) +normaliseFamInst env ty@(AppTy ty1 ty2) = + let (coi1,nty1) = normaliseFamInst env ty1 + (coi2,nty2) = normaliseFamInst env ty2 + in (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2) +normaliseFamInst env ty@(FunTy ty1 ty2) = + let (coi1,nty1) = normaliseFamInst env ty1 + (coi2,nty2) = normaliseFamInst env ty2 + in (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2) +normaliseFamInst env ty@(ForAllTy tyvar ty1) = + let (coi,nty1) = normaliseFamInst env ty1 + in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1) +normaliseFamInst env ty@(NoteTy note ty1) = + let (coi,nty1) = normaliseFamInst env ty1 + in (mkNoteTyCoI note coi,NoteTy note nty1) +normaliseFamInst env ty@(TyVarTy _) = + (IdCo,ty) +normaliseFamInst env (PredTy predty) = + normaliseFamInstPred env predty + +normaliseFamInstPred :: FamInstEnvs -> PredType -> (CoercionI,Type) +normaliseFamInstPred env (ClassP cls tys) = + let (cois,tys') = mapAndUnzip (normaliseFamInst env) tys + in (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys') +normaliseFamInstPred env (IParam ipn ty) = + let (coi,ty') = normaliseFamInst env ty + in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty') +normaliseFamInstPred env (EqPred ty1 ty2) = + let (coi1,ty1') = normaliseFamInst env ty1 + (coi2,ty2') = normaliseFamInst env ty2 + in (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2') + +lookupFamInst :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Type,Coercion) + +-- (lookupFamInst F tys) looks for a top-level instance +-- co : forall a. F tys' = G a +-- (The rhs is always of form G a; see Note [The FamInst structure] +-- in FamInst.) +-- where we can instantiate 'a' with t to make tys'[t/a] = tys +-- Hence (co t) : F tys ~ G t +-- Then we return (Just (G t, co t)) + +lookupFamInst env tycon tys + | not (isOpenTyCon tycon) -- Dead code; fix. + = Nothing + | otherwise + = case lookupFamInstEnv env tycon tys of + [(subst, fam_inst)] -> + Just (mkTyConApp rep_tc substituted_vars, mkTyConApp coercion_tycon substituted_vars) + where -- NB: invariant of lookupFamInstEnv is that (tyConTyVars rep_tc) + -- is in the domain of the substitution + rep_tc = famInstTyCon fam_inst + coercion_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc) + substituted_vars = substTyVars subst (tyConTyVars rep_tc) + other -> Nothing +\end{code} -- 1.7.10.4