--- 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)
--- 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
--- 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
--- 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
--- 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