Commit 259e1ae7 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

White space and line endings

parent ff07927e
......@@ -10,10 +10,10 @@ It's better to read it as: "if we know these, then we're going to know these"
\begin{code}
module FunDeps (
FDEq (..),
Equation(..), pprEquation,
improveFromInstEnv, improveFromAnother,
checkInstCoverage, checkFunDeps,
growThetaTyVars, pprFundeps
Equation(..), pprEquation,
improveFromInstEnv, improveFromAnother,
checkInstCoverage, checkFunDeps,
growThetaTyVars, pprFundeps
) where
#include "HsVersions.h"
......@@ -31,43 +31,43 @@ import Outputable
import Util
import FastString
import Data.List ( nubBy )
import Data.Maybe ( isJust )
import Data.List ( nubBy )
import Data.Maybe ( isJust )
\end{code}
%************************************************************************
%* *
%* *
\subsection{Close type variables}
%* *
%* *
%************************************************************************
oclose(vs,C) The result of extending the set of tyvars vs
using the functional dependencies from C
oclose(vs,C) The result of extending the set of tyvars vs
using the functional dependencies from C
growThetaTyVars(C,vs) The result of extend the set of tyvars vs
growThetaTyVars(C,vs) The result of extend the set of tyvars vs
using all conceivable links from C.
E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
Then grow(vs,C) = {a,b,c}
E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
Then grow(vs,C) = {a,b,c}
Note that grow(vs,C) `superset` grow(vs,simplify(C))
That is, simplfication can only shrink the result of grow.
Note that grow(vs,C) `superset` grow(vs,simplify(C))
That is, simplfication can only shrink the result of grow.
Notice that
oclose is conservative v `elem` oclose(vs,C)
one way: => v is definitely fixed by vs
oclose is conservative v `elem` oclose(vs,C)
one way: => v is definitely fixed by vs
growThetaTyVars is conservative if v might be fixed by vs
the other way: => v `elem` grow(vs,C)
growThetaTyVars is conservative if v might be fixed by vs
the other way: => v `elem` grow(vs,C)
----------------------------------------------------------
(oclose preds tvs) closes the set of type variables tvs,
wrt functional dependencies in preds. The result is a superset
of the argument set. For example, if we have
class C a b | a->b where ...
class C a b | a->b where ...
then
oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
because if we know x and y then that fixes z.
We also use equality predicates in the predicates; if we have an
......@@ -129,8 +129,8 @@ growThetaTyVars theta tvs
grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
growPredTyVars :: PredType
-> TyVarSet -- The set to extend
-> TyVarSet -- TyVars of the predicate if it intersects the set,
-> TyVarSet -- The set to extend
-> TyVarSet -- TyVars of the predicate if it intersects the set,
growPredTyVars pred tvs
| isIPPred pred = pred_tvs -- Always quantify over implicit parameers
| pred_tvs `intersectsVarSet` tvs = pred_tvs
......@@ -141,9 +141,9 @@ growPredTyVars pred tvs
%************************************************************************
%* *
%* *
\subsection{Generate equations from functional dependencies}
%* *
%* *
%************************************************************************
......@@ -197,13 +197,13 @@ unification variables when producing the FD constraints.
Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
\begin{code}
type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from
type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from
data Equation
= FDEqn { fd_qtvs :: [TyVar] -- Instantiate these type and kind vars to fresh unification vars
, fd_eqs :: [FDEq] -- and then make these equal
, fd_pred1, fd_pred2 :: Pred_Loc } -- The Equation arose from
-- combining these two constraints
= FDEqn { fd_qtvs :: [TyVar] -- Instantiate these type and kind vars to fresh unification vars
, fd_eqs :: [FDEq] -- and then make these equal
, fd_pred1, fd_pred2 :: Pred_Loc } -- The Equation arose from
-- combining these two constraints
data FDEq = FDEq { fd_pos :: Int -- We use '0' for the first position
, fd_ty_left :: Type
......@@ -216,23 +216,23 @@ instance Outputable FDEq where
Given a bunch of predicates that must hold, such as
C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
improve figures out what extra equations must hold.
For example, if we have
class C a b | a->b where ...
class C a b | a->b where ...
then improve will return
[(t1,t2), (t4,t5)]
[(t1,t2), (t4,t5)]
NOTA BENE:
* improve does not iterate. It's possible that when we make
t1=t2, for example, that will in turn trigger a new equation.
This would happen if we also had
C t1 t7, C t2 t8
C t1 t7, C t2 t8
If t1=t2, we also get t7=t8.
improve does *not* do this extra step. It relies on the caller
......@@ -283,7 +283,7 @@ improveFromAnother pred1@(ty1, _) pred2@(ty2, _)
, fd <- cls_fds
, let (ltys1, rs1) = instFD fd cls_tvs tys1
(ltys2, irs2) = instFD_WithPos fd cls_tvs tys2
, eqTypes ltys1 ltys2 -- The LHSs match
, eqTypes ltys1 ltys2 -- The LHSs match
, let eqs = zipAndComputeFDEqs eqType rs1 irs2
, not (null eqs) ]
......@@ -296,7 +296,7 @@ improveFromAnother _ _ = []
pprEquation :: Equation -> SDoc
pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
= vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr qtvs),
nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])]
nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])]
improveFromInstEnv :: (InstEnv,InstEnv)
-> Pred_Loc
......@@ -313,29 +313,29 @@ improveFromInstEnv inst_env pred@(ty, _)
instances = classInstances inst_env cls
rough_tcs = roughMatchTcs tys
= [ FDEqn { fd_qtvs = meta_tvs, fd_eqs = eqs, fd_pred1 = p_inst, fd_pred2=pred }
| fd <- cls_fds -- Iterate through the fundeps first,
-- because there often are none!
| fd <- cls_fds -- Iterate through the fundeps first,
-- because there often are none!
, let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
-- Trim the rough_tcs based on the head of the fundep.
-- Remember that instanceCantMatch treats both argumnents
-- symmetrically, so it's ok to trim the rough_tcs,
-- rather than trimming each inst_tcs in turn
-- Trim the rough_tcs based on the head of the fundep.
-- Remember that instanceCantMatch treats both argumnents
-- symmetrically, so it's ok to trim the rough_tcs,
-- rather than trimming each inst_tcs in turn
, ispec <- instances
, (meta_tvs, eqs) <- checkClsFD fd cls_tvs ispec
emptyVarSet tys trimmed_tcs -- NB: orientation
, let p_inst = (mkClassPred cls (is_tys ispec),
sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)
, ptext (sLit "in the instance declaration")
<+> pprNameDefnLoc (getName ispec)])
sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)
, ptext (sLit "in the instance declaration")
<+> pprNameDefnLoc (getName ispec)])
]
improveFromInstEnv _ _ = []
checkClsFD :: FunDep TyVar -> [TyVar] -- One functional dependency from the class
checkClsFD :: FunDep TyVar -> [TyVar] -- One functional dependency from the class
-> ClsInst -- An instance template
-> TyVarSet -> [Type] -> [Maybe Name] -- Arguments of this (C tys) predicate
-- TyVarSet are extra tyvars that can be instantiated
-> [([TyVar], [FDEq])]
-> [([TyVar], [FDEq])]
checkClsFD fd clas_tvs
(ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
......@@ -343,17 +343,17 @@ checkClsFD fd clas_tvs
-- 'qtvs' are the quantified type variables, the ones which an be instantiated
-- to make the types match. For example, given
-- class C a b | a->b where ...
-- instance C (Maybe x) (Tree x) where ..
-- class C a b | a->b where ...
-- instance C (Maybe x) (Tree x) where ..
--
-- and an Inst of form (C (Maybe t1) t2),
-- then we will call checkClsFD with
--
-- is_qtvs = {x}, is_tys = [Maybe x, Tree x]
-- tys_actual = [Maybe t1, t2]
-- is_qtvs = {x}, is_tys = [Maybe x, Tree x]
-- tys_actual = [Maybe t1, t2]
--
-- We can instantiate x to t1, and then we want to force
-- (Tree x) [t1/x] ~ t2
-- (Tree x) [t1/x] ~ t2
--
-- This function is also used when matching two Insts (rather than an Inst
-- against an instance decl. In that case, qtvs is empty, and we are doing
......@@ -364,22 +364,22 @@ checkClsFD fd clas_tvs
-- so we get matching
| instanceCantMatch rough_tcs_inst rough_tcs_actual
= [] -- Filter out ones that can't possibly match,
= [] -- Filter out ones that can't possibly match,
| otherwise
= ASSERT2( length tys_inst == length tys_actual &&
length tys_inst == length clas_tvs
, ppr tys_inst <+> ppr tys_actual )
length tys_inst == length clas_tvs
, ppr tys_inst <+> ppr tys_actual )
case tcUnifyTys bind_fn ltys1 ltys2 of
Nothing -> []
Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
-- Don't include any equations that already hold.
-- Reason: then we know if any actual improvement has happened,
-- in which case we need to iterate the solver
-- In making this check we must taking account of the fact that any
-- qtvs that aren't already instantiated can be instantiated to anything
-- at all
Nothing -> []
Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
-- Don't include any equations that already hold.
-- Reason: then we know if any actual improvement has happened,
-- in which case we need to iterate the solver
-- In making this check we must taking account of the fact that any
-- qtvs that aren't already instantiated can be instantiated to anything
-- at all
-- NB: We can't do this 'is-useful-equation' check element-wise
-- because of:
-- class C a b c | a -> b c
......@@ -394,12 +394,12 @@ checkClsFD fd clas_tvs
| otherwise
-> [(meta_tvs, fdeqs)]
-- We could avoid this substTy stuff by producing the eqn
-- (qtvs, ls1++rs1, ls2++rs2)
-- which will re-do the ls1/ls2 unification when the equation is
-- executed. What we're doing instead is recording the partial
-- work of the ls1/ls2 unification leaving a smaller unification problem
where
-- We could avoid this substTy stuff by producing the eqn
-- (qtvs, ls1++rs1, ls2++rs2)
-- which will re-do the ls1/ls2 unification when the equation is
-- executed. What we're doing instead is recording the partial
-- work of the ls1/ls2 unification leaving a smaller unification problem
where
rtys1' = map (substTy subst) rtys1
irs2' = map (\(i,x) -> (i,substTy subst x)) irs2
rtys2' = map snd irs2'
......@@ -410,16 +410,16 @@ checkClsFD fd clas_tvs
-- eqType again, since we know for sure that /at least one/
-- equation in there is useful)
meta_tvs = [ setVarType tv (substTy subst (varType tv))
meta_tvs = [ setVarType tv (substTy subst (varType tv))
| tv <- qtvs, tv `notElemTvSubst` subst ]
-- meta_tvs are the quantified type variables
-- that have not been substituted out
--
-- Eg. class C a b | a -> b
-- instance C Int [y]
-- Given constraint C Int z
-- we generate the equation
-- ({y}, [y], z)
-- meta_tvs are the quantified type variables
-- that have not been substituted out
--
-- Eg. class C a b | a -> b
-- instance C Int [y]
-- Given constraint C Int z
-- we generate the equation
-- ({y}, [y], z)
--
-- But note (a) we get them from the dfun_id, so they are *in order*
-- because the kind variables may be mentioned in the
......@@ -432,7 +432,7 @@ checkClsFD fd clas_tvs
qtv_set = mkVarSet qtvs
bind_fn tv | tv `elemVarSet` qtv_set = BindMe
| tv `elemVarSet` extra_qtvs = BindMe
| otherwise = Skolem
| otherwise = Skolem
(ltys1, rtys1) = instFD fd clas_tvs tys_inst
(ltys2, irs2) = instFD_WithPos fd clas_tvs tys_actual
......@@ -502,7 +502,7 @@ The liberal version ensures the self-consistency of the instance, but
it does not guarantee termination. Example:
class Mul a b c | a b -> c where
(.*.) :: a -> b -> c
(.*.) :: a -> b -> c
instance Mul Int Int Int where (.*.) = (*)
instance Mul Int Float Float where x .*. y = fromIntegral x * y
......@@ -512,52 +512,52 @@ In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )
But it is a mistake to accept the instance because then this defn:
f = \ b x y -> if b then x .*. [y] else y
f = \ b x y -> if b then x .*. [y] else y
makes instance inference go into a loop, because it requires the constraint
Mul a [b] b
Mul a [b] b
%************************************************************************
%* *
Check that a new instance decl is OK wrt fundeps
%* *
%* *
Check that a new instance decl is OK wrt fundeps
%* *
%************************************************************************
Here is the bad case:
class C a b | a->b where ...
instance C Int Bool where ...
instance C Int Char where ...
class C a b | a->b where ...
instance C Int Bool where ...
instance C Int Char where ...
The point is that a->b, so Int in the first parameter must uniquely
determine the second. In general, given the same class decl, and given
instance C s1 s2 where ...
instance C t1 t2 where ...
instance C s1 s2 where ...
instance C t1 t2 where ...
Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
Matters are a little more complicated if there are free variables in
the s2/t2.
class D a b c | a -> b
instance D a b => D [(a,a)] [b] Int
instance D a b => D [a] [b] Bool
class D a b c | a -> b
instance D a b => D [(a,a)] [b] Int
instance D a b => D [a] [b] Bool
The instance decls don't overlap, because the third parameter keeps
them separate. But we want to make sure that given any constraint
D s1 s2 s3
D s1 s2 s3
if s1 matches
\begin{code}
checkFunDeps :: (InstEnv, InstEnv) -> ClsInst
-> Maybe [ClsInst] -- Nothing <=> ok
-- Just dfs <=> conflict with dfs
-> Maybe [ClsInst] -- Nothing <=> ok
-- Just dfs <=> conflict with dfs
-- Check wheher adding DFunId would break functional-dependency constraints
-- Used only for instance decls defined in the module being compiled
checkFunDeps inst_envs ispec
| null bad_fundeps = Nothing
| otherwise = Just bad_fundeps
| otherwise = Just bad_fundeps
where
(ins_tvs, clas, ins_tys) = instanceHead ispec
ins_tv_set = mkVarSet ins_tvs
......@@ -565,25 +565,25 @@ checkFunDeps inst_envs ispec
bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
badFunDeps :: [ClsInst] -> Class
-> TyVarSet -> [Type] -- Proposed new instance type
-> [ClsInst]
-> TyVarSet -> [Type] -- Proposed new instance type
-> [ClsInst]
badFunDeps cls_insts clas ins_tv_set ins_tys
= nubBy eq_inst $
[ ispec | fd <- fds, -- fds is often empty, so do this first!
let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
ispec <- cls_insts,
notNull (checkClsFD fd clas_tvs ispec ins_tv_set ins_tys trimmed_tcs)
[ ispec | fd <- fds, -- fds is often empty, so do this first!
let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
ispec <- cls_insts,
notNull (checkClsFD fd clas_tvs ispec ins_tv_set ins_tys trimmed_tcs)
]
where
(clas_tvs, fds) = classTvsFds clas
rough_tcs = roughMatchTcs ins_tys
eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
-- An single instance may appear twice in the un-nubbed conflict list
-- because it may conflict with more than one fundep. E.g.
-- class C a b c | a -> b, a -> c
-- instance C Int Bool Bool
-- instance C Int Char Char
-- The second instance conflicts with the first by *both* fundeps
-- An single instance may appear twice in the un-nubbed conflict list
-- because it may conflict with more than one fundep. E.g.
-- class C a b c | a -> b, a -> c
-- instance C Int Bool Bool
-- instance C Int Char Char
-- The second instance conflicts with the first by *both* fundeps
trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
-- Computing rough_tcs for a particular fundep
......
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