added some typechecks to avoid using equations with the wrong type

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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index db185b421b040e5a1f8cbb63677c399b43114c7e..dfdbab6141effb9355ab848f32229766ab63e09f 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1023,6 +1023,9 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
+  let ok_types ty menv =
+    List.for_all (fun (_, _, mt) -> mt = ty) menv
+  in
   let rec aux index newmeta = function
     | [] -> [], newmeta
     | (Some (_, C.Decl (term)))::tl ->
@@ -1042,8 +1045,15 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
               in (
                 match head with
                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-                    when UriManager.eq uri eq_uri ->
-                    Printf.printf "OK: %s\n" (CicPp.ppterm term);
+                    when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
+                    debug_print (
+                      Printf.sprintf "OK: %s" (CicPp.ppterm term));
+(*                     debug_print ( *)
+(*                       Printf.sprintf "args: %s\n" *)
+(*                         (String.concat ", " (List.map CicPp.ppterm args))); *)
+(*                     debug_print ( *)
+(*                       Printf.sprintf "newmetas:\n%s\n" *)
+(*                         (print_metasenv newmetas)); *)
                     let o = !Utils.compare_terms t1 t2 in
                     let w = compute_equality_weight ty t1 t2 in
                     let proof = BasicProof p in
@@ -1084,7 +1094,8 @@ let equations_blacklist =
       "cic:/Coq/Init/Logic/f_equal.con";
       "cic:/Coq/Init/Logic/f_equal2.con";
       "cic:/Coq/Init/Logic/f_equal3.con";
-      "cic:/Coq/Init/Logic/sym_eq.con"
+      "cic:/Coq/Init/Logic/sym_eq.con";
+(*       "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *)
     ]
 ;;
 
@@ -1111,6 +1122,9 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
   let iseq uri =
     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
   in
+  let ok_types ty menv =
+    List.for_all (fun (_, _, mt) -> mt = ty) menv
+  in
   let rec aux newmeta = function
     | [] -> [], newmeta
     | (term, termty)::tl ->
@@ -1127,8 +1141,10 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
                   C.Appl (term::args)
               in (
                 match head with
-                | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
-                    Printf.printf "OK: %s\n" (CicPp.ppterm term);
+                | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+                    when (iseq uri) && (ok_types ty newmetas) ->
+                    debug_print (
+                      Printf.sprintf "OK: %s" (CicPp.ppterm term));
                     let o = !Utils.compare_terms t1 t2 in
                     let w = compute_equality_weight ty t1 t2 in
                     let proof = BasicProof p in