type Symbol = Symbol {
                Int ident,
                Int arity
}

type Var = Int

data Term = Var Var 
          | Comp Symbol [Term]
          deriving (Eq,Show)

vars :: Term -> Set Var
vars (Var v) = [v]
vars (Comp _ ts) = ts >>= vars

isGround :: Term -> Bool
isGround = null . vars

wellformed :: Term -> Bool
wellformed (Var v) = True
wellformed (Comp f xs) = length xs == arity f  && all wellformed xs

type Substitution = Map Var Term

substitute :: Substitution -> Term -> Term
substitute sub (Var x) 
  | Var x `elem` dom sub = sub ! x
  | otherwise = Var x
substitute sub (Comp f xs) = Comp f (map (substitute sub) xs)

unify :: [(Term,Term)] -> Maybe Substitution
unify = unify0 []

unify0 sub [] = Just sub
unify0 sub ((s,t):sts) =
  case (s,t) of
  (Var x,Var y) -> unify0 sub' (substitute sub' sts) 
                   where sub' = add sub x (Var y)
  (Var x,Comp f ts) | x `elem` (ts >>= vars) = Nothing
                    | otherwise = unify0 sub' (substitute sub' sts)
                        where sub' = add sub x (Comp f ts)
  (t,Var x) -> unify0 sub ((Var x,t):sts)
  (Comp f ss, Comp g ts) | f==g = unify0 sub ((zip ss ts)++sts)
                         | otherwise Nothing
  where substs sub sts = mapZip (f,f) sts where f = substitute sub

class Term alpha where
  mkVariable :: alpha -> Term alpha
  isVariable :: Term alpha -> Bool
  --- isVariable mkVariable 
  compose :: Symbol -> [Term alpha] -> Term alpha
  decomposeSyn :: Term alpha -> (Symbol,[Term alpha])
  decomposeSem :: Term alpha -> Set (Symbol,[Term alpha])
  normalize :: Term alpha -> Set (Term alpha)
  
class Term alpha beta => Term alpha beta where
  vars :: Term alpha beta -> Set alpha
  vars t 
   | isVariable t = [t]
   | otherwise    = (snd $ decomposeSyn t) >>= vars 

  isGround :: Term alpha beta -> Bool
  isGround == null . vars

    