--- a/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100
@@ -35,32 +35,4 @@
ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
-(*
-lemma "1 + 1 = 2"
- sledgehammer [slices = 40, max_proofs = 40]
-
-lemma "1 + 1 = 2"
- sledgehammer [verbose, slices = 4]
- oops
-*)
-
-(*
-lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x"
- sledgehammer [max_proofs = 3]
- oops
-*)
-
-(*
-declare nat_induct[no_atp]
-declare nat_induct_non_zero[no_atp]
-
-lemma "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"
- sledgehammer [cvc4] (add: nat.induct)
-*)
-
-(*
-lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x"
- sledgehammer [verbose, e, dont_preplay, max_facts = 2] (add_0_left one_add_one)
-*)
-
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
@@ -134,7 +134,7 @@
|> (fn (used_facts, (meth, play)) =>
(used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play)))
-fun launch_prover (params as {verbose, spy, ...}) mode learn
+fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn
(problem as {state, subgoal, factss, ...} : prover_problem)
(slice as ((num_facts, fact_filter), _)) name =
let
@@ -145,7 +145,7 @@
val _ =
if verbose then
writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^
- plural_s num_facts ^ "...")
+ plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slices timeout) ^ "...")
else
()
@@ -294,7 +294,8 @@
@ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers)
end
-fun prover_slices_of_schedule ctxt ({max_facts, fact_filter, ...} : params) schedule =
+fun prover_slices_of_schedule ctxt
+ ({max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases, ...} : params) schedule =
let
fun triplicate_slices original =
let
@@ -310,7 +311,9 @@
original @ shifted_once @ shifted_twice
end
- fun adjust_extra XXX = XXX (* ### FIXME *)
+ fun adjust_extra (format0, type_enc0, lam_trans0, uncurried_aliases0, extra_extra0) =
+ (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans,
+ the_default uncurried_aliases0 uncurried_aliases, extra_extra0)
fun adjust_slice ((num_facts0, fact_filter0), extra) =
((case max_facts of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100
@@ -47,10 +47,9 @@
names are enabled by default. *)
val atp_full_names = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_atp_full_names\<close> (K false)
-fun choose_type_enc strictness best_type_enc format =
- the_default best_type_enc
- #> type_enc_of_string strictness
- #> adjust_type_enc format
+fun choose_type_enc strictness format good_type_enc =
+ type_enc_of_string strictness good_type_enc
+ |> adjust_type_enc format
fun has_bound_or_var_of_type pred =
exists_subterm (fn Var (_, T as Type _) => pred T
@@ -103,9 +102,9 @@
val atp_important_message_keep_quotient = 25
fun run_atp mode name
- ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter,
- max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs,
- minimize, slices, timeout, preplay_timeout, spy, ...} : params)
+ ({debug, verbose, overlord, strict, fact_filter, max_facts, max_mono_iters,
+ max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slices, timeout,
+ preplay_timeout, spy, ...} : params)
({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem)
slice =
let
@@ -191,7 +190,7 @@
| SOME max_facts => max_facts)
|> Integer.min (length facts)
val strictness = if strict then Strict else Non_Strict
- val type_enc = type_enc |> choose_type_enc strictness good_type_enc good_format
+ val type_enc = choose_type_enc strictness good_format good_type_enc
val run_timeout = slice_timeout slices timeout
val generous_run_timeout = if mode = MaSh then one_day else run_timeout
val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () =>
@@ -199,8 +198,6 @@
val sound = is_type_enc_sound type_enc
val generate_info = (case good_format of DFG _ => true | _ => false)
val readable_names = not (Config.get ctxt atp_full_names)
- val lam_trans = lam_trans |> the_default good_lam_trans
- val uncurried_aliases = uncurried_aliases |> the_default good_uncurried_aliases
in
facts
|> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd)
@@ -208,7 +205,7 @@
|> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
|> map (apsnd Thm.prop_of)
|> generate_atp_problem ctxt generate_info good_format prem_role type_enc atp_mode
- lam_trans uncurried_aliases readable_names true hyp_ts concl_t
+ good_lam_trans good_uncurried_aliases readable_names true hyp_ts concl_t
end) ()
val () = spying spy (fn () =>