Reorganized foUtils, added Clauses module to avoid duplicate code around are_invertib...

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

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 47f6b4512cb33c452653221d258690d9b08b9087..89b390b07a11d3a9c4fc2f4f4f605c0eace95eac 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -186,58 +186,25 @@ let compare_terms o x y =
       | _ -> assert false
 ;;
 
+let are_invertible relocate alpha_eq l r =
+    let varlist = Terms.vars_of_term l in
+    let maxvar = List.fold_left max 0 varlist in
+    let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
+    let l = FoSubst.apply_subst subst l in
+      try (ignore(alpha_eq l r);true) with
+         FoUnif.UnificationFailure _ -> false;;
+
 module NRKBO (B : Terms.Blob) = struct
   let name = "nrkbo"
   include B 
 
   module Pp = Pp.Pp(B)
+  module Unif = FoUnif.FoUnif(B)
+  module Utils = FoUtils.Utils(B)
 
   let eq_foterm = eq_foterm B.eq;;
 
-exception UnificationFailure of string Lazy.t;;
-
-
-(* DUPLICATE CODE FOR TESTS (see FoUnif)  *)
-  let alpha_eq s t =
-    let rec equiv subst s t =
-      let s = match s with Terms.Var i -> FoSubst.lookup i subst | _ -> s
-      and t = match t with Terms.Var i -> FoSubst.lookup i subst | _ -> t
-        
-      in
-      match s, t with
-        | s, t when eq_foterm s t -> subst
-        | Terms.Var i, Terms.Var j
-            when (not (List.exists (fun (_,k) -> k=t) subst)) ->
-            let subst = FoSubst.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 FoSubst.id_subst s t
-;;
-
-let relocate maxvar varlist subst =
-    List.fold_right
-      (fun i (maxvar, varlist, s) -> 
-         maxvar+1, maxvar::varlist, FoSubst.build_subst i (Terms.Var maxvar) s)
-      varlist (maxvar+1, [], subst)
-  ;;
-
-  let are_invertible l r =
-    let varlist = Terms.vars_of_term l in
-    let maxvar = List.fold_left max 0 varlist in
-    let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
-    let l = FoSubst.apply_subst subst l in
-      try (ignore(alpha_eq l r);true) with
-         UnificationFailure _ -> false
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
 
   let compute_clause_weight = compute_clause_weight;;
   
@@ -270,9 +237,13 @@ module KBO (B : Terms.Blob) = struct
   include B 
 
   module Pp = Pp.Pp(B)
+  module Unif = FoUnif.FoUnif(B)
+  module Utils = FoUtils.Utils(B)
 
   let eq_foterm = eq_foterm B.eq;;
 
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
   let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
 
@@ -336,9 +307,13 @@ module LPO (B : Terms.Blob) = struct
   include B 
 
   module Pp = Pp.Pp(B)
+  module Unif = FoUnif.FoUnif(B)
+  module Utils = FoUtils.Utils(B)
 
   let eq_foterm = eq_foterm B.eq;;
 
+  let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
   let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;