@@ -2,59 +2,83 @@ module Type.Unify (unify) where
3import Type.Type
3import Type.Type
4import qualified Data.UnionFind.IO as UF
4import qualified Data.UnionFind.IO as UF
5+import qualified Type.Pool as Pool
6+import Control.Arrow (first,second)
7+import Control.Monad.State
6−success = return []
9+unify :: Variable -> Variable -> StateT (Pool.Pool, [String]) IO ()
7−
10+unify variable1 variable2 = do
11+ equivalent <- liftIO $ UF.equivalent variable1 variable2
12+ if equivalent then return ()
8−unify register variable1 variable2 =
13+ else actuallyUnify variable1 variable2
9− do equivalent <- UF.equivalent variable1 variable2
14+
10− if equivalent then success else do
15+actuallyUnify :: Variable -> Variable -> StateT (Pool.Pool, [String]) IO ()
16+actuallyUnify variable1 variable2 = do
11− desc1 <- UF.descriptor variable1
17+ desc1 <- liftIO $ UF.descriptor variable1
12− desc2 <- UF.descriptor variable2
18+ desc2 <- liftIO $ UF.descriptor variable2
19+ let name' :: Maybe String
13− let name' = case (name desc1, name desc2) of
20+ name' = case (name desc1, name desc2) of
14− (Just name1, Just name2)
21+ (Just name1, Just name2)
15− | name1 == name2 -> Just name1
22+ | name1 == name2 -> Just name1
16− | flex desc1 /= Flexible -> Just name1
23+ | flex desc1 /= Flexible -> Just name1
17− | flex desc2 /= Flexible -> Just name2
24+ | flex desc2 /= Flexible -> Just name2
18− | otherwise -> Nothing
25+ | otherwise -> Nothing
19− (Just name1, _) -> Just name1
26+ (Just name1, _) -> Just name1
20− (_, Just name2) -> Just name2
27+ (_, Just name2) -> Just name2
21− _ -> Nothing
28+ _ -> Nothing
23− flex' = if flex desc1 /= Flexible then flex desc1 else
31+ flex' = if flex desc1 /= Flexible then flex desc1 else
24− if flex desc2 /= Flexible then flex desc2 else Flexible
32+ if flex desc2 /= Flexible then flex desc2 else Flexible
26− rank' = min (rank desc1) (rank desc2)
35+ rank' = min (rank desc1) (rank desc2)
37+ merge1 :: StateT (Pool.Pool, [String]) IO ()
28− merge1 = do
38+ merge1 = liftIO $ do
29− UF.union variable2 variable1
39+ UF.union variable2 variable1
30− UF.setDescriptor variable1 (desc1 { flex = flex', name = name', rank = rank', mark = undefined })
40+ UF.setDescriptor variable1 (desc1 { flex = flex', name = name', rank = rank', mark = undefined })
42+ merge2 :: StateT (Pool.Pool, [String]) IO ()
32− merge2 = do
43+ merge2 = liftIO $ do
33− UF.union variable1 variable2
44+ UF.union variable1 variable2
34− UF.setDescriptor variable2 (desc2 { flex = flex', name = name', rank = rank', mark = undefined })
45+ UF.setDescriptor variable2 (desc2 { flex = flex', name = name', rank = rank', mark = undefined })
47+ fresh :: Maybe (Term1 Variable) -> StateT (Pool.Pool, [String]) IO Variable
36− fresh structure = -- gotta register this
48+ fresh structure = do
37− UF.fresh $ Descriptor {
49+ var <- liftIO . UF.fresh $ Descriptor {
38 structure = structure, rank = rank', flex = flex', name = name', mark = undefined
50 structure = structure, rank = rank', flex = flex', name = name', mark = undefined
54+ mistake :: String -> StateT (Pool.Pool, [String]) IO ()
55+ mistake err = modify $ second (err:)
57+ case (structure desc1, structure desc2) of
58+ (Nothing, _) | flex desc1 == Flexible -> merge2
59+ (_, Nothing) | flex desc2 == Flexible -> merge1
61+ (Just (Var1 v), _) -> unify v variable2
62+ (_, Just (Var1 v)) -> unify v variable1
64+ (Nothing, _) -> mistake "Cannot unify rigid type variable."
65+ (_, Nothing) -> mistake "Cannot unify rigid type variable."
67+ (Just type1, Just type2) ->
68+ case (type1,type2) of
69+ (App1 term1 term2, App1 term1' term2') ->
73+ (Fun1 term1 term2, Fun1 term1' term2') ->
78+ (EmptyRecord1, EmptyRecord1) ->
81+ (Record1 fields1 ext1, Record1 fields2 ext2) ->
82+ mistake "did not write record unification yet"
41− case (structure desc1, structure desc2) of
84+ _ -> mistake "Could not unify types"
42− (Nothing, _) | flex desc1 == Flexible -> merge2 >> success
43− (_, Nothing) | flex desc2 == Flexible -> merge1 >> success
44− (Just (Var1 v), _) -> unify register v variable2
45− (_, Just (Var1 v)) -> unify register v variable1
46− (Nothing, _) -> return ["Cannot unify rigid type variable."]
47− (_, Nothing) -> return ["Cannot unify rigid type variable."]
48− (Just type1, Just type2) ->
49− case (type1,type2) of
50− (App1 term1 term2, App1 term1' term2') ->
52− ok1 <- unify register term1 term1'
53− ok2 <- unify register term2 term2'
55− (Fun1 term1 term2, Fun1 term1' term2') ->
57− ok1 <- unify register term1 term1'
58− ok2 <- unify register term2 term2'