git.iko.soy/elk
on eeeaad8 help sign in
elk/elm/src/Types/Solver.hs
204 lines 8.0 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
17import System.IO.Unsafe
19isSolved ss (C _ _ (t1 :=: t2)) = t1 == t2
20isSolved ss (C _ _ (x :<<: _)) = isJust (lookup x ss)
21isSolved ss c = False
23crush :: Scheme -> GuidCounter (Either String Scheme)
24crush (Forall xs cs t) =
25 do subs <- solver cs Map.empty
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 (C 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 x s c = do s' <- crush s
40 case s' of
41 Right s'' -> Right `liftM` schemeSub' x s'' c
42 Left err -> return $ Left err
44schemeSub' x s c@(C txt span constraint) =
45 case constraint of
46 (t1 :=: t2) -> schemeSubHelp txt span x s t1 (:=:) t2
47 (t1 :<: t2) -> schemeSubHelp txt span x s t1 (:<:) t2
48 (y :<<: Forall cxs ccs ctipe)
49 | not (occurs x c) -> return [c]
50 | otherwise ->
51 do Forall xs cs tipe <- rescheme s
52 let ss = [(x,tipe)]
53 constraints = subst ss (cs ++ ccs)
54 c' = y :<<: Forall (cxs ++ xs) constraints (subst ss ctipe)
55 return [ C txt span c' ]
57p x = unsafePerformIO (print x) `seq` x
59recordConstraints eq fs t fs' t' =
60 liftM (p . 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 . p $ (cs ++ [eq t' tipe])
80 ([],bs) -> do x <- guid
81 let tipe = RecordT (Map.singleton k bs) (VarT x)
82 return . p $ (cs ++ [eq t tipe])
84solver :: [Context Constraint]
85 -> Map.Map X Type
86 -> GuidCounter (Either String (Map.Map X Type))
87solver [] subs = return $ Right subs
88solver (C txt span c : cs) subs =
89 let ctx = C txt span in
90 let eq t1 t2 = ctx (t1 :=: t2) in
91 case c of
92 -- Destruct Type-constructors
93 t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2) ->
94 if n1 /= n2 then uniError txt span t1 t2 else
95 solver (zipWith eq ts1 ts2 ++ cs) subs
97 LambdaT t1 t2 :=: LambdaT t1' t2' ->
98 solver ([ eq t1 t1', eq t2 t2' ] ++ cs) subs
100 RecordT fs t :=: RecordT fs' t' ->
101 unsafePerformIO (print c) `seq`
102 do cs' <- recordConstraints eq fs t fs' t'
103 solver (cs' ++ cs) subs
105 -- Type-equality
106 VarT x :=: VarT y
107 | x == y -> solver cs subs
108 | otherwise ->
109 case (Map.lookup x subs, Map.lookup y subs) of
110 (Just (Super xts), Just (Super yts)) ->
111 let ts = Set.intersection xts yts
112 setXY t = Map.insert x t . Map.insert y t
113 in case Set.toList ts of
114 [] -> unionError txt span xts yts
115 [t] -> let cs1 = subst [(x,t),(y,t)] cs in
116 cs1 `seq` solver cs1 (setXY t subs)
117 _ -> solver cs $ setXY (Super ts) subs
118 (Just (Super xts), _) ->
119 let cs2 = subst [(y,VarT x)] cs in
120 solver cs2 $ Map.insert y (VarT x) subs
121 (_, _) ->
122 let cs3 = subst [(x,VarT y)] cs in
123 solver cs3 $ Map.insert x (VarT y) subs
125 VarT x :=: t -> do
126 if x `occurs` t then occursError txt span (VarT x) t else
127 (case Map.lookup x subs of
128 Nothing -> let cs4 = subst [(x,t)] cs in
129 solver cs4 . Map.map (subst [(x,t)]) $
130 Map.insert x t subs
131 Just (Super ts) ->
132 let ts' = Set.intersection ts (Set.singleton t) in
133 case Set.toList ts' of
134 [] -> solver (ctx (t :<: Super ts) : cs) subs
135 [t'] -> let cs5 = subst [(x,t)] cs in
136 solver cs5 $ Map.insert x t' subs
137 _ -> solver cs $ Map.insert x (Super ts') subs
138 Just t' -> solver (ctx (t' :=: t) : cs) subs
139 )
141 t :=: VarT x -> solver ((ctx (VarT x :=: t)) : cs) subs
143 t1 :=: t2 | t1 == t2 -> solver cs subs
144 | otherwise -> uniError txt span t1 t2
146 -- subtypes
147 VarT x :<: Super ts ->
148 case Map.lookup x subs of
149 Nothing -> solver cs $ Map.insert x (Super ts) subs
150 Just (Super ts') ->
151 case Set.toList $ Set.intersection ts ts' of
152 [] -> unionError txt span ts ts'
153 [t] -> solver (subst [(x,t)] cs) $ Map.insert x t subs
154 ts'' -> solver cs $
155 Map.insert x (Super $ Set.fromList ts'') subs
157 ADT "List" [t] :<: Super ts
158 | any f (Set.toList ts) -> solver cs subs
159 | otherwise -> subtypeError txt span (ADT "List" [t]) (Super ts)
160 where f (ADT "List" [VarT _]) = True
161 f (ADT "List" [t']) = t == t'
162 f _ = False
164 t :<: Super ts
165 | Set.member t ts -> solver cs subs
166 | otherwise -> subtypeError txt span t (Super ts)
168 x :<<: s
169 | any (occurs x) cs ->
170 do css <- mapM (schemeSub x s) cs
171 case lefts css of
172 err : _ -> return $ Left err
173 [] -> solver (concat (rights css)) subs
174 | otherwise ->
175 do (t,cs7) <- concretize s
176 let cs'' = (cs ++ ctx (VarT x :=: t) : cs7)
177 solver cs'' subs
179showMsg msg = case msg of
180 Just str -> "\nIn context: " ++ str
181 Nothing -> ""
183occursError msg span t1 t2 =
184 return . Left $ concat
185 [ "Type error (" ++ show span ++ "):\n"
186 , "Occurs check: cannot construct the infinite type:\n"
187 , show t1, " = ", show t2, showMsg msg ]
189uniError msg span t1 t2 =
190 return . Left $ concat
191 [ "Type error (" ++ show span ++ "):\n"
192 , show t1, " is not equal to ", show t2, showMsg msg ]
194unionError msg span ts ts' =
195 return . Left $ concat
196 [ "Type error (" ++ show span ++ "):\n"
197 , "There are no types in both "
198 , show (Super ts), " and ", show (Super ts'), showMsg msg ]
200subtypeError msg span t s =
201 return . Left $ concat
202 [ "Type error (" ++ show span ++ "):\n"
203 , show t, " is not a ", show s, showMsg msg ]