Changed the type of compute-equality_weight that now takes also

[helm.git] / helm / software / components / tactics / paramodulation / indexing.ml

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 83dc1b180126d71f4ffce95640ee6dc92adf540f..bbc60562089780ec0c0956bca1ba768e8676b71a 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -589,9 +589,10 @@ let rec demodulation_equality ?from newmeta env table sign target =
   (* first, we simplify *)
   let right = U.guarded_simpl context right in
   let left = U.guarded_simpl context left in
-  let w = Utils.compute_equality_weight eq_ty left right in
   let order = !Utils.compare_terms left right in
-  let target = w, proof, (eq_ty, left, right, order), metas, args in
+  let stat = (eq_ty, left, right, order) in 
+  let w = Utils.compute_equality_weight stat in
+  let target = w, proof, stat, metas, args in
   if Utils.debug_metas then 
     ignore(check_target context target "demod equalities input");
   let metasenv' = (* metasenv @ *) metas in
@@ -691,11 +692,12 @@ let rec demodulation_equality ?from newmeta env table sign target =
     in
     let left, right = if is_left then newterm, right else left, newterm in
     let ordering = !Utils.compare_terms left right in
+    let stat = (eq_ty, left, right, ordering) in
     let time2 = Unix.gettimeofday () in
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
     let res =
-      let w = Utils.compute_equality_weight eq_ty left right in
-      (w, newproof, (eq_ty, left, right, ordering),newmenv,args) in
+      let w = Utils.compute_equality_weight stat in
+      (w, newproof, stat,newmenv,args) in
     if Utils.debug_metas then 
       ignore(check_target context res "buildnew_target output");
     !maxmeta, res 
@@ -945,12 +947,13 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
     let left, right =
       if ordering = U.Gt then newgoal, right else left, newgoal in
     let neworder = !Utils.compare_terms left right in
+    let stat = (eq_ty, left, right, neworder) in
     let newmenv = (* Inference.filter s *) menv in  
     let time2 = Unix.gettimeofday () in
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 
-    let w = Utils.compute_equality_weight eq_ty left right in
-    (w, newproof, (eq_ty, left, right, neworder), newmenv, []) 
+    let w = Utils.compute_equality_weight stat in
+    (w, newproof, stat, newmenv, []) 
 
   in
   !maxmeta, List.map build_new expansions
@@ -1028,9 +1031,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       let neworder = !Utils.compare_terms left right in
       let newmenv = (* Inference.filter s *) m in
       let newargs = args @ args' in
+      let stat = (eq_ty, left, right, neworder) in
       let eq' =
-        let w = Utils.compute_equality_weight eq_ty left right in
-        (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
+        let w = Utils.compute_equality_weight stat in
+        (w, newproof, stat, newmenv, newargs) in
       if Utils.debug_metas then 
        ignore (check_target context eq' "buildnew3");
       let newm, eq' = Inference.fix_metas !maxmeta eq' in