on ab53fac help sign in
elk/compiler/Type/Unify.hs
204 lines 8.7 kB history raw
1module Type.Unify (unify) where
3import Type.Type
4import qualified Data.UnionFind.IO as UF
5import qualified Data.Map as Map
6import qualified Data.Maybe as Maybe
7import qualified Type.State as TS
8import Control.Arrow (first,second)
9import Control.Monad.State
10import SourceSyntax.Location
11import Type.PrettyPrint
12import Text.PrettyPrint (render)
14unify :: SrcSpan -> Variable -> Variable -> StateT TS.SolverState IO ()
15unify span variable1 variable2 = do
16 equivalent <- liftIO $ UF.equivalent variable1 variable2
17 if equivalent then return ()
18 else actuallyUnify span variable1 variable2
20actuallyUnify :: SrcSpan -> Variable -> Variable -> StateT TS.SolverState IO ()
21actuallyUnify span variable1 variable2 = do
22 desc1 <- liftIO $ UF.descriptor variable1
23 desc2 <- liftIO $ UF.descriptor variable2
24 let unify' = unify span
26 name' :: Maybe String
27 name' = case (name desc1, name desc2) of
28 (Just name1, Just name2) ->
29 case (flex desc1, flex desc2) of
30 (_, Flexible) -> Just name1
31 (Flexible, _) -> Just name2
32 (Is Number, Is _) -> Just name1
33 (Is _, Is Number) -> Just name2
34 (Is _, Is _) -> Just name1
35 (_, _) -> Nothing
36 (Just name1, _) -> Just name1
37 (_, Just name2) -> Just name2
38 _ -> Nothing
40 flex' :: Flex
41 flex' = case (flex desc1, flex desc2) of
42 (f, Flexible) -> f
43 (Flexible, f) -> f
44 (Is Number, Is _) -> Is Number
45 (Is _, Is Number) -> Is Number
46 (Is super, Is _) -> Is super
47 (_, _) -> Flexible
49 rank' :: Int
50 rank' = min (rank desc1) (rank desc2)
52 merge1 :: StateT TS.SolverState IO ()
53 merge1 = liftIO $ do
54 if rank desc1 < rank desc2 then UF.union variable2 variable1
55 else UF.union variable1 variable2
56 UF.modifyDescriptor variable1 $ \desc ->
57 desc { structure = structure desc1, flex = flex', name = name' }
59 merge2 :: StateT TS.SolverState IO ()
60 merge2 = liftIO $ do
61 if rank desc1 < rank desc2 then UF.union variable2 variable1
62 else UF.union variable1 variable2
63 UF.modifyDescriptor variable2 $ \desc ->
64 desc { structure = structure desc2, flex = flex', name = name' }
66 merge = if rank desc1 < rank desc2 then merge1 else merge2
68 fresh :: Maybe (Term1 Variable) -> StateT TS.SolverState IO Variable
69 fresh structure = do
70 var <- liftIO . UF.fresh $ Descriptor {
71 structure = structure, rank = rank', flex = flex',
72 name = name', copy = Nothing, mark = noMark
73 }
74 TS.register var
76 flexAndUnify var = do
77 liftIO $ UF.modifyDescriptor var $ \desc -> desc { flex = Flexible }
78 unify' variable1 variable2
80 unifyNumber svar name
81 | name `elem` ["Int","Float","number"] = flexAndUnify svar
82 | otherwise = TS.addError span (Just hint) variable1 variable2
83 where hint = "A number must be an Int or Float"
85 comparableError maybe =
86 TS.addError span (Just $ Maybe.fromMaybe msg maybe) variable1 variable2
87 where msg = "A comparable must be an Int, Float, Char, String, list, or tuple"
89 unifyComparable var name
90 | name `elem` ["Int","Float","Char","String","comparable"] = flexAndUnify var
91 | otherwise = comparableError Nothing
93 unifyComparableStructure varSuper varFlex =
94 do struct <- liftIO $ collectApps varFlex
95 case struct of
96 Other -> comparableError Nothing
97 List v -> do flexAndUnify varSuper
98 unify' v =<< liftIO (var $ Is Comparable)
99 Tuple vs
100 | length vs > 6 ->
101 comparableError $ Just "Cannot compare a tuple with more than 6 elements"
102 | otherwise ->
103 do flexAndUnify varSuper
104 cmpVars <- liftIO $ forM [1..length vs] $ \_ -> var (Is Comparable)
105 zipWithM_ unify' vs cmpVars
107 unifyAppendable varSuper varFlex =
108 do struct <- liftIO $ collectApps varFlex
109 case struct of
110 List _ -> flexAndUnify varSuper
111 _ -> comparableError Nothing
113 rigidError variable = TS.addError span (Just hint) variable1 variable2
114 where
115 var = "'" ++ render (pretty Never variable) ++ "'"
116 hint = concat
117 [ "This probably relates to a type annotation. A type "
118 , "annotation may say ", var, " but should be a more "
119 , "specific type. Also, type variables are not "
120 , "shared between type annotations, so ", var, " in one "
121 , "is not the same as " ++ var ++ " in another. "
122 , "Something like that happened" ]
124 superUnify =
125 case (flex desc1, flex desc2, name desc1, name desc2) of
126 (Is super1, Is super2, _, _)
127 | super1 == super2 -> merge
128 (Is Number, Is Comparable, _, _) -> merge1
129 (Is Comparable, Is Number, _, _) -> merge2
131 (Is Number, _, _, Just name) -> unifyNumber variable1 name
132 (_, Is Number, Just name, _) -> unifyNumber variable2 name
134 (Is Comparable, _, _, Just name) -> unifyComparable variable1 name
135 (_, Is Comparable, Just name, _) -> unifyComparable variable2 name
136 (Is Comparable, _, _, _) -> unifyComparableStructure variable1 variable2
137 (_, Is Comparable, _, _) -> unifyComparableStructure variable2 variable1
139 (Is Appendable, _, _, Just ctor)
140 | ctor `elem` ["Text.Text","String"] -> flexAndUnify variable1
141 (_, Is Appendable, Just ctor, _)
142 | ctor `elem` ["Text.Text","String"] -> flexAndUnify variable2
143 (Is Appendable, _, _, _) -> unifyAppendable variable1 variable2
144 (_, Is Appendable, _, _) -> unifyAppendable variable2 variable1
146 (Rigid, _, _, _) -> rigidError variable1
147 (_, Rigid, _, _) -> rigidError variable2
148 _ -> TS.addError span Nothing variable1 variable2
150 case (structure desc1, structure desc2) of
151 (Nothing, Nothing) | flex desc1 == Flexible && flex desc1 == Flexible -> merge
152 (Nothing, _) | flex desc1 == Flexible -> merge2
153 (_, Nothing) | flex desc2 == Flexible -> merge1
155 (Just (Var1 v), _) -> unify' v variable2
156 (_, Just (Var1 v)) -> unify' v variable1
158 (Nothing, _) -> superUnify
159 (_, Nothing) -> superUnify
161 (Just type1, Just type2) ->
162 case (type1,type2) of
163 (App1 term1 term2, App1 term1' term2') ->
164 do merge
165 unify' term1 term1'
166 unify' term2 term2'
167 (Fun1 term1 term2, Fun1 term1' term2') ->
168 do merge
169 unify' term1 term1'
170 unify' term2 term2'
172 (EmptyRecord1, EmptyRecord1) ->
173 return ()
175 (Record1 fields ext, EmptyRecord1) | Map.null fields -> unify' ext variable2
176 (EmptyRecord1, Record1 fields ext) | Map.null fields -> unify' ext variable1
178 (Record1 fields1 ext1, Record1 fields2 ext2) ->
179 do sequence . concat . Map.elems $ Map.intersectionWith (zipWith unify') fields1 fields2
180 let mkRecord fs ext = fresh . Just $ Record1 fs ext
181 case (Map.null fields1', Map.null fields2') of
182 (True , True ) -> unify' ext1 ext2
183 (True , False) -> do
184 record2' <- mkRecord fields2' ext2
185 unify' ext1 record2'
186 (False, True ) -> do
187 record1' <- mkRecord fields1' ext1
188 unify' record1' ext2
189 (False, False) -> do
190 record1' <- mkRecord fields1' =<< fresh Nothing
191 record2' <- mkRecord fields2' =<< fresh Nothing
192 unify' record1' ext2
193 unify' ext1 record2'
194 where
195 fields1' = unmerged fields1 fields2
196 fields2' = unmerged fields2 fields1
198 unmerged a b = Map.filter (not . null) $ Map.union (Map.intersectionWith eat a b) a
200 eat (x:xs) (y:ys) = eat xs ys
201 eat xs ys = xs
203 _ -> TS.addError span Nothing variable1 variable2