# HG changeset patch # User blanchet # Date 1379709570 -7200 # Node ID 70d370743dc663c36eb0177d21904901d4a17e4f # Parent 06510d01a07b31a0520b1395c75b34fb2f28b660 hardcoded obscure option diff -r 06510d01a07b -r 70d370743dc6 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,7 +14,7 @@ type isar_proof = Sledgehammer_Proof.isar_proof type preplay_interface = Sledgehammer_Preplay.preplay_interface - val compress_proof : real -> int -> preplay_interface -> isar_proof -> isar_proof + val compress_proof : real -> preplay_interface -> isar_proof -> isar_proof end @@ -116,11 +116,12 @@ (*** main function ***) +val compress_degree = 2 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 +fun compress_proof isar_compress ({get_preplay_time, set_preplay_time, preplay_quietly, ...} : preplay_interface) proof = @@ -320,7 +321,7 @@ let val successors = get_successors l in - if length successors > isar_compress_degree + if length successors > compress_degree then steps else compression_loop candidates (try_eliminate cand successors steps) diff -r 06510d01a07b -r 70d370743dc6 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,7 +94,6 @@ ("max_new_mono_instances", "smart"), ("isar_proofs", "smart"), ("isar_compress", "10"), - ("isar_compress_degree", "2"), (* TODO: document *) ("isar_try0", "true"), (* TODO: document *) ("isar_minimize", "true"), (* TODO: document *) ("slice", "true"), @@ -304,7 +303,6 @@ lookup_option lookup_int "max_new_mono_instances" 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 isar_try0 = lookup_bool "isar_try0" val isar_minimize = lookup_bool "isar_minimize" val slice = mode <> Auto_Try andalso lookup_bool "slice" @@ -322,10 +320,9 @@ learn = learn, fact_filter = fact_filter, max_facts = max_facts, 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, - isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice, - minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, - expect = expect} + isar_compress = isar_compress, isar_try0 = isar_try0, + isar_minimize = isar_minimize, slice = slice, minimize = minimize, + timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun get_params mode = extract_params mode o default_raw_params diff -r 06510d01a07b -r 70d370743dc6 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,7 @@ 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, isar_try0, isar_minimize, - preplay_timeout, ...} : params) + isar_try0, isar_minimize, preplay_timeout, ...} : params) silent (prover : prover) timeout i n state facts = let val _ = @@ -81,9 +80,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, isar_try0 = isar_try0, - isar_minimize = isar_minimize, slice = false, minimize = SOME false, - timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} + 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)]} @@ -253,8 +252,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, isar_try0, isar_minimize, slice, - minimize, timeout, preplay_timeout, expect} : params) = + isar_compress, 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 @@ -271,10 +270,9 @@ learn = learn, fact_filter = fact_filter, max_facts = max_facts, 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, - isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice, - minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, - expect = expect} + isar_compress = isar_compress, 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 06510d01a07b -r 70d370743dc6 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 @@ -36,7 +36,6 @@ max_new_mono_instances : int option, isar_proofs : bool option, isar_compress : real, - isar_compress_degree : int, isar_try0 : bool, isar_minimize : bool, slice : bool, @@ -349,7 +348,6 @@ max_new_mono_instances : int option, isar_proofs : bool option, isar_compress : real, - isar_compress_degree : int, isar_try0 : bool, isar_minimize : bool, slice : bool, @@ -677,8 +675,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, isar_try0, isar_minimize, slice, - timeout, preplay_timeout, ...}) + isar_try0, isar_minimize, slice, timeout, + preplay_timeout, ...}) minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let @@ -953,9 +951,9 @@ else () val isar_params = - (debug, verbose, preplay_timeout, isar_compress, - isar_compress_degree, isar_try0, isar_minimize, pool, - fact_names, lifted, sym_tab, atp_proof, goal) + (debug, verbose, preplay_timeout, isar_compress, 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 06510d01a07b -r 70d370743dc6 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,9 +12,9 @@ type one_line_params = Sledgehammer_Print.one_line_params type isar_params = - 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 + bool * bool * Time.time option * real * bool * bool * string Symtab.table + * (string * stature) list vector * (string * term) list * int Symtab.table + * string atp_proof * thm val lam_trans_of_atp_proof : string atp_proof -> string -> string val is_typed_helper_used_in_atp_proof : string atp_proof -> bool @@ -408,14 +408,13 @@ in chain_proof end type isar_params = - 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 + bool * bool * Time.time option * real * 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, - isar_try0, isar_minimize, pool, fact_names, lifted, sym_tab, atp_proof, - goal) + (debug, verbose, preplay_timeout, isar_compress, 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 @@ -591,7 +590,6 @@ isar_proof |> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0) - (if isar_proofs = SOME true then isar_compress_degree else 100) preplay_interface |> isar_try0 ? try0 preplay_timeout preplay_interface |> minimize_dependencies_and_remove_unrefed_steps isar_minimize