(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)

exception UnificationFailure of string Lazy.t;;

let unification vars locked_vars t1 t2 =
  let lookup = Subst.lookup_subst in
  let rec occurs_check subst what where =
    match where with
    | Terms.Var i when i = what -> true
    | Terms.Var _ ->
        let t = lookup where subst in
        if t <> where then occurs_check subst what t else false
    | Terms.Node l -> List.exists (occurs_check subst what) l
    | _ -> false
  in
  let rec unif subst vars s t =
    let s = match s with Terms.Var _ -> lookup s subst | _ -> s
    and t = match t with Terms.Var _ -> lookup t subst | _ -> t
    
    in
    match s, t with
    | s, t when s = t -> subst, vars
    | Terms.Var i, Terms.Var j
        when (List.mem i locked_vars) &&(List.mem j locked_vars) ->
        raise
          (UnificationFailure (lazy "Inference.unification.unif"))
    | Terms.Var i, Terms.Var j when (List.mem i locked_vars) ->
        unif subst vars t s
    | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
        unif subst vars t s
    | Terms.Var i, t when occurs_check subst i t ->
        raise
          (UnificationFailure (lazy "Inference.unification.unif"))
    | Terms.Var i, t when (List.mem i locked_vars) -> 
        raise
          (UnificationFailure (lazy "Inference.unification.unif"))
    | Terms.Var i, t ->
        let subst = Subst.buildsubst i t subst in
        subst, vars
    | _, Terms.Var _ -> unif subst vars t s
    | Terms.Node (hds::_), Terms.Node (hdt::_) when hds <> hdt ->
        raise (UnificationFailure (lazy "Inference.unification.unif"))
    | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> (
        try
          List.fold_left2
            (fun (subst', vars) s t -> unif subst' vars s t)
            (subst, vars) tls tlt
        with Invalid_argument _ ->
          raise (UnificationFailure (lazy "Inference.unification.unif"))
      )
    | _, _ ->
        raise (UnificationFailure (lazy "Inference.unification.unif"))
  in
  let subst, vars = unif Subst.empty_subst vars t1 t2 in
  let vars = Subst.filter subst vars in
  subst, vars