--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Dec 19 18:07:21 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Dec 19 18:22:31 2013 +0100
@@ -93,7 +93,7 @@
(* Precondition: The proof must be labeled canonically
(cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
fun compress_proof isar_compress
- ({get_preplay_time, set_preplay_time, preplay_quietly, ...} : preplay_interface) proof =
+ ({get_preplay_result, set_preplay_result, preplay_quietly, ...} : preplay_interface) proof =
if isar_compress <= 1.0 then
proof
else
@@ -135,7 +135,7 @@
fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
if null subs orelse not (compress_further ()) then
- (set_preplay_time l (false, time);
+ (set_preplay_result l (Preplay_Success (false, time));
Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
else
(case subs of
@@ -145,7 +145,7 @@
val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
(* only touch proofs that can be preplayed sucessfully *)
- val (false, time') = get_preplay_time l'
+ val Preplay_Success (false, time') = get_preplay_result l'
(* merge steps *)
val subs'' = subs @ nontriv_subs
@@ -174,9 +174,10 @@
if subproofs = [] then
step
else
- (case get_preplay_time l of
- (true, _) => step (* timeout or fail *)
- | (false, time) => elim_subproofs' time qs fix l t lfs gfs meth subproofs [])
+ (case get_preplay_result l of
+ Preplay_Success (false, time) =>
+ elim_subproofs' time qs fix l t lfs gfs meth subproofs []
+ | _ => step)
(** top_level compression: eliminate steps by merging them into their
successors **)
@@ -210,9 +211,10 @@
fun try_eliminate (i, l, _) succ_lbls steps =
let
(* only touch steps that can be preplayed successfully *)
- val (false, time) = get_preplay_time l
+ val Preplay_Success (false, time) = get_preplay_result l
- val succ_times = map (get_preplay_time #> (fn (false, t) => t)) succ_lbls
+ val succ_times =
+ map (get_preplay_result #> (fn Preplay_Success (false, t) => t)) succ_lbls
val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
val timeouts =
map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
@@ -240,7 +242,7 @@
val steps2 = update_steps steps2 succs'
in
decrement_step_count (); (* candidate successfully eliminated *)
- map2 set_preplay_time succ_lbls preplay_times;
+ map2 (fn l => set_preplay_result l o Preplay_Success) succ_lbls preplay_times;
map (replace_successor l succ_lbls) lfs;
(* removing the step would mess up the indices -> replace with dummy step instead *)
steps1 @ dummy_isar_step :: steps2
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Thu Dec 19 18:07:21 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Thu Dec 19 18:22:31 2013 +0100
@@ -25,11 +25,10 @@
val slack = seconds 0.1
fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
- | min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...}
+ | min_deps_of_step {get_preplay_result, set_preplay_result, preplay_quietly, ...}
(step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
- (case get_preplay_time l of
- (true, _) => step (* don't touch steps that time out or fail *)
- | (false, time) =>
+ (case get_preplay_result l of
+ Preplay_Success (false, time) =>
let
fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
@@ -43,8 +42,9 @@
val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
in
- set_preplay_time l (false, time); mk_step_lfs_gfs min_lfs min_gfs
- end)
+ set_preplay_result l (Preplay_Success (false, time)); mk_step_lfs_gfs min_lfs min_gfs
+ end
+ | _ => step (* don't touch steps that time out or fail *))
fun postprocess_remove_unreferenced_steps postproc_step =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Dec 19 18:07:21 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Dec 19 18:22:31 2013 +0100
@@ -11,18 +11,16 @@
type isar_step = Sledgehammer_Proof.isar_step
type label = Sledgehammer_Proof.label
- type preplay_result
+ datatype preplay_result =
+ Preplay_Success of bool * Time.time |
+ Preplay_Failure
val trace: bool Config.T
- val zero_preplay_time: bool * Time.time
- val some_preplay_time: bool * Time.time
val add_preplay_time: bool * Time.time -> bool * Time.time -> bool * Time.time
type preplay_interface =
{get_preplay_result: label -> preplay_result,
set_preplay_result: label -> preplay_result -> unit,
- get_preplay_time: label -> bool * Time.time,
- set_preplay_time: label -> bool * Time.time -> unit,
preplay_quietly: Time.time -> isar_step -> bool * Time.time,
(* the returned flag signals a preplay failure *)
overall_preplay_stats: isar_proof -> (bool * Time.time) * bool}
@@ -45,7 +43,6 @@
Preplay_Failure
val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
-val some_preplay_time = (true, Time.zeroTime) (* > 0 ms *)
fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+ (t1, t2))
@@ -166,8 +163,6 @@
type preplay_interface =
{get_preplay_result: label -> preplay_result,
set_preplay_result: label -> preplay_result -> unit,
- get_preplay_time: label -> bool * Time.time,
- set_preplay_time: label -> bool * Time.time -> unit,
preplay_quietly: Time.time -> isar_step -> bool * Time.time,
(* the returned flag signals a preplay failure *)
overall_preplay_stats: isar_proof -> (bool * Time.time) * bool}
@@ -201,8 +196,6 @@
(* the dont_preplay option pretends that everything works just fine *)
{get_preplay_result = K (Preplay_Success zero_preplay_time),
set_preplay_result = K (K ()),
- get_preplay_time = K zero_preplay_time,
- set_preplay_time = K (K ()),
preplay_quietly = K (K zero_preplay_time),
overall_preplay_stats = K (zero_preplay_time, false)} : preplay_interface
else
@@ -250,13 +243,6 @@
fun set_preplay_result l result =
preplay_tab := Canonical_Lbl_Tab.update (l, Lazy.value result) (!preplay_tab)
- fun get_preplay_time l =
- (case get_preplay_result l of
- Preplay_Success preplay_time => preplay_time
- | Preplay_Failure => some_preplay_time)
-
- fun set_preplay_time l = set_preplay_result l o Preplay_Success
-
val result_of_step =
try (label_of_step #> the #> get_preplay_result)
#> the_default (Preplay_Success zero_preplay_time)
@@ -271,8 +257,6 @@
in
{get_preplay_result = get_preplay_result,
set_preplay_result = set_preplay_result,
- get_preplay_time = get_preplay_time,
- set_preplay_time = set_preplay_time,
preplay_quietly = preplay_quietly,
overall_preplay_stats = overall_preplay_stats}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Thu Dec 19 18:07:21 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Thu Dec 19 18:22:31 2013 +0100
@@ -29,13 +29,13 @@
fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout
- ({preplay_quietly, get_preplay_time, set_preplay_time, ...} : preplay_interface)
+ ({preplay_quietly, get_preplay_result, set_preplay_result, ...} : preplay_interface)
(step as Prove (_, _, l, _, _, _)) =
let
val timeout =
- (case get_preplay_time l of
- (true, _) => preplay_timeout
- | (false, t) => Time.+ (t, slack))
+ (case get_preplay_result l of
+ Preplay_Success (false, t) => Time.+ (t, slack)
+ | _ => preplay_timeout)
fun try_variant variant =
(case preplay_quietly timeout variant of
@@ -43,7 +43,7 @@
| time as (false, _) => SOME (variant, time))
in
(case Par_List.get_some try_variant (variants_of_step step) of
- SOME (step, time) => (set_preplay_time l time; step)
+ SOME (step, time) => (set_preplay_result l (Preplay_Success time); step)
| NONE => step)
end