# HG changeset patch # User blanchet # Date 1406897037 -7200 # Node ID 25d1495e6641bff0459b154b09d617965e1ac4bf # Parent 72d4c00064afbf505a323f836aa2ef6518e65ea3 eliminated needlessly complex message tail diff -r 72d4c00064af -r 25d1495e6641 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 01 14:43:57 2014 +0200 @@ -157,13 +157,13 @@ print_used_facts used_facts used_from | _ => ()) |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) - |> (fn {outcome, used_facts, used_from, preferred_methss, message, message_tail, ...} => + |> (fn {outcome, used_facts, used_from, preferred_methss, message, ...} => (if outcome = SOME ATP_Proof.TimedOut then timeoutN else if is_some outcome then noneN else someN, fn () => message (play_one_line_proof mode preplay_timeout (filter_used_facts false used_facts used_from) state subgoal - preferred_methss) ^ message_tail)) + preferred_methss))) fun go () = let diff -r 72d4c00064af -r 25d1495e6641 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Aug 01 14:43:57 2014 +0200 @@ -58,8 +58,7 @@ used_from : fact list, preferred_methss : proof_method * proof_method list list, run_time : Time.time, - message : proof_method * play_outcome -> string, - message_tail : string} + message : proof_method * play_outcome -> string} type prover = params -> prover_problem -> prover_result @@ -150,8 +149,7 @@ used_from : fact list, preferred_methss : proof_method * proof_method list list, run_time : Time.time, - message : proof_method * play_outcome -> string, - message_tail : string} + message : proof_method * play_outcome -> string} type prover = params -> prover_problem -> prover_result diff -r 72d4c00064af -r 25d1495e6641 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Aug 01 14:43:57 2014 +0200 @@ -127,8 +127,7 @@ the only ATP that does not honor its time limit. *) val atp_timeout_slack = seconds 1.0 -(* Important messages are important but not so important that users want to see - them each time. *) +(* Important messages are important but not so important that users want to see them each time. *) val atp_important_message_keep_quotient = 25 fun run_atp mode name @@ -354,7 +353,7 @@ else "" - val (used_facts, preferred_methss, message, message_tail) = + val (used_facts, preferred_methss, message) = (case outcome of NONE => let @@ -390,20 +389,19 @@ (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in - proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params - end, - (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^ - (if important_message <> "" then - "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message - else - "")) + proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained + one_line_params ^ + (if important_message <> "" then + "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message + else + "") + end) end | SOME failure => - ([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure, "")) + ([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) in {outcome = outcome, used_facts = used_facts, used_from = used_from, - preferred_methss = preferred_methss, run_time = run_time, message = message, - message_tail = message_tail} + preferred_methss = preferred_methss, run_time = run_time, message = message} end end; diff -r 72d4c00064af -r 25d1495e6641 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Aug 01 14:43:57 2014 +0200 @@ -22,12 +22,8 @@ val binary_min_facts : int Config.T val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state -> thm -> ((string * stature) * thm list) list -> - ((string * stature) * thm list) list option - * (((proof_method * play_outcome) -> string) * string) + ((string * stature) * thm list) list option * ((proof_method * play_outcome) -> string) val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover - - val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list -> - Proof.state -> unit end; structure Sledgehammer_Prover_Minimize : SLEDGEHAMMER_PROVER_MINIMIZE = @@ -209,8 +205,7 @@ val min = if length facts >= Config.get ctxt binary_min_facts then binary_minimize else linear_minimize - val (min_facts, {message, message_tail, ...}) = - min test (new_timeout timeout run_time) result facts + val (min_facts, {message, ...}) = min test (new_timeout timeout run_time) result facts in print silent (fn () => cat_lines ["Minimized to " ^ n_facts (map fst min_facts)] ^ @@ -218,38 +213,37 @@ 0 => "" | n => "\n(including " ^ string_of_int n ^ " chained)") ^ "."); (if learn then do_learn (maps snd min_facts) else ()); - (SOME min_facts, (message, message_tail)) + (SOME min_facts, message) end | {outcome = SOME TimedOut, ...} => - (NONE, (fn _ => + (NONE, fn _ => "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \ - \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", "")) - | {message, ...} => (NONE, (prefix "Prover error: " o message, "")))) - handle ERROR msg => (NONE, (fn _ => "Error: " ^ msg, "")) + \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").") + | {message, ...} => (NONE, (prefix "Prover error: " o message)))) + handle ERROR msg => (NONE, fn _ => "Error: " ^ msg) end fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...}) ({state, goal, subgoal, subgoal_count, ...} : prover_problem) - (result as {outcome, used_facts, used_from, preferred_methss, run_time, message, message_tail} + (result as {outcome, used_facts, used_from, preferred_methss, run_time, message} : prover_result) = if is_some outcome orelse null used_facts then result else let - val (used_facts, (message, _)) = + val (used_facts, message) = if minimize then minimize_facts do_learn name params (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state goal (filter_used_facts true used_facts (map (apsnd single) used_from)) |>> Option.map (map fst) else - (SOME used_facts, (message, "")) + (SOME used_facts, message) in (case used_facts of SOME used_facts => {outcome = NONE, used_facts = used_facts, used_from = used_from, - preferred_methss = preferred_methss, run_time = run_time, message = message, - message_tail = message_tail} + preferred_methss = preferred_methss, run_time = run_time, message = message} | NONE => result) end @@ -257,25 +251,4 @@ get_prover ctxt mode name params problem |> maybe_minimize mode do_learn name params problem -fun run_minimize (params as {provers, ...}) do_learn i refs state = - let - val ctxt = Proof.context_of state - val {goal, facts = chained_ths, ...} = Proof.goal state - val reserved = reserved_isar_keyword_table () - val css = clasimpset_rule_table_of ctxt - val facts = refs |> maps (map (apsnd single) o fact_of_ref ctxt reserved chained_ths css) - in - (case subgoal_count state of - 0 => Output.urgent_message "No subgoal!" - | n => - (case provers of - [] => error "No prover is set." - | prover :: _ => - (kill_provers (); - minimize_facts do_learn prover params false i n state goal facts - |> (fn (_, (message, message_tail)) => - Output.urgent_message (message (Metis_Method (NONE, NONE), - Play_Timed_Out Time.zeroTime) ^ message_tail))))) - end - end; diff -r 72d4c00064af -r 25d1495e6641 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Aug 01 14:43:57 2014 +0200 @@ -192,7 +192,7 @@ val used_facts = map fst used_named_facts val outcome = Option.map failure_of_smt2_failure outcome - val (preferred_methss, message, message_tail) = + val (preferred_methss, message) = (case outcome of NONE => let @@ -212,15 +212,14 @@ (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in - proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params - end, - if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "") + proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained + one_line_params + end) end - | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure, "")) + | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) in {outcome = outcome, used_facts = used_facts, used_from = used_from, - preferred_methss = preferred_methss, run_time = run_time, message = message, - message_tail = message_tail} + preferred_methss = preferred_methss, run_time = run_time, message = message} end end;