@@ -1,10 +1,6 @@
11
2−module Types.Substitutions (cSub
3− ,tSub
4− ,cSubNoContext
5− ,hasVarC
6− ,freeVars
7− ,schemeSub
2+module Types.Substitutions (subst
3+ ,occurs
84 ,concretize
95 ,rescheme
106 ,generalize) where
@@ -16,106 +12,83 @@ import qualified Data.Set as Set
1612import Guid
1713import Types.Types
1814
19−force x = x `deepseq` x
20−a ++++ b = foldl' (\tl hd -> hd : tl) b a
21−map' f xs = map (\x -> let v = f x in v `seq` v) xs
22−
23−instance (NFData a) => NFData (Context c a) where
24− rnf (Context _ a) = a `deepseq` ()
25−
26−instance NFData Scheme where
27− rnf (Forall vs cs t) = vs `deepseq` cs `deepseq` t `deepseq` ()
28−
29−instance NFData Constraint where
30− rnf (t1 :=: t2) = t1 `deepseq` t2 `deepseq` ()
31− rnf (t1 :<: t2) = t1 `deepseq` t2 `deepseq` ()
32− rnf (t :<<: s) = t `deepseq` s `deepseq` ()
33−
34−instance NFData Type where
35− rnf (LambdaT t1 t2) = t1 `deepseq` t2 `deepseq` ()
36− rnf (ADT _ ts) = foldl' (\acc x -> x `deepseq` acc) () ts
37− rnf t = t `seq` ()
38−
39−tSub k v t@(VarT x) = if k == x then v else t
40−tSub k v (LambdaT t1 t2) = tSub k v t1 `seq` tSub k v t2 `seq` LambdaT (tSub k v t1) (tSub k v t2)
41−tSub k v (ADT name ts) = map' (tSub k v) ts `seq` ADT name (map' (tSub k v) ts)
42−tSub k v (Super ts) = Super ts
43−
44−schemeSubHelp k s c t1 t2 relation = do
45− (t1',cs1) <- f t1
46− (t2',cs2) <- f t2
47− return $ Context c (relation t1' t2') : cs1 ++++ cs2
48− where f t | hasVar k t = do (v, cs) <- concretize s; return (tSub k v t, cs)
49− | otherwise = return (t, [])
50−
51−schemeSub k s (Context ctx (t1 :=: t2)) = t1 `seq` t2 `seq` schemeSubHelp k s ctx t1 t2 (:=:)
52−schemeSub k s (Context ctx (t1 :<: t2)) = t1 `seq` t2 `seq` schemeSubHelp k s ctx t1 t2 (:<:)
53−schemeSub k s c@(Context ctx (x :<<: Forall cxs ccs ctipe)) =
54− if not $ hasVarC k c then return [c]
55− else do
56− Forall xs cs tipe <- rescheme s
57− let constraints = map' (cSub k tipe) $ cs ++ ccs
58− let c' = x :<<: Forall (cxs ++ xs) constraints (tSub k tipe ctipe)
59− return [ Context ctx c' ]
60−
61−hasVar v (VarT x) = v == x
62−hasVar v (LambdaT t1 t2) = force (hasVar v t1 || hasVar v t2)
63−hasVar v (ADT _ ts) = force $ any (hasVar v) ts
64−hasVar v (Super _ ) = False
65−
66−cSub k v (Context ctx c) = out `deepseq` out
67− where out = Context ctx (cSubNoContext' k v c)
68−
69−cSubNoContext k v c = c' `deepseq` c'
70− where c' = cSubNoContext' k v c
71−
72−cSubNoContext' k v (t1 :=: t2) = let { t1' = tSub k v $! t1 ; t2' = tSub k v $! t2 } in
73− t1' `seq` t2' `seq` t1' :=: t2'
74−cSubNoContext' k v (t :<: super) = let t' = tSub k v t in t' `seq` t' :<: super
75−cSubNoContext' k v (x :<<: poly@(Forall vs cs tipe)) = (x :<<: poly')
76− where poly' | k `elem` vs = poly
77− | otherwise = let tipe' = tSub k v tipe in
78− tipe' `deepseq` Forall vs (map' (cSub k v) cs) tipe'
7915
80−concretize (Forall xs cs t) = do
81− pairs <- zip xs `liftM` mapM (const guid) xs
82− let tipe = foldl' (\t' (k,v) -> tSub k (VarT v) $! t') t pairs
83− let f c = foldl' (\c (k,v) -> cSub k (VarT v) $! c) c $! pairs
84− let cs' = f `seq` map' f cs
85− tipe `deepseq` cs' `deepseq` return (tipe, cs')
16+class Subst a where
17+ subst :: [(X,Type)] -> a -> a
18+
19+instance Subst Type where
20+ subst ss (VarT x) = case lookup x ss of
21+ Nothing -> VarT x
22+ Just (Super _) -> VarT x
23+ Just t -> t
24+ subst ss (LambdaT t1 t2) = LambdaT (subst ss t1) (subst ss t2)
25+ subst ss (ADT name ts) = ADT name (subst ss ts)
26+ subst ss (Super ts) = Super ts
27+
28+instance Subst Scheme where
29+ subst ss (Forall vs cs t) = Forall vs (subst ss cs) (subst ss t)
30+
31+instance Subst Constraint where
32+ subst ss (t1 :=: t2) = subst ss t1 :=: subst ss t2
33+ subst ss (t :<: super) = subst ss t :<: super
34+ subst ss (x :<<: poly) = x :<<: subst ss poly
35+
36+instance Subst a => Subst (Context c a) where
37+ subst ss (Context ctx c) = Context ctx (subst ss c)
38+
39+instance Subst a => Subst [a] where
40+ subst ss as = map (subst ss) as
8641
87−rescheme :: Scheme -> GuidCounter Scheme
88−rescheme (Forall xs cs t) = do
89− pairs <- zip xs `liftM` mapM (const guid) xs
90− let tipe = foldl' (\t' (k,v) -> tSub k (VarT v) $! t') t pairs
91− let fs = map (\(k,v) -> cSub k (VarT v)) pairs
92− let cs' = map (\c -> foldl' (\c f -> f $! c) c fs) cs
93− tipe `deepseq` cs' `deepseq` (return $ Forall (map' snd pairs) cs' tipe)
9442
95−freeVars t = let fs = freeVars' t in fs `deepseq` fs
43+class FreeVars a where
44+ freeVars :: a -> [X]
9645
97−freeVars' (VarT v) = [v]
98−freeVars' (LambdaT t1 t2) = freeVars' t1 ++++ freeVars' t2
99−freeVars' (ADT _ ts) = concatMap freeVars' ts
100−freeVars' (Super _ ) = []
46+instance FreeVars Type where
47+ freeVars (VarT v) = [v]
48+ freeVars (LambdaT t1 t2) = freeVars t1 ++ freeVars t2
49+ freeVars (ADT _ ts) = concatMap freeVars ts
50+ freeVars (Super _ ) = []
10151
102−cFreeVars c = let fs = cFreeVars' c in fs `deepseq` fs
52+instance FreeVars Constraint where
53+ freeVars (t1 :=: t2) = freeVars t1 ++ freeVars t2
54+ freeVars (t1 :<: t2) = freeVars t1 ++ freeVars t2
55+ freeVars (x :<<: Forall xs cs t) = filter (`notElem` xs) frees
56+ where frees = concatMap freeVars cs ++ freeVars t
10357
104−cFreeVars' (t1 :=: t2) = freeVars' t1 ++++ freeVars' t2
105−cFreeVars' (t1 :<: t2) = freeVars' t1 ++++ freeVars' t2
106−cFreeVars' (x :<<: Forall xs cs t) = filter (`notElem` xs) frees
107− where frees = concatMap (\(Context _ c) -> cFreeVars' c) cs ++++ freeVars' t
58+instance FreeVars a => FreeVars (Context c a) where
59+ freeVars (Context _ c) = freeVars c
10860
10961
110−hasVarC x (Context _ (t1 :=: t2)) = hasVar x t1 || hasVar x t2
111−hasVarC x (Context _ (t1 :<: t2)) = hasVar x t1 || hasVar x t2
112−hasVarC x (Context _ (y :<<: Forall xs cs t)) = x == y || hasVar x t || inCs
113− where inCs = x `notElem` xs && any (hasVarC x) cs
62+class Occurs a where
63+ occurs :: X -> a -> Bool
11464
115−decontext (Context _ c) = c
65+instance Occurs Type where
66+ occurs v (VarT x) = v == x
67+ occurs v (LambdaT t1 t2) = occurs v t1 || occurs v t2
68+ occurs v (ADT _ ts) = any (occurs v) ts
69+ occurs v (Super _ ) = False
70+
71+instance Occurs Constraint where
72+ occurs x (t1 :=: t2) = occurs x t1 || occurs x t2
73+ occurs x (t1 :<: t2) = occurs x t1 || occurs x t2
74+ occurs x (y :<<: Forall xs cs t) = x == y || occurs x t || inCs
75+ where inCs = x `notElem` xs && any (occurs x) cs
76+
77+instance Occurs a => Occurs (Context c a) where
78+ occurs x (Context _ c) = occurs x c
79+
80+concretize :: Scheme -> GuidCounter (Type, [Context String Constraint])
81+concretize (Forall xs cs t) = do
82+ ss <- zip xs `liftM` mapM (\_ -> liftM VarT guid) xs
83+ return (subst ss t, subst ss cs)
84+
85+rescheme :: Scheme -> GuidCounter Scheme
86+rescheme (Forall xs cs t) = do
87+ xs' <- mapM (const guid) xs
88+ let ss = zip xs (map VarT xs')
89+ return $ Forall xs' (subst ss cs) (subst ss t)
11690
11791generalize :: [X] -> Scheme -> GuidCounter Scheme
11892generalize exceptions (Forall xs cs t) = rescheme (Forall (xs ++ frees) cs t)
119− where allFrees = Set.fromList $ freeVars t ++ concatMap (cFreeVars . decontext) cs
93+ where allFrees = Set.fromList $ freeVars t ++ concatMap freeVars cs
12094 frees = Set.toList $ Set.difference allFrees (Set.fromList exceptions)
121−