# HG changeset patch # User blanchet # Date 1342035799 -7200 # Node ID 1065c307fafe15d33dc3f97afa9e7dd0c8eb5c59 # Parent 2bd242c56c90931f5cabd8d5f5555614e5ca3854 further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer) diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/IsaMakefile Wed Jul 11 21:43:19 2012 +0200 @@ -371,7 +371,10 @@ Tools/record.ML \ Tools/semiring_normalizer.ML \ Tools/Sledgehammer/async_manager.ML \ + Tools/Sledgehammer/sledgehammer_fact.ML \ Tools/Sledgehammer/sledgehammer_filter.ML \ + Tools/Sledgehammer/sledgehammer_filter_iter.ML \ + Tools/Sledgehammer/sledgehammer_filter_mash.ML \ Tools/Sledgehammer/sledgehammer_minimize.ML \ Tools/Sledgehammer/sledgehammer_isar.ML \ Tools/Sledgehammer/sledgehammer_provers.ML \ diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 11 21:43:19 2012 +0200 @@ -365,7 +365,7 @@ hd (#provers (Sledgehammer_Isar.default_params ctxt [])) handle List.Empty => error "No ATP available." fun get_prover name = - (name, Sledgehammer_Run.get_minimizing_prover ctxt + (name, Sledgehammer_Minimize.get_minimizing_prover ctxt Sledgehammer_Provers.Normal name) in (case AList.lookup (op =) args proverK of @@ -465,7 +465,7 @@ else raise Fail "inappropriate" val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name val facts = - Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override + Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts concl_t |> filter (is_appropriate_prop o prop_of o snd) |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Jul 11 21:43:19 2012 +0200 @@ -131,8 +131,8 @@ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover val facts = - Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override - chained_ths hyp_ts concl_t + Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override + chained_ths hyp_ts concl_t |> filter (is_appropriate_prop o prop_of o snd) |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds (the_default default_max_relevant max_relevant) diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Sledgehammer.thy Wed Jul 11 21:43:19 2012 +0200 @@ -11,8 +11,11 @@ keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl uses "Tools/Sledgehammer/async_manager.ML" "Tools/Sledgehammer/sledgehammer_util.ML" + "Tools/Sledgehammer/sledgehammer_fact.ML" + "Tools/Sledgehammer/sledgehammer_filter_iter.ML" + "Tools/Sledgehammer/sledgehammer_provers.ML" + "Tools/Sledgehammer/sledgehammer_filter_mash.ML" "Tools/Sledgehammer/sledgehammer_filter.ML" - "Tools/Sledgehammer/sledgehammer_provers.ML" "Tools/Sledgehammer/sledgehammer_minimize.ML" "Tools/Sledgehammer/sledgehammer_run.ML" "Tools/Sledgehammer/sledgehammer_isar.ML" diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200 @@ -18,7 +18,7 @@ *} ML {* -val do_it = true (* switch to "true" to generate the files *); +val do_it = false (* switch to "true" to generate the files *); val thy = @{theory Nat} *} diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/TPTP/MaSh_Import.thy --- a/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200 @@ -9,10 +9,6 @@ uses "mash_import.ML" begin -sledgehammer_params - [max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, - lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] - declare [[sledgehammer_instantiate_inducts]] ML {* @@ -20,13 +16,15 @@ *} ML {* -val do_it = false (* switch to "true" to generate the files *); +val do_it = true (* switch to "true" to generate the files *); val thy = @{theory List} *} ML {* -if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list" -else () +if do_it then + import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list" +else + () *} end diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/TPTP/ROOT.ML --- a/src/HOL/TPTP/ROOT.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/TPTP/ROOT.ML Wed Jul 11 21:43:19 2012 +0200 @@ -7,7 +7,6 @@ *) use_thys [ - "ATP_Theory_Export", "MaSh_Import", "TPTP_Interpret", "THF_Arith" diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 21:43:19 2012 +0200 @@ -61,8 +61,8 @@ fun all_facts_of_theory thy = let val ctxt = Proof_Context.init_global thy in - Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] [] - (Sledgehammer_Filter.clasimpset_rule_table_of ctxt) + Sledgehammer_Fact.all_facts ctxt false Symtab.empty true [] [] + (Sledgehammer_Fact.clasimpset_rule_table_of ctxt) |> rev (* try to restore the original order of facts, for MaSh *) end diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 11 21:43:19 2012 +0200 @@ -15,7 +15,7 @@ val theory_ord : theory * theory -> order val thm_ord : thm * thm -> order val dependencies_of : string list -> thm -> string list - val goal_of_thm : thm -> thm + val goal_of_thm : theory -> thm -> thm val meng_paulson_facts : Proof.context -> int -> thm -> (((unit -> string) * stature) * thm) list -> ((string * stature) * thm) list @@ -34,8 +34,9 @@ structure MaSh_Export : MASH_EXPORT = struct +open ATP_Util open ATP_Problem_Generate -open ATP_Util +open ATP_Theory_Export type prover_result = Sledgehammer_Provers.prover_result @@ -215,7 +216,7 @@ | freeze (Free (s, T)) = Free (s, freezeT T) | freeze t = t -val goal_of_thm = prop_of #> freeze #> cterm_of thy #> Goal.init +fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init fun meng_paulson_facts ctxt max_relevant goal = let @@ -241,7 +242,7 @@ {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, facts = facts |> map Sledgehammer_Provers.Untranslated_Fact} val prover = - Sledgehammer_Run.get_minimizing_prover ctxt + Sledgehammer_Minimize.get_minimizing_prover ctxt Sledgehammer_Provers.Normal (hd provers) in prover params (K (K (K ""))) problem end @@ -320,18 +321,25 @@ fun do_thm th = let val name = Thm.get_name_hint th - val goal = goal_of_thm th - val isa_deps = dependencies_of all_names th - val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) - val facts = - facts |> meng_paulson_facts ctxt (the max_relevant) goal - |> fold (add_isa_dep facts) isa_deps - |> map fix_name + val goal = goal_of_thm thy th val deps = - case run_sledgehammer ctxt facts goal of - {outcome = NONE, used_facts, ...} => - used_facts |> map fst |> sort string_ord - | _ => isa_deps + case dependencies_of all_names th of + [] => [] + | isa_dep as [_] => isa_dep (* can hardly beat that *) + | isa_deps => + let + val facts = + facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) + val facts = + facts |> meng_paulson_facts ctxt (the max_relevant) goal + |> fold (add_isa_dep facts) isa_deps + |> map fix_name + in + case run_sledgehammer ctxt facts goal of + {outcome = NONE, used_facts, ...} => + used_facts |> map fst |> sort string_ord + | _ => isa_deps + end val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" in File.append path s end in List.app do_thm ths end @@ -374,7 +382,7 @@ fun do_fact (fact as (_, th)) old_facts = let val name = Thm.get_name_hint th - val goal = goal_of_thm th + val goal = goal_of_thm thy th val kind = Thm.legacy_get_kind th val _ = if kind <> "" then diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/TPTP/mash_import.ML --- a/src/HOL/TPTP/mash_import.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/TPTP/mash_import.ML Wed Jul 11 21:43:19 2012 +0200 @@ -55,7 +55,7 @@ fun sugg_facts hyp_ts concl_t facts = map_filter (find_sugg facts o of_fact_name) #> take (max_relevant_slack * the max_relevant) - #> Sledgehammer_Filter.maybe_instantiate_inducts ctxt hyp_ts concl_t + #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t #> map (apfst (apfst (fn name => name ()))) fun meng_mash_facts fs1 fs2 = let @@ -106,7 +106,7 @@ SOME (_, th) => th | NONE => error ("No fact called \"" ^ name ^ "\"") val deps = dependencies_of all_names th - val goal = goal_of_thm th + val goal = goal_of_thm thy th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) val deps_facts = sugg_facts hyp_ts concl_t facts deps @@ -133,7 +133,7 @@ " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ Real.fmt (StringCvt.FIX (SOME 1)) (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" - val inst_inducts = Config.get ctxt Sledgehammer_Filter.instantiate_inducts + val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts val options = [prover_name, string_of_int (the max_relevant) ^ " facts", "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc, diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/TPTP/sledgehammer_tactics.ML --- a/src/HOL/TPTP/sledgehammer_tactics.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Wed Jul 11 21:43:19 2012 +0200 @@ -39,8 +39,8 @@ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers val facts = - Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override - chained_ths hyp_ts concl_t + Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override + chained_ths hyp_ts concl_t |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 11 21:43:19 2012 +0200 @@ -0,0 +1,439 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact.ML + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA + Author: Jasmin Blanchette, TU Muenchen + +Sledgehammer fact handling. +*) + +signature SLEDGEHAMMER_FACT = +sig + type status = ATP_Problem_Generate.status + type stature = ATP_Problem_Generate.stature + + type relevance_override = + {add : (Facts.ref * Attrib.src list) list, + del : (Facts.ref * Attrib.src list) list, + only : bool} + + val ignore_no_atp : bool Config.T + val instantiate_inducts : bool Config.T + val no_relevance_override : relevance_override + val fact_from_ref : + Proof.context -> unit Symtab.table -> thm list -> status Termtab.table + -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list + val all_facts : + Proof.context -> bool -> 'a Symtab.table -> bool -> thm list + -> thm list -> status Termtab.table + -> (((unit -> string) * stature) * thm) list + val clasimpset_rule_table_of : Proof.context -> status Termtab.table + val maybe_instantiate_inducts : + Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list + -> (((unit -> string) * 'a) * thm) list + val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list + val nearly_all_facts : + Proof.context -> bool -> relevance_override -> thm list -> term list -> term + -> (((unit -> string) * stature) * thm) list +end; + +structure Sledgehammer_Fact : SLEDGEHAMMER_FACT = +struct + +open ATP_Problem_Generate +open Metis_Tactic +open Sledgehammer_Util + +type relevance_override = + {add : (Facts.ref * Attrib.src list) list, + del : (Facts.ref * Attrib.src list) list, + only : bool} + +val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator + +(* experimental features *) +val ignore_no_atp = + Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false) +val instantiate_inducts = + Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false) + +val no_relevance_override = {add = [], del = [], only = false} + +fun needs_quoting reserved s = + Symtab.defined reserved s orelse + exists (not o Lexicon.is_identifier) (Long_Name.explode s) + +fun make_name reserved multi j name = + (name |> needs_quoting reserved name ? quote) ^ + (if multi then "(" ^ string_of_int j ^ ")" else "") + +fun explode_interval _ (Facts.FromTo (i, j)) = i upto j + | explode_interval max (Facts.From i) = i upto i + max - 1 + | explode_interval _ (Facts.Single i) = [i] + +val backquote = + raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`" + +(* unfolding these can yield really huge terms *) +val risky_defs = @{thms Bit0_def Bit1_def} + +fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs)) +fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t + | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2 + | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2 + | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2 + | is_rec_def _ = false + +fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms +fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths + +fun scope_of_thm global assms chained_ths th = + if is_chained chained_ths th then Chained + else if global then Global + else if is_assum assms th then Assum + else Local + +val may_be_induction = + exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) => + body_type T = @{typ bool} + | _ => false) + +fun status_of_thm css_table name th = + (* FIXME: use structured name *) + if (String.isSubstring ".induct" name orelse + String.isSubstring ".inducts" name) andalso + may_be_induction (prop_of th) then + Induction + else case Termtab.lookup css_table (prop_of th) of + SOME status => status + | NONE => General + +fun stature_of_thm global assms chained_ths css_table name th = + (scope_of_thm global assms chained_ths th, status_of_thm css_table name th) + +fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) = + let + val ths = Attrib.eval_thms ctxt [xthm] + val bracket = + map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args + |> implode + fun nth_name j = + case xref of + Facts.Fact s => backquote s ^ bracket + | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" + | Facts.Named ((name, _), NONE) => + make_name reserved (length ths > 1) (j + 1) name ^ bracket + | Facts.Named ((name, _), SOME intervals) => + make_name reserved true + (nth (maps (explode_interval (length ths)) intervals) j) name ^ + bracket + in + (ths, (0, [])) + |-> fold (fn th => fn (j, rest) => + let val name = nth_name j in + (j + 1, ((name, stature_of_thm false [] chained_ths + css_table name th), th) :: rest) + end) + |> snd + end + +(* Reject theorems with names like "List.filter.filter_list_def" or + "Accessible_Part.acc.defs", as these are definitions arising from packages. *) +fun is_package_def a = + let val names = Long_Name.explode a in + (length names > 2 andalso not (hd names = "local") andalso + String.isSuffix "_def" a) orelse String.isSuffix "_defs" a + end + +(* FIXME: put other record thms here, or declare as "no_atp" *) +fun multi_base_blacklist ctxt ho_atp = + ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", + "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", + "weak_case_cong"] + |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? + append ["induct", "inducts"] + |> map (prefix ".") + +val max_lambda_nesting = 3 (*only applies if not ho_atp*) + +fun term_has_too_many_lambdas max (t1 $ t2) = + exists (term_has_too_many_lambdas max) [t1, t2] + | term_has_too_many_lambdas max (Abs (_, _, t)) = + max = 0 orelse term_has_too_many_lambdas (max - 1) t + | term_has_too_many_lambdas _ _ = false + +(* Don't count nested lambdas at the level of formulas, since they are + quantifiers. *) +fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*) + | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) = + formula_has_too_many_lambdas false (T :: Ts) t + | formula_has_too_many_lambdas _ Ts t = + if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then + exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t)) + else + term_has_too_many_lambdas max_lambda_nesting t + +(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31) + was 11. *) +val max_apply_depth = 15 + +fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) + | apply_depth (Abs (_, _, t)) = apply_depth t + | apply_depth _ = 0 + +fun is_formula_too_complex ho_atp t = + apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t + +(* FIXME: Extend to "Meson" and "Metis" *) +val exists_sledgehammer_const = + exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) + +(* FIXME: make more reliable *) +val exists_low_level_class_const = + exists_Const (fn (s, _) => + s = @{const_name equal_class.equal} orelse + String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s) + +fun is_metastrange_theorem th = + case head_of (concl_of th) of + Const (s, _) => (s <> @{const_name Trueprop} andalso + s <> @{const_name "=="}) + | _ => false + +fun is_that_fact th = + String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th) + andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN + | _ => false) (prop_of th) + +fun is_theorem_bad_for_atps ho_atp exporter thm = + is_metastrange_theorem thm orelse + (not exporter andalso + let val t = prop_of thm in + is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse + exists_sledgehammer_const t orelse exists_low_level_class_const t orelse + is_that_fact thm + end) + +fun hackish_string_for_term ctxt t = + Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) + (print_mode_value ())) (Syntax.string_of_term ctxt) t + |> String.translate (fn c => if Char.isPrint c then str c else "") + |> simplify_spaces + +(* This is a terrible hack. Free variables are sometimes coded as "M__" when + they are displayed as "M" and we want to avoid clashes with these. But + sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all + prefixes of all free variables. In the worse case scenario, where the fact + won't be resolved correctly, the user can fix it manually, e.g., by naming + the fact in question. Ideally we would need nothing of it, but backticks + simply don't work with schematic variables. *) +fun all_prefixes_of s = + map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1) + +fun close_form t = + (t, [] |> Term.add_free_names t |> maps all_prefixes_of) + |> fold (fn ((s, i), T) => fn (t', taken) => + let val s' = singleton (Name.variant_list taken) s in + ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const + else Logic.all_const) T + $ Abs (s', T, abstract_over (Var ((s, i), T), t')), + s' :: taken) + end) + (Term.add_vars t [] |> sort_wrt (fst o fst)) + |> fst + +fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table = + let + val thy = Proof_Context.theory_of ctxt + val global_facts = Global_Theory.facts_of thy + val local_facts = Proof_Context.facts_of ctxt + val named_locals = local_facts |> Facts.dest_static [] + val assms = Assumption.all_assms_of ctxt + fun is_good_unnamed_local th = + not (Thm.has_name_hint th) andalso + forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals + val unnamed_locals = + union Thm.eq_thm_prop (Facts.props local_facts) chained_ths + |> filter is_good_unnamed_local |> map (pair "" o single) + val full_space = + Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) + fun add_facts global foldx facts = + foldx (fn (name0, ths) => + if not exporter andalso name0 <> "" andalso + forall (not o member Thm.eq_thm_prop add_ths) ths andalso + (Facts.is_concealed facts name0 orelse + (not (Config.get ctxt ignore_no_atp) andalso + is_package_def name0) orelse + exists (fn s => String.isSuffix s name0) + (multi_base_blacklist ctxt ho_atp)) then + I + else + let + val multi = length ths > 1 + val backquote_thm = + backquote o hackish_string_for_term ctxt o close_form o prop_of + fun check_thms a = + case try (Proof_Context.get_thms ctxt) a of + NONE => false + | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths') + in + pair 1 + #> fold (fn th => fn (j, (multis, unis)) => + (j + 1, + if not (member Thm.eq_thm_prop add_ths th) andalso + is_theorem_bad_for_atps ho_atp exporter th then + (multis, unis) + else + let + val new = + (((fn () => + if name0 = "" then + th |> backquote_thm + else + [Facts.extern ctxt facts name0, + Name_Space.extern ctxt full_space name0, + name0] + |> find_first check_thms + |> (fn SOME name => + make_name reserved multi j name + | NONE => "")), + stature_of_thm global assms chained_ths + css_table name0 th), th) + in + if multi then (new :: multis, unis) + else (multis, new :: unis) + end)) ths + #> snd + end) + in + (* The single-name theorems go after the multiple-name ones, so that single + names are preferred when both are available. *) + ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals) + |> add_facts true Facts.fold_static global_facts global_facts + |> op @ + end + +fun clasimpset_rule_table_of ctxt = + let + val thy = Proof_Context.theory_of ctxt + val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy + fun add stature normalizers get_th = + fold (fn rule => + let + val th = rule |> get_th + val t = + th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of + in + fold (fn normalize => Termtab.update (normalize t, stature)) + (I :: normalizers) + end) + val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = + ctxt |> claset_of |> Classical.rep_cs + val intros = Item_Net.content safeIs @ Item_Net.content hazIs +(* Add once it is used: + val elims = + Item_Net.content safeEs @ Item_Net.content hazEs + |> map Classical.classical_rule +*) + val simps = ctxt |> simpset_of |> dest_ss |> #simps + val specs = ctxt |> Spec_Rules.get + val (rec_defs, nonrec_defs) = + specs |> filter (curry (op =) Spec_Rules.Equational o fst) + |> maps (snd o snd) + |> filter_out (member Thm.eq_thm_prop risky_defs) + |> List.partition (is_rec_def o prop_of) + val spec_intros = + specs |> filter (member (op =) [Spec_Rules.Inductive, + Spec_Rules.Co_Inductive] o fst) + |> maps (snd o snd) + in + Termtab.empty |> add Simp [atomize] snd simps + |> add Simp [] I rec_defs + |> add Def [] I nonrec_defs +(* Add once it is used: + |> add Elim [] I elims +*) + |> add Intro [] I intros + |> add Inductive [] I spec_intros + end + +fun uniquify xs = + Termtab.fold (cons o snd) + (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) [] + +fun struct_induct_rule_on th = + case Logic.strip_horn (prop_of th) of + (prems, @{const Trueprop} + $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => + if not (is_TVar ind_T) andalso length prems > 1 andalso + exists (exists_subterm (curry (op aconv) p)) prems andalso + not (exists (exists_subterm (curry (op aconv) a)) prems) then + SOME (p_name, ind_T) + else + NONE + | _ => NONE + +fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x = + let + fun varify_noninducts (t as Free (s, T)) = + if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T) + | varify_noninducts t = t + val p_inst = + concl_prop |> map_aterms varify_noninducts |> close_form + |> lambda (Free ind_x) + |> hackish_string_for_term ctxt + in + ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", + stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)]) + end + +fun type_match thy (T1, T2) = + (Sign.typ_match thy (T2, T1) Vartab.empty; true) + handle Type.TYPE_MATCH => false + +fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) = + case struct_induct_rule_on th of + SOME (p_name, ind_T) => + let val thy = Proof_Context.theory_of ctxt in + stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T)) + |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax)) + end + | NONE => [ax] + +fun external_frees t = + [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) + +fun maybe_instantiate_inducts ctxt hyp_ts concl_t = + if Config.get ctxt instantiate_inducts then + let + val thy = Proof_Context.theory_of ctxt + val ind_stmt = + (hyp_ts |> filter_out (null o external_frees), concl_t) + |> Logic.list_implies |> Object_Logic.atomize_term thy + val ind_stmt_xs = external_frees ind_stmt + in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end + else + I + +fun maybe_filter_no_atps ctxt = + not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd) + +fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override) + chained_ths hyp_ts concl_t = + if only andalso null add then + [] + else + let + val reserved = reserved_isar_keyword_table () + val add_ths = Attrib.eval_thms ctxt add + val css_table = clasimpset_rule_table_of ctxt + in + (if only then + maps (map (fn ((name, stature), th) => ((K name, stature), th)) + o fact_from_ref ctxt reserved chained_ths css_table) add + else + all_facts ctxt ho_atp reserved false add_ths chained_ths css_table) + |> maybe_instantiate_inducts ctxt hyp_ts concl_t + |> not only ? maybe_filter_no_atps ctxt + |> uniquify + end + +end; diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Jul 11 21:43:19 2012 +0200 @@ -7,27 +7,10 @@ signature SLEDGEHAMMER_FILTER = sig - type status = ATP_Problem_Generate.status type stature = ATP_Problem_Generate.stature type relevance_fudge = Sledgehammer_Filter_Iter.relevance_fudge type relevance_override = Sledgehammer_Filter_Iter.relevance_override - val no_relevance_override : relevance_override - val fact_from_ref : - Proof.context -> unit Symtab.table -> thm list -> status Termtab.table - -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list - val all_facts : - Proof.context -> bool -> 'a Symtab.table -> bool -> thm list - -> thm list -> status Termtab.table - -> (((unit -> string) * stature) * thm) list - val clasimpset_rule_table_of : Proof.context -> status Termtab.table - val maybe_instantiate_inducts : - Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list - -> (((unit -> string) * 'a) * thm) list - val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list - val nearly_all_facts : - Proof.context -> bool -> relevance_override -> thm list -> term list -> term - -> (((unit -> string) * stature) * thm) list val relevant_facts : Proof.context -> real * real -> int -> (string * typ -> term list -> bool * term list) -> relevance_fudge @@ -39,394 +22,8 @@ structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER = struct -open ATP_Problem_Generate -open Metis_Tactic -open Sledgehammer_Util open Sledgehammer_Filter_Iter -val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator - -val no_relevance_override = {add = [], del = [], only = false} - -fun needs_quoting reserved s = - Symtab.defined reserved s orelse - exists (not o Lexicon.is_identifier) (Long_Name.explode s) - -fun make_name reserved multi j name = - (name |> needs_quoting reserved name ? quote) ^ - (if multi then "(" ^ string_of_int j ^ ")" else "") - -fun explode_interval _ (Facts.FromTo (i, j)) = i upto j - | explode_interval max (Facts.From i) = i upto i + max - 1 - | explode_interval _ (Facts.Single i) = [i] - -val backquote = - raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`" - -(* unfolding these can yield really huge terms *) -val risky_defs = @{thms Bit0_def Bit1_def} - -fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs)) -fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t - | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2 - | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2 - | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2 - | is_rec_def _ = false - -fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms -fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths - -fun scope_of_thm global assms chained_ths th = - if is_chained chained_ths th then Chained - else if global then Global - else if is_assum assms th then Assum - else Local - -val may_be_induction = - exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) => - body_type T = @{typ bool} - | _ => false) - -fun status_of_thm css_table name th = - (* FIXME: use structured name *) - if (String.isSubstring ".induct" name orelse - String.isSubstring ".inducts" name) andalso - may_be_induction (prop_of th) then - Induction - else case Termtab.lookup css_table (prop_of th) of - SOME status => status - | NONE => General - -fun stature_of_thm global assms chained_ths css_table name th = - (scope_of_thm global assms chained_ths th, status_of_thm css_table name th) - -fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) = - let - val ths = Attrib.eval_thms ctxt [xthm] - val bracket = - map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args - |> implode - fun nth_name j = - case xref of - Facts.Fact s => backquote s ^ bracket - | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" - | Facts.Named ((name, _), NONE) => - make_name reserved (length ths > 1) (j + 1) name ^ bracket - | Facts.Named ((name, _), SOME intervals) => - make_name reserved true - (nth (maps (explode_interval (length ths)) intervals) j) name ^ - bracket - in - (ths, (0, [])) - |-> fold (fn th => fn (j, rest) => - let val name = nth_name j in - (j + 1, ((name, stature_of_thm false [] chained_ths - css_table name th), th) :: rest) - end) - |> snd - end - -(*Reject theorems with names like "List.filter.filter_list_def" or - "Accessible_Part.acc.defs", as these are definitions arising from packages.*) -fun is_package_def a = - let val names = Long_Name.explode a in - (length names > 2 andalso not (hd names = "local") andalso - String.isSuffix "_def" a) orelse String.isSuffix "_defs" a - end - -(* FIXME: put other record thms here, or declare as "no_atp" *) -fun multi_base_blacklist ctxt ho_atp = - ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", - "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", - "weak_case_cong"] - |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? - append ["induct", "inducts"] - |> map (prefix ".") - -val max_lambda_nesting = 3 (*only applies if not ho_atp*) - -fun term_has_too_many_lambdas max (t1 $ t2) = - exists (term_has_too_many_lambdas max) [t1, t2] - | term_has_too_many_lambdas max (Abs (_, _, t)) = - max = 0 orelse term_has_too_many_lambdas (max - 1) t - | term_has_too_many_lambdas _ _ = false - -(* Don't count nested lambdas at the level of formulas, since they are - quantifiers. *) -fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*) - | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) = - formula_has_too_many_lambdas false (T :: Ts) t - | formula_has_too_many_lambdas _ Ts t = - if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then - exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t)) - else - term_has_too_many_lambdas max_lambda_nesting t - -(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31) - was 11. *) -val max_apply_depth = 15 - -fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1) - | apply_depth (Abs (_, _, t)) = apply_depth t - | apply_depth _ = 0 - -fun is_formula_too_complex ho_atp t = - apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t - -(* FIXME: Extend to "Meson" and "Metis" *) -val exists_sledgehammer_const = - exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) - -(* FIXME: make more reliable *) -val exists_low_level_class_const = - exists_Const (fn (s, _) => - s = @{const_name equal_class.equal} orelse - String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s) - -fun is_metastrange_theorem th = - case head_of (concl_of th) of - Const (s, _) => (s <> @{const_name Trueprop} andalso - s <> @{const_name "=="}) - | _ => false - -fun is_that_fact th = - String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th) - andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN - | _ => false) (prop_of th) - -fun is_theorem_bad_for_atps ho_atp exporter thm = - is_metastrange_theorem thm orelse - (not exporter andalso - let val t = prop_of thm in - is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse - exists_sledgehammer_const t orelse exists_low_level_class_const t orelse - is_that_fact thm - end) - -fun string_for_term ctxt t = - Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) - (print_mode_value ())) (Syntax.string_of_term ctxt) t - |> String.translate (fn c => if Char.isPrint c then str c else "") - |> simplify_spaces - -(* This is a terrible hack. Free variables are sometimes coded as "M__" when - they are displayed as "M" and we want to avoid clashes with these. But - sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all - prefixes of all free variables. In the worse case scenario, where the fact - won't be resolved correctly, the user can fix it manually, e.g., by naming - the fact in question. Ideally we would need nothing of it, but backticks - simply don't work with schematic variables. *) -fun all_prefixes_of s = - map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1) - -fun close_form t = - (t, [] |> Term.add_free_names t |> maps all_prefixes_of) - |> fold (fn ((s, i), T) => fn (t', taken) => - let val s' = singleton (Name.variant_list taken) s in - ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const - else Logic.all_const) T - $ Abs (s', T, abstract_over (Var ((s, i), T), t')), - s' :: taken) - end) - (Term.add_vars t [] |> sort_wrt (fst o fst)) - |> fst - -fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table = - let - val thy = Proof_Context.theory_of ctxt - val global_facts = Global_Theory.facts_of thy - val local_facts = Proof_Context.facts_of ctxt - val named_locals = local_facts |> Facts.dest_static [] - val assms = Assumption.all_assms_of ctxt - fun is_good_unnamed_local th = - not (Thm.has_name_hint th) andalso - forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals - val unnamed_locals = - union Thm.eq_thm_prop (Facts.props local_facts) chained_ths - |> filter is_good_unnamed_local |> map (pair "" o single) - val full_space = - Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) - fun add_facts global foldx facts = - foldx (fn (name0, ths) => - if not exporter andalso name0 <> "" andalso - forall (not o member Thm.eq_thm_prop add_ths) ths andalso - (Facts.is_concealed facts name0 orelse - (not (Config.get ctxt ignore_no_atp) andalso - is_package_def name0) orelse - exists (fn s => String.isSuffix s name0) - (multi_base_blacklist ctxt ho_atp)) then - I - else - let - val multi = length ths > 1 - val backquote_thm = - backquote o string_for_term ctxt o close_form o prop_of - fun check_thms a = - case try (Proof_Context.get_thms ctxt) a of - NONE => false - | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths') - in - pair 1 - #> fold (fn th => fn (j, (multis, unis)) => - (j + 1, - if not (member Thm.eq_thm_prop add_ths th) andalso - is_theorem_bad_for_atps ho_atp exporter th then - (multis, unis) - else - let - val new = - (((fn () => - if name0 = "" then - th |> backquote_thm - else - [Facts.extern ctxt facts name0, - Name_Space.extern ctxt full_space name0, - name0] - |> find_first check_thms - |> (fn SOME name => - make_name reserved multi j name - | NONE => "")), - stature_of_thm global assms chained_ths - css_table name0 th), th) - in - if multi then (new :: multis, unis) - else (multis, new :: unis) - end)) ths - #> snd - end) - in - (* The single-name theorems go after the multiple-name ones, so that single - names are preferred when both are available. *) - ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals) - |> add_facts true Facts.fold_static global_facts global_facts - |> op @ - end - -fun clasimpset_rule_table_of ctxt = - let - val thy = Proof_Context.theory_of ctxt - val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy - fun add stature normalizers get_th = - fold (fn rule => - let - val th = rule |> get_th - val t = - th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of - in - fold (fn normalize => Termtab.update (normalize t, stature)) - (I :: normalizers) - end) - val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = - ctxt |> claset_of |> Classical.rep_cs - val intros = Item_Net.content safeIs @ Item_Net.content hazIs -(* Add once it is used: - val elims = - Item_Net.content safeEs @ Item_Net.content hazEs - |> map Classical.classical_rule -*) - val simps = ctxt |> simpset_of |> dest_ss |> #simps - val specs = ctxt |> Spec_Rules.get - val (rec_defs, nonrec_defs) = - specs |> filter (curry (op =) Spec_Rules.Equational o fst) - |> maps (snd o snd) - |> filter_out (member Thm.eq_thm_prop risky_defs) - |> List.partition (is_rec_def o prop_of) - val spec_intros = - specs |> filter (member (op =) [Spec_Rules.Inductive, - Spec_Rules.Co_Inductive] o fst) - |> maps (snd o snd) - in - Termtab.empty |> add Simp [atomize] snd simps - |> add Simp [] I rec_defs - |> add Def [] I nonrec_defs -(* Add once it is used: - |> add Elim [] I elims -*) - |> add Intro [] I intros - |> add Inductive [] I spec_intros - end - -fun uniquify xs = - Termtab.fold (cons o snd) - (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) [] - -fun struct_induct_rule_on th = - case Logic.strip_horn (prop_of th) of - (prems, @{const Trueprop} - $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) => - if not (is_TVar ind_T) andalso length prems > 1 andalso - exists (exists_subterm (curry (op aconv) p)) prems andalso - not (exists (exists_subterm (curry (op aconv) a)) prems) then - SOME (p_name, ind_T) - else - NONE - | _ => NONE - -fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x = - let - fun varify_noninducts (t as Free (s, T)) = - if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T) - | varify_noninducts t = t - val p_inst = - concl_prop |> map_aterms varify_noninducts |> close_form - |> lambda (Free ind_x) - |> string_for_term ctxt - in - ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", - stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)]) - end - -fun type_match thy (T1, T2) = - (Sign.typ_match thy (T2, T1) Vartab.empty; true) - handle Type.TYPE_MATCH => false - -fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) = - case struct_induct_rule_on th of - SOME (p_name, ind_T) => - let val thy = Proof_Context.theory_of ctxt in - stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T)) - |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax)) - end - | NONE => [ax] - -fun external_frees t = - [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) - -fun maybe_instantiate_inducts ctxt hyp_ts concl_t = - if Config.get ctxt instantiate_inducts then - let - val thy = Proof_Context.theory_of ctxt - val ind_stmt = - (hyp_ts |> filter_out (null o external_frees), concl_t) - |> Logic.list_implies |> Object_Logic.atomize_term thy - val ind_stmt_xs = external_frees ind_stmt - in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end - else - I - -fun maybe_filter_no_atps ctxt = - not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd) - -fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override) - chained_ths hyp_ts concl_t = - if only andalso null add then - [] - else - let - val reserved = reserved_isar_keyword_table () - val add_ths = Attrib.eval_thms ctxt add - val css_table = clasimpset_rule_table_of ctxt - in - (if only then - maps (map (fn ((name, stature), th) => ((K name, stature), th)) - o fact_from_ref ctxt reserved chained_ths css_table) add - else - all_facts ctxt ho_atp reserved false add_ths chained_ths css_table) - |> maybe_instantiate_inducts ctxt hyp_ts concl_t - |> not only ? maybe_filter_no_atps ctxt - |> uniquify - end - val relevant_facts = iterative_relevant_facts end; diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 11 21:43:19 2012 +0200 @@ -8,6 +8,7 @@ signature SLEDGEHAMMER_FILTER_ITER = sig type stature = ATP_Problem_Generate.stature + type relevance_override = Sledgehammer_Fact.relevance_override type relevance_fudge = {local_const_multiplier : real, @@ -30,14 +31,7 @@ threshold_divisor : real, ridiculous_threshold : real} - type relevance_override = - {add : (Facts.ref * Attrib.src list) list, - del : (Facts.ref * Attrib.src list) list, - only : bool} - val trace : bool Config.T - val ignore_no_atp : bool Config.T - val instantiate_inducts : bool Config.T val pseudo_abs_name : string val pseudo_skolem_prefix : string val const_names_in_fact : @@ -55,17 +49,12 @@ struct open ATP_Problem_Generate +open Sledgehammer_Fact val trace = Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false) fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () -(* experimental features *) -val ignore_no_atp = - Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false) -val instantiate_inducts = - Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false) - type relevance_fudge = {local_const_multiplier : real, worse_irrel_freq : real, @@ -87,11 +76,6 @@ threshold_divisor : real, ridiculous_threshold : real} -type relevance_override = - {add : (Facts.ref * Attrib.src list) list, - del : (Facts.ref * Attrib.src list) list, - only : bool} - val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator val pseudo_abs_name = sledgehammer_prefix ^ "abs" val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko" diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 11 21:43:19 2012 +0200 @@ -23,7 +23,7 @@ open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util -open Sledgehammer_Filter +open Sledgehammer_Fact open Sledgehammer_Provers open Sledgehammer_Minimize open Sledgehammer_Run diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 11 21:43:19 2012 +0200 @@ -9,14 +9,19 @@ sig type stature = ATP_Problem_Generate.stature type play = ATP_Proof_Reconstruct.play + type mode = Sledgehammer_Provers.mode type params = Sledgehammer_Provers.params + type prover = Sledgehammer_Provers.prover val binary_min_facts : int Config.T + val auto_minimize_min_facts : int Config.T + val auto_minimize_max_time : real Config.T val minimize_facts : string -> params -> bool -> int -> int -> Proof.state -> ((string * stature) * thm list) list -> ((string * stature) * thm list) list option * ((unit -> play) * (play -> string) * string) + val get_minimizing_prover : Proof.context -> mode -> string -> prover val run_minimize : params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit end; @@ -29,7 +34,7 @@ open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util -open Sledgehammer_Filter +open Sledgehammer_Fact open Sledgehammer_Provers (* wrapper for calling external prover *) @@ -107,6 +112,12 @@ val binary_min_facts = Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts} (K 20) +val auto_minimize_min_facts = + Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} + (fn generic => Config.get_generic generic binary_min_facts) +val auto_minimize_max_time = + Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} + (K 5.0) fun linear_minimize test timeout result xs = let @@ -212,6 +223,106 @@ (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, "")) end +fun adjust_reconstructor_params override_params + ({debug, verbose, overlord, blocking, provers, type_enc, strict, + lam_trans, uncurried_aliases, relevance_thresholds, max_relevant, + max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor, + slice, minimize, timeout, preplay_timeout, expect} : params) = + let + fun lookup_override name default_value = + case AList.lookup (op =) override_params name of + SOME [s] => SOME s + | _ => default_value + (* Only those options that reconstructors are interested in are considered + here. *) + val type_enc = lookup_override "type_enc" type_enc + val lam_trans = lookup_override "lam_trans" lam_trans + in + {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, + provers = provers, type_enc = type_enc, strict = strict, + lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, + max_relevant = max_relevant, relevance_thresholds = relevance_thresholds, + max_mono_iters = max_mono_iters, + max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, + isar_shrink_factor = isar_shrink_factor, slice = slice, + minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, + expect = expect} + end + +fun minimize ctxt mode name + (params as {debug, verbose, isar_proof, minimize, ...}) + ({state, subgoal, subgoal_count, facts, ...} : prover_problem) + (result as {outcome, used_facts, run_time, preplay, message, + message_tail} : prover_result) = + if is_some outcome orelse null used_facts then + result + else + let + val num_facts = length used_facts + val ((perhaps_minimize, (minimize_name, params)), preplay) = + if mode = Normal then + if num_facts >= Config.get ctxt auto_minimize_min_facts then + ((true, (name, params)), preplay) + else + let + fun can_min_fast_enough time = + 0.001 + * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time) + <= Config.get ctxt auto_minimize_max_time + fun prover_fast_enough () = can_min_fast_enough run_time + in + if isar_proof then + ((prover_fast_enough (), (name, params)), preplay) + else + let val preplay = preplay () in + (case preplay of + Played (reconstr, timeout) => + if can_min_fast_enough timeout then + (true, extract_reconstructor params reconstr + ||> (fn override_params => + adjust_reconstructor_params + override_params params)) + else + (prover_fast_enough (), (name, params)) + | _ => (prover_fast_enough (), (name, params)), + K preplay) + end + end + else + ((false, (name, params)), preplay) + val minimize = minimize |> the_default perhaps_minimize + val (used_facts, (preplay, message, _)) = + if minimize then + minimize_facts minimize_name params (not verbose) subgoal + subgoal_count state + (filter_used_facts used_facts + (map (apsnd single o untranslated_fact) facts)) + |>> Option.map (map fst) + else + (SOME used_facts, (preplay, message, "")) + in + case used_facts of + SOME used_facts => + (if debug andalso not (null used_facts) then + facts ~~ (0 upto length facts - 1) + |> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j)) + |> filter_used_facts used_facts + |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) + |> commas + |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ + " proof (of " ^ string_of_int (length facts) ^ "): ") "." + |> Output.urgent_message + else + (); + {outcome = NONE, used_facts = used_facts, run_time = run_time, + preplay = preplay, message = message, message_tail = message_tail}) + | NONE => result + end + +fun get_minimizing_prover ctxt mode name params minimize_command problem = + get_prover ctxt mode name params minimize_command problem + |> minimize ctxt mode name params problem + fun run_minimize (params as {provers, ...}) i refs state = let val ctxt = Proof.context_of state diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 11 21:43:19 2012 +0200 @@ -14,7 +14,7 @@ type reconstructor = ATP_Proof_Reconstruct.reconstructor type play = ATP_Proof_Reconstruct.play type minimize_command = ATP_Proof_Reconstruct.minimize_command - type relevance_fudge = Sledgehammer_Filter.relevance_fudge + type relevance_fudge = Sledgehammer_Filter_Iter.relevance_fudge datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize @@ -124,7 +124,7 @@ open ATP_Proof_Reconstruct open Metis_Tactic open Sledgehammer_Util -open Sledgehammer_Filter +open Sledgehammer_Filter_Iter (** The Sledgehammer **) diff -r 2bd242c56c90 -r 1065c307fafe src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 11 21:43:19 2012 +0200 @@ -12,15 +12,11 @@ type relevance_override = Sledgehammer_Filter.relevance_override type mode = Sledgehammer_Provers.mode type params = Sledgehammer_Provers.params - type prover = Sledgehammer_Provers.prover val someN : string val noneN : string val timeoutN : string val unknownN : string - val auto_minimize_min_facts : int Config.T - val auto_minimize_max_time : real Config.T - val get_minimizing_prover : Proof.context -> mode -> string -> prover val run_sledgehammer : params -> mode -> int -> relevance_override -> ((string * string list) list -> string -> minimize_command) @@ -34,9 +30,10 @@ open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util -open Sledgehammer_Filter +open Sledgehammer_Fact open Sledgehammer_Provers open Sledgehammer_Minimize +open Sledgehammer_Filter val someN = "some" val noneN = "none" @@ -65,113 +62,6 @@ (if blocking then "." else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) -val auto_minimize_min_facts = - Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} - (fn generic => Config.get_generic generic binary_min_facts) -val auto_minimize_max_time = - Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} - (K 5.0) - -fun adjust_reconstructor_params override_params - ({debug, verbose, overlord, blocking, provers, type_enc, strict, - lam_trans, uncurried_aliases, relevance_thresholds, max_relevant, - max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor, - slice, minimize, timeout, preplay_timeout, expect} : params) = - let - fun lookup_override name default_value = - case AList.lookup (op =) override_params name of - SOME [s] => SOME s - | _ => default_value - (* Only those options that reconstructors are interested in are considered - here. *) - val type_enc = lookup_override "type_enc" type_enc - val lam_trans = lookup_override "lam_trans" lam_trans - in - {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, - provers = provers, type_enc = type_enc, strict = strict, - lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, - max_relevant = max_relevant, relevance_thresholds = relevance_thresholds, - max_mono_iters = max_mono_iters, - max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, - isar_shrink_factor = isar_shrink_factor, slice = slice, - minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, - expect = expect} - end - -fun minimize ctxt mode name - (params as {debug, verbose, isar_proof, minimize, ...}) - ({state, subgoal, subgoal_count, facts, ...} : prover_problem) - (result as {outcome, used_facts, run_time, preplay, message, - message_tail} : prover_result) = - if is_some outcome orelse null used_facts then - result - else - let - val num_facts = length used_facts - val ((perhaps_minimize, (minimize_name, params)), preplay) = - if mode = Normal then - if num_facts >= Config.get ctxt auto_minimize_min_facts then - ((true, (name, params)), preplay) - else - let - fun can_min_fast_enough time = - 0.001 - * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time) - <= Config.get ctxt auto_minimize_max_time - fun prover_fast_enough () = can_min_fast_enough run_time - in - if isar_proof then - ((prover_fast_enough (), (name, params)), preplay) - else - let val preplay = preplay () in - (case preplay of - Played (reconstr, timeout) => - if can_min_fast_enough timeout then - (true, extract_reconstructor params reconstr - ||> (fn override_params => - adjust_reconstructor_params - override_params params)) - else - (prover_fast_enough (), (name, params)) - | _ => (prover_fast_enough (), (name, params)), - K preplay) - end - end - else - ((false, (name, params)), preplay) - val minimize = minimize |> the_default perhaps_minimize - val (used_facts, (preplay, message, _)) = - if minimize then - minimize_facts minimize_name params (not verbose) subgoal - subgoal_count state - (filter_used_facts used_facts - (map (apsnd single o untranslated_fact) facts)) - |>> Option.map (map fst) - else - (SOME used_facts, (preplay, message, "")) - in - case used_facts of - SOME used_facts => - (if debug andalso not (null used_facts) then - facts ~~ (0 upto length facts - 1) - |> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j)) - |> filter_used_facts used_facts - |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) - |> commas - |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ - " proof (of " ^ string_of_int (length facts) ^ "): ") "." - |> Output.urgent_message - else - (); - {outcome = NONE, used_facts = used_facts, run_time = run_time, - preplay = preplay, message = message, message_tail = message_tail}) - | NONE => result - end - -fun get_minimizing_prover ctxt mode name params minimize_command problem = - get_prover ctxt mode name params minimize_command problem - |> minimize ctxt mode name params problem - fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice, timeout, expect, ...}) mode minimize_command only {state, goal, subgoal, subgoal_count, facts}