(text "input=" <+> ppr co) $$\r
(text "simple=" <+> ppr simple_result) $$\r
(text "opt=" <+> ppr co1) )\r
- 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
+ same_co_kind = s1 `eqType` s2 && t1 `eqType` t2\r
+ Pair s t = coercionKind (substCo env co)\r
(s1,t1) | sym = (t,s)\r
| otherwise = (s,t)\r
- (s2,t2) = coercionKind co1\r
+ Pair s2 t2 = coercionKind co1\r
\r
- simple_result | sym = mkSymCoercion (substTy env co)\r
- | otherwise = substTy env co\r
+ simple_result | sym = mkSymCo (substCo env co)\r
+ | otherwise = substCo 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
+opt_co' env _ (Refl ty) = Refl (substTy env ty)\r
+opt_co' env sym (SymCo co) = opt_co env (not sym) co\r
- opt_co' env sym (TyConAppCo tc cos) = TyConAppCo tc (map (opt_co env sym) cos)\r
++\r
++opt_co' env sym (TyConAppCo tc cos) = mkTyConAppCo tc (map (opt_co env sym) cos)\r
+opt_co' env sym (AppCo co1 co2) = mkAppCo (opt_co env sym co1) (opt_co env sym co2)\r
+opt_co' env sym (ForAllCo tv co) = case substTyVarBndr env tv of\r
- (env', tv') -> ForAllCo tv' (opt_co env' sym co)\r
++ (env', tv') -> mkForAllCo tv' (opt_co env' sym co)\r
++ -- Use the "mk" functions to check for nested Refls\r
++\r
+opt_co' env sym (CoVarCo cv)\r
+ | Just co <- lookupCoVar env cv\r
+ = opt_co (zapCvSubstEnv env) sym co\r
+\r
+ | Just cv1 <- lookupInScope (getCvInScope env) cv\r
+ = ASSERT( isCoVar cv1 ) wrapSym sym (CoVarCo cv1)\r
+ -- cv1 might have a substituted kind!\r
+\r
+ | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)\r
+ ASSERT( isCoVar cv )\r
+ wrapSym sym (CoVarCo cv)\r
+\r
+opt_co' env sym (AxiomInstCo con cos)\r
+ -- 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
+ = wrapSym sym $ AxiomInstCo con (map (opt_co env False) cos)\r
+ -- Note that the_co does *not* have sym pushed into it\r
+\r
+opt_co' env sym (UnsafeCo ty1 ty2)\r
+ | ty1' `eqType` ty2' = Refl ty1'\r
+ | sym = mkUnsafeCo ty2' ty1'\r
+ | otherwise = mkUnsafeCo ty1' ty2'\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
+ ty1' = substTy env ty1\r
+ ty2' = substTy env ty2\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
+opt_co' env sym (TransCo co1 co2)\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
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
+ opt_co1 = opt_co env sym co1\r
+ opt_co2 = opt_co env sym co2\r
\r
+opt_co' env sym (NthCo n co)\r
+ | TyConAppCo tc cos <- co'\r
+ , isDecomposableTyCon tc -- Not synonym families\r
+ = ASSERT( n < length cos )\r
+ cos !! n\r
+ | otherwise\r
+ = NthCo n co'\r
where\r
- (co1 : cos1) = cos\r
- (co2 : _) = cos1\r
+ co' = opt_co env sym co\r
\r
- ty1' = substTy env co1\r
- ty2' = substTy env co2\r
+opt_co' env sym (InstCo co ty)\r
+ -- See if the first arg is already a forall\r
+ -- ...then we can just extend the current substitution\r
+ | Just (tv, co_body) <- splitForAllCo_maybe co\r
+ = opt_co (extendTvSubst env tv ty') sym co_body\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
+ -- See if it is a forall after optimization\r
+ | Just (tv, co'_body) <- splitForAllCo_maybe co'\r
+ = substCoWithTy tv ty' co'_body -- An inefficient one-variable substitution\r
\r
- the_unary_opt_co = TyConApp tc [opt_co1]\r
+ | otherwise = InstCo co' ty'\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
+ where\r
+ co' = opt_co env sym co\r
+ ty' = substTy env ty\r
\r
-------------\r
-opt_transL :: [NormalCo] -> [NormalCo] -> [NormalCo]\r
-opt_transL = zipWith opt_trans\r
+opt_transList :: [NormalCo] -> [NormalCo] -> [NormalCo]\r
+opt_transList = zipWith opt_trans\r
\r
opt_trans :: NormalCo -> NormalCo -> NormalCo\r
opt_trans co1 co2\r
------------------
-- OK, here's the main printer
-pprKind, pprParendKind :: Kind -> SDoc
-pprKind = pprType
-pprParendKind = pprParendType
-
ppr_type :: Prec -> Type -> SDoc
- ppr_type _ (TyVarTy tv) -- Note [Infix type variables]
- | isSymOcc (getOccName tv) = parens (ppr tv)
- | otherwise = ppr tv
+ ppr_type _ (TyVarTy tv) = ppr_tvar tv
ppr_type p (PredTy pred) = maybeParen p TyConPrec $
- ifPprDebug (ptext (sLit "<pred>")) <> (ppr pred)
-ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
+ ifPprDebug (ptext (sLit "<pred>")) <> (pprPredTy pred)
+ppr_type p (TyConApp tc tys) = pprTcApp p ppr_type tc tys
ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
pprType t1 <+> ppr_type TyConPrec t2
(tvs, rho) = split1 [] ty
(ctxt, tau) = split2 [] rho
- -- We need to be extra careful here as equality constraints will occur as
- -- type variables with an equality kind. So, while collecting quantified
- -- variables, we separate the coercion variables out and turn them into
- -- equality predicates.
- split1 tvs (ForAllTy tv ty)
- | not (isCoVar tv) = split1 (tv:tvs) ty
- split1 tvs ty = (reverse tvs, ty)
+ split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
+ split1 tvs ty = (reverse tvs, ty)
split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
- split2 ps (ForAllTy tv ty)
- | isCoVar tv = split2 (coVarPred tv : ps) ty
split2 ps ty = (reverse ps, ty)
- -------------------
-ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
-ppr_tc_app _ tc []
- = ppr_tc tc
-ppr_tc_app _ tc [ty]
- | tc `hasKey` listTyConKey = brackets (pprType ty)
- | tc `hasKey` parrTyConKey = ptext (sLit "[:") <> pprType ty <> ptext (sLit ":]")
- | tc `hasKey` liftedTypeKindTyConKey = ptext (sLit "*")
- | tc `hasKey` unliftedTypeKindTyConKey = ptext (sLit "#")
- | tc `hasKey` openTypeKindTyConKey = ptext (sLit "(?)")
- | tc `hasKey` ubxTupleKindTyConKey = ptext (sLit "(#)")
- | tc `hasKey` argTypeKindTyConKey = ptext (sLit "??")
-
-ppr_tc_app p tc tys
- | isTupleTyCon tc && tyConArity tc == length tys
- = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
- | otherwise
- = ppr_type_app p (getName tc) tys
-
-ppr_type_app :: Prec -> Name -> [Type] -> SDoc
--- Used for classes as well as types; that's why it's separate from ppr_tc_app
-ppr_type_app p tc tys
- | is_sym_occ -- Print infix if possible
- , [ty1,ty2] <- tys -- We know nothing of precedence though
- = maybeParen p FunPrec (sep [ppr_type FunPrec ty1,
- pprInfixVar True (ppr tc) <+> ppr_type FunPrec ty2])
- | otherwise
- = maybeParen p TyConPrec (hang (pprPrefixVar is_sym_occ (ppr tc))
- 2 (sep (map pprParendType tys)))
- where
- is_sym_occ = isSymOcc (getOccName tc)
-
-ppr_tc :: TyCon -> SDoc -- No brackets for SymOcc
-ppr_tc tc
- = pp_nt_debug <> ppr tc
- where
- pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
- then ptext (sLit "<recnt>")
- else ptext (sLit "<nt>"))
- | otherwise = empty
-
+ ppr_tvar :: TyVar -> SDoc
+ ppr_tvar tv -- Note [Infix type variables]
+ | isSymOcc (getOccName tv) = parens (ppr tv)
+ | otherwise = ppr tv
+
--------------------
pprForAll :: [TyVar] -> SDoc
pprForAll [] = empty
pprForAll tvs = ptext (sLit "forall") <+> sep (map pprTvBndr tvs) <> dot
pprTvBndr :: TyVar -> SDoc
-pprTvBndr tv | isLiftedTypeKind kind = ppr_tvar tv
- | otherwise = parens (ppr_tvar tv <+> dcolon <+> pprKind kind)
- where
- kind = tyVarKind tv
+pprTvBndr tv
- | isLiftedTypeKind kind = ppr tv
- | otherwise = parens (ppr tv <+> dcolon <+> pprKind kind)
++ | isLiftedTypeKind kind = ppr_tvar tv
++ | otherwise = parens (ppr_tvar tv <+> dcolon <+> pprKind kind)
+ where
+ kind = tyVarKind tv
\end{code}
Note [Infix type variables]
projects / ghc-hetmet.git / commitdiff