hashExpr,
-- Equality
- cheapEqExpr, tcEqExpr, tcEqExprX, applyTypeToArgs, applyTypeToArg
+ cheapEqExpr, tcEqExpr, tcEqExprX, applyTypeToArgs, applyTypeToArg,
+
+ dataConInstPat
) where
#include "HsVersions.h"
import CoreSyn
import CoreFVs ( exprFreeVars )
import PprCore ( pprCoreExpr )
-import Var ( Var, TyVar )
+import Var ( Var, TyVar, CoVar, isCoVar, tyVarKind, setVarUnique,
+ mkCoVar, mkTyVar, mkCoVar )
import VarSet ( unionVarSet )
import VarEnv
-import Name ( hashName )
+import Name ( hashName, mkSysTvName )
#if mingw32_TARGET_OS
import Packages ( isDllName )
#endif
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,
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 )
-- 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}
-- 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] -- An infinite list of uniques
+ -> DataCon
+ -> [Type] -- Types to instantiate the universally quantified tyvars
+ -> ([TyVar], [CoVar], [Id]) -- Return instantiated variables
+dataConInstPat uniqs 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
+ (ex_uniqs, uniqs') = splitAt n_ex uniqs
+ (co_uniqs, id_uniqs) = splitAt n_co uniqs'
+
+ -- make existential type variables
+ mk_ex_var uniq var = setVarUnique var uniq
+ ex_bndrs = zipWith mk_ex_var ex_uniqs ex_tvs
+
+ -- make the instantiation substitution
+ inst_subst = substTyWith (univ_tvs ++ ex_tvs) (inst_tys ++ map mkTyVarTy ex_bndrs)
+
+ -- make a new coercion vars, instantiating kind
+ mk_co_var uniq eq_pred = mkCoVar new_name (inst_subst (mkPredTy eq_pred))
+ where
+ new_name = mkSysTvName uniq FSLIT("co")
+
+ co_bndrs = zipWith mk_co_var co_uniqs eq_preds
+
+ -- make value vars, instantiating types
+ mk_id_var uniq ty = mkSysLocal FSLIT("ca") uniq (inst_subst ty)
+
+ id_bndrs = zipWith mk_id_var id_uniqs 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)
-- (# 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
-- 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 ->
projects / ghc-hetmet.git / blobdiff