src/Types/Unify.hs · elk

on 0ca86e4 help sign in

elk/src/Types/Unify.hs

53 lines 1.6 kB history raw

2module Unify where

4import Constrain

5import Control.Arrow (second)

6import Types

8unify expr = ( constrain expr, solver (constrain expr) [] )

10solver [] subs = Right subs

12-------- Destruct Type-constructors --------

14solver ((ADT n1 ts1 :<: ADT n2 ts2) : cs) subs =

15 if n1 /= n2 then Left "unification error" else

16 solver (zipWith (:<:) ts1 ts2 ++ cs) subs

18solver ((ADT n1 ts1 :=: ADT n2 ts2) : cs) subs =

19 if n1 /= n2 then Left "unification error" else

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

22solver ((LambdaT t1 t2 :<: LambdaT t1' t2') : cs) subs =

23 solver ([ t1 :<: t1', t2 :<: t2' ] ++ cs) subs

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

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

28-------- subtypes --------

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

31 where cs' = if all isSubtype cs then cs else (cs ++ [t :<: VarT x])

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

34-------- Type-equality --------

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

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

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

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

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

41 if t1 /= t2 then Left $ show t1 ++ " is not equal to " ++ show t2 else

42 solver cs subs

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

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

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

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

50tSub _ _ t = t

52isSubtype (_ :<: _) = True

53isSubtype _ = False