# HG changeset patch # User blanchet # Date 1321391751 -3600 # Node ID a6cce8032fffba23ae8acf1741b0cd7a8ae7cd35 # Parent 9b0f8ca4388e0212632caf6da1bd5eeaf329772f rename configuration option to more reasonable length diff -r 9b0f8ca4388e -r a6cce8032fff src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 15 22:15:51 2011 +0100 @@ -11,7 +11,7 @@ val type_encK = "type_enc" val soundK = "sound" val slicingK = "slicing" -val lambda_translationK = "lambda_translation" +val lambda_transK = "lambda_trans" val e_weight_methodK = "e_weight_method" val force_sosK = "force_sos" val max_relevantK = "max_relevant" @@ -355,9 +355,8 @@ SH_FAIL of int * int | SH_ERROR -fun run_sh prover_name prover type_enc sound max_relevant slicing - lambda_translation e_weight_method force_sos hard_timeout timeout dir - pos st = +fun run_sh prover_name prover type_enc sound max_relevant slicing lambda_trans + e_weight_method force_sos hard_timeout timeout dir pos st = let val {context = ctxt, facts = chained_ths, goal} = Proof.goal st val i = 1 @@ -373,8 +372,8 @@ st |> Proof.map_context (set_file_name dir #> (Option.map (Config.put - Sledgehammer_Provers.atp_lambda_translation) - lambda_translation |> the_default I) + Sledgehammer_Provers.atp_lambda_trans) + lambda_trans |> the_default I) #> (Option.map (Config.put ATP_Systems.e_weight_method) e_weight_method |> the_default I) #> (Option.map (Config.put ATP_Systems.force_sos) @@ -466,7 +465,7 @@ 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 lambda_translation = AList.lookup (op =) args lambda_translationK + val lambda_trans = AList.lookup (op =) args lambda_transK val e_weight_method = AList.lookup (op =) args e_weight_methodK val force_sos = AList.lookup (op =) args force_sosK |> Option.map (curry (op <>) "false") @@ -476,9 +475,8 @@ 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 - lambda_translation e_weight_method force_sos hard_timeout timeout dir - pos st + run_sh prover_name prover type_enc sound max_relevant slicing lambda_trans + e_weight_method force_sos hard_timeout timeout dir pos st in case result of SH_OK (time_isa, time_prover, names) => diff -r 9b0f8ca4388e -r a6cce8032fff src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 22:15:51 2011 +0100 @@ -243,7 +243,7 @@ fun generic_metis_tac type_syss ctxt ths i st0 = let - val lambda_trans = Config.get ctxt lambda_translation + val lambda_trans = Config.get ctxt lambda_trans val _ = trace_msg ctxt (fn () => "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths)) diff -r 9b0f8ca4388e -r a6cce8032fff src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 22:15:51 2011 +0100 @@ -24,7 +24,7 @@ val metis_generated_var_prefix : string val trace : bool Config.T val verbose : bool Config.T - val lambda_translation : string Config.T + val lambda_trans : string Config.T val trace_msg : Proof.context -> (unit -> string) -> unit val verbose_warning : Proof.context -> string -> unit val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list @@ -52,9 +52,8 @@ val trace = Attrib.setup_config_bool @{binding metis_trace} (K false) val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true) -val lambda_translation = - Attrib.setup_config_string @{binding metis_lambda_translation} - (K combinatorsN) +val lambda_trans = + Attrib.setup_config_string @{binding metis_lambda_trans} (K combinatorsN) fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () fun verbose_warning ctxt msg = diff -r 9b0f8ca4388e -r a6cce8032fff src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 15 22:13:39 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 15 22:15:51 2011 +0100 @@ -62,7 +62,7 @@ val dest_dir : string Config.T val problem_prefix : string Config.T - val atp_lambda_translation : string Config.T + val atp_lambda_trans : string Config.T val atp_full_names : bool Config.T val smt_triggers : bool Config.T val smt_weights : bool Config.T @@ -339,9 +339,8 @@ val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob") -val atp_lambda_translation = - Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation} - (K smartN) +val atp_lambda_trans = + Attrib.setup_config_string @{binding sledgehammer_atp_lambda_trans} (K smartN) (* In addition to being easier to read, readable names are often much shorter, especially if types are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short names are enabled by default. *) @@ -674,7 +673,7 @@ val (atp_problem, pool, conjecture_offset, facts_offset, fact_names, typed_helpers, _, sym_tab) = prepare_atp_problem ctxt format conj_sym_kind prem_kind - type_enc false (Config.get ctxt atp_lambda_translation) + type_enc false (Config.get ctxt atp_lambda_trans) (not (Config.get ctxt atp_full_names)) true hyp_ts concl_t facts fun weights () = atp_problem_weights atp_problem