--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Dec 19 18:39:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Dec 19 19:16:44 2013 +0100
@@ -18,6 +18,7 @@
struct
open Sledgehammer_Util
+open Sledgehammer_Reconstructor
open Sledgehammer_Proof
open Sledgehammer_Preplay
@@ -93,7 +94,7 @@
(* Precondition: The proof must be labeled canonically
(cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
fun compress_proof isar_compress
- ({get_preplay_result, set_preplay_result, preplay_quietly, ...} : preplay_interface) proof =
+ ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface) proof =
if isar_compress <= 1.0 then
proof
else
@@ -135,7 +136,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_result l (Preplay_Success (false, time));
+ (set_preplay_outcome l (Played time);
Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
else
(case subs of
@@ -145,7 +146,7 @@
val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
(* only touch proofs that can be preplayed sucessfully *)
- val Preplay_Success (false, time') = get_preplay_result l'
+ val Played time' = get_preplay_outcome l'
(* merge steps *)
val subs'' = subs @ nontriv_subs
@@ -158,7 +159,7 @@
(* check if the modified step can be preplayed fast enough *)
val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
- val Preplay_Success (false, time'') = preplay_quietly timeout step''
+ val Played time'' = preplay_quietly timeout step''
in
decrement_step_count (); (* l' successfully eliminated! *)
@@ -174,9 +175,8 @@
if subproofs = [] then
step
else
- (case get_preplay_result l of
- Preplay_Success (false, time) =>
- elim_subproofs' time qs fix l t lfs gfs meth subproofs []
+ (case get_preplay_outcome l of
+ Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
| _ => step)
(** top_level compression: eliminate steps by merging them into their
@@ -211,10 +211,10 @@
fun try_eliminate (i, l, _) succ_lbls steps =
let
(* only touch steps that can be preplayed successfully *)
- val Preplay_Success (false, time) = get_preplay_result l
+ val Played time = get_preplay_outcome l
val succ_times =
- map (get_preplay_result #> (fn Preplay_Success (false, t) => t)) succ_lbls
+ map (get_preplay_outcome #> (fn Played 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
@@ -232,17 +232,17 @@
val succs' = map (try_merge cand #> the) succs
(* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
- val preplay_results = map2 preplay_quietly timeouts succs'
+ val play_outcomes = map2 preplay_quietly timeouts succs'
(* ensure none of the modified successors timed out *)
- val true = List.all (fn Preplay_Success _ => true) preplay_results
+ val true = List.all (fn Played _ => true) play_outcomes
val (steps1, _ :: steps2) = chop i steps
(* replace successors with their modified versions *)
val steps2 = update_steps steps2 succs'
in
decrement_step_count (); (* candidate successfully eliminated *)
- map2 set_preplay_result succ_lbls preplay_results;
+ map2 set_preplay_outcome succ_lbls play_outcomes;
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