From cb983fed69f0d209e19e22f3abcac5041f5f4a63 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Thu, 21 Jul 2005 21:37:52 +0000 Subject: [PATCH] added some typechecks to avoid using equations with the wrong type --- helm/ocaml/paramodulation/indexing.ml | 192 +++++++++++++----------- helm/ocaml/paramodulation/inference.ml | 3 +- helm/ocaml/paramodulation/saturation.ml | 4 - helm/ocaml/paramodulation/utils.ml | 5 + helm/ocaml/paramodulation/utils.mli | 2 + 5 files changed, 117 insertions(+), 89 deletions(-) diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 64a96f82a..be02d8c1b 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -1,4 +1,7 @@ +let debug_print = Utils.debug_print;; + + type retrieval_mode = Matching | Unification;; @@ -142,51 +145,61 @@ let rec find_matches metasenv context ugraph lift_amount term = let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in let names = Utils.names_of_context context in + let termty, ugraph = + CicTypeChecker.type_of_aux' metasenv context term ugraph + in function | [] -> None | candidate::tl -> let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in - let do_match c other eq_URI = - let subst', metasenv', ugraph' = - let t1 = Unix.gettimeofday () in - try - let r = - Inference.matching (metasenv @ metas) context - term (S.lift lift_amount c) ugraph in - let t2 = Unix.gettimeofday () in - match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); - r - with e -> - let t2 = Unix.gettimeofday () in - match_unif_time_no := !match_unif_time_no +. (t2 -. t1); - raise e - in + if not (fst (CicReduction.are_convertible + ~metasenv context termty ty ugraph)) then ( + debug_print ( + Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" + (CicPp.pp termty names) (CicPp.pp ty names)); + find_matches metasenv context ugraph lift_amount term tl + ) else + let do_match c other eq_URI = + let subst', metasenv', ugraph' = + let t1 = Unix.gettimeofday () in + try + let r = + Inference.matching (metasenv @ metas) context + term (S.lift lift_amount c) ugraph in + let t2 = Unix.gettimeofday () in + match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); + r + with e -> + let t2 = Unix.gettimeofday () in + match_unif_time_no := !match_unif_time_no +. (t2 -. t1); + raise e + in Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph', (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 - in - if o <> U.Incomparable then - try - do_match c other eq_URI - with e -> - find_matches metasenv context ugraph lift_amount term tl - else - let res = try do_match c other eq_URI with e -> None in - match res with - | Some (_, s, _, _, _) -> - let c' = (* M. *)apply_subst s c - and other' = (* M. *)apply_subst s other in - let order = cmp c' other' in - let names = U.names_of_context context in - if order = U.Gt then - res - else - find_matches metasenv context ugraph lift_amount term tl - | None -> + 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 + in + if o <> U.Incomparable then + try + do_match c other eq_URI + with e -> find_matches metasenv context ugraph lift_amount term tl + else + let res = try do_match c other eq_URI with e -> None in + match res with + | Some (_, s, _, _, _) -> + let c' = (* M. *)apply_subst s c + and other' = (* M. *)apply_subst s other in + let order = cmp c' other' in + let names = U.names_of_context context in + if order = U.Gt then + res + else + find_matches metasenv context ugraph lift_amount term tl + | None -> + find_matches metasenv context ugraph lift_amount term tl ;; @@ -199,58 +212,69 @@ let rec find_all_matches ?(unif_fun=Inference.unification) let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in let names = Utils.names_of_context context in + let termty, ugraph = + CicTypeChecker.type_of_aux' metasenv context term ugraph + in function | [] -> [] | candidate::tl -> let pos, (_, _, (ty, left, right, o), metas, args) = candidate in - let do_match c other eq_URI = - let subst', metasenv', ugraph' = - let t1 = Unix.gettimeofday () in + if not (fst (CicReduction.are_convertible + ~metasenv context termty ty ugraph)) then ( + debug_print ( + Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" + (CicPp.pp termty names) (CicPp.pp ty names)); + find_all_matches ~unif_fun metasenv context ugraph + lift_amount term tl + ) else + let do_match c other eq_URI = + let subst', metasenv', ugraph' = + let t1 = Unix.gettimeofday () in + try + let r = + unif_fun (metasenv @ metas) context + term (S.lift lift_amount c) ugraph in + let t2 = Unix.gettimeofday () in + match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); + r + with e -> + let t2 = Unix.gettimeofday () in + match_unif_time_no := !match_unif_time_no +. (t2 -. t1); + raise e + in + (C.Rel (1 + lift_amount), subst', metasenv', ugraph', + (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 + in + if o <> U.Incomparable then try - let r = - unif_fun (metasenv @ metas) context - term (S.lift lift_amount c) ugraph in - let t2 = Unix.gettimeofday () in - match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); - r + let res = do_match c other eq_URI in + res::(find_all_matches ~unif_fun metasenv context ugraph + lift_amount term tl) with e -> - let t2 = Unix.gettimeofday () in - match_unif_time_no := !match_unif_time_no +. (t2 -. t1); - raise e - in - (C.Rel (1 + lift_amount), subst', metasenv', ugraph', - (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 - in - if o <> U.Incomparable then - try - let res = do_match c other eq_URI in - res::(find_all_matches ~unif_fun metasenv context ugraph - lift_amount term tl) - with e -> - find_all_matches ~unif_fun metasenv context ugraph - lift_amount term tl - else - try - let res = do_match c other eq_URI in - match res with - | _, s, _, _, _ -> - let c' = (* M. *)apply_subst s c - and other' = (* M. *)apply_subst s other in - let order = cmp c' other' in - let names = U.names_of_context context in - if order <> U.Lt && order <> U.Le then - res::(find_all_matches ~unif_fun metasenv context ugraph - lift_amount term tl) - else - find_all_matches ~unif_fun metasenv context ugraph - lift_amount term tl - with e -> - find_all_matches ~unif_fun metasenv context ugraph - lift_amount term tl + find_all_matches ~unif_fun metasenv context ugraph + lift_amount term tl + else + try + let res = do_match c other eq_URI in + match res with + | _, s, _, _, _ -> + let c' = (* M. *)apply_subst s c + and other' = (* M. *)apply_subst s other in + let order = cmp c' other' in + let names = U.names_of_context context in + if order <> U.Lt && order <> U.Le then + res::(find_all_matches ~unif_fun metasenv context ugraph + lift_amount term tl) + else + find_all_matches ~unif_fun metasenv context ugraph + lift_amount term tl + with e -> + find_all_matches ~unif_fun metasenv context ugraph + lift_amount term tl ;; diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index db185b421..0ff8aeb7a 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1084,7 +1084,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"; *) ] ;; diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index ec7634d94..f56b8946f 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -5,10 +5,6 @@ open Utils;; (* set to false to disable paramodulation inside auto_tac *) let connect_to_auto = true;; -let debug = true;; - -let debug_print = if debug then prerr_endline else ignore;; - (* profiling statistics... *) let infer_time = ref 0.;; diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index d6454f202..840b3a828 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -1,3 +1,8 @@ +let debug = true;; + +let debug_print = if debug then prerr_endline else ignore;; + + let print_metasenv metasenv = String.concat "\n--------------------------\n" (List.map (fun (i, context, term) -> diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli index e69caed4d..0187f94a7 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/paramodulation/utils.mli @@ -41,3 +41,5 @@ type pos = Left | Right val string_of_pos: pos -> string val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int + +val debug_print: string -> unit -- 2.39.2