-%\r
-% (c) The University of Glasgow 2006\r
-%\r
-\r
-\begin{code}\r
-{-# OPTIONS_GHC -w #-}\r
-module OptCoercion (\r
- optCoercion\r
- ) where \r
-\r
-#include "HsVersions.h"\r
-\r
-import Unify ( tcMatchTy )\r
-import Coercion\r
-import Type\r
-import TypeRep\r
-import TyCon\r
-import Var\r
-import VarSet\r
-import VarEnv\r
-import PrelNames\r
-import StaticFlags ( opt_NoOptCoercion )\r
-import Util\r
-import Outputable\r
-\end{code}\r
-\r
-%************************************************************************\r
-%* *\r
- Optimising coercions \r
-%* *\r
-%************************************************************************\r
-\r
-Note [Subtle shadowing in coercions]\r
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\r
-Supose we optimising a coercion\r
- optCoercion (forall (co_X5:t1~t2). ...co_B1...)\r
-The co_X5 is a wild-card; the bound variable of a coercion for-all\r
-should never appear in the body of the forall. Indeed we often\r
-write it like this\r
- optCoercion ( (t1~t2) => ...co_B1... )\r
-\r
-Just because it's a wild-card doesn't mean we are free to choose\r
-whatever variable we like. For example it'd be wrong for optCoercion\r
-to return\r
- forall (co_B1:t1~t2). ...co_B1...\r
-because now the co_B1 (which is really free) has been captured, and\r
-subsequent substitutions will go wrong. That's why we can't use\r
-mkCoPredTy in the ForAll case, where this note appears. \r
-\r
-\begin{code}\r
-optCoercion :: TvSubst -> Coercion -> NormalCo\r
--- ^ optCoercion applies a substitution to a coercion, \r
--- *and* optimises it to reduce its size\r
-optCoercion env co \r
- | opt_NoOptCoercion = substTy env co\r
- | otherwise = opt_co env False co\r
-\r
-type NormalCo = Coercion\r
- -- Invariants: \r
- -- * The substitution has been fully applied\r
- -- * For trans coercions (co1 `trans` co2)\r
- -- co1 is not a trans, and neither co1 nor co2 is identity\r
- -- * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)\r
-\r
-type NormalNonIdCo = NormalCo -- Extra invariant: not the identity\r
-\r
-opt_co, opt_co' :: TvSubst\r
- -> Bool -- True <=> return (sym co)\r
- -> Coercion\r
- -> NormalCo \r
-opt_co = opt_co'\r
-\r
-{- Debuggery \r
-opt_co env sym co \r
--- = pprTrace "opt_co {" (ppr sym <+> ppr co) $\r
--- co1 `seq` \r
--- pprTrace "opt_co done }" (ppr co1) \r
--- WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (s1,t1) \r
--- $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )\r
- = WARN( not (coreEqType co1 simple_result), \r
- (text "env=" <+> ppr env) $$\r
- (text "input=" <+> ppr co) $$\r
- (text "simple=" <+> ppr simple_result) $$\r
- (text "opt=" <+> ppr co1) )\r
- co1\r
- where\r
- co1 = opt_co' env sym co\r
- same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2\r
- (s,t) = coercionKind (substTy env co)\r
- (s1,t1) | sym = (t,s)\r
- | otherwise = (s,t)\r
- (s2,t2) = coercionKind co1\r
-\r
- simple_result | sym = mkSymCoercion (substTy env co)\r
- | otherwise = substTy env co\r
--}\r
-\r
-opt_co' env sym (AppTy ty1 ty2) = mkAppTy (opt_co env sym ty1) (opt_co env sym ty2)\r
-opt_co' env sym (FunTy ty1 ty2) = FunTy (opt_co env sym ty1) (opt_co env sym ty2)\r
-opt_co' env sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co env sym) tys))\r
-opt_co' env sym (PredTy (IParam n ty)) = PredTy (IParam n (opt_co env sym ty))\r
-opt_co' _ _ co@(PredTy (EqPred {})) = pprPanic "optCoercion" (ppr co)\r
-\r
-opt_co' env sym co@(TyVarTy tv)\r
- | Just ty <- lookupTyVar env tv = opt_co' (zapTvSubstEnv env) sym ty\r
- | not (isCoVar tv) = co -- Identity; does not mention a CoVar\r
- | ty1 `coreEqType` ty2 = ty1 -- Identity; ..ditto..\r
- | not sym = co\r
- | otherwise = mkSymCoercion co\r
- where\r
- (ty1,ty2) = coVarKind tv\r
-\r
-opt_co' env sym (ForAllTy tv cor) \r
- | isTyVar tv = case substTyVarBndr env tv of\r
- (env', tv') -> ForAllTy tv' (opt_co' env' sym cor)\r
-\r
-opt_co' env sym co@(ForAllTy co_var cor) \r
- | isCoVar co_var \r
- = WARN( co_var `elemVarSet` tyVarsOfType cor, ppr co )\r
- ForAllTy co_var' cor'\r
- where\r
- (co1,co2) = coVarKind co_var\r
- co1' = opt_co' env sym co1\r
- co2' = opt_co' env sym co2\r
- cor' = opt_co' env sym cor\r
- co_var' = uniqAway (getTvInScope env) (mkWildCoVar (mkCoKind co1' co2'))\r
- -- See Note [Subtle shadowing in coercions]\r
-\r
-opt_co' env sym (TyConApp tc cos)\r
- | Just (arity, desc) <- isCoercionTyCon_maybe tc\r
- = mkAppTys (opt_co_tc_app env sym tc desc (take arity cos))\r
- (map (opt_co env sym) (drop arity cos))\r
- | otherwise\r
- = TyConApp tc (map (opt_co env sym) cos)\r
-\r
---------\r
-opt_co_tc_app :: TvSubst -> Bool -> TyCon -> CoTyConDesc -> [Coercion] -> NormalCo\r
--- Used for CoercionTyCons only\r
--- Arguments are *not* already simplified/substituted\r
-opt_co_tc_app env sym tc desc cos\r
- = case desc of\r
- CoAxiom {} -- Do *not* push sym inside top-level axioms\r
- -- e.g. if g is a top-level axiom\r
- -- g a : F a ~ a\r
- -- Then (sym (g ty)) /= g (sym ty) !!\r
- | sym -> mkSymCoercion the_co \r
- | otherwise -> the_co\r
- where\r
- the_co = TyConApp tc (map (opt_co env False) cos)\r
- -- Note that the_co does *not* have sym pushed into it\r
- \r
- CoTrans \r
- | sym -> opt_trans opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g\r
- | otherwise -> opt_trans opt_co1 opt_co2\r
-\r
- CoUnsafe\r
- | sym -> mkUnsafeCoercion ty2' ty1'\r
- | otherwise -> mkUnsafeCoercion ty1' ty2'\r
-\r
- CoSym -> opt_co env (not sym) co1\r
- CoLeft -> opt_lr fst\r
- CoRight -> opt_lr snd\r
- CoCsel1 -> opt_csel fstOf3\r
- CoCsel2 -> opt_csel sndOf3\r
- CoCselR -> opt_csel thirdOf3\r
-\r
- CoInst -- See if the first arg is already a forall\r
- -- ...then we can just extend the current substitution\r
- | Just (tv, co1_body) <- splitForAllTy_maybe co1\r
- -> opt_co (extendTvSubst env tv ty2') sym co1_body\r
-\r
- -- See if is *now* a forall\r
- | Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1\r
- -> substTyWith [tv] [ty2'] opt_co1_body -- An inefficient one-variable substitution\r
-\r
- | otherwise\r
- -> TyConApp tc [opt_co1, ty2']\r
-\r
- where\r
- (co1 : cos1) = cos\r
- (co2 : _) = cos1\r
-\r
- ty1' = substTy env co1\r
- ty2' = substTy env co2\r
-\r
- -- These opt_cos have the sym pushed into them\r
- opt_co1 = opt_co env sym co1\r
- opt_co2 = opt_co env sym co2\r
-\r
- the_unary_opt_co = TyConApp tc [opt_co1]\r
-\r
- opt_lr sel = case splitAppTy_maybe opt_co1 of\r
- Nothing -> the_unary_opt_co \r
- Just lr -> sel lr\r
- opt_csel sel = case splitCoPredTy_maybe opt_co1 of\r
- Nothing -> the_unary_opt_co \r
- Just lr -> sel lr\r
-\r
--------------\r
-opt_transL :: [NormalCo] -> [NormalCo] -> [NormalCo]\r
-opt_transL = zipWith opt_trans\r
-\r
-opt_trans :: NormalCo -> NormalCo -> NormalCo\r
-opt_trans co1 co2\r
- | isIdNormCo co1 = co2\r
- | otherwise = opt_trans1 co1 co2\r
-\r
-opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo\r
--- First arg is not the identity\r
-opt_trans1 co1 co2\r
- | isIdNormCo co2 = co1\r
- | otherwise = opt_trans2 co1 co2\r
-\r
-opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo\r
--- Neither arg is the identity\r
-opt_trans2 (TyConApp tc [co1a,co1b]) co2\r
- | tc `hasKey` transCoercionTyConKey\r
- = opt_trans1 co1a (opt_trans2 co1b co2)\r
-\r
-opt_trans2 co1 co2 \r
- | Just co <- opt_trans_rule co1 co2\r
- = co\r
-\r
-opt_trans2 co1 (TyConApp tc [co2a,co2b])\r
- | tc `hasKey` transCoercionTyConKey\r
- , Just co1_2a <- opt_trans_rule co1 co2a\r
- = if isIdNormCo co1_2a\r
- then co2b\r
- else opt_trans2 co1_2a co2b\r
-\r
-opt_trans2 co1 co2\r
- = mkTransCoercion co1 co2\r
-\r
-------\r
-opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo\r
-opt_trans_rule (TyConApp tc1 args1) (TyConApp tc2 args2)\r
- | tc1 == tc2\r
- = case isCoercionTyCon_maybe tc1 of\r
- Nothing \r
- -> Just (TyConApp tc1 (opt_transL args1 args2))\r
- Just (arity, desc) \r
- | arity == length args1\r
- -> opt_trans_rule_equal_tc desc args1 args2\r
- | otherwise\r
- -> case opt_trans_rule_equal_tc desc \r
- (take arity args1) \r
- (take arity args2) of\r
- Just co -> Just $ mkAppTys co $ \r
- opt_transL (drop arity args1) (drop arity args2)\r
- Nothing -> Nothing \r
- \r
--- Push transitivity inside apply\r
-opt_trans_rule co1 co2\r
- | Just (co1a, co1b) <- splitAppTy_maybe co1\r
- , Just (co2a, co2b) <- etaApp_maybe co2\r
- = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))\r
-\r
- | Just (co2a, co2b) <- splitAppTy_maybe co2\r
- , Just (co1a, co1b) <- etaApp_maybe co1\r
- = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))\r
-\r
--- Push transitivity inside (s~t)=>r\r
--- We re-use the CoVar rather than using mkCoPredTy\r
--- See Note [Subtle shadowing in coercions]\r
-opt_trans_rule co1 co2\r
- | Just (cv1,r1) <- splitForAllTy_maybe co1\r
- , isCoVar cv1\r
- , Just (s1,t1) <- coVarKind_maybe cv1\r
- , Just (s2,t2,r2) <- etaCoPred_maybe co2\r
- = Just (ForAllTy (mkCoVar (coVarName cv1) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))\r
- (opt_trans r1 r2))\r
-\r
- | Just (cv2,r2) <- splitForAllTy_maybe co2\r
- , isCoVar cv2\r
- , Just (s2,t2) <- coVarKind_maybe cv2\r
- , Just (s1,t1,r1) <- etaCoPred_maybe co1\r
- = Just (ForAllTy (mkCoVar (coVarName cv2) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))\r
- (opt_trans r1 r2))\r
-\r
--- Push transitivity inside forall\r
-opt_trans_rule co1 co2\r
- | Just (tv1,r1) <- splitTypeForAll_maybe co1\r
- , Just (tv2,r2) <- etaForAll_maybe co2\r
- , let r2' = substTyWith [tv2] [TyVarTy tv1] r2\r
- = Just (ForAllTy tv1 (opt_trans2 r1 r2'))\r
-\r
- | Just (tv2,r2) <- splitTypeForAll_maybe co2\r
- , Just (tv1,r1) <- etaForAll_maybe co1\r
- , let r1' = substTyWith [tv1] [TyVarTy tv2] r1\r
- = Just (ForAllTy tv1 (opt_trans2 r1' r2))\r
-\r
-opt_trans_rule co1 co2\r
-{- Omitting for now, because unsound\r
- | Just (sym1, (ax_tc1, ax1_args, ax_tvs, ax_lhs, ax_rhs)) <- co1_is_axiom_maybe\r
- , Just (sym2, (ax_tc2, ax2_args, _, _, _)) <- co2_is_axiom_maybe\r
- , ax_tc1 == ax_tc2\r
- , sym1 /= sym2\r
- = Just $\r
- if sym1 \r
- then substTyWith ax_tvs (opt_transL (map mkSymCoercion ax1_args) ax2_args) ax_rhs\r
- else substTyWith ax_tvs (opt_transL ax1_args (map mkSymCoercion ax2_args)) ax_lhs\r
--}\r
-\r
- | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- co1_is_axiom_maybe\r
- , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co2\r
- = Just $ \r
- if sym \r
- then mkSymCoercion $ TyConApp ax_tc (opt_transL (map mkSymCoercion cos) ax_args)\r
- else TyConApp ax_tc (opt_transL ax_args cos)\r
-\r
- | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- isAxiom_maybe co2\r
- , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co1\r
- = Just $ \r
- if sym \r
- then mkSymCoercion $ TyConApp ax_tc (opt_transL ax_args (map mkSymCoercion cos))\r
- else TyConApp ax_tc (opt_transL cos ax_args)\r
- where\r
- co1_is_axiom_maybe = isAxiom_maybe co1\r
- co2_is_axiom_maybe = isAxiom_maybe co2\r
-\r
-opt_trans_rule co1 co2 -- Identity rule\r
- | (ty1,_) <- coercionKind co1\r
- , (_,ty2) <- coercionKind co2\r
- , ty1 `coreEqType` ty2\r
- = Just ty2\r
-\r
-opt_trans_rule _ _ = Nothing\r
-\r
------------ \r
-isAxiom_maybe :: Coercion -> Maybe (Bool, (TyCon, [Coercion], [TyVar], Type, Type))\r
-isAxiom_maybe co\r
- | Just (tc, args) <- splitTyConApp_maybe co\r
- , Just (_, desc) <- isCoercionTyCon_maybe tc\r
- = case desc of\r
- CoAxiom { co_ax_tvs = tvs, co_ax_lhs = lhs, co_ax_rhs = rhs } \r
- -> Just (False, (tc, args, tvs, lhs, rhs))\r
- CoSym | (arg1:_) <- args \r
- -> case isAxiom_maybe arg1 of\r
- Nothing -> Nothing\r
- Just (sym, stuff) -> Just (not sym, stuff)\r
- _ -> Nothing\r
- | otherwise\r
- = Nothing\r
-\r
-matchesAxiomLhs :: [TyVar] -> Type -> Type -> Maybe [Type]\r
-matchesAxiomLhs tvs ty_tmpl ty \r
- = case tcMatchTy (mkVarSet tvs) ty_tmpl ty of\r
- Nothing -> Nothing\r
- Just subst -> Just (map (substTyVar subst) tvs)\r
-\r
------------ \r
-opt_trans_rule_equal_tc :: CoTyConDesc -> [Coercion] -> [Coercion] -> Maybe Coercion\r
--- Rules for Coercion TyCons only\r
-\r
--- Push transitivity inside instantiation\r
-opt_trans_rule_equal_tc desc [co1,ty1] [co2,ty2]\r
- | CoInst <- desc\r
- , ty1 `coreEqType` ty2\r
- , co1 `compatible_co` co2\r
- = Just (mkInstCoercion (opt_trans2 co1 co2) ty1) \r
-\r
-opt_trans_rule_equal_tc desc [co1] [co2]\r
- | CoLeft <- desc, is_compat = Just (mkLeftCoercion res_co)\r
- | CoRight <- desc, is_compat = Just (mkRightCoercion res_co)\r
- | CoCsel1 <- desc, is_compat = Just (mkCsel1Coercion res_co)\r
- | CoCsel2 <- desc, is_compat = Just (mkCsel2Coercion res_co)\r
- | CoCselR <- desc, is_compat = Just (mkCselRCoercion res_co)\r
- where\r
- is_compat = co1 `compatible_co` co2\r
- res_co = opt_trans2 co1 co2\r
-\r
-opt_trans_rule_equal_tc _ _ _ = Nothing\r
-\r
--------------\r
-compatible_co :: Coercion -> Coercion -> Bool\r
--- Check whether (co1 . co2) will be well-kinded\r
-compatible_co co1 co2\r
- = x1 `coreEqType` x2 \r
- where\r
- (_,x1) = coercionKind co1\r
- (x2,_) = coercionKind co2\r
-\r
--------------\r
-etaForAll_maybe :: Coercion -> Maybe (TyVar, Coercion)\r
--- Try to make the coercion be of form (forall tv. co)\r
-etaForAll_maybe co\r
- | Just (tv, r) <- splitForAllTy_maybe co\r
- , not (isCoVar tv) -- Check it is a *type* forall, not a (t1~t2)=>co\r
- = Just (tv, r)\r
-\r
- | (ty1,ty2) <- coercionKind co\r
- , Just (tv1, _) <- splitTypeForAll_maybe ty1\r
- , Just (tv2, _) <- splitTypeForAll_maybe ty2\r
- , tyVarKind tv1 `eqKind` tyVarKind tv2\r
- = Just (tv1, mkInstCoercion co (mkTyVarTy tv1))\r
-\r
- | otherwise\r
- = Nothing\r
-\r
-etaCoPred_maybe :: Coercion -> Maybe (Coercion, Coercion, Coercion)\r
-etaCoPred_maybe co \r
- | Just (s,t,r) <- splitCoPredTy_maybe co\r
- = Just (s,t,r)\r
- \r
- -- co :: (s1~t1)=>r1 ~ (s2~t2)=>r2\r
- | (ty1,ty2) <- coercionKind co -- We know ty1,ty2 have same kind\r
- , Just (s1,_,_) <- splitCoPredTy_maybe ty1\r
- , Just (s2,_,_) <- splitCoPredTy_maybe ty2\r
- , typeKind s1 `eqKind` typeKind s2 -- t1,t2 have same kinds\r
- = Just (mkCsel1Coercion co, mkCsel2Coercion co, mkCselRCoercion co)\r
- \r
- | otherwise\r
- = Nothing\r
-\r
-etaApp_maybe :: Coercion -> Maybe (Coercion, Coercion)\r
--- Split a coercion g :: t1a t1b ~ t2a t2b\r
--- into (left g, right g) if possible\r
-etaApp_maybe co\r
- | Just (co1, co2) <- splitAppTy_maybe co\r
- = Just (co1, co2)\r
-\r
- | (ty1,ty2) <- coercionKind co\r
- , Just (ty1a, _) <- splitAppTy_maybe ty1\r
- , Just (ty2a, _) <- splitAppTy_maybe ty2\r
- , typeKind ty1a `eqKind` typeKind ty2a\r
- = Just (mkLeftCoercion co, mkRightCoercion co)\r
-\r
- | otherwise\r
- = Nothing\r
-\r
--------------\r
-splitTypeForAll_maybe :: Type -> Maybe (TyVar, Type)\r
--- Returns Just only for a *type* forall, not a (t1~t2)=>co\r
-splitTypeForAll_maybe ty\r
- | Just (tv, rty) <- splitForAllTy_maybe ty\r
- , not (isCoVar tv)\r
- = Just (tv, rty)\r
-\r
- | otherwise\r
- = Nothing\r
-\r
--------------\r
-isIdNormCo :: NormalCo -> Bool\r
--- Cheap identity test: look for coercions with no coercion variables at all\r
--- So it'll return False for (sym g `trans` g)\r
-isIdNormCo ty = go ty\r
- where\r
- go (TyVarTy tv) = not (isCoVar tv)\r
- go (AppTy t1 t2) = go t1 && go t2\r
- go (FunTy t1 t2) = go t1 && go t2\r
- go (ForAllTy tv ty) = go (tyVarKind tv) && go ty\r
- go (TyConApp tc tys) = not (isCoercionTyCon tc) && all go tys\r
- go (PredTy (IParam _ ty)) = go ty\r
- go (PredTy (ClassP _ tys)) = all go tys\r
- go (PredTy (EqPred t1 t2)) = go t1 && go t2\r
-\end{code} \r
+%
+% (c) The University of Glasgow 2006
+%
+
+\begin{code}
+module OptCoercion ( optCoercion ) where
+
+#include "HsVersions.h"
+
+import Coercion
+import Type hiding( substTyVarBndr, substTy, extendTvSubst )
+import TyCon
+import Var
+import VarSet
+import VarEnv
+import StaticFlags ( opt_NoOptCoercion )
+import Outputable
+import Pair
+import Maybes( allMaybes )
+import FastString
+\end{code}
+
+%************************************************************************
+%* *
+ Optimising coercions
+%* *
+%************************************************************************
+
+Note [Subtle shadowing in coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Supose we optimising a coercion
+ optCoercion (forall (co_X5:t1~t2). ...co_B1...)
+The co_X5 is a wild-card; the bound variable of a coercion for-all
+should never appear in the body of the forall. Indeed we often
+write it like this
+ optCoercion ( (t1~t2) => ...co_B1... )
+
+Just because it's a wild-card doesn't mean we are free to choose
+whatever variable we like. For example it'd be wrong for optCoercion
+to return
+ forall (co_B1:t1~t2). ...co_B1...
+because now the co_B1 (which is really free) has been captured, and
+subsequent substitutions will go wrong. That's why we can't use
+mkCoPredTy in the ForAll case, where this note appears.
+
+\begin{code}
+optCoercion :: CvSubst -> Coercion -> NormalCo
+-- ^ optCoercion applies a substitution to a coercion,
+-- *and* optimises it to reduce its size
+optCoercion env co
+ | opt_NoOptCoercion = substCo env co
+ | otherwise = opt_co env False co
+
+type NormalCo = Coercion
+ -- Invariants:
+ -- * The substitution has been fully applied
+ -- * For trans coercions (co1 `trans` co2)
+ -- co1 is not a trans, and neither co1 nor co2 is identity
+ -- * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
+
+type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
+
+opt_co, opt_co' :: CvSubst
+ -> Bool -- True <=> return (sym co)
+ -> Coercion
+ -> NormalCo
+opt_co = opt_co'
+{-
+opt_co env sym co
+ = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $
+ co1 `seq`
+ pprTrace "opt_co done }" (ppr co1) $
+ (WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (Pair s1 t1)
+ $$ ppr co1 <+> dcolon <+> pprEqPred (Pair s2 t2) )
+ WARN( not (coreEqCoercion co1 simple_result),
+ (text "env=" <+> ppr env) $$
+ (text "input=" <+> ppr co) $$
+ (text "simple=" <+> ppr simple_result) $$
+ (text "opt=" <+> ppr co1) )
+ co1)
+ where
+ co1 = opt_co' env sym co
+ same_co_kind = s1 `eqType` s2 && t1 `eqType` t2
+ Pair s t = coercionKind (substCo env co)
+ (s1,t1) | sym = (t,s)
+ | otherwise = (s,t)
+ Pair s2 t2 = coercionKind co1
+
+ simple_result | sym = mkSymCo (substCo env co)
+ | otherwise = substCo env co
+-}
+
+opt_co' env _ (Refl ty) = Refl (substTy env ty)
+opt_co' env sym (SymCo co) = opt_co env (not sym) co
+opt_co' env sym (TyConAppCo tc cos) = mkTyConAppCo tc (map (opt_co env sym) cos)
+opt_co' env sym (AppCo co1 co2) = mkAppCo (opt_co env sym co1) (opt_co env sym co2)
+opt_co' env sym (ForAllCo tv co) = case substTyVarBndr env tv of
+ (env', tv') -> mkForAllCo tv' (opt_co env' sym co)
+ -- Use the "mk" functions to check for nested Refls
+
+opt_co' env sym (CoVarCo cv)
+ | Just co <- lookupCoVar env cv
+ = opt_co (zapCvSubstEnv env) sym co
+
+ | Just cv1 <- lookupInScope (getCvInScope env) cv
+ = ASSERT( isCoVar cv1 ) wrapSym sym (CoVarCo cv1)
+ -- cv1 might have a substituted kind!
+
+ | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)
+ ASSERT( isCoVar cv )
+ wrapSym sym (CoVarCo cv)
+
+opt_co' env sym (AxiomInstCo con cos)
+ -- Do *not* push sym inside top-level axioms
+ -- e.g. if g is a top-level axiom
+ -- g a : f a ~ a
+ -- then (sym (g ty)) /= g (sym ty) !!
+ = wrapSym sym $ AxiomInstCo con (map (opt_co env False) cos)
+ -- Note that the_co does *not* have sym pushed into it
+
+opt_co' env sym (UnsafeCo ty1 ty2)
+ | ty1' `eqType` ty2' = Refl ty1'
+ | sym = mkUnsafeCo ty2' ty1'
+ | otherwise = mkUnsafeCo ty1' ty2'
+ where
+ ty1' = substTy env ty1
+ ty2' = substTy env ty2
+
+opt_co' env sym (TransCo co1 co2)
+ | sym = opt_trans opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g
+ | otherwise = opt_trans opt_co1 opt_co2
+ where
+ opt_co1 = opt_co env sym co1
+ opt_co2 = opt_co env sym co2
+
+opt_co' env sym (NthCo n co)
+ | TyConAppCo tc cos <- co'
+ , isDecomposableTyCon tc -- Not synonym families
+ = ASSERT( n < length cos )
+ cos !! n
+ | otherwise
+ = NthCo n co'
+ where
+ co' = opt_co env sym co
+
+opt_co' env sym (InstCo co ty)
+ -- See if the first arg is already a forall
+ -- ...then we can just extend the current substitution
+ | Just (tv, co_body) <- splitForAllCo_maybe co
+ = opt_co (extendTvSubst env tv ty') sym co_body
+
+ -- See if it is a forall after optimization
+ | Just (tv, co'_body) <- splitForAllCo_maybe co'
+ = substCoWithTy tv ty' co'_body -- An inefficient one-variable substitution
+
+ | otherwise = InstCo co' ty'
+
+ where
+ co' = opt_co env sym co
+ ty' = substTy env ty
+
+-------------
+opt_transList :: [NormalCo] -> [NormalCo] -> [NormalCo]
+opt_transList = zipWith opt_trans
+
+opt_trans :: NormalCo -> NormalCo -> NormalCo
+opt_trans co1 co2
+ | isReflCo co1 = co2
+ | otherwise = opt_trans1 co1 co2
+
+opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo
+-- First arg is not the identity
+opt_trans1 co1 co2
+ | isReflCo co2 = co1
+ | otherwise = opt_trans2 co1 co2
+
+opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo
+-- Neither arg is the identity
+opt_trans2 (TransCo co1a co1b) co2
+ -- Don't know whether the sub-coercions are the identity
+ = opt_trans co1a (opt_trans co1b co2)
+
+opt_trans2 co1 co2
+ | Just co <- opt_trans_rule co1 co2
+ = co
+
+opt_trans2 co1 (TransCo co2a co2b)
+ | Just co1_2a <- opt_trans_rule co1 co2a
+ = if isReflCo co1_2a
+ then co2b
+ else opt_trans1 co1_2a co2b
+
+opt_trans2 co1 co2
+ = mkTransCo co1 co2
+
+------
+-- Optimize coercions with a top-level use of transitivity.
+opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
+
+-- push transitivity down through matching top-level constructors.
+opt_trans_rule in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
+ | tc1 == tc2 = fireTransRule "PushTyConApp" in_co1 in_co2 $
+ TyConAppCo tc1 (opt_transList cos1 cos2)
+
+-- push transitivity through matching destructors
+opt_trans_rule in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
+ | d1 == d2
+ , co1 `compatible_co` co2
+ = fireTransRule "PushNth" in_co1 in_co2 $
+ mkNthCo d1 (opt_trans co1 co2)
+
+-- Push transitivity inside instantiation
+opt_trans_rule in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
+ | ty1 `eqType` ty2
+ , co1 `compatible_co` co2
+ = fireTransRule "TrPushInst" in_co1 in_co2 $
+ mkInstCo (opt_trans co1 co2) ty1
+
+-- Push transitivity inside apply
+opt_trans_rule in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
+ = fireTransRule "TrPushApp" in_co1 in_co2 $
+ mkAppCo (opt_trans co1a co2a) (opt_trans co1b co2b)
+
+opt_trans_rule co1@(TyConAppCo tc cos1) co2
+ | Just cos2 <- etaTyConAppCo_maybe tc co2
+ = ASSERT( length cos1 == length cos2 )
+ fireTransRule "EtaCompL" co1 co2 $
+ TyConAppCo tc (zipWith opt_trans cos1 cos2)
+
+opt_trans_rule co1 co2@(TyConAppCo tc cos2)
+ | Just cos1 <- etaTyConAppCo_maybe tc co1
+ = ASSERT( length cos1 == length cos2 )
+ fireTransRule "EtaCompR" co1 co2 $
+ TyConAppCo tc (zipWith opt_trans cos1 cos2)
+
+-- Push transitivity inside forall
+opt_trans_rule co1 co2
+ | Just (tv1,r1) <- splitForAllCo_maybe co1
+ , Just (tv2,r2) <- etaForAllCo_maybe co2
+ , let r2' = substCoWithTy tv2 (mkTyVarTy tv1) r2
+ = fireTransRule "EtaAllL" co1 co2 $
+ mkForAllCo tv1 (opt_trans2 r1 r2')
+
+ | Just (tv2,r2) <- splitForAllCo_maybe co2
+ , Just (tv1,r1) <- etaForAllCo_maybe co1
+ , let r1' = substCoWithTy tv1 (mkTyVarTy tv2) r1
+ = fireTransRule "EtaAllR" co1 co2 $
+ mkForAllCo tv1 (opt_trans2 r1' r2)
+
+-- Push transitivity inside axioms
+opt_trans_rule co1 co2
+
+ -- TrPushAxR/TrPushSymAxR
+ | Just (sym, con, cos1) <- co1_is_axiom_maybe
+ , Just cos2 <- matchAxiom sym con co2
+ = fireTransRule "TrPushAxR" co1 co2 $
+ if sym
+ then SymCo $ AxiomInstCo con (opt_transList (map mkSymCo cos2) cos1)
+ else AxiomInstCo con (opt_transList cos1 cos2)
+
+ -- TrPushAxL/TrPushSymAxL
+ | Just (sym, con, cos2) <- co2_is_axiom_maybe
+ , Just cos1 <- matchAxiom (not sym) con co1
+ = fireTransRule "TrPushAxL" co1 co2 $
+ if sym
+ then SymCo $ AxiomInstCo con (opt_transList cos2 (map mkSymCo cos1))
+ else AxiomInstCo con (opt_transList cos1 cos2)
+
+ -- TrPushAxSym/TrPushSymAx
+ | Just (sym1, con1, cos1) <- co1_is_axiom_maybe
+ , Just (sym2, con2, cos2) <- co2_is_axiom_maybe
+ , con1 == con2
+ , sym1 == not sym2
+ , let qtvs = co_ax_tvs con1
+ lhs = co_ax_lhs con1
+ rhs = co_ax_rhs con1
+ pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)
+ , all (`elemVarSet` pivot_tvs) qtvs
+ = fireTransRule "TrPushAxSym" co1 co2 $
+ if sym2
+ then liftCoSubstWith qtvs (opt_transList cos1 (map mkSymCo cos2)) lhs -- TrPushAxSym
+ else liftCoSubstWith qtvs (opt_transList (map mkSymCo cos1) cos2) rhs -- TrPushSymAx
+ where
+ co1_is_axiom_maybe = isAxiom_maybe co1
+ co2_is_axiom_maybe = isAxiom_maybe co2
+
+opt_trans_rule co1 co2 -- Identity rule
+ | Pair ty1 _ <- coercionKind co1
+ , Pair _ ty2 <- coercionKind co2
+ , ty1 `eqType` ty2
+ = fireTransRule "RedTypeDirRefl" co1 co2 $
+ Refl ty2
+
+opt_trans_rule _ _ = Nothing
+
+fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
+fireTransRule _rule _co1 _co2 res
+ = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
+ Just res
+
+-----------
+wrapSym :: Bool -> Coercion -> Coercion
+wrapSym sym co | sym = SymCo co
+ | otherwise = co
+
+-----------
+isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom, [Coercion])
+isAxiom_maybe (SymCo co)
+ | Just (sym, con, cos) <- isAxiom_maybe co
+ = Just (not sym, con, cos)
+isAxiom_maybe (AxiomInstCo con cos)
+ = Just (False, con, cos)
+isAxiom_maybe _ = Nothing
+
+matchAxiom :: Bool -- True = match LHS, False = match RHS
+ -> CoAxiom -> Coercion -> Maybe [Coercion]
+-- If we succeed in matching, then *all the quantified type variables are bound*
+-- E.g. if tvs = [a,b], lhs/rhs = [b], we'll fail
+matchAxiom sym (CoAxiom { co_ax_tvs = qtvs, co_ax_lhs = lhs, co_ax_rhs = rhs }) co
+ = case liftCoMatch (mkVarSet qtvs) (if sym then lhs else rhs) co of
+ Nothing -> Nothing
+ Just subst -> allMaybes (map (liftCoSubstTyVar subst) qtvs)
+
+-------------
+compatible_co :: Coercion -> Coercion -> Bool
+-- Check whether (co1 . co2) will be well-kinded
+compatible_co co1 co2
+ = x1 `eqType` x2
+ where
+ Pair _ x1 = coercionKind co1
+ Pair x2 _ = coercionKind co2
+
+-------------
+etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
+-- Try to make the coercion be of form (forall tv. co)
+etaForAllCo_maybe co
+ | Just (tv, r) <- splitForAllCo_maybe co
+ = Just (tv, r)
+
+ | Pair ty1 ty2 <- coercionKind co
+ , Just (tv1, _) <- splitForAllTy_maybe ty1
+ , Just (tv2, _) <- splitForAllTy_maybe ty2
+ , tyVarKind tv1 `eqKind` tyVarKind tv2
+ = Just (tv1, mkInstCo co (mkTyVarTy tv1))
+
+ | otherwise
+ = Nothing
+
+etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
+-- If possible, split a coercion
+-- g :: T s1 .. sn ~ T t1 .. tn
+-- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
+etaTyConAppCo_maybe tc (TyConAppCo tc2 cos2)
+ = ASSERT( tc == tc2 ) Just cos2
+
+etaTyConAppCo_maybe tc co
+ | isDecomposableTyCon tc
+ , Pair ty1 ty2 <- coercionKind co
+ , Just (tc1, tys1) <- splitTyConApp_maybe ty1
+ , Just (tc2, tys2) <- splitTyConApp_maybe ty2
+ , tc1 == tc2
+ , let n = length tys1
+ = ASSERT( tc == tc1 )
+ ASSERT( n == length tys2 )
+ Just (decomposeCo n co)
+ -- NB: n might be <> tyConArity tc
+ -- e.g. data family T a :: * -> *
+ -- g :: T a b ~ T c d
+
+ | otherwise
+ = Nothing
+\end{code}
projects / ghc-hetmet.git / blobdiff