fix

[helm.git] / components / tactics / paramodulation / utils.ml

diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index 84de8800e7c8de566ff7e93cd0d7bec23c0fea9d..8fb1d42bcf60bf6adae07c5ae7826995632f245e 100644 (file)
--- a/components/tactics/paramodulation/utils.ml
+++ b/components/tactics/paramodulation/utils.ml
@@ -292,20 +292,44 @@ end
 
 module IntSet = Set.Make(OrderedInt)
 
-let compute_equality_weight ty left right =
+let compute_equality_weight (ty,left,right,o) =
+  let factor = 1 in
+  match o with
+    | Lt -> 
+       let w, m = (weight_of_term 
+              ~consider_metas:true ~count_metas_occurrences:false right) in
+         w + (factor * (List.length m)) ;
+    | Le -> assert false
+    | Gt -> 
+       let w, m = (weight_of_term 
+              ~consider_metas:true ~count_metas_occurrences:false left) in
+         w + (factor * (List.length m)) ;
+  | Ge -> assert false
+  | Eq 
+  | Incomparable -> 
+      let w1, m1 = (weight_of_term 
+              ~consider_metas:true ~count_metas_occurrences:false right) in
+      let w2, m2 = (weight_of_term 
+              ~consider_metas:true ~count_metas_occurrences:false left) in
+      w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
+;;
+
+(* old
+let compute_equality_weight (ty,left,right,o) =
   let metasw = ref 0 in
   let weight_of t =
     let w, m = (weight_of_term 
                  ~consider_metas:true ~count_metas_occurrences:false t) in
-    metasw := !metasw + (2 * (List.length m)) ;
+    metasw := !metasw + (1 * (List.length m)) ;
     w
   in
   (* Warning: the following let cannot be expanded since it forces the
      right evaluation order!!!! *)
-  let w = (weight_of ty) + (weight_of left) + (weight_of right) in
+  let w = (weight_of ty) + (weight_of left) + (weight_of right) in 
+  (* let w = weight_of (Cic.Appl [ty;left;right]) in *)
   w + !metasw
 ;;
-
+*)
 
 (* returns a "normalized" version of the polynomial weight wl (with type
  * weight list), i.e. a list sorted ascending by meta number,