fixed bug in proof generation, new weight function to sort equalities, which

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

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 877e5929a552b3822c866d30a745aabac0d9e2d7..c933aec0b48c3c11115d8d8346302f1144c93892 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -44,7 +44,7 @@ let symbols_of_equality (_, (_, left, right), _, _) =
 ;;
 *)
 
-let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
+let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
   let m1 = symbols_of_term left in
   let m = 
     TermMap.fold
@@ -71,8 +71,8 @@ module OrderedEquality = struct
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
     | false ->
-        let w1, (ty, left, right, _), _, a = eq1
-        and w2, (ty', left', right', _), _, a' = eq2 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 *)
@@ -414,7 +414,7 @@ let contains_empty env (negative, positive) =
   try
     let found =
       List.find
-        (fun (proof, (ty, left, right, ordering), m, a) ->
+        (fun (w, proof, (ty, left, right, ordering), m, a) ->
            fst (CicReduction.are_convertible context left right ugraph))
         negative
     in
@@ -459,7 +459,7 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
     maxmeta := newmeta;
     if is_identity env newcurrent then
       if sign = Negative then Some (sign, newcurrent)
-      else (Inference.delete_proof newcurrent; None)
+      else None
     else
       Some (sign, newcurrent)
   in
@@ -483,13 +483,12 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
       if ok then res else None
   | Some (Positive, c) ->
       if Indexing.in_index active_table c then
-        (Inference.delete_proof c; None)
+        None
       else
         match passive_table with
         | None -> res
         | Some passive_table ->
-            if Indexing.in_index passive_table c then
-              (Inference.delete_proof c; None)
+            if Indexing.in_index passive_table c then None
             else res
 
 (*   | Some (s, c) -> if find_duplicate s c all then None else res *)
@@ -572,12 +571,9 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
     List.fold_left
       (fun s e ->
          if not (Inference.is_identity env e) then
-           if EqualitySet.mem e s then
-             (Inference.delete_proof e; s)
-           else
-             EqualitySet.add e s
-         else
-           (Inference.delete_proof e; s))
+           if EqualitySet.mem e s then s
+           else EqualitySet.add e s
+         else s)
       EqualitySet.empty new_pos
   in
   let new_pos = EqualitySet.elements new_pos_set in
@@ -609,16 +605,11 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   let is_duplicate =
     match passive_table with
     | None ->
-        (fun e ->
-           let ok = not (Indexing.in_index active_table e) in
-           if not ok then Inference.delete_proof e;
-           ok)
+        (fun e -> not (Indexing.in_index active_table e))
     | Some passive_table ->
         (fun e ->
-           let ok = not ((Indexing.in_index active_table e) ||
-                           (Indexing.in_index passive_table e)) in
-           if not ok then Inference.delete_proof e;
-           ok)
+           not ((Indexing.in_index active_table e) ||
+                  (Indexing.in_index passive_table e)))
   in
   new_neg, List.filter is_duplicate new_pos
 
@@ -655,7 +646,6 @@ let backward_simplify_active env new_pos new_table active =
          if List.mem (s, eq) res then
            res, tbl
          else if (is_identity env eq) || (find eq res) then (
-           Inference.delete_proof eq;
            res, tbl
          ) (* else if (find eq res) then *)
 (*            res, tbl *)
@@ -665,7 +655,6 @@ let backward_simplify_active env new_pos new_table active =
     List.fold_right
       (fun (s, eq) (n, p) ->
          if (s <> Negative) && (is_identity env eq) then (
-           Inference.delete_proof eq;
            (n, p)
          ) else
            if s = Negative then eq::n, p
@@ -1017,7 +1006,7 @@ let main () =
   let env = (metasenv, context, ugraph) in
   try
     let term_equality = equality_of_term meta_proof goal in
-    let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
+    let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
     let active = make_active () in
     let passive = make_passive [term_equality] equalities in
     Printf.printf "\ncurrent goal: %s\n"