type term = V of int
          | A of int * term list;;

exception Unify;;

let rec rev_assoc a l =
  match l with
    (x,y)::t -> if compare y a = 0 then x else rev_assoc a t
  | [] -> raise Not_found;;

let rec istriv env x t =
  match t with
    V y -> y = x or
              (try let t' = rev_assoc y env in istriv env x t'
               with Not_found -> false)
  | A(f,args) -> List.exists (istriv env x) args & raise Unify;;

let rec itlist2 f l1 l2 b =
  match (l1,l2) with
    ([],[]) -> b
  | (h1::t1,h2::t2) -> f h1 h2 (itlist2 f t1 t2 b)
  | _ -> failwith "itlist2";;

let rec rev_assocd a l d =
  match l with
    [] -> d
  | (x,y)::t -> if Pervasives.compare y a = 0 then x else rev_assocd a t d;;

let rec qmap f l =
  match l with
    h::t -> let h' = f h and t' = qmap f t in
            if h' == h & t' == t then l else h'::t'
  | _ -> l;;

let rec fol_subst_bump offset theta tm =
    match tm with
      V v -> let v' = v + offset in
             rev_assocd v' theta (V(v'))
    | A(f,args) ->
          let args' = qmap (fol_subst_bump offset theta) args in
          if args' == args then tm else A(f,args');;

let rec fol_unify offset tm1 tm2 sofar =
    match tm1,tm2 with
      A(f,fargs),A(g,gargs) ->
          if f <> g then raise Unify else
          itlist2 (fol_unify offset) fargs gargs sofar
    | _,V(x) ->
         (let x' = x + offset in
          try let tm2' = rev_assoc x' sofar in
              fol_unify 0 tm1 tm2' sofar
          with Not_found ->
              if istriv sofar x' tm1 then sofar
              else (tm1,x')::sofar)
    | V(x),_ ->
         (try let tm1' = rev_assoc x sofar in
              fol_unify offset tm1' tm2 sofar
          with Not_found ->
              let tm2' = fol_subst_bump offset [] tm2 in
              if istriv sofar x tm2' then sofar
              else (tm2',x)::sofar);;