module type unif =
sig
type gterm = 
  |Gvar of string
  |Node of string * gterm list
  
val applysubst: (gterm * gterm) list -> gterm -> gterm

val gunify: gterm * gterm -> (gterm * gterm) list  

val unifylist: (gterm * gterm) list -> (gterm * gterm) list 

val newvar : unit -> gterm

val initvar : unit -> unit 

end




module Unif : unif =
struct

type gterm = 
  |Gvar of string
  |Node of string * gterm list

type subst = (gterm * gterm) list
 
let emptysubst = []

let newassociation (x,t) = [(x,t)]

let rec map f l =
  match l with
  [] -> []
  |(a::ll) -> ((f a)::(map f ll))

let rec assoc (st,s) =
   match s with 
   [] -> st
   |((x,t)::y) -> if x = st then t else assoc(st,y)

let rec applysubst s t =
  match t with
  (Gvar(x)) -> assoc(Gvar(x),s)
  |(Node(x,y)) -> Node(x,map (applysubst s) y)

    
let rec occurs (x,s) =
  match s with
  [] -> false
  |((y,t)::z) -> if x=y then true else occurs(x,z)
  
let rec simpl (sigma1,sigma2) = 
  match sigma2 with
  [] -> []
  |((x,t)::y) -> if occurs (x,sigma1) 
                 then simpl(sigma1,y)
                 else ((x,t)::(simpl(sigma1,y))) 

let rec compose (sigma1,sigma2) =
   match sigma1 with
   [] -> simpl(sigma1,sigma2)
   |((x,t)::s) -> let n = applysubst sigma2 t in
                  if n = x 
                  then compose(s,sigma2)
                  else ((x, n)::(compose(s,sigma2)))

let rec bigor l =
   match l with
   [] -> false
   |(a::b) -> if a then true else bigor(b)

let rec occur_in_term x t =
   match t with
   Gvar(y) -> if x=t then true else false
   |Node(_,l) -> bigor(map (occur_in_term x) l)

let rec gunify (pat,ter) =
  match (pat, ter) with
  |(Gvar(x),Gvar(y)) -> if x = y then emptysubst else
                        newassociation(pat,ter)
  |(Gvar(x),t) -> if occur_in_term pat ter 
                 then failwith ("no unification - left occur") 
                 else newassociation(pat,ter)
  |(t,Gvar(x)) -> if occur_in_term ter pat 
                 then failwith ("no unification - right occur") 
                 else newassociation(ter,pat)
  |(Node(x,lp),Node(y,lt)) -> if x = y 
                              then lgunify(lp,lt)
                              else failwith ("no unification - different 
                              constructors")
  and lgunify (lp,lt) =
  match (lp,lt) with
  ([],[]) -> emptysubst
  |((p1::pp),(t1::tt)) -> let sigma = gunify(p1,t1) in
                          compose(sigma,
                          (lgunify 
                             (map (applysubst sigma) pp,
                              map (applysubst sigma) tt)))
  | (_,_) -> failwith ("no unification - different arity")

let rec appplys (s,l) =
   match l with
     |[] -> []
     |(a,b)::l1 -> [(((applysubst s) a),((applysubst s) 
     b))] @ appplys(s,l1) 

  
let rec unifylist (l) =
   match l with
     |[] -> emptysubst
     |(a,b)::l1 -> let sigma = gunify(a,b) in
                     compose(sigma, 
                     unifylist(appplys(sigma,l1)))          

let (newvar,initvar) =
   let count = ref(-1) in
   (fun () -> count := !count +1;
              Gvar("var" ^ (string_of_int !count))),
   (fun () -> count := -1)

end