Added the computation of max_weight for equations in proofs.

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

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 4414d2f435f3af14a1d8cc1d32c131bd0b241db7..ac5cb1a0ccae66e3495e267aedb339e096321a98 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -67,6 +67,7 @@ let mk_equality (weight,p,(ty,l,r,o),m) =
   let id = freshid () in
   let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
   Hashtbl.add id_to_eq id eq;
+
   eq
 ;;
 
@@ -108,6 +109,31 @@ let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
   Pervasives.compare s1 s2
 ;;
 
+let rec max_weight_in_proof current =
+  function
+   | Exact _ -> current
+   | Step (_, (_,id1,(_,id2),_)) ->
+       let eq1 = Hashtbl.find id_to_eq id1 in
+       let eq2 = Hashtbl.find id_to_eq id2 in  
+       let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in
+       let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in
+       let current = max current w1 in
+       let current = max_weight_in_proof current p1 in
+       let current = max current w2 in
+       max_weight_in_proof current p2
+
+let max_weight_in_goal_proof =
+  List.fold_left 
+    (fun current (_,_,id,_,_) ->
+       let eq = Hashtbl.find id_to_eq id in
+       let (w,p,(_,_,_,_),_,_) = open_equality eq in
+       let current = max current w in
+       max_weight_in_proof current p)
+
+let max_weight goal_proof proof =
+  let current = max_weight_in_proof 0 proof in
+  max_weight_in_goal_proof current goal_proof
+
 let proof_of_id id =
   try
     let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in