improved proof parsing

--- a/src/HOL/Tools/ATP/AtpCommunication.ML	Wed Sep 21 18:35:19 2005 +0200
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Wed Sep 21 18:35:31 2005 +0200
@@ -44,13 +44,11 @@
      o snd o cut_after ":"
      o snd o cut_after "Here is a proof with"
      o fst o cut_after " ||  -> .") s
-  else if cut_exists start_V8 s then
+  else if cut_exists end_V8 s then
     (kill_lines 0    (*Vampire 8.0*)
-     o snd o cut_after start_V8
      o fst o cut_before end_V8) s
   else if cut_exists end_E s then
     (kill_lines 0    (*eproof*)
-     o snd o cut_after start_E
      o fst o cut_before end_E) s
   else "??extract_proof failed" (*Couldn't find a proof*)
 end;
@@ -61,124 +59,82 @@
 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
 (*********************************************************************************)
 
-fun startTransfer (startS,endS)
-      (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
- let val thisLine = TextIO.inputLine fromChild
-     fun transferInput currentString =
+fun startTransfer (endS, fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
+ let fun transferInput currentString =
       let val thisLine = TextIO.inputLine fromChild
       in
 	if thisLine = "" (*end of file?*)
 	then (File.write (File.tmp_path (Path.basic"extraction_failed")) 
-	                 ("start bracket: " ^ startS ^
-	                  "\nend bracket: " ^ endS ^
+	                 ("end bracket: " ^ endS ^
 	                  "\naccumulated text: " ^ currentString);
 	      raise EOF)                    
 	else if String.isPrefix endS thisLine
 	then let val proofextract = extract_proof (currentString^thisLine)
 	     in
 	       File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; 
-	       Recon_Transfer.prover_lemma_list proofextract goalstring toParent ppid clause_arr
+	       (if endS = end_V8 (*vampire?*)
+		then Recon_Transfer.vamp_lemma_list
+		else Recon_Transfer.e_lemma_list)
+	           proofextract goalstring toParent ppid clause_arr
 	     end
 	else transferInput (currentString^thisLine)
       end
  in
-   if thisLine = "" then false
-   else if String.isPrefix startS thisLine
-   then
-    (File.append (File.tmp_path (Path.basic "transfer_start"))
-		 ("about to transfer proof, first line is: " ^ thisLine);
-     transferInput thisLine;
-     true) handle EOF => false
-   else
-      startTransfer (startS,endS)
-                    (fromChild, toParent, ppid, goalstring,
-		     childCmd, clause_arr)
- end
+     transferInput "";  true
+ end handle EOF => false
+
+fun signal_parent (toParent, ppid, msg, goalstring) =
+ (TextIO.output (toParent, msg);
+  TextIO.output (toParent, goalstring^"\n");
+  TextIO.flushOut toParent;
+  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+  (*Space apart signals arising from multiple subgoals*)
+  Posix.Process.sleep(Time.fromMilliseconds 200));
 
 (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
 fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
- let val proof_file = TextIO.openAppend
-	   (File.platform_path(File.tmp_path (Path.basic "vampire_proof")))
-     val _ = File.write (File.tmp_path (Path.basic "vampire_checking_prf"))
-			("checking if proof found. childCmd is " ^ childCmd ^
-			 "\ngoalstring is: " ^ goalstring)
-     val thisLine = TextIO.inputLine fromChild
+ let val thisLine = TextIO.inputLine fromChild
  in   
-     File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
+     File.append (File.tmp_path (Path.basic "proof")) thisLine;
      if thisLine = "" 
-     then (TextIO.output (proof_file, "No proof output seen \n");
-	   TextIO.closeOut proof_file;
+     then (File.append (File.tmp_path (Path.basic "proof"))
+                      "No proof output seen \n";
 	   false)
-     else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine
+     else if String.isPrefix start_V8 thisLine
      then
-       startTransfer (start_V8, end_V8)
-	      (fromChild, toParent, ppid, goalstring,
-	       childCmd, clause_arr)
+       startTransfer (end_V8, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
      else if (String.isPrefix "Satisfiability detected" thisLine) orelse
              (String.isPrefix "Refutation not found" thisLine)
      then
-       (TextIO.output (toParent, "Failure\n");
-	TextIO.output (toParent, goalstring^"\n");
-	TextIO.flushOut toParent;
-	TextIO.output (proof_file, thisLine);
-	TextIO.closeOut proof_file;
-	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-	(* Attempt to prevent several signals from turning up simultaneously *)
-	Posix.Process.sleep(Time.fromSeconds 1);
+       (signal_parent (toParent, ppid, "Failure\n", goalstring);
 	true)
      else
-       (TextIO.output (proof_file, thisLine);
-	TextIO.flushOut proof_file;
-	checkVampProofFound  (fromChild, toParent, ppid, 
-	   goalstring,childCmd, clause_arr))
+        checkVampProofFound  (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
   end
 
 
 (*Called from watcher. Returns true if the E process has returned a verdict.*)
 fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, clause_arr) = 
- let val E_proof_file = TextIO.openAppend
-	   (File.platform_path(File.tmp_path (Path.basic "e_proof")))
-     val _ = File.write (File.tmp_path (Path.basic "e_checking_prf"))
-			("checking if proof found. childCmd is " ^ childCmd ^
-			 "\ngoalstring is: " ^ goalstring)
-     val thisLine = TextIO.inputLine fromChild  
+ let val thisLine = TextIO.inputLine fromChild  
  in   
-     File.write (File.tmp_path (Path.basic "e_response")) thisLine;
+     File.append (File.tmp_path (Path.basic "proof")) thisLine;
      if thisLine = "" 
-     then (TextIO.output (E_proof_file, "No proof output seen \n");
-	    TextIO.closeOut E_proof_file;
-	    false)
-     else if thisLine = "# TSTP exit status: Unsatisfiable\n"
+     then (File.append (File.tmp_path (Path.basic "proof"))
+                      "No proof output seen \n";
+	   false)
+     else if String.isPrefix start_E thisLine
      then      
-       startTransfer (start_E, end_E)
-             (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
+       startTransfer (end_E, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
      else if String.isPrefix "# Problem is satisfiable" thisLine
      then  
-       (TextIO.output (toParent, "Invalid\n");
-	TextIO.output (toParent, goalstring^"\n");
-	TextIO.flushOut toParent;
-	TextIO.output (E_proof_file, thisLine);
-	TextIO.closeOut E_proof_file;
-	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-	(* Attempt to prevent several signals from turning up simultaneously *)
-	Posix.Process.sleep(Time.fromSeconds 1);
+       (signal_parent (toParent, ppid, "Invalid\n", goalstring);
 	true)
      else if String.isPrefix "# Failure: Resource limit exceeded" thisLine
      then  (*In fact, E distingishes "out of time" and "out of memory"*)
-       (File.write (File.tmp_path (Path.basic "e_response")) thisLine;
-	TextIO.output (toParent, "Failure\n");
-	TextIO.output (toParent, goalstring^"\n");
-	TextIO.flushOut toParent;
-	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-	TextIO.output (E_proof_file, "signalled parent\n");
-	TextIO.closeOut E_proof_file;
-	(* Attempt to prevent several signals from turning up simultaneously *)
-	Posix.Process.sleep(Time.fromSeconds 1);
+       (signal_parent (toParent, ppid, "Failure\n", goalstring);
 	true)
      else
-	(TextIO.output (E_proof_file, thisLine);
-	TextIO.flushOut E_proof_file;
-	checkEProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr))
+	checkEProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
  end
 
 
@@ -207,7 +163,7 @@
     then 
       let val proofextract = extract_proof (currentString^thisLine)
       in 
-	 File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract;
+	 File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract;
 	 if !reconstruct 
 	 then (spass_reconstruct_tac proofextract goalstring toParent ppid sg_num 
 		clause_arr thm; ())
@@ -246,8 +202,6 @@
                           thm, sg_num, clause_arr) = 
  let val spass_proof_file = TextIO.openAppend
            (File.platform_path(File.tmp_path (Path.basic "spass_proof")))
-     val _ = File.write(File.tmp_path (Path.basic "spass_checking_prf"))
-		("checking if proof found, thm is: "^(string_of_thm thm))
      val thisLine = TextIO.inputLine fromChild  
  in    
      File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
@@ -263,24 +217,14 @@
      then  
        (TextIO.output (spass_proof_file, thisLine);
 	TextIO.closeOut spass_proof_file;
-	TextIO.output (toParent, "Invalid\n");
-	TextIO.output (toParent, goalstring^"\n");
-	TextIO.flushOut toParent;
-	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-	(* Attempt to prevent several signals from turning up simultaneously *)
-	Posix.Process.sleep(Time.fromSeconds 1);
+	signal_parent (toParent, ppid, "Invalid\n", goalstring);
 	true)
      else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
              thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
      then  
-       (TextIO.output (toParent, "Failure\n");
-	TextIO.output (toParent, goalstring^"\n");
-	TextIO.flushOut toParent;
-	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+       (signal_parent (toParent, ppid, "Failure\n", goalstring);
 	TextIO.output (spass_proof_file, "signalled parent\n");
 	TextIO.closeOut spass_proof_file;
-	(* Attempt to prevent several signals from turning up simultaneously *)
-	Posix.Process.sleep(Time.fromSeconds 1);
 	true)
     else
        (TextIO.output (spass_proof_file, thisLine);

--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 21 18:35:19 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 21 18:35:31 2005 +0200
@@ -189,7 +189,7 @@
     get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr
   end;
     
- (*String contains multiple lines, terminated with newline characters.
+ (*String contains multiple lines.
   A list consisting of the first number in each line is returned. *)
 fun get_linenums proofstr = 
   let val numerics = String.tokens (not o Char.isDigit)
@@ -198,9 +198,22 @@
       val lines = String.tokens (fn c => c = #"\n") proofstr
   in  List.mapPartial (firstno o numerics) lines  end
 
-fun get_axiom_names_vamp_E proofstr clause_arr  =
+fun get_axiom_names_e proofstr clause_arr  =
    get_axiom_names (get_linenums proofstr) clause_arr;
     
+ (*String contains multiple lines. We want those of the form 
+     "*********** [448, input] ***********".
+  A list consisting of the first number in each line is returned. *)
+fun get_vamp_linenums proofstr = 
+  let val toks = String.tokens (not o Char.isAlphaNum)
+      fun inputno [n,"input"] = Int.fromString n
+        | inputno _ = NONE
+      val lines = String.tokens (fn c => c = #"\n") proofstr
+  in  List.mapPartial (inputno o toks) lines  end
+
+fun get_axiom_names_vamp proofstr clause_arr  =
+   get_axiom_names (get_vamp_linenums proofstr) clause_arr;
+    
 
 (***********************************************)
 (* get axioms for reconstruction               *)
@@ -303,7 +316,9 @@
       (* Attempt to prevent several signals from turning up simultaneously *)
       Posix.Process.sleep(Time.fromSeconds 1); ());
 
-val prover_lemma_list = prover_lemma_list_aux get_axiom_names_vamp_E;
+val e_lemma_list = prover_lemma_list_aux get_axiom_names_e;
+
+val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
 
 val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;