# HG changeset patch # User blanchet # Date 1269011055 -3600 # Node ID 491a97039ce150ed52ed9b5cd5b0330c914ef708 # Parent 16279c4c7a3332e4e705df96ed627728debf0cf7 renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar"; "full" sounds like "full types" or something, not like a structured Isar proof -- at some point I hope to make this an option that's orthogonal to the prover diff -r 16279c4c7a33 -r 491a97039ce1 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 15:33:18 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 16:04:15 2010 +0100 @@ -184,7 +184,7 @@ emit_structured_proof = full}; val vampire = tptp_prover ("vampire", vampire_prover_config false); -val vampire_full = tptp_prover ("vampire_full", vampire_prover_config true); +val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true); (* E prover *) @@ -206,7 +206,7 @@ emit_structured_proof = full}; val eprover = tptp_prover ("e", eprover_config false); -val eprover_full = tptp_prover ("e_full", eprover_config true); +val eprover_isar = tptp_prover ("e_isar", eprover_config true); (* SPASS *) @@ -290,7 +290,7 @@ "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const); val provers = - [spass, vampire, eprover, vampire_full, eprover_full, spass_no_tc, + [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc, remote_vampire, remote_spass, remote_eprover] val prover_setup = fold add_prover provers diff -r 16279c4c7a33 -r 491a97039ce1 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Mar 19 15:33:18 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Mar 19 16:04:15 2010 +0100 @@ -428,26 +428,33 @@ fun isar_header [] = proofstart | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n"; -fun decode_tstp_file cnfs ctxt th sgno thm_names = - let val _ = trace_proof_msg (K "\ndecode_tstp_file: start\n") - val tuples = map (dest_tstp o tstp_line o explode) cnfs - val _ = trace_proof_msg (fn () => Int.toString (length tuples) ^ " tuples extracted\n") - val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt - val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples) - val _ = trace_proof_msg (fn () => Int.toString (length raw_lines) ^ " raw_lines extracted\n") - val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines - val _ = trace_proof_msg (fn () => Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n") - val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines - val _ = trace_proof_msg (fn () => Int.toString (length lines) ^ " lines extracted\n") - val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno - val _ = trace_proof_msg (fn () => Int.toString (length ccls) ^ " conjecture clauses\n") - val ccls = map forall_intr_vars ccls - val _ = app (fn th => trace_proof_msg (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls - val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines) - val _ = trace_proof_msg (K "\ndecode_tstp_file: finishing\n") - in - isar_header (map #1 fixes) ^ implode ilines ^ "qed\n" - end handle STREE _ => error "Could not extract proof (ATP output malformed?)"; +fun isar_proof_from_tstp_file cnfs ctxt th sgno thm_names = + let + val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n") + val tuples = map (dest_tstp o tstp_line o explode) cnfs + val _ = trace_proof_msg (fn () => + Int.toString (length tuples) ^ " tuples extracted\n") + val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt + val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples) + val _ = trace_proof_msg (fn () => + Int.toString (length raw_lines) ^ " raw_lines extracted\n") + val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines + val _ = trace_proof_msg (fn () => + Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n") + val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines + val _ = trace_proof_msg (fn () => + Int.toString (length lines) ^ " lines extracted\n") + val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno + val _ = trace_proof_msg (fn () => + Int.toString (length ccls) ^ " conjecture clauses\n") + val ccls = map forall_intr_vars ccls + val _ = app (fn th => trace_proof_msg + (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls + val isar_lines = isar_lines ctxt (map prop_of ccls) + (stringify_deps thm_names [] lines) + val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n") + in isar_header (map #1 fixes) ^ implode isar_lines ^ "qed\n" end + handle STREE _ => error "Could not extract proof (ATP output malformed?)"; (*=== EXTRACTING PROOF-TEXT === *) @@ -530,19 +537,17 @@ (* atp_minimize [atp=] *) fun minimize_line _ [] = "" | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^ - (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^ - space_implode " " (kill_chained lemmas)) - -val sendback_metis_no_chained = - Markup.markup Markup.sendback o metis_line o kill_chained + Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^ + space_implode " " (kill_chained lemmas)) fun metis_lemma_list dfg name result = - let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result - in (sendback_metis_no_chained lemmas ^ "\n" ^ minimize_line name lemmas ^ - (if used_conj then - "" - else - "\nWarning: The goal is provable because the context is inconsistent."), + let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in + (Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^ + minimize_line name lemmas ^ + (if used_conj then + "" + else + "\nWarning: The goal is provable because the context is inconsistent."), kill_chained lemmas) end; @@ -551,15 +556,17 @@ let (* Could use "split_lines", but it can return blank lines *) val lines = String.tokens (equal #"\n"); - val kill_spaces = String.translate (fn c => if Char.isSpace c then "" else str c) + val kill_spaces = + String.translate (fn c => if Char.isSpace c then "" else str c) val extract = get_proof_extract proof val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract)) val (one_line_proof, lemma_names) = metis_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 + val tokens = String.tokens (fn c => c = #" ") one_line_proof + val isar_proof = + if member (op =) tokens chained_hint then "" + else isar_proof_from_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 isar_proof, lemma_names) end