diff options
Diffstat (limited to 'compiler/coreSyn')
| -rw-r--r-- | compiler/coreSyn/CoreArity.lhs | 42 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreFVs.lhs | 24 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreLint.lhs | 440 | ||||
| -rw-r--r-- | compiler/coreSyn/CorePrep.lhs | 37 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreSubst.lhs | 259 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreSyn.lhs | 64 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreTidy.lhs | 9 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreUnfold.lhs | 48 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreUtils.lhs | 239 | ||||
| -rw-r--r-- | compiler/coreSyn/ExternalCore.lhs | 13 | ||||
| -rw-r--r-- | compiler/coreSyn/MkCore.lhs | 10 | ||||
| -rw-r--r-- | compiler/coreSyn/MkExternalCore.lhs | 54 | ||||
| -rw-r--r-- | compiler/coreSyn/PprCore.lhs | 16 | ||||
| -rw-r--r-- | compiler/coreSyn/PprExternalCore.lhs | 6 |
14 files changed, 674 insertions, 587 deletions
diff --git a/compiler/coreSyn/CoreArity.lhs b/compiler/coreSyn/CoreArity.lhs index 678c961c18..0fa1c381e9 100644 --- a/compiler/coreSyn/CoreArity.lhs +++ b/compiler/coreSyn/CoreArity.lhs @@ -29,6 +29,7 @@ import BasicTypes import Unique import Outputable import FastString +import Pair \end{code} %************************************************************************ @@ -79,11 +80,13 @@ exprArity e = go e go (Lam x e) | isId x = go e + 1 | otherwise = go e go (Note n e) | notSccNote n = go e - go (Cast e co) = go e `min` length (typeArity (snd (coercionKind co))) - -- Note [exprArity invariant] + go (Cast e co) = go e `min` length (typeArity (pSnd (coercionKind co))) + -- Note [exprArity invariant] go (App e (Type _)) = go e go (App f a) | exprIsTrivial a = (go f - 1) `max` 0 -- See Note [exprArity for applications] + -- NB: coercions count as a value argument + go _ = 0 @@ -549,7 +552,7 @@ arityType cheap_fn (Lam x e) | isId x = arityLam x (arityType cheap_fn e) | otherwise = arityType cheap_fn e - -- Applications; decrease arity + -- Applications; decrease arity, except for types arityType cheap_fn (App fun (Type _)) = arityType cheap_fn fun arityType cheap_fn (App fun arg ) @@ -663,14 +666,14 @@ etaExpand n orig_expr -- Strip off existing lambdas and casts -- Note [Eta expansion and SCCs] go 0 expr = expr - go n (Lam v body) | isTyCoVar v = Lam v (go n body) - | otherwise = Lam v (go (n-1) body) + go n (Lam v body) | isTyVar v = Lam v (go n body) + | otherwise = Lam v (go (n-1) body) go n (Cast expr co) = Cast (go n expr) co go n expr = -- pprTrace "ee" (vcat [ppr orig_expr, ppr expr, ppr etas]) $ etaInfoAbs etas (etaInfoApp subst' expr etas) where in_scope = mkInScopeSet (exprFreeVars expr) - (in_scope', etas) = mkEtaWW n in_scope (exprType expr) + (in_scope', etas) = mkEtaWW n orig_expr in_scope (exprType expr) subst' = mkEmptySubst in_scope' -- Wrapper Unwrapper @@ -685,10 +688,10 @@ instance Outputable EtaInfo where pushCoercion :: Coercion -> [EtaInfo] -> [EtaInfo] pushCoercion co1 (EtaCo co2 : eis) - | isIdentityCoercion co = eis - | otherwise = EtaCo co : eis + | isReflCo co = eis + | otherwise = EtaCo co : eis where - co = co1 `mkTransCoercion` co2 + co = co1 `mkTransCo` co2 pushCoercion co eis = EtaCo co : eis @@ -696,7 +699,7 @@ pushCoercion co eis = EtaCo co : eis etaInfoAbs :: [EtaInfo] -> CoreExpr -> CoreExpr etaInfoAbs [] expr = expr etaInfoAbs (EtaVar v : eis) expr = Lam v (etaInfoAbs eis expr) -etaInfoAbs (EtaCo co : eis) expr = Cast (etaInfoAbs eis expr) (mkSymCoercion co) +etaInfoAbs (EtaCo co : eis) expr = Cast (etaInfoAbs eis expr) (mkSymCo co) -------------- etaInfoApp :: Subst -> CoreExpr -> [EtaInfo] -> CoreExpr @@ -704,15 +707,12 @@ etaInfoApp :: Subst -> CoreExpr -> [EtaInfo] -> CoreExpr -- ((substExpr s e) `appliedto` eis) etaInfoApp subst (Lam v1 e) (EtaVar v2 : eis) - = etaInfoApp subst' e eis - where - subst' | isTyCoVar v1 = CoreSubst.extendTvSubst subst v1 (mkTyVarTy v2) - | otherwise = CoreSubst.extendIdSubst subst v1 (Var v2) + = etaInfoApp (CoreSubst.extendSubstWithVar subst v1 v2) e eis etaInfoApp subst (Cast e co1) eis = etaInfoApp subst e (pushCoercion co' eis) where - co' = CoreSubst.substTy subst co1 + co' = CoreSubst.substCo subst co1 etaInfoApp subst (Case e b _ alts) eis = Case (subst_expr subst e) b1 (coreAltsType alts') alts' @@ -739,24 +739,24 @@ etaInfoApp subst e eis go e (EtaCo co : eis) = go (Cast e co) eis -------------- -mkEtaWW :: Arity -> InScopeSet -> Type +mkEtaWW :: Arity -> CoreExpr -> InScopeSet -> Type -> (InScopeSet, [EtaInfo]) -- EtaInfo contains fresh variables, -- not free in the incoming CoreExpr -- Outgoing InScopeSet includes the EtaInfo vars -- and the original free vars -mkEtaWW orig_n in_scope orig_ty +mkEtaWW orig_n orig_expr in_scope orig_ty = go orig_n empty_subst orig_ty [] where - empty_subst = mkTvSubst in_scope emptyTvSubstEnv + empty_subst = TvSubst in_scope emptyTvSubstEnv go n subst ty eis -- See Note [exprArity invariant] | n == 0 = (getTvInScope subst, reverse eis) | Just (tv,ty') <- splitForAllTy_maybe ty - , let (subst', tv') = substTyVarBndr subst tv + , let (subst', tv') = Type.substTyVarBndr subst tv -- Avoid free vars of the original expression = go n subst' ty' (EtaVar tv' : eis) @@ -772,11 +772,11 @@ mkEtaWW orig_n in_scope orig_ty -- eta_expand 1 e T -- We want to get -- coerce T (\x::[T] -> (coerce ([T]->Int) e) x) - go n subst ty' (EtaCo (Type.substTy subst co) : eis) + go n subst ty' (EtaCo co : eis) | otherwise -- We have an expression of arity > 0, -- but its type isn't a function. - = WARN( True, ppr orig_n <+> ppr orig_ty ) + = WARN( True, (ppr orig_n <+> ppr orig_ty) $$ ppr orig_expr ) (getTvInScope subst, reverse eis) -- This *can* legitmately happen: -- e.g. coerce Int (\x. x) Essentially the programmer is diff --git a/compiler/coreSyn/CoreFVs.lhs b/compiler/coreSyn/CoreFVs.lhs index af414f7550..88509f90f3 100644 --- a/compiler/coreSyn/CoreFVs.lhs +++ b/compiler/coreSyn/CoreFVs.lhs @@ -49,6 +49,7 @@ import Name import VarSet import Var import TcType +import Coercion import Util import BasicTypes( Activation ) import Outputable @@ -179,12 +180,13 @@ addBndrs bndrs fv = foldr addBndr fv bndrs expr_fvs :: CoreExpr -> FV expr_fvs (Type ty) = someVars (tyVarsOfType ty) +expr_fvs (Coercion co) = someVars (tyCoVarsOfCo co) expr_fvs (Var var) = oneVar var expr_fvs (Lit _) = noVars expr_fvs (Note _ expr) = expr_fvs expr expr_fvs (App fun arg) = expr_fvs fun `union` expr_fvs arg expr_fvs (Lam bndr body) = addBndr bndr (expr_fvs body) -expr_fvs (Cast expr co) = expr_fvs expr `union` someVars (tyVarsOfType co) +expr_fvs (Cast expr co) = expr_fvs expr `union` someVars (tyCoVarsOfCo co) expr_fvs (Case scrut bndr ty alts) = expr_fvs scrut `union` someVars (tyVarsOfType ty) `union` addBndr bndr @@ -248,10 +250,11 @@ exprOrphNames e where n = idName v go (Lit _) = emptyNameSet go (Type ty) = orphNamesOfType ty -- Don't need free tyvars + go (Coercion co) = orphNamesOfCo co go (App e1 e2) = go e1 `unionNameSets` go e2 go (Lam v e) = go e `delFromNameSet` idName v go (Note _ e) = go e - go (Cast e co) = go e `unionNameSets` orphNamesOfType co + go (Cast e co) = go e `unionNameSets` orphNamesOfCo co go (Let (NonRec _ r) e) = go e `unionNameSets` go r go (Let (Rec prs) e) = exprsOrphNames (map snd prs) `unionNameSets` go e go (Case e _ ty as) = go e `unionNameSets` orphNamesOfType ty @@ -392,15 +395,15 @@ varTypeTyVars :: Var -> TyVarSet -- Find the type variables free in the type of the variable -- Remember, coercion variables can mention type variables... varTypeTyVars var - | isLocalId var || isCoVar var = tyVarsOfType (idType var) - | otherwise = emptyVarSet -- Global Ids and non-coercion TyVars + | isLocalId var = tyVarsOfType (idType var) + | otherwise = emptyVarSet -- Global Ids and non-coercion TyVars varTypeTcTyVars :: Var -> TyVarSet -- Find the type variables free in the type of the variable -- Remember, coercion variables can mention type variables... varTypeTcTyVars var - | isLocalId var || isCoVar var = tcTyVarsOfType (idType var) - | otherwise = emptyVarSet -- Global Ids and non-coercion TyVars + | isLocalId var = tcTyVarsOfType (idType var) + | otherwise = emptyVarSet -- Global Ids and non-coercion TyVars idFreeVars :: Id -> VarSet -- Type variables, rule variables, and inline variables @@ -411,7 +414,7 @@ idFreeVars id = ASSERT( isId id) bndrRuleAndUnfoldingVars ::Var -> VarSet -- A 'let' can bind a type variable, and idRuleVars assumes -- it's seeing an Id. This function tests first. -bndrRuleAndUnfoldingVars v | isTyCoVar v = emptyVarSet +bndrRuleAndUnfoldingVars v | isTyVar v = emptyVarSet | otherwise = idRuleAndUnfoldingVars v idRuleAndUnfoldingVars :: Id -> VarSet @@ -510,12 +513,11 @@ freeVars (Let (Rec binds) body) body2 = freeVars body body_fvs = freeVarsOf body2 - freeVars (Cast expr co) - = (freeVarsOf expr2 `unionFVs` cfvs, AnnCast expr2 co) + = (freeVarsOf expr2 `unionFVs` cfvs, AnnCast expr2 (cfvs, co)) where expr2 = freeVars expr - cfvs = tyVarsOfType co + cfvs = tyCoVarsOfCo co freeVars (Note other_note expr) = (freeVarsOf expr2, AnnNote other_note expr2) @@ -523,5 +525,7 @@ freeVars (Note other_note expr) expr2 = freeVars expr freeVars (Type ty) = (tyVarsOfType ty, AnnType ty) + +freeVars (Coercion co) = (tyCoVarsOfCo co, AnnCoercion co) \end{code} diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs index 5cc82a2ae2..031fd613cc 100644 --- a/compiler/coreSyn/CoreLint.lhs +++ b/compiler/coreSyn/CoreLint.lhs @@ -15,6 +15,7 @@ import Demand import CoreSyn import CoreFVs import CoreUtils +import Pair import Bag import Literal import DataCon @@ -27,6 +28,7 @@ import Id import PprCore import ErrUtils import SrcLoc +import Kind import Type import TypeRep import Coercion @@ -41,6 +43,7 @@ import FastString import Util import Control.Monad import Data.Maybe +import Data.Traversable (traverse) \end{code} %************************************************************************ @@ -166,7 +169,7 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs) -- Check the rhs do { ty <- lintCoreExpr rhs ; lintBinder binder -- Check match to RHS type - ; binder_ty <- applySubst binder_ty + ; binder_ty <- applySubstTy binder_ty ; checkTys binder_ty ty (mkRhsMsg binder ty) -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples) ; checkL (not (isUnLiftedType binder_ty) @@ -207,14 +210,15 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs) %************************************************************************ \begin{code} -type InType = Type -- Substitution not yet applied -type InVar = Var -type InTyVar = TyVar +type InType = Type -- Substitution not yet applied +type InCoercion = Coercion +type InVar = Var +type InTyVar = TyVar -type OutType = Type -- Substitution has been applied to this -type OutVar = Var -type OutTyVar = TyVar -type OutCoVar = CoVar +type OutType = Type -- Substitution has been applied to this +type OutCoercion = Coercion +type OutVar = Var +type OutTyVar = TyVar lintCoreExpr :: CoreExpr -> LintM OutType -- The returned type has the substitution from the monad @@ -227,6 +231,9 @@ lintCoreExpr (Var var) = do { checkL (not (var == oneTupleDataConId)) (ptext (sLit "Illegal one-tuple")) + ; checkL (isId var && not (isCoVar var)) + (ptext (sLit "Non term variable") <+> ppr var) + ; checkDeadIdOcc var ; var' <- lookupIdInScope var ; return (idType var') } @@ -236,7 +243,7 @@ lintCoreExpr (Lit lit) lintCoreExpr (Cast expr co) = do { expr_ty <- lintCoreExpr expr - ; co' <- applySubst co + ; co' <- applySubstCo co ; (from_ty, to_ty) <- lintCoercion co' ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty) ; return to_ty } @@ -251,29 +258,20 @@ lintCoreExpr (Let (NonRec tv (Type ty)) body) ; lintTyBndr tv $ \ tv' -> addLoc (BodyOfLetRec [tv]) $ extendSubstL tv' ty' $ do - { checkKinds tv' ty' + { checkTyKind tv' ty' -- Now extend the substitution so we -- take advantage of it in the body ; lintCoreExpr body } } - | isCoVar tv - = do { co <- applySubst ty - ; (s1,s2) <- addLoc (RhsOf tv) $ lintCoercion co - ; lintTyBndr tv $ \ tv' -> - addLoc (BodyOfLetRec [tv]) $ do - { let (t1,t2) = coVarKind tv' - ; checkTys s1 t1 (mkTyVarLetErr tv ty) - ; checkTys s2 t2 (mkTyVarLetErr tv ty) - ; lintCoreExpr body } } - - | otherwise - = failWithL (mkTyVarLetErr tv ty) -- Not quite accurate - lintCoreExpr (Let (NonRec bndr rhs) body) + | isId bndr = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs) - ; addLoc (BodyOfLetRec [bndr]) + ; addLoc (BodyOfLetRec [bndr]) (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) } + | otherwise + = failWithL (mkLetErr bndr rhs) -- Not quite accurate + lintCoreExpr (Let (Rec pairs) body) = lintAndScopeIds bndrs $ \_ -> do { checkL (null dups) (dupVars dups) @@ -298,7 +296,7 @@ lintCoreExpr (Lam var expr) else return (mkForAllTy var' body_ty) } - -- The applySubst is needed to apply the subst to var + -- The applySubstTy is needed to apply the subst to var lintCoreExpr e@(Case scrut var alt_ty alts) = -- Check the scrutinee @@ -338,6 +336,11 @@ lintCoreExpr e@(Case scrut var alt_ty alts) = lintCoreExpr (Type ty) = do { ty' <- lintInTy ty ; return (typeKind ty') } + +lintCoreExpr (Coercion co) + = do { co' <- lintInCo co + ; let Pair ty1 ty2 = coercionKind co' + ; return (mkPredTy $ EqPred ty1 ty2) } \end{code} %************************************************************************ @@ -352,12 +355,12 @@ subtype of the required type, as one would expect. \begin{code} lintCoreArg :: OutType -> CoreArg -> LintM OutType lintCoreArg fun_ty (Type arg_ty) - = do { arg_ty' <- applySubst arg_ty - ; lintTyApp fun_ty arg_ty' } + = do { arg_ty' <- applySubstTy arg_ty + ; lintTyApp fun_ty arg_ty' } lintCoreArg fun_ty arg - = do { arg_ty <- lintCoreExpr arg - ; lintValApp arg fun_ty arg_ty } + = do { arg_ty <- lintCoreExpr arg + ; lintValApp arg fun_ty arg_ty } ----------------- lintAltBinders :: OutType -- Scrutinee type @@ -367,7 +370,7 @@ lintAltBinders :: OutType -- Scrutinee type lintAltBinders scrut_ty con_ty [] = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty) lintAltBinders scrut_ty con_ty (bndr:bndrs) - | isTyCoVar bndr + | isTyVar bndr = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr) ; lintAltBinders scrut_ty con_ty' bndrs } | otherwise @@ -378,11 +381,10 @@ lintAltBinders scrut_ty con_ty (bndr:bndrs) lintTyApp :: OutType -> OutType -> LintM OutType lintTyApp fun_ty arg_ty | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty - = do { checkKinds tyvar arg_ty - ; if isCoVar tyvar then - return body_ty -- Co-vars don't appear in body_ty! - else - return (substTyWith [tyvar] [arg_ty] body_ty) } + , isTyVar tyvar + = do { checkTyKind tyvar arg_ty + ; return (substTyWith [tyvar] [arg_ty] body_ty) } + | otherwise = failWithL (mkTyAppMsg fun_ty arg_ty) @@ -400,22 +402,34 @@ lintValApp arg fun_ty arg_ty \end{code} \begin{code} -checkKinds :: OutVar -> OutType -> LintM () +checkTyKind :: OutTyVar -> OutType -> LintM () -- Both args have had substitution applied -checkKinds tyvar arg_ty +checkTyKind tyvar arg_ty -- Arg type might be boxed for a function with an uncommitted -- tyvar; notably this is used so that we can give -- error :: forall a:*. String -> a -- and then apply it to both boxed and unboxed types. - | isCoVar tyvar = do { (s2,t2) <- lintCoercion arg_ty - ; unless (s1 `coreEqType` s2 && t1 `coreEqType` t2) - (addErrL (mkCoAppErrMsg tyvar arg_ty)) } - | otherwise = do { arg_kind <- lintType arg_ty - ; unless (arg_kind `isSubKind` tyvar_kind) - (addErrL (mkKindErrMsg tyvar arg_ty)) } + = do { arg_kind <- lintType arg_ty + ; unless (arg_kind `isSubKind` tyvar_kind) + (addErrL (mkKindErrMsg tyvar arg_ty)) } where tyvar_kind = tyVarKind tyvar - (s1,t1) = coVarKind tyvar + +-- Check that the kinds of a type variable and a coercion match, that +-- is, if tv :: k then co :: t1 ~ t2 where t1 :: k and t2 :: k. +checkTyCoKind :: TyVar -> OutCoercion -> LintM (OutType, OutType) +checkTyCoKind tv co + = do { (t1,t2) <- lintCoercion co + ; k1 <- lintType t1 + ; k2 <- lintType t2 + ; unless ((k1 `isSubKind` tyvar_kind) && (k2 `isSubKind` tyvar_kind)) + (addErrL (mkTyCoAppErrMsg tv co)) + ; return (t1,t2) } + where + tyvar_kind = tyVarKind tv + +checkTyCoKinds :: [TyVar] -> [OutCoercion] -> LintM [(OutType, OutType)] +checkTyCoKinds = zipWithM checkTyCoKind checkDeadIdOcc :: Id -> LintM () -- Occurrences of an Id should never be dead.... @@ -536,7 +550,7 @@ lintBinder var linterF lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a lintTyBndr tv thing_inside = do { subst <- getTvSubst - ; let (subst', tv') = substTyVarBndr subst tv + ; let (subst', tv') = Type.substTyVarBndr subst tv ; lintTyBndrKind tv' ; updateTvSubst subst' (thing_inside tv') } @@ -581,10 +595,19 @@ lintInTy :: InType -> LintM OutType -- ToDo: check the kind structure of the type lintInTy ty = addLoc (InType ty) $ - do { ty' <- applySubst ty + do { ty' <- applySubstTy ty ; _ <- lintType ty' ; return ty' } +lintInCo :: InCoercion -> LintM OutCoercion +-- Check the coercion, and apply the substitution to it +-- See Note [Linting type lets] +lintInCo co + = addLoc (InCo co) $ + do { co' <- applySubstCo co + ; _ <- lintCoercion co' + ; return co' } + ------------------- lintKind :: Kind -> LintM () -- Check well-formedness of kinds: *, *->*, etc @@ -598,124 +621,71 @@ lintKind kind ------------------- lintTyBndrKind :: OutTyVar -> LintM () -lintTyBndrKind tv - | isCoVar tv = lintCoVarKind tv - | otherwise = lintKind (tyVarKind tv) - -------------------- -lintCoVarKind :: OutCoVar -> LintM () --- Check the kind of a coercion binder -lintCoVarKind tv - = do { (ty1,ty2) <- lintSplitCoVar tv - ; k1 <- lintType ty1 - ; k2 <- lintType ty2 - ; unless (k1 `eqKind` k2) - (addErrL (sep [ ptext (sLit "Kind mis-match in coercion kind of:") - , nest 2 (quotes (ppr tv)) - , ppr [k1,k2] ])) } - -------------------- -lintSplitCoVar :: CoVar -> LintM (Type,Type) -lintSplitCoVar cv - = case coVarKind_maybe cv of - Just ts -> return ts - Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:") - , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))]) +lintTyBndrKind tv = lintKind (tyVarKind tv) ------------------- -lintCoercion, lintCoercion' :: OutType -> LintM (OutType, OutType) +lintCoercion :: OutCoercion -> LintM (OutType, OutType) -- Check the kind of a coercion term, returning the kind -lintCoercion co - = addLoc (InCoercion co) $ lintCoercion' co - -lintCoercion' ty@(TyVarTy tv) - = do { checkTyVarInScope tv - ; if isCoVar tv then return (coVarKind tv) - else return (ty, ty) } - -lintCoercion' ty@(AppTy ty1 ty2) - = do { (s1,t1) <- lintCoercion ty1 - ; (s2,t2) <- lintCoercion ty2 - ; check_co_app ty (typeKind s1) [s2] - ; return (mkAppTy s1 s2, mkAppTy t1 t2) } - -lintCoercion' ty@(FunTy ty1 ty2) - = do { (s1,t1) <- lintCoercion ty1 - ; (s2,t2) <- lintCoercion ty2 - ; check_co_app ty (tyConKind funTyCon) [s1, s2] - ; return (FunTy s1 s2, FunTy t1 t2) } - -lintCoercion' ty@(TyConApp tc tys) - | Just (ar, desc) <- isCoercionTyCon_maybe tc - = do { unless (tys `lengthAtLeast` ar) (badCo ty) - ; (s,t) <- lintCoTyConApp ty desc (take ar tys) - ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys) - ; check_co_app ty (typeKind s) ss - ; return (mkAppTys s ss, mkAppTys t ts) } +lintCoercion (Refl ty) + = do { ty' <- lintInTy ty + ; return (ty', ty') } - | not (tyConHasKind tc) -- Just something bizarre like SuperKindTyCon - = badCo ty +lintCoercion co@(TyConAppCo tc cos) + = do { (ss,ts) <- mapAndUnzipM lintCoercion cos + ; check_co_app co (tyConKind tc) ss + ; return (mkTyConApp tc ss, mkTyConApp tc ts) } - | otherwise - = do { (ss,ts) <- mapAndUnzipM lintCoercion tys - ; check_co_app ty (tyConKind tc) ss - ; return (TyConApp tc ss, TyConApp tc ts) } - -lintCoercion' ty@(PredTy (ClassP cls tys)) - = do { (ss,ts) <- mapAndUnzipM lintCoercion tys - ; check_co_app ty (tyConKind (classTyCon cls)) ss - ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) } - -lintCoercion' (PredTy (IParam n p_ty)) - = do { (s,t) <- lintCoercion p_ty - ; return (PredTy (IParam n s), PredTy (IParam n t)) } - -lintCoercion' ty@(PredTy (EqPred {})) - = failWithL (badEq ty) - -lintCoercion' (ForAllTy tv ty) - | isCoVar tv - = do { (co1, co2) <- lintSplitCoVar tv - ; (s1,t1) <- lintCoercion co1 - ; (s2,t2) <- lintCoercion co2 - ; (sr,tr) <- lintCoercion ty - ; return (mkCoPredTy s1 s2 sr, mkCoPredTy t1 t2 tr) } +lintCoercion co@(AppCo co1 co2) + = do { (s1,t1) <- lintCoercion co1 + ; (s2,t2) <- lintCoercion co2 + ; check_co_app co (typeKind s1) [s2] + ; return (mkAppTy s1 s2, mkAppTy t1 t2) } - | otherwise - = do { lintKind (tyVarKind tv) - ; (s,t) <- addInScopeVar tv (lintCoercion ty) - ; return (ForAllTy tv s, ForAllTy tv t) } - -badCo :: Coercion -> LintM a -badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co)) - ---------------- -lintCoTyConApp :: Coercion -> CoTyConDesc -> [Coercion] -> LintM (Type,Type) --- Always called with correct number of coercion arguments --- First arg is just for error message -lintCoTyConApp _ CoLeft (co:_) = lintLR fst co -lintCoTyConApp _ CoRight (co:_) = lintLR snd co -lintCoTyConApp _ CoCsel1 (co:_) = lintCsel fstOf3 co -lintCoTyConApp _ CoCsel2 (co:_) = lintCsel sndOf3 co -lintCoTyConApp _ CoCselR (co:_) = lintCsel thirdOf3 co - -lintCoTyConApp _ CoSym (co:_) - = do { (ty1,ty2) <- lintCoercion co - ; return (ty2,ty1) } - -lintCoTyConApp co CoTrans (co1:co2:_) +lintCoercion (ForAllCo v co) + = do { lintKind (tyVarKind v) + ; (s,t) <- addInScopeVar v (lintCoercion co) + ; return (ForAllTy v s, ForAllTy v t) } + +lintCoercion (CoVarCo cv) + = do { checkTyCoVarInScope cv + ; return (coVarKind cv) } + +lintCoercion (AxiomInstCo (CoAxiom { co_ax_tvs = tvs + , co_ax_lhs = lhs + , co_ax_rhs = rhs }) + cos) + = do { (tys1, tys2) <- liftM unzip (checkTyCoKinds tvs cos) + ; return (substTyWith tvs tys1 lhs, + substTyWith tvs tys2 rhs) } + +lintCoercion (UnsafeCo ty1 ty2) + = do { ty1' <- lintInTy ty1 + ; ty2' <- lintInTy ty2 + ; return (ty1', ty2') } + +lintCoercion (SymCo co) + = do { (ty1, ty2) <- lintCoercion co + ; return (ty2, ty1) } + +lintCoercion co@(TransCo co1 co2) = do { (ty1a, ty1b) <- lintCoercion co1 ; (ty2a, ty2b) <- lintCoercion co2 - ; checkL (ty1b `coreEqType` ty2a) + ; checkL (ty1b `eqType` ty2a) (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co) 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b])) ; return (ty1a, ty2b) } -lintCoTyConApp _ CoInst (co:arg_ty:_) - = do { co_tys <- lintCoercion co +lintCoercion the_co@(NthCo d co) + = do { (s,t) <- lintCoercion co + ; sn <- checkTcApp the_co d s + ; tn <- checkTcApp the_co d t + ; return (sn, tn) } + +lintCoercion (InstCo co arg_ty) + = do { co_tys <- lintCoercion co ; arg_kind <- lintType arg_ty - ; case decompInst_maybe co_tys of - Just ((tv1,tv2), (ty1,ty2)) + ; case splitForAllTy_maybe `traverse` toPair co_tys of + Just (Pair (tv1,ty1) (tv2,ty2)) | arg_kind `isSubKind` tyVarKind tv1 -> return (substTyWith [tv1] [arg_ty] ty1, substTyWith [tv2] [arg_ty] ty2) @@ -723,40 +693,20 @@ lintCoTyConApp _ CoInst (co:arg_ty:_) -> failWithL (ptext (sLit "Kind mis-match in inst coercion")) Nothing -> failWithL (ptext (sLit "Bad argument of inst")) } -lintCoTyConApp _ (CoAxiom { co_ax_tvs = tvs - , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos - = do { (tys1, tys2) <- mapAndUnzipM lintCoercion cos - ; sequence_ (zipWith checkKinds tvs tys1) - ; return (substTyWith tvs tys1 lhs_ty, - substTyWith tvs tys2 rhs_ty) } - -lintCoTyConApp _ CoUnsafe (ty1:ty2:_) - = do { _ <- lintType ty1 - ; _ <- lintType ty2 -- Ignore kinds; it's unsafe! - ; return (ty1,ty2) } - -lintCoTyConApp _ _ _ = panic "lintCoTyConApp" -- Called with wrong number of coercion args - ----------- -lintLR :: (forall a. (a,a)->a) -> Coercion -> LintM (Type,Type) -lintLR sel co - = do { (ty1,ty2) <- lintCoercion co - ; case decompLR_maybe (ty1,ty2) of - Just res -> return (sel res) - Nothing -> failWithL (ptext (sLit "Bad argument of left/right")) } - ---------- -lintCsel :: (forall a. (a,a,a)->a) -> Coercion -> LintM (Type,Type) -lintCsel sel co - = do { (ty1,ty2) <- lintCoercion co - ; case decompCsel_maybe (ty1,ty2) of - Just res -> return (sel res) - Nothing -> failWithL (ptext (sLit "Bad argument of csel")) } +checkTcApp :: Coercion -> Int -> Type -> LintM Type +checkTcApp co n ty + | Just (_, tys) <- splitTyConApp_maybe ty + , n < length tys + = return (tys !! n) + | otherwise + = failWithL (hang (ptext (sLit "Bad getNth:") <+> ppr co) + 2 (ptext (sLit "Offending type:") <+> ppr ty)) ------------------- lintType :: OutType -> LintM Kind lintType (TyVarTy tv) - = do { checkTyVarInScope tv + = do { checkTyCoVarInScope tv ; return (tyVarKind tv) } lintType ty@(AppTy t1 t2) @@ -782,8 +732,13 @@ lintType ty@(PredTy (ClassP cls tys)) lintType (PredTy (IParam _ p_ty)) = lintType p_ty -lintType ty@(PredTy (EqPred {})) - = failWithL (badEq ty) +lintType ty@(PredTy (EqPred t1 t2)) + = do { k1 <- lintType t1 + ; k2 <- lintType t2 + ; unless (k1 `eqKind` k2) + (addErrL (sep [ ptext (sLit "Kind mis-match in equality predicate:") + , nest 2 (ppr ty) ])) + ; return unliftedTypeKind } ---------------- lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind @@ -812,10 +767,6 @@ lint_kind_app doc kfn ks = go kfn ks Just (kfa, kfb) -> do { unless (k `isSubKind` kfa) (addErrL fail_msg) ; go kfb ks } --------------- -badEq :: Type -> SDoc -badEq ty = hang (ptext (sLit "Unexpected equality predicate:")) - 1 (quotes (ppr ty)) \end{code} %************************************************************************ @@ -870,7 +821,7 @@ data LintLocInfo | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which) | TopLevelBindings | InType Type -- Inside a type - | InCoercion Coercion -- Inside a type + | InCo Coercion -- Inside a coercion \end{code} @@ -936,12 +887,15 @@ updateTvSubst subst' m = getTvSubst :: LintM TvSubst getTvSubst = LintM (\ _ subst errs -> (Just subst, errs)) -applySubst :: Type -> LintM Type -applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) } +applySubstTy :: Type -> LintM Type +applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) } + +applySubstCo :: Coercion -> LintM Coercion +applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) } extendSubstL :: TyVar -> Type -> LintM a -> LintM a extendSubstL tv ty m - = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs) + = LintM (\ loc subst errs -> unLintM m loc (Type.extendTvSubst subst tv ty) errs) \end{code} \begin{code} @@ -969,8 +923,8 @@ checkBndrIdInScope binder id msg = ptext (sLit "is out of scope inside info for") <+> ppr binder -checkTyVarInScope :: TyVar -> LintM () -checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv +checkTyCoVarInScope :: TyCoVar -> LintM () +checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v checkInScope :: SDoc -> Var -> LintM () checkInScope loc_msg var = @@ -982,7 +936,7 @@ checkTys :: OutType -> OutType -> Message -> LintM () -- check ty2 is subtype of ty1 (ie, has same structure but usage -- annotations need only be consistent, not equal) -- Assumes ty1,ty2 are have alrady had the substitution applied -checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg +checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg \end{code} %************************************************************************ @@ -1021,8 +975,8 @@ dumpLoc TopLevelBindings = (noSrcLoc, empty) dumpLoc (InType ty) = (noSrcLoc, text "In the type" <+> quotes (ppr ty)) -dumpLoc (InCoercion ty) - = (noSrcLoc, text "In the coercion" <+> quotes (ppr ty)) +dumpLoc (InCo co) + = (noSrcLoc, text "In the coercion" <+> quotes (ppr co)) pp_binders :: [Var] -> SDoc pp_binders bs = sep (punctuate comma (map pp_binder bs)) @@ -1114,29 +1068,21 @@ mkNonFunAppMsg fun_ty arg_ty arg hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty), hang (ptext (sLit "Arg:")) 4 (ppr arg)] -mkTyVarLetErr :: TyVar -> Type -> Message -mkTyVarLetErr tyvar ty - = vcat [ptext (sLit "Bad `let' binding for type or coercion variable:"), - hang (ptext (sLit "Type/coercion variable:")) - 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)), - hang (ptext (sLit "Arg type/coercion:")) - 4 (ppr ty)] - -mkKindErrMsg :: TyVar -> Type -> Message -mkKindErrMsg tyvar arg_ty - = vcat [ptext (sLit "Kinds don't match in type application:"), - hang (ptext (sLit "Type variable:")) - 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)), - hang (ptext (sLit "Arg type:")) - 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))] - -mkCoAppErrMsg :: TyVar -> Type -> Message -mkCoAppErrMsg tyvar arg_ty - = vcat [ptext (sLit "Kinds don't match in coercion application:"), - hang (ptext (sLit "Coercion variable:")) +mkLetErr :: TyVar -> CoreExpr -> Message +mkLetErr bndr rhs + = vcat [ptext (sLit "Bad `let' binding:"), + hang (ptext (sLit "Variable:")) + 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)), + hang (ptext (sLit "Rhs:")) + 4 (ppr rhs)] + +mkTyCoAppErrMsg :: TyVar -> Coercion -> Message +mkTyCoAppErrMsg tyvar arg_co + = vcat [ptext (sLit "Kinds don't match in lifted coercion application:"), + hang (ptext (sLit "Type variable:")) 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)), hang (ptext (sLit "Arg coercion:")) - 4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))] + 4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))] mkTyAppMsg :: Type -> Type -> Message mkTyAppMsg ty arg_ty @@ -1168,6 +1114,15 @@ mkStrictMsg binder hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)] ] + +mkKindErrMsg :: TyVar -> Type -> Message +mkKindErrMsg tyvar arg_ty + = vcat [ptext (sLit "Kinds don't match in type application:"), + hang (ptext (sLit "Type variable:")) + 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)), + hang (ptext (sLit "Arg type:")) + 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))] + mkArityMsg :: Id -> Message mkArityMsg binder = vcat [hsep [ptext (sLit "Demand type has "), @@ -1203,3 +1158,56 @@ dupExtVars vars = hang (ptext (sLit "Duplicate top-level variables with the same qualified name")) 2 (ppr vars) \end{code} + +-------------- DEAD CODE ------------------- + +------------------- +checkCoKind :: CoVar -> OutCoercion -> LintM () +-- Both args have had substitution applied +checkCoKind covar arg_co + = do { (s2,t2) <- lintCoercion arg_co + ; unless (s1 `eqType` s2 && t1 `coreEqType` t2) + (addErrL (mkCoAppErrMsg covar arg_co)) } + where + (s1,t1) = coVarKind covar + +lintCoVarKind :: OutCoVar -> LintM () +-- Check the kind of a coercion binder +lintCoVarKind tv + = do { (ty1,ty2) <- lintSplitCoVar tv + ; lintEqType ty1 ty2 + + +------------------- +lintSplitCoVar :: CoVar -> LintM (Type,Type) +lintSplitCoVar cv + = case coVarKind_maybe cv of + Just ts -> return ts + Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:") + , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))]) + +mkCoVarLetErr :: CoVar -> Coercion -> Message +mkCoVarLetErr covar co + = vcat [ptext (sLit "Bad `let' binding for coercion variable:"), + hang (ptext (sLit "Coercion variable:")) + 4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)), + hang (ptext (sLit "Arg coercion:")) + 4 (ppr co)] + +mkCoAppErrMsg :: CoVar -> Coercion -> Message +mkCoAppErrMsg covar arg_co + = vcat [ptext (sLit "Kinds don't match in coercion application:"), + hang (ptext (sLit "Coercion variable:")) + 4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)), + hang (ptext (sLit "Arg coercion:")) + 4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))] + + +mkCoAppMsg :: Type -> Coercion -> Message +mkCoAppMsg ty arg_co + = vcat [text "Illegal type application:", + hang (ptext (sLit "exp type:")) + 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)), + hang (ptext (sLit "arg type:")) + 4 (ppr arg_co <+> dcolon <+> ppr (coercionKind arg_co))] + diff --git a/compiler/coreSyn/CorePrep.lhs b/compiler/coreSyn/CorePrep.lhs index 42379b4c01..04057160b8 100644 --- a/compiler/coreSyn/CorePrep.lhs +++ b/compiler/coreSyn/CorePrep.lhs @@ -37,6 +37,7 @@ import OrdList import ErrUtils import DynFlags import Util +import Pair import Outputable import MonadUtils import FastString @@ -78,9 +79,9 @@ The goal of this pass is to prepare for code generation. weaker guarantee of no clashes which the simplifier provides. And that is what the code generator needs. - We don't clone TyVars. The code gen doesn't need that, + We don't clone TyVars or CoVars. The code gen doesn't need that, and doing so would be tiresome because then we'd need - to substitute in types. + to substitute in types and coercions. 7. Give each dynamic CCall occurrence a fresh unique; this is @@ -104,19 +105,21 @@ Invariants Here is the syntax of the Core produced by CorePrep: Trivial expressions - triv ::= lit | var | triv ty | /\a. triv | triv |> co + triv ::= lit | var + | triv ty | /\a. triv + | truv co | /\c. triv | triv |> co Applications - app ::= lit | var | app triv | app ty | app |> co + app ::= lit | var | app triv | app ty | app co | app |> co Expressions body ::= app | let(rec) x = rhs in body -- Boxed only | case body of pat -> body - | /\a. body + | /\a. body | /\c. body | body |> co - Right hand sides (only place where lambdas can occur) + Right hand sides (only place where value lambdas can occur) rhs ::= /\a.rhs | \x.rhs | body We define a synonym for each of these non-terminals. Functions @@ -440,9 +443,10 @@ cpeRhsE :: CorePrepEnv -> CoreExpr -> UniqSM (Floats, CpeRhs) -- For example -- f (g x) ===> ([v = g x], f v) -cpeRhsE _env expr@(Type _) = return (emptyFloats, expr) -cpeRhsE _env expr@(Lit _) = return (emptyFloats, expr) -cpeRhsE env expr@(Var {}) = cpeApp env expr +cpeRhsE _env expr@(Type {}) = return (emptyFloats, expr) +cpeRhsE _env expr@(Coercion {}) = return (emptyFloats, expr) +cpeRhsE _env expr@(Lit {}) = return (emptyFloats, expr) +cpeRhsE env expr@(Var {}) = cpeApp env expr cpeRhsE env (Var f `App` _ `App` arg) | f `hasKey` lazyIdKey -- Replace (lazy a) by a @@ -528,7 +532,7 @@ rhsToBody (Cast e co) rhsToBody expr@(Lam {}) | Just no_lam_result <- tryEtaReducePrep bndrs body = return (emptyFloats, no_lam_result) - | all isTyCoVar bndrs -- Type lambdas are ok + | all isTyVar bndrs -- Type lambdas are ok = return (emptyFloats, expr) | otherwise -- Some value lambdas = do { fn <- newVar (exprType expr) @@ -579,6 +583,10 @@ cpeApp env expr = do { (fun',hd,fun_ty,floats,ss) <- collect_args fun depth ; return (App fun' arg, hd, applyTy fun_ty arg_ty, floats, ss) } + collect_args (App fun arg@(Coercion arg_co)) depth + = do { (fun',hd,fun_ty,floats,ss) <- collect_args fun depth + ; return (App fun' arg, hd, applyCo fun_ty arg_co, floats, ss) } + collect_args (App fun arg) depth = do { (fun',hd,fun_ty,floats,ss) <- collect_args fun (depth+1) ; let @@ -608,7 +616,7 @@ cpeApp env expr -- partial application might be seq'd collect_args (Cast fun co) depth - = do { let (_ty1,ty2) = coercionKind co + = do { let Pair _ty1 ty2 = coercionKind co ; (fun', hd, _, floats, ss) <- collect_args fun depth ; return (Cast fun' co, hd, ty2, floats, ss) } @@ -751,11 +759,12 @@ cpe_ExprIsTrivial :: CoreExpr -> Bool -- Version that doesn't consider an scc annotation to be trivial. cpe_ExprIsTrivial (Var _) = True cpe_ExprIsTrivial (Type _) = True +cpe_ExprIsTrivial (Coercion _) = True cpe_ExprIsTrivial (Lit _) = True cpe_ExprIsTrivial (App e arg) = isTypeArg arg && cpe_ExprIsTrivial e cpe_ExprIsTrivial (Note n e) = notSccNote n && cpe_ExprIsTrivial e cpe_ExprIsTrivial (Cast e _) = cpe_ExprIsTrivial e -cpe_ExprIsTrivial (Lam b body) | isTyCoVar b = cpe_ExprIsTrivial body +cpe_ExprIsTrivial (Lam b body) | isTyVar b = cpe_ExprIsTrivial body cpe_ExprIsTrivial _ = False \end{code} @@ -1070,7 +1079,7 @@ cloneBndrs env bs = mapAccumLM cloneBndr env bs cloneBndr :: CorePrepEnv -> Var -> UniqSM (CorePrepEnv, Var) cloneBndr env bndr - | isLocalId bndr + | isLocalId bndr, not (isCoVar bndr) = do bndr' <- setVarUnique bndr <$> getUniqueM -- We are going to OccAnal soon, so drop (now-useless) rules/unfoldings @@ -1082,7 +1091,7 @@ cloneBndr env bndr | otherwise -- Top level things, which we don't want -- to clone, have become GlobalIds by now - -- And we don't clone tyvars + -- And we don't clone tyvars, or coercion variables = return (env, bndr) diff --git a/compiler/coreSyn/CoreSubst.lhs b/compiler/coreSyn/CoreSubst.lhs index a229b8c4e9..047e6c337b 100644 --- a/compiler/coreSyn/CoreSubst.lhs +++ b/compiler/coreSyn/CoreSubst.lhs @@ -12,14 +12,15 @@ module CoreSubst ( -- ** Substituting into expressions and related types deShadowBinds, substSpec, substRulesForImportedIds, - substTy, substExpr, substExprSC, substBind, substBindSC, + substTy, substCo, substExpr, substExprSC, substBind, substBindSC, substUnfolding, substUnfoldingSC, - substUnfoldingSource, lookupIdSubst, lookupTvSubst, substIdOcc, + substUnfoldingSource, lookupIdSubst, lookupTvSubst, lookupCvSubst, substIdOcc, -- ** Operations on substitutions emptySubst, mkEmptySubst, mkSubst, mkOpenSubst, substInScope, isEmptySubst, extendIdSubst, extendIdSubstList, extendTvSubst, extendTvSubstList, - extendSubst, extendSubstList, zapSubstEnv, + extendCvSubst, extendCvSubstList, + extendSubst, extendSubstList, extendSubstWithVar, zapSubstEnv, addInScopeSet, extendInScope, extendInScopeList, extendInScopeIds, isInScope, setInScope, delBndr, delBndrs, @@ -37,18 +38,23 @@ module CoreSubst ( import CoreSyn import CoreFVs import CoreUtils -import PprCore import OccurAnal( occurAnalyseExpr, occurAnalysePgm ) import qualified Type -import Type ( Type, TvSubst(..), TvSubstEnv ) -import Coercion ( isIdentityCoercion ) +import qualified Coercion + + -- We are defining local versions +import Type hiding ( substTy, extendTvSubst, extendTvSubstList + , isInScope, substTyVarBndr ) +import Coercion hiding ( substTy, substCo, extendTvSubst, substTyVarBndr, substCoVarBndr ) + import OptCoercion ( optCoercion ) +import PprCore ( pprCoreBindings ) import VarSet import VarEnv import Id import Name ( Name ) -import Var ( Var, TyVar, setVarUnique ) +import Var import IdInfo import Unique import UniqSupply @@ -92,7 +98,8 @@ data Subst = Subst InScopeSet -- Variables in in scope (both Ids and TyVars) /after/ -- applying the substitution IdSubstEnv -- Substitution for Ids - TvSubstEnv -- Substitution for TyVars + TvSubstEnv -- Substitution from TyVars to Types + CvSubstEnv -- Substitution from TyCoVars to Coercions -- INVARIANT 1: See #in_scope_invariant# -- This is what lets us deal with name capture properly @@ -126,6 +133,11 @@ In consequence: * In substIdBndr, we extend the IdSubstEnv only when the unique changes +* If the CvSubstEnv, TvSubstEnv and IdSubstEnv are all empty, + substExpr does nothing (Note that the above rule for substIdBndr + maintains this property. If the incoming envts are both empty, then + substituting the type and IdInfo can't change anything.) + * In lookupIdSubst, we *must* look up the Id in the in-scope set, because it may contain non-trivial changes. Example: (/\a. \x:a. ...x...) Int @@ -140,7 +152,8 @@ In consequence: * (However, we don't need to do so for expressions found in the IdSubst itself, whose range is assumed to be correct wrt the in-scope set.) -Why do we make a different choice for the IdSubstEnv than the TvSubstEnv? +Why do we make a different choice for the IdSubstEnv than the +TvSubstEnv and CvSubstEnv? * For Ids, we change the IdInfo all the time (e.g. deleting the unfolding), and adding it back later, so using the TyVar convention @@ -158,70 +171,82 @@ type IdSubstEnv = IdEnv CoreExpr ---------------------------- isEmptySubst :: Subst -> Bool -isEmptySubst (Subst _ id_env tv_env) = isEmptyVarEnv id_env && isEmptyVarEnv tv_env +isEmptySubst (Subst _ id_env tv_env cv_env) + = isEmptyVarEnv id_env && isEmptyVarEnv tv_env && isEmptyVarEnv cv_env emptySubst :: Subst -emptySubst = Subst emptyInScopeSet emptyVarEnv emptyVarEnv +emptySubst = Subst emptyInScopeSet emptyVarEnv emptyVarEnv emptyVarEnv mkEmptySubst :: InScopeSet -> Subst -mkEmptySubst in_scope = Subst in_scope emptyVarEnv emptyVarEnv - -mkSubst :: InScopeSet -> TvSubstEnv -> IdSubstEnv -> Subst -mkSubst in_scope tvs ids = Subst in_scope ids tvs - --- getTvSubst :: Subst -> TvSubst --- getTvSubst (Subst in_scope _ tv_env) = TvSubst in_scope tv_env +mkEmptySubst in_scope = Subst in_scope emptyVarEnv emptyVarEnv emptyVarEnv --- getTvSubstEnv :: Subst -> TvSubstEnv --- getTvSubstEnv (Subst _ _ tv_env) = tv_env --- --- setTvSubstEnv :: Subst -> TvSubstEnv -> Subst --- setTvSubstEnv (Subst in_scope ids _) tvs = Subst in_scope ids tvs +mkSubst :: InScopeSet -> TvSubstEnv -> CvSubstEnv -> IdSubstEnv -> Subst +mkSubst in_scope tvs cvs ids = Subst in_scope ids tvs cvs -- | Find the in-scope set: see "CoreSubst#in_scope_invariant" substInScope :: Subst -> InScopeSet -substInScope (Subst in_scope _ _) = in_scope +substInScope (Subst in_scope _ _ _) = in_scope -- | Remove all substitutions for 'Id's and 'Var's that might have been built up -- while preserving the in-scope set zapSubstEnv :: Subst -> Subst -zapSubstEnv (Subst in_scope _ _) = Subst in_scope emptyVarEnv emptyVarEnv +zapSubstEnv (Subst in_scope _ _ _) = Subst in_scope emptyVarEnv emptyVarEnv emptyVarEnv -- | Add a substitution for an 'Id' to the 'Subst': you must ensure that the in-scope set is -- such that the "CoreSubst#in_scope_invariant" is true after extending the substitution like this extendIdSubst :: Subst -> Id -> CoreExpr -> Subst -- ToDo: add an ASSERT that fvs(subst-result) is already in the in-scope set -extendIdSubst (Subst in_scope ids tvs) v r = Subst in_scope (extendVarEnv ids v r) tvs +extendIdSubst (Subst in_scope ids tvs cvs) v r = Subst in_scope (extendVarEnv ids v r) tvs cvs -- | Adds multiple 'Id' substitutions to the 'Subst': see also 'extendIdSubst' extendIdSubstList :: Subst -> [(Id, CoreExpr)] -> Subst -extendIdSubstList (Subst in_scope ids tvs) prs = Subst in_scope (extendVarEnvList ids prs) tvs +extendIdSubstList (Subst in_scope ids tvs cvs) prs = Subst in_scope (extendVarEnvList ids prs) tvs cvs -- | Add a substitution for a 'TyVar' to the 'Subst': you must ensure that the in-scope set is -- such that the "CoreSubst#in_scope_invariant" is true after extending the substitution like this extendTvSubst :: Subst -> TyVar -> Type -> Subst -extendTvSubst (Subst in_scope ids tvs) v r = Subst in_scope ids (extendVarEnv tvs v r) +extendTvSubst (Subst in_scope ids tvs cvs) v r = Subst in_scope ids (extendVarEnv tvs v r) cvs -- | Adds multiple 'TyVar' substitutions to the 'Subst': see also 'extendTvSubst' extendTvSubstList :: Subst -> [(TyVar,Type)] -> Subst -extendTvSubstList (Subst in_scope ids tvs) prs = Subst in_scope ids (extendVarEnvList tvs prs) +extendTvSubstList (Subst in_scope ids tvs cvs) prs = Subst in_scope ids (extendVarEnvList tvs prs) cvs --- | Add a substitution for a 'TyVar' or 'Id' as appropriate to the 'Var' being added. See also --- 'extendIdSubst' and 'extendTvSubst' -extendSubst :: Subst -> Var -> CoreArg -> Subst -extendSubst (Subst in_scope ids tvs) tv (Type ty) - = ASSERT( isTyCoVar tv ) Subst in_scope ids (extendVarEnv tvs tv ty) -extendSubst (Subst in_scope ids tvs) id expr - = ASSERT( isId id ) Subst in_scope (extendVarEnv ids id expr) tvs +-- | Add a substitution from a 'TyCoVar' to a 'Coercion' to the 'Subst': you must ensure that the in-scope set is +-- such that the "CoreSubst#in_scope_invariant" is true after extending the substitution like this +extendCvSubst :: Subst -> TyCoVar -> Coercion -> Subst +extendCvSubst (Subst in_scope ids tvs cvs) v r = Subst in_scope ids tvs (extendVarEnv cvs v r) + +-- | Adds multiple 'TyCoVar' -> 'Coercion' substitutions to the +-- 'Subst': see also 'extendCvSubst' +extendCvSubstList :: Subst -> [(TyCoVar,Coercion)] -> Subst +extendCvSubstList (Subst in_scope ids tvs cvs) prs = Subst in_scope ids tvs (extendVarEnvList cvs prs) --- | Add a substitution for a 'TyVar' or 'Id' as appropriate to all the 'Var's being added. See also 'extendSubst' +-- | Add a substitution appropriate to the thing being substituted +-- (whether an expression, type, or coercion). See also +-- 'extendIdSubst', 'extendTvSubst', and 'extendCvSubst'. +extendSubst :: Subst -> Var -> CoreArg -> Subst +extendSubst subst var arg + = case arg of + Type ty -> ASSERT( isTyVar var ) extendTvSubst subst var ty + Coercion co -> ASSERT( isCoVar var ) extendCvSubst subst var co + _ -> ASSERT( isId var ) extendIdSubst subst var arg + +extendSubstWithVar :: Subst -> Var -> Var -> Subst +extendSubstWithVar subst v1 v2 + | isTyVar v1 = ASSERT( isTyVar v2 ) extendTvSubst subst v1 (mkTyVarTy v2) + | isCoVar v1 = ASSERT( isCoVar v2 ) extendCvSubst subst v1 (mkCoVarCo v2) + | otherwise = ASSERT( isId v2 ) extendIdSubst subst v1 (Var v2) + +-- | Add a substitution as appropriate to each of the terms being +-- substituted (whether expressions, types, or coercions). See also +-- 'extendSubst'. extendSubstList :: Subst -> [(Var,CoreArg)] -> Subst extendSubstList subst [] = subst extendSubstList subst ((var,rhs):prs) = extendSubstList (extendSubst subst var rhs) prs -- | Find the substitution for an 'Id' in the 'Subst' lookupIdSubst :: SDoc -> Subst -> Id -> CoreExpr -lookupIdSubst doc (Subst in_scope ids _) v +lookupIdSubst doc (Subst in_scope ids _ _) v | not (isLocalId v) = Var v | Just e <- lookupVarEnv ids v = e | Just v' <- lookupInScope in_scope v = Var v' @@ -231,18 +256,22 @@ lookupIdSubst doc (Subst in_scope ids _) v -- | Find the substitution for a 'TyVar' in the 'Subst' lookupTvSubst :: Subst -> TyVar -> Type -lookupTvSubst (Subst _ _ tvs) v = lookupVarEnv tvs v `orElse` Type.mkTyVarTy v +lookupTvSubst (Subst _ _ tvs _) v = ASSERT( isTyVar v) lookupVarEnv tvs v `orElse` Type.mkTyVarTy v + +-- | Find the coercion substitution for a 'TyCoVar' in the 'Subst' +lookupCvSubst :: Subst -> CoVar -> Coercion +lookupCvSubst (Subst _ _ _ cvs) v = ASSERT( isCoVar v ) lookupVarEnv cvs v `orElse` mkCoVarCo v delBndr :: Subst -> Var -> Subst -delBndr (Subst in_scope tvs ids) v - | isId v = Subst in_scope tvs (delVarEnv ids v) - | otherwise = Subst in_scope (delVarEnv tvs v) ids +delBndr (Subst in_scope ids tvs cvs) v + | isCoVar v = Subst in_scope ids tvs (delVarEnv cvs v) + | isTyVar v = Subst in_scope ids (delVarEnv tvs v) cvs + | otherwise = Subst in_scope (delVarEnv ids v) tvs cvs delBndrs :: Subst -> [Var] -> Subst -delBndrs (Subst in_scope tvs ids) vs - = Subst in_scope (delVarEnvList tvs vs_tv) (delVarEnvList ids vs_id) - where - (vs_id, vs_tv) = partition isId vs +delBndrs (Subst in_scope ids tvs cvs) vs + = Subst in_scope (delVarEnvList ids vs) (delVarEnvList tvs vs) (delVarEnvList cvs vs) + -- Easist thing is just delete all from all! -- | Simultaneously substitute for a bunch of variables -- No left-right shadowing @@ -252,49 +281,51 @@ mkOpenSubst :: InScopeSet -> [(Var,CoreArg)] -> Subst mkOpenSubst in_scope pairs = Subst in_scope (mkVarEnv [(id,e) | (id, e) <- pairs, isId id]) (mkVarEnv [(tv,ty) | (tv, Type ty) <- pairs]) + (mkVarEnv [(v,co) | (v, Coercion co) <- pairs]) ------------------------------ isInScope :: Var -> Subst -> Bool -isInScope v (Subst in_scope _ _) = v `elemInScopeSet` in_scope +isInScope v (Subst in_scope _ _ _) = v `elemInScopeSet` in_scope -- | Add the 'Var' to the in-scope set, but do not remove -- any existing substitutions for it addInScopeSet :: Subst -> VarSet -> Subst -addInScopeSet (Subst in_scope ids tvs) vs - = Subst (in_scope `extendInScopeSetSet` vs) ids tvs +addInScopeSet (Subst in_scope ids tvs cvs) vs + = Subst (in_scope `extendInScopeSetSet` vs) ids tvs cvs -- | Add the 'Var' to the in-scope set: as a side effect, -- and remove any existing substitutions for it extendInScope :: Subst -> Var -> Subst -extendInScope (Subst in_scope ids tvs) v +extendInScope (Subst in_scope ids tvs cvs) v = Subst (in_scope `extendInScopeSet` v) - (ids `delVarEnv` v) (tvs `delVarEnv` v) + (ids `delVarEnv` v) (tvs `delVarEnv` v) (cvs `delVarEnv` v) -- | Add the 'Var's to the in-scope set: see also 'extendInScope' extendInScopeList :: Subst -> [Var] -> Subst -extendInScopeList (Subst in_scope ids tvs) vs +extendInScopeList (Subst in_scope ids tvs cvs) vs = Subst (in_scope `extendInScopeSetList` vs) - (ids `delVarEnvList` vs) (tvs `delVarEnvList` vs) + (ids `delVarEnvList` vs) (tvs `delVarEnvList` vs) (cvs `delVarEnvList` vs) -- | Optimized version of 'extendInScopeList' that can be used if you are certain --- all the things being added are 'Id's and hence none are 'TyVar's +-- all the things being added are 'Id's and hence none are 'TyVar's or 'CoVar's extendInScopeIds :: Subst -> [Id] -> Subst -extendInScopeIds (Subst in_scope ids tvs) vs +extendInScopeIds (Subst in_scope ids tvs cvs) vs = Subst (in_scope `extendInScopeSetList` vs) - (ids `delVarEnvList` vs) tvs + (ids `delVarEnvList` vs) tvs cvs setInScope :: Subst -> InScopeSet -> Subst -setInScope (Subst _ ids tvs) in_scope = Subst in_scope ids tvs +setInScope (Subst _ ids tvs cvs) in_scope = Subst in_scope ids tvs cvs \end{code} Pretty printing, for debugging only \begin{code} instance Outputable Subst where - ppr (Subst in_scope ids tvs) + ppr (Subst in_scope ids tvs cvs) = ptext (sLit "<InScope =") <+> braces (fsep (map ppr (varEnvElts (getInScopeVars in_scope)))) $$ ptext (sLit " IdSubst =") <+> ppr ids $$ ptext (sLit " TvSubst =") <+> ppr tvs + $$ ptext (sLit " CvSubst =") <+> ppr cvs <> char '>' \end{code} @@ -326,10 +357,11 @@ subst_expr subst expr where go (Var v) = lookupIdSubst (text "subst_expr") subst v go (Type ty) = Type (substTy subst ty) + go (Coercion co) = Coercion (substCo subst co) go (Lit lit) = Lit lit go (App fun arg) = App (go fun) (go arg) go (Note note e) = Note (go_note note) (go e) - go (Cast e co) = Cast (go e) (optCoercion (getTvSubst subst) co) + go (Cast e co) = Cast (go e) (substCo subst co) -- Do not optimise even identity coercions -- Reason: substitution applies to the LHS of RULES, and -- if you "optimise" an identity coercion, you may @@ -416,8 +448,9 @@ preserve occ info in rules. -- 'IdInfo' is preserved by this process, although it is substituted into appropriately. substBndr :: Subst -> Var -> (Subst, Var) substBndr subst bndr - | isTyCoVar bndr = substTyVarBndr subst bndr - | otherwise = substIdBndr (text "var-bndr") subst subst bndr + | isTyVar bndr = substTyVarBndr subst bndr + | isCoVar bndr = substCoVarBndr subst bndr + | otherwise = substIdBndr (text "var-bndr") subst subst bndr -- | Applies 'substBndr' to a number of 'Var's, accumulating a new 'Subst' left-to-right substBndrs :: Subst -> [Var] -> (Subst, [Var]) @@ -439,9 +472,9 @@ substIdBndr :: SDoc -> (Subst, Id) -- ^ Transformed pair -- NB: unfolding may be zapped -substIdBndr _doc rec_subst subst@(Subst in_scope env tvs) old_id +substIdBndr _doc rec_subst subst@(Subst in_scope env tvs cvs) old_id = -- pprTrace "substIdBndr" (doc $$ ppr old_id $$ ppr in_scope) $ - (Subst (in_scope `extendInScopeSet` new_id) new_env tvs, new_id) + (Subst (in_scope `extendInScopeSet` new_id) new_env tvs cvs, new_id) where id1 = uniqAway in_scope old_id -- id1 is cloned if necessary id2 | no_type_change = id1 @@ -498,8 +531,8 @@ clone_id :: Subst -- Substitution for the IdInfo -> Subst -> (Id, Unique) -- Substitition and Id to transform -> (Subst, Id) -- Transformed pair -clone_id rec_subst subst@(Subst in_scope env tvs) (old_id, uniq) - = (Subst (in_scope `extendInScopeSet` new_id) new_env tvs, new_id) +clone_id rec_subst subst@(Subst in_scope env tvs cvs) (old_id, uniq) + = (Subst (in_scope `extendInScopeSet` new_id) new_env tvs cvs, new_id) where id1 = setVarUnique old_id uniq id2 = substIdType subst id1 @@ -510,26 +543,40 @@ clone_id rec_subst subst@(Subst in_scope env tvs) (old_id, uniq) %************************************************************************ %* * - Types + Types and Coercions %* * %************************************************************************ -For types we just call the corresponding function in Type, but we have -to repackage the substitution, from a Subst to a TvSubst +For types and coercions we just call the corresponding functions in +Type and Coercion, but we have to repackage the substitution, from a +Subst to a TvSubst. \begin{code} substTyVarBndr :: Subst -> TyVar -> (Subst, TyVar) -substTyVarBndr (Subst in_scope id_env tv_env) tv +substTyVarBndr (Subst in_scope id_env tv_env cv_env) tv = case Type.substTyVarBndr (TvSubst in_scope tv_env) tv of (TvSubst in_scope' tv_env', tv') - -> (Subst in_scope' id_env tv_env', tv') + -> (Subst in_scope' id_env tv_env' cv_env, tv') + +substCoVarBndr :: Subst -> TyVar -> (Subst, TyVar) +substCoVarBndr (Subst in_scope id_env tv_env cv_env) cv + = case Coercion.substCoVarBndr (CvSubst in_scope tv_env cv_env) cv of + (CvSubst in_scope' tv_env' cv_env', cv') + -> (Subst in_scope' id_env tv_env' cv_env', cv') -- | See 'Type.substTy' substTy :: Subst -> Type -> Type substTy subst ty = Type.substTy (getTvSubst subst) ty getTvSubst :: Subst -> TvSubst -getTvSubst (Subst in_scope _id_env tv_env) = TvSubst in_scope tv_env +getTvSubst (Subst in_scope _ tenv _) = TvSubst in_scope tenv + +getCvSubst :: Subst -> CvSubst +getCvSubst (Subst in_scope _ tenv cenv) = CvSubst in_scope tenv cenv + +-- | See 'Coercion.substCo' +substCo :: Subst -> Coercion -> Coercion +substCo subst co = Coercion.substCo (getCvSubst subst) co \end{code} @@ -541,8 +588,8 @@ getTvSubst (Subst in_scope _id_env tv_env) = TvSubst in_scope tv_env \begin{code} substIdType :: Subst -> Id -> Id -substIdType subst@(Subst _ _ tv_env) id - | isEmptyVarEnv tv_env || isEmptyVarSet (Type.tyVarsOfType old_ty) = id +substIdType subst@(Subst _ _ tv_env cv_env) id + | (isEmptyVarEnv tv_env && isEmptyVarEnv cv_env) || isEmptyVarSet (Type.tyVarsOfType old_ty) = id | otherwise = setIdType id (substTy subst old_ty) -- The tyVarsOfType is cheaper than it looks -- because we cache the free tyvars of the type @@ -555,7 +602,7 @@ substIdType subst@(Subst _ _ tv_env) id substIdInfo :: Subst -> Id -> IdInfo -> Maybe IdInfo substIdInfo subst new_id info | nothing_to_do = Nothing - | otherwise = Just (info `setSpecInfo` substSpec subst new_id old_rules + | otherwise = Just (info `setSpecInfo` substSpec subst new_id old_rules `setUnfoldingInfo` substUnfolding subst old_unf) where old_rules = specInfo info @@ -594,7 +641,7 @@ substUnfolding _ unf = unf -- NoUnfolding, OtherCon ------------------- substUnfoldingSource :: Subst -> UnfoldingSource -> UnfoldingSource -substUnfoldingSource (Subst in_scope ids _) (InlineWrapper wkr) +substUnfoldingSource (Subst in_scope ids _ _) (InlineWrapper wkr) | Just wkr_expr <- lookupVarEnv ids wkr = case wkr_expr of Var w1 -> InlineWrapper w1 @@ -628,7 +675,7 @@ substSpec subst new_id (SpecInfo rules rhs_fvs) where subst_ru_fn = const (idName new_id) new_spec = SpecInfo (map (substRule subst subst_ru_fn) rules) - (substVarSet subst rhs_fvs) + (substVarSet subst rhs_fvs) ------------------ substRulesForImportedIds :: Subst -> [CoreRule] -> [CoreRule] @@ -646,7 +693,6 @@ substRule :: Subst -> (Name -> Name) -> CoreRule -> CoreRule -- - Rules for *local* Ids are in the IdInfo for that Id, -- and the ru_fn field is simply replaced by the new name -- of the Id - substRule _ _ rule@(BuiltinRule {}) = rule substRule subst subst_ru_fn rule@(Rule { ru_bndrs = bndrs, ru_args = args , ru_fn = fn_name, ru_rhs = rhs @@ -664,7 +710,7 @@ substRule subst subst_ru_fn rule@(Rule { ru_bndrs = bndrs, ru_args = args ------------------ substVarSet :: Subst -> VarSet -> VarSet -substVarSet subst fvs +substVarSet subst fvs = foldVarSet (unionVarSet . subst_fv subst) emptyVarSet fvs where subst_fv subst fv @@ -713,7 +759,7 @@ simpleOptExpr expr -- won't *be* substituting for x if it occurs inside a -- lambda. -- - -- It's a bit painful to call exprFreeVars, because it makes + -- It's a bit painful to call exprFreeVars, because it makes -- three passes instead of two (occ-anal, and go) simpleOptExprWith :: Subst -> InExpr -> OutExpr @@ -747,19 +793,22 @@ type OutExpr = CoreExpr -- In these functions the substitution maps InVar -> OutExpr ---------------------- -simple_opt_expr :: Subst -> InExpr -> OutExpr -simple_opt_expr subst expr +simple_opt_expr, simple_opt_expr' :: Subst -> InExpr -> OutExpr +simple_opt_expr s e = simple_opt_expr' s e + +simple_opt_expr' subst expr = go expr where go (Var v) = lookupIdSubst (text "simpleOptExpr") subst v go (App e1 e2) = simple_app subst e1 [go e2] - go (Type ty) = Type (substTy subst ty) + go (Type ty) = Type (substTy subst ty) + go (Coercion co) = Coercion (optCoercion (getCvSubst subst) co) go (Lit lit) = Lit lit go (Note note e) = Note note (go e) - go (Cast e co) | isIdentityCoercion co' = go e - | otherwise = Cast (go e) co' + go (Cast e co) | isReflCo co' = go e + | otherwise = Cast (go e) co' where - co' = substTy subst co + co' = optCoercion (getCvSubst subst) co go (Let bind body) = case simple_opt_bind subst bind of (subst', Nothing) -> simple_opt_expr subst' body @@ -806,21 +855,25 @@ simple_app subst e as = foldl App (simple_opt_expr subst e) as ---------------------- -simple_opt_bind :: Subst -> CoreBind -> (Subst, Maybe CoreBind) -simple_opt_bind subst (Rec prs) - = (subst'', Just (Rec (reverse rev_prs'))) +simple_opt_bind,simple_opt_bind' :: Subst -> CoreBind -> (Subst, Maybe CoreBind) +simple_opt_bind s b -- Can add trace stuff here + = simple_opt_bind' s b + +simple_opt_bind' subst (Rec prs) + = (subst'', res_bind) where + res_bind = Just (Rec (reverse rev_prs')) (subst', bndrs') = subst_opt_bndrs subst (map fst prs) (subst'', rev_prs') = foldl do_pr (subst', []) (prs `zip` bndrs') do_pr (subst, prs) ((b,r), b') = case maybe_substitute subst b r2 of Just subst' -> (subst', prs) - Nothing -> (subst, (b2,r2):prs) + Nothing -> (subst, (b2,r2):prs) where b2 = add_info subst b b' r2 = simple_opt_expr subst r -simple_opt_bind subst (NonRec b r) +simple_opt_bind' subst (NonRec b r) = case maybe_substitute subst b r' of Just ext_subst -> (ext_subst, Nothing) Nothing -> (subst', Just (NonRec b2 r')) @@ -836,10 +889,14 @@ maybe_substitute :: Subst -> InVar -> OutExpr -> Maybe Subst -- or returns Nothing maybe_substitute subst b r | Type ty <- r -- let a::* = TYPE ty in <body> - = ASSERT( isTyCoVar b ) + = ASSERT( isTyVar b ) Just (extendTvSubst subst b ty) - | isId b -- let x = e in <body> + | Coercion co <- r + = ASSERT( isCoVar b ) + Just (extendCvSubst subst b co) + + | isId b -- let x = e in <body> , safe_to_inline (idOccInfo b) , isAlwaysActive (idInlineActivation b) -- Note [Inline prag in simplOpt] , not (isStableUnfolding (idUnfolding b)) @@ -859,19 +916,20 @@ maybe_substitute subst b r ---------------------- subst_opt_bndr :: Subst -> InVar -> (Subst, OutVar) subst_opt_bndr subst bndr - | isTyCoVar bndr = substTyVarBndr subst bndr - | otherwise = subst_opt_id_bndr subst bndr + | isTyVar bndr = substTyVarBndr subst bndr + | isCoVar bndr = substCoVarBndr subst bndr + | otherwise = subst_opt_id_bndr subst bndr subst_opt_id_bndr :: Subst -> InId -> (Subst, OutId) -- Nuke all fragile IdInfo, unfolding, and RULES; -- it gets added back later by add_info -- Rather like SimplEnv.substIdBndr -- --- It's important to zap fragile OccInfo (which CoreSubst.SubstIdBndr +-- It's important to zap fragile OccInfo (which CoreSubst.substIdBndr -- carefully does not do) because simplOptExpr invalidates it -subst_opt_id_bndr subst@(Subst in_scope id_subst tv_subst) old_id - = (Subst new_in_scope new_id_subst tv_subst, new_id) +subst_opt_id_bndr subst@(Subst in_scope id_subst tv_subst cv_subst) old_id + = (Subst new_in_scope new_id_subst tv_subst cv_subst, new_id) where id1 = uniqAway in_scope old_id id2 = setIdType id1 (substTy subst (idType old_id)) @@ -894,9 +952,9 @@ subst_opt_bndrs subst bndrs ---------------------- add_info :: Subst -> InVar -> OutVar -> OutVar -add_info subst old_bndr new_bndr - | isTyCoVar old_bndr = new_bndr - | otherwise = maybeModifyIdInfo mb_new_info new_bndr +add_info subst old_bndr new_bndr + | isTyVar old_bndr = new_bndr + | otherwise = maybeModifyIdInfo mb_new_info new_bndr where mb_new_info = substIdInfo subst new_bndr (idInfo old_bndr) \end{code} @@ -920,3 +978,4 @@ we don't know what phase we're in. Here's an example When inlining 'foo' in 'bar' we want the let-binding for 'inner' to remain visible until Phase 1 + diff --git a/compiler/coreSyn/CoreSyn.lhs b/compiler/coreSyn/CoreSyn.lhs index 603b745cf2..e754c6dda5 100644 --- a/compiler/coreSyn/CoreSyn.lhs +++ b/compiler/coreSyn/CoreSyn.lhs @@ -15,7 +15,7 @@ module CoreSyn ( -- ** 'Expr' construction mkLets, mkLams, - mkApps, mkTyApps, mkVarApps, + mkApps, mkTyApps, mkCoApps, mkVarApps, mkIntLit, mkIntLitInt, mkWordLit, mkWordLitWord, @@ -23,18 +23,19 @@ module CoreSyn ( mkFloatLit, mkFloatLitFloat, mkDoubleLit, mkDoubleLitDouble, - mkConApp, mkTyBind, + mkConApp, mkTyBind, mkCoBind, varToCoreExpr, varsToCoreExprs, - isTyCoVar, isId, cmpAltCon, cmpAlt, ltAlt, + isId, cmpAltCon, cmpAlt, ltAlt, -- ** Simple 'Expr' access functions and predicates bindersOf, bindersOfBinds, rhssOfBind, rhssOfAlts, collectBinders, collectTyBinders, collectValBinders, collectTyAndValBinders, collectArgs, coreExprCc, flattenBinds, - isValArg, isTypeArg, valArgCount, valBndrCount, isRuntimeArg, isRuntimeVar, - notSccNote, + isValArg, isTypeArg, isTyCoArg, valArgCount, valBndrCount, + isRuntimeArg, isRuntimeVar, + notSccNote, -- * Unfolding data types Unfolding(..), UnfoldingGuidance(..), UnfoldingSource(..), @@ -95,7 +96,7 @@ import Util import Data.Data import Data.Word -infixl 4 `mkApps`, `mkTyApps`, `mkVarApps`, `App` +infixl 4 `mkApps`, `mkTyApps`, `mkVarApps`, `App`, `mkCoApps` -- Left associative, so that we can say (f `mkTyApps` xs `mkVarApps` ys) \end{code} @@ -239,6 +240,8 @@ data Expr b | Type Type -- ^ A type: this should only show up at the top -- level of an Arg + + | Coercion Coercion -- ^ A coercion deriving (Data, Typeable) -- | Type synonym for expressions that occur in function argument positions. @@ -878,6 +881,8 @@ instance Outputable b => OutputableBndr (TaggedBndr b) where mkApps :: Expr b -> [Arg b] -> Expr b -- | Apply a list of type argument expressions to a function expression in a nested fashion mkTyApps :: Expr b -> [Type] -> Expr b +-- | Apply a list of coercion argument expressions to a function expression in a nested fashion +mkCoApps :: Expr b -> [Coercion] -> Expr b -- | Apply a list of type or value variables to a function expression in a nested fashion mkVarApps :: Expr b -> [Var] -> Expr b -- | Apply a list of argument expressions to a data constructor in a nested fashion. Prefer to @@ -886,6 +891,7 @@ mkConApp :: DataCon -> [Arg b] -> Expr b mkApps f args = foldl App f args mkTyApps f args = foldl (\ e a -> App e (Type a)) f args +mkCoApps f args = foldl (\ e a -> App e (Coercion a)) f args mkVarApps f vars = foldl (\ e a -> App e (varToCoreExpr a)) f vars mkConApp con args = mkApps (Var (dataConWorkId con)) args @@ -956,10 +962,16 @@ mkLets binds body = foldr Let body binds mkTyBind :: TyVar -> Type -> CoreBind mkTyBind tv ty = NonRec tv (Type ty) +-- | Create a binding group where a type variable is bound to a type. Per "CoreSyn#type_let", +-- this can only be used to bind something in a non-recursive @let@ expression +mkCoBind :: CoVar -> Coercion -> CoreBind +mkCoBind cv co = NonRec cv (Coercion co) + -- | Convert a binder into either a 'Var' or 'Type' 'Expr' appropriately varToCoreExpr :: CoreBndr -> Expr b -varToCoreExpr v | isId v = Var v - | otherwise = Type (mkTyVarTy v) +varToCoreExpr v | isTyVar v = Type (mkTyVarTy v) + | isCoVar v = Coercion (mkCoVarCo v) + | otherwise = ASSERT( isId v ) Var v varsToCoreExprs :: [CoreBndr] -> [Expr b] varsToCoreExprs vs = map varToCoreExpr vs @@ -1025,7 +1037,7 @@ collectTyAndValBinders expr collectTyBinders expr = go [] expr where - go tvs (Lam b e) | isTyCoVar b = go (b:tvs) e + go tvs (Lam b e) | isTyVar b = go (b:tvs) e go tvs e = (reverse tvs, e) collectValBinders expr @@ -1076,15 +1088,23 @@ isRuntimeVar = isId isRuntimeArg :: CoreExpr -> Bool isRuntimeArg = isValArg --- | Returns @False@ iff the expression is a 'Type' expression at its top level +-- | Returns @False@ iff the expression is a 'Type' or 'Coercion' +-- expression at its top level isValArg :: Expr b -> Bool -isValArg (Type _) = False -isValArg _ = True +isValArg e = not (isTypeArg e) + +-- | Returns @True@ iff the expression is a 'Type' or 'Coercion' +-- expression at its top level +isTyCoArg :: Expr b -> Bool +isTyCoArg (Type {}) = True +isTyCoArg (Coercion {}) = True +isTyCoArg _ = False --- | Returns @True@ iff the expression is a 'Type' expression at its top level +-- | Returns @True@ iff the expression is a 'Type' expression at its +-- top level. Note this does NOT include 'Coercion's. isTypeArg :: Expr b -> Bool -isTypeArg (Type _) = True -isTypeArg _ = False +isTypeArg (Type {}) = True +isTypeArg _ = False -- | The number of binders that bind values rather than types valBndrCount :: [CoreBndr] -> Int @@ -1114,9 +1134,10 @@ seqExpr (App f a) = seqExpr f `seq` seqExpr a seqExpr (Lam b e) = seqBndr b `seq` seqExpr e seqExpr (Let b e) = seqBind b `seq` seqExpr e seqExpr (Case e b t as) = seqExpr e `seq` seqBndr b `seq` seqType t `seq` seqAlts as -seqExpr (Cast e co) = seqExpr e `seq` seqType co +seqExpr (Cast e co) = seqExpr e `seq` seqCo co seqExpr (Note n e) = seqNote n `seq` seqExpr e -seqExpr (Type t) = seqType t +seqExpr (Type t) = seqType t +seqExpr (Coercion co) = seqCo co seqExprs :: [CoreExpr] -> () seqExprs [] = () @@ -1170,9 +1191,11 @@ data AnnExpr' bndr annot | AnnApp (AnnExpr bndr annot) (AnnExpr bndr annot) | AnnCase (AnnExpr bndr annot) bndr Type [AnnAlt bndr annot] | AnnLet (AnnBind bndr annot) (AnnExpr bndr annot) - | AnnCast (AnnExpr bndr annot) Coercion + | AnnCast (AnnExpr bndr annot) (annot, Coercion) + -- Put an annotation on the (root of) the coercion | AnnNote Note (AnnExpr bndr annot) | AnnType Type + | AnnCoercion Coercion -- | A clone of the 'Alt' type but allowing annotation at every tree node type AnnAlt bndr annot = (AltCon, [bndr], AnnExpr bndr annot) @@ -1199,12 +1222,13 @@ deAnnotate :: AnnExpr bndr annot -> Expr bndr deAnnotate (_, e) = deAnnotate' e deAnnotate' :: AnnExpr' bndr annot -> Expr bndr -deAnnotate' (AnnType t) = Type t +deAnnotate' (AnnType t) = Type t +deAnnotate' (AnnCoercion co) = Coercion co deAnnotate' (AnnVar v) = Var v deAnnotate' (AnnLit lit) = Lit lit deAnnotate' (AnnLam binder body) = Lam binder (deAnnotate body) deAnnotate' (AnnApp fun arg) = App (deAnnotate fun) (deAnnotate arg) -deAnnotate' (AnnCast e co) = Cast (deAnnotate e) co +deAnnotate' (AnnCast e (_,co)) = Cast (deAnnotate e) co deAnnotate' (AnnNote note body) = Note note (deAnnotate body) deAnnotate' (AnnLet bind body) diff --git a/compiler/coreSyn/CoreTidy.lhs b/compiler/coreSyn/CoreTidy.lhs index 582f873d18..377bfd8c84 100644 --- a/compiler/coreSyn/CoreTidy.lhs +++ b/compiler/coreSyn/CoreTidy.lhs @@ -17,7 +17,7 @@ import CoreSyn import CoreArity import Id import IdInfo -import TcType( tidyType, tidyTyVarBndr ) +import TcType( tidyType, tidyCo, tidyTyVarBndr ) import Var import VarEnv import UniqFM @@ -55,11 +55,12 @@ tidyBind env (Rec prs) ------------ Expressions -------------- tidyExpr :: TidyEnv -> CoreExpr -> CoreExpr tidyExpr env (Var v) = Var (tidyVarOcc env v) -tidyExpr env (Type ty) = Type (tidyType env ty) +tidyExpr env (Type ty) = Type (tidyType env ty) +tidyExpr env (Coercion co) = Coercion (tidyCo env co) tidyExpr _ (Lit lit) = Lit lit tidyExpr env (App f a) = App (tidyExpr env f) (tidyExpr env a) tidyExpr env (Note n e) = Note (tidyNote env n) (tidyExpr env e) -tidyExpr env (Cast e co) = Cast (tidyExpr env e) (tidyType env co) +tidyExpr env (Cast e co) = Cast (tidyExpr env e) (tidyCo env co) tidyExpr env (Let b e) = tidyBind env b =: \ (env', b') -> @@ -125,7 +126,7 @@ tidyVarOcc (_, var_env) v = lookupVarEnv var_env v `orElse` v -- tidyBndr is used for lambda and case binders tidyBndr :: TidyEnv -> Var -> (TidyEnv, Var) tidyBndr env var - | isTyCoVar var = tidyTyVarBndr env var + | isTyVar var = tidyTyVarBndr env var | otherwise = tidyIdBndr env var tidyBndrs :: TidyEnv -> [Var] -> (TidyEnv, [Var]) diff --git a/compiler/coreSyn/CoreUnfold.lhs b/compiler/coreSyn/CoreUnfold.lhs index d1b9fa0412..5883013a06 100644 --- a/compiler/coreSyn/CoreUnfold.lhs +++ b/compiler/coreSyn/CoreUnfold.lhs @@ -60,6 +60,7 @@ import PrelNames import VarEnv ( mkInScopeSet ) import Bag import Util +import Pair import FastTypes import FastString import Outputable @@ -107,7 +108,7 @@ mkWwInlineRule id expr arity mkCompulsoryUnfolding :: CoreExpr -> Unfolding mkCompulsoryUnfolding expr -- Used for things that absolutely must be unfolded = mkCoreUnfolding InlineCompulsory True - expr 0 -- Arity of unfolding doesn't matter + (simpleOptExpr expr) 0 -- Arity of unfolding doesn't matter (UnfWhen unSaturatedOk boringCxtOk) mkInlineUnfolding :: Maybe Arity -> CoreExpr -> Unfolding @@ -348,11 +349,13 @@ sizeExpr bOMB_OUT_SIZE top_args expr size_up (Cast e _) = size_up e size_up (Note _ e) = size_up e size_up (Type _) = sizeZero -- Types cost nothing + size_up (Coercion _) = sizeZero size_up (Lit lit) = sizeN (litSize lit) size_up (Var f) = size_up_call f [] -- Make sure we get constructor -- discounts even on nullary constructors size_up (App fun (Type _)) = size_up fun + size_up (App fun (Coercion _)) = size_up fun size_up (App fun arg) = size_up arg `addSizeNSD` size_up_app fun [arg] @@ -408,7 +411,7 @@ sizeExpr bOMB_OUT_SIZE top_args expr ------------ -- size_up_app is used when there's ONE OR MORE value args size_up_app (App fun arg) args - | isTypeArg arg = size_up_app fun args + | isTyCoArg arg = size_up_app fun args | otherwise = size_up arg `addSizeNSD` size_up_app fun (arg:args) size_up_app (Var fun) args = size_up_call fun args @@ -1147,12 +1150,14 @@ interestingArg e = go e 0 conlike_unfolding = isConLikeUnfolding (idUnfolding v) go (Type _) _ = TrivArg - go (App fn (Type _)) n = go fn n + go (Coercion _) _ = TrivArg + go (App fn (Type _)) n = go fn n + go (App fn (Coercion _)) n = go fn n go (App fn _) n = go fn (n+1) go (Note _ a) n = go a n go (Cast e _) n = go e n go (Lam v e) n - | isTyCoVar v = go e n + | isTyVar v = go e n | n>0 = go e (n-1) | otherwise = ValueArg go (Let _ e) n = case go e n of { ValueArg -> ValueArg; _ -> NonTrivArg } @@ -1208,7 +1213,7 @@ exprIsConApp_maybe id_unf (Cast expr co) Nothing -> Nothing ; Just (dc, _dc_univ_args, dc_args) -> - let (_from_ty, to_ty) = coercionKind co + let Pair _from_ty to_ty = coercionKind co dc_tc = dataConTyCon dc in case splitTyConApp_maybe to_ty of { @@ -1228,41 +1233,28 @@ exprIsConApp_maybe id_unf (Cast expr co) dc_ex_tyvars = dataConExTyVars dc arg_tys = dataConRepArgTys dc - dc_eqs :: [(Type,Type)] -- All equalities from the DataCon - dc_eqs = [(mkTyVarTy tv, ty) | (tv,ty) <- dataConEqSpec dc] ++ - [getEqPredTys eq_pred | eq_pred <- dataConEqTheta dc] - - (ex_args, rest1) = splitAtList dc_ex_tyvars dc_args - (co_args, val_args) = splitAtList dc_eqs rest1 + (ex_args, val_args) = splitAtList dc_ex_tyvars dc_args -- Make the "theta" from Fig 3 of the paper gammas = decomposeCo tc_arity co - theta = zipOpenTvSubst (dc_univ_tyvars ++ dc_ex_tyvars) - (gammas ++ stripTypeArgs ex_args) - - -- Cast the existential coercion arguments - cast_co (ty1, ty2) (Type co) - = Type $ mkSymCoercion (substTy theta ty1) - `mkTransCoercion` co - `mkTransCoercion` (substTy theta ty2) - cast_co _ other_arg = pprPanic "cast_co" (ppr other_arg) - new_co_args = zipWith cast_co dc_eqs co_args - + theta = zipOpenCvSubst (dc_univ_tyvars ++ dc_ex_tyvars) + (gammas ++ map mkReflCo (stripTypeArgs ex_args)) + -- Cast the value arguments (which include dictionaries) new_val_args = zipWith cast_arg arg_tys val_args - cast_arg arg_ty arg = mkCoerce (substTy theta arg_ty) arg + cast_arg arg_ty arg = mkCoerce (liftCoSubst theta arg_ty) arg in #ifdef DEBUG let dump_doc = vcat [ppr dc, ppr dc_univ_tyvars, ppr dc_ex_tyvars, ppr arg_tys, ppr dc_args, ppr _dc_univ_args, ppr ex_args, ppr val_args] in - ASSERT2( coreEqType _from_ty (mkTyConApp dc_tc _dc_univ_args), dump_doc ) - ASSERT2( all isTypeArg (ex_args ++ co_args), dump_doc ) + ASSERT2( eqType _from_ty (mkTyConApp dc_tc _dc_univ_args), dump_doc ) + ASSERT2( all isTypeArg ex_args, dump_doc ) ASSERT2( equalLength val_args arg_tys, dump_doc ) #endif - Just (dc, to_tc_arg_tys, ex_args ++ new_co_args ++ new_val_args) + Just (dc, to_tc_arg_tys, ex_args ++ new_val_args) }} exprIsConApp_maybe id_unf expr @@ -1301,7 +1293,7 @@ exprIsConApp_maybe id_unf expr ----------- beta (Lam v body) pairs (arg : args) - | isTypeArg arg + | isTyCoArg arg = beta body ((v,arg):pairs) args beta (Lam {}) _ _ -- Un-saturated, or not a type lambda @@ -1313,10 +1305,10 @@ exprIsConApp_maybe id_unf expr subst = mkOpenSubst (mkInScopeSet (exprFreeVars fun)) pairs -- doc = vcat [ppr fun, ppr expr, ppr pairs, ppr args] - stripTypeArgs :: [CoreExpr] -> [Type] stripTypeArgs args = ASSERT2( all isTypeArg args, ppr args ) [ty | Type ty <- args] + -- We really do want isTypeArg here, not isTyCoArg! \end{code} Note [Unfolding DFuns] diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs index 70e1db7e2a..a0a229f6c6 100644 --- a/compiler/coreSyn/CoreUtils.lhs +++ b/compiler/coreSyn/CoreUtils.lhs @@ -16,7 +16,7 @@ Utility functions on @Core@ syntax -- | Commonly useful utilites for manipulating the Core language module CoreUtils ( -- * Constructing expressions - mkSCC, mkCoerce, mkCoerceI, + mkSCC, mkCoerce, bindNonRec, needsCaseBinding, mkAltExpr, mkPiType, mkPiTypes, @@ -45,7 +45,7 @@ module CoreUtils ( -- * Manipulating data constructors and types applyTypeToArgs, applyTypeToArg, - dataConOrigInstPat, dataConRepInstPat, dataConRepFSInstPat + dataConRepInstPat, dataConRepFSInstPat ) where #include "HsVersions.h" @@ -62,7 +62,6 @@ import DataCon import PrimOp import Id import IdInfo -import TcType ( isPredTy ) import Type import Coercion import TyCon @@ -73,6 +72,7 @@ import TysPrim import FastString import Maybes import Util +import Pair import Data.Word import Data.Bits \end{code} @@ -91,9 +91,10 @@ exprType :: CoreExpr -> Type -- really be said to have a type exprType (Var var) = idType var exprType (Lit lit) = literalType lit +exprType (Coercion co) = coercionType co exprType (Let _ body) = exprType body exprType (Case _ _ ty _) = ty -exprType (Cast _ co) = snd (coercionKind co) +exprType (Cast _ co) = pSnd (coercionKind co) exprType (Note _ e) = exprType e exprType (Lam binder expr) = mkPiType binder (exprType expr) exprType e@(App _ _) @@ -110,7 +111,7 @@ coreAltType (_,bs,rhs) where ty = exprType rhs free_tvs = tyVarsOfType ty - bad_binder b = isTyCoVar b && b `elemVarSet` free_tvs + bad_binder b = isTyVar b && b `elemVarSet` free_tvs coreAltsType :: [CoreAlt] -> Type -- ^ Returns the type of the first alternative, which should be the same as for all alternatives @@ -143,10 +144,10 @@ Various possibilities suggest themselves: we are doing here. It's not too expensive, I think. \begin{code} -mkPiType :: EvVar -> Type -> Type +mkPiType :: Var -> Type -> Type -- ^ Makes a @(->)@ type or a forall type, depending -- on whether it is given a type variable or a term variable. -mkPiTypes :: [EvVar] -> Type -> Type +mkPiTypes :: [Var] -> Type -> Type -- ^ 'mkPiType' for multiple type or value arguments mkPiType v ty @@ -172,11 +173,11 @@ applyTypeToArgs e op_ty (Type ty : args) go [ty] args where go rev_tys (Type ty : args) = go (ty:rev_tys) args - go rev_tys rest_args = applyTypeToArgs e op_ty' rest_args - where - op_ty' = applyTysD msg op_ty (reverse rev_tys) - msg = ptext (sLit "applyTypeToArgs") <+> - panic_msg e op_ty + go rev_tys rest_args = applyTypeToArgs e op_ty' rest_args + where + op_ty' = applyTysD msg op_ty (reverse rev_tys) + msg = ptext (sLit "applyTypeToArgs") <+> + panic_msg e op_ty applyTypeToArgs e op_ty (_ : args) = case (splitFunTy_maybe op_ty) of @@ -194,25 +195,22 @@ panic_msg e op_ty = pprCoreExpr e $$ ppr op_ty %************************************************************************ \begin{code} --- | Wrap the given expression in the coercion, dropping identity coercions and coalescing nested coercions -mkCoerceI :: CoercionI -> CoreExpr -> CoreExpr -mkCoerceI (IdCo _) e = e -mkCoerceI (ACo co) e = mkCoerce co e - --- | Wrap the given expression in the coercion safely, coalescing nested coercions +-- | Wrap the given expression in the coercion safely, dropping +-- identity coercions and coalescing nested coercions mkCoerce :: Coercion -> CoreExpr -> CoreExpr +mkCoerce co e | isReflCo co = e mkCoerce co (Cast expr co2) - = ASSERT(let { (from_ty, _to_ty) = coercionKind co; - (_from_ty2, to_ty2) = coercionKind co2} in - from_ty `coreEqType` to_ty2 ) - mkCoerce (mkTransCoercion co2 co) expr + = ASSERT(let { Pair from_ty _to_ty = coercionKind co; + Pair _from_ty2 to_ty2 = coercionKind co2} in + from_ty `eqType` to_ty2 ) + mkCoerce (mkTransCo co2 co) expr mkCoerce co expr - = let (from_ty, _to_ty) = coercionKind co in --- if to_ty `coreEqType` from_ty + = let Pair from_ty _to_ty = coercionKind co in +-- if to_ty `eqType` from_ty -- then expr -- else - WARN(not (from_ty `coreEqType` exprType expr), text "Trying to coerce" <+> text "(" <> ppr expr $$ text "::" <+> ppr (exprType expr) <> text ")" $$ ppr co $$ pprEqPred (coercionKind co)) + WARN(not (from_ty `eqType` exprType expr), text "Trying to coerce" <+> text "(" <> ppr expr $$ text "::" <+> ppr (exprType expr) <> text ")" $$ ppr co $$ pprEqPred (coercionKind co)) (Cast expr co) \end{code} @@ -415,7 +413,8 @@ discount. \begin{code} exprIsTrivial :: CoreExpr -> Bool exprIsTrivial (Var _) = True -- See Note [Variables are trivial] -exprIsTrivial (Type _) = True +exprIsTrivial (Type _) = True +exprIsTrivial (Coercion _) = True exprIsTrivial (Lit lit) = litIsTrivial lit exprIsTrivial (App e arg) = not (isRuntimeArg arg) && exprIsTrivial e exprIsTrivial (Note _ e) = exprIsTrivial e -- See Note [SCCs are trivial] @@ -469,10 +468,11 @@ exprIsDupable e = isJust (go dupAppSize e) where go :: Int -> CoreExpr -> Maybe Int - go n (Type {}) = Just n - go n (Var {}) = decrement n - go n (Note _ e) = go n e - go n (Cast e _) = go n e + go n (Type {}) = Just n + go n (Coercion {}) = Just n + go n (Var {}) = decrement n + go n (Note _ e) = go n e + go n (Cast e _) = go n e go n (App f a) | Just n' <- go n a = go n' f go n (Lit lit) | litIsDupable lit = decrement n go _ _ = Nothing @@ -540,13 +540,14 @@ exprIsExpandable = exprIsCheap' isExpandableApp -- See Note [CONLIKE pragma] in type CheapAppFun = Id -> Int -> Bool exprIsCheap' :: CheapAppFun -> CoreExpr -> Bool -exprIsCheap' _ (Lit _) = True -exprIsCheap' _ (Type _) = True -exprIsCheap' _ (Var _) = True -exprIsCheap' good_app (Note _ e) = exprIsCheap' good_app e -exprIsCheap' good_app (Cast e _) = exprIsCheap' good_app e -exprIsCheap' good_app (Lam x e) = isRuntimeVar x - || exprIsCheap' good_app e +exprIsCheap' _ (Lit _) = True +exprIsCheap' _ (Type _) = True +exprIsCheap' _ (Coercion _) = True +exprIsCheap' _ (Var _) = True +exprIsCheap' good_app (Note _ e) = exprIsCheap' good_app e +exprIsCheap' good_app (Cast e _) = exprIsCheap' good_app e +exprIsCheap' good_app (Lam x e) = isRuntimeVar x + || exprIsCheap' good_app e exprIsCheap' good_app (Case e _ _ alts) = exprIsCheap' good_app e && and [exprIsCheap' good_app rhs | (_,_,rhs) <- alts] @@ -684,8 +685,9 @@ it's applied only to dictionaries. -- We can only do this if the @y + 1@ is ok for speculation: it has no -- side effects, and can't diverge or raise an exception. exprOkForSpeculation :: CoreExpr -> Bool -exprOkForSpeculation (Lit _) = True -exprOkForSpeculation (Type _) = True +exprOkForSpeculation (Lit _) = True +exprOkForSpeculation (Type _) = True +exprOkForSpeculation (Coercion _) = True exprOkForSpeculation (Var v) | isTickBoxOp v = False -- Tick boxes are *not* suitable for speculation @@ -865,12 +867,14 @@ exprIsHNFlike is_con is_con_unf = is_hnf_like -- we could get an infinite loop is_hnf_like (Lit _) = True - is_hnf_like (Type _) = True -- Types are honorary Values; + is_hnf_like (Type _) = True -- Types are honorary Values; -- we don't mind copying them + is_hnf_like (Coercion _) = True -- Same for coercions is_hnf_like (Lam b e) = isRuntimeVar b || is_hnf_like e is_hnf_like (Note _ e) = is_hnf_like e is_hnf_like (Cast e _) = is_hnf_like e - is_hnf_like (App e (Type _)) = is_hnf_like e + is_hnf_like (App e (Type _)) = is_hnf_like e + is_hnf_like (App e (Coercion _)) = is_hnf_like e is_hnf_like (App e a) = app_is_value e [a] is_hnf_like (Let _ e) = is_hnf_like e -- Lazy let(rec)s don't affect us is_hnf_like _ = False @@ -896,36 +900,26 @@ exprIsHNFlike is_con is_con_unf = is_hnf_like These InstPat functions go here to avoid circularity between DataCon and Id \begin{code} -dataConRepInstPat, dataConOrigInstPat :: [Unique] -> DataCon -> [Type] -> ([TyVar], [CoVar], [Id]) -dataConRepFSInstPat :: [FastString] -> [Unique] -> DataCon -> [Type] -> ([TyVar], [CoVar], [Id]) +dataConRepInstPat :: [Unique] -> DataCon -> [Type] -> ([TyVar], [Id]) +dataConRepFSInstPat :: [FastString] -> [Unique] -> DataCon -> [Type] -> ([TyVar], [Id]) -dataConRepInstPat = dataConInstPat dataConRepArgTys (repeat ((fsLit "ipv"))) -dataConRepFSInstPat = dataConInstPat dataConRepArgTys -dataConOrigInstPat = dataConInstPat dc_arg_tys (repeat ((fsLit "ipv"))) - where - dc_arg_tys dc = map mkPredTy (dataConEqTheta dc) ++ map mkPredTy (dataConDictTheta dc) ++ dataConOrigArgTys dc - -- Remember to include the existential dictionaries - -dataConInstPat :: (DataCon -> [Type]) -- function used to find arg tys - -> [FastString] -- A long enough list of FSs to use for names - -> [Unique] -- An equally long list of uniques, at least one for each binder - -> DataCon - -> [Type] -- Types to instantiate the universally quantified tyvars - -> ([TyVar], [CoVar], [Id]) -- Return instantiated variables +dataConRepInstPat = dataConInstPat (repeat ((fsLit "ipv"))) +dataConRepFSInstPat = dataConInstPat + +dataConInstPat :: [FastString] -- A long enough list of FSs to use for names + -> [Unique] -- An equally long list of uniques, at least one for each binder + -> DataCon + -> [Type] -- Types to instantiate the universally quantified tyvars + -> ([TyVar], [Id]) -- Return instantiated variables -- dataConInstPat arg_fun fss us con inst_tys returns a triple --- (ex_tvs, co_tvs, arg_ids), +-- (ex_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 --- The co_tvs include both GADT equalities (dcEqSpec) and --- programmer-specified equalities (dcEqTheta) --- -- arg_ids are indended to be used as binders for value arguments, -- and their types have been instantiated with inst_tys and ex_tys --- The arg_ids include both dicts (dcDictTheta) and --- programmer-specified arguments (after rep-ing) (deRepArgTys) +-- The arg_ids include both evidence and +-- programmer-specified arguments (both after rep-ing) -- -- Example. -- The following constructor T1 @@ -940,29 +934,22 @@ dataConInstPat :: (DataCon -> [Type]) -- function used to find arg tys -- -- dataConInstPat fss us T1 (a1',b') will return -- --- ([a1'', b''], [c :: (a1', b')~(a1'', b'')], [x :: Int, y :: b'']) +-- ([a1'', b''], [c :: (a1', b')~(a1'', b''), x :: Int, y :: b'']) -- -- where the double-primed variables are created with the FastStrings and -- Uniques given as fss and us -dataConInstPat arg_fun fss uniqs con inst_tys - = (ex_bndrs, co_bndrs, arg_ids) +dataConInstPat fss uniqs con inst_tys + = (ex_bndrs, arg_ids) where univ_tvs = dataConUnivTyVars con ex_tvs = dataConExTyVars con - arg_tys = arg_fun con - eq_spec = dataConEqSpec con - eq_theta = dataConEqTheta con - eq_preds = eqSpecPreds eq_spec ++ eq_theta + arg_tys = dataConRepArgTys con n_ex = length ex_tvs - n_co = length eq_preds -- split the Uniques and FastStrings - (ex_uniqs, uniqs') = splitAt n_ex uniqs - (co_uniqs, id_uniqs) = splitAt n_co uniqs' - - (ex_fss, fss') = splitAt n_ex fss - (co_fss, id_fss) = splitAt n_co fss' + (ex_uniqs, id_uniqs) = splitAt n_ex uniqs + (ex_fss, id_fss) = splitAt n_ex fss -- Make existential type variables ex_bndrs = zipWith3 mk_ex_var ex_uniqs ex_fss ex_tvs @@ -974,17 +961,9 @@ dataConInstPat arg_fun fss uniqs con inst_tys -- Make the instantiating substitution subst = zipOpenTvSubst (univ_tvs ++ ex_tvs) (inst_tys ++ map mkTyVarTy ex_bndrs) - -- Make new coercion vars, instantiating kind - co_bndrs = zipWith3 mk_co_var co_uniqs co_fss eq_preds - mk_co_var uniq fs eq_pred = mkCoVar new_name co_kind - where - new_name = mkSysTvName uniq fs - co_kind = substTy subst (mkPredTy eq_pred) - - -- make value vars, instantiating types - mk_id_var uniq fs ty = mkUserLocal (mkVarOccFS fs) uniq (substTy subst ty) noSrcSpan + -- Make value vars, instantiating types + mk_id_var uniq fs ty = mkUserLocal (mkVarOccFS fs) uniq (Type.substTy subst ty) noSrcSpan arg_ids = zipWith3 mk_id_var id_uniqs id_fss arg_tys - \end{code} %************************************************************************ @@ -1003,7 +982,8 @@ cheapEqExpr :: Expr b -> Expr b -> Bool cheapEqExpr (Var v1) (Var v2) = v1==v2 cheapEqExpr (Lit lit1) (Lit lit2) = lit1 == lit2 -cheapEqExpr (Type t1) (Type t2) = t1 `coreEqType` t2 +cheapEqExpr (Type t1) (Type t2) = t1 `eqType` t2 +cheapEqExpr (Coercion c1) (Coercion c2) = c1 `coreEqCoercion` c2 cheapEqExpr (App f1 a1) (App f2 a2) = f1 `cheapEqExpr` f2 && a1 `cheapEqExpr` a2 @@ -1019,7 +999,8 @@ exprIsBig :: Expr b -> Bool -- ^ Returns @True@ of expressions that are too big to be compared by 'cheapEqExpr' exprIsBig (Lit _) = False exprIsBig (Var _) = False -exprIsBig (Type _) = False +exprIsBig (Type _) = False +exprIsBig (Coercion _) = False exprIsBig (Lam _ e) = exprIsBig e exprIsBig (App f a) = exprIsBig f || exprIsBig a exprIsBig (Cast e _) = exprIsBig e -- Hopefully coercions are not too big! @@ -1061,14 +1042,15 @@ eqExprX id_unfolding_fun env e1 e2 , Just e2' <- expandUnfolding_maybe (id_unfolding_fun (lookupRnInScope env v2)) = go (nukeRnEnvR env) e1 e2' - go _ (Lit lit1) (Lit lit2) = lit1 == lit2 - go env (Type t1) (Type t2) = tcEqTypeX env t1 t2 - go env (Cast e1 co1) (Cast e2 co2) = tcEqTypeX env co1 co2 && go env e1 e2 + go _ (Lit lit1) (Lit lit2) = lit1 == lit2 + go env (Type t1) (Type t2) = eqTypeX env t1 t2 + go env (Coercion co1) (Coercion co2) = coreEqCoercion2 env co1 co2 + go env (Cast e1 co1) (Cast e2 co2) = coreEqCoercion2 env co1 co2 && go env e1 e2 go env (App f1 a1) (App f2 a2) = go env f1 f2 && go env a1 a2 go env (Note n1 e1) (Note n2 e2) = go_note n1 n2 && go env e1 e2 go env (Lam b1 e1) (Lam b2 e2) - = tcEqTypeX env (varType b1) (varType b2) -- False for Id/TyVar combination + = eqTypeX env (varType b1) (varType b2) -- False for Id/TyVar combination && go (rnBndr2 env b1 b2) e1 e2 go env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2) @@ -1084,7 +1066,7 @@ eqExprX id_unfolding_fun env e1 e2 go env (Case e1 b1 _ a1) (Case e2 b2 _ a2) = go env e1 e2 - && tcEqTypeX env (idType b1) (idType b2) + && eqTypeX env (idType b1) (idType b2) && all2 (go_alt (rnBndr2 env b1 b2)) a1 a2 go _ _ _ = False @@ -1128,16 +1110,17 @@ exprSize (App f a) = exprSize f + exprSize a exprSize (Lam b e) = varSize b + exprSize e exprSize (Let b e) = bindSize b + exprSize e exprSize (Case e b t as) = seqType t `seq` exprSize e + varSize b + 1 + foldr ((+) . altSize) 0 as -exprSize (Cast e co) = (seqType co `seq` 1) + exprSize e +exprSize (Cast e co) = (seqCo co `seq` 1) + exprSize e exprSize (Note n e) = noteSize n + exprSize e -exprSize (Type t) = seqType t `seq` 1 +exprSize (Type t) = seqType t `seq` 1 +exprSize (Coercion co) = seqCo co `seq` 1 noteSize :: Note -> Int noteSize (SCC cc) = cc `seq` 1 noteSize (CoreNote s) = s `seq` 1 -- hdaume: core annotations varSize :: Var -> Int -varSize b | isTyCoVar b = 1 +varSize b | isTyVar b = 1 | otherwise = seqType (idType b) `seq` megaSeqIdInfo (idInfo b) `seq` 1 @@ -1187,30 +1170,23 @@ bndrStats v = oneTM `plusCS` tyStats (varType v) exprStats :: CoreExpr -> CoreStats exprStats (Var {}) = oneTM exprStats (Lit {}) = oneTM -exprStats (App f (Type t))= tyCoStats (exprType f) t +exprStats (Type t) = tyStats t +exprStats (Coercion c) = coStats c exprStats (App f a) = exprStats f `plusCS` exprStats a exprStats (Lam b e) = bndrStats b `plusCS` exprStats e exprStats (Let b e) = bindStats b `plusCS` exprStats e exprStats (Case e b _ as) = exprStats e `plusCS` bndrStats b `plusCS` sumCS altStats as exprStats (Cast e co) = coStats co `plusCS` exprStats e exprStats (Note _ e) = exprStats e -exprStats (Type ty) = zeroCS { cs_ty = typeSize ty } - -- Ugh (might be a co) altStats :: CoreAlt -> CoreStats altStats (_, bs, r) = sumCS bndrStats bs `plusCS` exprStats r -tyCoStats :: Type -> Type -> CoreStats -tyCoStats fun_ty arg - = case splitForAllTy_maybe fun_ty of - Just (tv,_) | isCoVar tv -> coStats arg - _ -> tyStats arg - tyStats :: Type -> CoreStats tyStats ty = zeroCS { cs_ty = typeSize ty } coStats :: Coercion -> CoreStats -coStats co = zeroCS { cs_co = typeSize co } +coStats co = zeroCS { cs_co = coercionSize co } \end{code} %************************************************************************ @@ -1252,15 +1228,17 @@ hash_expr env (Lam b e) = hash_expr (extend_env env b) e hash_expr _ (Type _) = WARN(True, text "hash_expr: type") 1 -- Shouldn't happen. Better to use WARN than trace, because trace -- prevents the CPR optimisation kicking in for hash_expr. +hash_expr _ (Coercion _) = WARN(True, text "hash_expr: coercion") 1 fast_hash_expr :: HashEnv -> CoreExpr -> Word32 -fast_hash_expr env (Var v) = hashVar env v -fast_hash_expr env (Type t) = fast_hash_type env t -fast_hash_expr _ (Lit lit) = fromIntegral (hashLiteral lit) -fast_hash_expr env (Cast e _) = fast_hash_expr env e -fast_hash_expr env (Note _ e) = fast_hash_expr env e -fast_hash_expr env (App _ a) = fast_hash_expr env a -- A bit idiosyncratic ('a' not 'f')! -fast_hash_expr _ _ = 1 +fast_hash_expr env (Var v) = hashVar env v +fast_hash_expr env (Type t) = fast_hash_type env t +fast_hash_expr env (Coercion co) = fast_hash_co env co +fast_hash_expr _ (Lit lit) = fromIntegral (hashLiteral lit) +fast_hash_expr env (Cast e _) = fast_hash_expr env e +fast_hash_expr env (Note _ e) = fast_hash_expr env e +fast_hash_expr env (App _ a) = fast_hash_expr env a -- A bit idiosyncratic ('a' not 'f')! +fast_hash_expr _ _ = 1 fast_hash_type :: HashEnv -> Type -> Word32 fast_hash_type env ty @@ -1269,6 +1247,13 @@ fast_hash_type env ty in foldr (\t n -> fast_hash_type env t + n) hash_tc tys | otherwise = 1 +fast_hash_co :: HashEnv -> Coercion -> Word32 +fast_hash_co env co + | Just cv <- getCoVar_maybe co = hashVar env cv + | Just (tc,cos) <- splitTyConAppCo_maybe co = let hash_tc = fromIntegral (hashName (tyConName tc)) + in foldr (\c n -> fast_hash_co env c + n) hash_tc cos + | otherwise = 1 + extend_env :: HashEnv -> Var -> (Int, VarEnv Int) extend_env (n,env) b = (n+1, extendVarEnv env b n) @@ -1368,18 +1353,18 @@ need to address that here. \begin{code} tryEtaReduce :: [Var] -> CoreExpr -> Maybe CoreExpr tryEtaReduce bndrs body - = go (reverse bndrs) body (IdCo (exprType body)) + = go (reverse bndrs) body (mkReflCo (exprType body)) where incoming_arity = count isId bndrs go :: [Var] -- Binders, innermost first, types [a3,a2,a1] -> CoreExpr -- Of type tr - -> CoercionI -- Of type tr ~ ts + -> Coercion -- Of type tr ~ ts -> Maybe CoreExpr -- Of type a1 -> a2 -> a3 -> ts -- See Note [Eta reduction with casted arguments] -- for why we have an accumulating coercion go [] fun co - | ok_fun fun = Just (mkCoerceI co fun) + | ok_fun fun = Just (mkCoerce co fun) go (b : bs) (App fun arg) co | Just co' <- ok_arg b arg co @@ -1390,7 +1375,7 @@ tryEtaReduce bndrs body --------------- -- Note [Eta reduction conditions] ok_fun (App fun (Type ty)) - | not (any (`elemVarSet` tyVarsOfType ty) bndrs) + | not (any (`elemVarSet` tyVarsOfType ty) bndrs) = ok_fun fun ok_fun (Var fun_id) = not (fun_id `elem` bndrs) @@ -1406,22 +1391,22 @@ tryEtaReduce bndrs body | otherwise = idArity fun --------------- - ok_lam v = isTyCoVar v || isDictId v + ok_lam v = isTyVar v || isEvVar v --------------- - ok_arg :: Var -- Of type bndr_t - -> CoreExpr -- Of type arg_t - -> CoercionI -- Of kind (t1~t2) - -> Maybe CoercionI -- Of type (arg_t -> t1 ~ bndr_t -> t2) - -- (and similarly for tyvars, coercion args) + ok_arg :: Var -- Of type bndr_t + -> CoreExpr -- Of type arg_t + -> Coercion -- Of kind (t1~t2) + -> Maybe Coercion -- Of type (arg_t -> t1 ~ bndr_t -> t2) + -- (and similarly for tyvars, coercion args) -- See Note [Eta reduction with casted arguments] ok_arg bndr (Type ty) co | Just tv <- getTyVar_maybe ty - , bndr == tv = Just (mkForAllTyCoI tv co) + , bndr == tv = Just (mkForAllCo tv co) ok_arg bndr (Var v) co - | bndr == v = Just (mkFunTyCoI (IdCo (idType bndr)) co) + | bndr == v = Just (mkFunCo (mkReflCo (idType bndr)) co) ok_arg bndr (Cast (Var v) co_arg) co - | bndr == v = Just (mkFunTyCoI (ACo (mkSymCoercion co_arg)) co) + | bndr == v = Just (mkFunCo (mkSymCo co_arg) co) -- The simplifier combines multiple casts into one, -- so we can have a simple-minded pattern match here ok_arg _ _ _ = Nothing diff --git a/compiler/coreSyn/ExternalCore.lhs b/compiler/coreSyn/ExternalCore.lhs index 07a1dfbd8e..359419ca06 100644 --- a/compiler/coreSyn/ExternalCore.lhs +++ b/compiler/coreSyn/ExternalCore.lhs @@ -4,7 +4,6 @@ \begin{code} module ExternalCore where - data Module = Module Mname [Tdef] [Vdefg] @@ -51,21 +50,21 @@ data Alt type Vbind = (Var,Ty) type Tbind = (Tvar,Kind) +-- Internally, we represent types and coercions separately; but for +-- the purposes of external core (at least for now) it's still +-- convenient to collapse them into a single type. data Ty = Tvar Tvar | Tcon (Qual Tcon) | Tapp Ty Ty | Tforall Tbind Ty --- We distinguish primitive coercions --- (represented in GHC by wired-in names), because --- External Core treats them specially, so we have --- to print them out with special syntax. +-- We distinguish primitive coercions because External Core treats +-- them specially, so we have to print them out with special syntax. | TransCoercion Ty Ty | SymCoercion Ty | UnsafeCoercion Ty Ty | InstCoercion Ty Ty - | LeftCoercion Ty - | RightCoercion Ty + | NthCoercion Int Ty data Kind = Klifted diff --git a/compiler/coreSyn/MkCore.lhs b/compiler/coreSyn/MkCore.lhs index f1d42738a2..b6bc7d4b37 100644 --- a/compiler/coreSyn/MkCore.lhs +++ b/compiler/coreSyn/MkCore.lhs @@ -45,8 +45,7 @@ module MkCore ( #include "HsVersions.h" import Id -import IdInfo -import Var ( EvVar, mkWildCoVar, setTyVarUnique ) +import Var ( EvVar, setTyVarUnique ) import CoreSyn import CoreUtils ( exprType, needsCaseBinding, bindNonRec ) @@ -58,8 +57,10 @@ import PrelNames import TcType ( mkSigmaTy ) import Type +import Coercion import TysPrim import DataCon ( DataCon, dataConWorkId ) +import IdInfo ( vanillaIdInfo, setStrictnessInfo, setArityInfo ) import Demand import Name import Outputable @@ -102,6 +103,7 @@ mkCoreApp :: CoreExpr -> CoreExpr -> CoreExpr -- Check the invariant that the arg of an App is ok-for-speculation if unlifted -- See CoreSyn Note [CoreSyn let/app invariant] mkCoreApp fun (Type ty) = App fun (Type ty) +mkCoreApp fun (Coercion co) = App fun (Coercion co) mkCoreApp fun arg = ASSERT2( isFunTy fun_ty, ppr fun $$ ppr arg ) mk_val_app fun arg arg_ty res_ty where @@ -117,6 +119,7 @@ mkCoreApps orig_fun orig_args where go fun _ [] = fun go fun fun_ty (Type ty : args) = go (App fun (Type ty)) (applyTy fun_ty ty) args + go fun fun_ty (Coercion co : args) = go (App fun (Coercion co)) (applyCo fun_ty co) args go fun fun_ty (arg : args) = ASSERT2( isFunTy fun_ty, ppr fun_ty $$ ppr orig_fun $$ ppr orig_args ) go (mk_val_app fun arg arg_ty res_ty) res_ty args where @@ -148,8 +151,7 @@ mk_val_app fun arg arg_ty res_ty -- fragmet of it as the fun part of a 'mk_val_app'. mkWildEvBinder :: PredType -> EvVar -mkWildEvBinder pred@(EqPred {}) = mkWildCoVar (mkPredTy pred) -mkWildEvBinder pred = mkWildValBinder (mkPredTy pred) +mkWildEvBinder pred = mkWildValBinder (mkPredTy pred) -- | Make a /wildcard binder/. This is typically used when you need a binder -- that you expect to use only at a *binding* site. Do not use it at diff --git a/compiler/coreSyn/MkExternalCore.lhs b/compiler/coreSyn/MkExternalCore.lhs index cb784e8ab4..78df509dd6 100644 --- a/compiler/coreSyn/MkExternalCore.lhs +++ b/compiler/coreSyn/MkExternalCore.lhs @@ -13,6 +13,8 @@ import Module import CoreSyn import HscTypes import TyCon +-- import Class +-- import TysPrim( eqPredPrimTyCon ) import TypeRep import Type import PprExternalCore () -- Instances @@ -78,10 +80,7 @@ collect_tdefs tcon tdefs where tdef | isNewTyCon tcon = C.Newtype (qtc tcon) - (case newTyConCo_maybe tcon of - Just co -> qtc co - Nothing -> pprPanic ("MkExternalCore: newtype tcon\ - should have a coercion: ") (ppr tcon)) + (qcc (newTyConCo tcon)) (map make_tbind tyvars) (make_ty (snd (newTyConRhs tcon))) | otherwise = @@ -94,6 +93,8 @@ collect_tdefs _ tdefs = tdefs qtc :: TyCon -> C.Qual C.Tcon qtc = make_con_qid . tyConName +qcc :: CoAxiom -> C.Qual C.Tcon +qcc = make_con_qid . co_ax_name make_cdef :: DataCon -> C.Cdef make_cdef dcon = C.Constr dcon_name existentials tys @@ -142,15 +143,16 @@ make_exp (Var v) = do make_exp (Lit (MachLabel s _ _)) = return $ C.Label (unpackFS s) make_exp (Lit l) = return $ C.Lit (make_lit l) make_exp (App e (Type t)) = make_exp e >>= (\ b -> return $ C.Appt b (make_ty t)) +make_exp (App _e (Coercion _co)) = error "make_exp (App _ (Coercion _))" -- TODO make_exp (App e1 e2) = do rator <- make_exp e1 rand <- make_exp e2 return $ C.App rator rand -make_exp (Lam v e) | isTyCoVar v = make_exp e >>= (\ b -> +make_exp (Lam v e) | isTyVar v = make_exp e >>= (\ b -> return $ C.Lam (C.Tb (make_tbind v)) b) make_exp (Lam v e) | otherwise = make_exp e >>= (\ b -> return $ C.Lam (C.Vb (make_vbind v)) b) -make_exp (Cast e co) = make_exp e >>= (\ b -> return $ C.Cast b (make_ty co)) +make_exp (Cast e co) = make_exp e >>= (\ b -> return $ C.Cast b (make_co co)) make_exp (Let b e) = do vd <- make_vdef False b body <- make_exp e @@ -170,7 +172,7 @@ make_alt (DataAlt dcon, vs, e) = do (map make_tbind tbs) (map make_vbind vbs) newE - where (tbs,vbs) = span isTyCoVar vs + where (tbs,vbs) = span isTyVar vs make_alt (LitAlt l,_,e) = make_exp e >>= (return . (C.Alit (make_lit l))) make_alt (DEFAULT,[],e) = make_exp e >>= (return . C.Adefault) -- This should never happen, as the DEFAULT alternative binds no variables, @@ -229,29 +231,12 @@ make_ty' (TyConApp tc ts) = make_tyConApp tc ts make_ty' (PredTy p) = make_ty (predTypeRep p) make_tyConApp :: TyCon -> [Type] -> C.Ty -make_tyConApp tc [t1, t2] | tc == transCoercionTyCon = - C.TransCoercion (make_ty t1) (make_ty t2) -make_tyConApp tc [t] | tc == symCoercionTyCon = - C.SymCoercion (make_ty t) -make_tyConApp tc [t1, t2] | tc == unsafeCoercionTyCon = - C.UnsafeCoercion (make_ty t1) (make_ty t2) -make_tyConApp tc [t] | tc == leftCoercionTyCon = - C.LeftCoercion (make_ty t) -make_tyConApp tc [t] | tc == rightCoercionTyCon = - C.RightCoercion (make_ty t) -make_tyConApp tc [t1, t2] | tc == instCoercionTyCon = - C.InstCoercion (make_ty t1) (make_ty t2) --- this fails silently if we have an application --- of a wired-in coercion tycon to the wrong number of args. --- Not great... make_tyConApp tc ts = foldl C.Tapp (C.Tcon (qtc tc)) (map make_ty ts) - make_kind :: Kind -> C.Kind -make_kind (PredTy p) | isEqPred p = C.Keq (make_ty t1) (make_ty t2) - where (t1, t2) = getEqPredTys p +make_kind (PredTy (EqPred t1 t2)) = C.Keq (make_ty t1) (make_ty t2) make_kind (FunTy k1 k2) = C.Karrow (make_kind k1) (make_kind k2) make_kind k | isLiftedTypeKind k = C.Klifted @@ -299,6 +284,25 @@ make_var_qid force_unqual = make_qid force_unqual True make_con_qid :: Name -> C.Qual C.Id make_con_qid = make_qid False False +make_co :: Coercion -> C.Ty +make_co (Refl ty) = make_ty ty +make_co (TyConAppCo tc cos) = make_conAppCo (qtc tc) cos +make_co (AppCo c1 c2) = C.Tapp (make_co c1) (make_co c2) +make_co (ForAllCo tv co) = C.Tforall (make_tbind tv) (make_co co) +make_co (CoVarCo cv) = C.Tvar (make_var_id (coVarName cv)) +make_co (AxiomInstCo cc cos) = make_conAppCo (qcc cc) cos +make_co (UnsafeCo t1 t2) = C.UnsafeCoercion (make_ty t1) (make_ty t2) +make_co (SymCo co) = C.SymCoercion (make_co co) +make_co (TransCo c1 c2) = C.TransCoercion (make_co c1) (make_co c2) +make_co (NthCo d co) = C.NthCoercion d (make_co co) +make_co (InstCo co ty) = C.InstCoercion (make_co co) (make_ty ty) + +-- Used for both tycon app coercions and axiom instantiations. +make_conAppCo :: C.Qual C.Tcon -> [Coercion] -> C.Ty +make_conAppCo con cos = + foldl C.Tapp (C.Tcon con) + (map make_co cos) + ------- isALocal :: Name -> CoreM Bool isALocal vName = do diff --git a/compiler/coreSyn/PprCore.lhs b/compiler/coreSyn/PprCore.lhs index 041b842b81..e9452dcb73 100644 --- a/compiler/coreSyn/PprCore.lhs +++ b/compiler/coreSyn/PprCore.lhs @@ -106,7 +106,9 @@ ppr_expr :: OutputableBndr b => (SDoc -> SDoc) -> Expr b -> SDoc -- The function adds parens in context that need -- an atomic value (e.g. function args) -ppr_expr add_par (Type ty) = add_par (ptext (sLit "TYPE") <+> ppr ty) -- Wierd +ppr_expr add_par (Type ty) = add_par (ptext (sLit "TYPE") <+> ppr ty) -- Wierd + +ppr_expr add_par (Coercion co) = add_par (ptext (sLit "CO") <+> ppr co) ppr_expr _ (Var name) = ppr name ppr_expr _ (Lit lit) = ppr lit @@ -255,8 +257,8 @@ pprArg :: OutputableBndr a => Expr a -> SDoc pprArg (Type ty) | opt_SuppressTypeApplications = empty | otherwise = ptext (sLit "@") <+> pprParendType ty - -pprArg expr = pprParendExpr expr +pprArg (Coercion co) = ptext (sLit "@~") <+> pprParendCo co +pprArg expr = pprParendExpr expr \end{code} Other printing bits-and-bobs used with the general @pprCoreBinding@ @@ -268,7 +270,7 @@ instance OutputableBndr Var where pprCoreBinder :: BindingSite -> Var -> SDoc pprCoreBinder LetBind binder - | isTyCoVar binder = pprKindedTyVarBndr binder + | isTyVar binder = pprKindedTyVarBndr binder | otherwise = pprTypedBinder binder $$ ppIdInfo binder (idInfo binder) @@ -279,7 +281,7 @@ pprCoreBinder bind_site bndr pprUntypedBinder :: Var -> SDoc pprUntypedBinder binder - | isTyCoVar binder = ptext (sLit "@") <+> ppr binder -- NB: don't print kind + | isTyVar binder = ptext (sLit "@") <+> ppr binder -- NB: don't print kind | otherwise = pprIdBndr binder pprTypedLCBinder :: BindingSite -> Bool -> Var -> SDoc @@ -287,7 +289,7 @@ pprTypedLCBinder :: BindingSite -> Bool -> Var -> SDoc pprTypedLCBinder bind_site debug_on var | not debug_on && isDeadBinder var = char '_' | not debug_on, CaseBind <- bind_site = pprUntypedBinder var -- No parens, no kind info - | isTyCoVar var = parens (pprKindedTyVarBndr var) + | isTyVar var = parens (pprKindedTyVarBndr var) | otherwise = parens (hang (pprIdBndr var) 2 (vcat [ dcolon <+> pprType (idType var), pp_unf])) where @@ -298,7 +300,7 @@ pprTypedLCBinder bind_site debug_on var pprTypedBinder :: Var -> SDoc -- Print binder with a type or kind signature (not paren'd) pprTypedBinder binder - | isTyCoVar binder = pprKindedTyVarBndr binder + | isTyVar binder = pprKindedTyVarBndr binder | opt_SuppressTypeSignatures = empty | otherwise = hang (pprIdBndr binder) 2 (dcolon <+> pprType (idType binder)) diff --git a/compiler/coreSyn/PprExternalCore.lhs b/compiler/coreSyn/PprExternalCore.lhs index 3c4b25e420..5303b0d1b6 100644 --- a/compiler/coreSyn/PprExternalCore.lhs +++ b/compiler/coreSyn/PprExternalCore.lhs @@ -106,10 +106,8 @@ pty (SymCoercion t) = sep [text "%sym", paty t] pty (UnsafeCoercion t1 t2) = sep [text "%unsafe", paty t1, paty t2] -pty (LeftCoercion t) = - sep [text "%left", paty t] -pty (RightCoercion t) = - sep [text "%right", paty t] +pty (NthCoercion n t) = + sep [text "%nth", int n, paty t] pty (InstCoercion t1 t2) = sep [text "%inst", paty t1, paty t2] pty t = pbty t |