--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 13 13:18:14 2014 +0100
@@ -369,9 +369,8 @@
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
(case play of
Played _ => meth = SMT2_Method andalso smt_proofs <> SOME true
- | Play_Timed_Out _ => true
- | Play_Failed => true
- | Not_Played => false)
+ | Play_Timed_Out time => Time.> (time, Time.zeroTime)
+ | Play_Failed => true)
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
(one_line_params as (preplay, _, _, _, _, _)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Mar 13 13:18:14 2014 +0100
@@ -178,7 +178,8 @@
end
| set_preplay_outcomes_of_isar_step _ _ _ _ _ _ = ()
-fun peek_at_outcome outcome = if Lazy.is_finished outcome then Lazy.force outcome else Not_Played
+fun peek_at_outcome outcome =
+ if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime
fun get_best_method_outcome force =
tap (List.app (K () o Lazy.future Future.default_params o snd)) (* optional parallelism *)
@@ -195,14 +196,17 @@
outcome as Played _ => outcome
| _ => snd (get_best_method_outcome Lazy.force meths_outcomes))
else
- (case get_best_method_outcome peek_at_outcome meths_outcomes of
- (_, Not_Played) => snd (get_best_method_outcome Lazy.force meths_outcomes)
- | (_, outcome) => outcome)
+ let val outcome = snd (get_best_method_outcome peek_at_outcome meths_outcomes) in
+ if outcome = Play_Timed_Out Time.zeroTime then
+ snd (get_best_method_outcome Lazy.force meths_outcomes)
+ else
+ outcome
+ end
end
fun preplay_outcome_of_isar_step_for_method preplay_data l =
AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
- #> the_default (Lazy.value Not_Played)
+ #> the_default (Lazy.value (Play_Timed_Out Time.zeroTime))
fun fastest_method_of_isar_step preplay_data =
the o Canonical_Label_Tab.lookup preplay_data
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Mar 13 13:18:14 2014 +0100
@@ -26,8 +26,7 @@
datatype play_outcome =
Played of Time.time |
Play_Timed_Out of Time.time |
- Play_Failed |
- Not_Played
+ Play_Failed
type minimize_command = string list -> string
type one_line_params =
@@ -65,8 +64,7 @@
datatype play_outcome =
Played of Time.time |
Play_Timed_Out of Time.time |
- Play_Failed |
- Not_Played
+ Play_Failed
type minimize_command = string list -> string
type one_line_params =
@@ -120,17 +118,14 @@
end
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
- | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
+ | string_of_play_outcome (Play_Timed_Out time) =
+ if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out"
| string_of_play_outcome Play_Failed = "failed"
- | string_of_play_outcome _ = "unknown"
fun play_outcome_ord (Played time1, Played time2) =
int_ord (pairself Time.toMilliseconds (time1, time2))
| play_outcome_ord (Played _, _) = LESS
| play_outcome_ord (_, Played _) = GREATER
- | play_outcome_ord (Not_Played, Not_Played) = EQUAL
- | play_outcome_ord (Not_Played, _) = LESS
- | play_outcome_ord (_, Not_Played) = GREATER
| play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
int_ord (pairself Time.toMilliseconds (time1, time2))
| play_outcome_ord (Play_Timed_Out _, _) = LESS
@@ -159,11 +154,11 @@
(* unusing_chained_facts used_chaineds num_chained ^ *)
apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss
-fun show_time NONE = ""
- | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
-
-fun try_command_line banner time command =
- banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^ show_time time ^ "."
+fun try_command_line banner play command =
+ let val s = string_of_play_outcome play in
+ banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^
+ (s |> s <> "" ? enclose " (" ")") ^ "."
+ end
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
@@ -181,18 +176,11 @@
let
val (chained, extra) = split_used_facts used_facts
- val (failed, ext_time) =
- (case play of
- Played time => (false, (SOME (false, time)))
- | Play_Timed_Out time => (false, SOME (true, time))
- | Play_Failed => (true, NONE)
- | Not_Played => (false, NONE))
-
val try_line =
map fst extra
|> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
- |> (if failed then enclose "One-line proof reconstruction failed: " "."
- else try_command_line banner ext_time)
+ |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "."
+ else try_command_line banner play)
in
try_line ^ minimize_line minimize_command (map fst (extra @ chained))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Mar 13 13:18:14 2014 +0100
@@ -219,7 +219,7 @@
fun get_preferred meths = if member (op =) meths preferred then preferred else meth
in
if timeout = Time.zeroTime then
- (get_preferred meths, Not_Played)
+ (get_preferred meths, Play_Timed_Out Time.zeroTime)
else
let
val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()