# HG changeset patch # User kleing # Date 1116228905 -7200 # Node ID f2074e12d1d4d9908e03d07efa14923874e44ba7 # Parent 5b70f789e07909aa1608f03a8673d7d72677c2c8 searching for thms by combination of criteria (intro, elim, dest, name, term pattern) diff -r 5b70f789e079 -r f2074e12d1d4 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Mon May 16 09:34:20 2005 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Mon May 16 09:35:05 2005 +0200 @@ -56,7 +56,7 @@ val print_trans_rules: Toplevel.transition -> Toplevel.transition val print_methods: Toplevel.transition -> Toplevel.transition val print_antiquotations: Toplevel.transition -> Toplevel.transition - val print_thms_containing: int option * string list + val print_thms_containing: int option * (bool * ProofContext.search_criterion) list -> Toplevel.transition -> Toplevel.transition val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition val print_binds: Toplevel.transition -> Toplevel.transition @@ -244,9 +244,22 @@ val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations; -fun print_thms_containing (lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state => - ProofContext.print_thms_containing - (Toplevel.node_case ProofContext.init Proof.context_of state) lim spec); +fun print_thms_containing (lim, spec) = Toplevel.unknown_theory o +Toplevel.keep (fn state => + let + fun get_goal () = + let val (_, (_, st)) = Proof.get_goal (Toplevel.proof_of state); + in prop_of st end; + + (* searching is permitted without a goal. + I am not sure whether the only exception that I should catch is UNDEF *) + val goal = SOME (get_goal ()) handle Toplevel.UNDEF => NONE; + + val ctxt = (Toplevel.node_case ProofContext.init Proof.context_of state); + in + ProofContext.print_thms_containing ctxt goal lim spec + end); + fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state => ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state))); diff -r 5b70f789e079 -r f2074e12d1d4 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon May 16 09:34:20 2005 +0200 +++ b/src/Pure/Isar/isar_syn.ML Mon May 16 09:35:05 2005 +0200 @@ -631,10 +631,30 @@ (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations)); val thms_containingP = - OuterSyntax.improper_command "thms_containing" - "print facts containing certain constants or variables" - K.diag (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) -- - Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing)); + let + (* intro, elim, dest and rewrite are reserved, otherwise it's a pattern *) + fun decode "intro" = ProofContext.Intro + | decode "elim" = ProofContext.Elim + | decode "dest" = ProofContext.Dest + | decode "rewrite" = ProofContext.Rewrite + | decode x = ProofContext.Pattern x; + + (* either name:term or term *) + val criterion = ((P.term :-- (fn "name" => P.$$$ ":" |-- P.term | + _ => Scan.fail) + ) >> (ProofContext.Name o #2)) || + (P.term >> decode); + in + OuterSyntax.improper_command "thms_containing" + "print facts meeting specified criteria" + K.diag + (* obtain (int option * (bool * string) list) representing + a limit and a set of constraints (the bool indicates whether + the constraint is inclusive or exclusive) *) + (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) -- + Scan.repeat (((Scan.option P.minus >> is_none) -- criterion)) + >> (Toplevel.no_timing oo IsarCmd.print_thms_containing)) + end; val thm_depsP = OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" diff -r 5b70f789e079 -r f2074e12d1d4 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon May 16 09:34:20 2005 +0200 +++ b/src/Pure/Isar/proof_context.ML Mon May 16 09:35:05 2005 +0200 @@ -155,7 +155,9 @@ val prems_limit: int ref val pretty_asms: context -> Pretty.T list val pretty_context: context -> Pretty.T list - val print_thms_containing: context -> int option -> string list -> unit + datatype search_criterion = Intro | Elim | Dest | Rewrite | + Pattern of string | Name of string; + val print_thms_containing: context -> term option -> int option -> (bool * search_criterion) list -> unit end; signature PRIVATE_PROOF_CONTEXT = @@ -171,6 +173,8 @@ structure ProofContext: PRIVATE_PROOF_CONTEXT = struct +datatype search_criterion = Intro | Elim | Dest | Rewrite | + Pattern of string | Name of string; (** datatype context **) @@ -1470,28 +1474,159 @@ (* things like "prems" can occur twice under some circumstances *) gen_distinct eq_fst (FactIndex.find ([],[]) index); -fun print_thms_containing ctxt opt_limit ss = +fun isSubstring pat str = + if String.size pat = 0 then true + else if String.size pat > String.size str then false + else if String.substring (str, 0, String.size pat) = pat then true + else isSubstring pat (String.extract (str, 1, NONE)); + +(* Takes a string pattern, such as "(_::nat) + (_ + _)" and converts it into + a term with all free variables made schematic *) +fun str_pattern_to_term sg str_pattern = + let + (* pattern as term with dummies as Consts *) + val term_pattern = read_cterm sg (str_pattern, TypeInfer.logicT) + |> Thm.term_of; + (* with dummies as Vars *) + val v_pattern = #2 (Term.replace_dummy_patterns (1,term_pattern)); + in + (* with schematic vars *) + #1 (Type.varify (v_pattern, [])) + end; + +(* alternate rem_top which checks for a Trueprop, unlike that in PureThy *) +fun rem_top_c (Term.Const ("Trueprop", _) $ t) = t + | rem_top_c _ = Bound 0; + +(* ---------- search filter contructions go here *) + +(* terms supplied in string form as patterns *) +fun str_term_pat_to_filter sg str_pat = + let + val tsig = Sign.tsig_of sg; + val pat = str_pattern_to_term sg str_pat; + + (* must qualify type so ML doesn't go and replace it with a concrete one *) + fun name_thm_matches_pattern tsig pat (_:string, thm) = + Pattern.matches_subterm tsig (pat, Thm.prop_of thm); + in + name_thm_matches_pattern (Sign.tsig_of sg) pat + end; + +(* create filter that just looks for a string in the name, + substring match only (no regexps are performed) *) +fun str_name_pat_to_filter str_pat (name, _:Thm.thm) = isSubstring str_pat name; + +(* for elimination and destruction rules, we must check if the major premise + matches with one of the assumptions in the top subgoal, but we must + additionally make sure that we tell elim/dest apart, using thm_check_fun *) +fun elim_dest_filter thm_check_fun sg goal = + let + val elims_extract = (fn thm => if Thm.no_prems thm then [] else [thm], + rem_top_c o hd o Logic.strip_imp_prems); + + (* assumptions of the top subgoal *) + val prems = map rem_top_c (Logic.prems_of_goal goal 1); + + fun prem_matches_name_thm prems (name_thm as (name,thm)) = + List.exists + (fn p => PureThy.is_matching_thm elims_extract sg p name_thm + andalso (thm_check_fun thm)) prems; + in + prem_matches_name_thm prems + end; + +(* ------------ *) + +(* collect all the Var statements in a term *) +fun vars_of_term (Const _) = [] + | vars_of_term (Free _) = [] + | vars_of_term (Bound _) = [] + | vars_of_term (Abs (_,_,t)) = vars_of_term t + | vars_of_term (v as (Var _)) = [v] + | vars_of_term (x $ y) = vars_of_term x @ (vars_of_term y); + +(* elimination rule: conclusion is a Var and + no Var in the conclusion appears in the major premise + Note: only makes sense if the major premise already matched the assumption + of some goal! *) +fun is_elim_rule thm = + let + val {prop, ...} = rep_thm thm; + val concl = rem_top_c (Logic.strip_imp_concl prop); + val major_prem = hd (Logic.strip_imp_prems prop); + val prem_vars = distinct (vars_of_term major_prem); + val concl_vars = distinct (vars_of_term concl); + in + Term.is_Var concl andalso ((prem_vars inter concl_vars) = []) + end; + +fun crit2str (Name name) = "name:" ^ name + | crit2str Elim = "elim" + | crit2str Intro = "intro" + | crit2str Rewrite = "rewrite" + | crit2str Dest = "dest" + | crit2str (Pattern x) = x; + +val criteria_to_str = + let + fun criterion_to_str ( true, ct) = "+ : " ^ crit2str ct + | criterion_to_str (false, ct) = "- : " ^ crit2str ct + in + map criterion_to_str + end; + +fun make_filter _ _ (Name name) = str_name_pat_to_filter name + | make_filter sg _ (Pattern p) = str_term_pat_to_filter sg p + (* beyond this point, only criteria requiring a goal! *) + | make_filter _ NONE c = + error ("Need to have a current goal to use " ^ (crit2str c)) + | make_filter sg (SOME goal) Elim = + elim_dest_filter is_elim_rule sg goal + | make_filter sg (SOME goal) Dest = + (* in this case all that is not elim rule is dest *) + elim_dest_filter (not o is_elim_rule) sg goal + | make_filter sg (SOME goal) Intro = + let + (* filter by checking conclusion of theorem against conclusion of goal *) + fun intros_extract () = (single, rem_top_c o Logic.strip_imp_concl); + val concl = rem_top_c (Logic.concl_of_goal goal 1); + in + (fn name_thm => + PureThy.is_matching_thm (intros_extract ()) sg concl name_thm) + end + | make_filter _ _ c = + error (crit2str c ^ " unimplemented"); + (* XXX: searching for rewrites currently impossible since we'd need + a simplifier, which is included *after* Pure *) + +(* create filters ... convert negative ones to positive ones *) +fun make_filters sg opt_goal = + map (fn (b,sc) => (if b then I else not) o (make_filter sg opt_goal sc)); + +fun print_thms_containing ctxt opt_goal opt_limit criteria = let val prt_term = pretty_term ctxt; val prt_fact = pretty_fact ctxt; + val ss = criteria_to_str criteria; - (* theorems from the theory and its ancestors *) + (* facts from the theory and its ancestors *) val thy = theory_of ctxt; val sg1 = Theory.sign_of thy; val all_thys = thy :: (Theory.ancestors_of thy) - val thms1 = List.concat (map PureThy.thms_with_names_of all_thys); - val facts1 = - PureThy.find_theorems sg1 thms1 ss; + val facts1 = List.concat (map PureThy.thms_with_names_of all_thys); + val filters1 = make_filters sg1 opt_goal criteria; + val matches1 = PureThy.find_theorems facts1 filters1; - (* theorems from the local context *) + (* facts from the local context *) val sg2 = sign_of ctxt; - val thms2 = local_facts ctxt; - val facts2 = - PureThy.find_theorems sg2 thms2 ss; + val facts2 = local_facts ctxt; + val filters2 = make_filters sg2 opt_goal criteria; + val matches2 = PureThy.find_theorems facts2 filters2; (* combine them, use a limit, then print *) - val facts = facts1 @ facts2; - val len = length facts; + val matches = matches1 @ matches2; + val len = length matches; val limit = getOpt (opt_limit, ! thms_containing_limit); val count = Int.min (limit, len); @@ -1503,13 +1638,14 @@ " theorems (" ^ (Int.toString count) ^ " displayed):"), Pretty.fbrk]); in - if null facts then + if null matches then warning "find_theorems: nothing found" else - Pretty.writeln header; - ((if len <= limit then [] else [Pretty.str "..."]) @ - map (prt_fact) (Library.drop (len - limit, facts))) |> - Pretty.chunks |> Pretty.writeln + Pretty.writeln header; + ((if len <= limit then [] else [Pretty.str "..."]) @ + map (prt_fact) (Library.drop (len - limit, matches))) |> + Pretty.chunks |> Pretty.writeln end; end; + diff -r 5b70f789e079 -r f2074e12d1d4 src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Mon May 16 09:34:20 2005 +0200 +++ b/src/Pure/proof_general.ML Mon May 16 09:35:05 2005 +0200 @@ -372,8 +372,11 @@ (* misc commands for ProofGeneral/isa *) +(* PG/isa mode does not go through the Isar parser, hence we + interpret everything as term pattern only *) fun thms_containing ss = - ProofContext.print_thms_containing (ProofContext.init (the_context ())) NONE ss; + ProofContext.print_thms_containing (ProofContext.init (the_context ())) NONE NONE + (map (fn s => (true, ProofContext.Pattern s)) ss); val welcome = priority o Session.welcome; val help = welcome; diff -r 5b70f789e079 -r f2074e12d1d4 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Mon May 16 09:34:20 2005 +0200 +++ b/src/Pure/pure_thy.ML Mon May 16 09:35:05 2005 +0200 @@ -33,10 +33,12 @@ val select_thm: thmref -> thm list -> thm list val cond_extern_thm_sg: Sign.sg -> string -> xstring val thms_containing: theory -> string list * string list -> (string * thm list) list - val find_theorems: Sign.sg -> (string * thm list) list -> string list -> (string * thm list) list + val find_theorems: ('a * 'b list) list -> ('a * 'b -> bool) list -> ('a * 'b list) list val thms_containing_consts: theory -> string list -> (string * thm) list val find_matching_thms: (thm -> thm list) * (term -> term) -> theory -> term -> (string * thm) list + val is_matching_thm: (thm -> thm list) * (term -> term) + -> Sign.sg -> term -> (string * thm) -> bool val find_intros: theory -> term -> (string * thm) list val find_intros_goal : theory -> thm -> int -> (string * thm) list val find_elims : theory -> term -> (string * thm) list @@ -252,46 +254,29 @@ thms_containing thy (consts, []) |> map #2 |> List.concat |> map (fn th => (Thm.name_of_thm th, th)) -(* find_theorems - finding theorems by matching on a series of subterms *) - -(* Takes a string pattern, such as "(_::nat) + (_ + _)" and converts it into - a term with all free variables made schematic *) -fun str_pattern_to_term sg str_pattern = - let - (* pattern as term with dummies as Consts *) - val term_pattern = read_cterm sg (str_pattern, TypeInfer.logicT) - |> Thm.term_of; - (* with dummies as Vars *) - val v_pattern = #2 (Term.replace_dummy_patterns (1,term_pattern)); - in - (* with schematic vars *) - #1 (Type.varify (v_pattern, [])) - end; +(* Searching based on filters *) +(* a filter must only take a (name:string, theorem:Thm.thm) and return true + if it finds a match, false if it doesn't *) -(* find all thms such that for each returned thm, all given - propositions are subterms of it *) -fun thms_matching_patterns tsign (pat::pats) thms = - let - fun match_single pattern thm = - Pattern.matches_subterm tsign (pat, Thm.prop_of thm); - in - thms_matching_patterns tsign pats - (List.filter (match_single pat) thms) - end - | thms_matching_patterns _ _ thms = thms; +(* given facts and filters, find all facts in which at least one theorem + matches on ALL filters *) +fun find_theorems facts filters = + let + (* break fact up into theorems, but associate them with the name of this + fact, so that filters looking by name will only consider the fact's + name *) + fun fact_to_names_thms (name, thms) = + map (fn thm => (name, thm)) thms; -(* facts are pairs of theorem name and a list of its thms *) -fun find_theorems sg facts str_patterns = - let - val typesg = Sign.tsig_of sg; - - (* the patterns we will be looking for *) - val patterns = map (str_pattern_to_term sg) str_patterns; + (* all filters return true when applied to a named theorem *) + fun match_all_filters filters name_thm = + List.all (fn filter => filter name_thm) filters; - (* we are interested in theorems which have one or more thms for which - all patterns are subterms *) - fun matches (_, thms) = - (not o null o (thms_matching_patterns typesg patterns)) thms + (* at least one theorem in this fact which matches all filters *) + fun fact_matches_filters filters fact = + List.exists (match_all_filters filters) (fact_to_names_thms fact); + + fun matches x = (fact_matches_filters filters x) in List.filter matches facts end; @@ -347,6 +332,13 @@ in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end; +(* like find_matching_thms, but for one named theorem only *) +fun is_matching_thm extract sg prop name_thm = + (case top_const prop of NONE => false + | SOME c => + not ([] = select_match(c,prop, sg,[name_thm],extract))); + + fun find_matching_thms extract thy prop = (case top_const prop of NONE => [] | SOME c => let val thms = thms_containing_consts thy [c]