git.iko.soy/elk
on 44b2e45 help sign in
elk/src/Types/Unify.hs
71 lines 2.1 kB history raw
2module Unify where
4import Constrain
5import Control.Arrow (second)
6import Control.Monad (liftM)
7import Data.List (foldl')
8import qualified Data.Set as Set
9import Guid
10import Types
12import Control.DeepSeq (NFData (..), deepseq)
14unify hints expr = run $ do
15 cs <- constrain hints expr
16 solver cs []
18solver [] subs = return $ Right subs
20-------- Destruct Type-constructors --------
22solver ((t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2)) : cs) subs =
23 if n1 /= n2 then uniError t1 t2 else
24 solver (zipWith (:=:) ts1 ts2 ++ cs) subs
25solver ((LambdaT t1 t2 :=: LambdaT t1' t2') : cs) subs =
26 solver ([ t1 :=: t1', t2 :=: t2' ] ++ cs) subs
28-------- Type-equality --------
30solver ((VarT x :=: t) : cs) subs =
31 solver (map (cSub x t) cs) . map (second $ tSub x t) $ (x,t):subs
32solver ((t :=: VarT x) : cs) subs =
33 solver (map (cSub x t) cs) . map (second $ tSub x t) $ (x,t):subs
34solver ((t1 :=: t2) : cs) subs =
35 if t1 /= t2 then uniError t1 t2 else solver cs subs
37-------- subtypes --------
39solver ((t1 :<: t2) : cs) subs = do
40 let f x = do y <- guid ; return (x,VarT y)
41 pairs <- mapM f . Set.toList $ getVars t2
42 let t2' = foldr (uncurry tSub) t2 pairs
43 solver ((t1 :=: t2') : cs) subs
46cSub k v (t1 :=: t2) = force $ tSub k v t1 :=: tSub k v t2
47cSub k v (t1 :<: t2) = force $ tSub k v t1 :<: tSub k v t2
49tSub k v t@(VarT x) = if k == x then v else t
50tSub k v (LambdaT t1 t2) = force $ LambdaT (tSub k v t1) (tSub k v t2)
51tSub k v (ADT name ts) = ADT name (map (force . tSub k v) ts)
52tSub _ _ t = t
54getVars (VarT x) = Set.singleton x
55getVars (LambdaT t1 t2) = Set.union (getVars t1) (getVars t2)
56getVars (ADT name ts) = Set.unions $ map getVars ts
57getVars _ = Set.empty
59uniError t1 t2 =
60 return . Left $ "Type error: " ++ show t1 ++ " is not equal to " ++ show t2
62force x = x `deepseq` x
64instance NFData Constraint where
65 rnf (t1 :=: t2) = t1 `deepseq` t2 `deepseq` ()
66 rnf (t1 :<: t2) = t1 `deepseq` t2 `deepseq` ()
68instance NFData Type where
69 rnf (LambdaT t1 t2) = t1 `deepseq` t2 `deepseq` ()
70 rnf (ADT _ ts) = foldl' (\acc x -> x `deepseq` acc) () ts
71 rnf t = t `seq` ()