# HG changeset patch # User wenzelm # Date 1235745982 -3600 # Node ID 8d6145694bb5b2bc5c87ee2f55bce9f682a384b0 # Parent c59a1258559baa134c6b56c10fc6be4007c2cafb moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each; diff -r c59a1258559b -r 8d6145694bb5 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri Feb 27 12:28:28 2009 +0100 +++ b/src/Pure/IsaMakefile Fri Feb 27 15:46:22 2009 +0100 @@ -59,18 +59,18 @@ Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \ Isar/class_target.ML Isar/code.ML Isar/code_unit.ML \ Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \ - Isar/expression.ML Isar/find_consts.ML Isar/find_theorems.ML \ - Isar/isar.ML Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML \ - Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \ - Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML \ - Isar/obtain.ML Isar/outer_keyword.ML Isar/outer_lex.ML \ - Isar/outer_parse.ML Isar/outer_syntax.ML Isar/overloading.ML \ - Isar/proof.ML Isar/proof_context.ML Isar/proof_display.ML \ - Isar/proof_node.ML Isar/rule_cases.ML Isar/rule_insts.ML \ - Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML \ - Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \ - Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_context.ML ML/ml_lex.ML \ - ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML Proof/extraction.ML \ + Isar/expression.ML Isar/isar.ML Isar/isar_cmd.ML \ + Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \ + Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \ + Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \ + Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \ + Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \ + Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \ + Isar/rule_cases.ML Isar/rule_insts.ML Isar/session.ML \ + Isar/skip_proof.ML Isar/spec_parse.ML Isar/specification.ML \ + Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML \ + ML/ml_antiquote.ML ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML \ + ML/ml_syntax.ML ML/ml_thms.ML Proof/extraction.ML \ Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \ Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \ ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \ @@ -84,16 +84,17 @@ Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \ Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML \ Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML \ - Thy/thy_syntax.ML Tools/ROOT.ML Tools/isabelle_process.ML \ - Tools/named_thms.ML Tools/xml_syntax.ML assumption.ML axclass.ML \ - codegen.ML config.ML conjunction.ML consts.ML context.ML \ - context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML \ - facts.ML goal.ML interpretation.ML library.ML logic.ML \ - meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML \ - old_goals.ML old_term.ML pattern.ML primitive_defs.ML proofterm.ML \ - pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML \ - subgoal.ML tactic.ML tctical.ML term.ML term_ord.ML term_subst.ML \ - theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML + Thy/thy_syntax.ML Tools/ROOT.ML Tools/find_consts.ML \ + Tools/find_theorems.ML Tools/isabelle_process.ML Tools/named_thms.ML \ + Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \ + conjunction.ML consts.ML context.ML context_position.ML conv.ML \ + defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \ + interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \ + morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML \ + primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML \ + sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML \ + term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML \ + type_infer.ML unify.ML variable.ML @./mk diff -r c59a1258559b -r 8d6145694bb5 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Fri Feb 27 12:28:28 2009 +0100 +++ b/src/Pure/Isar/ROOT.ML Fri Feb 27 15:46:22 2009 +0100 @@ -89,7 +89,5 @@ (*theory and proof operations*) use "rule_insts.ML"; use "../Thy/thm_deps.ML"; -use "find_theorems.ML"; -use "find_consts.ML"; use "isar_cmd.ML"; use "isar_syn.ML"; diff -r c59a1258559b -r 8d6145694bb5 src/Pure/Isar/find_consts.ML --- a/src/Pure/Isar/find_consts.ML Fri Feb 27 12:28:28 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,120 +0,0 @@ -(* Title: find_consts.ML - Author: Timothy Bourke and Gerwin Klein, NICTA - - Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by type - over constants, but matching is not fuzzy -*) - -signature FIND_CONSTS = -sig - datatype criterion = Strict of string - | Loose of string - | Name of string - - val default_criteria : (bool * criterion) list ref - - val find_consts : Proof.context -> (bool * criterion) list -> unit -end; - -structure FindConsts : FIND_CONSTS = -struct - -datatype criterion = Strict of string - | Loose of string - | Name of string; - -val default_criteria = ref [(false, Name ".sko_")]; - -fun add_tye (_, (_, t)) n = size_of_typ t + n; - -fun matches_subtype thy typat = let - val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty); - - fun fs [] = false - | fs (t::ts) = f t orelse fs ts - - and f (t as Type (_, ars)) = p t orelse fs ars - | f t = p t; - in f end; - -fun check_const p (nm, (ty, _)) = if p (nm, ty) - then SOME (size_of_typ ty) - else NONE; - -fun opt_not f (c as (_, (ty, _))) = if is_some (f c) - then NONE else SOME (size_of_typ ty); - -fun filter_const (_, NONE) = NONE - | filter_const (f, (SOME (c, r))) = Option.map - (pair c o ((curry Int.min) r)) (f c); - -fun pretty_criterion (b, c) = - let - fun prfx s = if b then s else "-" ^ s; - in - (case c of - Strict pat => Pretty.str (prfx "strict: " ^ quote pat) - | Loose pat => Pretty.str (prfx (quote pat)) - | Name name => Pretty.str (prfx "name: " ^ quote name)) - end; - -fun pretty_const ctxt (nm, ty) = let - val ty' = Logic.unvarifyT ty; - in - Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk, - Pretty.str "::", Pretty.brk 1, - Pretty.quote (Syntax.pretty_typ ctxt ty')] - end; - -fun find_consts ctxt raw_criteria = let - val start = start_timing (); - - val thy = ProofContext.theory_of ctxt; - val low_ranking = 10000; - - fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit) - |> type_of; - - fun make_match (Strict arg) = - let val qty = make_pattern arg; in - fn (_, (ty, _)) => let - val tye = Sign.typ_match thy (qty, ty) Vartab.empty; - val sub_size = Vartab.fold add_tye tye 0; - in SOME sub_size end handle MATCH => NONE - end - - | make_match (Loose arg) = - check_const (matches_subtype thy (make_pattern arg) o snd) - - | make_match (Name arg) = check_const (match_string arg o fst); - - fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit); - val criteria = map make_criterion ((!default_criteria) @ raw_criteria); - - val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy; - fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria; - - val matches = Symtab.fold (cons o eval_entry) consts [] - |> map_filter I - |> sort (rev_order o int_ord o pairself snd) - |> map ((apsnd fst) o fst); - - val end_msg = " in " ^ - (List.nth (String.tokens Char.isSpace (end_timing start), 3)) - ^ " secs" - in - Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) - :: Pretty.str "" - :: (Pretty.str o concat) - (if null matches - then ["nothing found", end_msg] - else ["found ", (string_of_int o length) matches, - " constants", end_msg, ":"]) - :: Pretty.str "" - :: map (pretty_const ctxt) matches - |> Pretty.chunks - |> Pretty.writeln - end handle ERROR s => Output.error_msg s - -end; - diff -r c59a1258559b -r 8d6145694bb5 src/Pure/Isar/find_theorems.ML --- a/src/Pure/Isar/find_theorems.ML Fri Feb 27 12:28:28 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,378 +0,0 @@ -(* Title: Pure/Isar/find_theorems.ML - Author: Rafal Kolanski and Gerwin Klein, NICTA - -Retrieve theorems from proof context. -*) - -signature FIND_THEOREMS = -sig - val limit: int ref - val tac_limit: int ref - - datatype 'term criterion = - Name of string | Intro | Elim | Dest | Solves | Simp of 'term | - Pattern of 'term - - val find_theorems: Proof.context -> thm option -> bool -> - (bool * string criterion) list -> (Facts.ref * thm) list - - val print_theorems: Proof.context -> thm option -> int option -> bool -> - (bool * string criterion) list -> unit -end; - -structure FindTheorems: FIND_THEOREMS = -struct - -(** search criteria **) - -datatype 'term criterion = - Name of string | Intro | Elim | Dest | Solves | Simp of 'term | - Pattern of 'term; - -fun read_criterion _ (Name name) = Name name - | read_criterion _ Intro = Intro - | read_criterion _ Elim = Elim - | read_criterion _ Dest = Dest - | read_criterion _ Solves = Solves - | read_criterion ctxt (Simp str) = Simp (ProofContext.read_term_pattern ctxt str) - | read_criterion ctxt (Pattern str) = Pattern (ProofContext.read_term_pattern ctxt str); - -fun pretty_criterion ctxt (b, c) = - let - fun prfx s = if b then s else "-" ^ s; - in - (case c of - Name name => Pretty.str (prfx "name: " ^ quote name) - | Intro => Pretty.str (prfx "intro") - | Elim => Pretty.str (prfx "elim") - | Dest => Pretty.str (prfx "dest") - | Solves => Pretty.str (prfx "solves") - | Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1, - Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))] - | Pattern pat => Pretty.enclose (prfx " \"") "\"" - [Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)]) - end; - -(** search criterion filters **) - -(*generated filters are to be of the form - input: (Facts.ref * thm) - output: (p:int, s:int) option, where - NONE indicates no match - p is the primary sorting criterion - (eg. number of assumptions in the theorem) - s is the secondary sorting criterion - (eg. size of the substitution for intro, elim and dest) - when applying a set of filters to a thm, fold results in: - (biggest p, sum of all s) - currently p and s only matter for intro, elim, dest and simp filters, - otherwise the default ordering is used. -*) - - -(* matching theorems *) - -fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy; - -(*extract terms from term_src, refine them to the parts that concern us, - if po try match them against obj else vice versa. - trivial matches are ignored. - returns: smallest substitution size*) -fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src = - let - val thy = ProofContext.theory_of ctxt; - - fun matches pat = - is_nontrivial thy pat andalso - Pattern.matches thy (if po then (pat, obj) else (obj, pat)); - - fun substsize pat = - let val (_, subst) = - Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty) - in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end; - - fun bestmatch [] = NONE - | bestmatch xs = SOME (foldr1 Int.min xs); - - val match_thm = matches o refine_term; - in - map (substsize o refine_term) (filter match_thm (extract_terms term_src)) - |> bestmatch - end; - - -(* filter_name *) - -fun filter_name str_pat (thmref, _) = - if match_string str_pat (Facts.name_of_ref thmref) - then SOME (0, 0) else NONE; - -(* filter intro/elim/dest/solves rules *) - -fun filter_dest ctxt goal (_, thm) = - let - val extract_dest = - (fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm], - hd o Logic.strip_imp_prems); - val prems = Logic.prems_of_goal goal 1; - - fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm; - val successful = prems |> map_filter try_subst; - in - (*if possible, keep best substitution (one with smallest size)*) - (*dest rules always have assumptions, so a dest with one - assumption is as good as an intro rule with none*) - if not (null successful) - then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE - end; - -fun filter_intro ctxt goal (_, thm) = - let - val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl); - val concl = Logic.concl_of_goal goal 1; - val ss = is_matching_thm extract_intro ctxt true concl thm; - in - if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE - end; - -fun filter_elim ctxt goal (_, thm) = - if not (Thm.no_prems thm) then - let - val rule = Thm.full_prop_of thm; - val prems = Logic.prems_of_goal goal 1; - val goal_concl = Logic.concl_of_goal goal 1; - val rule_mp = hd (Logic.strip_imp_prems rule); - val rule_concl = Logic.strip_imp_concl rule; - fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2); - val rule_tree = combine rule_mp rule_concl; - fun goal_tree prem = combine prem goal_concl; - fun try_subst prem = - is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree; - val successful = prems |> map_filter try_subst; - in - (*elim rules always have assumptions, so an elim with one - assumption is as good as an intro rule with none*) - if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm) - andalso not (null successful) - then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE - end - else NONE - -val tac_limit = ref 5; - -fun filter_solves ctxt goal = let - val baregoal = Logic.get_goal (prop_of goal) 1; - - fun etacn thm i = Seq.take (!tac_limit) o etac thm i; - fun try_thm thm = if Thm.no_prems thm then rtac thm 1 goal - else (etacn thm THEN_ALL_NEW - (Goal.norm_hhf_tac THEN' - Method.assumption_tac ctxt)) 1 goal; - in - fn (_, thm) => if (is_some o Seq.pull o try_thm) thm - then SOME (Thm.nprems_of thm, 0) else NONE - end; - -(* filter_simp *) - -fun filter_simp ctxt t (_, thm) = - let - val (_, {mk_rews = {mk, ...}, ...}) = - Simplifier.rep_ss (Simplifier.local_simpset_of ctxt); - val extract_simp = - (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl); - val ss = is_matching_thm extract_simp ctxt false t thm - in - if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE - end; - - -(* filter_pattern *) - -fun get_names t = (Term.add_const_names t []) union (Term.add_free_names t []); -fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm); - (* Including all constants and frees is only sound because - matching uses higher-order patterns. If full matching - were used, then constants that may be subject to - beta-reduction after substitution of frees should - not be included for LHS set because they could be - thrown away by the substituted function. - e.g. for (?F 1 2) do not include 1 or 2, if it were - possible for ?F to be (% x y. 3) - The largest possible set should always be included on - the RHS. *) - -fun filter_pattern ctxt pat = let - val pat_consts = get_names pat; - - fun check (t, NONE) = check (t, SOME (get_thm_names t)) - | check ((_, thm), c as SOME thm_consts) = - (if pat_consts subset_string thm_consts - andalso (Pattern.matches_subterm (ProofContext.theory_of ctxt) - (pat, Thm.full_prop_of thm)) - then SOME (0, 0) else NONE, c); - in check end; - -(* interpret criteria as filters *) - -local - -fun err_no_goal c = - error ("Current goal required for " ^ c ^ " search criterion"); - -val fix_goal = Thm.prop_of; -val fix_goalo = Option.map fix_goal; - -fun filter_crit _ _ (Name name) = apfst (filter_name name) - | filter_crit _ NONE Intro = err_no_goal "intro" - | filter_crit _ NONE Elim = err_no_goal "elim" - | filter_crit _ NONE Dest = err_no_goal "dest" - | filter_crit _ NONE Solves = err_no_goal "solves" - | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt - (fix_goal goal)) - | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt - (fix_goal goal)) - | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt - (fix_goal goal)) - | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal) - | filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat) - | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat; - -fun opt_not x = if is_some x then NONE else SOME (0, 0); - -fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int) - | opt_add _ _ = NONE; - -fun app_filters thm = let - fun app (NONE, _, _) = NONE - | app (SOME v, consts, []) = SOME (v, thm) - | app (r, consts, f::fs) = let val (r', consts') = f (thm, consts) - in app (opt_add r r', consts', fs) end; - in app end; - -in - -fun filter_criterion ctxt opt_goal (b, c) = - (if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c; - -fun all_filters filters thms = - let - fun eval_filters thm = app_filters thm (SOME (0, 0), NONE, filters); - - (*filters return: (number of assumptions, substitution size) option, so - sort (desc. in both cases) according to number of assumptions first, - then by the substitution size*) - fun thm_ord (((p0, s0), _), ((p1, s1), _)) = - prod_ord int_ord int_ord ((p1, s1), (p0, s0)); - in map_filter eval_filters thms |> sort thm_ord |> map #2 end; - -end; - - -(* removing duplicates, preferring nicer names, roughly n log n *) - -local - -val index_ord = option_ord (K EQUAL); -val hidden_ord = bool_ord o pairself NameSpace.is_hidden; -val qual_ord = int_ord o pairself (length o NameSpace.explode); -val txt_ord = int_ord o pairself size; - -fun nicer_name (x, i) (y, j) = - (case hidden_ord (x, y) of EQUAL => - (case index_ord (i, j) of EQUAL => - (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord) - | ord => ord) - | ord => ord) <> GREATER; - -fun rem_cdups nicer xs = - let - fun rem_c rev_seen [] = rev rev_seen - | rem_c rev_seen [x] = rem_c (x :: rev_seen) [] - | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) = - if Thm.eq_thm_prop (t, t') - then rem_c rev_seen ((if nicer n n' then x else y) :: xs) - else rem_c (x :: rev_seen) (y :: xs) - in rem_c [] xs end; - -in - -fun nicer_shortest ctxt = let - val ns = ProofContext.theory_of ctxt - |> PureThy.facts_of - |> Facts.space_of; - - val len_sort = sort (int_ord o (pairself size)); - fun shorten s = (case len_sort (NameSpace.get_accesses ns s) of - [] => s - | s'::_ => s'); - - fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = - nicer_name (shorten x, i) (shorten y, j) - | nicer (Facts.Fact _) (Facts.Named _) = true - | nicer (Facts.Named _) (Facts.Fact _) = false; - in nicer end; - -fun rem_thm_dups nicer xs = - xs ~~ (1 upto length xs) - |> sort (TermOrd.fast_term_ord o pairself (Thm.prop_of o #2 o #1)) - |> rem_cdups nicer - |> sort (int_ord o pairself #2) - |> map #1; - -end; - - -(* print_theorems *) - -fun all_facts_of ctxt = - maps Facts.selections - (Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @ - Facts.dest_static [] (ProofContext.facts_of ctxt)); - -val limit = ref 40; - -fun find_theorems ctxt opt_goal rem_dups raw_criteria = - let - val add_prems = Seq.hd o (TRY (Method.insert_tac - (Assumption.prems_of ctxt) 1)); - val opt_goal' = Option.map add_prems opt_goal; - - val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; - val filters = map (filter_criterion ctxt opt_goal') criteria; - - val raw_matches = all_filters filters (all_facts_of ctxt); - - val matches = - if rem_dups - then rem_thm_dups (nicer_shortest ctxt) raw_matches - else raw_matches; - in matches end; - -fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = let - val start = start_timing (); - - val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; - val matches = find_theorems ctxt opt_goal rem_dups raw_criteria; - - val len = length matches; - val lim = the_default (! limit) opt_limit; - val thms = Library.drop (len - lim, matches); - - val end_msg = " in " ^ - (List.nth (String.tokens Char.isSpace (end_timing start), 3)) - ^ " secs" - in - Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) - :: Pretty.str "" :: - (if null thms then [Pretty.str ("nothing found" ^ end_msg)] - else - [Pretty.str ("found " ^ string_of_int len ^ " theorems" ^ - (if len <= lim then "" - else " (" ^ string_of_int lim ^ " displayed)") - ^ end_msg ^ ":"), Pretty.str ""] @ - map Display.pretty_fact thms) - |> Pretty.chunks |> Pretty.writeln - end - -end; diff -r c59a1258559b -r 8d6145694bb5 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Fri Feb 27 12:28:28 2009 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Fri Feb 27 15:46:22 2009 +0100 @@ -62,10 +62,6 @@ val class_deps: Toplevel.transition -> Toplevel.transition val thy_deps: Toplevel.transition -> Toplevel.transition val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition - val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list - -> Toplevel.transition -> Toplevel.transition - val find_consts: (bool * FindConsts.criterion) list -> - Toplevel.transition -> Toplevel.transition val unused_thms: (string list * string list option) option -> Toplevel.transition -> Toplevel.transition val print_binds: Toplevel.transition -> Toplevel.transition @@ -403,20 +399,9 @@ |> sort (int_ord o pairself #1) |> map #2; in Present.display_graph gr end); - -(* retrieve theorems *) - fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state => ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args)); -fun find_theorems ((opt_lim, rem_dups), spec) = - Toplevel.unknown_theory o Toplevel.keep (fn state => - let - val proof_state = Toplevel.enter_proof_body state; - val ctxt = Proof.context_of proof_state; - val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2); - in FindTheorems.print_theorems ctxt opt_goal opt_lim rem_dups spec end); - (* find unused theorems *) @@ -434,12 +419,6 @@ |> map pretty_thm |> Pretty.chunks |> Pretty.writeln end); -(* retrieve constants *) - -fun find_consts spec = - Toplevel.unknown_theory o Toplevel.keep (fn state => - let val ctxt = (Proof.context_of o Toplevel.enter_proof_body) state - in FindConsts.find_consts ctxt spec end); (* print proof context contents *) diff -r c59a1258559b -r 8d6145694bb5 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Feb 27 12:28:28 2009 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Feb 27 15:46:22 2009 +0100 @@ -37,6 +37,7 @@ (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory)); + (** markup commands **) val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag @@ -79,7 +80,7 @@ -(** theory sections **) +(** theory commands **) (* classes and sorts *) @@ -853,47 +854,6 @@ OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); -local - -val criterion = - P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindTheorems.Name || - P.reserved "intro" >> K FindTheorems.Intro || - P.reserved "elim" >> K FindTheorems.Elim || - P.reserved "dest" >> K FindTheorems.Dest || - P.reserved "solves" >> K FindTheorems.Solves || - P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp || - P.term >> FindTheorems.Pattern; - -val options = - Scan.optional - (P.$$$ "(" |-- - P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true - --| P.$$$ ")")) (NONE, true); -in - -val _ = - OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag - (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion)) - >> (Toplevel.no_timing oo IsarCmd.find_theorems)); - -end; - -local - -val criterion = - P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindConsts.Strict || - P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindConsts.Name || - P.xname >> FindConsts.Loose; - -in - -val _ = - OuterSyntax.improper_command "find_consts" "search constants by type pattern" - K.diag (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion)) - >> (Toplevel.no_timing oo IsarCmd.find_consts)); - -end; - val _ = OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); @@ -948,6 +908,7 @@ (Toplevel.no_timing oo IsarCmd.unused_thms)); + (** system commands (for interactive mode only) **) val _ = diff -r c59a1258559b -r 8d6145694bb5 src/Pure/Tools/ROOT.ML --- a/src/Pure/Tools/ROOT.ML Fri Feb 27 12:28:28 2009 +0100 +++ b/src/Pure/Tools/ROOT.ML Fri Feb 27 15:46:22 2009 +0100 @@ -9,6 +9,9 @@ (*basic XML support*) use "xml_syntax.ML"; +use "find_theorems.ML"; +use "find_consts.ML"; + (*quickcheck/autosolve needed here because of pg preferences*) use "../../Tools/quickcheck.ML"; use "../../Tools/auto_solve.ML"; diff -r c59a1258559b -r 8d6145694bb5 src/Pure/Tools/find_consts.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/find_consts.ML Fri Feb 27 15:46:22 2009 +0100 @@ -0,0 +1,146 @@ +(* Title: find_consts.ML + Author: Timothy Bourke and Gerwin Klein, NICTA + + Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by type + over constants, but matching is not fuzzy +*) + +signature FIND_CONSTS = +sig + datatype criterion = Strict of string + | Loose of string + | Name of string + + val default_criteria : (bool * criterion) list ref + + val find_consts : Proof.context -> (bool * criterion) list -> unit +end; + +structure FindConsts : FIND_CONSTS = +struct + +datatype criterion = Strict of string + | Loose of string + | Name of string; + +val default_criteria = ref [(false, Name ".sko_")]; + +fun add_tye (_, (_, t)) n = size_of_typ t + n; + +fun matches_subtype thy typat = let + val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty); + + fun fs [] = false + | fs (t::ts) = f t orelse fs ts + + and f (t as Type (_, ars)) = p t orelse fs ars + | f t = p t; + in f end; + +fun check_const p (nm, (ty, _)) = if p (nm, ty) + then SOME (size_of_typ ty) + else NONE; + +fun opt_not f (c as (_, (ty, _))) = if is_some (f c) + then NONE else SOME (size_of_typ ty); + +fun filter_const (_, NONE) = NONE + | filter_const (f, (SOME (c, r))) = Option.map + (pair c o ((curry Int.min) r)) (f c); + +fun pretty_criterion (b, c) = + let + fun prfx s = if b then s else "-" ^ s; + in + (case c of + Strict pat => Pretty.str (prfx "strict: " ^ quote pat) + | Loose pat => Pretty.str (prfx (quote pat)) + | Name name => Pretty.str (prfx "name: " ^ quote name)) + end; + +fun pretty_const ctxt (nm, ty) = let + val ty' = Logic.unvarifyT ty; + in + Pretty.block [Pretty.quote (Pretty.str nm), Pretty.fbrk, + Pretty.str "::", Pretty.brk 1, + Pretty.quote (Syntax.pretty_typ ctxt ty')] + end; + +fun find_consts ctxt raw_criteria = let + val start = start_timing (); + + val thy = ProofContext.theory_of ctxt; + val low_ranking = 10000; + + fun make_pattern crit = ProofContext.read_term_pattern ctxt ("_::" ^ crit) + |> type_of; + + fun make_match (Strict arg) = + let val qty = make_pattern arg; in + fn (_, (ty, _)) => let + val tye = Sign.typ_match thy (qty, ty) Vartab.empty; + val sub_size = Vartab.fold add_tye tye 0; + in SOME sub_size end handle MATCH => NONE + end + + | make_match (Loose arg) = + check_const (matches_subtype thy (make_pattern arg) o snd) + + | make_match (Name arg) = check_const (match_string arg o fst); + + fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit); + val criteria = map make_criterion ((!default_criteria) @ raw_criteria); + + val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy; + fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria; + + val matches = Symtab.fold (cons o eval_entry) consts [] + |> map_filter I + |> sort (rev_order o int_ord o pairself snd) + |> map ((apsnd fst) o fst); + + val end_msg = " in " ^ + (List.nth (String.tokens Char.isSpace (end_timing start), 3)) + ^ " secs" + in + Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) + :: Pretty.str "" + :: (Pretty.str o concat) + (if null matches + then ["nothing found", end_msg] + else ["found ", (string_of_int o length) matches, + " constants", end_msg, ":"]) + :: Pretty.str "" + :: map (pretty_const ctxt) matches + |> Pretty.chunks + |> Pretty.writeln + end handle ERROR s => Output.error_msg s + + + +(** command syntax **) + +fun find_consts_cmd spec = + Toplevel.unknown_theory o Toplevel.keep (fn state => + find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec); + +local + +structure P = OuterParse and K = OuterKeyword; + +val criterion = + P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Strict || + P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name || + P.xname >> Loose; + +in + +val _ = + OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag + (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion)) + >> (Toplevel.no_timing oo find_consts_cmd)); + +end; + +end; + diff -r c59a1258559b -r 8d6145694bb5 src/Pure/Tools/find_theorems.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/find_theorems.ML Fri Feb 27 15:46:22 2009 +0100 @@ -0,0 +1,422 @@ +(* Title: Pure/Isar/find_theorems.ML + Author: Rafal Kolanski and Gerwin Klein, NICTA + +Retrieve theorems from proof context. +*) + +signature FIND_THEOREMS = +sig + val limit: int ref + val tac_limit: int ref + + datatype 'term criterion = + Name of string | Intro | Elim | Dest | Solves | Simp of 'term | + Pattern of 'term + + val find_theorems: Proof.context -> thm option -> bool -> + (bool * string criterion) list -> (Facts.ref * thm) list + + val print_theorems: Proof.context -> thm option -> int option -> bool -> + (bool * string criterion) list -> unit +end; + +structure FindTheorems: FIND_THEOREMS = +struct + +(** search criteria **) + +datatype 'term criterion = + Name of string | Intro | Elim | Dest | Solves | Simp of 'term | + Pattern of 'term; + +fun read_criterion _ (Name name) = Name name + | read_criterion _ Intro = Intro + | read_criterion _ Elim = Elim + | read_criterion _ Dest = Dest + | read_criterion _ Solves = Solves + | read_criterion ctxt (Simp str) = Simp (ProofContext.read_term_pattern ctxt str) + | read_criterion ctxt (Pattern str) = Pattern (ProofContext.read_term_pattern ctxt str); + +fun pretty_criterion ctxt (b, c) = + let + fun prfx s = if b then s else "-" ^ s; + in + (case c of + Name name => Pretty.str (prfx "name: " ^ quote name) + | Intro => Pretty.str (prfx "intro") + | Elim => Pretty.str (prfx "elim") + | Dest => Pretty.str (prfx "dest") + | Solves => Pretty.str (prfx "solves") + | Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1, + Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))] + | Pattern pat => Pretty.enclose (prfx " \"") "\"" + [Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)]) + end; + + + +(** search criterion filters **) + +(*generated filters are to be of the form + input: (Facts.ref * thm) + output: (p:int, s:int) option, where + NONE indicates no match + p is the primary sorting criterion + (eg. number of assumptions in the theorem) + s is the secondary sorting criterion + (eg. size of the substitution for intro, elim and dest) + when applying a set of filters to a thm, fold results in: + (biggest p, sum of all s) + currently p and s only matter for intro, elim, dest and simp filters, + otherwise the default ordering is used. +*) + + +(* matching theorems *) + +fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy; + +(*extract terms from term_src, refine them to the parts that concern us, + if po try match them against obj else vice versa. + trivial matches are ignored. + returns: smallest substitution size*) +fun is_matching_thm (extract_terms, refine_term) ctxt po obj term_src = + let + val thy = ProofContext.theory_of ctxt; + + fun matches pat = + is_nontrivial thy pat andalso + Pattern.matches thy (if po then (pat, obj) else (obj, pat)); + + fun substsize pat = + let val (_, subst) = + Pattern.match thy (if po then (pat, obj) else (obj, pat)) (Vartab.empty, Vartab.empty) + in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end; + + fun bestmatch [] = NONE + | bestmatch xs = SOME (foldr1 Int.min xs); + + val match_thm = matches o refine_term; + in + map (substsize o refine_term) (filter match_thm (extract_terms term_src)) + |> bestmatch + end; + + +(* filter_name *) + +fun filter_name str_pat (thmref, _) = + if match_string str_pat (Facts.name_of_ref thmref) + then SOME (0, 0) else NONE; + + +(* filter intro/elim/dest/solves rules *) + +fun filter_dest ctxt goal (_, thm) = + let + val extract_dest = + (fn thm => if Thm.no_prems thm then [] else [Thm.full_prop_of thm], + hd o Logic.strip_imp_prems); + val prems = Logic.prems_of_goal goal 1; + + fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm; + val successful = prems |> map_filter try_subst; + in + (*if possible, keep best substitution (one with smallest size)*) + (*dest rules always have assumptions, so a dest with one + assumption is as good as an intro rule with none*) + if not (null successful) + then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE + end; + +fun filter_intro ctxt goal (_, thm) = + let + val extract_intro = (single o Thm.full_prop_of, Logic.strip_imp_concl); + val concl = Logic.concl_of_goal goal 1; + val ss = is_matching_thm extract_intro ctxt true concl thm; + in + if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE + end; + +fun filter_elim ctxt goal (_, thm) = + if not (Thm.no_prems thm) then + let + val rule = Thm.full_prop_of thm; + val prems = Logic.prems_of_goal goal 1; + val goal_concl = Logic.concl_of_goal goal 1; + val rule_mp = hd (Logic.strip_imp_prems rule); + val rule_concl = Logic.strip_imp_concl rule; + fun combine t1 t2 = Const ("*combine*", dummyT --> dummyT) $ (t1 $ t2); + val rule_tree = combine rule_mp rule_concl; + fun goal_tree prem = combine prem goal_concl; + fun try_subst prem = + is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree; + val successful = prems |> map_filter try_subst; + in + (*elim rules always have assumptions, so an elim with one + assumption is as good as an intro rule with none*) + if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm) + andalso not (null successful) + then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE + end + else NONE + +val tac_limit = ref 5; + +fun filter_solves ctxt goal = let + val baregoal = Logic.get_goal (prop_of goal) 1; + + fun etacn thm i = Seq.take (!tac_limit) o etac thm i; + fun try_thm thm = if Thm.no_prems thm then rtac thm 1 goal + else (etacn thm THEN_ALL_NEW + (Goal.norm_hhf_tac THEN' + Method.assumption_tac ctxt)) 1 goal; + in + fn (_, thm) => if (is_some o Seq.pull o try_thm) thm + then SOME (Thm.nprems_of thm, 0) else NONE + end; + + +(* filter_simp *) + +fun filter_simp ctxt t (_, thm) = + let + val (_, {mk_rews = {mk, ...}, ...}) = + Simplifier.rep_ss (Simplifier.local_simpset_of ctxt); + val extract_simp = + (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl); + val ss = is_matching_thm extract_simp ctxt false t thm + in + if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE + end; + + +(* filter_pattern *) + +fun get_names t = (Term.add_const_names t []) union (Term.add_free_names t []); +fun get_thm_names (_, thm) = get_names (Thm.full_prop_of thm); + (* Including all constants and frees is only sound because + matching uses higher-order patterns. If full matching + were used, then constants that may be subject to + beta-reduction after substitution of frees should + not be included for LHS set because they could be + thrown away by the substituted function. + e.g. for (?F 1 2) do not include 1 or 2, if it were + possible for ?F to be (% x y. 3) + The largest possible set should always be included on + the RHS. *) + +fun filter_pattern ctxt pat = let + val pat_consts = get_names pat; + + fun check (t, NONE) = check (t, SOME (get_thm_names t)) + | check ((_, thm), c as SOME thm_consts) = + (if pat_consts subset_string thm_consts + andalso (Pattern.matches_subterm (ProofContext.theory_of ctxt) + (pat, Thm.full_prop_of thm)) + then SOME (0, 0) else NONE, c); + in check end; + + +(* interpret criteria as filters *) + +local + +fun err_no_goal c = + error ("Current goal required for " ^ c ^ " search criterion"); + +val fix_goal = Thm.prop_of; +val fix_goalo = Option.map fix_goal; + +fun filter_crit _ _ (Name name) = apfst (filter_name name) + | filter_crit _ NONE Intro = err_no_goal "intro" + | filter_crit _ NONE Elim = err_no_goal "elim" + | filter_crit _ NONE Dest = err_no_goal "dest" + | filter_crit _ NONE Solves = err_no_goal "solves" + | filter_crit ctxt (SOME goal) Intro = apfst (filter_intro ctxt + (fix_goal goal)) + | filter_crit ctxt (SOME goal) Elim = apfst (filter_elim ctxt + (fix_goal goal)) + | filter_crit ctxt (SOME goal) Dest = apfst (filter_dest ctxt + (fix_goal goal)) + | filter_crit ctxt (SOME goal) Solves = apfst (filter_solves ctxt goal) + | filter_crit ctxt _ (Simp pat) = apfst (filter_simp ctxt pat) + | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat; + +fun opt_not x = if is_some x then NONE else SOME (0, 0); + +fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int) + | opt_add _ _ = NONE; + +fun app_filters thm = let + fun app (NONE, _, _) = NONE + | app (SOME v, consts, []) = SOME (v, thm) + | app (r, consts, f::fs) = let val (r', consts') = f (thm, consts) + in app (opt_add r r', consts', fs) end; + in app end; + +in + +fun filter_criterion ctxt opt_goal (b, c) = + (if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c; + +fun all_filters filters thms = + let + fun eval_filters thm = app_filters thm (SOME (0, 0), NONE, filters); + + (*filters return: (number of assumptions, substitution size) option, so + sort (desc. in both cases) according to number of assumptions first, + then by the substitution size*) + fun thm_ord (((p0, s0), _), ((p1, s1), _)) = + prod_ord int_ord int_ord ((p1, s1), (p0, s0)); + in map_filter eval_filters thms |> sort thm_ord |> map #2 end; + +end; + + +(* removing duplicates, preferring nicer names, roughly n log n *) + +local + +val index_ord = option_ord (K EQUAL); +val hidden_ord = bool_ord o pairself NameSpace.is_hidden; +val qual_ord = int_ord o pairself (length o NameSpace.explode); +val txt_ord = int_ord o pairself size; + +fun nicer_name (x, i) (y, j) = + (case hidden_ord (x, y) of EQUAL => + (case index_ord (i, j) of EQUAL => + (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord) + | ord => ord) + | ord => ord) <> GREATER; + +fun rem_cdups nicer xs = + let + fun rem_c rev_seen [] = rev rev_seen + | rem_c rev_seen [x] = rem_c (x :: rev_seen) [] + | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) = + if Thm.eq_thm_prop (t, t') + then rem_c rev_seen ((if nicer n n' then x else y) :: xs) + else rem_c (x :: rev_seen) (y :: xs) + in rem_c [] xs end; + +in + +fun nicer_shortest ctxt = let + val ns = ProofContext.theory_of ctxt + |> PureThy.facts_of + |> Facts.space_of; + + val len_sort = sort (int_ord o (pairself size)); + fun shorten s = (case len_sort (NameSpace.get_accesses ns s) of + [] => s + | s'::_ => s'); + + fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = + nicer_name (shorten x, i) (shorten y, j) + | nicer (Facts.Fact _) (Facts.Named _) = true + | nicer (Facts.Named _) (Facts.Fact _) = false; + in nicer end; + +fun rem_thm_dups nicer xs = + xs ~~ (1 upto length xs) + |> sort (TermOrd.fast_term_ord o pairself (Thm.prop_of o #2 o #1)) + |> rem_cdups nicer + |> sort (int_ord o pairself #2) + |> map #1; + +end; + + +(* print_theorems *) + +fun all_facts_of ctxt = + maps Facts.selections + (Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @ + Facts.dest_static [] (ProofContext.facts_of ctxt)); + +val limit = ref 40; + +fun find_theorems ctxt opt_goal rem_dups raw_criteria = + let + val add_prems = Seq.hd o (TRY (Method.insert_tac + (Assumption.prems_of ctxt) 1)); + val opt_goal' = Option.map add_prems opt_goal; + + val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; + val filters = map (filter_criterion ctxt opt_goal') criteria; + + val raw_matches = all_filters filters (all_facts_of ctxt); + + val matches = + if rem_dups + then rem_thm_dups (nicer_shortest ctxt) raw_matches + else raw_matches; + in matches end; + +fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = let + val start = start_timing (); + + val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; + val matches = find_theorems ctxt opt_goal rem_dups raw_criteria; + + val len = length matches; + val lim = the_default (! limit) opt_limit; + val thms = Library.drop (len - lim, matches); + + val end_msg = " in " ^ + (List.nth (String.tokens Char.isSpace (end_timing start), 3)) + ^ " secs" + in + Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) + :: Pretty.str "" :: + (if null thms then [Pretty.str ("nothing found" ^ end_msg)] + else + [Pretty.str ("found " ^ string_of_int len ^ " theorems" ^ + (if len <= lim then "" + else " (" ^ string_of_int lim ^ " displayed)") + ^ end_msg ^ ":"), Pretty.str ""] @ + map Display.pretty_fact thms) + |> Pretty.chunks |> Pretty.writeln + end; + + + +(** command syntax **) + +fun find_theorems_cmd ((opt_lim, rem_dups), spec) = + Toplevel.unknown_theory o Toplevel.keep (fn state => + let + val proof_state = Toplevel.enter_proof_body state; + val ctxt = Proof.context_of proof_state; + val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2); + in print_theorems ctxt opt_goal opt_lim rem_dups spec end); + +local + +structure P = OuterParse and K = OuterKeyword; + +val criterion = + P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name || + P.reserved "intro" >> K Intro || + P.reserved "elim" >> K Elim || + P.reserved "dest" >> K Dest || + P.reserved "solves" >> K Solves || + P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Simp || + P.term >> Pattern; + +val options = + Scan.optional + (P.$$$ "(" |-- + P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true + --| P.$$$ ")")) (NONE, true); +in + +val _ = + OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag + (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion)) + >> (Toplevel.no_timing oo find_theorems_cmd)); + +end; + +end;