# HG changeset patch # User blanchet # Date 1379709570 -7200 # Node ID 06510d01a07b31a0520b1395c75b34fb2f28b660 # Parent 4d34e267fba9c38474bb97d272b09adcc06f3ecf hard-coded an obscure option diff -r 4d34e267fba9 -r 06510d01a07b src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Sep 20 22:39:30 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Sep 20 22:39:30 2013 +0200 @@ -14,8 +14,7 @@ type isar_proof = Sledgehammer_Proof.isar_proof type preplay_interface = Sledgehammer_Preplay.preplay_interface - val compress_proof : - real -> int -> real -> preplay_interface -> isar_proof -> isar_proof + val compress_proof : real -> int -> preplay_interface -> isar_proof -> isar_proof end @@ -117,16 +116,18 @@ (*** main function ***) +val merge_timeout_slack = 1.2 + (* PRE CONDITION: the proof must be labeled canocially, see Slegehammer_Proof.relabel_proof_canonically *) -fun compress_proof isar_compress isar_compress_degree merge_timeout_slack - ({get_preplay_time, set_preplay_time, preplay_quietly, ...} : preplay_interface) +fun compress_proof isar_compress isar_compress_degree + ({get_preplay_time, set_preplay_time, preplay_quietly, ...} + : preplay_interface) proof = if isar_compress <= 1.0 then proof else let - val (compress_further : unit -> bool, decrement_step_count : unit -> unit) = let diff -r 4d34e267fba9 -r 06510d01a07b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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_compress_degree", "2"), (* TODO: document; right value?? *) - ("merge_timeout_slack", "1.2"), (* TODO: document *) + ("isar_compress_degree", "2"), (* TODO: document *) ("isar_try0", "true"), (* TODO: document *) ("isar_minimize", "true"), (* TODO: document *) ("slice", "true"), @@ -306,7 +305,6 @@ val isar_proofs = lookup_option lookup_bool "isar_proofs" val isar_compress = Real.max (1.0, lookup_real "isar_compress") val isar_compress_degree = Int.max (1, lookup_int "isar_compress_degree") - val merge_timeout_slack = Real.max (1.0, lookup_real "merge_timeout_slack") val isar_try0 = lookup_bool "isar_try0" val isar_minimize = lookup_bool "isar_minimize" val slice = mode <> Auto_Try andalso lookup_bool "slice" @@ -325,8 +323,7 @@ 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_compress_degree = isar_compress_degree, - merge_timeout_slack = merge_timeout_slack, isar_try0 = isar_try0, - isar_minimize = isar_minimize, slice = slice, + isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end diff -r 4d34e267fba9 -r 06510d01a07b src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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 @@ -58,8 +58,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_compress_degree, merge_timeout_slack, isar_try0, - isar_minimize, preplay_timeout, ...} : params) + isar_compress_degree, isar_try0, isar_minimize, + preplay_timeout, ...} : params) silent (prover : prover) timeout i n state facts = let val _ = @@ -81,11 +81,9 @@ 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_compress_degree = isar_compress_degree, - merge_timeout_slack = merge_timeout_slack, - isar_try0 = isar_try0, isar_minimize = isar_minimize, - slice = false, minimize = SOME false, timeout = timeout, - preplay_timeout = preplay_timeout, expect = ""} + isar_compress_degree = isar_compress_degree, isar_try0 = isar_try0, + isar_minimize = isar_minimize, 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)]} @@ -255,9 +253,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_compress_degree, merge_timeout_slack, isar_try0, - isar_minimize, slice, minimize, timeout, preplay_timeout, expect} : - params) = + isar_compress, isar_compress_degree, isar_try0, isar_minimize, slice, + minimize, timeout, preplay_timeout, expect} : params) = let fun lookup_override name default_value = case AList.lookup (op =) override_params name of @@ -275,9 +272,9 @@ 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_compress_degree = isar_compress_degree, - merge_timeout_slack = merge_timeout_slack, isar_try0 = isar_try0, - isar_minimize = isar_minimize, slice = slice, minimize = minimize, - timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} + isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice, + minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, + expect = expect} end fun maybe_minimize ctxt mode do_learn name diff -r 4d34e267fba9 -r 06510d01a07b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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_compress_degree : int, - merge_timeout_slack : real, isar_try0 : bool, isar_minimize : bool, slice : bool, @@ -351,7 +350,6 @@ isar_proofs : bool option, isar_compress : real, isar_compress_degree : int, - merge_timeout_slack : real, isar_try0 : bool, isar_minimize : bool, slice : bool, @@ -679,8 +677,8 @@ (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_compress_degree, merge_timeout_slack, isar_try0, - isar_minimize, slice, timeout, preplay_timeout, ...}) + isar_compress_degree, isar_try0, isar_minimize, slice, + timeout, preplay_timeout, ...}) minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let @@ -956,9 +954,8 @@ () val isar_params = (debug, verbose, preplay_timeout, isar_compress, - isar_compress_degree, merge_timeout_slack, isar_try0, - isar_minimize, pool, fact_names, lifted, sym_tab, atp_proof, - goal) + isar_compress_degree, isar_try0, isar_minimize, 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 diff -r 4d34e267fba9 -r 06510d01a07b src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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 * int * real * bool * bool + bool * bool * Time.time option * real * int * bool * bool * string Symtab.table * (string * stature) list vector * (string * term) list * int Symtab.table * string atp_proof * thm @@ -408,14 +408,14 @@ in chain_proof end type isar_params = - bool * bool * Time.time option * real * int * real * bool * bool + bool * bool * Time.time option * real * int * bool * 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_compress_degree, - merge_timeout_slack, isar_try0, isar_minimize, pool, fact_names, lifted, - sym_tab, atp_proof, goal) + isar_try0, isar_minimize, 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 @@ |> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0) (if isar_proofs = SOME true then isar_compress_degree else 100) - merge_timeout_slack preplay_interface + preplay_interface |> isar_try0 ? try0 preplay_timeout preplay_interface |> minimize_dependencies_and_remove_unrefed_steps isar_minimize preplay_interface