X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Ffounif.ml;h=bcea59ad57c02acde74bbef56614c3a0d623a041;hb=b97a7976503b2d2e5cbc9199f848135a324775a8;hp=bc18aaf00f3248dc715df19ff72d2b680b791e81;hpb=6c4056ea40b96039f24eeda9a1e1900c95bad7c8;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/founif.ml b/helm/software/components/ng_paramodulation/founif.ml
index bc18aaf00..bcea59ad5 100644
--- a/helm/software/components/ng_paramodulation/founif.ml
+++ b/helm/software/components/ng_paramodulation/founif.ml
@@ -14,34 +14,35 @@
 exception UnificationFailure of string Lazy.t;;
 
 module Founif (B : Terms.Blob) = struct
-  module Subst = Subst.Subst(B)
+  module Subst = Fosubst.Subst(B)
+  module U = Terms.Utils(B)
 
   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.Var i ->
+          let t = lookup i subst in
+          if not (U.eq_foterm 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
+    let rec unif subst s t =
+      let s = match s with Terms.Var i -> lookup i subst | _ -> s
+      and t = match t with Terms.Var i -> lookup i subst | _ -> t
       
       in
       match s, t with
-      | s, t when s = t -> subst, vars
+      | s, t when U.eq_foterm s t -> subst
       | 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
+          unif subst t s
       | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
-          unif subst vars t s
+          unif subst t s
       | Terms.Var i, t when occurs_check subst i t ->
           raise
             (UnificationFailure (lazy "Inference.unification.unif"))
@@ -49,23 +50,21 @@ module Founif (B : Terms.Blob) = struct
           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) -> (
+          let subst = Subst.build_subst i t subst in
+          subst
+      | _, Terms.Var _ -> unif subst t s
+      | Terms.Node l1, Terms.Node l2 -> (
           try
             List.fold_left2
-              (fun (subst', vars) s t -> unif subst' vars s t)
-              (subst, vars) tls tlt
+              (fun subst' s t -> unif subst' s t)
+              subst l1 l2
           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 subst = unif Subst.id_subst t1 t2 in
     let vars = Subst.filter subst vars in
     subst, vars