Commit 91ab6902 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

Remove dead code dealing with type refinement

parent 372a8c47
......@@ -12,10 +12,6 @@ module Unify (
dataConCannotMatch,
-- GADT type refinement
Refinement, emptyRefinement, isEmptyRefinement,
matchRefine, refineType, refinePred, refineResType,
-- Side-effect free unification
tcUnifyTys, BindFlag(..)
......@@ -374,130 +370,6 @@ dataConCannotMatch tys con
\end{code}
%************************************************************************
%* *
What a refinement is
%* *
%************************************************************************
\begin{code}
data Refinement = Reft InScopeSet InternalReft
type InternalReft = TyVarEnv (Coercion, Type)
-- INVARIANT: a->(co,ty) then co :: (a~ty)
-- Not necessarily idemopotent
instance Outputable Refinement where
ppr (Reft _in_scope env)
= ptext (sLit "Refinement") <+>
braces (ppr env)
emptyRefinement :: Refinement
emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
isEmptyRefinement :: Refinement -> Bool
isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
refineType :: Refinement -> Type -> Maybe (Coercion, Type)
-- Apply the refinement to the type.
-- If (refineType r ty) = (co, ty')
-- Then co :: ty~ty'
-- Nothing => the refinement does nothing to this type
refineType (Reft in_scope env) ty
| not (isEmptyVarEnv env), -- Common case
any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
= Just (substTy co_subst ty, substTy tv_subst ty)
| otherwise
= Nothing -- The type doesn't mention any refined type variables
where
tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
co_subst = mkTvSubst in_scope (mapVarEnv fst env)
refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType)
refinePred (Reft in_scope env) pred
| not (isEmptyVarEnv env), -- Common case
any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred))
= Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred)
| otherwise
= Nothing -- The type doesn't mention any refined type variables
where
tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
co_subst = mkTvSubst in_scope (mapVarEnv fst env)
refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
-- Like refineType, but returns the 'sym' coercion
-- If (refineResType r ty) = (co, ty')
-- Then co :: ty'~ty
refineResType reft ty
= case refineType reft ty of
Just (co, ty1) -> Just (mkSymCoercion co, ty1)
Nothing -> Nothing
\end{code}
%************************************************************************
%* *
Simple generation of a type refinement
%* *
%************************************************************************
\begin{code}
matchRefine :: [TyVar] -> [Coercion] -> Refinement
\end{code}
Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
is a specialisation of ty1, produce a type refinement that maps the variables
of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg,
matchRefine (co :: [(a, b)] ~ [(c, Maybe d)])
= { right (left (right co)) :: a ~ c
, right (right co) :: b ~ Maybe d
}
Precondition: The rhs types must indeed be a specialisation of the lhs types;
i.e., some free variables of the lhs are replaced with either distinct free
variables or proper type terms to obtain the rhs. (We don't perform full
unification or type matching here!)
NB: matchRefine does *not* expand the type synonyms.
\begin{code}
matchRefine in_scope_tvs cos
= Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne cos))
where
in_scope = mkInScopeSet (mkVarSet in_scope_tvs)
-- NB: in_scope_tvs include both coercion variables
-- *and* the tyvars in their kinds
refineOne co = refine co ty1 ty2
where
(ty1, ty2) = coercionKind co
refine co (TyVarTy tv) ty = unitVarEnv tv (co, ty)
refine co (TyConApp _ tys) (TyConApp _ tys') = refineArgs co tys tys'
refine _ (PredTy _) (PredTy _) =
error "Unify.matchRefine: PredTy"
refine co (FunTy arg res) (FunTy arg' res') =
refine (mkRightCoercion (mkLeftCoercion co)) arg arg'
`plusVarEnv`
refine (mkRightCoercion co) res res'
refine co (AppTy fun arg) (AppTy fun' arg') =
refine (mkLeftCoercion co) fun fun'
`plusVarEnv`
refine (mkRightCoercion co) arg arg'
refine co (ForAllTy tv ty) (ForAllTy _tv ty') =
refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv
refine _ _ _ = error "RcGadt.matchRefine: mismatch"
refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
refineArgs co tys tys' =
fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
where
refineArg (ty, ty') (reft, coWrapper)
= (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft,
mkLeftCoercion . coWrapper)
\end{code}
%************************************************************************
%* *
......
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