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

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

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 5a8960101d21c2a513b4acc18223817c1aad27c7..c50d809acbd3d4c4bb6515bdedb9d4b07fc000f1 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -399,7 +399,7 @@ let rec demodulation newmeta env table target =
       in
       let t' = C.Lambda (C.Anonymous, ty, bo'') in
       bo,
-      C.Implicit None
+      Inference.ProofBlock (subst, eq_URI, t', eq_found, target)
 (*       (\* M. *\)apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
 (*                                    proof; other; proof']) *)
     in
@@ -417,8 +417,13 @@ let rec demodulation newmeta env table target =
 
     let time2 = Unix.gettimeofday () in
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-    
-    newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
+
+    let res =
+      let w = Utils.compute_equality_weight eq_ty left right in
+      (w, (eq_ty, left, right, ordering), newmetasenv, newargs)
+    in
+    Inference.store_proof res newproof;
+    newmeta, res
   in
 (*   let build_newtarget = *)
 (*     let profile = CicUtil.profile "Indexing.demodulation.build_newtarget" in *)
@@ -586,7 +591,7 @@ let superposition_left (metasenv, context, ugraph) table target =
       in
       let t' = C.Lambda (C.Anonymous, ty, bo'') in
       bo',
-      C.Implicit None
+      Inference.ProofBlock (s, eq_URI, t', eq_found, target)
 (*       (\* M. *\)apply_subst s *)
 (*         (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
 (*                  proof; other; proof']) *)
@@ -597,8 +602,13 @@ let superposition_left (metasenv, context, ugraph) table target =
 
     let time2 = Unix.gettimeofday () in
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-    
-    (newproof, (eq_ty, left, right, neworder), [], [])
+
+    let res =
+      let w = Utils.compute_equality_weight eq_ty left right in
+      (w, (eq_ty, left, right, neworder), [], [])
+    in
+    Inference.store_proof res newproof;
+    res
   in
 (*   let build_new = *)
 (*     let profile = CicUtil.profile "Inference.superposition_left.build_new" in *)
@@ -649,7 +659,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       in
       let t' = C.Lambda (C.Anonymous, ty, bo'') in
       bo',
-      C.Implicit None
+      Inference.ProofBlock (s, eq_URI, t', eq_found, target)
 (*       (\* M. *\)apply_subst s *)
 (*         (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
 (*                  eqproof; other; proof']) *)
@@ -661,7 +671,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       let neworder = !Utils.compare_terms left right 
       and newmenv = newmetas @ menv'
       and newargs = args @ args' in
-      let eq' = (newproof, (eq_ty, left, right, neworder), newmenv, newargs)
+      let eq' =
+        let w = Utils.compute_equality_weight eq_ty left right in
+        (w, (eq_ty, left, right, neworder), newmenv, newargs)
       and env = (metasenv, context, ugraph) in
       let newm, eq' = Inference.fix_metas !maxmeta eq' in
       newm, eq'
@@ -670,7 +682,8 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
 
     let time2 = Unix.gettimeofday () in
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-    
+
+    Inference.store_proof newequality newproof;
     newequality
   in