From: Alberto Griggio <griggio@fbk.eu>
Date: Thu, 21 Jul 2005 22:28:31 +0000 (+0000)
Subject: added some typechecks to avoid using equations with the wrong type
X-Git-Tag: V_0_7_2~112
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6643f73eb21f6736ab7c60c84def0d5d8829e0e0;p=helm.git

added some typechecks to avoid using equations with the wrong type
---

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 0ff8aeb7a..dfdbab614 100644
--- 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
@@ -1112,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 ->
@@ -1128,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