upgraded code to work with non-default equalities

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

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index e30d4403490cd01fce5fe4050141656bef3a48f4..a7b2c30399d20ab40016827e1419fe4bbc4a8b5d 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -228,8 +228,8 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
                   (candidate, eq_URI))
           in
           let c, other, eq_URI =
-            if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
-            else right, left, HL.Logic.eq_ind_r_URI
+            if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
+            else right, left, Utils.eq_ind_r_URI ()
           in
           if o <> U.Incomparable then
             try
@@ -317,8 +317,8 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
              (candidate, eq_URI))
           in
           let c, other, eq_URI =
-            if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
-            else right, left, HL.Logic.eq_ind_r_URI
+            if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
+            else right, left, Utils.eq_ind_r_URI ()
           in
           if o <> U.Incomparable then
             try
@@ -507,16 +507,6 @@ let rec demodulation_aux metasenv context ugraph table lift_amount term =
 ;;
 
 
-let build_ens_for_sym_eq ty x y = 
-  [(UriManager.uri_of_string
-      "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty);
-   (UriManager.uri_of_string
-      "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x);
-   (UriManager.uri_of_string
-      "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)]
-;;
-
-
 let build_newtarget_time = ref 0.;;
 
 
@@ -555,7 +545,7 @@ let rec demodulation_equality newmeta env table sign target =
       incr demod_counter;
       let bo' =
         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
-        C.Appl [C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
+        C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
                 S.lift 1 eq_ty; l; r]
       in
       if sign = Utils.Positive then
@@ -574,13 +564,16 @@ let rec demodulation_equality newmeta env table sign target =
 (*         let target' = *)
           let eq_found =
             let proof' =
-              let ens =
-                if pos = Utils.Left then
-                  build_ens_for_sym_eq ty what other
-                else
-                  build_ens_for_sym_eq ty other what
+(*               let ens = *)
+(*                 if pos = Utils.Left then *)
+(*                   build_ens_for_sym_eq ty what other *)
+(*                 else *)
+(*                   build_ens_for_sym_eq ty other what *)
+              let termlist =
+                if pos = Utils.Left then [ty; what; other]
+                else [ty; other; what]
               in
-              Inference.ProofSymBlock (ens, proof')
+              Inference.ProofSymBlock (termlist, proof')
             in
             let what, other =
               if pos = Utils.Left then what, other else other, what
@@ -606,7 +599,7 @@ let rec demodulation_equality newmeta env table sign target =
 (*         in *)
         let refl =
           C.Appl [C.MutConstruct (* reflexivity *)
-                    (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
+                    (LibraryObjects.eq_URI (), 0, 1, []);
                   eq_ty; if is_left then right else left]          
         in
         (bo,
@@ -828,7 +821,8 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
       let bo'' = 
         let l, r =
           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
-        C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty; l; r]
+        C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+                S.lift 1 eq_ty; l; r]
       in
       incr maxmeta;
       let metaproof =
@@ -839,13 +833,17 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
 (*       let target' = *)
         let eq_found =
           let proof' =
-            let ens =
-              if pos = Utils.Left then
-                build_ens_for_sym_eq ty what other
-              else
-                build_ens_for_sym_eq ty other what
+(*             let ens = *)
+(*               if pos = Utils.Left then *)
+(*                 build_ens_for_sym_eq ty what other *)
+(*               else *)
+(*                 build_ens_for_sym_eq ty other what *)
+(*             in *)
+            let termlist =
+              if pos = Utils.Left then [ty; what; other]
+              else [ty; other; what]
             in
-            Inference.ProofSymBlock (ens, proof')
+            Inference.ProofSymBlock (termlist, proof')
           in
           let what, other =
             if pos = Utils.Left then what, other else other, what
@@ -870,7 +868,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
 (*       in *)
       let refl =
         C.Appl [C.MutConstruct (* reflexivity *)
-                  (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
+                  (LibraryObjects.eq_URI (), 0, 1, []);
                 eq_ty; if ordering = U.Gt then right else left]
       in
       (bo',
@@ -940,7 +938,8 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       let bo'' =
         let l, r =
           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
-        C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty; l; r]
+        C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+                S.lift 1 eq_ty; l; r]
       in
       bo',
       Inference.ProofBlock (
@@ -1029,11 +1028,15 @@ let rec demodulation_goal newmeta env table goal =
       in
       let eq_found =
         let proof' =
-          let ens =
-            if pos = Utils.Left then build_ens_for_sym_eq ty what other
-            else build_ens_for_sym_eq ty other what
+(*           let ens = *)
+(*             if pos = Utils.Left then build_ens_for_sym_eq ty what other *)
+(*             else build_ens_for_sym_eq ty other what *)
+(*           in *)
+          let termlist =
+            if pos = Utils.Left then [ty; what; other]
+            else [ty; other; what]
           in
-          Inference.ProofSymBlock (ens, proof')
+          Inference.ProofSymBlock (termlist, proof')
         in
         let what, other =
           if pos = Utils.Left then what, other else other, what