# HG changeset patch # User blanchet # Date 1307385394 -7200 # Node ID 68e3cd19fee849d99bd719a2eabb18ba9cea1b0c # Parent 8cf188ff76a3bbc090c1eaa97a67702b2cf0dc03 show what failed to play diff -r 8cf188ff76a3 -r 68e3cd19fee8 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 06 20:36:34 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 06 20:36:34 2011 +0200 @@ -398,7 +398,7 @@ | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) fun failed failure = ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE, - preplay = K ATP_Reconstruct.Failed_to_Play, + preplay = K (ATP_Reconstruct.Failed_to_Play ATP_Reconstruct.Metis), message = K ""}, ~1) val ({outcome, used_facts, run_time_in_msecs, preplay, message} : Sledgehammer_Provers.prover_result, diff -r 8cf188ff76a3 -r 68e3cd19fee8 src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:34 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:34 2011 +0200 @@ -22,7 +22,7 @@ datatype play = Played of reconstructor * Time.time | Trust_Playable of reconstructor * Time.time option| - Failed_to_Play + Failed_to_Play of reconstructor type minimize_command = string list -> string type one_line_params = @@ -73,7 +73,7 @@ datatype play = Played of reconstructor * Time.time | Trust_Playable of reconstructor * Time.time option | - Failed_to_Play + Failed_to_Play of reconstructor type minimize_command = string list -> string type one_line_params = @@ -294,23 +294,22 @@ subgoal, subgoal_count) = let val (chained, extra) = split_used_facts used_facts - val (reconstructor, ext_time) = + val (failed, reconstructor, ext_time) = case preplay of Played (reconstructor, time) => - (SOME reconstructor, (SOME (false, time))) + (false, reconstructor, (SOME (false, time))) | Trust_Playable (reconstructor, time) => - (SOME reconstructor, + (false, reconstructor, case time of NONE => NONE | SOME time => if time = Time.zeroTime then NONE else SOME (true, time)) - | Failed_to_Play => (NONE, NONE) + | Failed_to_Play reconstructor => (true, reconstructor, NONE) val try_line = - case reconstructor of - SOME r => ([], map fst extra) - |> reconstructor_command r subgoal subgoal_count - |> try_command_line banner ext_time - | NONE => "One-line proof reconstruction failed." + ([], map fst extra) + |> reconstructor_command reconstructor subgoal subgoal_count + |> (if failed then enclose "One-line proof reconstruction failed: " "." + else try_command_line banner ext_time) in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end (** Hard-core proof reconstruction: structured Isar proofs **) @@ -1103,7 +1102,7 @@ fun proof_text ctxt isar_proof isar_params (one_line_params as (preplay, _, _, _, _, _)) = - (if isar_proof orelse preplay = Failed_to_Play then + (if case preplay of Failed_to_Play _ => true | _ => isar_proof then isar_proof_text ctxt isar_proof isar_params else one_line_proof_text) one_line_params diff -r 8cf188ff76a3 -r 68e3cd19fee8 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Jun 06 20:36:34 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Jun 06 20:36:34 2011 +0200 @@ -185,7 +185,8 @@ string_of_int (10 + msecs div 1000) ^ "\").")) | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message))) - handle ERROR msg => (NONE, (K Failed_to_Play, fn _ => "Error: " ^ msg)) + handle ERROR msg => + (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg)) end fun run_minimize (params as {provers, ...}) i refs state = diff -r 8cf188ff76a3 -r 68e3cd19fee8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:36:34 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:36:34 2011 +0200 @@ -429,7 +429,7 @@ fun play_one_line_proof debug timeout ths state i reconstructors = let - fun play [] [] = Failed_to_Play + fun play [] [] = Failed_to_Play (hd reconstructors) | play (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout) | play timed_out (reconstructor :: reconstructors) = let val timer = Timer.startRealTimer () in @@ -815,7 +815,7 @@ end) end | SOME failure => - ([], K Failed_to_Play, fn _ => string_for_failure failure) + ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure) in {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs, preplay = preplay, message = message} @@ -1000,7 +1000,8 @@ else "") end) - | SOME failure => (K Failed_to_Play, fn _ => string_for_failure failure) + | SOME failure => + (K (Failed_to_Play Metis), fn _ => string_for_failure failure) in {outcome = outcome, used_facts = used_facts, run_time_in_msecs = run_time_in_msecs, preplay = preplay, @@ -1029,7 +1030,9 @@ minimize_command name, subgoal, subgoal_count) in one_line_proof_text one_line_params end} | play => - let val failure = if play = Failed_to_Play then GaveUp else TimedOut in + let + val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut + in {outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE, preplay = K play, message = fn _ => string_for_failure failure} end