type id = string;;
type term =   | Var of id   | Term of id * term list

(* invariant for substitutions: *) 
(* no id on a lhs occurs in any term earlier in the list *) 
type substitution = (id * term) list

(* check if a variable occurs in a term *) 
let rec occurs (x : id) (t : term)  =   match t with   
    | Var y -> x = y   
    | Term (_, s) -> List.exists (occurs x) s

(* substitute term s for all occurrences of variable x in term t *) 
let rec subst (s : term) (x : id) (t : term)  =  match t with   
    | Var y -> if x = y then s else t   
    | Term (f, u) -> Term (f, List.map (subst s x) u)

(* apply a substitution right to left *) 
let apply (s : substitution) (t : term)  =  List.fold_right (fun (x, u) -> subst u x) s t

(* unify one pair *) 
let rec unify_one (s : term) (t : term)  =   match (s, t) with   
    | (Var x, Var y) -> if x = y then [] else [(x, t)]   
    | (Term (f, sc), Term (g, tc)) ->  
        if f = g && List.length sc = List.length tc  
             then unify (List.combine sc tc)       
             else failwith "not unifiable: head symbol conflict"   
    | ((Var x, (Term (_, _) as t)) 
    | ((Term (_, _) as t), Var x)) ->  
        if occurs x t       
            then failwith "not unifiable: circularity"       
            else [(x, t)]

(* unify a list of pairs *) 
and unify (s : (term * term) list)  =   match s with   
     | [] -> []   
     | (x, y) :: t ->       
	let t2 = unify t in       
	let t1 = unify_one (apply t2 x) (apply t2 y) in  
	t1 @ t2 ;;