X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoUnif.ml;h=0946873b9af5c11fea237022b2394a40393e3de6;hb=86a273d0b145e058baf50b6e97fcb0dc0adc90e3;hp=6eb014062f81451292249ac8382e8272da65cc58;hpb=8de1a75899a83dd31e856804bd448c1bd87d9ab3;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index 6eb014062..0946873b9 100644
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -13,46 +13,59 @@
 
 exception UnificationFailure of string Lazy.t;;
 
-module Founif (B : Terms.Blob) = struct
-  module Subst = FoSubst (*.Subst(B)*)
+let mem2 a b l =
+  let rec aux found_a found_b = function
+    | x :: tl ->
+       let found_a = found_a || x = a in
+       let found_b = found_b || x = b in
+       if found_a && found_b then true, true
+       else aux found_a found_b tl
+    | [] -> found_a, found_b
+  in
+   aux false false l
+;;
+
+module Founif (B : Orderings.Blob) = struct
+  module Subst = FoSubst 
   module U = FoUtils.Utils(B)
 
-  let unification vars locked_vars t1 t2 =
-    let lookup = Subst.lookup_subst in
+  let unification (* vars *) locked_vars t1 t2 =
     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
       | 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 t s
-      | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
-          unif subst t s
+      | Terms.Var i, Terms.Var j ->
+          (* TODO: look in locked vars for both i and j at once *)
+          let i_locked, j_locked = mem2 i j locked_vars in
+          if i_locked then
+            if j_locked then
+              raise (UnificationFailure (lazy "Inference.unification.unif"))
+            else
+              Subst.build_subst j s subst
+          else
+            Subst.build_subst i t subst
       | Terms.Var i, t when occurs_check subst i t ->
-          raise
-            (UnificationFailure (lazy "Inference.unification.unif"))
+          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.build_subst i t subst in
-          subst
-      | _, Terms.Var _ -> unif subst t s
+          raise (UnificationFailure (lazy "Inference.unification.unif"))
+      | Terms.Var i, t -> Subst.build_subst i t subst
+      | t, Terms.Var i when occurs_check subst i t ->
+          raise (UnificationFailure (lazy "Inference.unification.unif"))
+      | t, Terms.Var i when (List.mem i locked_vars) -> 
+          raise (UnificationFailure (lazy "Inference.unification.unif"))
+      | t, Terms.Var i -> Subst.build_subst i t subst
       | Terms.Node l1, Terms.Node l2 -> (
           try
             List.fold_left2
@@ -65,7 +78,35 @@ module Founif (B : Terms.Blob) = struct
           raise (UnificationFailure (lazy "Inference.unification.unif"))
     in
     let subst = unif Subst.id_subst t1 t2 in
-    let vars = Subst.filter subst vars in
-    subst, vars
-  
+    subst
+;;
+
+(* Sets of variables in s and t are assumed to be disjoint  *)
+  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