src/Types/Unify.hs · elk

on f5bdeae help sign in

elk/src/Types/Unify.hs

37 lines 1.1 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

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

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 ((LambdaT t1 t2 :=: LambdaT t1' t2') : cs) subs =

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

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

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

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

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

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

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

29 solver cs subs

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

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

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

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

37tSub _ _ t = t