--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Jan 31 18:43:16 2014 +0100
@@ -96,7 +96,7 @@
(* Precondition: The proof must be labeled canonically
(cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
fun compress_isar_proof compress_isar
- ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
+ ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
if compress_isar <= 1.0 then
proof
else
@@ -148,7 +148,7 @@
val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
(* only touch proofs that can be preplayed sucessfully *)
- val Played time' = get_preplay_outcome l'
+ val Played time' = preplay_outcome l'
(* merge steps *)
val subs'' = subs @ nontriv_subs
@@ -177,7 +177,7 @@
if subproofs = [] then
step
else
- (case get_preplay_outcome l of
+ (case preplay_outcome l of
Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
| _ => step)
@@ -214,10 +214,9 @@
fun try_eliminate (i, l, _) succ_lbls steps =
let
(* only touch steps that can be preplayed successfully *)
- val Played time = get_preplay_outcome l
+ val Played time = preplay_outcome l
- val succ_times =
- map (get_preplay_outcome #> (fn Played t => t)) succ_lbls
+ val succ_times = map (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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Jan 31 18:43:16 2014 +0100
@@ -26,9 +26,9 @@
val slack = seconds 0.1
fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
- | minimize_isar_step_dependencies {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
+ | minimize_isar_step_dependencies {preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
(step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
- (case get_preplay_outcome l of
+ (case preplay_outcome l of
Played time =>
let
fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 18:43:16 2014 +0100
@@ -15,8 +15,9 @@
val trace : bool Config.T
type isar_preplay_data =
- {get_preplay_outcome: label -> play_outcome,
+ {preplay_outcome: label -> play_outcome,
set_preplay_outcome: label -> play_outcome -> unit,
+ string_of_preplay_outcome: label -> string,
preplay_quietly: Time.time -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
@@ -145,12 +146,10 @@
play_outcome)
end
-
-(*** proof preplay interface ***)
-
type isar_preplay_data =
- {get_preplay_outcome: label -> play_outcome,
+ {preplay_outcome: label -> play_outcome,
set_preplay_outcome: label -> play_outcome -> unit,
+ string_of_preplay_outcome: label -> string,
preplay_quietly: Time.time -> isar_step -> play_outcome,
overall_preplay_outcome: isar_proof -> play_outcome}
@@ -189,8 +188,9 @@
fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
if not do_preplay then
(* the "dont_preplay" option pretends that everything works just fine *)
- {get_preplay_outcome = K (Played Time.zeroTime),
+ {preplay_outcome = K (Played Time.zeroTime),
set_preplay_outcome = K (K ()),
+ string_of_preplay_outcome = K "",
preplay_quietly = K (K (Played Time.zeroTime)),
overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
else
@@ -228,22 +228,25 @@
|> Unsynchronized.ref
end
- fun get_preplay_outcome l =
+ fun preplay_outcome l =
Canonical_Label_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
handle Option.Option => raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
fun set_preplay_outcome l result =
preplay_tab := Canonical_Label_Tab.update (l, Lazy.value result) (!preplay_tab)
+ fun string_of_preplay_outcome l = @{make_string} (preplay_outcome l)
+
val result_of_step =
- try (label_of_step #> the #> get_preplay_outcome)
+ try (label_of_step #> the #> preplay_outcome)
#> the_default (Played Time.zeroTime)
fun overall_preplay_outcome (Proof (_, _, steps)) =
fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
in
- {get_preplay_outcome = get_preplay_outcome,
+ {preplay_outcome = preplay_outcome,
set_preplay_outcome = set_preplay_outcome,
+ string_of_preplay_outcome = string_of_preplay_outcome,
preplay_quietly = preplay_quietly,
overall_preplay_outcome = overall_preplay_outcome}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 18:43:16 2014 +0100
@@ -30,11 +30,11 @@
fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout
- ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
+ ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
(step as Prove (_, _, l, _, _, _)) =
let
val timeout =
- (case get_preplay_outcome l of
+ (case preplay_outcome l of
Played time => Time.+ (time, slack)
| _ => preplay_timeout)