@@ -2,7 +2,7 @@
22module Types.Substitutions (cSub
33 ,tSub
44 ,cSubNoContext
5− ,cFreeVars
5+ ,hasVarC
66 ,freeVars
77 ,schemeSub
88 ,concretize
@@ -17,14 +17,19 @@ import Guid
1717import Types
1818
1919force 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
2022
2123instance (NFData a) => NFData (Context c a) where
2224 rnf (Context _ a) = a `deepseq` ()
2325
26+instance NFData Scheme where
27+ rnf (Forall vs cs t) = vs `deepseq` cs `deepseq` t `deepseq` ()
28+
2429instance NFData Constraint where
2530 rnf (t1 :=: t2) = t1 `deepseq` t2 `deepseq` ()
26− rnf (t :<: _) = t `deepseq` ()
27− rnf (t :<<: _) = t `deepseq` ()
31+ rnf (t1 :<: t2) = t1 `deepseq` t2 `deepseq` ()
32+ rnf (t :<<: s) = t `deepseq` s `deepseq` ()
2833
2934instance NFData Type where
3035 rnf (LambdaT t1 t2) = t1 `deepseq` t2 `deepseq` ()
@@ -32,63 +37,80 @@ instance NFData Type where
3237 rnf t = t `seq` ()
3338
3439tSub k v t@(VarT x) = if k == x then v else t
35−tSub k v (LambdaT t1 t2) = force $ LambdaT (tSub k v t1) (tSub k v t2)
36−tSub k v (ADT name ts) = ADT name (map (force . tSub k v) ts)
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)
3742tSub k v (Super ts) = Super ts
3843
3944schemeSubHelp k s c t1 t2 relation = do
40− (t1',cs1) <- f1 ; (t2',cs2) <- f2
41− return (Context c (relation t1' t2') : cs1 ++ cs2)
42− where f1 | hasVar k t1 = do (v, cs) <- concretize s; return (tSub k v t1, cs)
43− | otherwise = return (t1, [])
44− f2 | hasVar k t2 = do (v, cs) <- concretize s; return (tSub k v t2, cs)
45− | otherwise = return (t2, [])
46−
47−schemeSub k s (Context ctx (t1 :=: t2)) = schemeSubHelp k s ctx t1 t2 (:=:)
48−schemeSub k s (Context ctx (t1 :<: t2)) = schemeSubHelp k s ctx t1 t2 (:<:)
49−schemeSub k s (Context ctx c@(x :<<: Forall cxs ccs ctipe))
50− | k `elem` cxs || k `notElem` cFreeVars c = return [Context ctx c]
51− | otherwise = do
52− Forall xs cs tipe <- rescheme s
53− let constraints = (map (cSub k tipe) $ cs ++ ccs)
54− let c' = x :<<: Forall (cxs ++ xs) constraints (tSub k tipe ctipe)
55− return [ Context ctx c' ]
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' ]
5660
5761hasVar v (VarT x) = v == x
58−hasVar v (LambdaT t1 t2) = hasVar v t1 || hasVar v t2
59−hasVar v (ADT _ ts) = any (hasVar v) ts
62+hasVar v (LambdaT t1 t2) = force (hasVar v t1 || hasVar v t2)
63+hasVar v (ADT _ ts) = force $ any (hasVar v) ts
6064hasVar v (Super _ ) = False
6165
62−cSub k v (Context ctx c) = Context ctx (cSubNoContext k v c)
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
6371
64−cSubNoContext k v (t1 :=: t2) = force $ tSub k v t1 :=: tSub k v t2
65−cSubNoContext k v (t :<: super) = force $ tSub k v t :<: super
66−cSubNoContext k v (x :<<: poly@(Forall vs cs tipe)) = force $ x :<<: poly'
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')
6776 where poly' | k `elem` vs = poly
68− | otherwise = let cs' = map (cSub k v) cs in
69− Forall vs cs' (tSub k v tipe)
77+ | otherwise = let tipe' = tSub k v tipe in
78+ tipe' `deepseq` Forall vs (map' (cSub k v) cs) tipe'
7079
7180concretize (Forall xs cs t) = do
72− pairs <- mapM (\x -> liftM ((,) x) guid) xs
73− return ( foldl' (\t' (k,v) -> tSub k (VarT v) t') t pairs
74− , foldl' (\cs' (k,v) -> map (cSub k $ VarT v) cs') cs pairs )
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')
7586
7687rescheme :: Scheme -> GuidCounter Scheme
7788rescheme (Forall xs cs t) = do
78− pairs <- mapM (\x -> liftM ((,) x) guid) xs
79− let tipe = foldl' (\t' (k,v) -> tSub k (VarT v) t') t pairs
80− let cs' = foldl' (\cs' (k,v) -> map (cSub k $ VarT v) cs') cs pairs
81− return $ Forall (map snd pairs) cs' tipe
82−
83−freeVars (VarT v) = [v]
84−freeVars (LambdaT t1 t2) = freeVars t1 ++ freeVars t2
85−freeVars (ADT _ ts) = concatMap freeVars ts
86−freeVars (Super _ ) = []
87−
88−cFreeVars (t1 :=: t2) = freeVars t1 ++ freeVars t2
89−cFreeVars (t1 :<: t2) = freeVars t1 ++ freeVars t2
90−cFreeVars (x :<<: Forall xs cs t) = filter (`notElem` xs) frees
91− where frees = concatMap (\(Context _ c) -> cFreeVars c) cs ++ freeVars t
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)
94+
95+freeVars t = let fs = freeVars' t in fs `deepseq` fs
96+
97+freeVars' (VarT v) = [v]
98+freeVars' (LambdaT t1 t2) = freeVars' t1 ++++ freeVars' t2
99+freeVars' (ADT _ ts) = concatMap freeVars' ts
100+freeVars' (Super _ ) = []
101+
102+cFreeVars c = let fs = cFreeVars' c in fs `deepseq` fs
103+
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
108+
109+
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
92114
93115decontext (Context _ c) = c
94116