--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 20 22:39:30 2013 +0200
@@ -94,8 +94,7 @@
("max_new_mono_instances", "smart"),
("isar_proofs", "smart"),
("isar_compress", "10"),
- ("isar_try0", "true"), (* TODO: document *)
- ("isar_minimize", "true"), (* TODO: document *)
+ ("isar_try0", "true"),
("slice", "true"),
("minimize", "smart"),
("preplay_timeout", "3")]
@@ -116,8 +115,7 @@
("no_isar_proofs", "isar_proofs"),
("dont_slice", "slice"),
("dont_minimize", "minimize"),
- ("dont_try0_isar", "isar_try0"),
- ("dont_minimize_isar", "isar_minimize")]
+ ("dont_try0_isar", "isar_try0")]
val params_not_for_minimize =
["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice",
@@ -304,7 +302,6 @@
val isar_proofs = lookup_option lookup_bool "isar_proofs"
val isar_compress = Real.max (1.0, lookup_real "isar_compress")
val isar_try0 = lookup_bool "isar_try0"
- val isar_minimize = lookup_bool "isar_minimize"
val slice = mode <> Auto_Try andalso lookup_bool "slice"
val minimize =
if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
@@ -320,9 +317,9 @@
learn = learn, fact_filter = fact_filter, max_facts = max_facts,
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- isar_compress = isar_compress, isar_try0 = isar_try0,
- isar_minimize = isar_minimize, slice = slice, minimize = minimize,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice,
+ minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
+ expect = expect}
end
fun get_params mode = extract_params mode o default_raw_params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Sep 20 22:39:30 2013 +0200
@@ -57,8 +57,8 @@
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
max_new_mono_instances, type_enc, strict, lam_trans,
- uncurried_aliases, isar_proofs, isar_compress,
- isar_try0, isar_minimize, preplay_timeout, ...} : params)
+ uncurried_aliases, isar_proofs, isar_compress, isar_try0,
+ preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state facts =
let
val _ =
@@ -80,9 +80,8 @@
fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances,
isar_proofs = isar_proofs, isar_compress = isar_compress,
- isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = false,
- minimize = SOME false, timeout = timeout,
- preplay_timeout = preplay_timeout, expect = ""}
+ isar_try0 = isar_try0, slice = false, minimize = SOME false,
+ timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
factss = [("", facts)]}
@@ -252,8 +251,8 @@
({debug, verbose, overlord, blocking, provers, type_enc, strict,
lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
- isar_compress, isar_try0, isar_minimize, slice, minimize, timeout,
- preplay_timeout, expect} : params) =
+ isar_compress, isar_try0, slice, minimize, timeout, preplay_timeout,
+ expect} : params) =
let
fun lookup_override name default_value =
case AList.lookup (op =) override_params name of
@@ -270,9 +269,9 @@
learn = learn, fact_filter = fact_filter, max_facts = max_facts,
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- isar_compress = isar_compress, isar_try0 = isar_try0,
- isar_minimize = isar_minimize, slice = slice, minimize = minimize,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice,
+ minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
+ expect = expect}
end
fun maybe_minimize ctxt mode do_learn name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Fri Sep 20 22:39:30 2013 +0200
@@ -49,8 +49,8 @@
mk_step_lfs_gfs min_lfs min_gfs
end)
-fun minimize_dependencies_and_remove_unrefed_steps
- isar_minimize preplay_interface proof =
+fun minimize_dependencies_and_remove_unrefed_steps isar_try0 preplay_interface
+ proof =
let
fun cons_to xs x = x :: xs
@@ -86,7 +86,7 @@
and do_refed_step step =
step
- |> isar_minimize ? min_deps_of_step preplay_interface
+ |> isar_try0 ? min_deps_of_step preplay_interface
|> do_refed_step'
and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
@@ -101,7 +101,6 @@
in
(refed, step)
end
-
in
snd (do_proof proof)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Sep 20 22:39:30 2013 +0200
@@ -37,7 +37,6 @@
isar_proofs : bool option,
isar_compress : real,
isar_try0 : bool,
- isar_minimize : bool,
slice : bool,
minimize : bool option,
timeout : Time.time option,
@@ -349,7 +348,6 @@
isar_proofs : bool option,
isar_compress : real,
isar_try0 : bool,
- isar_minimize : bool,
slice : bool,
minimize : bool option,
timeout : Time.time option,
@@ -675,8 +673,7 @@
(params as {debug, verbose, overlord, type_enc, strict, lam_trans,
uncurried_aliases, fact_filter, max_facts, max_mono_iters,
max_new_mono_instances, isar_proofs, isar_compress,
- isar_try0, isar_minimize, slice, timeout,
- preplay_timeout, ...})
+ isar_try0, slice, timeout, preplay_timeout, ...})
minimize_command
({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
@@ -952,8 +949,7 @@
()
val isar_params =
(debug, verbose, preplay_timeout, isar_compress, isar_try0,
- isar_minimize, pool, fact_names, lifted, sym_tab, atp_proof,
- goal)
+ pool, fact_names, lifted, sym_tab, atp_proof, goal)
val one_line_params =
(preplay, proof_banner mode name, used_facts,
choose_minimize_command ctxt params minimize_command name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 20 22:39:30 2013 +0200
@@ -12,7 +12,7 @@
type one_line_params = Sledgehammer_Print.one_line_params
type isar_params =
- bool * bool * Time.time option * real * bool * bool * string Symtab.table
+ bool * bool * Time.time option * real * bool * string Symtab.table
* (string * stature) list vector * (string * term) list * int Symtab.table
* string atp_proof * thm
@@ -408,13 +408,13 @@
in chain_proof end
type isar_params =
- bool * bool * Time.time option * real * bool * bool * string Symtab.table
+ bool * bool * Time.time option * real * bool * string Symtab.table
* (string * stature) list vector * (string * term) list * int Symtab.table
* string atp_proof * thm
fun isar_proof_text ctxt isar_proofs
- (debug, verbose, preplay_timeout, isar_compress, isar_try0, isar_minimize,
- pool, fact_names, lifted, sym_tab, atp_proof, goal)
+ (debug, verbose, preplay_timeout, isar_compress, isar_try0, pool,
+ fact_names, lifted, sym_tab, atp_proof, goal)
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
@@ -592,7 +592,7 @@
(if isar_proofs = SOME true then isar_compress else 1000.0)
preplay_interface
|> isar_try0 ? try0 preplay_timeout preplay_interface
- |> minimize_dependencies_and_remove_unrefed_steps isar_minimize
+ |> minimize_dependencies_and_remove_unrefed_steps isar_try0
preplay_interface
|> `overall_preplay_stats
||> clean_up_labels_in_proof