# HG changeset patch # User blanchet # Date 1394713094 -3600 # Node ID 4eeb73a1feec3f70d3b7e27de033314e9f5d61ce # Parent 1ba075db8fe477975a96df3d1661ca2caa3792c5 simplified preplaying information diff -r 1ba075db8fe4 -r 4eeb73a1feec src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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, _, _, _, _, _)) = diff -r 1ba075db8fe4 -r 4eeb73a1feec src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- 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 diff -r 1ba075db8fe4 -r 4eeb73a1feec src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- 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 diff -r 1ba075db8fe4 -r 4eeb73a1feec src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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 ()