git.iko.soy/elk
on d15e080 help sign in
elk/elm/src/Types/Solver.hs
157 lines 6.1 kB history raw
2module Types.Solver (solver) where
4import Control.Arrow (second)
5import Control.Monad (liftM)
6import Data.Either (lefts,rights)
7import Data.List (foldl')
8import Data.Maybe (isJust)
9import qualified Data.Set as Set
10import qualified Data.Map as Map
11import Guid
12import Types.Types
13import Types.Constrain
14import Types.Substitutions
17eq ctx t1 t2 = Context ctx (t1 :=: t2)
19isSolved ss (Context _ (t1 :=: t2)) = t1 == t2
20isSolved ss (Context _ (x :<<: _)) = isJust (lookup x ss)
21isSolved ss c = False
23crush (Forall xs cs t) =
24 do subs <- solver cs Map.empty
25 return $ do ss' <- subs
26 let ss = Map.toList ss'
27 cs' = filter (not . isSolved ss) (subst ss cs)
28 return $ Forall xs cs' (subst ss t)
30schemeSubHelp ctx x s t1 rltn t2 = do
31 (t1',cs1) <- sub t1
32 (t2',cs2) <- sub t2
33 return (Context ctx (rltn t1' t2') : cs1 ++ cs2)
34 where sub t | not (occurs x t) = return (t, [])
35 | otherwise = do (st, cs) <- concretize s
36 return (subst [(x,st)] t, cs)
38schemeSub x s c = do s' <- crush s
39 case s' of
40 Right s'' -> Right `liftM` schemeSub' x s'' c
41 Left err -> return $ Left err
43schemeSub' x s (Context ctx (t1 :=: t2)) = schemeSubHelp ctx x s t1 (:=:) t2
44schemeSub' x s (Context ctx (t1 :<: t2)) = schemeSubHelp ctx x s t1 (:<:) t2
45schemeSub' x s c@(Context ctx (y :<<: Forall cxs ccs ctipe))
46 | not (occurs x c) = return [c]
47 | otherwise =
48 do Forall xs cs tipe <- rescheme s
49 let ss = [(x,tipe)]
50 constraints = subst ss (cs ++ ccs)
51 c' = y :<<: Forall (cxs ++ xs) constraints (subst ss ctipe)
52 return [ Context ctx c' ]
55solver :: [Context String Constraint]
56 -> Map.Map X Type
57 -> GuidCounter (Either String (Map.Map X Type))
58solver [] subs = return $ Right subs
60-------- Destruct Type-constructors --------
62solver ((Context ctx (t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2))) : cs) subs =
63 if n1 /= n2 then uniError ctx t1 t2 else
64 solver (zipWith (eq ctx) ts1 ts2 ++ cs) subs
65solver ((Context ctx (LambdaT t1 t2 :=: LambdaT t1' t2')) : cs) subs =
66 solver ([ eq ctx t1 t1', eq ctx t2 t2' ] ++ cs) subs
68-------- Type-equality --------
70solver (Context ctx (VarT x :=: VarT y) : cs) subs
71 | x == y = solver cs subs
72 | otherwise =
73 case (Map.lookup x subs, Map.lookup y subs) of
74 (Just (Super xts), Just (Super yts)) ->
75 let ts = Set.intersection xts yts
76 setXY t = Map.insert x t . Map.insert y t
77 in case Set.toList ts of
78 [] -> unionError ctx xts yts
79 [t] -> let cs1 = subst [(x,t),(y,t)] cs in
80 cs1 `seq` solver cs1 (setXY t subs)
81 _ -> solver cs $ setXY (Super ts) subs
82 (Just (Super xts), _) ->
83 let cs2 = subst [(y,VarT x)] cs in
84 solver cs2 $ Map.insert y (VarT x) subs
85 (_, _) ->
86 let cs3 = subst [(x,VarT y)] cs in
87 solver cs3 $ Map.insert x (VarT y) subs
88solver (Context ctx (VarT x :=: t) : cs) subs = do
89 if x `occurs` t then occursError ctx (VarT x) t else
90 (case Map.lookup x subs of
91 Nothing -> let cs4 = subst [(x,t)] cs in
92 solver cs4 . Map.map (subst [(x,t)]) $ Map.insert x t subs
93 Just (Super ts) ->
94 let ts' = Set.intersection ts (Set.singleton t) in
95 case Set.toList ts' of
96 [] -> solver (Context ctx (t :<: Super ts) : cs) subs
97 [t'] -> let cs5 = subst [(x,t)] cs in
98 solver cs5 $ Map.insert x t' subs
99 _ -> solver cs $ Map.insert x (Super ts') subs
100 Just t' -> solver (Context ctx (t' :=: t) : cs) subs
101 )
102solver ((Context ctx (t :=: VarT x)) : cs) subs =
103 solver ((Context ctx (VarT x :=: t)) : cs) subs
104solver ((Context ctx (t1 :=: t2)) : cs) subs
105 | t1 == t2 = solver cs subs
106 | otherwise = uniError ctx t1 t2
109-------- subtypes --------
111solver (Context ctx (VarT x :<: Super ts) : cs) subs =
112 case Map.lookup x subs of
113 Nothing -> solver cs $ Map.insert x (Super ts) subs
114 Just (Super ts') ->
115 case Set.toList $ Set.intersection ts ts' of
116 [] -> unionError ctx ts ts'
117 [t] -> solver (subst [(x,t)] cs) $ Map.insert x t subs
118 ts'' -> solver cs $ Map.insert x (Super $ Set.fromList ts'') subs
120solver (Context ctx (ADT "List" [t] :<: Super ts) : cs) subs
121 | any f (Set.toList ts) = solver cs subs
122 | otherwise = subtypeError ctx (ADT "List" [t]) (Super ts)
123 where f (ADT "List" [VarT _]) = True
124 f (ADT "List" [t']) = t == t'
125 f _ = False
127solver (Context ctx (t :<: Super ts) : cs) subs
128 | Set.member t ts = solver cs subs
129 | otherwise = subtypeError ctx t (Super ts)
131solver (Context ctx (x :<<: s) : cs) subs
132 | any (occurs x) cs =
133 do css <- mapM (schemeSub x s) cs
134 case lefts css of
135 err : _ -> return $ Left err
136 [] -> solver (concat (rights css)) subs
137 | otherwise =
138 do (t,cs7) <- concretize s
139 let cs'' = (cs ++ Context ctx (VarT x :=: t) : map (extendCtx ctx) cs7)
140 solver cs'' subs
142occursError ctx t1 t2 =
143 return . Left $ "Type error: Occurs check: cannot construct the infinite type: " ++ show t1 ++
144 " = " ++ show t2 ++
145 " in context " ++ ctx
146uniError ctx t1 t2 =
147 return . Left $ "Type error: " ++ show t1 ++
148 " is not equal to " ++ show t2 ++
149 " in context " ++ ctx
150unionError ctx ts ts' =
151 return . Left $ concat [ "Type error: There are no types in both "
152 , show (Super ts), " and ", show (Super ts')
153 , " in context ", ctx ]
154subtypeError ctx t s =
155 return . Left $ concat [ "Type error: ", show t, " is not a ", show s
156 , " in context ", ctx ]