src/Types/Unify.hs · elk

on 4e15a25 help sign in

elk/src/Types/Unify.hs

57 lines 1.7 kB history raw

2module Unify where

4import Constrain

5import Control.Arrow (second)

6import Control.Monad (liftM)

7import qualified Data.Set as Set

8import Types

10import Guid

12unify hints expr = run $ do

13 cs <- constrain hints expr

14 solver cs []

16solver [] subs = return $ Right subs

18-------- Destruct Type-constructors --------

20solver ((t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2)) : cs) subs =

21 if n1 /= n2 then uniError t1 t2 else

22 solver (zipWith (:=:) ts1 ts2 ++ cs) subs

23solver ((LambdaT t1 t2 :=: LambdaT t1' t2') : cs) subs =

24 solver ([ t1 :=: t1', t2 :=: t2' ] ++ cs) subs

26-------- Type-equality --------

28solver ((VarT x :=: t) : cs) subs =

29 solver (map (cSub x t) cs) . map (second $ tSub x t) $ (x,t):subs

30solver ((t :=: VarT x) : cs) subs =

31 solver (map (cSub x t) cs) . map (second $ tSub x t) $ (x,t):subs

32solver ((t1 :=: t2) : cs) subs =

33 if t1 /= t2 then uniError t1 t2 else solver cs subs

35-------- subtypes --------

37solver ((t1 :<: t2) : cs) subs = do

38 let f x = do y <- guid ; return (x,VarT y)

39 t2' <- foldr (uncurry tSub) t2 `liftM` (mapM f . Set.toList $ getVars t2)

40 solver ((t1 :=: t2') : cs) subs

43cSub k v (t1 :=: t2) = tSub k v t1 :=: tSub k v t2

44cSub k v (t1 :<: t2) = tSub k v t1 :<: tSub k v t2

46tSub k v (VarT x) = if k == x then v else (VarT x)

47tSub k v (LambdaT t1 t2) = LambdaT (tSub k v t1) (tSub k v t2)

48tSub k v (ADT name ts) = ADT name (map (tSub k v) ts)

49tSub _ _ t = t

51getVars (VarT x) = Set.singleton x

52getVars (LambdaT t1 t2) = Set.union (getVars t1) (getVars t2)

53getVars (ADT name ts) = Set.unions $ map getVars ts

54getVars _ = Set.empty

56uniError t1 t2 =

57 return . Left $ "Type error: " ++ show t1 ++ " is not equal to " ++ show t2