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

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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 163fabddbac6ebf6e04eaac05363615b9839ac02..f5233d03dbab9e907e5c02711729023019b32afa 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -2,7 +2,7 @@ open Utils;;
 
 
 type equality =
-    Cic.term  *          (* proof *)
+    int  *               (* weight *)
     (Cic.term *          (* type *)
      Cic.term *          (* left side *)
      Cic.term *          (* right side *)
@@ -1026,7 +1026,8 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
                     Printf.printf "OK: %s\n" (CicPp.ppterm term);
                     let o = !Utils.compare_terms t1 t2 in
-                    let e = (p, (ty, t1, t2, o), newmetas, args) in
+                    let w = compute_equality_weight ty t1 t2 in
+                    let e = (w, (ty, t1, t2, o), newmetas, args) in
                     store_proof e (BasicProof p);
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
@@ -1035,7 +1036,8 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
               let t1 = S.lift index t1
               and t2 = S.lift index t2 in
               let o = !Utils.compare_terms t1 t2 in
-              let e = (C.Rel index, (ty, t1, t2, o), [], []) in
+              let w = compute_equality_weight ty t1 t2 in
+              let e = (w, (ty, t1, t2, o), [], []) in
               store_proof e (BasicProof (C.Rel index));
               Some e, (newmeta+1)
           | _ -> None, newmeta
@@ -1054,7 +1056,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 ;;
 
 
-let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) =
+let fix_metas newmeta ((weight, (ty, left, right, o), menv, args) as equality) =
   let table = Hashtbl.create (List.length args) in
   let newargs, _ =
     List.fold_right
@@ -1090,7 +1092,7 @@ let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) =
       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
   in
   (newmeta + (List.length newargs) + 1,
-   (repl proof, (ty, left, right, o), menv', newargs))
+   (weight, (ty, left, right, o), menv', newargs))
 ;;
 
 
@@ -1099,7 +1101,8 @@ exception TermIsNotAnEquality;;
 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
       let o = !Utils.compare_terms t1 t2 in
-      let e = (proof, (ty, t1, t2, o), [], []) in
+      let w = compute_equality_weight ty t1 t2 in
+      let e = (w, (ty, t1, t2, o), [], []) in
       store_proof e (BasicProof proof);
       e
 (*       (proof, (ty, t1, t2, o), [], []) *)
@@ -1111,6 +1114,7 @@ let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 
 
+(*
 let superposition_left (metasenv, context, ugraph) target source =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -1312,6 +1316,7 @@ let superposition_right newmeta (metasenv, context, ugraph) target source =
     (!maxmeta,
      (List.filter ok (new1 @ new2 @ new3 @ new4)))
 ;;
+*)
 
 
 let is_identity ((_, context, ugraph) as env) = function
@@ -1328,6 +1333,7 @@ let is_identity ((_, context, ugraph) as env) = function
 ;;
 
 
+(*
 let demodulation newmeta (metasenv, context, ugraph) target source =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -1525,6 +1531,7 @@ let subsumption env target source =
     );
     res
 ;;
+*)
 
 
 let extract_differing_subterms t1 t2 =