git.iko.soy/elk
on 8a700e8 help sign in
elk/compiler/src/Types/Solver.hs
199 lines 7.8 kB history raw
2module Types.Solver (solver) where
4import Context
5import Control.Arrow (second)
6import Control.Monad (liftM)
7import Data.Either (lefts,rights)
8import Data.List (foldl')
9import Data.Maybe (isJust)
10import qualified Data.Set as Set
11import qualified Data.Map as Map
12import Guid
13import Types.Types
14import Types.Constrain
15import Types.Substitutions
17isSolved ss (C _ _ (t1 :=: t2)) = t1 == t2
18isSolved ss (C _ _ (x :<<: _)) = isJust (lookup x ss)
19isSolved ss c = False
21crush :: Scheme -> GuidCounter (Either String Scheme)
22crush (Forall xs cs t) =
23 do subs <- solver cs Map.empty
24 return $ do ss' <- subs
25 let ss = Map.toList ss'
26 cs' = filter (not . isSolved ss) (subst ss cs)
27 return $ Forall xs cs' (subst ss t)
29schemeSubHelp txt span x s t1 rltn t2 = do
30 (t1',cs1) <- sub t1
31 (t2',cs2) <- sub t2
32 return (C txt span (rltn t1' t2') : cs1 ++ cs2)
33 where sub t | not (occurs x t) = return (t, [])
34 | otherwise = do (st, cs) <- concretize s
35 return (subst [(x,st)] t, cs)
37schemeSub x s c = do s' <- crush s
38 case s' of
39 Right s'' -> Right `liftM` schemeSub' x s'' c
40 Left err -> return $ Left err
42schemeSub' x s c@(C txt span constraint) =
43 case constraint of
44 (t1 :=: t2) -> schemeSubHelp txt span x s t1 (:=:) t2
45 (t1 :<: t2) -> schemeSubHelp txt span x s t1 (:<:) t2
46 (y :<<: Forall cxs ccs ctipe)
47 | not (occurs x c) -> return [c]
48 | otherwise ->
49 do Forall xs cs tipe <- rescheme s
50 let ss = [(x,tipe)]
51 constraints = subst ss (cs ++ ccs)
52 c' = y :<<: Forall (cxs ++ xs) constraints (subst ss ctipe)
53 return [ C txt span c' ]
55recordConstraints eq fs t fs' t' =
56 liftM concat . sequence $
57 [ constrain fs fs'
58 , liftM concat . mapM (\(k,ts) -> zipper [] k ts []) . Map.toList $
59 Map.difference fs fs'
60 , liftM concat . mapM (\(k,ts) -> zipper [] k [] ts) . Map.toList $
61 Map.difference fs' fs
62 ]
63 where constrain :: Map.Map String [Type] -> Map.Map String [Type]
64 -> GuidCounter [Context Constraint]
65 constrain as bs = liftM concat . sequence . Map.elems $
66 Map.intersectionWithKey (zipper []) as bs
67 zipper :: [Context Constraint] -> String -> [Type] -> [Type]
68 -> GuidCounter [Context Constraint]
69 zipper cs k xs ys =
70 case (xs,ys) of
71 (a:as, b:bs) -> zipper (eq a b : cs) k as bs
72 ([],[]) -> return cs
73 (as,[]) -> do x <- guid
74 let tipe = RecordT (Map.singleton k as) (VarT x)
75 return (cs ++ [eq t' tipe])
76 ([],bs) -> do x <- guid
77 let tipe = RecordT (Map.singleton k bs) (VarT x)
78 return (cs ++ [eq t tipe])
80solver :: [Context Constraint]
81 -> Map.Map X Type
82 -> GuidCounter (Either String (Map.Map X Type))
83solver [] subs = return $ Right subs
84solver (C txt span c : cs) subs =
85 let ctx = C txt span
86 eq t1 t2 = ctx (t1 :=: t2)
87 in case c of
88 -- Destruct Type-constructors
89 t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2) ->
90 if n1 /= n2 then uniError txt span t1 t2 else
91 solver (zipWith eq ts1 ts2 ++ cs) subs
93 LambdaT t1 t2 :=: LambdaT t1' t2' ->
94 solver ([ eq t1 t1', eq t2 t2' ] ++ cs) subs
96 RecordT fs t :=: RecordT fs' t' ->
97 do cs' <- recordConstraints eq fs t fs' t'
98 solver (cs' ++ cs) subs
100 -- Type-equality
101 VarT x :=: VarT y
102 | x == y -> solver cs subs
103 | otherwise ->
104 case (Map.lookup x subs, Map.lookup y subs) of
105 (Just (Super xts), Just (Super yts)) ->
106 let ts = Set.intersection xts yts
107 setXY t = Map.insert x t . Map.insert y t
108 in case Set.toList ts of
109 [] -> unionError txt span xts yts
110 [t] -> let cs1 = subst [(x,t),(y,t)] cs in
111 cs1 `seq` solver cs1 (setXY t subs)
112 _ -> solver cs $ setXY (Super ts) subs
113 (Just (Super xts), _) ->
114 let cs2 = subst [(y,VarT x)] cs in
115 solver cs2 $ Map.insert y (VarT x) subs
116 (_, _) ->
117 let cs3 = subst [(x,VarT y)] cs in
118 solver cs3 $ Map.insert x (VarT y) subs
120 VarT x :=: t -> do
121 if x `occurs` t then occursError txt span (VarT x) t else
122 (case Map.lookup x subs of
123 Nothing -> let cs4 = subst [(x,t)] cs in
124 solver cs4 . Map.map (subst [(x,t)]) $
125 Map.insert x t subs
126 Just (Super ts) ->
127 let ts' = Set.intersection ts (Set.singleton t) in
128 case Set.toList ts' of
129 [] -> solver (ctx (t :<: Super ts) : cs) subs
130 [t'] -> let cs5 = subst [(x,t)] cs in
131 solver cs5 $ Map.insert x t' subs
132 _ -> solver cs $ Map.insert x (Super ts') subs
133 Just t' -> solver (ctx (t' :=: t) : cs) subs
134 )
136 t :=: VarT x -> solver ((ctx (VarT x :=: t)) : cs) subs
138 t1 :=: t2 | t1 == t2 -> solver cs subs
139 | otherwise -> uniError txt span t1 t2
141 -- subtypes
142 VarT x :<: Super ts ->
143 case Map.lookup x subs of
144 Nothing -> solver cs $ Map.insert x (Super ts) subs
145 Just (Super ts') ->
146 case Set.toList $ Set.intersection ts ts' of
147 [] -> unionError txt span ts ts'
148 [t] -> solver (subst [(x,t)] cs) $ Map.insert x t subs
149 ts'' -> solver cs $
150 Map.insert x (Super $ Set.fromList ts'') subs
152 ADT "List" [t] :<: Super ts
153 | any f (Set.toList ts) -> solver cs subs
154 | otherwise -> subtypeError txt span (ADT "List" [t]) (Super ts)
155 where f (ADT "List" [VarT _]) = True
156 f (ADT "List" [t']) = t == t'
157 f _ = False
159 t :<: Super ts
160 | Set.member t ts -> solver cs subs
161 | otherwise -> subtypeError txt span t (Super ts)
163 x :<<: s
164 | any (occurs x) cs ->
165 do css <- mapM (schemeSub x s) cs
166 case lefts css of
167 err : _ -> return $ Left err
168 [] -> solver (concat (rights css)) subs
169 | otherwise ->
170 do (t,cs7) <- concretize s
171 let cs'' = (cs ++ ctx (VarT x :=: t) : cs7)
172 solver cs'' subs
174showMsg msg = case msg of
175 Just str -> "\nIn context: " ++ str
176 Nothing -> ""
178occursError msg span t1 t2 =
179 return . Left $ concat
180 [ "Type error (" ++ show span ++ "):\n"
181 , "Occurs check: cannot construct the infinite type:\n"
182 , show t1, " = ", show t2, showMsg msg ]
184uniError msg span t1 t2 =
185 return . Left $ concat
186 [ "Type error (" ++ show span ++ "):\n"
187 , show t1, " is not equal to ", show t2, showMsg msg ]
189unionError msg span ts ts' =
190 return . Left $ concat
191 [ "Type error (" ++ show span ++ "):\n"
192 , "There are no types in both "
193 , show (Super ts), " and ", show (Super ts'), showMsg msg ]
195subtypeError msg span t s =
196 return . Left $ concat
197 [ "Type error (" ++ show span ++ "):\n"
198 , show t, " is not a ", show s, showMsg msg ]