# HG changeset patch # User wenzelm # Date 1256828903 -3600 # Node ID 44f9665c20911144439c3206efca890150ff606e # Parent 5f67433e6dd8772961f011f47499a7749723e80b proper header; tuned whitespace; diff -r 5f67433e6dd8 -r 44f9665c2091 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Thu Oct 29 16:07:27 2009 +0100 +++ b/src/HOL/Tools/res_reconstruct.ML Thu Oct 29 16:08:23 2009 +0100 @@ -1,8 +1,9 @@ -(* Author: L C Paulson and Claire Quigley, Cambridge University Computer Laboratory *) +(* Title: HOL/Tools/res_reconstruct.ML + Author: Lawrence C Paulson and Claire Quigley, Cambridge University Computer Laboratory -(***************************************************************************) -(* Code to deal with the transfer of proofs from a prover process *) -(***************************************************************************) +Transfer of proofs from external provers. +*) + signature RES_RECONSTRUCT = sig val chained_hint: string @@ -456,124 +457,128 @@ end; - (*=== EXTRACTING PROOF-TEXT === *) +(*=== EXTRACTING PROOF-TEXT === *) - val begin_proof_strings = ["# SZS output start CNFRefutation.", - "=========== Refutation ==========", +val begin_proof_strings = ["# SZS output start CNFRefutation.", + "=========== Refutation ==========", "Here is a proof"]; - val end_proof_strings = ["# SZS output end CNFRefutation", - "======= End of refutation =======", + +val end_proof_strings = ["# SZS output end CNFRefutation", + "======= End of refutation =======", "Formulae used in the proof"]; - fun get_proof_extract proof = - let + +fun get_proof_extract proof = + let (*splits to_split by the first possible of a list of splitters*) val (begin_string, end_string) = (find_first (fn s => String.isSubstring s proof) begin_proof_strings, find_first (fn s => String.isSubstring s proof) end_proof_strings) - in - if is_none begin_string orelse is_none end_string - then error "Could not extract proof (no substring indicating a proof)" - else proof |> first_field (the begin_string) |> the |> snd - |> first_field (the end_string) |> the |> fst end; + in + if is_none begin_string orelse is_none end_string + then error "Could not extract proof (no substring indicating a proof)" + else proof |> first_field (the begin_string) |> the |> snd + |> first_field (the end_string) |> the |> fst + end; (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *) - val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable", - "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"]; - val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"]; - val failure_strings_SPASS = ["SPASS beiseite: Completion found.", - "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."]; - val failure_strings_remote = ["Remote-script could not extract proof"]; - fun find_failure proof = - let val failures = - map_filter (fn s => if String.isSubstring s proof then SOME s else NONE) - (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote) - val correct = null failures andalso - exists (fn s => String.isSubstring s proof) begin_proof_strings andalso - exists (fn s => String.isSubstring s proof) end_proof_strings - in - if correct then NONE - else if null failures then SOME "Output of ATP not in proper format" - else SOME (hd failures) end; +val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable", + "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"]; +val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"]; +val failure_strings_SPASS = ["SPASS beiseite: Completion found.", + "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."]; +val failure_strings_remote = ["Remote-script could not extract proof"]; +fun find_failure proof = + let val failures = + map_filter (fn s => if String.isSubstring s proof then SOME s else NONE) + (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote) + val correct = null failures andalso + exists (fn s => String.isSubstring s proof) begin_proof_strings andalso + exists (fn s => String.isSubstring s proof) end_proof_strings + in + if correct then NONE + else if null failures then SOME "Output of ATP not in proper format" + else SOME (hd failures) end; - (* === EXTRACTING LEMMAS === *) - (* lines have the form "cnf(108, axiom, ...", - the number (108) has to be extracted)*) - fun get_step_nums false proofextract = - let val toks = String.tokens (not o Char.isAlphaNum) - fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok - | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok - | inputno _ = NONE - val lines = split_lines proofextract - in map_filter (inputno o toks) lines end - (*String contains multiple lines. We want those of the form - "253[0:Inp] et cetera..." - A list consisting of the first number in each line is returned. *) - | get_step_nums true proofextract = - let val toks = String.tokens (not o Char.isAlphaNum) - fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok - | inputno _ = NONE - val lines = split_lines proofextract - in map_filter (inputno o toks) lines end - - (*extracting lemmas from tstp-output between the lines from above*) - fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) = +(* === EXTRACTING LEMMAS === *) +(* lines have the form "cnf(108, axiom, ...", +the number (108) has to be extracted)*) +fun get_step_nums false proofextract = + let val toks = String.tokens (not o Char.isAlphaNum) + fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok + | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok + | inputno _ = NONE + val lines = split_lines proofextract + in map_filter (inputno o toks) lines end +(*String contains multiple lines. We want those of the form + "253[0:Inp] et cetera..." + A list consisting of the first number in each line is returned. *) +| get_step_nums true proofextract = + let val toks = String.tokens (not o Char.isAlphaNum) + fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok + | inputno _ = NONE + val lines = split_lines proofextract + in map_filter (inputno o toks) lines end + +(*extracting lemmas from tstp-output between the lines from above*) +fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) = + let + (* get the names of axioms from their numbers*) + fun get_axiom_names thm_names step_nums = let - (* get the names of axioms from their numbers*) - fun get_axiom_names thm_names step_nums = - let - val last_axiom = Vector.length thm_names - fun is_axiom n = n <= last_axiom - fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count - fun getname i = Vector.sub(thm_names, i-1) - in - (sort_distinct string_ord (filter (fn x => x <> "??.unknown") - (map getname (filter is_axiom step_nums))), - exists is_conj step_nums) - end - val proofextract = get_proof_extract proof + val last_axiom = Vector.length thm_names + fun is_axiom n = n <= last_axiom + fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count + fun getname i = Vector.sub(thm_names, i-1) in - get_axiom_names thm_names (get_step_nums proofextract) - end; + (sort_distinct string_ord (filter (fn x => x <> "??.unknown") + (map getname (filter is_axiom step_nums))), + exists is_conj step_nums) + end + val proofextract = get_proof_extract proof + in + get_axiom_names thm_names (get_step_nums proofextract) + end; - (*Used to label theorems chained into the sledgehammer call*) - val chained_hint = "CHAINED"; - val nochained = filter_out (fn y => y = chained_hint) - - (* metis-command *) - fun metis_line [] = "apply metis" - | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")" +(*Used to label theorems chained into the sledgehammer call*) +val chained_hint = "CHAINED"; +val nochained = filter_out (fn y => y = chained_hint) + +(* metis-command *) +fun metis_line [] = "apply metis" + | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")" - (* 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 " " (nochained lemmas)) +(* 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 " " (nochained lemmas)) - fun sendback_metis_nochained lemmas = - (Markup.markup Markup.sendback o metis_line) (nochained lemmas) +fun sendback_metis_nochained lemmas = + (Markup.markup Markup.sendback o metis_line) (nochained lemmas) - 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 ^ - (if used_conj then "" - else "\nWarning: Goal is provable because context is inconsistent."), - nochained lemmas) - end; +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 ^ + (if used_conj then "" + else "\nWarning: Goal is provable because context is inconsistent."), + nochained lemmas) + end; - (* === Extracting structured Isar-proof === *) - fun structured_proof name (result as (proof, thm_names, conj_count, ctxt, goal, subgoalno)) = - let - (*Could use split_lines, but it can return blank lines...*) - val lines = String.tokens (equal #"\n"); - 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_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, lemma_names) - end +(* === Extracting structured Isar-proof === *) +fun structured_proof name (result as (proof, thm_names, conj_count, ctxt, goal, subgoalno)) = + let + (*Could use split_lines, but it can return blank lines...*) + val lines = String.tokens (equal #"\n"); + 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_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, lemma_names) +end end;