# HG changeset patch # User blanchet # Date 1322742853 -3600 # Node ID 418846ea4f99655620b0464d077bdea63e6596dc # Parent a25ff4283352f358b68b03aed93165fc0975e107 renamed "slicing" to "slice" diff -r a25ff4283352 -r 418846ea4f99 NEWS --- 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 diff -r a25ff4283352 -r 418846ea4f99 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 diff -r a25ff4283352 -r 418846ea4f99 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- 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 diff -r a25ff4283352 -r 418846ea4f99 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r a25ff4283352 -r 418846ea4f99 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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, diff -r a25ff4283352 -r 418846ea4f99 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 diff -r a25ff4283352 -r 418846ea4f99 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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) diff -r a25ff4283352 -r 418846ea4f99 src/HOL/ex/sledgehammer_tactics.ML --- 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 =