From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 9 Jul 2009 09:31:48 +0000 (+0000)
Subject: micro optimizations to unification
X-Git-Tag: make_still_working~3719
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2f77bd6071bd316ed0a91448f4c04e638f853442;p=helm.git

micro optimizations to unification
---

diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index 83179b404..3a5c241f5 100644
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -13,6 +13,18 @@
 
 exception UnificationFailure of string Lazy.t;;
 
+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 : Terms.Blob) = struct
   module Subst = FoSubst (*.Subst(B)*)
   module U = FoUtils.Utils(B)
@@ -34,24 +46,26 @@ module Founif (B : Terms.Blob) = struct
       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