--- a/NEWS Thu Dec 01 13:34:12 2011 +0100
+++ b/NEWS Thu Dec 01 13:34:13 2011 +0100
@@ -148,6 +148,7 @@
* Sledgehammer:
- Added "lam_trans" option.
+ - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
* Metis:
- Added possibility to specify lambda translations scheme as a
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Dec 01 13:34:12 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Dec 01 13:34:13 2011 +0100
@@ -10,7 +10,7 @@
val keepK = "keep"
val type_encK = "type_enc"
val soundK = "sound"
-val slicingK = "slicing"
+val sliceK = "slice"
val lam_transK = "lam_trans"
val e_weight_methodK = "e_weight_method"
val force_sosK = "force_sos"
@@ -361,7 +361,7 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
+fun run_sh prover_name prover type_enc sound max_relevant slice lam_trans
e_weight_method force_sos hard_timeout timeout dir pos st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
@@ -381,7 +381,7 @@
e_weight_method |> the_default I)
#> (Option.map (Config.put ATP_Systems.force_sos)
force_sos |> the_default I))
- val params as {relevance_thresholds, max_relevant, slicing, ...} =
+ val params as {relevance_thresholds, max_relevant, slice, ...} =
Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),
("type_enc", type_enc),
@@ -389,11 +389,11 @@
("lam_trans", lam_trans |> the_default "smart"),
("preplay_timeout", preplay_timeout),
("max_relevant", max_relevant),
- ("slicing", slicing),
+ ("slice", slice),
("timeout", string_of_int timeout),
("preplay_timeout", preplay_timeout)]
val default_max_relevant =
- Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
+ Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
prover_name
val is_appropriate_prop =
Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name
@@ -469,7 +469,7 @@
val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
val sound = AList.lookup (op =) args soundK |> the_default "false"
val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
- val slicing = AList.lookup (op =) args slicingK |> the_default "true"
+ val slice = AList.lookup (op =) args sliceK |> the_default "true"
val lam_trans = AList.lookup (op =) args lam_transK
val e_weight_method = AList.lookup (op =) args e_weight_methodK
val force_sos = AList.lookup (op =) args force_sosK
@@ -480,7 +480,7 @@
minimizer has a chance to do its magic *)
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
- run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
+ run_sh prover_name prover type_enc sound max_relevant slice lam_trans
e_weight_method force_sos hard_timeout timeout dir pos st
in
case result of
@@ -555,7 +555,7 @@
("max_relevant", "0"),
("type_enc", type_enc),
("sound", "true"),
- ("slicing", "false"),
+ ("slice", "false"),
("timeout", timeout |> Time.toSeconds |> string_of_int)]
fun run_reconstructor trivial full m name reconstructor named_thms id
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Dec 01 13:34:12 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Dec 01 13:34:13 2011 +0100
@@ -113,10 +113,10 @@
val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
val prover = AList.lookup (op =) args "prover"
|> the_default default_prover
- val {relevance_thresholds, max_relevant, slicing, ...} =
+ val {relevance_thresholds, max_relevant, slice, ...} =
Sledgehammer_Isar.default_params ctxt args
val default_max_relevant =
- Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
+ Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
prover
val is_appropriate_prop =
Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Dec 01 13:34:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Dec 01 13:34:13 2011 +0100
@@ -95,7 +95,7 @@
("max_new_mono_instances", "200"),
("isar_proof", "false"),
("isar_shrink_factor", "1"),
- ("slicing", "true"),
+ ("slice", "true"),
("preplay_timeout", "4")]
val alias_params =
@@ -107,7 +107,7 @@
("non_blocking", "blocking"),
("unsound", "sound"),
("no_isar_proof", "isar_proof"),
- ("no_slicing", "slicing")]
+ ("dont_slice", "slice")]
val params_for_minimize =
["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans",
@@ -289,7 +289,7 @@
val max_new_mono_instances = lookup_int "max_new_mono_instances"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
- val slicing = mode <> Auto_Try andalso lookup_bool "slicing"
+ val slice = mode <> Auto_Try andalso lookup_bool "slice"
val timeout =
(if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout
val preplay_timeout =
@@ -302,8 +302,8 @@
lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
max_relevant = max_relevant, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
- isar_shrink_factor = isar_shrink_factor, slicing = slicing,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ isar_shrink_factor = isar_shrink_factor, slice = slice, 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 Thu Dec 01 13:34:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Dec 01 13:34:13 2011 +0100
@@ -65,7 +65,7 @@
lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
- isar_shrink_factor = isar_shrink_factor, slicing = false,
+ isar_shrink_factor = isar_shrink_factor, slice = false,
timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 01 13:34:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 01 13:34:13 2011 +0100
@@ -33,7 +33,7 @@
max_new_mono_instances: int,
isar_proof: bool,
isar_shrink_factor: int,
- slicing: bool,
+ slice: bool,
timeout: Time.time,
preplay_timeout: Time.time,
expect: string}
@@ -163,18 +163,18 @@
is_reconstructor orf is_smt_prover ctxt orf
is_atp_installed (Proof_Context.theory_of ctxt)
-fun get_slices slicing slices =
- (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
+fun get_slices slice slices =
+ (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
val reconstructor_default_max_relevant = 20
-fun default_max_relevant_for_prover ctxt slicing name =
+fun default_max_relevant_for_prover ctxt slice name =
let val thy = Proof_Context.theory_of ctxt in
if is_reconstructor name then
reconstructor_default_max_relevant
else if is_atp thy name then
fold (Integer.max o #1 o snd o snd o snd)
- (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
+ (get_slices slice (#best_slices (get_atp thy name) ctxt)) 0
else (* is_smt_prover ctxt name *)
SMT_Solver.default_max_relevant ctxt name
end
@@ -296,7 +296,7 @@
max_new_mono_instances: int,
isar_proof: bool,
isar_shrink_factor: int,
- slicing: bool,
+ slice: bool,
timeout: Time.time,
preplay_timeout: Time.time,
expect: string}
@@ -578,7 +578,7 @@
conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
(params as {debug, verbose, overlord, type_enc, sound, lam_trans,
max_relevant, max_mono_iters, max_new_mono_instances,
- isar_proof, isar_shrink_factor, slicing, timeout,
+ isar_proof, isar_shrink_factor, slice, timeout,
preplay_timeout, ...})
minimize_command
({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
@@ -624,7 +624,7 @@
let
(* If slicing is disabled, we expand the last slice to fill the
entire time available. *)
- val actual_slices = get_slices slicing (best_slices ctxt)
+ val actual_slices = get_slices slice (best_slices ctxt)
val num_actual_slices = length actual_slices
fun monomorphize_facts facts =
let
@@ -873,10 +873,10 @@
fun smt_filter_loop ctxt name
({debug, verbose, overlord, max_mono_iters,
- max_new_mono_instances, timeout, slicing, ...} : params)
+ max_new_mono_instances, timeout, slice, ...} : params)
state i smt_filter =
let
- val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
+ val max_slices = if slice then Config.get ctxt smt_max_slices else 1
val repair_context =
select_smt_solver name
#> Config.put SMT_Config.verbose debug
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Dec 01 13:34:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Dec 01 13:34:13 2011 +0100
@@ -75,8 +75,8 @@
fun adjust_reconstructor_params override_params
({debug, verbose, overlord, blocking, provers, type_enc, sound,
lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
- max_new_mono_instances, isar_proof, isar_shrink_factor, slicing,
- timeout, preplay_timeout, expect} : params) =
+ max_new_mono_instances, isar_proof, isar_shrink_factor, slice, timeout,
+ preplay_timeout, expect} : params) =
let
fun lookup_override name default_value =
case AList.lookup (op =) override_params name of
@@ -93,8 +93,8 @@
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, slicing = slicing,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,
+ preplay_timeout = preplay_timeout, expect = expect}
end
fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
@@ -172,7 +172,7 @@
fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true
| is_induction_fact _ = false
-fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,
+fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
timeout, expect, ...})
mode minimize_command only
{state, goal, subgoal, subgoal_count, facts, smt_filter} name =
@@ -183,7 +183,7 @@
val death_time = Time.+ (birth_time, hard_timeout)
val max_relevant =
max_relevant
- |> the_default (default_max_relevant_for_prover ctxt slicing name)
+ |> the_default (default_max_relevant_for_prover ctxt slice name)
val num_facts = length facts |> not only ? Integer.min max_relevant
fun desc () =
prover_description ctxt params name num_facts subgoal subgoal_count goal
@@ -277,7 +277,7 @@
val auto_try_max_relevant_divisor = 2 (* FUDGE *)
fun run_sledgehammer (params as {debug, verbose, blocking, provers,
- relevance_thresholds, max_relevant, slicing,
+ relevance_thresholds, max_relevant, slice,
timeout, ...})
mode i (relevance_override as {only, ...}) minimize_command state =
if null provers then
@@ -338,7 +338,7 @@
SOME n => n
| NONE =>
0 |> fold (Integer.max
- o default_max_relevant_for_prover ctxt slicing)
+ o default_max_relevant_for_prover ctxt slice)
provers
|> mode = Auto_Try
? (fn n => n div auto_try_max_relevant_divisor)
--- a/src/HOL/ex/sledgehammer_tactics.ML Thu Dec 01 13:34:12 2011 +0100
+++ b/src/HOL/ex/sledgehammer_tactics.ML Thu Dec 01 13:34:13 2011 +0100
@@ -25,13 +25,13 @@
fun run_atp override_params relevance_override i n ctxt goal =
let
val chained_ths = [] (* a tactic has no chained ths *)
- val params as {provers, relevance_thresholds, max_relevant, slicing, ...} =
+ val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
Sledgehammer_Isar.default_params ctxt override_params
val name = hd provers
val prover =
Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
val default_max_relevant =
- Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
+ Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
val is_built_in_const =
Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
val relevance_fudge =