# HG changeset patch # User boehmes # Date 1251575826 -7200 # Node ID 8f0dc876fb1b76aed35ea7acc01a4d7f2d6cab25 # Parent 6b93b73a712b1c8dd5ab77586306cf9355b85c8b propagate theorem names, in addition to generated return message diff -r 6b93b73a712b -r 8f0dc876fb1b src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Aug 28 19:57:12 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Sat Aug 29 21:57:06 2009 +0200 @@ -24,7 +24,7 @@ type prover = int -> (thm * (string * int)) list option -> (thm * (string * int)) list option -> string -> int -> Proof.context * (thm list * thm) -> - bool * string * string * string vector * (thm * (string * int)) list + bool * (string * string list) * string * string vector * (thm * (string * int)) list val add_prover: string -> prover -> theory -> theory val print_provers: theory -> unit val get_prover: string -> theory -> prover option @@ -305,7 +305,7 @@ type prover = int -> (thm * (string * int)) list option -> (thm * (string * int)) list option -> string -> int -> Proof.context * (thm list * thm) -> - bool * string * string * string vector * (thm * (string * int)) list + bool * (string * string list) * string * string vector * (thm * (string * int)) list fun err_dup_prover name = error ("Duplicate prover: " ^ quote name); @@ -345,7 +345,7 @@ let val _ = register birthtime deadtime (Thread.self (), desc) val result = - let val (success, message, _, _, _) = + let val (success, (message, _), _, _, _) = prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state) in (success, message) end handle ResHolClause.TOO_TRIVIAL diff -r 6b93b73a712b -r 8f0dc876fb1b src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Aug 28 19:57:12 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Sat Aug 29 21:57:06 2009 +0200 @@ -89,10 +89,10 @@ val failure = find_failure proof val success = rc = 0 andalso is_none failure val message = - if is_some failure then "External prover failed." - else if rc <> 0 then "External prover failed: " ^ proof - else "Try this command: " ^ - produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno) + if is_some failure then ("External prover failed.", []) + else if rc <> 0 then ("External prover failed: " ^ proof, []) + else apfst (fn s => "Try this command: " ^ s) + (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno)) val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof) in (success, message, proof, thm_names, the_filtered_clauses) end; diff -r 6b93b73a712b -r 8f0dc876fb1b src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Fri Aug 28 19:57:12 2009 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Sat Aug 29 21:57:06 2009 +0200 @@ -17,10 +17,10 @@ (* extracting lemma list*) val find_failure: string -> string option val lemma_list: bool -> string -> - string * string vector * (int * int) * Proof.context * Thm.thm * int -> string + string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list (* structured proofs *) val structured_proof: string -> - string * string vector * (int * int) * Proof.context * Thm.thm * int -> string + string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list end; structure ResReconstruct : RES_RECONSTRUCT = @@ -554,9 +554,10 @@ fun lemma_list dfg name result = let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result - in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^ + in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^ (if used_conj then "" - else "\nWarning: Goal is provable because context is inconsistent.") + else "\nWarning: Goal is provable because context is inconsistent."), + lemmas) end; (* === Extracting structured Isar-proof === *) @@ -567,11 +568,11 @@ val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c) val proofextract = get_proof_extract proof val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract)) - val one_line_proof = lemma_list false name result + val (one_line_proof, lemma_names) = lemma_list false name result val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then "" else decode_tstp_file cnfs ctxt goal subgoalno thm_names in - one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured + (one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured, lemma_names) end end;