--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Dec 19 18:22:31 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Dec 19 18:39:54 2013 +0100
@@ -158,7 +158,7 @@
(* check if the modified step can be preplayed fast enough *)
val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
- val (false, time'') = preplay_quietly timeout step''
+ val Preplay_Success (false, time'') = preplay_quietly timeout step''
in
decrement_step_count (); (* l' successfully eliminated! *)
@@ -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_times = map2 preplay_quietly timeouts succs'
+ val preplay_results = map2 preplay_quietly timeouts succs'
(* ensure none of the modified successors timed out *)
- val false = List.exists fst preplay_times
+ val true = List.all (fn Preplay_Success _ => true) preplay_results
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 (fn l => set_preplay_result l o Preplay_Success) succ_lbls preplay_times;
+ map2 set_preplay_result succ_lbls preplay_results;
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:22:31 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Thu Dec 19 18:39:54 2013 +0100
@@ -36,8 +36,8 @@
fun minimize_facts _ time min_facts [] = (time, min_facts)
| minimize_facts mk_step time min_facts (f :: facts) =
(case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of
- (true, _) => minimize_facts mk_step time (f :: min_facts) facts
- | (false, time) => minimize_facts mk_step time min_facts facts)
+ Preplay_Success (false, time) => minimize_facts mk_step time min_facts facts
+ | _ => minimize_facts mk_step time (f :: min_facts) facts)
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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Dec 19 18:22:31 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Dec 19 18:39:54 2013 +0100
@@ -16,14 +16,12 @@
Preplay_Failure
val trace: bool Config.T
- 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,
- 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}
+ preplay_quietly: Time.time -> isar_step -> preplay_result,
+ overall_preplay_stats: isar_proof -> preplay_result}
val proof_preplay_interface: bool -> Proof.context -> string -> string -> bool -> Time.time ->
isar_proof -> preplay_interface
@@ -44,8 +42,6 @@
val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
-fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+ (t1, t2))
-
fun preplay_trace ctxt assms concl time =
let
val ctxt = ctxt |> Config.put show_markup true
@@ -163,9 +159,8 @@
type preplay_interface =
{get_preplay_result: label -> preplay_result,
set_preplay_result: label -> preplay_result -> 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}
+ preplay_quietly: Time.time -> isar_step -> preplay_result,
+ overall_preplay_stats: isar_proof -> preplay_result}
fun enrich_context_with_local_facts proof ctxt =
let
@@ -185,6 +180,10 @@
enrich_with_proof proof ctxt
end
+fun merge_preplay_results (Preplay_Success (b1, t1)) (Preplay_Success (b2, t2)) =
+ Preplay_Success (b1 orelse b2, Time.+ (t1, t2))
+ | merge_preplay_results _ _ = Preplay_Failure
+
(* Given a proof, produces an imperative preplay interface with a shared table mapping from labels
to preplay results. The preplay results are caluclated lazyly and cached to avoid repeated
calculation.
@@ -196,8 +195,8 @@
(* the dont_preplay option pretends that everything works just fine *)
{get_preplay_result = K (Preplay_Success zero_preplay_time),
set_preplay_result = K (K ()),
- preplay_quietly = K (K zero_preplay_time),
- overall_preplay_stats = K (zero_preplay_time, false)} : preplay_interface
+ preplay_quietly = K (K (Preplay_Success zero_preplay_time)),
+ overall_preplay_stats = K (Preplay_Success zero_preplay_time)} : preplay_interface
else
let
val ctxt = enrich_context_with_local_facts proof ctxt
@@ -216,10 +215,7 @@
Preplay_Failure)
(* preplay steps treating exceptions like timeouts *)
- fun preplay_quietly timeout step =
- (case preplay true timeout step of
- Preplay_Success preplay_time => preplay_time
- | Preplay_Failure => (true, timeout))
+ fun preplay_quietly timeout = preplay true timeout
val preplay_tab =
let
@@ -247,13 +243,9 @@
try (label_of_step #> the #> get_preplay_result)
#> the_default (Preplay_Success zero_preplay_time)
- fun do_step step =
- (case result_of_step step of
- Preplay_Success preplay_time => apfst (add_preplay_time preplay_time)
- | Preplay_Failure => apsnd (K true))
-
fun overall_preplay_stats (Proof (_, _, steps)) =
- fold_isar_steps do_step steps (zero_preplay_time, false)
+ Preplay_Success (false, Time.zeroTime)
+ |> fold_isar_steps (merge_preplay_results o result_of_step) steps
in
{get_preplay_result = get_preplay_result,
set_preplay_result = set_preplay_result,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 18:22:31 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 18:39:54 2013 +0100
@@ -355,7 +355,7 @@
|> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay
preplay_timeout)
- val ((preplay_time, preplay_fail), isar_proof) =
+ val (preplay_result, isar_proof) =
isar_proof
|> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0)
preplay_interface
@@ -383,7 +383,9 @@
else
[]) @
(if do_preplay then
- [(if preplay_fail then "may fail, " else "") ^ string_of_ext_time preplay_time]
+ [(case preplay_result of
+ Preplay_Success ext_time => string_of_ext_time ext_time
+ | Preplay_Failure => "may fail")]
else
[])
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Thu Dec 19 18:22:31 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Thu Dec 19 18:39:54 2013 +0100
@@ -29,7 +29,7 @@
fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout
- ({preplay_quietly, get_preplay_result, set_preplay_result, ...} : preplay_interface)
+ ({get_preplay_result, set_preplay_result, preplay_quietly, ...} : preplay_interface)
(step as Prove (_, _, l, _, _, _)) =
let
val timeout =
@@ -39,11 +39,11 @@
fun try_variant variant =
(case preplay_quietly timeout variant of
- (true, _) => NONE
- | time as (false, _) => SOME (variant, time))
+ result as Preplay_Success _ => SOME (variant, result)
+ | _ => NONE)
in
(case Par_List.get_some try_variant (variants_of_step step) of
- SOME (step, time) => (set_preplay_result l (Preplay_Success time); step)
+ SOME (step', result) => (set_preplay_result l result; step')
| NONE => step)
end