git.iko.soy/elk
on df667ca help sign in
elk/compiler/Types/Solver.hs
210 lines 8.2 kB history raw
2module Types.Solver (solver) where
4import Located
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.Substitutions
15import Types.Alias (dealias)
17isSolved ss (L _ _ (t1 :=: t2)) = t1 == t2
18isSolved ss (L _ _ (x :<<: _)) = isJust (lookup x ss)
19isSolved ss c = False
21type Aliases = Map.Map String ([X],Type)
23crush :: Aliases -> Scheme -> GuidCounter (Either String Scheme)
24crush aliases (Forall xs cs t) =
25 do subs <- solver aliases Map.empty cs
26 return $ do ss' <- subs
27 let ss = Map.toList ss'
28 cs' = filter (not . isSolved ss) (subst ss cs)
29 return $ Forall xs cs' (subst ss t)
31schemeSubHelp txt span x s t1 rltn t2 = do
32 (t1',cs1) <- sub t1
33 (t2',cs2) <- sub t2
34 return (L txt span (rltn t1' t2') : cs1 ++ cs2)
35 where sub t | not (occurs x t) = return (t, [])
36 | otherwise = do (st, cs) <- concretize s
37 return (subst [(x,st)] t, cs)
39schemeSub aliases x s c =
40 do s' <- crush aliases s
41 case s' of
42 Right s'' -> Right `liftM` schemeSub' x s'' c
43 Left err -> return $ Left err
45schemeSub' x s c@(L txt span constraint) =
46 case constraint of
47 (t1 :=: t2) -> schemeSubHelp txt span x s t1 (:=:) t2
48 (t1 :<: t2) -> schemeSubHelp txt span x s t1 (:<:) t2
49 (y :<<: Forall cxs ccs ctipe)
50 | not (occurs x c) -> return [c]
51 | otherwise ->
52 do Forall xs cs tipe <- rescheme s
53 let ss = [(x,tipe)]
54 constraints = subst ss (cs ++ ccs)
55 c' = y :<<: Forall (cxs ++ xs) constraints (subst ss ctipe)
56 return [ L txt span c' ]
58recordConstraints eq fs t fs' t' =
59 liftM concat . sequence $
60 [ constrain fs fs'
61 , liftM concat . mapM (\(k,ts) -> zipper [] k ts []) . Map.toList $
62 Map.difference fs fs'
63 , liftM concat . mapM (\(k,ts) -> zipper [] k [] ts) . Map.toList $
64 Map.difference fs' fs
65 ]
66 where constrain :: Map.Map String [Type] -> Map.Map String [Type]
67 -> GuidCounter [Located Constraint]
68 constrain as bs = liftM concat . sequence . Map.elems $
69 Map.intersectionWithKey (zipper []) as bs
70 zipper :: [Located Constraint] -> String -> [Type] -> [Type]
71 -> GuidCounter [Located Constraint]
72 zipper cs k xs ys =
73 case (xs,ys) of
74 (a:as, b:bs) -> zipper (eq a b : cs) k as bs
75 ([],[]) -> return cs
76 (as,[]) -> do x <- guid
77 let tipe = RecordT (Map.singleton k as) (VarT x)
78 return (cs ++ [eq t' tipe])
79 ([],bs) -> do x <- guid
80 let tipe = RecordT (Map.singleton k bs) (VarT x)
81 return (cs ++ [eq t tipe])
83solver :: Aliases
84 -> Map.Map X Type
85 -> [Located Constraint]
86 -> GuidCounter (Either String (Map.Map X Type))
87solver _ subs [] = return $ Right subs
88solver aliases subs (L txt span c : cs) =
89 let loc = L txt span
90 eq t1 t2 = loc (t1 :=: t2)
91 solv = solver aliases subs
92 uniError' = uniError (\t1 t2 -> solv (eq t1 t2 : cs)) aliases txt span
93 in case c of
94 -- Destruct Type-constructors
95 t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2) ->
96 if n1 == n2 then solv (zipWith eq ts1 ts2 ++ cs)
97 else uniError' t1 t2
99 LambdaT t1 t2 :=: LambdaT t1' t2' ->
100 solv ([ eq t1 t1', eq t2 t2' ] ++ cs)
102 RecordT fs t :=: RecordT fs' t' ->
103 do cs' <- recordConstraints eq fs t fs' t'
104 solv (cs' ++ cs)
106 -- Type-equality
107 VarT x :=: VarT y
108 | x == y -> solv cs
109 | otherwise ->
110 case (Map.lookup x subs, Map.lookup y subs) of
111 (Just (Super xts), Just (Super yts)) ->
112 let ts = Set.intersection xts yts
113 setXY t = Map.insert x t . Map.insert y t
114 in case Set.toList ts of
115 [] -> unionError txt span xts yts
116 [t] -> let cs1 = subst [(x,t),(y,t)] cs in
117 cs1 `seq` solver aliases (setXY t subs) cs1
118 _ -> solver aliases (setXY (Super ts) subs) cs
119 (Just (Super xts), _) ->
120 let cs2 = subst [(y,VarT x)] cs in
121 solver aliases (Map.insert y (VarT x) subs) cs2
122 (_, _) ->
123 let cs3 = subst [(x,VarT y)] cs in
124 solver aliases (Map.insert x (VarT y) subs) cs3
126 VarT x :=: t -> do
127 if x `occurs` t then occursError txt span (VarT x) t else
128 (case Map.lookup x subs of
129 Nothing ->
130 let cs4 = subst [(x,t)] cs
131 subs' = Map.map (subst [(x,t)]) $ Map.insert x t subs
132 in solver aliases subs' cs4
133 Just (Super ts) ->
134 let ts' = Set.intersection ts (Set.singleton t) in
135 case Set.toList ts' of
136 [] -> solv (loc (t :<: Super ts) : cs)
137 [t'] -> let cs5 = subst [(x,t)] cs in
138 solver aliases (Map.insert x t' subs) cs5
139 _ -> solver aliases (Map.insert x (Super ts') subs) cs
140 Just t' -> solv (loc (t' :=: t) : cs)
141 )
143 t :=: VarT x -> solv ((loc (VarT x :=: t)) : cs)
145 t1 :=: t2 | t1 == t2 -> solv cs
146 | otherwise -> uniError' t1 t2
148 -- subtypes
149 VarT x :<: Super ts ->
150 case Map.lookup x subs of
151 Nothing -> solver aliases (Map.insert x (Super ts) subs) cs
152 Just (Super ts') ->
153 case Set.toList $ Set.intersection ts ts' of
154 [] -> unionError txt span ts ts'
155 [t] -> solver aliases (Map.insert x t subs) (subst [(x,t)] cs)
156 ts'' -> solver aliases subs' cs
157 where subs' = Map.insert x (Super $ Set.fromList ts'') subs
159 ADT "List" [t] :<: Super ts
160 | any f (Set.toList ts) -> solv cs
161 | otherwise -> subtypeError txt span (ADT "List" [t]) (Super ts)
162 where f (ADT "List" [VarT _]) = True
163 f (ADT "List" [t']) = dealias aliases t == t'
164 f _ = False
166 t :<: Super ts
167 | Set.member t ts -> solv cs
168 | Set.member (dealias aliases t) ts -> solv cs
169 | otherwise -> subtypeError txt span t (Super ts)
171 x :<<: s
172 | any (occurs x) cs ->
173 do css <- mapM (schemeSub aliases x s) cs
174 case lefts css of
175 err : _ -> return $ Left err
176 [] -> solv (concat (rights css))
177 | otherwise ->
178 do (t,cs7) <- concretize s
179 solv (cs ++ loc (VarT x :=: t) : cs7)
181showMsg msg = case msg of
182 Just str -> "\nIn context: " ++ str
183 Nothing -> ""
185occursError msg span t1 t2 =
186 return . Left $ concat
187 [ "Type error (" ++ show span ++ "):\n"
188 , "Occurs check: cannot construct the infinite type:\n"
189 , show t1, " = ", show t2, showMsg msg ]
191uniError solveWith aliases msg span t1 t2 =
192 let t1' = dealias aliases t1
193 t2' = dealias aliases t2
194 in if t1 /= t1' || t2 /= t2'
195 then solveWith t1' t2'
196 else return . Left $ concat
197 [ "Type error (" ++ show span ++ "):\n"
198 , show t1, " is not equal to ", show t2, showMsg msg ]
200unionError msg span ts ts' =
201 return . Left $ concat
202 [ "Type error (" ++ show span ++ "):\n"
203 , "There are no types in both "
204 , show (Super ts), " and ", show (Super ts'), showMsg msg ]
206subtypeError msg span t s =
207 return . Left $ concat
208 [ "Type error (" ++ show span ++ "):\n"
209 , show t, " is not a ", show s, showMsg msg ]