git.iko.soy/elk
on 87fa86c help sign in
elk/compiler/Types/Solver.hs
208 lines 8.2 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 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 let t1' = dealias aliases t1
98 t2' = dealias aliases t2
99 in if t1 == t1' && t2 == t2' then uniError txt span t1 t2
100 else solv (ctx (t1' :=: t2') : cs)
102 LambdaT t1 t2 :=: LambdaT t1' t2' ->
103 solv ([ eq t1 t1', eq t2 t2' ] ++ cs)
105 RecordT fs t :=: RecordT fs' t' ->
106 do cs' <- recordConstraints eq fs t fs' t'
107 solv (cs' ++ cs)
109 -- Type-equality
110 VarT x :=: VarT y
111 | x == y -> solv cs
112 | otherwise ->
113 case (Map.lookup x subs, Map.lookup y subs) of
114 (Just (Super xts), Just (Super yts)) ->
115 let ts = Set.intersection xts yts
116 setXY t = Map.insert x t . Map.insert y t
117 in case Set.toList ts of
118 [] -> unionError txt span xts yts
119 [t] -> let cs1 = subst [(x,t),(y,t)] cs in
120 cs1 `seq` solver aliases (setXY t subs) cs1
121 _ -> solver aliases (setXY (Super ts) subs) cs
122 (Just (Super xts), _) ->
123 let cs2 = subst [(y,VarT x)] cs in
124 solver aliases (Map.insert y (VarT x) subs) cs2
125 (_, _) ->
126 let cs3 = subst [(x,VarT y)] cs in
127 solver aliases (Map.insert x (VarT y) subs) cs3
129 VarT x :=: t -> do
130 if x `occurs` t then occursError txt span (VarT x) t else
131 (case Map.lookup x subs of
132 Nothing ->
133 let cs4 = subst [(x,t)] cs
134 subs' = Map.map (subst [(x,t)]) $ Map.insert x t subs
135 in solver aliases subs' cs4
136 Just (Super ts) ->
137 let ts' = Set.intersection ts (Set.singleton t) in
138 case Set.toList ts' of
139 [] -> solv (ctx (t :<: Super ts) : cs)
140 [t'] -> let cs5 = subst [(x,t)] cs in
141 solver aliases (Map.insert x t' subs) cs5
142 _ -> solver aliases (Map.insert x (Super ts') subs) cs
143 Just t' -> solv (ctx (t' :=: t) : cs)
144 )
146 t :=: VarT x -> solv ((ctx (VarT x :=: t)) : cs)
148 t1 :=: t2 | t1 == t2 -> solv cs
149 | otherwise -> uniError txt span t1 t2
151 -- subtypes
152 VarT x :<: Super ts ->
153 case Map.lookup x subs of
154 Nothing -> solver aliases (Map.insert x (Super ts) subs) cs
155 Just (Super ts') ->
156 case Set.toList $ Set.intersection ts ts' of
157 [] -> unionError txt span ts ts'
158 [t] -> solver aliases (Map.insert x t subs) (subst [(x,t)] cs)
159 ts'' -> solver aliases subs' cs
160 where subs' = Map.insert x (Super $ Set.fromList ts'') subs
162 ADT "List" [t] :<: Super ts
163 | any f (Set.toList ts) -> solv cs
164 | otherwise -> subtypeError txt span (ADT "List" [t]) (Super ts)
165 where f (ADT "List" [VarT _]) = True
166 f (ADT "List" [t']) = t == t'
167 f _ = False
169 t :<: Super ts
170 | Set.member t ts -> solv cs
171 | otherwise -> subtypeError txt span t (Super ts)
173 x :<<: s
174 | any (occurs x) cs ->
175 do css <- mapM (schemeSub aliases x s) cs
176 case lefts css of
177 err : _ -> return $ Left err
178 [] -> solv (concat (rights css))
179 | otherwise ->
180 do (t,cs7) <- concretize s
181 solv (cs ++ ctx (VarT x :=: t) : cs7)
183showMsg msg = case msg of
184 Just str -> "\nIn context: " ++ str
185 Nothing -> ""
187occursError msg span t1 t2 =
188 return . Left $ concat
189 [ "Type error (" ++ show span ++ "):\n"
190 , "Occurs check: cannot construct the infinite type:\n"
191 , show t1, " = ", show t2, showMsg msg ]
193uniError msg span t1 t2 =
194 return . Left $ concat
195 [ "Type error (" ++ show span ++ "):\n"
196 , show t1, " is not equal to ", show t2, showMsg msg ]
198unionError msg span ts ts' =
199 return . Left $ concat
200 [ "Type error (" ++ show span ++ "):\n"
201 , "There are no types in both "
202 , show (Super ts), " and ", show (Super ts'), showMsg msg ]
204subtypeError msg span t s =
205 return . Left $ concat
206 [ "Type error (" ++ show span ++ "):\n"
207 , show t, " is not a ", show s, showMsg msg ]