From 6643f73eb21f6736ab7c60c84def0d5d8829e0e0 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Thu, 21 Jul 2005 22:28:31 +0000 Subject: [PATCH] added some typechecks to avoid using equations with the wrong type --- helm/ocaml/paramodulation/inference.ml | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) 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 -- 2.39.2