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