Commit 0d1fca15 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com
Browse files

Minor refactoring

parent 41c97fdc
...@@ -47,6 +47,8 @@ import UniqFM ...@@ -47,6 +47,8 @@ import UniqFM
\begin{code} \begin{code}
data Refinement = Reft InScopeSet InternalReft data Refinement = Reft InScopeSet InternalReft
type InternalReft = TyVarEnv (Coercion, Type)
-- INVARIANT: a->(co,ty) then co :: (a:=:ty) -- INVARIANT: a->(co,ty) then co :: (a:=:ty)
-- Not necessarily idemopotent -- Not necessarily idemopotent
...@@ -139,7 +141,7 @@ gadtRefine (Reft in_scope env1) ...@@ -139,7 +141,7 @@ gadtRefine (Reft in_scope env1)
ex_tvs co_vars ex_tvs co_vars
-- Precondition: fvs( co_vars ) # env1 -- Precondition: fvs( co_vars ) # env1
-- That is, the kinds of the co_vars are a -- That is, the kinds of the co_vars are a
-- fixed point of the incoming refinement -- fixed point of the incoming refinement
= ASSERT2( not $ any (`elemVarEnv` env1) (varSetElems $ tyVarsOfTypes $ map tyVarKind co_vars), = ASSERT2( not $ any (`elemVarEnv` env1) (varSetElems $ tyVarsOfTypes $ map tyVarKind co_vars),
ppr env1 $$ ppr co_vars $$ ppr (map tyVarKind co_vars) ) ppr env1 $$ ppr co_vars $$ ppr (map tyVarKind co_vars) )
...@@ -157,9 +159,11 @@ gadtRefine (Reft in_scope env1) ...@@ -157,9 +159,11 @@ gadtRefine (Reft in_scope env1)
where where
tv_set = mkVarSet ex_tvs tv_set = mkVarSet ex_tvs
in_scope' = foldr extend in_scope co_vars in_scope' = foldr extend in_scope co_vars
-- For each co_var, add it *and* the tyvars it mentions, to in_scope
extend co_var in_scope extend co_var in_scope
= extendInScopeSetSet (extendInScopeSet in_scope co_var) = extendInScopeSetSet in_scope $
(tyVarsOfType (tyVarKind co_var)) extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2 do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2
where where
...@@ -252,11 +256,6 @@ tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe ...@@ -252,11 +256,6 @@ tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
%************************************************************************ %************************************************************************
\begin{code} \begin{code}
type InternalReft = TyVarEnv (Coercion, Type)
-- INVARIANT: a->(co,ty) then co :: (a:=:ty)
-- Not necessarily idemopotent
#ifdef DEBUG #ifdef DEBUG
badReftElts :: InternalReft -> [(Unique, (Coercion,Type))] badReftElts :: InternalReft -> [(Unique, (Coercion,Type))]
-- Return the BAD elements of the refinement -- Return the BAD elements of the refinement
......
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