Commit 373167c1 authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.
Browse files

GADT tweaks

Mon Jul 31 12:42:07 EDT 2006  kevind@bu.edu
parent 7caf75c4
...@@ -47,32 +47,31 @@ import Outputable ...@@ -47,32 +47,31 @@ import Outputable
%************************************************************************ %************************************************************************
\begin{code} \begin{code}
data Refinement = Reft InScopeSet TvSubstEnv CoSubstEnv data Refinement = Reft InScopeSet InternalReft
type CoSubstEnv = TvSubstEnv -- Maps type variables to *coercions* -- INVARIANT: a->(co,ty) then co :: (a:=:ty)
-- INVARIANT: in the refinement (tsub, csub) -- Not necessarily idemopotent
-- forall a. (csub(a) :: a:=:tsub(a))
instance Outputable Refinement where instance Outputable Refinement where
ppr (Reft in_scope tv_env co_env) ppr (Reft in_scope env)
= ptext SLIT("Refinment") <+> = ptext SLIT("Refinement") <+>
braces (ppr tv_env $$ ppr co_env) braces (ppr env)
emptyRefinement :: Refinement emptyRefinement :: Refinement
emptyRefinement = Reft emptyInScopeSet emptyVarEnv emptyVarEnv emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
refineType :: Refinement -> Type -> (ExprCoFn, Type) refineType :: Refinement -> Type -> (ExprCoFn, Type)
-- Apply the refinement to the type. -- Apply the refinement to the type.
-- If (refineType r ty) = (co, ty') -- If (refineType r ty) = (co, ty')
-- Then co :: ty:=:ty' -- Then co :: ty:=:ty'
refineType (Reft in_scope tv_env co_env) ty refineType (Reft in_scope env) ty
| not (isEmptyVarEnv tv_env), -- Common case | not (isEmptyVarEnv env), -- Common case
any (`elemVarEnv` tv_env) (varSetElems (tyVarsOfType ty)) any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
= (ExprCoFn (substTy co_subst ty), substTy tv_subst ty) = (ExprCoFn (substTy co_subst ty), substTy tv_subst ty)
| otherwise | otherwise
= (idCoercion, ty) -- The type doesn't mention any refined type variables = (idCoercion, ty) -- The type doesn't mention any refined type variables
where where
tv_subst = mkTvSubst in_scope tv_env tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
co_subst = mkTvSubst in_scope co_env co_subst = mkTvSubst in_scope (mapVarEnv fst env)
refineResType :: Refinement -> Type -> (ExprCoFn, Type) refineResType :: Refinement -> Type -> (ExprCoFn, Type)
-- Like refineType, but returns the 'sym' coercion -- Like refineType, but returns the 'sym' coercion
...@@ -135,9 +134,9 @@ Two refinements: ...@@ -135,9 +134,9 @@ Two refinements:
-- The result is idempotent: the -- The result is idempotent: the
\begin{code} \begin{code}
gadtRefine (Reft in_scope tv_env1 co_env1) gadtRefine (Reft in_scope env1)
ex_tvs co_vars ex_tvs co_vars
-- Precondition: fvs( co_vars ) # tv_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
...@@ -147,11 +146,9 @@ gadtRefine (Reft in_scope tv_env1 co_env1) ...@@ -147,11 +146,9 @@ gadtRefine (Reft in_scope tv_env1 co_env1)
-- Find the fixed point of the resulting -- Find the fixed point of the resulting
-- non-idempotent substitution -- non-idempotent substitution
; let tv_env2 = tv_env1 `plusVarEnv` mapVarEnv snd env2 ; let tmp_env = env1 `plusVarEnv` env2
co_env2 = co_env1 `plusVarEnv` mapVarEnv fst env2 out_env = fixTvCoEnv in_scope' tmp_env
; return (Reft in_scope' out_env) }
; return (Reft in_scope' (fixTvSubstEnv in_scope' tv_env2)
(fixTvSubstEnv in_scope' co_env2)) }
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
...@@ -196,9 +193,26 @@ tcUnifyTys bind_fn tys1 tys2 ...@@ -196,9 +193,26 @@ tcUnifyTys bind_fn tys1 tys2
---------------------------- ----------------------------
fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv fixTvCoEnv :: InScopeSet -> InternalReft -> InternalReft
-- Find the fixed point of a TvSubstEnv -- Find the fixed point of a Refinement
-- (assuming it has no loops!) -- (assuming it has no loops!)
fixTvCoEnv in_scope env
= fixpt
where
fixpt = mapVarEnv step env
step (co, ty) = (co', ty')
-- Apply fixpt one step:
-- Use refineType to get a substituted type, ty', and a coercion, co_fn,
-- which justifies the substitution. If the coercion is not the identity
-- then use transitivity with the original coercion
where
(co_fn, ty') = refineType (Reft in_scope fixpt) ty
co' | ExprCoFn co'' <- co_fn = mkTransCoercion co co''
| otherwise = ASSERT( isIdCoercion co_fn ) co
-----------------------------
fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
fixTvSubstEnv in_scope env fixTvSubstEnv in_scope env
= fixpt = fixpt
where where
......
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