use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jan 02 10:41:53 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jan 02 10:54:36 2013 +0100
@@ -457,8 +457,8 @@
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
fun failed failure =
({outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
- preplay =
- K (Sledgehammer_Reconstruct.Failed_to_Play Sledgehammer_Provers.plain_metis),
+ preplay = Lazy.value (Sledgehammer_Reconstruct.Failed_to_Play
+ Sledgehammer_Provers.plain_metis),
message = K "", message_tail = ""}, ~1)
val ({outcome, used_facts, run_time, preplay, message, message_tail}
: Sledgehammer_Provers.prover_result,
@@ -487,7 +487,7 @@
handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
val time_prover = run_time |> Time.toMilliseconds
- val msg = message (preplay ()) ^ message_tail
+ val msg = message (Lazy.force preplay) ^ message_tail
in
case outcome of
NONE => (msg, SH_OK (time_isa, time_prover, used_facts))
@@ -601,7 +601,7 @@
val _ = log separator
val (used_facts, (preplay, message, message_tail)) =
minimize st (these (!named_thms))
- val msg = message (preplay ()) ^ message_tail
+ val msg = message (Lazy.force preplay) ^ message_tail
in
case used_facts of
SOME named_thms' =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jan 02 10:41:53 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jan 02 10:54:36 2013 +0100
@@ -20,7 +20,7 @@
(string -> thm list -> unit) -> string -> params -> bool -> int -> int
-> Proof.state -> ((string * stature) * thm list) list
-> ((string * stature) * thm list) list option
- * ((unit -> play) * (play -> string) * string)
+ * (play Lazy.lazy * (play -> string) * string)
val get_minimizing_isar_prover :
Proof.context -> mode -> (string -> thm list -> unit) -> string -> prover
val run_minimize :
@@ -236,7 +236,8 @@
| {preplay, message, ...} =>
(NONE, (preplay, prefix "Prover error: " o message, "")))
handle ERROR msg =>
- (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, ""))
+ (NONE, (Lazy.value (Failed_to_Play plain_metis),
+ fn _ => "Error: " ^ msg, ""))
end
fun adjust_reconstructor_params override_params
@@ -290,19 +291,17 @@
if isar_proofs then
((prover_fast_enough (), (name, params)), preplay)
else
- let val preplay = preplay () in
- (case preplay of
- Played (reconstr, timeout) =>
- if can_min_fast_enough timeout then
- (true, extract_reconstructor params reconstr
- ||> (fn override_params =>
- adjust_reconstructor_params
- override_params params))
- else
- (prover_fast_enough (), (name, params))
- | _ => (prover_fast_enough (), (name, params)),
- K preplay)
- end
+ (case Lazy.force preplay of
+ Played (reconstr, timeout) =>
+ if can_min_fast_enough timeout then
+ (true, extract_reconstructor params reconstr
+ ||> (fn override_params =>
+ adjust_reconstructor_params
+ override_params params))
+ else
+ (prover_fast_enough (), (name, params))
+ | _ => (prover_fast_enough (), (name, params)),
+ preplay)
end
else
((false, (name, params)), preplay)
@@ -352,7 +351,7 @@
(kill_provers ();
minimize_facts do_learn prover params false i n state facts
|> (fn (_, (preplay, message, message_tail)) =>
- message (preplay ()) ^ message_tail
+ message (Lazy.force preplay) ^ message_tail
|> Output.urgent_message))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jan 02 10:41:53 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jan 02 10:54:36 2013 +0100
@@ -77,7 +77,7 @@
{outcome : failure option,
used_facts : (string * stature) list,
run_time : Time.time,
- preplay : unit -> play,
+ preplay : play Lazy.lazy,
message : play -> string,
message_tail : string}
@@ -370,7 +370,7 @@
{outcome : failure option,
used_facts : (string * stature) list,
run_time : Time.time,
- preplay : unit -> play,
+ preplay : play Lazy.lazy,
message : play -> string,
message_tail : string}
@@ -884,15 +884,15 @@
else metis_default_lam_trans))
in
(used_facts,
- fn () =>
- let
- val used_pairs =
- facts |> map untranslated_fact
- |> filter_used_facts false used_facts
- in
- play_one_line_proof mode debug verbose preplay_timeout
- used_pairs state subgoal (hd reconstrs) reconstrs
- end,
+ Lazy.lazy (fn () =>
+ let
+ val used_pairs =
+ facts |> map untranslated_fact
+ |> filter_used_facts false used_facts
+ in
+ play_one_line_proof mode debug verbose preplay_timeout
+ used_pairs state subgoal (hd reconstrs) reconstrs
+ end),
fn preplay =>
let
val _ =
@@ -923,7 +923,7 @@
""))
end
| SOME failure =>
- ([], K (Failed_to_Play plain_metis),
+ ([], Lazy.value (Failed_to_Play plain_metis),
fn _ => string_for_failure failure, "")
in
{outcome = outcome, used_facts = used_facts, run_time = run_time,
@@ -1086,13 +1086,11 @@
val (preplay, message, message_tail) =
case outcome of
NONE =>
- (fn () =>
- play_one_line_proof mode debug verbose preplay_timeout used_pairs
- state subgoal SMT
- (bunch_of_reconstructors false
- (fn desperate =>
- if desperate then liftingN
- else metis_default_lam_trans)),
+ (Lazy.lazy (fn () =>
+ play_one_line_proof mode debug verbose preplay_timeout used_pairs
+ state subgoal SMT
+ (bunch_of_reconstructors false (fn desperate =>
+ if desperate then liftingN else metis_default_lam_trans))),
fn preplay =>
let
val one_line_params =
@@ -1106,7 +1104,8 @@
else
"")
| SOME failure =>
- (K (Failed_to_Play plain_metis), fn _ => string_for_failure failure, "")
+ (Lazy.value (Failed_to_Play plain_metis),
+ fn _ => string_for_failure failure, "")
in
{outcome = outcome, used_facts = used_facts, run_time = run_time,
preplay = preplay, message = message, message_tail = message_tail}
@@ -1133,7 +1132,7 @@
[reconstr] of
play as Played (_, time) =>
{outcome = NONE, used_facts = used_facts, run_time = time,
- preplay = K play,
+ preplay = Lazy.value play,
message =
fn play =>
let
@@ -1150,8 +1149,8 @@
val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut
in
{outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
- preplay = K play, message = fn _ => string_for_failure failure,
- message_tail = ""}
+ preplay = Lazy.value play,
+ message = fn _ => string_for_failure failure, message_tail = ""}
end
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jan 02 10:41:53 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jan 02 10:54:36 2013 +0100
@@ -102,7 +102,7 @@
|> (fn {outcome, preplay, message, message_tail, ...} =>
(if outcome = SOME ATP_Proof.TimedOut then timeoutN
else if is_some outcome then noneN
- else someN, fn () => message (preplay ()) ^ message_tail))
+ else someN, fn () => message (Lazy.force preplay) ^ message_tail))
fun go () =
let
val (outcome_code, message) =