git.iko.soy/elk
on d178521 help sign in
elk/elm/src/Types/Unify.hs
119 lines 4.6 kB history raw
2module Types.Unify (unify) where
4import Control.Arrow (second)
5import Control.Monad (liftM)
6import Data.List (foldl')
7import qualified Data.Set as Set
8import qualified Data.Map as Map
9import Guid
10import Types
11import Types.Constrain
12import Types.Substitutions
14--import System.IO.Unsafe
16prints xs v = v --} unsafePerformIO (putStrLn "----------" >> mapM print xs) `seq` v
18unify hints modul = run $ do
19 (escapees, cs) <- constrain hints modul
20 subs <- solver cs Map.empty
21 prints cs $ return ((,) escapees `liftM` subs)
23eq ctx t1 t2 = Context ctx (t1 :=: t2)
25solver [] subs = prints (Map.toList subs) $ return $ Right subs
27-------- Destruct Type-constructors --------
29solver ((Context ctx (t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2))) : cs) subs =
30 if n1 /= n2 then uniError ctx t1 t2 else
31 solver (zipWith (eq ctx) ts1 ts2 ++ cs) subs
32solver ((Context ctx (LambdaT t1 t2 :=: LambdaT t1' t2')) : cs) subs =
33 solver ([ eq ctx t1 t1', eq ctx t2 t2' ] ++ cs) subs
35-------- Type-equality --------
37solver (Context ctx (VarT x :=: VarT y) : cs) subs
38 | x == y = solver cs subs
39 | otherwise =
40 case (Map.lookup x subs, Map.lookup y subs) of
41 (Just (Super xts), Just (Super yts)) ->
42 let ts = Set.intersection xts yts
43 setXY t = Map.insert x t . Map.insert y t
44 in case Set.toList ts of
45 [] -> unionError ctx xts yts
46 [t] -> solver (map (cSub x t . cSub y t) cs) $ setXY t subs
47 _ -> solver cs $ setXY (Super ts) subs
48 (Just (Super xts), _) ->
49 solver (map (cSub y (VarT x)) cs) $ Map.insert y (VarT x) subs
50 (_, _) ->
51 solver (map (cSub x (VarT y)) cs) $ Map.insert x (VarT y) subs
52solver (Context ctx (VarT x :=: t) : cs) subs = do
53 if x `occursIn` t then occursError ctx (VarT x) t else
54 (case Map.lookup x subs of
55 Nothing -> solver (map (cSub x t) cs) . Map.map (tSub x t) $ Map.insert x t subs
56 Just (Super ts) ->
57 let ts' = Set.intersection ts (Set.singleton t) in
58 case Set.toList ts' of
59 [] -> solver (Context ctx (t :<: Super ts) : cs) subs
60 [t'] -> solver (map (cSub x t') cs) $ Map.insert x t' subs
61 _ -> solver cs $ Map.insert x (Super ts') subs
62 Just t' -> solver (Context ctx (t' :=: t) : cs) subs
63 )
64solver ((Context ctx (t :=: VarT x)) : cs) subs =
65 solver ((Context ctx (VarT x :=: t)) : cs) subs
66solver ((Context ctx (t1 :=: t2)) : cs) subs
67 | t1 == t2 = solver cs subs
68 | otherwise = uniError ctx t1 t2
71-------- subtypes --------
73solver (Context ctx (VarT x :<: Super ts) : cs) subs =
74 case Map.lookup x subs of
75 Nothing -> solver cs $ Map.insert x (Super ts) subs
76 Just (Super ts') ->
77 case Set.toList $ Set.intersection ts ts' of
78 [] -> unionError ctx ts ts'
79 [t] -> solver (map (cSub x t) cs) $ Map.insert x t subs
80 ts'' -> solver cs $ Map.insert x (Super $ Set.fromList ts'') subs
82solver (Context ctx (ADT "List" [t] :<: Super ts) : cs) subs
83 | any f (Set.toList ts) = solver cs subs
84 | otherwise = subtypeError ctx (ADT "List" [t]) (Super ts)
85 where f (ADT "List" [VarT _]) = True
86 f (ADT "List" [t']) = t == t'
87 f _ = False
89solver (Context ctx (t :<: Super ts) : cs) subs
90 | Set.member t ts = solver cs subs
91 | otherwise = subtypeError ctx t (Super ts)
93solver (Context ctx (x :<<: s) : cs) subs
94 | any (\(Context _ c) -> x `elem` cFreeVars c) cs =
95 do cs' <- concat `liftM` mapM (schemeSub x s) cs
96 prints cs' $ solver cs' subs
97 | otherwise =
98 do (t,cs') <- concretize s
99 let cs'' = (cs ++ Context ctx (VarT x :=: t) : map (extendCtx ctx) cs')
100 prints cs'' $ solver cs'' subs
103occursError ctx t1 t2 =
104 return . Left $ "Type error: Occurs check: cannot construct the infinite type: " ++ show t1 ++
105 " = " ++ show t2 ++
106 " in context " ++ ctx
107uniError ctx t1 t2 =
108 return . Left $ "Type error: " ++ show t1 ++
109 " is not equal to " ++ show t2 ++
110 " in context " ++ ctx
111unionError ctx ts ts' =
112 return . Left $ concat [ "Type error: There are no types in both "
113 , show (Super ts), " and ", show (Super ts')
114 , " in context ", ctx ]
115subtypeError ctx t s =
116 return . Left $ concat [ "Type error: ", show t, " is not a ", show s
117 , " in context ", ctx ]
119occursIn x t = x `elem` freeVars t