Implemented check for duplicates (in goals)

[helm.git] / helm / software / components / ng_paramodulation / foUnif.ml

diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index 6eb014062f81451292249ac8382e8272da65cc58..83179b4045592ba149a849bbe0b513e61b8b963c 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -18,19 +18,18 @@ module Founif (B : Terms.Blob) = struct
   module U = FoUtils.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 i ->
-          let t = lookup i subst in
+          let t = Subst.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 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
+      let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
+      and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t
       
       in
       match s, t with
@@ -67,5 +66,32 @@ module Founif (B : Terms.Blob) = struct
     let subst = unif Subst.id_subst t1 t2 in
     let vars = Subst.filter subst vars in
     subst, vars
-  
+;;
+
+  let alpha_eq s t =
+    let rec equiv subst s t =
+      let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
+      and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t
+       
+      in
+      match s, t with
+       | s, t when U.eq_foterm s t -> subst
+       | Terms.Var i, Terms.Var j
+           when (not (List.exists (fun (_,k) -> k=t) subst)) ->
+            let subst = Subst.build_subst i t subst in
+              subst
+       | Terms.Node l1, Terms.Node l2 -> (
+            try
+              List.fold_left2
+               (fun subst' s t -> equiv subst' s t)
+               subst l1 l2
+            with Invalid_argument _ ->
+              raise (UnificationFailure (lazy "Inference.unification.unif"))
+          )
+       | _, _ ->
+            raise (UnificationFailure (lazy "Inference.unification.unif"))
+    in
+      equiv Subst.id_subst s t
+;;
+
 end