further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
1.1 --- a/src/HOL/IsaMakefile Wed Jul 11 21:43:19 2012 +0200
1.2 +++ b/src/HOL/IsaMakefile Wed Jul 11 21:43:19 2012 +0200
1.3 @@ -371,7 +371,10 @@
1.4 Tools/record.ML \
1.5 Tools/semiring_normalizer.ML \
1.6 Tools/Sledgehammer/async_manager.ML \
1.7 + Tools/Sledgehammer/sledgehammer_fact.ML \
1.8 Tools/Sledgehammer/sledgehammer_filter.ML \
1.9 + Tools/Sledgehammer/sledgehammer_filter_iter.ML \
1.10 + Tools/Sledgehammer/sledgehammer_filter_mash.ML \
1.11 Tools/Sledgehammer/sledgehammer_minimize.ML \
1.12 Tools/Sledgehammer/sledgehammer_isar.ML \
1.13 Tools/Sledgehammer/sledgehammer_provers.ML \
2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 11 21:43:19 2012 +0200
2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 11 21:43:19 2012 +0200
2.3 @@ -365,7 +365,7 @@
2.4 hd (#provers (Sledgehammer_Isar.default_params ctxt []))
2.5 handle List.Empty => error "No ATP available."
2.6 fun get_prover name =
2.7 - (name, Sledgehammer_Run.get_minimizing_prover ctxt
2.8 + (name, Sledgehammer_Minimize.get_minimizing_prover ctxt
2.9 Sledgehammer_Provers.Normal name)
2.10 in
2.11 (case AList.lookup (op =) args proverK of
2.12 @@ -465,7 +465,7 @@
2.13 else raise Fail "inappropriate"
2.14 val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
2.15 val facts =
2.16 - Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
2.17 + Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
2.18 chained_ths hyp_ts concl_t
2.19 |> filter (is_appropriate_prop o prop_of o snd)
2.20 |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Jul 11 21:43:19 2012 +0200
3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Jul 11 21:43:19 2012 +0200
3.3 @@ -131,8 +131,8 @@
3.4 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
3.5 val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
3.6 val facts =
3.7 - Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
3.8 - chained_ths hyp_ts concl_t
3.9 + Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
3.10 + chained_ths hyp_ts concl_t
3.11 |> filter (is_appropriate_prop o prop_of o snd)
3.12 |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
3.13 (the_default default_max_relevant max_relevant)
4.1 --- a/src/HOL/Sledgehammer.thy Wed Jul 11 21:43:19 2012 +0200
4.2 +++ b/src/HOL/Sledgehammer.thy Wed Jul 11 21:43:19 2012 +0200
4.3 @@ -11,8 +11,11 @@
4.4 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
4.5 uses "Tools/Sledgehammer/async_manager.ML"
4.6 "Tools/Sledgehammer/sledgehammer_util.ML"
4.7 + "Tools/Sledgehammer/sledgehammer_fact.ML"
4.8 + "Tools/Sledgehammer/sledgehammer_filter_iter.ML"
4.9 + "Tools/Sledgehammer/sledgehammer_provers.ML"
4.10 + "Tools/Sledgehammer/sledgehammer_filter_mash.ML"
4.11 "Tools/Sledgehammer/sledgehammer_filter.ML"
4.12 - "Tools/Sledgehammer/sledgehammer_provers.ML"
4.13 "Tools/Sledgehammer/sledgehammer_minimize.ML"
4.14 "Tools/Sledgehammer/sledgehammer_run.ML"
4.15 "Tools/Sledgehammer/sledgehammer_isar.ML"
5.1 --- a/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200
5.2 +++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200
5.3 @@ -18,7 +18,7 @@
5.4 *}
5.5
5.6 ML {*
5.7 -val do_it = true (* switch to "true" to generate the files *);
5.8 +val do_it = false (* switch to "true" to generate the files *);
5.9 val thy = @{theory Nat}
5.10 *}
5.11
6.1 --- a/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200
6.2 +++ b/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200
6.3 @@ -9,10 +9,6 @@
6.4 uses "mash_import.ML"
6.5 begin
6.6
6.7 -sledgehammer_params
6.8 - [max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
6.9 - lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
6.10 -
6.11 declare [[sledgehammer_instantiate_inducts]]
6.12
6.13 ML {*
6.14 @@ -20,13 +16,15 @@
6.15 *}
6.16
6.17 ML {*
6.18 -val do_it = false (* switch to "true" to generate the files *);
6.19 +val do_it = true (* switch to "true" to generate the files *);
6.20 val thy = @{theory List}
6.21 *}
6.22
6.23 ML {*
6.24 -if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
6.25 -else ()
6.26 +if do_it then
6.27 + import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
6.28 +else
6.29 + ()
6.30 *}
6.31
6.32 end
7.1 --- a/src/HOL/TPTP/ROOT.ML Wed Jul 11 21:43:19 2012 +0200
7.2 +++ b/src/HOL/TPTP/ROOT.ML Wed Jul 11 21:43:19 2012 +0200
7.3 @@ -7,7 +7,6 @@
7.4 *)
7.5
7.6 use_thys [
7.7 - "ATP_Theory_Export",
7.8 "MaSh_Import",
7.9 "TPTP_Interpret",
7.10 "THF_Arith"
8.1 --- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 21:43:19 2012 +0200
8.2 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 21:43:19 2012 +0200
8.3 @@ -61,8 +61,8 @@
8.4
8.5 fun all_facts_of_theory thy =
8.6 let val ctxt = Proof_Context.init_global thy in
8.7 - Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] []
8.8 - (Sledgehammer_Filter.clasimpset_rule_table_of ctxt)
8.9 + Sledgehammer_Fact.all_facts ctxt false Symtab.empty true [] []
8.10 + (Sledgehammer_Fact.clasimpset_rule_table_of ctxt)
8.11 |> rev (* try to restore the original order of facts, for MaSh *)
8.12 end
8.13
9.1 --- a/src/HOL/TPTP/mash_export.ML Wed Jul 11 21:43:19 2012 +0200
9.2 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 11 21:43:19 2012 +0200
9.3 @@ -15,7 +15,7 @@
9.4 val theory_ord : theory * theory -> order
9.5 val thm_ord : thm * thm -> order
9.6 val dependencies_of : string list -> thm -> string list
9.7 - val goal_of_thm : thm -> thm
9.8 + val goal_of_thm : theory -> thm -> thm
9.9 val meng_paulson_facts :
9.10 Proof.context -> int -> thm -> (((unit -> string) * stature) * thm) list
9.11 -> ((string * stature) * thm) list
9.12 @@ -34,8 +34,9 @@
9.13 structure MaSh_Export : MASH_EXPORT =
9.14 struct
9.15
9.16 +open ATP_Util
9.17 open ATP_Problem_Generate
9.18 -open ATP_Util
9.19 +open ATP_Theory_Export
9.20
9.21 type prover_result = Sledgehammer_Provers.prover_result
9.22
9.23 @@ -215,7 +216,7 @@
9.24 | freeze (Free (s, T)) = Free (s, freezeT T)
9.25 | freeze t = t
9.26
9.27 -val goal_of_thm = prop_of #> freeze #> cterm_of thy #> Goal.init
9.28 +fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
9.29
9.30 fun meng_paulson_facts ctxt max_relevant goal =
9.31 let
9.32 @@ -241,7 +242,7 @@
9.33 {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
9.34 facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
9.35 val prover =
9.36 - Sledgehammer_Run.get_minimizing_prover ctxt
9.37 + Sledgehammer_Minimize.get_minimizing_prover ctxt
9.38 Sledgehammer_Provers.Normal (hd provers)
9.39 in prover params (K (K (K ""))) problem end
9.40
9.41 @@ -320,18 +321,25 @@
9.42 fun do_thm th =
9.43 let
9.44 val name = Thm.get_name_hint th
9.45 - val goal = goal_of_thm th
9.46 - val isa_deps = dependencies_of all_names th
9.47 - val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
9.48 - val facts =
9.49 - facts |> meng_paulson_facts ctxt (the max_relevant) goal
9.50 - |> fold (add_isa_dep facts) isa_deps
9.51 - |> map fix_name
9.52 + val goal = goal_of_thm thy th
9.53 val deps =
9.54 - case run_sledgehammer ctxt facts goal of
9.55 - {outcome = NONE, used_facts, ...} =>
9.56 - used_facts |> map fst |> sort string_ord
9.57 - | _ => isa_deps
9.58 + case dependencies_of all_names th of
9.59 + [] => []
9.60 + | isa_dep as [_] => isa_dep (* can hardly beat that *)
9.61 + | isa_deps =>
9.62 + let
9.63 + val facts =
9.64 + facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
9.65 + val facts =
9.66 + facts |> meng_paulson_facts ctxt (the max_relevant) goal
9.67 + |> fold (add_isa_dep facts) isa_deps
9.68 + |> map fix_name
9.69 + in
9.70 + case run_sledgehammer ctxt facts goal of
9.71 + {outcome = NONE, used_facts, ...} =>
9.72 + used_facts |> map fst |> sort string_ord
9.73 + | _ => isa_deps
9.74 + end
9.75 val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
9.76 in File.append path s end
9.77 in List.app do_thm ths end
9.78 @@ -374,7 +382,7 @@
9.79 fun do_fact (fact as (_, th)) old_facts =
9.80 let
9.81 val name = Thm.get_name_hint th
9.82 - val goal = goal_of_thm th
9.83 + val goal = goal_of_thm thy th
9.84 val kind = Thm.legacy_get_kind th
9.85 val _ =
9.86 if kind <> "" then
10.1 --- a/src/HOL/TPTP/mash_import.ML Wed Jul 11 21:43:19 2012 +0200
10.2 +++ b/src/HOL/TPTP/mash_import.ML Wed Jul 11 21:43:19 2012 +0200
10.3 @@ -55,7 +55,7 @@
10.4 fun sugg_facts hyp_ts concl_t facts =
10.5 map_filter (find_sugg facts o of_fact_name)
10.6 #> take (max_relevant_slack * the max_relevant)
10.7 - #> Sledgehammer_Filter.maybe_instantiate_inducts ctxt hyp_ts concl_t
10.8 + #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
10.9 #> map (apfst (apfst (fn name => name ())))
10.10 fun meng_mash_facts fs1 fs2 =
10.11 let
10.12 @@ -106,7 +106,7 @@
10.13 SOME (_, th) => th
10.14 | NONE => error ("No fact called \"" ^ name ^ "\"")
10.15 val deps = dependencies_of all_names th
10.16 - val goal = goal_of_thm th
10.17 + val goal = goal_of_thm thy th
10.18 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
10.19 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
10.20 val deps_facts = sugg_facts hyp_ts concl_t facts deps
10.21 @@ -133,7 +133,7 @@
10.22 " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
10.23 Real.fmt (StringCvt.FIX (SOME 1))
10.24 (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
10.25 - val inst_inducts = Config.get ctxt Sledgehammer_Filter.instantiate_inducts
10.26 + val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts
10.27 val options =
10.28 [prover_name, string_of_int (the max_relevant) ^ " facts",
10.29 "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
11.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML Wed Jul 11 21:43:19 2012 +0200
11.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Wed Jul 11 21:43:19 2012 +0200
11.3 @@ -39,8 +39,8 @@
11.4 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
11.5 val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
11.6 val facts =
11.7 - Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
11.8 - chained_ths hyp_ts concl_t
11.9 + Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
11.10 + chained_ths hyp_ts concl_t
11.11 |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
11.12 (the_default default_max_relevant max_relevant) is_built_in_const
11.13 relevance_fudge relevance_override chained_ths hyp_ts concl_t
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 11 21:43:19 2012 +0200
12.3 @@ -0,0 +1,439 @@
12.4 +(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact.ML
12.5 + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
12.6 + Author: Jasmin Blanchette, TU Muenchen
12.7 +
12.8 +Sledgehammer fact handling.
12.9 +*)
12.10 +
12.11 +signature SLEDGEHAMMER_FACT =
12.12 +sig
12.13 + type status = ATP_Problem_Generate.status
12.14 + type stature = ATP_Problem_Generate.stature
12.15 +
12.16 + type relevance_override =
12.17 + {add : (Facts.ref * Attrib.src list) list,
12.18 + del : (Facts.ref * Attrib.src list) list,
12.19 + only : bool}
12.20 +
12.21 + val ignore_no_atp : bool Config.T
12.22 + val instantiate_inducts : bool Config.T
12.23 + val no_relevance_override : relevance_override
12.24 + val fact_from_ref :
12.25 + Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
12.26 + -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
12.27 + val all_facts :
12.28 + Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
12.29 + -> thm list -> status Termtab.table
12.30 + -> (((unit -> string) * stature) * thm) list
12.31 + val clasimpset_rule_table_of : Proof.context -> status Termtab.table
12.32 + val maybe_instantiate_inducts :
12.33 + Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
12.34 + -> (((unit -> string) * 'a) * thm) list
12.35 + val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
12.36 + val nearly_all_facts :
12.37 + Proof.context -> bool -> relevance_override -> thm list -> term list -> term
12.38 + -> (((unit -> string) * stature) * thm) list
12.39 +end;
12.40 +
12.41 +structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
12.42 +struct
12.43 +
12.44 +open ATP_Problem_Generate
12.45 +open Metis_Tactic
12.46 +open Sledgehammer_Util
12.47 +
12.48 +type relevance_override =
12.49 + {add : (Facts.ref * Attrib.src list) list,
12.50 + del : (Facts.ref * Attrib.src list) list,
12.51 + only : bool}
12.52 +
12.53 +val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
12.54 +
12.55 +(* experimental features *)
12.56 +val ignore_no_atp =
12.57 + Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
12.58 +val instantiate_inducts =
12.59 + Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
12.60 +
12.61 +val no_relevance_override = {add = [], del = [], only = false}
12.62 +
12.63 +fun needs_quoting reserved s =
12.64 + Symtab.defined reserved s orelse
12.65 + exists (not o Lexicon.is_identifier) (Long_Name.explode s)
12.66 +
12.67 +fun make_name reserved multi j name =
12.68 + (name |> needs_quoting reserved name ? quote) ^
12.69 + (if multi then "(" ^ string_of_int j ^ ")" else "")
12.70 +
12.71 +fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
12.72 + | explode_interval max (Facts.From i) = i upto i + max - 1
12.73 + | explode_interval _ (Facts.Single i) = [i]
12.74 +
12.75 +val backquote =
12.76 + raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
12.77 +
12.78 +(* unfolding these can yield really huge terms *)
12.79 +val risky_defs = @{thms Bit0_def Bit1_def}
12.80 +
12.81 +fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
12.82 +fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
12.83 + | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
12.84 + | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
12.85 + | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
12.86 + | is_rec_def _ = false
12.87 +
12.88 +fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
12.89 +fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths
12.90 +
12.91 +fun scope_of_thm global assms chained_ths th =
12.92 + if is_chained chained_ths th then Chained
12.93 + else if global then Global
12.94 + else if is_assum assms th then Assum
12.95 + else Local
12.96 +
12.97 +val may_be_induction =
12.98 + exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
12.99 + body_type T = @{typ bool}
12.100 + | _ => false)
12.101 +
12.102 +fun status_of_thm css_table name th =
12.103 + (* FIXME: use structured name *)
12.104 + if (String.isSubstring ".induct" name orelse
12.105 + String.isSubstring ".inducts" name) andalso
12.106 + may_be_induction (prop_of th) then
12.107 + Induction
12.108 + else case Termtab.lookup css_table (prop_of th) of
12.109 + SOME status => status
12.110 + | NONE => General
12.111 +
12.112 +fun stature_of_thm global assms chained_ths css_table name th =
12.113 + (scope_of_thm global assms chained_ths th, status_of_thm css_table name th)
12.114 +
12.115 +fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) =
12.116 + let
12.117 + val ths = Attrib.eval_thms ctxt [xthm]
12.118 + val bracket =
12.119 + map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
12.120 + |> implode
12.121 + fun nth_name j =
12.122 + case xref of
12.123 + Facts.Fact s => backquote s ^ bracket
12.124 + | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
12.125 + | Facts.Named ((name, _), NONE) =>
12.126 + make_name reserved (length ths > 1) (j + 1) name ^ bracket
12.127 + | Facts.Named ((name, _), SOME intervals) =>
12.128 + make_name reserved true
12.129 + (nth (maps (explode_interval (length ths)) intervals) j) name ^
12.130 + bracket
12.131 + in
12.132 + (ths, (0, []))
12.133 + |-> fold (fn th => fn (j, rest) =>
12.134 + let val name = nth_name j in
12.135 + (j + 1, ((name, stature_of_thm false [] chained_ths
12.136 + css_table name th), th) :: rest)
12.137 + end)
12.138 + |> snd
12.139 + end
12.140 +
12.141 +(* Reject theorems with names like "List.filter.filter_list_def" or
12.142 + "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
12.143 +fun is_package_def a =
12.144 + let val names = Long_Name.explode a in
12.145 + (length names > 2 andalso not (hd names = "local") andalso
12.146 + String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
12.147 + end
12.148 +
12.149 +(* FIXME: put other record thms here, or declare as "no_atp" *)
12.150 +fun multi_base_blacklist ctxt ho_atp =
12.151 + ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
12.152 + "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
12.153 + "weak_case_cong"]
12.154 + |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
12.155 + append ["induct", "inducts"]
12.156 + |> map (prefix ".")
12.157 +
12.158 +val max_lambda_nesting = 3 (*only applies if not ho_atp*)
12.159 +
12.160 +fun term_has_too_many_lambdas max (t1 $ t2) =
12.161 + exists (term_has_too_many_lambdas max) [t1, t2]
12.162 + | term_has_too_many_lambdas max (Abs (_, _, t)) =
12.163 + max = 0 orelse term_has_too_many_lambdas (max - 1) t
12.164 + | term_has_too_many_lambdas _ _ = false
12.165 +
12.166 +(* Don't count nested lambdas at the level of formulas, since they are
12.167 + quantifiers. *)
12.168 +fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
12.169 + | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
12.170 + formula_has_too_many_lambdas false (T :: Ts) t
12.171 + | formula_has_too_many_lambdas _ Ts t =
12.172 + if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
12.173 + exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
12.174 + else
12.175 + term_has_too_many_lambdas max_lambda_nesting t
12.176 +
12.177 +(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
12.178 + was 11. *)
12.179 +val max_apply_depth = 15
12.180 +
12.181 +fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
12.182 + | apply_depth (Abs (_, _, t)) = apply_depth t
12.183 + | apply_depth _ = 0
12.184 +
12.185 +fun is_formula_too_complex ho_atp t =
12.186 + apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
12.187 +
12.188 +(* FIXME: Extend to "Meson" and "Metis" *)
12.189 +val exists_sledgehammer_const =
12.190 + exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
12.191 +
12.192 +(* FIXME: make more reliable *)
12.193 +val exists_low_level_class_const =
12.194 + exists_Const (fn (s, _) =>
12.195 + s = @{const_name equal_class.equal} orelse
12.196 + String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
12.197 +
12.198 +fun is_metastrange_theorem th =
12.199 + case head_of (concl_of th) of
12.200 + Const (s, _) => (s <> @{const_name Trueprop} andalso
12.201 + s <> @{const_name "=="})
12.202 + | _ => false
12.203 +
12.204 +fun is_that_fact th =
12.205 + String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
12.206 + andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
12.207 + | _ => false) (prop_of th)
12.208 +
12.209 +fun is_theorem_bad_for_atps ho_atp exporter thm =
12.210 + is_metastrange_theorem thm orelse
12.211 + (not exporter andalso
12.212 + let val t = prop_of thm in
12.213 + is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
12.214 + exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
12.215 + is_that_fact thm
12.216 + end)
12.217 +
12.218 +fun hackish_string_for_term ctxt t =
12.219 + Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
12.220 + (print_mode_value ())) (Syntax.string_of_term ctxt) t
12.221 + |> String.translate (fn c => if Char.isPrint c then str c else "")
12.222 + |> simplify_spaces
12.223 +
12.224 +(* This is a terrible hack. Free variables are sometimes coded as "M__" when
12.225 + they are displayed as "M" and we want to avoid clashes with these. But
12.226 + sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
12.227 + prefixes of all free variables. In the worse case scenario, where the fact
12.228 + won't be resolved correctly, the user can fix it manually, e.g., by naming
12.229 + the fact in question. Ideally we would need nothing of it, but backticks
12.230 + simply don't work with schematic variables. *)
12.231 +fun all_prefixes_of s =
12.232 + map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
12.233 +
12.234 +fun close_form t =
12.235 + (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
12.236 + |> fold (fn ((s, i), T) => fn (t', taken) =>
12.237 + let val s' = singleton (Name.variant_list taken) s in
12.238 + ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
12.239 + else Logic.all_const) T
12.240 + $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
12.241 + s' :: taken)
12.242 + end)
12.243 + (Term.add_vars t [] |> sort_wrt (fst o fst))
12.244 + |> fst
12.245 +
12.246 +fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
12.247 + let
12.248 + val thy = Proof_Context.theory_of ctxt
12.249 + val global_facts = Global_Theory.facts_of thy
12.250 + val local_facts = Proof_Context.facts_of ctxt
12.251 + val named_locals = local_facts |> Facts.dest_static []
12.252 + val assms = Assumption.all_assms_of ctxt
12.253 + fun is_good_unnamed_local th =
12.254 + not (Thm.has_name_hint th) andalso
12.255 + forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
12.256 + val unnamed_locals =
12.257 + union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
12.258 + |> filter is_good_unnamed_local |> map (pair "" o single)
12.259 + val full_space =
12.260 + Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
12.261 + fun add_facts global foldx facts =
12.262 + foldx (fn (name0, ths) =>
12.263 + if not exporter andalso name0 <> "" andalso
12.264 + forall (not o member Thm.eq_thm_prop add_ths) ths andalso
12.265 + (Facts.is_concealed facts name0 orelse
12.266 + (not (Config.get ctxt ignore_no_atp) andalso
12.267 + is_package_def name0) orelse
12.268 + exists (fn s => String.isSuffix s name0)
12.269 + (multi_base_blacklist ctxt ho_atp)) then
12.270 + I
12.271 + else
12.272 + let
12.273 + val multi = length ths > 1
12.274 + val backquote_thm =
12.275 + backquote o hackish_string_for_term ctxt o close_form o prop_of
12.276 + fun check_thms a =
12.277 + case try (Proof_Context.get_thms ctxt) a of
12.278 + NONE => false
12.279 + | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
12.280 + in
12.281 + pair 1
12.282 + #> fold (fn th => fn (j, (multis, unis)) =>
12.283 + (j + 1,
12.284 + if not (member Thm.eq_thm_prop add_ths th) andalso
12.285 + is_theorem_bad_for_atps ho_atp exporter th then
12.286 + (multis, unis)
12.287 + else
12.288 + let
12.289 + val new =
12.290 + (((fn () =>
12.291 + if name0 = "" then
12.292 + th |> backquote_thm
12.293 + else
12.294 + [Facts.extern ctxt facts name0,
12.295 + Name_Space.extern ctxt full_space name0,
12.296 + name0]
12.297 + |> find_first check_thms
12.298 + |> (fn SOME name =>
12.299 + make_name reserved multi j name
12.300 + | NONE => "")),
12.301 + stature_of_thm global assms chained_ths
12.302 + css_table name0 th), th)
12.303 + in
12.304 + if multi then (new :: multis, unis)
12.305 + else (multis, new :: unis)
12.306 + end)) ths
12.307 + #> snd
12.308 + end)
12.309 + in
12.310 + (* The single-name theorems go after the multiple-name ones, so that single
12.311 + names are preferred when both are available. *)
12.312 + ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
12.313 + |> add_facts true Facts.fold_static global_facts global_facts
12.314 + |> op @
12.315 + end
12.316 +
12.317 +fun clasimpset_rule_table_of ctxt =
12.318 + let
12.319 + val thy = Proof_Context.theory_of ctxt
12.320 + val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
12.321 + fun add stature normalizers get_th =
12.322 + fold (fn rule =>
12.323 + let
12.324 + val th = rule |> get_th
12.325 + val t =
12.326 + th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
12.327 + in
12.328 + fold (fn normalize => Termtab.update (normalize t, stature))
12.329 + (I :: normalizers)
12.330 + end)
12.331 + val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
12.332 + ctxt |> claset_of |> Classical.rep_cs
12.333 + val intros = Item_Net.content safeIs @ Item_Net.content hazIs
12.334 +(* Add once it is used:
12.335 + val elims =
12.336 + Item_Net.content safeEs @ Item_Net.content hazEs
12.337 + |> map Classical.classical_rule
12.338 +*)
12.339 + val simps = ctxt |> simpset_of |> dest_ss |> #simps
12.340 + val specs = ctxt |> Spec_Rules.get
12.341 + val (rec_defs, nonrec_defs) =
12.342 + specs |> filter (curry (op =) Spec_Rules.Equational o fst)
12.343 + |> maps (snd o snd)
12.344 + |> filter_out (member Thm.eq_thm_prop risky_defs)
12.345 + |> List.partition (is_rec_def o prop_of)
12.346 + val spec_intros =
12.347 + specs |> filter (member (op =) [Spec_Rules.Inductive,
12.348 + Spec_Rules.Co_Inductive] o fst)
12.349 + |> maps (snd o snd)
12.350 + in
12.351 + Termtab.empty |> add Simp [atomize] snd simps
12.352 + |> add Simp [] I rec_defs
12.353 + |> add Def [] I nonrec_defs
12.354 +(* Add once it is used:
12.355 + |> add Elim [] I elims
12.356 +*)
12.357 + |> add Intro [] I intros
12.358 + |> add Inductive [] I spec_intros
12.359 + end
12.360 +
12.361 +fun uniquify xs =
12.362 + Termtab.fold (cons o snd)
12.363 + (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
12.364 +
12.365 +fun struct_induct_rule_on th =
12.366 + case Logic.strip_horn (prop_of th) of
12.367 + (prems, @{const Trueprop}
12.368 + $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
12.369 + if not (is_TVar ind_T) andalso length prems > 1 andalso
12.370 + exists (exists_subterm (curry (op aconv) p)) prems andalso
12.371 + not (exists (exists_subterm (curry (op aconv) a)) prems) then
12.372 + SOME (p_name, ind_T)
12.373 + else
12.374 + NONE
12.375 + | _ => NONE
12.376 +
12.377 +fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
12.378 + let
12.379 + fun varify_noninducts (t as Free (s, T)) =
12.380 + if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
12.381 + | varify_noninducts t = t
12.382 + val p_inst =
12.383 + concl_prop |> map_aterms varify_noninducts |> close_form
12.384 + |> lambda (Free ind_x)
12.385 + |> hackish_string_for_term ctxt
12.386 + in
12.387 + ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
12.388 + stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
12.389 + end
12.390 +
12.391 +fun type_match thy (T1, T2) =
12.392 + (Sign.typ_match thy (T2, T1) Vartab.empty; true)
12.393 + handle Type.TYPE_MATCH => false
12.394 +
12.395 +fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
12.396 + case struct_induct_rule_on th of
12.397 + SOME (p_name, ind_T) =>
12.398 + let val thy = Proof_Context.theory_of ctxt in
12.399 + stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
12.400 + |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
12.401 + end
12.402 + | NONE => [ax]
12.403 +
12.404 +fun external_frees t =
12.405 + [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
12.406 +
12.407 +fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
12.408 + if Config.get ctxt instantiate_inducts then
12.409 + let
12.410 + val thy = Proof_Context.theory_of ctxt
12.411 + val ind_stmt =
12.412 + (hyp_ts |> filter_out (null o external_frees), concl_t)
12.413 + |> Logic.list_implies |> Object_Logic.atomize_term thy
12.414 + val ind_stmt_xs = external_frees ind_stmt
12.415 + in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
12.416 + else
12.417 + I
12.418 +
12.419 +fun maybe_filter_no_atps ctxt =
12.420 + not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
12.421 +
12.422 +fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
12.423 + chained_ths hyp_ts concl_t =
12.424 + if only andalso null add then
12.425 + []
12.426 + else
12.427 + let
12.428 + val reserved = reserved_isar_keyword_table ()
12.429 + val add_ths = Attrib.eval_thms ctxt add
12.430 + val css_table = clasimpset_rule_table_of ctxt
12.431 + in
12.432 + (if only then
12.433 + maps (map (fn ((name, stature), th) => ((K name, stature), th))
12.434 + o fact_from_ref ctxt reserved chained_ths css_table) add
12.435 + else
12.436 + all_facts ctxt ho_atp reserved false add_ths chained_ths css_table)
12.437 + |> maybe_instantiate_inducts ctxt hyp_ts concl_t
12.438 + |> not only ? maybe_filter_no_atps ctxt
12.439 + |> uniquify
12.440 + end
12.441 +
12.442 +end;
13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Jul 11 21:43:19 2012 +0200
13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Jul 11 21:43:19 2012 +0200
13.3 @@ -7,27 +7,10 @@
13.4
13.5 signature SLEDGEHAMMER_FILTER =
13.6 sig
13.7 - type status = ATP_Problem_Generate.status
13.8 type stature = ATP_Problem_Generate.stature
13.9 type relevance_fudge = Sledgehammer_Filter_Iter.relevance_fudge
13.10 type relevance_override = Sledgehammer_Filter_Iter.relevance_override
13.11
13.12 - val no_relevance_override : relevance_override
13.13 - val fact_from_ref :
13.14 - Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
13.15 - -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
13.16 - val all_facts :
13.17 - Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
13.18 - -> thm list -> status Termtab.table
13.19 - -> (((unit -> string) * stature) * thm) list
13.20 - val clasimpset_rule_table_of : Proof.context -> status Termtab.table
13.21 - val maybe_instantiate_inducts :
13.22 - Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
13.23 - -> (((unit -> string) * 'a) * thm) list
13.24 - val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
13.25 - val nearly_all_facts :
13.26 - Proof.context -> bool -> relevance_override -> thm list -> term list -> term
13.27 - -> (((unit -> string) * stature) * thm) list
13.28 val relevant_facts :
13.29 Proof.context -> real * real -> int
13.30 -> (string * typ -> term list -> bool * term list) -> relevance_fudge
13.31 @@ -39,394 +22,8 @@
13.32 structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
13.33 struct
13.34
13.35 -open ATP_Problem_Generate
13.36 -open Metis_Tactic
13.37 -open Sledgehammer_Util
13.38 open Sledgehammer_Filter_Iter
13.39
13.40 -val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
13.41 -
13.42 -val no_relevance_override = {add = [], del = [], only = false}
13.43 -
13.44 -fun needs_quoting reserved s =
13.45 - Symtab.defined reserved s orelse
13.46 - exists (not o Lexicon.is_identifier) (Long_Name.explode s)
13.47 -
13.48 -fun make_name reserved multi j name =
13.49 - (name |> needs_quoting reserved name ? quote) ^
13.50 - (if multi then "(" ^ string_of_int j ^ ")" else "")
13.51 -
13.52 -fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
13.53 - | explode_interval max (Facts.From i) = i upto i + max - 1
13.54 - | explode_interval _ (Facts.Single i) = [i]
13.55 -
13.56 -val backquote =
13.57 - raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
13.58 -
13.59 -(* unfolding these can yield really huge terms *)
13.60 -val risky_defs = @{thms Bit0_def Bit1_def}
13.61 -
13.62 -fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
13.63 -fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
13.64 - | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
13.65 - | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
13.66 - | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
13.67 - | is_rec_def _ = false
13.68 -
13.69 -fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
13.70 -fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths
13.71 -
13.72 -fun scope_of_thm global assms chained_ths th =
13.73 - if is_chained chained_ths th then Chained
13.74 - else if global then Global
13.75 - else if is_assum assms th then Assum
13.76 - else Local
13.77 -
13.78 -val may_be_induction =
13.79 - exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
13.80 - body_type T = @{typ bool}
13.81 - | _ => false)
13.82 -
13.83 -fun status_of_thm css_table name th =
13.84 - (* FIXME: use structured name *)
13.85 - if (String.isSubstring ".induct" name orelse
13.86 - String.isSubstring ".inducts" name) andalso
13.87 - may_be_induction (prop_of th) then
13.88 - Induction
13.89 - else case Termtab.lookup css_table (prop_of th) of
13.90 - SOME status => status
13.91 - | NONE => General
13.92 -
13.93 -fun stature_of_thm global assms chained_ths css_table name th =
13.94 - (scope_of_thm global assms chained_ths th, status_of_thm css_table name th)
13.95 -
13.96 -fun fact_from_ref ctxt reserved chained_ths css_table (xthm as (xref, args)) =
13.97 - let
13.98 - val ths = Attrib.eval_thms ctxt [xthm]
13.99 - val bracket =
13.100 - map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
13.101 - |> implode
13.102 - fun nth_name j =
13.103 - case xref of
13.104 - Facts.Fact s => backquote s ^ bracket
13.105 - | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
13.106 - | Facts.Named ((name, _), NONE) =>
13.107 - make_name reserved (length ths > 1) (j + 1) name ^ bracket
13.108 - | Facts.Named ((name, _), SOME intervals) =>
13.109 - make_name reserved true
13.110 - (nth (maps (explode_interval (length ths)) intervals) j) name ^
13.111 - bracket
13.112 - in
13.113 - (ths, (0, []))
13.114 - |-> fold (fn th => fn (j, rest) =>
13.115 - let val name = nth_name j in
13.116 - (j + 1, ((name, stature_of_thm false [] chained_ths
13.117 - css_table name th), th) :: rest)
13.118 - end)
13.119 - |> snd
13.120 - end
13.121 -
13.122 -(*Reject theorems with names like "List.filter.filter_list_def" or
13.123 - "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
13.124 -fun is_package_def a =
13.125 - let val names = Long_Name.explode a in
13.126 - (length names > 2 andalso not (hd names = "local") andalso
13.127 - String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
13.128 - end
13.129 -
13.130 -(* FIXME: put other record thms here, or declare as "no_atp" *)
13.131 -fun multi_base_blacklist ctxt ho_atp =
13.132 - ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
13.133 - "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
13.134 - "weak_case_cong"]
13.135 - |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
13.136 - append ["induct", "inducts"]
13.137 - |> map (prefix ".")
13.138 -
13.139 -val max_lambda_nesting = 3 (*only applies if not ho_atp*)
13.140 -
13.141 -fun term_has_too_many_lambdas max (t1 $ t2) =
13.142 - exists (term_has_too_many_lambdas max) [t1, t2]
13.143 - | term_has_too_many_lambdas max (Abs (_, _, t)) =
13.144 - max = 0 orelse term_has_too_many_lambdas (max - 1) t
13.145 - | term_has_too_many_lambdas _ _ = false
13.146 -
13.147 -(* Don't count nested lambdas at the level of formulas, since they are
13.148 - quantifiers. *)
13.149 -fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
13.150 - | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
13.151 - formula_has_too_many_lambdas false (T :: Ts) t
13.152 - | formula_has_too_many_lambdas _ Ts t =
13.153 - if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
13.154 - exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
13.155 - else
13.156 - term_has_too_many_lambdas max_lambda_nesting t
13.157 -
13.158 -(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
13.159 - was 11. *)
13.160 -val max_apply_depth = 15
13.161 -
13.162 -fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
13.163 - | apply_depth (Abs (_, _, t)) = apply_depth t
13.164 - | apply_depth _ = 0
13.165 -
13.166 -fun is_formula_too_complex ho_atp t =
13.167 - apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
13.168 -
13.169 -(* FIXME: Extend to "Meson" and "Metis" *)
13.170 -val exists_sledgehammer_const =
13.171 - exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
13.172 -
13.173 -(* FIXME: make more reliable *)
13.174 -val exists_low_level_class_const =
13.175 - exists_Const (fn (s, _) =>
13.176 - s = @{const_name equal_class.equal} orelse
13.177 - String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
13.178 -
13.179 -fun is_metastrange_theorem th =
13.180 - case head_of (concl_of th) of
13.181 - Const (s, _) => (s <> @{const_name Trueprop} andalso
13.182 - s <> @{const_name "=="})
13.183 - | _ => false
13.184 -
13.185 -fun is_that_fact th =
13.186 - String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
13.187 - andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
13.188 - | _ => false) (prop_of th)
13.189 -
13.190 -fun is_theorem_bad_for_atps ho_atp exporter thm =
13.191 - is_metastrange_theorem thm orelse
13.192 - (not exporter andalso
13.193 - let val t = prop_of thm in
13.194 - is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
13.195 - exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
13.196 - is_that_fact thm
13.197 - end)
13.198 -
13.199 -fun string_for_term ctxt t =
13.200 - Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
13.201 - (print_mode_value ())) (Syntax.string_of_term ctxt) t
13.202 - |> String.translate (fn c => if Char.isPrint c then str c else "")
13.203 - |> simplify_spaces
13.204 -
13.205 -(* This is a terrible hack. Free variables are sometimes coded as "M__" when
13.206 - they are displayed as "M" and we want to avoid clashes with these. But
13.207 - sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
13.208 - prefixes of all free variables. In the worse case scenario, where the fact
13.209 - won't be resolved correctly, the user can fix it manually, e.g., by naming
13.210 - the fact in question. Ideally we would need nothing of it, but backticks
13.211 - simply don't work with schematic variables. *)
13.212 -fun all_prefixes_of s =
13.213 - map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
13.214 -
13.215 -fun close_form t =
13.216 - (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
13.217 - |> fold (fn ((s, i), T) => fn (t', taken) =>
13.218 - let val s' = singleton (Name.variant_list taken) s in
13.219 - ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
13.220 - else Logic.all_const) T
13.221 - $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
13.222 - s' :: taken)
13.223 - end)
13.224 - (Term.add_vars t [] |> sort_wrt (fst o fst))
13.225 - |> fst
13.226 -
13.227 -fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
13.228 - let
13.229 - val thy = Proof_Context.theory_of ctxt
13.230 - val global_facts = Global_Theory.facts_of thy
13.231 - val local_facts = Proof_Context.facts_of ctxt
13.232 - val named_locals = local_facts |> Facts.dest_static []
13.233 - val assms = Assumption.all_assms_of ctxt
13.234 - fun is_good_unnamed_local th =
13.235 - not (Thm.has_name_hint th) andalso
13.236 - forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
13.237 - val unnamed_locals =
13.238 - union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
13.239 - |> filter is_good_unnamed_local |> map (pair "" o single)
13.240 - val full_space =
13.241 - Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
13.242 - fun add_facts global foldx facts =
13.243 - foldx (fn (name0, ths) =>
13.244 - if not exporter andalso name0 <> "" andalso
13.245 - forall (not o member Thm.eq_thm_prop add_ths) ths andalso
13.246 - (Facts.is_concealed facts name0 orelse
13.247 - (not (Config.get ctxt ignore_no_atp) andalso
13.248 - is_package_def name0) orelse
13.249 - exists (fn s => String.isSuffix s name0)
13.250 - (multi_base_blacklist ctxt ho_atp)) then
13.251 - I
13.252 - else
13.253 - let
13.254 - val multi = length ths > 1
13.255 - val backquote_thm =
13.256 - backquote o string_for_term ctxt o close_form o prop_of
13.257 - fun check_thms a =
13.258 - case try (Proof_Context.get_thms ctxt) a of
13.259 - NONE => false
13.260 - | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
13.261 - in
13.262 - pair 1
13.263 - #> fold (fn th => fn (j, (multis, unis)) =>
13.264 - (j + 1,
13.265 - if not (member Thm.eq_thm_prop add_ths th) andalso
13.266 - is_theorem_bad_for_atps ho_atp exporter th then
13.267 - (multis, unis)
13.268 - else
13.269 - let
13.270 - val new =
13.271 - (((fn () =>
13.272 - if name0 = "" then
13.273 - th |> backquote_thm
13.274 - else
13.275 - [Facts.extern ctxt facts name0,
13.276 - Name_Space.extern ctxt full_space name0,
13.277 - name0]
13.278 - |> find_first check_thms
13.279 - |> (fn SOME name =>
13.280 - make_name reserved multi j name
13.281 - | NONE => "")),
13.282 - stature_of_thm global assms chained_ths
13.283 - css_table name0 th), th)
13.284 - in
13.285 - if multi then (new :: multis, unis)
13.286 - else (multis, new :: unis)
13.287 - end)) ths
13.288 - #> snd
13.289 - end)
13.290 - in
13.291 - (* The single-name theorems go after the multiple-name ones, so that single
13.292 - names are preferred when both are available. *)
13.293 - ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
13.294 - |> add_facts true Facts.fold_static global_facts global_facts
13.295 - |> op @
13.296 - end
13.297 -
13.298 -fun clasimpset_rule_table_of ctxt =
13.299 - let
13.300 - val thy = Proof_Context.theory_of ctxt
13.301 - val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
13.302 - fun add stature normalizers get_th =
13.303 - fold (fn rule =>
13.304 - let
13.305 - val th = rule |> get_th
13.306 - val t =
13.307 - th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
13.308 - in
13.309 - fold (fn normalize => Termtab.update (normalize t, stature))
13.310 - (I :: normalizers)
13.311 - end)
13.312 - val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
13.313 - ctxt |> claset_of |> Classical.rep_cs
13.314 - val intros = Item_Net.content safeIs @ Item_Net.content hazIs
13.315 -(* Add once it is used:
13.316 - val elims =
13.317 - Item_Net.content safeEs @ Item_Net.content hazEs
13.318 - |> map Classical.classical_rule
13.319 -*)
13.320 - val simps = ctxt |> simpset_of |> dest_ss |> #simps
13.321 - val specs = ctxt |> Spec_Rules.get
13.322 - val (rec_defs, nonrec_defs) =
13.323 - specs |> filter (curry (op =) Spec_Rules.Equational o fst)
13.324 - |> maps (snd o snd)
13.325 - |> filter_out (member Thm.eq_thm_prop risky_defs)
13.326 - |> List.partition (is_rec_def o prop_of)
13.327 - val spec_intros =
13.328 - specs |> filter (member (op =) [Spec_Rules.Inductive,
13.329 - Spec_Rules.Co_Inductive] o fst)
13.330 - |> maps (snd o snd)
13.331 - in
13.332 - Termtab.empty |> add Simp [atomize] snd simps
13.333 - |> add Simp [] I rec_defs
13.334 - |> add Def [] I nonrec_defs
13.335 -(* Add once it is used:
13.336 - |> add Elim [] I elims
13.337 -*)
13.338 - |> add Intro [] I intros
13.339 - |> add Inductive [] I spec_intros
13.340 - end
13.341 -
13.342 -fun uniquify xs =
13.343 - Termtab.fold (cons o snd)
13.344 - (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
13.345 -
13.346 -fun struct_induct_rule_on th =
13.347 - case Logic.strip_horn (prop_of th) of
13.348 - (prems, @{const Trueprop}
13.349 - $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
13.350 - if not (is_TVar ind_T) andalso length prems > 1 andalso
13.351 - exists (exists_subterm (curry (op aconv) p)) prems andalso
13.352 - not (exists (exists_subterm (curry (op aconv) a)) prems) then
13.353 - SOME (p_name, ind_T)
13.354 - else
13.355 - NONE
13.356 - | _ => NONE
13.357 -
13.358 -fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
13.359 - let
13.360 - fun varify_noninducts (t as Free (s, T)) =
13.361 - if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
13.362 - | varify_noninducts t = t
13.363 - val p_inst =
13.364 - concl_prop |> map_aterms varify_noninducts |> close_form
13.365 - |> lambda (Free ind_x)
13.366 - |> string_for_term ctxt
13.367 - in
13.368 - ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
13.369 - stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
13.370 - end
13.371 -
13.372 -fun type_match thy (T1, T2) =
13.373 - (Sign.typ_match thy (T2, T1) Vartab.empty; true)
13.374 - handle Type.TYPE_MATCH => false
13.375 -
13.376 -fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
13.377 - case struct_induct_rule_on th of
13.378 - SOME (p_name, ind_T) =>
13.379 - let val thy = Proof_Context.theory_of ctxt in
13.380 - stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
13.381 - |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
13.382 - end
13.383 - | NONE => [ax]
13.384 -
13.385 -fun external_frees t =
13.386 - [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
13.387 -
13.388 -fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
13.389 - if Config.get ctxt instantiate_inducts then
13.390 - let
13.391 - val thy = Proof_Context.theory_of ctxt
13.392 - val ind_stmt =
13.393 - (hyp_ts |> filter_out (null o external_frees), concl_t)
13.394 - |> Logic.list_implies |> Object_Logic.atomize_term thy
13.395 - val ind_stmt_xs = external_frees ind_stmt
13.396 - in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
13.397 - else
13.398 - I
13.399 -
13.400 -fun maybe_filter_no_atps ctxt =
13.401 - not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
13.402 -
13.403 -fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
13.404 - chained_ths hyp_ts concl_t =
13.405 - if only andalso null add then
13.406 - []
13.407 - else
13.408 - let
13.409 - val reserved = reserved_isar_keyword_table ()
13.410 - val add_ths = Attrib.eval_thms ctxt add
13.411 - val css_table = clasimpset_rule_table_of ctxt
13.412 - in
13.413 - (if only then
13.414 - maps (map (fn ((name, stature), th) => ((K name, stature), th))
13.415 - o fact_from_ref ctxt reserved chained_ths css_table) add
13.416 - else
13.417 - all_facts ctxt ho_atp reserved false add_ths chained_ths css_table)
13.418 - |> maybe_instantiate_inducts ctxt hyp_ts concl_t
13.419 - |> not only ? maybe_filter_no_atps ctxt
13.420 - |> uniquify
13.421 - end
13.422 -
13.423 val relevant_facts = iterative_relevant_facts
13.424
13.425 end;
14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 11 21:43:19 2012 +0200
14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 11 21:43:19 2012 +0200
14.3 @@ -8,6 +8,7 @@
14.4 signature SLEDGEHAMMER_FILTER_ITER =
14.5 sig
14.6 type stature = ATP_Problem_Generate.stature
14.7 + type relevance_override = Sledgehammer_Fact.relevance_override
14.8
14.9 type relevance_fudge =
14.10 {local_const_multiplier : real,
14.11 @@ -30,14 +31,7 @@
14.12 threshold_divisor : real,
14.13 ridiculous_threshold : real}
14.14
14.15 - type relevance_override =
14.16 - {add : (Facts.ref * Attrib.src list) list,
14.17 - del : (Facts.ref * Attrib.src list) list,
14.18 - only : bool}
14.19 -
14.20 val trace : bool Config.T
14.21 - val ignore_no_atp : bool Config.T
14.22 - val instantiate_inducts : bool Config.T
14.23 val pseudo_abs_name : string
14.24 val pseudo_skolem_prefix : string
14.25 val const_names_in_fact :
14.26 @@ -55,17 +49,12 @@
14.27 struct
14.28
14.29 open ATP_Problem_Generate
14.30 +open Sledgehammer_Fact
14.31
14.32 val trace =
14.33 Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false)
14.34 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
14.35
14.36 -(* experimental features *)
14.37 -val ignore_no_atp =
14.38 - Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
14.39 -val instantiate_inducts =
14.40 - Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
14.41 -
14.42 type relevance_fudge =
14.43 {local_const_multiplier : real,
14.44 worse_irrel_freq : real,
14.45 @@ -87,11 +76,6 @@
14.46 threshold_divisor : real,
14.47 ridiculous_threshold : real}
14.48
14.49 -type relevance_override =
14.50 - {add : (Facts.ref * Attrib.src list) list,
14.51 - del : (Facts.ref * Attrib.src list) list,
14.52 - only : bool}
14.53 -
14.54 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
14.55 val pseudo_abs_name = sledgehammer_prefix ^ "abs"
14.56 val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko"
15.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 11 21:43:19 2012 +0200
15.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 11 21:43:19 2012 +0200
15.3 @@ -23,7 +23,7 @@
15.4 open ATP_Problem_Generate
15.5 open ATP_Proof_Reconstruct
15.6 open Sledgehammer_Util
15.7 -open Sledgehammer_Filter
15.8 +open Sledgehammer_Fact
15.9 open Sledgehammer_Provers
15.10 open Sledgehammer_Minimize
15.11 open Sledgehammer_Run
16.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 11 21:43:19 2012 +0200
16.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 11 21:43:19 2012 +0200
16.3 @@ -9,14 +9,19 @@
16.4 sig
16.5 type stature = ATP_Problem_Generate.stature
16.6 type play = ATP_Proof_Reconstruct.play
16.7 + type mode = Sledgehammer_Provers.mode
16.8 type params = Sledgehammer_Provers.params
16.9 + type prover = Sledgehammer_Provers.prover
16.10
16.11 val binary_min_facts : int Config.T
16.12 + val auto_minimize_min_facts : int Config.T
16.13 + val auto_minimize_max_time : real Config.T
16.14 val minimize_facts :
16.15 string -> params -> bool -> int -> int -> Proof.state
16.16 -> ((string * stature) * thm list) list
16.17 -> ((string * stature) * thm list) list option
16.18 * ((unit -> play) * (play -> string) * string)
16.19 + val get_minimizing_prover : Proof.context -> mode -> string -> prover
16.20 val run_minimize :
16.21 params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
16.22 end;
16.23 @@ -29,7 +34,7 @@
16.24 open ATP_Problem_Generate
16.25 open ATP_Proof_Reconstruct
16.26 open Sledgehammer_Util
16.27 -open Sledgehammer_Filter
16.28 +open Sledgehammer_Fact
16.29 open Sledgehammer_Provers
16.30
16.31 (* wrapper for calling external prover *)
16.32 @@ -107,6 +112,12 @@
16.33 val binary_min_facts =
16.34 Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
16.35 (K 20)
16.36 +val auto_minimize_min_facts =
16.37 + Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
16.38 + (fn generic => Config.get_generic generic binary_min_facts)
16.39 +val auto_minimize_max_time =
16.40 + Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
16.41 + (K 5.0)
16.42
16.43 fun linear_minimize test timeout result xs =
16.44 let
16.45 @@ -212,6 +223,106 @@
16.46 (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, ""))
16.47 end
16.48
16.49 +fun adjust_reconstructor_params override_params
16.50 + ({debug, verbose, overlord, blocking, provers, type_enc, strict,
16.51 + lam_trans, uncurried_aliases, relevance_thresholds, max_relevant,
16.52 + max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
16.53 + slice, minimize, timeout, preplay_timeout, expect} : params) =
16.54 + let
16.55 + fun lookup_override name default_value =
16.56 + case AList.lookup (op =) override_params name of
16.57 + SOME [s] => SOME s
16.58 + | _ => default_value
16.59 + (* Only those options that reconstructors are interested in are considered
16.60 + here. *)
16.61 + val type_enc = lookup_override "type_enc" type_enc
16.62 + val lam_trans = lookup_override "lam_trans" lam_trans
16.63 + in
16.64 + {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
16.65 + provers = provers, type_enc = type_enc, strict = strict,
16.66 + lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
16.67 + max_relevant = max_relevant, relevance_thresholds = relevance_thresholds,
16.68 + max_mono_iters = max_mono_iters,
16.69 + max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
16.70 + isar_shrink_factor = isar_shrink_factor, slice = slice,
16.71 + minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
16.72 + expect = expect}
16.73 + end
16.74 +
16.75 +fun minimize ctxt mode name
16.76 + (params as {debug, verbose, isar_proof, minimize, ...})
16.77 + ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
16.78 + (result as {outcome, used_facts, run_time, preplay, message,
16.79 + message_tail} : prover_result) =
16.80 + if is_some outcome orelse null used_facts then
16.81 + result
16.82 + else
16.83 + let
16.84 + val num_facts = length used_facts
16.85 + val ((perhaps_minimize, (minimize_name, params)), preplay) =
16.86 + if mode = Normal then
16.87 + if num_facts >= Config.get ctxt auto_minimize_min_facts then
16.88 + ((true, (name, params)), preplay)
16.89 + else
16.90 + let
16.91 + fun can_min_fast_enough time =
16.92 + 0.001
16.93 + * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
16.94 + <= Config.get ctxt auto_minimize_max_time
16.95 + fun prover_fast_enough () = can_min_fast_enough run_time
16.96 + in
16.97 + if isar_proof then
16.98 + ((prover_fast_enough (), (name, params)), preplay)
16.99 + else
16.100 + let val preplay = preplay () in
16.101 + (case preplay of
16.102 + Played (reconstr, timeout) =>
16.103 + if can_min_fast_enough timeout then
16.104 + (true, extract_reconstructor params reconstr
16.105 + ||> (fn override_params =>
16.106 + adjust_reconstructor_params
16.107 + override_params params))
16.108 + else
16.109 + (prover_fast_enough (), (name, params))
16.110 + | _ => (prover_fast_enough (), (name, params)),
16.111 + K preplay)
16.112 + end
16.113 + end
16.114 + else
16.115 + ((false, (name, params)), preplay)
16.116 + val minimize = minimize |> the_default perhaps_minimize
16.117 + val (used_facts, (preplay, message, _)) =
16.118 + if minimize then
16.119 + minimize_facts minimize_name params (not verbose) subgoal
16.120 + subgoal_count state
16.121 + (filter_used_facts used_facts
16.122 + (map (apsnd single o untranslated_fact) facts))
16.123 + |>> Option.map (map fst)
16.124 + else
16.125 + (SOME used_facts, (preplay, message, ""))
16.126 + in
16.127 + case used_facts of
16.128 + SOME used_facts =>
16.129 + (if debug andalso not (null used_facts) then
16.130 + facts ~~ (0 upto length facts - 1)
16.131 + |> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j))
16.132 + |> filter_used_facts used_facts
16.133 + |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
16.134 + |> commas
16.135 + |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
16.136 + " proof (of " ^ string_of_int (length facts) ^ "): ") "."
16.137 + |> Output.urgent_message
16.138 + else
16.139 + ();
16.140 + {outcome = NONE, used_facts = used_facts, run_time = run_time,
16.141 + preplay = preplay, message = message, message_tail = message_tail})
16.142 + | NONE => result
16.143 + end
16.144 +
16.145 +fun get_minimizing_prover ctxt mode name params minimize_command problem =
16.146 + get_prover ctxt mode name params minimize_command problem
16.147 + |> minimize ctxt mode name params problem
16.148 +
16.149 fun run_minimize (params as {provers, ...}) i refs state =
16.150 let
16.151 val ctxt = Proof.context_of state
17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 11 21:43:19 2012 +0200
17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 11 21:43:19 2012 +0200
17.3 @@ -14,7 +14,7 @@
17.4 type reconstructor = ATP_Proof_Reconstruct.reconstructor
17.5 type play = ATP_Proof_Reconstruct.play
17.6 type minimize_command = ATP_Proof_Reconstruct.minimize_command
17.7 - type relevance_fudge = Sledgehammer_Filter.relevance_fudge
17.8 + type relevance_fudge = Sledgehammer_Filter_Iter.relevance_fudge
17.9
17.10 datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
17.11
17.12 @@ -124,7 +124,7 @@
17.13 open ATP_Proof_Reconstruct
17.14 open Metis_Tactic
17.15 open Sledgehammer_Util
17.16 -open Sledgehammer_Filter
17.17 +open Sledgehammer_Filter_Iter
17.18
17.19 (** The Sledgehammer **)
17.20
18.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 11 21:43:19 2012 +0200
18.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 11 21:43:19 2012 +0200
18.3 @@ -12,15 +12,11 @@
18.4 type relevance_override = Sledgehammer_Filter.relevance_override
18.5 type mode = Sledgehammer_Provers.mode
18.6 type params = Sledgehammer_Provers.params
18.7 - type prover = Sledgehammer_Provers.prover
18.8
18.9 val someN : string
18.10 val noneN : string
18.11 val timeoutN : string
18.12 val unknownN : string
18.13 - val auto_minimize_min_facts : int Config.T
18.14 - val auto_minimize_max_time : real Config.T
18.15 - val get_minimizing_prover : Proof.context -> mode -> string -> prover
18.16 val run_sledgehammer :
18.17 params -> mode -> int -> relevance_override
18.18 -> ((string * string list) list -> string -> minimize_command)
18.19 @@ -34,9 +30,10 @@
18.20 open ATP_Problem_Generate
18.21 open ATP_Proof_Reconstruct
18.22 open Sledgehammer_Util
18.23 -open Sledgehammer_Filter
18.24 +open Sledgehammer_Fact
18.25 open Sledgehammer_Provers
18.26 open Sledgehammer_Minimize
18.27 +open Sledgehammer_Filter
18.28
18.29 val someN = "some"
18.30 val noneN = "none"
18.31 @@ -65,113 +62,6 @@
18.32 (if blocking then "."
18.33 else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
18.34
18.35 -val auto_minimize_min_facts =
18.36 - Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
18.37 - (fn generic => Config.get_generic generic binary_min_facts)
18.38 -val auto_minimize_max_time =
18.39 - Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
18.40 - (K 5.0)
18.41 -
18.42 -fun adjust_reconstructor_params override_params
18.43 - ({debug, verbose, overlord, blocking, provers, type_enc, strict,
18.44 - lam_trans, uncurried_aliases, relevance_thresholds, max_relevant,
18.45 - max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
18.46 - slice, minimize, timeout, preplay_timeout, expect} : params) =
18.47 - let
18.48 - fun lookup_override name default_value =
18.49 - case AList.lookup (op =) override_params name of
18.50 - SOME [s] => SOME s
18.51 - | _ => default_value
18.52 - (* Only those options that reconstructors are interested in are considered
18.53 - here. *)
18.54 - val type_enc = lookup_override "type_enc" type_enc
18.55 - val lam_trans = lookup_override "lam_trans" lam_trans
18.56 - in
18.57 - {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
18.58 - provers = provers, type_enc = type_enc, strict = strict,
18.59 - lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
18.60 - max_relevant = max_relevant, relevance_thresholds = relevance_thresholds,
18.61 - max_mono_iters = max_mono_iters,
18.62 - max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
18.63 - isar_shrink_factor = isar_shrink_factor, slice = slice,
18.64 - minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
18.65 - expect = expect}
18.66 - end
18.67 -
18.68 -fun minimize ctxt mode name
18.69 - (params as {debug, verbose, isar_proof, minimize, ...})
18.70 - ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
18.71 - (result as {outcome, used_facts, run_time, preplay, message,
18.72 - message_tail} : prover_result) =
18.73 - if is_some outcome orelse null used_facts then
18.74 - result
18.75 - else
18.76 - let
18.77 - val num_facts = length used_facts
18.78 - val ((perhaps_minimize, (minimize_name, params)), preplay) =
18.79 - if mode = Normal then
18.80 - if num_facts >= Config.get ctxt auto_minimize_min_facts then
18.81 - ((true, (name, params)), preplay)
18.82 - else
18.83 - let
18.84 - fun can_min_fast_enough time =
18.85 - 0.001
18.86 - * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
18.87 - <= Config.get ctxt auto_minimize_max_time
18.88 - fun prover_fast_enough () = can_min_fast_enough run_time
18.89 - in
18.90 - if isar_proof then
18.91 - ((prover_fast_enough (), (name, params)), preplay)
18.92 - else
18.93 - let val preplay = preplay () in
18.94 - (case preplay of
18.95 - Played (reconstr, timeout) =>
18.96 - if can_min_fast_enough timeout then
18.97 - (true, extract_reconstructor params reconstr
18.98 - ||> (fn override_params =>
18.99 - adjust_reconstructor_params
18.100 - override_params params))
18.101 - else
18.102 - (prover_fast_enough (), (name, params))
18.103 - | _ => (prover_fast_enough (), (name, params)),
18.104 - K preplay)
18.105 - end
18.106 - end
18.107 - else
18.108 - ((false, (name, params)), preplay)
18.109 - val minimize = minimize |> the_default perhaps_minimize
18.110 - val (used_facts, (preplay, message, _)) =
18.111 - if minimize then
18.112 - minimize_facts minimize_name params (not verbose) subgoal
18.113 - subgoal_count state
18.114 - (filter_used_facts used_facts
18.115 - (map (apsnd single o untranslated_fact) facts))
18.116 - |>> Option.map (map fst)
18.117 - else
18.118 - (SOME used_facts, (preplay, message, ""))
18.119 - in
18.120 - case used_facts of
18.121 - SOME used_facts =>
18.122 - (if debug andalso not (null used_facts) then
18.123 - facts ~~ (0 upto length facts - 1)
18.124 - |> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j))
18.125 - |> filter_used_facts used_facts
18.126 - |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
18.127 - |> commas
18.128 - |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
18.129 - " proof (of " ^ string_of_int (length facts) ^ "): ") "."
18.130 - |> Output.urgent_message
18.131 - else
18.132 - ();
18.133 - {outcome = NONE, used_facts = used_facts, run_time = run_time,
18.134 - preplay = preplay, message = message, message_tail = message_tail})
18.135 - | NONE => result
18.136 - end
18.137 -
18.138 -fun get_minimizing_prover ctxt mode name params minimize_command problem =
18.139 - get_prover ctxt mode name params minimize_command problem
18.140 - |> minimize ctxt mode name params problem
18.141 -
18.142 fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
18.143 timeout, expect, ...})
18.144 mode minimize_command only {state, goal, subgoal, subgoal_count, facts}