# HG changeset patch # User paulson # Date 1159803138 -7200 # Node ID 32640c8956e70a5b681c331c9d6f6b796976aac5 # Parent 4b48fd429b18c82a5429cfb29f0b38fc823518b3 tidying and simplifying diff -r 4b48fd429b18 -r 32640c8956e7 src/HOL/Tools/ATP/AtpCommunication.ML --- a/src/HOL/Tools/ATP/AtpCommunication.ML Mon Oct 02 17:32:03 2006 +0200 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML Mon Oct 02 17:32:18 2006 +0200 @@ -123,36 +123,13 @@ val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass; -(**** Cutting lines of text FIXME: TIDY UP|!! ****) +(**** Extracting proofs from an ATP's output ****) -exception NOCUT -fun remove_prefix [] l = l - | remove_prefix (h::t) [] = error "can't remove prefix" - | remove_prefix (h::t) (h'::t') = remove_prefix t t' -fun ccut t [] = raise NOCUT - | ccut t s = - if is_prefix (op =) t s then ([], remove_prefix t s) else - let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end -fun cut t s = - let - val t' = explode t - val s' = explode s - val (a, b) = ccut t' s' - in - (implode a, implode b) - end - -fun cut_exists t s - = let val (a, b) = cut t s in true end handle NOCUT => false - -fun cut_before t s = let val (a, b) = cut t s in (a, t ^ b) end -fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end - -fun kill_lines 0 = Library.I - | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n"; - - -(**** Extracting proofs from an ATP's output ****) +(*Return everything in s that comes before the string t*) +fun cut_before t s = + let val (s1,s2) = Substring.position t (Substring.full s) + val _ = assert (Substring.size s2 <> 0) "cut_before: string not found" + in Substring.string s2 end; val start_E = "# Proof object starts here." val end_E = "# Proof object ends here." @@ -160,20 +137,7 @@ val end_V6 = "%============== End of proof. ==================" val start_V8 = "=========== Refutation ==========" val end_V8 = "======= End of refutation =======" - -(*Identifies the start/end lines of an ATP's output*) -fun extract_proof s = - if cut_exists "Formulae used in the proof" s then (*SPASS*) - (kill_lines 0 - o fst o cut_before "Formulae used in the proof") s - else if cut_exists end_V8 s then - (kill_lines 0 (*Vampire 8.0*) - o fst o cut_before end_V8) s - else if cut_exists end_E s then - (kill_lines 0 (*eproof*) - o fst o cut_before end_E) s - else "??extract_proof failed" (*Couldn't find a proof*) - +val end_SPASS = "Formulae used in the proof" (*********************************************************************************) (* Inspect the output of an ATP process to see if it has found a proof, *) @@ -189,9 +153,8 @@ "\naccumulated text: " ^ currentString); raise EOF) else if String.isPrefix endS thisLine - then let val proofextract = extract_proof (currentString^thisLine) - val lemma_list = if endS = end_V8 - then vamp_lemma_list + then let val proofextract = currentString ^ cut_before endS thisLine + val lemma_list = if endS = end_V8 then vamp_lemma_list else e_lemma_list in trace ("\nExtracted proof:\n" ^ proofextract); @@ -227,31 +190,27 @@ (String.isPrefix "Refutation not found" thisLine) then (signal_parent (toParent, ppid, "Failure\n", probfile); true) - else - checkVampProofFound (fromChild, toParent, ppid, probfile, names_arr) + else checkVampProofFound (fromChild, toParent, ppid, probfile, names_arr) end - (*Called from watcher. Returns true if the E process has returned a verdict.*) fun checkEProofFound (fromChild, toParent, ppid, probfile, names_arr) = let val thisLine = TextIO.inputLine fromChild in trace thisLine; - if thisLine = "" - then (trace "\nNo proof output seen"; false) + if thisLine = "" then (trace "\nNo proof output seen"; false) else if String.isPrefix start_E thisLine - then - startTransfer (end_E, fromChild, toParent, ppid, probfile, names_arr) + then startTransfer (end_E, fromChild, toParent, ppid, probfile, names_arr) else if String.isPrefix "# Problem is satisfiable" thisLine then (signal_parent (toParent, ppid, "Invalid\n", probfile); true) else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine then (signal_parent (toParent, ppid, "Failure\n", probfile); true) - else - checkEProofFound (fromChild, toParent, ppid, probfile, names_arr) + else checkEProofFound (fromChild, toParent, ppid, probfile, names_arr) end +(*FIXME: can't these two functions be replaced by startTransfer above?*) fun transferSpassInput (fromChild, toParent, ppid, probfile, currentString, thm, sg_num, names_arr) = let val thisLine = TextIO.inputLine fromChild @@ -262,25 +221,18 @@ raise EOF) else if String.isPrefix "Formulae used in the proof" thisLine then - let val proofextract = extract_proof (currentString^thisLine) + let val proofextract = currentString ^ cut_before end_SPASS thisLine in trace ("\nextracted spass proof: " ^ proofextract); - spass_lemma_list proofextract probfile toParent - ppid names_arr + spass_lemma_list proofextract probfile toParent ppid names_arr end else transferSpassInput (fromChild, toParent, ppid, probfile, - (currentString^thisLine), thm, sg_num, names_arr) + currentString ^ thisLine, thm, sg_num, names_arr) end; - -(*********************************************************************************) -(* Inspect the output of a Spass process to see if it has found a proof, *) -(* and if so, transfer output to the input pipe of the main Isabelle process *) -(*********************************************************************************) - - -fun startSpassTransfer (fromChild, toParent, ppid, probfile, - thm, sg_num,names_arr) = +(*Inspect the output of a SPASS process to see if it has found a proof, + and if so, transfer output to the input pipe of the main Isabelle process*) +fun startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,names_arr) = let val thisLine = TextIO.inputLine fromChild in if thisLine = "" then false @@ -294,8 +246,7 @@ (*Called from watcher. Returns true if the SPASS process has returned a verdict.*) -fun checkSpassProofFound (fromChild, toParent, ppid, probfile, - thm, sg_num, names_arr) = +fun checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr) = let val thisLine = TextIO.inputLine fromChild in trace thisLine;