# HG changeset patch # User blanchet # Date 1357120476 -3600 # Node ID 84c7cf36b2e07799b0e820bc15e5bd6e5f6ef20f # Parent e25275f7d15e3e0e04dd70c2fb473a01ea4faa88 use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most) diff -r e25275f7d15e -r 84c7cf36b2e0 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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' => diff -r e25275f7d15e -r 84c7cf36b2e0 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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 diff -r e25275f7d15e -r 84c7cf36b2e0 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 diff -r e25275f7d15e -r 84c7cf36b2e0 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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) =