git.iko.soy/elk
on master help sign in
Make type checking faster.
4a57153evancz
elm/src/Types/Substitutions.hs+68−46
compare with master
unifiedsplit
@@ -2,7 +2,7 @@
2module Types.Substitutions (cSub
2module Types.Substitutions (cSub
3 ,tSub
3 ,tSub
4 ,cSubNoContext
4 ,cSubNoContext
5− ,cFreeVars
5+ ,hasVarC
6 ,freeVars
6 ,freeVars
7 ,schemeSub
7 ,schemeSub
8 ,concretize
8 ,concretize
@@ -17,14 +17,19 @@ import Guid
17import Types
17import Types
18
18
19force x = x `deepseq` x
19force 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
20
22
21instance (NFData a) => NFData (Context c a) where
23instance (NFData a) => NFData (Context c a) where
22 rnf (Context _ a) = a `deepseq` ()
24 rnf (Context _ a) = a `deepseq` ()
23
25
26+instance NFData Scheme where
27+ rnf (Forall vs cs t) = vs `deepseq` cs `deepseq` t `deepseq` ()
28+
24instance NFData Constraint where
29instance NFData Constraint where
25 rnf (t1 :=: t2) = t1 `deepseq` t2 `deepseq` ()
30 rnf (t1 :=: t2) = t1 `deepseq` t2 `deepseq` ()
26− rnf (t :<: _) = t `deepseq` ()
31+ rnf (t1 :<: t2) = t1 `deepseq` t2 `deepseq` ()
27− rnf (t :<<: _) = t `deepseq` ()
32+ rnf (t :<<: s) = t `deepseq` s `deepseq` ()
28
33
29instance NFData Type where
34instance NFData Type where
30 rnf (LambdaT t1 t2) = t1 `deepseq` t2 `deepseq` ()
35 rnf (LambdaT t1 t2) = t1 `deepseq` t2 `deepseq` ()
@@ -32,63 +37,80 @@ instance NFData Type where
32 rnf t = t `seq` ()
37 rnf t = t `seq` ()
33
38
34tSub k v t@(VarT x) = if k == x then v else t
39tSub 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)
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)
36−tSub k v (ADT name ts) = ADT name (map (force . tSub k v) ts)
41+tSub k v (ADT name ts) = map' (tSub k v) ts `seq` ADT name (map' (tSub k v) ts)
37tSub k v (Super ts) = Super ts
42tSub k v (Super ts) = Super ts
38
43
39schemeSubHelp k s c t1 t2 relation = do
44schemeSubHelp k s c t1 t2 relation = do
40− (t1',cs1) <- f1 ; (t2',cs2) <- f2
45+ (t1',cs1) <- f t1
46+ (t2',cs2) <- f t2
41− return (Context c (relation t1' t2') : cs1 ++ cs2)
47+ 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)
48+ where f t | hasVar k t = do (v, cs) <- concretize s; return (tSub k v t, cs)
45− | otherwise = return (t2, [])
49+ | otherwise = return (t, [])
46−
50+
47−schemeSub k s (Context ctx (t1 :=: t2)) = schemeSubHelp k s ctx t1 t2 (:=:)
51+schemeSub k s (Context ctx (t1 :=: t2)) = t1 `seq` t2 `seq` schemeSubHelp k s ctx t1 t2 (:=:)
48−schemeSub k s (Context ctx (t1 :<: t2)) = schemeSubHelp k s ctx t1 t2 (:<:)
52+schemeSub k s (Context ctx (t1 :<: t2)) = t1 `seq` t2 `seq` schemeSubHelp k s ctx t1 t2 (:<:)
49−schemeSub k s (Context ctx c@(x :<<: Forall cxs ccs ctipe))
53+schemeSub k s c@(Context ctx (x :<<: Forall cxs ccs ctipe)) =
50− | k `elem` cxs || k `notElem` cFreeVars c = return [Context ctx c]
54+ if not $ hasVarC k c then return [c]
51− | otherwise = do
55+ else do
52− Forall xs cs tipe <- rescheme s
56+ Forall xs cs tipe <- rescheme s
53− let constraints = (map (cSub k tipe) $ cs ++ ccs)
57+ let constraints = map' (cSub k tipe) $ cs ++ ccs
54− let c' = x :<<: Forall (cxs ++ xs) constraints (tSub k tipe ctipe)
58+ let c' = x :<<: Forall (cxs ++ xs) constraints (tSub k tipe ctipe)
55− return [ Context ctx c' ]
59+ return [ Context ctx c' ]
56
60
57hasVar v (VarT x) = v == x
61hasVar v (VarT x) = v == x
58−hasVar v (LambdaT t1 t2) = hasVar v t1 || hasVar v t2
62+hasVar v (LambdaT t1 t2) = force (hasVar v t1 || hasVar v t2)
59−hasVar v (ADT _ ts) = any (hasVar v) ts
63+hasVar v (ADT _ ts) = force $ any (hasVar v) ts
60hasVar v (Super _ ) = False
64hasVar v (Super _ ) = False
61
65
66+cSub k v (Context ctx c) = out `deepseq` out
62−cSub k v (Context ctx c) = Context ctx (cSubNoContext k v c)
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
63
71
64−cSubNoContext k v (t1 :=: t2) = force $ tSub k v t1 :=: tSub k v t2
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'
65−cSubNoContext k v (t :<: super) = force $ tSub k v t :<: super
74+cSubNoContext' k v (t :<: super) = let t' = tSub k v t in t' `seq` t' :<: super
66−cSubNoContext k v (x :<<: poly@(Forall vs cs tipe)) = force $ x :<<: poly'
75+cSubNoContext' k v (x :<<: poly@(Forall vs cs tipe)) = (x :<<: poly')
67 where poly' | k `elem` vs = poly
76 where poly' | k `elem` vs = poly
68− | otherwise = let cs' = map (cSub k v) cs in
77+ | otherwise = let tipe' = tSub k v tipe in
69− Forall vs cs' (tSub k v tipe)
78+ tipe' `deepseq` Forall vs (map' (cSub k v) cs) tipe'
70
79
71concretize (Forall xs cs t) = do
80concretize (Forall xs cs t) = do
72− pairs <- mapM (\x -> liftM ((,) x) guid) xs
81+ pairs <- zip xs `liftM` mapM (const guid) xs
73− return ( foldl' (\t' (k,v) -> tSub k (VarT v) t') t pairs
82+ let tipe = foldl' (\t' (k,v) -> tSub k (VarT v) $! t') t pairs
74− , foldl' (\cs' (k,v) -> map (cSub k $ VarT v) cs') cs 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')
75
86
76rescheme :: Scheme -> GuidCounter Scheme
87rescheme :: Scheme -> GuidCounter Scheme
77rescheme (Forall xs cs t) = do
88rescheme (Forall xs cs t) = do
78− pairs <- mapM (\x -> liftM ((,) x) guid) xs
89+ pairs <- zip xs `liftM` mapM (const guid) xs
79− let tipe = foldl' (\t' (k,v) -> tSub k (VarT v) t') t pairs
90+ 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
91+ let fs = map (\(k,v) -> cSub k (VarT v)) pairs
92+ let cs' = map (\c -> foldl' (\c f -> f $! c) c fs) cs
81− return $ Forall (map snd pairs) cs' tipe
93+ tipe `deepseq` cs' `deepseq` (return $ Forall (map' snd pairs) cs' tipe)
82−
94+
95+freeVars t = let fs = freeVars' t in fs `deepseq` fs
96+
83−freeVars (VarT v) = [v]
97+freeVars' (VarT v) = [v]
84−freeVars (LambdaT t1 t2) = freeVars t1 ++ freeVars t2
98+freeVars' (LambdaT t1 t2) = freeVars' t1 ++++ freeVars' t2
85−freeVars (ADT _ ts) = concatMap freeVars ts
99+freeVars' (ADT _ ts) = concatMap freeVars' ts
86−freeVars (Super _ ) = []
100+freeVars' (Super _ ) = []
87−
101+
102+cFreeVars c = let fs = cFreeVars' c in fs `deepseq` fs
103+
88−cFreeVars (t1 :=: t2) = freeVars t1 ++ freeVars t2
104+cFreeVars' (t1 :=: t2) = freeVars' t1 ++++ freeVars' t2
89−cFreeVars (t1 :<: t2) = freeVars t1 ++ freeVars t2
105+cFreeVars' (t1 :<: t2) = freeVars' t1 ++++ freeVars' t2
90−cFreeVars (x :<<: Forall xs cs t) = filter (`notElem` xs) frees
106+cFreeVars' (x :<<: Forall xs cs t) = filter (`notElem` xs) frees
91− where frees = concatMap (\(Context _ c) -> cFreeVars c) cs ++ freeVars t
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
92
114
93decontext (Context _ c) = c
115decontext (Context _ c) = c
94
116
elm/src/Types/Unify.hs+18−11
@@ -11,6 +11,7 @@ import Types
11import Types.Constrain
11import Types.Constrain
12import Types.Substitutions
12import Types.Substitutions
13
13
14+import Control.DeepSeq (deepseq)
14--import System.IO.Unsafe
15--import System.IO.Unsafe
15
16
16prints xs v = v --} unsafePerformIO (putStrLn "----------" >> mapM print xs) `seq` v
17prints xs v = v --} unsafePerformIO (putStrLn "----------" >> mapM print xs) `seq` v
@@ -22,6 +23,7 @@ unify hints modul = run $ do
22
23
23eq ctx t1 t2 = Context ctx (t1 :=: t2)
24eq ctx t1 t2 = Context ctx (t1 :=: t2)
24
25
26+
25solver [] subs = prints (Map.toList subs) $ return $ Right subs
27solver [] subs = prints (Map.toList subs) $ return $ Right subs
26
28
27-------- Destruct Type-constructors --------
29-------- Destruct Type-constructors --------
@@ -43,21 +45,26 @@ solver (Context ctx (VarT x :=: VarT y) : cs) subs
43 setXY t = Map.insert x t . Map.insert y t
45 setXY t = Map.insert x t . Map.insert y t
44 in case Set.toList ts of
46 in case Set.toList ts of
45 [] -> unionError ctx xts yts
47 [] -> unionError ctx xts yts
46− [t] -> solver (map (cSub x t . cSub y t) cs) $ setXY t subs
48+ [t] -> let cs1 = map (\c -> cSub y t c `seq` cSub x t (cSub y t c)) cs in
49+ cs1 `seq` solver cs1 (setXY t subs)
47 _ -> solver cs $ setXY (Super ts) subs
50 _ -> solver cs $ setXY (Super ts) subs
48 (Just (Super xts), _) ->
51 (Just (Super xts), _) ->
52+ let cs2 = map (cSub y (VarT x)) cs in
49− solver (map (cSub y (VarT x)) cs) $ Map.insert y (VarT x) subs
53+ cs2 `seq` solver cs2 $ Map.insert y (VarT x) subs
50 (_, _) ->
54 (_, _) ->
55+ let cs3 = map (cSub x (VarT y)) cs in
51− solver (map (cSub x (VarT y)) cs) $ Map.insert x (VarT y) subs
56+ cs3 `deepseq` solver cs3 $ Map.insert x (VarT y) subs
52solver (Context ctx (VarT x :=: t) : cs) subs = do
57solver (Context ctx (VarT x :=: t) : cs) subs = do
53 if x `occursIn` t then occursError ctx (VarT x) t else
58 if x `occursIn` t then occursError ctx (VarT x) t else
54 (case Map.lookup x subs of
59 (case Map.lookup x subs of
60+ Nothing -> let cs4 = map (cSub x t) cs in
55− Nothing -> solver (map (cSub x t) cs) . Map.map (tSub x t) $ Map.insert x t subs
61+ cs4 `deepseq` (solver cs4 . Map.map (tSub x t) $ Map.insert x t subs)
56 Just (Super ts) ->
62 Just (Super ts) ->
57 let ts' = Set.intersection ts (Set.singleton t) in
63 let ts' = Set.intersection ts (Set.singleton t) in
58 case Set.toList ts' of
64 case Set.toList ts' of
59 [] -> solver (Context ctx (t :<: Super ts) : cs) subs
65 [] -> solver (Context ctx (t :<: Super ts) : cs) subs
66+ [t'] -> let cs5 = map (cSub x t) cs in
60− [t'] -> solver (map (cSub x t') cs) $ Map.insert x t' subs
67+ cs5 `seq` solver cs5 $ Map.insert x t' subs
61 _ -> solver cs $ Map.insert x (Super ts') subs
68 _ -> solver cs $ Map.insert x (Super ts') subs
62 Just t' -> solver (Context ctx (t' :=: t) : cs) subs
69 Just t' -> solver (Context ctx (t' :=: t) : cs) subs
63 )
70 )
@@ -91,13 +98,13 @@ solver (Context ctx (t :<: Super ts) : cs) subs
91 | otherwise = subtypeError ctx t (Super ts)
98 | otherwise = subtypeError ctx t (Super ts)
92
99
93solver (Context ctx (x :<<: s) : cs) subs
100solver (Context ctx (x :<<: s) : cs) subs
94− | any (\(Context _ c) -> x `elem` cFreeVars c) cs =
101+ | any (hasVarC x) cs =
95− do cs' <- concat `liftM` mapM (schemeSub x s) cs
102+ do cs6 <- concat `liftM` mapM (schemeSub x s) cs
96− prints cs' $ solver cs' subs
103+ solver cs6 subs
97 | otherwise =
104 | otherwise =
98− do (t,cs') <- concretize s
105+ do (t,cs7) <- concretize s
99− let cs'' = (cs ++ Context ctx (VarT x :=: t) : map (extendCtx ctx) cs')
106+ let cs'' = (cs ++ Context ctx (VarT x :=: t) : map (extendCtx ctx) cs7)
100− prints cs'' $ solver cs'' subs
107+ solver cs'' subs
101
108
102
109
103occursError ctx t1 t2 =
110occursError ctx t1 t2 =