module Term where

import Monad
			   
data Term a b = F a [Term a b] | V b

type Subst a b c = b -> Term a c

instance Monad (Term a) where V b >>= f    = f b
			      F a ts >>= f = F a (map (>>=f) ts)
			      return = V

notIn :: Eq b => b -> Term a b -> Bool
x `notIn` V y    = x /= y
x `notIn` F _ ts = all (notIn x) ts

unify :: (Eq a,Eq b) => Term a b -> Term a b -> Maybe (Subst a b b)
unify (V x) (V y)       = Just (if x == y then V else upd V x (V y))
unify (V x) t           = do guard (x `notIn` t); Just (upd V x t)
unify t (V x)           = unify (V x) t
unify (F x ts) (F y us) = do guard (x == y); unifyall ts us

unifyall :: (Eq a,Eq b) => [Term a b] -> [Term a b] -> Maybe (Subst a b b)
unifyall [] [] 	       = Just V
unifyall (t:ts) (u:us) = do f <- unify t u
                            g <- unifyall (map (>>=f) ts) (map (>>=f) us)
       	 	            Just ((>>= g) . f)
unifyall _ _	       = Nothing

upd :: Eq a => (a -> b) -> a -> b -> a -> b
upd f a b x = if x == a then b else f x

data TypeConstr = List | Prod | Func | INT | BOOL