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