# HG changeset patch # User blanchet # Date 1321613232 -3600 # Node ID 57227eedce815acaeacc00e437f98aa1ab3d61dd # Parent 1606122a2d0f547b7ea92725c57a15a4e3038e03 don't propagate user-set "type_enc" or "lam_trans" to Metis calls diff -r 1606122a2d0f -r 57227eedce81 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Nov 18 11:47:12 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Nov 18 11:47:12 2011 +0100 @@ -80,7 +80,7 @@ val plain_metis : reconstructor val select_smt_solver : string -> Proof.context -> Proof.context val extract_reconstructor : - reconstructor -> string * (string * string list) list + params -> reconstructor -> string * (string * string list) list val is_reconstructor : string -> bool val is_atp : theory -> string -> bool val is_smt_prover : Proof.context -> string -> bool @@ -132,29 +132,10 @@ "Async_Manager". *) val das_tool = "Sledgehammer" -fun extract_reconstructor (Metis (type_enc, lam_trans)) = - let - val override_params = - (if type_enc = hd partial_type_encs then [] - else [("type_enc", [type_enc])]) @ - (if lam_trans = metis_default_lam_trans then [] - else [("lam_trans", [lam_trans])]) - in (metisN, override_params) end - | extract_reconstructor SMT = (smtN, []) - val reconstructor_names = [metisN, smtN] val plain_metis = Metis (hd partial_type_encs, combinatorsN) +val is_reconstructor = member (op =) reconstructor_names -fun bunch_of_reconstructors needs_full_types lam_trans = - [(false, Metis (hd partial_type_encs, lam_trans true)), - (true, Metis (hd full_type_encs, lam_trans false)), - (false, Metis (no_type_enc, lam_trans false)), - (true, SMT)] - |> map_filter (fn (full_types, reconstr) => - if needs_full_types andalso not full_types then NONE - else SOME reconstr) - -val is_reconstructor = member (op =) reconstructor_names val is_atp = member (op =) o supported_atps val select_smt_solver = Context.proof_map o SMT_Config.select_solver @@ -415,6 +396,30 @@ | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" | _ => "Try this" +fun bunch_of_reconstructors needs_full_types lam_trans = + [(false, Metis (hd partial_type_encs, lam_trans true)), + (true, Metis (hd full_type_encs, lam_trans false)), + (false, Metis (no_type_enc, lam_trans false)), + (true, SMT)] + |> map_filter (fn (full_types, reconstr) => + if needs_full_types andalso not full_types then NONE + else SOME reconstr) + +fun extract_reconstructor ({type_enc, lam_trans, ...} : params) + (Metis (type_enc', lam_trans')) = + let + val override_params = + (if is_none type_enc andalso type_enc' = hd partial_type_encs then + [] + else + [("type_enc", [type_enc'])]) @ + (if is_none lam_trans andalso lam_trans' = metis_default_lam_trans then + [] + else + [("lam_trans", [lam_trans'])]) + in (metisN, override_params) end + | extract_reconstructor _ SMT = (smtN, []) + (* based on "Mirabelle.can_apply" and generalized *) fun timed_apply timeout tac state i = let @@ -541,13 +546,13 @@ val metis_minimize_max_time = seconds 2.0 -fun choose_minimize_command minimize_command name preplay = +fun choose_minimize_command params minimize_command name preplay = let val (name, override_params) = case preplay of Played (reconstr, time) => if Time.<= (time, metis_minimize_max_time) then - extract_reconstructor reconstr + extract_reconstructor params reconstr else (name, []) | _ => (name, []) @@ -570,9 +575,10 @@ fun run_atp mode name ({exec, required_execs, arguments, proof_delims, known_failures, conj_sym_kind, prem_kind, best_slices, ...} : atp_config) - ({debug, verbose, overlord, type_enc, sound, lam_trans, max_relevant, - max_mono_iters, max_new_mono_instances, isar_proof, - isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params) + (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, + preplay_timeout, ...}) minimize_command ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = let @@ -807,7 +813,7 @@ atp_proof, goal) val one_line_params = (preplay, proof_banner mode name, used_facts, - choose_minimize_command minimize_command name preplay, + choose_minimize_command params minimize_command name preplay, subgoal, subgoal_count) in proof_text ctxt isar_proof isar_params one_line_params end, (if verbose then @@ -987,7 +993,7 @@ let val one_line_params = (preplay, proof_banner mode name, used_facts, - choose_minimize_command minimize_command name preplay, + choose_minimize_command params minimize_command name preplay, subgoal, subgoal_count) in one_line_proof_text one_line_params end, if verbose then @@ -1002,7 +1008,7 @@ end fun run_reconstructor mode name - ({debug, verbose, timeout, type_enc, lam_trans, ...} : params) + (params as {debug, verbose, timeout, type_enc, lam_trans, ...}) minimize_command ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = let @@ -1023,14 +1029,15 @@ play as Played (_, time) => {outcome = NONE, used_facts = used_facts, run_time = time, preplay = K play, - message = fn play => - let - val (_, override_params) = extract_reconstructor reconstr - val one_line_params = - (play, proof_banner mode name, used_facts, - minimize_command override_params name, subgoal, - subgoal_count) - in one_line_proof_text one_line_params end, + message = + fn play => + let + val (_, override_params) = extract_reconstructor params reconstr + val one_line_params = + (play, proof_banner mode name, used_facts, + minimize_command override_params name, subgoal, + subgoal_count) + in one_line_proof_text one_line_params end, message_tail = ""} | play => let diff -r 1606122a2d0f -r 57227eedce81 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Nov 18 11:47:12 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Nov 18 11:47:12 2011 +0100 @@ -125,7 +125,7 @@ (case preplay of Played (reconstr, timeout) => if can_min_fast_enough timeout then - (true, extract_reconstructor reconstr + (true, extract_reconstructor params reconstr ||> (fn override_params => adjust_reconstructor_params override_params params))