X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2FcoreSyn%2FCoreUtils.lhs;h=1bd0acd07de3604a8c56288a7370290d82e4f84e;hb=9621257fcd85a572a5c305b77995bda62689bb86;hp=9b581596d5d166f621fbd8c91dc5956b9a1ae2f3;hpb=ad0e3c1e2b5edc0b95252acd1c615faeec8b99dc;p=ghc-hetmet.git diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs index 9b58159..1bd0acd 100644 --- a/compiler/coreSyn/CoreUtils.lhs +++ b/compiler/coreSyn/CoreUtils.lhs @@ -31,7 +31,9 @@ module CoreUtils ( hashExpr, -- Equality - cheapEqExpr, tcEqExpr, tcEqExprX, applyTypeToArgs, applyTypeToArg + cheapEqExpr, tcEqExpr, tcEqExprX, applyTypeToArgs, applyTypeToArg, + + dataConInstPat, dataConOccInstPat ) where #include "HsVersions.h" @@ -42,10 +44,12 @@ import GLAEXTS -- For `xori` import CoreSyn import CoreFVs ( exprFreeVars ) import PprCore ( pprCoreExpr ) -import Var ( Var, TyVar ) +import Var ( Var, TyVar, CoVar, isCoVar, tyVarKind, setVarUnique, + mkCoVar, mkTyVar, mkCoVar ) +import OccName ( OccName, occNameFS, mkVarOcc ) import VarSet ( unionVarSet ) import VarEnv -import Name ( hashName ) +import Name ( hashName, mkSysTvName ) #if mingw32_TARGET_OS import Packages ( isDllName ) #endif @@ -53,7 +57,7 @@ import Literal ( hashLiteral, literalType, litIsDupable, litIsTrivial, isZeroLit, Literal( MachLabel ) ) import DataCon ( DataCon, dataConRepArity, isVanillaDataCon, dataConTyCon, dataConRepArgTys, - dataConUnivTyVars ) + dataConUnivTyVars, dataConExTyVars, dataConEqSpec ) import PrimOp ( PrimOp(..), primOpOkForSpeculation, primOpIsCheap ) import Id ( Id, idType, globalIdDetails, idNewStrictness, mkWildId, idArity, idName, idUnfolding, idInfo, @@ -67,11 +71,12 @@ import Type ( Type, mkFunTy, mkForAllTy, splitFunTy_maybe, applyTys, isUnLiftedType, seqType, mkTyVarTy, splitForAllTy_maybe, isForAllTy, splitRecNewType_maybe, splitTyConApp_maybe, coreEqType, funResultTy, applyTy, - substTyWith + substTyWith, mkPredTy ) import Coercion ( Coercion, mkTransCoercion, coercionKind, - splitRecNewTypeCo_maybe, mkSymCoercion, mkLeftCoercion, - mkRightCoercion, decomposeCo, coercionKindTyConApp ) + splitNewTypeRepCo_maybe, mkSymCoercion, mkLeftCoercion, + mkRightCoercion, decomposeCo, coercionKindPredTy, + splitCoercionKind, mkEqPred ) import TyCon ( tyConArity ) import TysWiredIn ( boolTy, trueDataCon, falseDataCon ) import CostCentre ( CostCentre ) @@ -82,6 +87,7 @@ import Outputable import DynFlags ( DynFlags, DynFlag(Opt_DictsCheap), dopt ) import TysPrim ( alphaTy ) -- Debugging only import Util ( equalLength, lengthAtLeast, foldl2 ) +import FastString ( mkFastString ) \end{code} @@ -214,7 +220,7 @@ mkCoerce co expr -- if to_ty `coreEqType` from_ty -- then expr -- else - ASSERT2(from_ty `coreEqType` (exprType expr), text "Trying to coerce" <+> text "(" <> ppr expr $$ text "::" <+> ppr (exprType expr) <> text ")" $$ ppr co $$ ppr (coercionKindTyConApp co)) + ASSERT2(from_ty `coreEqType` (exprType expr), text "Trying to coerce" <+> text "(" <> ppr expr $$ text "::" <+> ppr (exprType expr) <> text ")" $$ ppr co $$ ppr (coercionKindPredTy co)) (Cast expr co) \end{code} @@ -673,6 +679,96 @@ deepCast ty tyVars co -- coArgs = [right (left (left co)), right (left co), right co] coArgs = decomposeCo (length tyVars) co +-- This goes here to avoid circularity between DataCon and Id +dataConInstPat :: [Unique] -- A long enough list of uniques, at least one for each binder + -> DataCon + -> [Type] -- Types to instantiate the universally quantified tyvars + -> ([TyVar], [CoVar], [Id]) -- Return instantiated variables +-- dataConInstPat us con inst_tys returns a triple (ex_tvs, co_tvs, arg_ids), +-- +-- ex_tvs are intended to be used as binders for existential type args +-- +-- co_tvs are intended to be used as binders for coercion args and the kinds +-- of these vars have been instantiated by the inst_tys and the ex_tys +-- +-- arg_ids are indended to be used as binders for value arguments, including +-- dicts, and have their types instantiated with inst_tys and ex_tys +-- +-- Example. +-- The following constructor T1 +-- +-- data T a where +-- T1 :: forall b. Int -> b -> T(a,b) +-- ... +-- +-- has representation type +-- forall a. forall a1. forall a2. forall b. (a :=: (a1,a2)) => +-- Int -> b -> T a +-- +-- dataConInstPat us T1 (a1',a2') will return +-- +-- ([a1'', a2'', b''],[c :: (a1',a2'):=:(a1'',a2'')],[x :: Int,y :: b'']) +-- +-- where the double-primed variables are created from the unique list input +dataConInstPat uniqs con inst_tys + = dataConOccInstPat uniqs occs con inst_tys + where + -- dataConOccInstPat doesn't actually make use of the OccName directly for + -- existential and coercion variable binders, so it is right to just + -- use the VarName namespace for all of the OccNames + occs = mk_occs 1 + mk_occs n = mkVarOcc ("ipv" ++ show n) : mk_occs (n+1) + +dataConOccInstPat :: [Unique] -- A long enough list of uniques, at least one for each binder + -> [OccName] -- An equally long list of OccNames to use + -> DataCon + -> [Type] -- Types to instantiate the universally quantified tyvars + -> ([TyVar], [CoVar], [Id]) -- Return instantiated variables +-- This function actually does the job specified in the comment for +-- dataConInstPat, but uses the specified list of OccNames. This is +-- is necessary for use in e.g. tcIfaceDataAlt +dataConOccInstPat uniqs occs con inst_tys + = (ex_bndrs, co_bndrs, id_bndrs) + where + univ_tvs = dataConUnivTyVars con + ex_tvs = dataConExTyVars con + arg_tys = dataConRepArgTys con + eq_spec = dataConEqSpec con + eq_preds = [ mkEqPred (mkTyVarTy tv, ty) | (tv,ty) <- eq_spec ] + + n_ex = length ex_tvs + n_co = length eq_spec + n_id = length arg_tys + + -- split the Uniques and OccNames + (ex_uniqs, uniqs') = splitAt n_ex uniqs + (co_uniqs, id_uniqs) = splitAt n_co uniqs' + + (ex_occs, occs') = splitAt n_ex occs + (co_occs, id_occs) = splitAt n_co occs' + + -- make existential type variables + mk_ex_var uniq occ var = mkTyVar new_name kind + where + new_name = mkSysTvName uniq (occNameFS occ) + kind = tyVarKind var + + ex_bndrs = zipWith3 mk_ex_var ex_uniqs ex_occs ex_tvs + + -- make the instantiation substitution + inst_subst = substTyWith (univ_tvs ++ ex_tvs) (inst_tys ++ map mkTyVarTy ex_bndrs) + + -- make new coercion vars, instantiating kind + mk_co_var uniq occ eq_pred = mkCoVar new_name (inst_subst (mkPredTy eq_pred)) + where + new_name = mkSysTvName uniq (occNameFS occ) + + co_bndrs = zipWith3 mk_co_var co_uniqs co_occs eq_preds + + -- make value vars, instantiating types + mk_id_var uniq occ ty = mkUserLocal occ uniq (inst_subst ty) noSrcLoc + id_bndrs = zipWith3 mk_id_var id_uniqs id_occs arg_tys + exprIsConApp_maybe :: CoreExpr -> Maybe (DataCon, [CoreExpr]) -- Returns (Just (dc, [x1..xn])) if the argument expression is -- a constructor application of the form (dc x1 .. xn) @@ -687,30 +783,62 @@ exprIsConApp_maybe (Cast expr co) -- (# r, s #) -> ... -- where the memcpy is in the IO monad, but the call is in -- the (ST s) monad - let (from_ty, to_ty) = coercionKind co in case exprIsConApp_maybe expr of { Nothing -> Nothing ; Just (dc, args) -> + + let (from_ty, to_ty) = coercionKind co in case splitTyConApp_maybe to_ty of { Nothing -> Nothing ; Just (tc, tc_arg_tys) | tc /= dataConTyCon dc -> Nothing - | not (isVanillaDataCon dc) -> Nothing + -- | not (isVanillaDataCon dc) -> Nothing | otherwise -> - -- Type constructor must match - -- We knock out existentials to keep matters simple(r) + -- Type constructor must match datacon + + case splitTyConApp_maybe from_ty of { + Nothing -> Nothing ; + Just (tc', tc_arg_tys') | tc /= tc' -> Nothing + -- Both sides of coercion must have the same type constructor + | otherwise -> + let + -- here we do the PushC reduction rule as described in the FC paper arity = tyConArity tc - val_args = drop arity args + n_ex_tvs = length dc_ex_tyvars + + (univ_args, rest) = splitAt arity args + (ex_args, val_args) = splitAt n_ex_tvs rest + arg_tys = dataConRepArgTys dc dc_tyvars = dataConUnivTyVars dc + dc_ex_tyvars = dataConExTyVars dc + deep arg_ty = deepCast arg_ty dc_tyvars co + + -- first we appropriately cast the value arguments + arg_cos = map deep arg_tys new_val_args = zipWith mkCoerce (map deep arg_tys) val_args + + -- then we cast the existential coercion arguments + orig_tvs = dc_tyvars ++ dc_ex_tyvars + gammas = decomposeCo arity co + new_tys = gammas ++ (map (\ (Type t) -> t) ex_args) + theta = substTyWith orig_tvs new_tys + cast_ty tv (Type ty) + | isCoVar tv + , (ty1, ty2) <- splitCoercionKind (tyVarKind tv) + = Type $ mkTransCoercion (mkSymCoercion (theta ty1)) + (mkTransCoercion ty (theta ty2)) + | otherwise + = Type ty + new_ex_args = zipWith cast_ty dc_ex_tyvars ex_args + in ASSERT( all isTypeArg (take arity args) ) ASSERT( equalLength val_args arg_tys ) - Just (dc, map Type tc_arg_tys ++ new_val_args) - }} + Just (dc, map Type tc_arg_tys ++ new_ex_args ++ new_val_args) + }}} exprIsConApp_maybe (Note _ expr) = exprIsConApp_maybe expr @@ -1028,7 +1156,12 @@ eta_expand n us (Lam v body) ty eta_expand n us expr ty = ASSERT2 (exprType expr `coreEqType` ty, ppr (exprType expr) $$ ppr ty) case splitForAllTy_maybe ty of { - Just (tv,ty') -> Lam tv (eta_expand n us (App expr (Type (mkTyVarTy tv))) ty') + Just (tv,ty') -> + + Lam lam_tv (eta_expand n us2 (App expr (Type (mkTyVarTy lam_tv))) (substTyWith [tv] [mkTyVarTy lam_tv] ty')) + where + lam_tv = mkTyVar (mkSysTvName uniq FSLIT("etaT")) (tyVarKind tv) + (uniq:us2) = us ; Nothing -> @@ -1047,7 +1180,7 @@ eta_expand n us expr ty -- We want to get -- coerce T (\x::[T] -> (coerce ([T]->Int) e) x) - case splitRecNewTypeCo_maybe ty of { + case splitNewTypeRepCo_maybe ty of { Just(ty1,co) -> mkCoerce co (eta_expand n us (mkCoerce (mkSymCoercion co) expr) ty1) ; Nothing ->