From: Matteo Selmi Date: Mon, 17 May 2004 20:58:56 +0000 (+0000) Subject: Added a filter for uris in tactic "auto". X-Git-Tag: V_0_0_9~49 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=6150b8ef905aaea17b47ff466c067054f976cd8f Added a filter for uris in tactic "auto". Uris of theorems containing, in the conclusion or in the hypothesis, constants not present in the proof (hypothesis or conclusion) are filtered out. --- diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 2aeb6fda3..36c81117f 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -4,6 +4,7 @@ REQUIRES = \ helm-cic_unification helm-mathql_interpreter helm-mathql_generator INTERFACE_FILES = \ + newConstraints.mli match_concl.mli filter_auto.mli\ proofEngineReduction.mli proofEngineHelpers.mli \ newConstraints.mli match_concl.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ diff --git a/helm/ocaml/tactics/filter_auto.ml b/helm/ocaml/tactics/filter_auto.ml new file mode 100644 index 000000000..6fae7b737 --- /dev/null +++ b/helm/ocaml/tactics/filter_auto.ml @@ -0,0 +1,65 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +let in_hypothesis = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis'" ;; + +let main_hypothesis = "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis'" ;; + +let main_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion'" ;; + +let in_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'" ;; + + +let hyp_const (conn:Mysql.dbd) uri = + (*query to obtain all the constants in the hypothesis of the theorem*) + let query = + "select h_occurrence from refObj where source='"^uri^ + "' and (h_position="^main_hypothesis^" or h_position="^in_hypothesis^ + "or h_position="^main_conclusion^" or h_position="^in_conclusion^")" in + prerr_endline ("$$$$$$$$$$$$$$$"^query); + let result = Mysql.exec conn query in + (* now we transform the result in a set *) + let f a = + match (Array.to_list a) with + [Some uri] -> uri + | _ -> assert false in + let result = Mysql.map ~f:f result in + List.fold_left + (fun set uri -> + NewConstraints.StringSet.add uri set) + NewConstraints.StringSet.empty result +;; + +(* for each uri check if its costants are a subset of + const, the set of the costants of the proof *) +let filter_new_constants (conn:Mysql.dbd) const (_,uri) = + let hyp = hyp_const conn uri in + prerr_endline (NewConstraints.pp_StringSet hyp); + NewConstraints.StringSet.subset hyp const +;; + + + diff --git a/helm/ocaml/tactics/filter_auto.mli b/helm/ocaml/tactics/filter_auto.mli new file mode 100644 index 000000000..44dfd32a9 --- /dev/null +++ b/helm/ocaml/tactics/filter_auto.mli @@ -0,0 +1,33 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + + +val filter_new_constants: + Mysql.dbd -> + NewConstraints.StringSet.t -> + int * string -> + bool + diff --git a/helm/ocaml/tactics/newConstraints.mli b/helm/ocaml/tactics/newConstraints.mli index e57d6b1e0..d81c66fb0 100644 --- a/helm/ocaml/tactics/newConstraints.mli +++ b/helm/ocaml/tactics/newConstraints.mli @@ -40,15 +40,21 @@ module SetSet : Set.S with type elt = StringSet.t val pp_SetSet : SetSet.t -> string +val pp_StringSet : StringSet.t -> string + + + val inspect_term : int -> Cic.term -> string option * SetSet.t val prefixes : int -> Cic.term -> string option * ((int * (StringSet.elt list)) list) -(* (constants_of t) returns a pair (b,n) where n is the number of +(* (constants_of t) returns a pair (b,n) where n is the set of the constants in the conclusion of t, and b is true if in MainConclusion we have an equality *) val constants_of : Cic.term -> bool * StringSet.t +val constants_concl : Cic.term -> StringSet.t + val pp_prefixes : ((int * (StringSet.elt list)) list) -> string diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index edb69bf50..d3ba1d2a3 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -131,21 +131,31 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st (fun (n,u) -> (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u)) result in + (* delete all .var uris *) let isvar (_,s) = let len = String.length s in let suffix = String.sub s (len-4) 4 in not (suffix = ".var") in let uris = List.filter isvar uris in + (* delete all not "cic:/Coq" uris *) let uris = (* TODO ristretto per ragioni di efficienza *) - prerr_endline "STO FILTRANDO2"; List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in + (* concl_cost are the costants in the conclusion of the proof + while hyp_const are the constants in the hypothesis *) + let (_,concl_const) = NewConstraints.constants_of ty in + prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris)); + let hyp t set = + match t with + Some (_,Cic.Decl t) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t)) + | Some (_,Cic.Def (t,_)) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t)) + | _ -> set in + let hyp_const = + List.fold_right hyp ey NewConstraints.StringSet.empty in + prerr_endline (NewConstraints.pp_StringSet (NewConstraints.StringSet.union hyp_const concl_const)); + (* uris with new constants in the proof are filtered *) + let uris = List.filter (Filter_auto.filter_new_constants conn (NewConstraints.StringSet.union hyp_const concl_const)) uris in (* - let uris = - (* TODO ristretto per ragioni di efficienza *) - prerr_endline "STO FILTRANDO2"; - List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris - in let uris = (* ristretto all cache *) prerr_endline "SOLO CACHE"; @@ -174,7 +184,8 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris)); filter_out uris in - uris' + prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris')); + uris' ;; (*funzione che sceglie il penultimo livello di profondita' dei must*) @@ -279,7 +290,7 @@ let searchTheorems mqi_handle (proof,goal) = else l1 - l2) subproofs in - (* now we may drop the prefix tag *) + (* now we may drop the prefix tag *) List.map snd res diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index bb5be64d8..f8c9cfa94 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -23,6 +23,34 @@ * http://cs.unibo.it/helm/. *) + +(* Da rimuovere, solo per debug*) +let print_context ctx = + let print_name = + function + Cic.Name n -> n + | Cic.Anonymous -> "_" + in + List.fold_right + (fun i (output,context) -> + let (newoutput,context') = + match i with + Some (n,Cic.Decl t) -> + print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context + | Some (n,Cic.Def (t,None)) -> + print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context + | None -> + "_ ?= _\n", None::context + | Some (_,Cic.Def (_,Some _)) -> assert false + in + output^newoutput,context' + ) ctx ("",[]) + ;; + + + + + let search_theorems_in_context status = let (proof, goal) = status in let module C = Cic in @@ -76,6 +104,7 @@ else match meta_inf with Some (ey, ty) -> prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); + prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey))); (* let time1 = Unix.gettimeofday() in let _, all_paths = NewConstraints.prefixes 5 ty in