+
+%************************************************************************
+%* *
+ exprIsConApp_maybe
+%* *
+%************************************************************************
+
+Note [exprIsConApp_maybe]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+exprIsConApp_maybe is a very important function. There are two principal
+uses:
+ * case e of { .... }
+ * cls_op e, where cls_op is a class operation
+
+In both cases you want to know if e is of form (C e1..en) where C is
+a data constructor.
+
+However e might not *look* as if
+
+\begin{code}
+-- | Returns @Just (dc, [t1..tk], [x1..xn])@ if the argument expression is
+-- a *saturated* constructor application of the form @dc t1..tk x1 .. xn@,
+-- where t1..tk are the *universally-qantified* type args of 'dc'
+exprIsConApp_maybe :: CoreExpr -> Maybe (DataCon, [Type], [CoreExpr])
+
+exprIsConApp_maybe (Note _ expr)
+ = exprIsConApp_maybe expr
+ -- We ignore all notes. For example,
+ -- case _scc_ "foo" (C a b) of
+ -- C a b -> e
+ -- should be optimised away, but it will be only if we look
+ -- through the SCC note.
+
+exprIsConApp_maybe (Cast expr co)
+ = -- Here we do the KPush reduction rule as described in the FC paper
+ -- The transformation applies iff we have
+ -- (C e1 ... en) `cast` co
+ -- where co :: (T t1 .. tn) ~ to_ty
+ -- The left-hand one must be a T, because exprIsConApp returned True
+ -- but the right-hand one might not be. (Though it usually will.)
+
+ case exprIsConApp_maybe expr of {
+ Nothing -> Nothing ;
+ Just (dc, _dc_univ_args, dc_args) ->
+
+ let (_from_ty, to_ty) = coercionKind co
+ dc_tc = dataConTyCon dc
+ in
+ case splitTyConApp_maybe to_ty of {
+ Nothing -> Nothing ;
+ Just (to_tc, to_tc_arg_tys)
+ | dc_tc /= to_tc -> Nothing
+ -- These two Nothing cases are possible; we might see
+ -- (C x y) `cast` (g :: T a ~ S [a]),
+ -- where S is a type function. In fact, exprIsConApp
+ -- will probably not be called in such circumstances,
+ -- but there't nothing wrong with it
+
+ | otherwise ->
+ let
+ tc_arity = tyConArity dc_tc
+ dc_univ_tyvars = dataConUnivTyVars dc
+ 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
+
+ -- 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
+
+ -- 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
+ 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( equalLength val_args arg_tys, dump_doc )
+#endif
+
+ Just (dc, to_tc_arg_tys, ex_args ++ new_co_args ++ new_val_args)
+ }}
+
+exprIsConApp_maybe expr
+ = analyse expr []
+ where
+ analyse (App fun arg) args = analyse fun (arg:args)
+ analyse fun@(Lam {}) args = beta fun [] args
+
+ analyse (Var fun) args
+ | Just con <- isDataConWorkId_maybe fun
+ , is_saturated
+ , let (univ_ty_args, rest_args) = splitAtList (dataConUnivTyVars con) args
+ = Just (con, stripTypeArgs univ_ty_args, rest_args)
+
+ -- Look through dictionary functions; see Note [Unfolding DFuns]
+ | DFunUnfolding con ops <- unfolding
+ , is_saturated
+ , let (dfun_tvs, _cls, dfun_res_tys) = tcSplitDFunTy (idType fun)
+ subst = zipOpenTvSubst dfun_tvs (stripTypeArgs (takeList dfun_tvs args))
+ = Just (con, substTys subst dfun_res_tys,
+ [mkApps op args | op <- ops])
+
+ -- Look through unfoldings, but only cheap ones, because
+ -- we are effectively duplicating the unfolding
+ | CoreUnfolding { uf_expandable = expand_me, uf_tmpl = rhs } <- unfolding
+ , expand_me = -- pprTrace "expanding" (ppr fun $$ ppr rhs) $
+ analyse rhs args
+ where
+ is_saturated = count isValArg args == idArity fun
+ unfolding = idUnfolding fun -- Does not look through loop breakers
+ -- ToDo: we *may* look through variables that are NOINLINE
+ -- in this phase, and that is really not right
+
+ analyse _ _ = Nothing
+
+ -----------
+ in_scope = mkInScopeSet (exprFreeVars expr)
+
+ -----------
+ beta (Lam v body) pairs (arg : args)
+ | isTypeArg arg
+ = beta body ((v,arg):pairs) args
+
+ beta (Lam {}) _ _ -- Un-saturated, or not a type lambda
+ = Nothing
+
+ beta fun pairs args
+ = case analyse (substExpr subst fun) args of
+ Nothing -> -- pprTrace "Bale out! exprIsConApp_maybe" doc $
+ Nothing
+ Just ans -> -- pprTrace "Woo-hoo! exprIsConApp_maybe" doc $
+ Just ans
+ where
+ subst = mkOpenSubst in_scope 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]
+\end{code}
+
+Note [Unfolding DFuns]
+~~~~~~~~~~~~~~~~~~~~~~
+DFuns look like
+
+ df :: forall a b. (Eq a, Eq b) -> Eq (a,b)
+ df a b d_a d_b = MkEqD (a,b) ($c1 a b d_a d_b)
+ ($c2 a b d_a d_b)
+
+So to split it up we just need to apply the ops $c1, $c2 etc
+to the very same args as the dfun. It takes a little more work
+to compute the type arguments to the dictionary constructor.
+