searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
--- 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)));
--- 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"
--- 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;
+
+(* ------------</filter constructions> *)
+
+(* 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;
+
--- 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;
--- 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]