removed first Cic.term from type equality, added an int (weight of the equality)

[helm.git] / helm / ocaml / paramodulation / saturation.ml

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 793e48423b1d999d97a342fa8affe2048d2f3399..877e5929a552b3822c866d30a745aabac0d9e2d7 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -64,17 +64,6 @@ let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
 ;;
 
 
-let weight_of_equality (_, (ty, left, right, _), _, _) =
-  let meta_number = ref 0 in
-  let weight_of t =
-    let weight, ml =  weight_of_term t in
-    meta_number := !meta_number + (List.fold_left (fun r (_, n) -> r+n) 0 ml);
-    weight
-  in
-  (weight_of ty) + (weight_of left) + (weight_of right), meta_number
-;;
-
-
 module OrderedEquality = struct
   type t = Inference.equality
 
@@ -82,17 +71,25 @@ module OrderedEquality = struct
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
     | false ->
-        let _, (ty, left, right, _), _, _ = eq1
-        and _, (ty', left', right', _), _, _ = eq2 in
-(*         let w1, m1 = weight_of_equality eq1 *)
-(*         and w2, m2 = weight_of_equality eq2 in        *)
-        let weight_of t = fst (weight_of_term ~consider_metas:false t) in
-        let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
-        and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
+        let w1, (ty, left, right, _), _, a = eq1
+        and w2, (ty', left', right', _), _, a' = eq2 in
+(*         let weight_of t = fst (weight_of_term ~consider_metas:false t) in *)
+(*         let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *)
+(*         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *)
         match Pervasives.compare w1 w2 with
-        | 0 -> Pervasives.compare eq1 eq2
-(*             let res = Pervasives.compare m1 m2 in *)
-(*             if res = 0 then Pervasives.compare eq1 eq2 else res *)
+        | 0 ->
+            let res = (List.length a) - (List.length a') in
+            if res <> 0 then res else (
+              try
+                let res = Pervasives.compare (List.hd a) (List.hd a') in
+                if res <> 0 then res else Pervasives.compare eq1 eq2
+              with _ -> Pervasives.compare eq1 eq2
+(*               match a, a' with *)
+(*               | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
+(*                   let res = Pervasives.compare i j in *)
+(*                   if res <> 0 then res else Pervasives.compare eq1 eq2 *)
+(*               | _, _ -> Pervasives.compare eq1 eq2 *)
+            )
         | res -> res
 end