Commit e91c7ea8 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

A bit more work to to keep the right in-scope set around

This change gets rid of a debug WARNING; it wasn't
actually making anything go wrong, but it's best to
have the correct in-scope set.
parent f43cf5c1
......@@ -33,8 +33,9 @@ import TyCon
import DataCon
import Class
import Var
import VarEnv( mkInScopeSet )
import VarSet( mkVarSet )
import Pair
--import VarSet
import CoreUtils ( mkPiTypes )
import CoreUnfold ( mkDFunUnfolding )
import CoreSyn ( Expr(Var), CoreExpr, varToCoreExpr )
......@@ -1186,7 +1187,8 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
rep_pred = mkClassPred clas (init_inst_tys ++ [rep_ty])
-- co : [p] ~ T p
co = substCoWithTys inst_tvs (mkTyVarTys tyvars) $
co = substCoWithTys (mkInScopeSet (mkVarSet tyvars))
inst_tvs (mkTyVarTys tyvars) $
mkSymCo coi
----------------
......
......@@ -593,11 +593,9 @@ mkNthCo :: Int -> Coercion -> Coercion
mkNthCo n (Refl ty) = Refl (getNth n ty)
mkNthCo n co = NthCo n co
-- | Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs
-- the resulting beta-reduction, otherwise it creates a suspended instantiation.
-- | Instantiates a 'Coercion' with a 'Type' argument.
mkInstCo :: Coercion -> Type -> Coercion
mkInstCo (ForAllCo tv co) ty = substCoWithTy tv ty co
mkInstCo co ty = InstCo co ty
mkInstCo co ty = InstCo co ty
-- | Manufacture a coercion from thin air. Needless to say, this is
-- not usually safe, but it is used when we know we are dealing with
......@@ -817,18 +815,16 @@ zipOpenCvSubst vs cos
mkTopCvSubst :: [(Var,Coercion)] -> CvSubst
mkTopCvSubst prs = CvSubst emptyInScopeSet emptyTvSubstEnv (mkVarEnv prs)
substCoWithTy :: TyVar -> Type -> Coercion -> Coercion
substCoWithTy tv ty = substCoWithTys [tv] [ty]
substCoWithTy :: InScopeSet -> TyVar -> Type -> Coercion -> Coercion
substCoWithTy in_scope tv ty = substCoWithTys in_scope [tv] [ty]
substCoWithTys :: [TyVar] -> [Type] -> Coercion -> Coercion
substCoWithTys tvs tys co
substCoWithTys :: InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion
substCoWithTys in_scope tvs tys co
| debugIsOn && (length tvs /= length tys)
= pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
| otherwise
= ASSERT( length tvs == length tys )
substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co
where
in_scope = mkInScopeSet (tyVarsOfTypes tys)
-- | Substitute within a 'Coercion'
substCo :: CvSubst -> Coercion -> Coercion
......@@ -870,7 +866,7 @@ substCoVar :: CvSubst -> CoVar -> Coercion
substCoVar (CvSubst in_scope _ cenv) cv
| Just co <- lookupVarEnv cenv cv = co
| Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
| otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv )
| otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv $$ ppr in_scope)
ASSERT( isCoVar cv ) CoVarCo cv
substCoVars :: CvSubst -> [CoVar] -> [Coercion]
......
......@@ -127,11 +127,12 @@ opt_co' env sym (UnsafeCo ty1 ty2)
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
| sym = opt_trans in_scope opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g
| otherwise = opt_trans in_scope opt_co1 opt_co2
where
opt_co1 = opt_co env sym co1
opt_co2 = opt_co env sym co2
in_scope = getCvInScope env
opt_co' env sym (NthCo n co)
| TyConAppCo tc cos <- co'
......@@ -149,9 +150,10 @@ opt_co' env sym (InstCo co ty)
| Just (tv, co_body) <- splitForAllCo_maybe co
= opt_co (extendTvSubst env tv ty') sym co_body
-- See if it is a forall after optimization
-- See if it is a forall after optimization
-- If so, do an inefficient one-variable substitution
| Just (tv, co'_body) <- splitForAllCo_maybe co'
= substCoWithTy tv ty' co'_body -- An inefficient one-variable substitution
= substCoWithTy (getCvInScope env) tv ty' co'_body
| otherwise = InstCo co' ty'
......@@ -160,111 +162,111 @@ opt_co' env sym (InstCo co ty)
ty' = substTy env ty
-------------
opt_transList :: [NormalCo] -> [NormalCo] -> [NormalCo]
opt_transList = zipWith opt_trans
opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
opt_transList is = zipWith (opt_trans is)
opt_trans :: NormalCo -> NormalCo -> NormalCo
opt_trans co1 co2
opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
opt_trans is co1 co2
| isReflCo co1 = co2
| otherwise = opt_trans1 co1 co2
| otherwise = opt_trans1 is co1 co2
opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo
opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
-- First arg is not the identity
opt_trans1 co1 co2
opt_trans1 is co1 co2
| isReflCo co2 = co1
| otherwise = opt_trans2 co1 co2
| otherwise = opt_trans2 is co1 co2
opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo
opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
-- Neither arg is the identity
opt_trans2 (TransCo co1a co1b) co2
opt_trans2 is (TransCo co1a co1b) co2
-- Don't know whether the sub-coercions are the identity
= opt_trans co1a (opt_trans co1b co2)
= opt_trans is co1a (opt_trans is co1b co2)
opt_trans2 co1 co2
| Just co <- opt_trans_rule co1 co2
opt_trans2 is co1 co2
| Just co <- opt_trans_rule is co1 co2
= co
opt_trans2 co1 (TransCo co2a co2b)
| Just co1_2a <- opt_trans_rule co1 co2a
opt_trans2 is co1 (TransCo co2a co2b)
| Just co1_2a <- opt_trans_rule is co1 co2a
= if isReflCo co1_2a
then co2b
else opt_trans1 co1_2a co2b
else opt_trans1 is co1_2a co2b
opt_trans2 co1 co2
opt_trans2 _ co1 co2
= mkTransCo co1 co2
------
-- Optimize coercions with a top-level use of transitivity.
opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
opt_trans_rule :: InScopeSet -> 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)
opt_trans_rule is in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
| tc1 == tc2 = fireTransRule "PushTyConApp" in_co1 in_co2 $
TyConAppCo tc1 (opt_transList cos1 cos2)
TyConAppCo tc1 (opt_transList is cos1 cos2)
-- push transitivity through matching destructors
opt_trans_rule in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
opt_trans_rule is 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)
mkNthCo d1 (opt_trans is co1 co2)
-- Push transitivity inside instantiation
opt_trans_rule in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
opt_trans_rule is 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
mkInstCo (opt_trans is co1 co2) ty1
-- Push transitivity inside apply
opt_trans_rule in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
opt_trans_rule is 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)
mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
opt_trans_rule co1@(TyConAppCo tc cos1) co2
opt_trans_rule is 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)
TyConAppCo tc (opt_transList is cos1 cos2)
opt_trans_rule co1 co2@(TyConAppCo tc cos2)
opt_trans_rule is 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)
TyConAppCo tc (opt_transList is cos1 cos2)
-- Push transitivity inside forall
opt_trans_rule co1 co2
opt_trans_rule is co1 co2
| Just (tv1,r1) <- splitForAllCo_maybe co1
, Just (tv2,r2) <- etaForAllCo_maybe co2
, let r2' = substCoWithTy tv2 (mkTyVarTy tv1) r2
, let r2' = substCoWithTy is tv2 (mkTyVarTy tv1) r2
= fireTransRule "EtaAllL" co1 co2 $
mkForAllCo tv1 (opt_trans2 r1 r2')
mkForAllCo tv1 (opt_trans2 (extendInScopeSet is tv1) r1 r2')
| Just (tv2,r2) <- splitForAllCo_maybe co2
, Just (tv1,r1) <- etaForAllCo_maybe co1
, let r1' = substCoWithTy tv1 (mkTyVarTy tv2) r1
, let r1' = substCoWithTy is tv1 (mkTyVarTy tv2) r1
= fireTransRule "EtaAllR" co1 co2 $
mkForAllCo tv1 (opt_trans2 r1' r2)
mkForAllCo tv1 (opt_trans2 (extendInScopeSet is tv2) r1' r2)
-- Push transitivity inside axioms
opt_trans_rule co1 co2
opt_trans_rule is 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)
then SymCo $ AxiomInstCo con (opt_transList is (map mkSymCo cos2) cos1)
else AxiomInstCo con (opt_transList is 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)
then SymCo $ AxiomInstCo con (opt_transList is cos2 (map mkSymCo cos1))
else AxiomInstCo con (opt_transList is cos1 cos2)
-- TrPushAxSym/TrPushSymAx
| Just (sym1, con1, cos1) <- co1_is_axiom_maybe
......@@ -278,20 +280,20 @@ opt_trans_rule co1 co2
, 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
then liftCoSubstWith qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs -- TrPushAxSym
else liftCoSubstWith qtvs (opt_transList is (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
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
opt_trans_rule _ _ _ = Nothing
fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule _rule _co1 _co2 res
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment