git.iko.soy/elk
on 0050157 help sign in
elk/src/Types/Unify.hs
70 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
14force x = x `deepseq` x
16instance NFData Constraint where
17 rnf (t1 :=: t2) = t1 `deepseq` t2 `deepseq` ()
18 rnf (t1 :<: t2) = t1 `deepseq` t2 `deepseq` ()
20instance NFData Type where
21 rnf (LambdaT t1 t2) = t1 `deepseq` t2 `deepseq` ()
22 rnf (ADT _ ts) = foldl' (\acc x -> x `deepseq` acc) () ts
23 rnf t = t `seq` ()
25unify hints expr = run $ do
26 cs <- constrain hints expr
27 solver cs []
29solver [] subs = return $ Right subs
31-------- Destruct Type-constructors --------
33solver ((t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2)) : cs) subs =
34 if n1 /= n2 then uniError t1 t2 else
35 solver (zipWith (:=:) ts1 ts2 ++ cs) subs
36solver ((LambdaT t1 t2 :=: LambdaT t1' t2') : cs) subs =
37 solver ([ t1 :=: t1', t2 :=: t2' ] ++ cs) subs
39-------- Type-equality --------
41solver ((VarT x :=: t) : cs) subs =
42 solver (map (cSub x t) cs) . map (second $ tSub x t) $ (x,t):subs
43solver ((t :=: VarT x) : cs) subs =
44 solver (map (cSub x t) cs) . map (second $ tSub x t) $ (x,t):subs
45solver ((t1 :=: t2) : cs) subs =
46 if t1 /= t2 then uniError t1 t2 else solver cs subs
48-------- subtypes --------
50solver ((t1 :<: t2) : cs) subs = do
51 let f x = do y <- guid ; return (x,VarT y)
52 t2' <- foldl' (uncurry . flip tSub) t2 `liftM` (mapM f . Set.toList $ getVars t2)
53 solver ((t1 :=: t2') : cs) subs
56cSub k v (t1 :=: t2) = force $ tSub k v t1 :=: tSub k v t2
57cSub k v (t1 :<: t2) = force $ tSub k v t1 :<: tSub k v t2
59tSub k v t@(VarT x) = if k == x then v else t
60tSub k v (LambdaT t1 t2) = force $ LambdaT (tSub k v t1) (tSub k v t2)
61tSub k v (ADT name ts) = ADT name (map (force . tSub k v) ts)
62tSub _ _ t = t
64getVars (VarT x) = Set.singleton x
65getVars (LambdaT t1 t2) = Set.union (getVars t1) (getVars t2)
66getVars (ADT name ts) = Set.unions $ map getVars ts
67getVars _ = Set.empty
69uniError t1 t2 =
70 return . Left $ "Type error: " ++ show t1 ++ " is not equal to " ++ show t2