2013-07-07 10:52:48 +00:00
|
|
|
module Type.Unify (unify) where
|
|
|
|
|
|
|
|
import Type.Type
|
|
|
|
import qualified Data.UnionFind.IO as UF
|
2013-07-09 08:25:50 +00:00
|
|
|
import qualified Type.State as TS
|
2013-07-08 18:03:08 +00:00
|
|
|
import Control.Arrow (first,second)
|
|
|
|
import Control.Monad.State
|
2013-07-10 12:31:57 +00:00
|
|
|
import qualified Text.PrettyPrint as P
|
2013-07-07 10:52:48 +00:00
|
|
|
|
2013-07-09 08:25:50 +00:00
|
|
|
unify :: Variable -> Variable -> StateT TS.SolverState IO ()
|
2013-07-08 18:03:08 +00:00
|
|
|
unify variable1 variable2 = do
|
|
|
|
equivalent <- liftIO $ UF.equivalent variable1 variable2
|
|
|
|
if equivalent then return ()
|
|
|
|
else actuallyUnify variable1 variable2
|
|
|
|
|
2013-07-09 08:25:50 +00:00
|
|
|
actuallyUnify :: Variable -> Variable -> StateT TS.SolverState IO ()
|
2013-07-08 18:03:08 +00:00
|
|
|
actuallyUnify variable1 variable2 = do
|
|
|
|
desc1 <- liftIO $ UF.descriptor variable1
|
|
|
|
desc2 <- liftIO $ UF.descriptor variable2
|
|
|
|
let name' :: Maybe String
|
|
|
|
name' = case (name desc1, name desc2) of
|
2013-07-25 13:48:58 +00:00
|
|
|
(Just name1, Just name2) ->
|
|
|
|
case (flex desc1, flex desc2) of
|
|
|
|
(_, Flexible) -> Just name1
|
|
|
|
(Flexible, _) -> Just name2
|
2013-07-25 16:07:04 +00:00
|
|
|
(Is Number, Is _) -> Just name1
|
|
|
|
(Is _, Is Number) -> Just name2
|
|
|
|
(Is _, Is _) -> Just name1
|
2013-07-25 13:48:58 +00:00
|
|
|
(_, _) -> Nothing
|
2013-07-08 18:03:08 +00:00
|
|
|
(Just name1, _) -> Just name1
|
|
|
|
(_, Just name2) -> Just name2
|
|
|
|
_ -> Nothing
|
|
|
|
|
|
|
|
flex' :: Flex
|
2013-07-25 13:48:58 +00:00
|
|
|
flex' = case (flex desc1, flex desc2) of
|
|
|
|
(f, Flexible) -> f
|
|
|
|
(Flexible, f) -> f
|
2013-07-25 16:07:04 +00:00
|
|
|
(Is Number, Is _) -> Is Number
|
|
|
|
(Is _, Is Number) -> Is Number
|
|
|
|
(Is super, Is _) -> Is super
|
2013-07-25 13:48:58 +00:00
|
|
|
(_, _) -> Flexible
|
2013-07-08 18:03:08 +00:00
|
|
|
|
|
|
|
rank' :: Int
|
|
|
|
rank' = min (rank desc1) (rank desc2)
|
|
|
|
|
2013-07-09 08:25:50 +00:00
|
|
|
merge1 :: StateT TS.SolverState IO ()
|
2013-07-25 13:48:58 +00:00
|
|
|
merge1 = liftIO $ do
|
|
|
|
if rank desc1 < rank desc2 then UF.union variable2 variable1
|
|
|
|
else UF.union variable1 variable2
|
|
|
|
UF.modifyDescriptor variable1 $ \desc ->
|
|
|
|
desc { structure = structure desc1, flex = flex', name = name' }
|
2013-07-08 18:03:08 +00:00
|
|
|
|
2013-07-09 08:25:50 +00:00
|
|
|
merge2 :: StateT TS.SolverState IO ()
|
2013-07-25 13:48:58 +00:00
|
|
|
merge2 = liftIO $ do
|
|
|
|
if rank desc1 < rank desc2 then UF.union variable2 variable1
|
|
|
|
else UF.union variable1 variable2
|
|
|
|
UF.modifyDescriptor variable2 $ \desc ->
|
|
|
|
desc { structure = structure desc2, flex = flex', name = name' }
|
2013-07-12 09:05:03 +00:00
|
|
|
|
|
|
|
merge = if rank desc1 < rank desc2 then merge1 else merge2
|
2013-07-08 18:03:08 +00:00
|
|
|
|
2013-07-09 08:25:50 +00:00
|
|
|
fresh :: Maybe (Term1 Variable) -> StateT TS.SolverState IO Variable
|
2013-07-08 18:03:08 +00:00
|
|
|
fresh structure = do
|
|
|
|
var <- liftIO . UF.fresh $ Descriptor {
|
2013-07-12 09:05:03 +00:00
|
|
|
structure = structure, rank = rank', flex = flex',
|
|
|
|
name = name', copy = Nothing, mark = noMark
|
2013-07-07 10:52:48 +00:00
|
|
|
}
|
2013-07-09 08:25:50 +00:00
|
|
|
TS.register var
|
2013-07-08 18:03:08 +00:00
|
|
|
|
2013-07-24 23:24:16 +00:00
|
|
|
flexAndUnify var = do
|
|
|
|
liftIO $ UF.modifyDescriptor var $ \desc -> desc { flex = Flexible }
|
|
|
|
unify variable1 variable2
|
|
|
|
|
|
|
|
superUnify =
|
|
|
|
case (flex desc1, flex desc2, name desc1, name desc2) of
|
2013-07-25 16:07:04 +00:00
|
|
|
(Is super1, Is super2, _, _)
|
2013-07-25 15:10:01 +00:00
|
|
|
| super1 == super2 -> merge
|
2013-07-25 16:07:04 +00:00
|
|
|
(Is Number, Is Comparable, _, _) -> merge1
|
|
|
|
(Is Comparable, Is Number, _, _) -> merge2
|
2013-07-25 13:48:58 +00:00
|
|
|
|
2013-07-25 16:07:04 +00:00
|
|
|
(Is Number, _, _, Just name)
|
2013-07-25 12:54:21 +00:00
|
|
|
| name `elem` ["Int","Float"] -> flexAndUnify variable1
|
2013-07-25 13:48:58 +00:00
|
|
|
| otherwise -> TS.addError "Expecting a number (Int or Float)" variable1 variable2
|
2013-07-24 23:24:16 +00:00
|
|
|
|
2013-07-25 16:07:04 +00:00
|
|
|
(_, Is Number, Just name, _)
|
2013-07-25 12:54:21 +00:00
|
|
|
| name `elem` ["Int","Float"] -> flexAndUnify variable2
|
2013-07-25 13:48:58 +00:00
|
|
|
| otherwise -> TS.addError "Expecting a number (Int or Float)" variable1 variable2
|
2013-07-24 23:24:16 +00:00
|
|
|
|
2013-07-25 16:07:04 +00:00
|
|
|
(Is Comparable, _, _, Just name)
|
2013-07-25 12:54:21 +00:00
|
|
|
| name `elem` ["Int","Float","Char"] -> flexAndUnify variable1
|
2013-07-25 13:48:58 +00:00
|
|
|
| otherwise -> TS.addError "Expecting something comparable (Int, Float, Char, [comparable])." variable1 variable2
|
2013-07-24 23:24:16 +00:00
|
|
|
|
2013-07-25 16:07:04 +00:00
|
|
|
(_, Is Comparable, Just name, _)
|
2013-07-25 12:54:21 +00:00
|
|
|
| name `elem` ["Int","Float","Char"] -> flexAndUnify variable2
|
2013-07-25 13:48:58 +00:00
|
|
|
| otherwise -> TS.addError "Expecting something comparable (Int, Float, Char, [comparable])." variable1 variable2
|
2013-07-24 23:24:16 +00:00
|
|
|
|
|
|
|
_ -> TS.addError "The following types are not equal" variable1 variable2
|
|
|
|
|
2013-07-08 18:03:08 +00:00
|
|
|
case (structure desc1, structure desc2) of
|
2013-07-12 09:05:03 +00:00
|
|
|
(Nothing, Nothing) | flex desc1 == Flexible && flex desc1 == Flexible -> merge
|
2013-07-08 18:03:08 +00:00
|
|
|
(Nothing, _) | flex desc1 == Flexible -> merge2
|
|
|
|
(_, Nothing) | flex desc2 == Flexible -> merge1
|
|
|
|
|
|
|
|
(Just (Var1 v), _) -> unify v variable2
|
|
|
|
(_, Just (Var1 v)) -> unify v variable1
|
|
|
|
|
2013-07-24 23:24:16 +00:00
|
|
|
(Nothing, _) -> superUnify
|
|
|
|
(_, Nothing) -> superUnify
|
2013-07-08 18:03:08 +00:00
|
|
|
|
|
|
|
(Just type1, Just type2) ->
|
|
|
|
case (type1,type2) of
|
|
|
|
(App1 term1 term2, App1 term1' term2') ->
|
2013-07-12 09:05:03 +00:00
|
|
|
do merge
|
2013-07-08 18:03:08 +00:00
|
|
|
unify term1 term1'
|
|
|
|
unify term2 term2'
|
|
|
|
(Fun1 term1 term2, Fun1 term1' term2') ->
|
2013-07-12 09:05:03 +00:00
|
|
|
do merge
|
2013-07-08 18:03:08 +00:00
|
|
|
unify term1 term1'
|
|
|
|
unify term2 term2'
|
|
|
|
|
|
|
|
(EmptyRecord1, EmptyRecord1) ->
|
|
|
|
return ()
|
|
|
|
|
|
|
|
(Record1 fields1 ext1, Record1 fields2 ext2) ->
|
2013-07-10 12:31:57 +00:00
|
|
|
TS.addError "did not write record unification yet" variable1 variable2
|
2013-07-07 10:52:48 +00:00
|
|
|
|
2013-07-24 23:24:16 +00:00
|
|
|
_ -> TS.addError "could not unify types" variable1 variable2
|
|
|
|
|