consolidation of duplicate code in Isabelle-ATP linkup
authorpaulson
Thu Sep 08 17:35:02 2005 +0200 (2005-09-08)
changeset 173155bf0e0aacc24
parent 17314 04e21a27c0ad
child 17316 fc7cc8137b97
consolidation of duplicate code in Isabelle-ATP linkup
src/HOL/Reconstruction.thy
src/HOL/Tools/ATP/ECommunication.ML
src/HOL/Tools/ATP/SpassCommunication.ML
src/HOL/Tools/ATP/VampCommunication.ML
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/watcher.ML
     1.1 --- a/src/HOL/Reconstruction.thy	Thu Sep 08 16:09:23 2005 +0200
     1.2 +++ b/src/HOL/Reconstruction.thy	Thu Sep 08 17:35:02 2005 +0200
     1.3 @@ -22,7 +22,6 @@
     1.4  	 "Tools/ATP/recon_transfer_proof.ML"
     1.5  	 "Tools/ATP/VampCommunication.ML"
     1.6  	 "Tools/ATP/SpassCommunication.ML"
     1.7 -     "Tools/ATP/ECommunication.ML"
     1.8  	 "Tools/ATP/watcher.ML"
     1.9  	 "Tools/ATP/res_clasimpset.ML"
    1.10  	 "Tools/res_atp.ML"
     2.1 --- a/src/HOL/Tools/ATP/ECommunication.ML	Thu Sep 08 16:09:23 2005 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,222 +0,0 @@
     2.4 -(*  Title:      SpassCommunication.ml
     2.5 -    ID:         $Id$
     2.6 -    Author:     Claire Quigley
     2.7 -    Copyright   2004  University of Cambridge
     2.8 -*)
     2.9 -
    2.10 -(***************************************************************************)
    2.11 -(*  Code to deal with the transfer of proofs from a E process          *)
    2.12 -(***************************************************************************)
    2.13 -signature E_COMM =
    2.14 -  sig
    2.15 -    val E: bool ref
    2.16 -    val getEInput : TextIO.instream -> string * string * string
    2.17 -    val checkEProofFound: 
    2.18 -          TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
    2.19 -          string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
    2.20 -  end;
    2.21 -
    2.22 -structure EComm : E_COMM =
    2.23 -struct
    2.24 -
    2.25 -val E = ref false;
    2.26 -
    2.27 -exception EOF;
    2.28 -
    2.29 -(**********************************************************************)
    2.30 -(*  Reconstruct the E proof w.r.t. thmstring (string version of   *)
    2.31 -(*  Isabelle goal to be proved), then transfer the reconstruction     *)
    2.32 -(*  steps as a string to the input pipe of the main Isabelle process  *)
    2.33 -(**********************************************************************)
    2.34 -
    2.35 -fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
    2.36 -                    clause_arr num_of_clauses = 
    2.37 -   SELECT_GOAL
    2.38 -    (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
    2.39 -             METAHYPS(fn negs => 
    2.40 -    (Recon_Transfer.EString_to_lemmaString proofextract thmstring goalstring 
    2.41 -              toParent ppid negs clause_arr  num_of_clauses ))]) sg_num	
    2.42 -
    2.43 -
    2.44 -fun transferEInput (fromChild, toParent, ppid,thmstring,goalstring, 
    2.45 -                    currentString, thm, sg_num,clause_arr, num_of_clauses) = 
    2.46 - let val thisLine = TextIO.inputLine fromChild 
    2.47 - in 
    2.48 -     File.append (File.tmp_path (Path.basic "eprover_transfer"))
    2.49 -		      ("transferEInput input line: " ^ thisLine);        
    2.50 -    if thisLine = "" (*end of file?*)
    2.51 -    then (File.write (File.tmp_path (Path.basic"eprover_extraction_failed")) currentString;
    2.52 -	  raise EOF)                    
    2.53 -    else if thisLine = "# Proof object ends here.\n"
    2.54 -    then 
    2.55 -      let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    2.56 -      in 
    2.57 -	  File.write (File.tmp_path (Path.basic"eprover_extracted_prf")) proofextract;
    2.58 -	  reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
    2.59 -	      clause_arr num_of_clauses thm
    2.60 -      end
    2.61 -    else transferEInput (fromChild, toParent, ppid,thmstring, goalstring,
    2.62 -			     (currentString^thisLine), thm, sg_num, clause_arr, 
    2.63 -			     num_of_clauses)
    2.64 - end;
    2.65 -
    2.66 -
    2.67 -(*********************************************************************************)
    2.68 -(*  Inspect the output of an E process to see if it has found a proof,     *)
    2.69 -(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    2.70 -(*********************************************************************************)
    2.71 -
    2.72 - 
    2.73 -fun startETransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
    2.74 -                    thm, sg_num,clause_arr, num_of_clauses) = 
    2.75 -    let val thisLine = TextIO.inputLine fromChild  
    2.76 -    in                 
    2.77 -      if thisLine = "" then false
    2.78 -      else if String.isPrefix "# Proof object starts" thisLine 
    2.79 -      then     
    2.80 -	 (File.append (File.tmp_path (Path.basic "eprover_transfer"))
    2.81 -		      ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n");
    2.82 -	  transferEInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, 
    2.83 -			      thm, sg_num,clause_arr, num_of_clauses);
    2.84 -	  true) handle EOF => false
    2.85 -      else startETransfer (fromChild, toParent, ppid, thmstring, goalstring,
    2.86 -			       childCmd, thm, sg_num,clause_arr, num_of_clauses)
    2.87 -     end
    2.88 -
    2.89 -
    2.90 -fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd,
    2.91 -                      thm, sg_num, clause_arr, num_of_clauses) = 
    2.92 - let val E_proof_file = TextIO.openAppend
    2.93 -	   (File.platform_path(File.tmp_path (Path.basic "eprover_proof")))
    2.94 -     val _ = File.write (File.tmp_path (Path.basic "eprover_checking_prf"))
    2.95 -			("checking if proof found, thm is: " ^ string_of_thm thm)
    2.96 -     val thisLine = TextIO.inputLine fromChild  
    2.97 - in   
    2.98 -     if thisLine = "" 
    2.99 -     then (TextIO.output (E_proof_file, ("No proof output seen \n"));
   2.100 -	    TextIO.closeOut E_proof_file;
   2.101 -	    false)
   2.102 -     else if (*thisLine = "# Problem is unsatisfiable (or provable), constructing proof object\n"*)
   2.103 -	 thisLine = "# TSTP exit status: Unsatisfiable\n"
   2.104 -     then      
   2.105 -       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
   2.106 -	startETransfer (fromChild, toParent, ppid, thmstring,goalstring,
   2.107 -			childCmd, thm, sg_num, clause_arr, num_of_clauses))
   2.108 -     else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n"
   2.109 -     then  
   2.110 -       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
   2.111 -	TextIO.output (toParent,childCmd^"\n" );
   2.112 -	TextIO.flushOut toParent;
   2.113 -	TextIO.output (E_proof_file, thisLine);
   2.114 -	TextIO.closeOut E_proof_file;
   2.115 -
   2.116 -	TextIO.output (toParent, thisLine^"\n");
   2.117 -	TextIO.output (toParent, thmstring^"\n");
   2.118 -	TextIO.output (toParent, goalstring^"\n");
   2.119 -	TextIO.flushOut toParent;
   2.120 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.121 -	(* Attempt to prevent several signals from turning up simultaneously *)
   2.122 -	Posix.Process.sleep(Time.fromSeconds 1);
   2.123 -	 true)
   2.124 -     else if thisLine = "# Failure: Resource limit exceeded (time)\n" 
   2.125 -     then  
   2.126 -       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
   2.127 -	TextIO.output (toParent, thisLine^"\n");
   2.128 -	TextIO.output (toParent, thmstring^"\n");
   2.129 -	TextIO.output (toParent, goalstring^"\n");
   2.130 -	TextIO.flushOut toParent;
   2.131 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.132 -	TextIO.output (E_proof_file, "signalled parent\n");
   2.133 -	TextIO.closeOut E_proof_file;
   2.134 -	(* Attempt to prevent several signals from turning up simultaneously *)
   2.135 -	Posix.Process.sleep(Time.fromSeconds 1);
   2.136 -	true)
   2.137 -     else if thisLine = "# Failure: Resource limit exceeded (memory)\n"                                                            		                 
   2.138 -     then
   2.139 -	(Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.140 -	 TextIO.output (toParent,childCmd^"\n" );
   2.141 -	 TextIO.flushOut toParent;
   2.142 -	 TextIO.output (toParent, thisLine);
   2.143 -	 TextIO.flushOut toParent;
   2.144 -	 true)
   2.145 -     else
   2.146 -	(TextIO.output (E_proof_file, thisLine);
   2.147 -	TextIO.flushOut E_proof_file;
   2.148 -	checkEProofFound  (fromChild, toParent, ppid, thmstring,goalstring,
   2.149 -	childCmd, thm, sg_num, clause_arr, num_of_clauses))
   2.150 - end
   2.151 -
   2.152 -
   2.153 -  
   2.154 -(***********************************************************************)
   2.155 -(*  Function used by the Isabelle process to read in an E proof   *)
   2.156 -(***********************************************************************)
   2.157 -
   2.158 -fun getEInput instr = 
   2.159 -    let val thisLine = TextIO.inputLine instr 
   2.160 -        val _ = File.write (File.tmp_path (Path.basic "eprover_line")) thisLine
   2.161 -    in 
   2.162 -      if thisLine = "" then ("No output from reconstruction process.\n","","")
   2.163 -      else if String.sub (thisLine, 0) = #"["
   2.164 -      then 
   2.165 -	let val reconstr = thisLine
   2.166 -	    val thmstring = TextIO.inputLine instr 
   2.167 -	    val goalstring = TextIO.inputLine instr   
   2.168 -	in
   2.169 -	    (reconstr, thmstring, goalstring)
   2.170 -	end
   2.171 -      else if String.isPrefix "SPASS beiseite:" thisLine (*FIXME: wrong!!*)
   2.172 -      then 
   2.173 -	 let val reconstr = thisLine
   2.174 -	     val thmstring = TextIO.inputLine instr
   2.175 -	     val goalstring = TextIO.inputLine instr
   2.176 -	 in
   2.177 -	     (reconstr, thmstring, goalstring)
   2.178 -	 end
   2.179 -
   2.180 -       else if String.isPrefix "# No proof" thisLine 
   2.181 -      then 
   2.182 -	 let val reconstr = thisLine
   2.183 -	     val thmstring = TextIO.inputLine instr
   2.184 -	     val goalstring = TextIO.inputLine instr
   2.185 -	 in
   2.186 -	     (reconstr, thmstring, goalstring)
   2.187 -	 end
   2.188 -
   2.189 -       else if String.isPrefix "# Failure" thisLine 
   2.190 -      then 
   2.191 -	 let val reconstr = thisLine
   2.192 -	     val thmstring = TextIO.inputLine instr
   2.193 -	     val goalstring = TextIO.inputLine instr
   2.194 -	 in
   2.195 -	     (reconstr, thmstring, goalstring)
   2.196 -	 end
   2.197 -      else if String.isPrefix  "Rules from"  thisLine
   2.198 -      then 
   2.199 -	   let val reconstr = thisLine
   2.200 -	       val thmstring = TextIO.inputLine instr
   2.201 -	       val goalstring = TextIO.inputLine instr
   2.202 -	   in
   2.203 -	       (reconstr, thmstring, goalstring)
   2.204 -	   end
   2.205 -      else if substring (thisLine, 0,5) = "Proof"
   2.206 -      then
   2.207 -	let val reconstr = thisLine
   2.208 -	    val thmstring = TextIO.inputLine instr
   2.209 -	    val goalstring = TextIO.inputLine instr
   2.210 -	in
   2.211 -          File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine;
   2.212 -          (reconstr, thmstring, goalstring)
   2.213 -        end
   2.214 -      else if substring (thisLine, 0,1) = "%"
   2.215 -      then
   2.216 -	let val reconstr = thisLine
   2.217 -	    val thmstring = TextIO.inputLine instr
   2.218 -	    val goalstring = TextIO.inputLine instr
   2.219 -	in
   2.220 -           File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine;
   2.221 -	   (reconstr, thmstring, goalstring)
   2.222 -	end
   2.223 -      else getEInput instr
   2.224 -     end
   2.225 -end;
     3.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Thu Sep 08 16:09:23 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Thu Sep 08 17:35:02 2005 +0200
     3.3 @@ -48,7 +48,7 @@
     3.4   let val thisLine = TextIO.inputLine fromChild 
     3.5   in 
     3.6      if thisLine = "" (*end of file?*)
     3.7 -    then (File.write (File.tmp_path (Path.basic"eprover_extraction_failed")) currentString;
     3.8 +    then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString;
     3.9  	  raise EOF)                    
    3.10      else if thisLine = "--------------------------SPASS-STOP------------------------------\n"
    3.11      then 
     4.1 --- a/src/HOL/Tools/ATP/VampCommunication.ML	Thu Sep 08 16:09:23 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/VampCommunication.ML	Thu Sep 08 17:35:02 2005 +0200
     4.3 @@ -9,6 +9,11 @@
     4.4  (***************************************************************************)
     4.5  signature VAMP_COMM =
     4.6    sig
     4.7 +    val getEInput : TextIO.instream -> string * string * string
     4.8 +    val checkEProofFound: 
     4.9 +          TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
    4.10 +          string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
    4.11 +
    4.12      val getVampInput : TextIO.instream -> string * string * string
    4.13      val checkVampProofFound: 
    4.14            TextIO.instream * TextIO.outstream * Posix.Process.pid * string *
    4.15 @@ -21,7 +26,7 @@
    4.16  exception EOF;
    4.17  
    4.18  (**********************************************************************)
    4.19 -(*  Reconstruct the Vampire proof w.r.t. thmstring (string version of   *)
    4.20 +(*  Reconstruct the Vampire/E proof w.r.t. thmstring (string version of   *)
    4.21  (*  Isabelle goal to be proved), then transfer the reconstruction     *)
    4.22  (*  steps as a string to the input pipe of the main Isabelle process  *)
    4.23  (**********************************************************************)
    4.24 @@ -32,121 +37,165 @@
    4.25        (EVERY1
    4.26          [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
    4.27  	 METAHYPS(fn negs =>
    4.28 -		     (Recon_Transfer.vampString_to_lemmaString proofextract thmstring 
    4.29 +		     (Recon_Transfer.proverString_to_lemmaString proofextract thmstring 
    4.30  		       goalstring toParent ppid negs clause_arr num_of_clauses))]) sg_num
    4.31  
    4.32  
    4.33 -fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, 
    4.34 -                       currentString, thm, sg_num,clause_arr, num_of_clauses) =
    4.35 -  let val thisLine = TextIO.inputLine fromChild
    4.36 -  in
    4.37 -    if thisLine = "" (*end of file?*)
    4.38 -    then (File.write (File.tmp_path (Path.basic"vampire_extraction_failed")) currentString;
    4.39 -	  raise EOF)                    
    4.40 -    else if (thisLine = "%==============  End of proof. ==================\n" )
    4.41 -    then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    4.42 -	 in
    4.43 -	   File.write (File.tmp_path (Path.basic"vampire_extracted_prf")) proofextract; 
    4.44 -	   reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  
    4.45 -	                   clause_arr num_of_clauses thm
    4.46 -	 end
    4.47 -    else transferVampInput (fromChild, toParent, ppid,thmstring, goalstring, 
    4.48 -             currentString^thisLine, thm, sg_num, clause_arr, num_of_clauses)
    4.49 -  end;
    4.50 -
    4.51 -
    4.52  (*********************************************************************************)
    4.53 -(*  Inspect the output of a Vampire process to see if it has found a proof,     *)
    4.54 +(*  Inspect the output of an ATP process to see if it has found a proof,     *)
    4.55  (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    4.56  (*********************************************************************************)
    4.57  
    4.58 -
    4.59 -fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
    4.60 -                       thm, sg_num,clause_arr, num_of_clauses) =
    4.61 -    let val thisLine = TextIO.inputLine fromChild
    4.62 -    in
    4.63 -      if thisLine = "" then false
    4.64 -      else if (thisLine = "%================== Proof: ======================\n")
    4.65 -      then
    4.66 -       (File.append (File.tmp_path (Path.basic "vampire_transfer"))
    4.67 -		    ("about to transfer proof, thm is: " ^ string_of_thm thm);
    4.68 -	transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,
    4.69 -			   thisLine, thm, sg_num,clause_arr, num_of_clauses);
    4.70 -	true) handle EOF => false
    4.71 -      else
    4.72 -	 startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,
    4.73 -			    childCmd, thm, sg_num,clause_arr, num_of_clauses)
    4.74 -    end
    4.75 +fun startTransfer (startS,endS)
    4.76 +      (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
    4.77 +       thm, sg_num,clause_arr, num_of_clauses) =
    4.78 + let val thisLine = TextIO.inputLine fromChild
    4.79 +     fun transferInput currentString =
    4.80 +      let val thisLine = TextIO.inputLine fromChild
    4.81 +      in
    4.82 +	if thisLine = "" (*end of file?*)
    4.83 +	then (File.write (File.tmp_path (Path.basic"extraction_failed")) 
    4.84 +	                 ("start bracket: " ^ startS ^
    4.85 +	                  "\nend bracket: " ^ endS ^
    4.86 +	                  "\naccumulated text: " ^ currentString);
    4.87 +	      raise EOF)                    
    4.88 +	else if String.isPrefix endS thisLine
    4.89 +	then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    4.90 +	     in
    4.91 +	       File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; 
    4.92 +	       reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  
    4.93 +			       clause_arr num_of_clauses thm
    4.94 +	     end
    4.95 +	else transferInput (currentString^thisLine)
    4.96 +      end
    4.97 + in
    4.98 +   if thisLine = "" then false
    4.99 +   else if String.isPrefix startS thisLine
   4.100 +   then
   4.101 +    (File.append (File.tmp_path (Path.basic "transfer_start"))
   4.102 +		 ("about to transfer proof, thm is: " ^ string_of_thm thm);
   4.103 +     transferInput thisLine;
   4.104 +     true) handle EOF => false
   4.105 +   else
   4.106 +      startTransfer (startS,endS)
   4.107 +                    (fromChild, toParent, ppid, thmstring, goalstring,
   4.108 +		     childCmd, thm, sg_num,clause_arr, num_of_clauses)
   4.109 + end
   4.110  
   4.111  
   4.112  fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, 
   4.113                           thm, sg_num, clause_arr, num_of_clauses) =
   4.114 - let val vamp_proof_file = TextIO.openAppend
   4.115 -	   (File.platform_path(File.tmp_path (Path.basic "vampire_proof")))
   4.116 -     val _ = File.write (File.tmp_path (Path.basic "vampire_checking_prf"))
   4.117 + let val proof_file = TextIO.openAppend
   4.118 +	   (File.platform_path(File.tmp_path (Path.basic "atp_proof")))
   4.119 +     val _ = File.write (File.tmp_path (Path.basic "atp_checking_prf"))
   4.120  			("checking if proof found, thm is: " ^ string_of_thm thm)
   4.121       val thisLine = TextIO.inputLine fromChild
   4.122   in   
   4.123       if thisLine = "" 
   4.124 -     then (TextIO.output (vamp_proof_file, ("No proof output seen \n"));
   4.125 -	   TextIO.closeOut vamp_proof_file;
   4.126 +     then (TextIO.output (proof_file, "No proof output seen \n");
   4.127 +	   TextIO.closeOut proof_file;
   4.128  	   false)
   4.129       else if thisLine = "% Proof found. Thanks to Tanya!\n"
   4.130       then
   4.131 -      (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
   4.132 -       startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,
   4.133 -			  childCmd, thm, sg_num, clause_arr, num_of_clauses))
   4.134 -     else if (thisLine = "% Unprovable.\n" )
   4.135 +       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
   4.136 +	startTransfer (Recon_Parse.start_V6, Recon_Parse.end_V6)
   4.137 +	      (fromChild, toParent, ppid, thmstring, goalstring,
   4.138 +	       childCmd, thm, sg_num, clause_arr, num_of_clauses))
   4.139 +     else if (thisLine = "% Unprovable.\n" ) orelse
   4.140 +             (thisLine = "% Proof not found. Time limit expired.\n")
   4.141       then
   4.142 -      (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
   4.143 -       TextIO.output (toParent,childCmd^"\n" );
   4.144 -       TextIO.flushOut toParent;
   4.145 -       TextIO.output (vamp_proof_file, thisLine);
   4.146 -       TextIO.closeOut vamp_proof_file;
   4.147 -       (*TextIO.output (toParent, thisLine);
   4.148 +       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
   4.149 +	TextIO.output (toParent,childCmd^"\n");
   4.150  	TextIO.flushOut toParent;
   4.151 -	TextIO.output (toParent, "bar\n");
   4.152 -	TextIO.flushOut toParent;*)
   4.153 -
   4.154 -       TextIO.output (toParent, thisLine^"\n");
   4.155 -       TextIO.output (toParent, thmstring^"\n");
   4.156 -       TextIO.output (toParent, goalstring^"\n");
   4.157 -       TextIO.flushOut toParent;
   4.158 -       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.159 -       (* Attempt to prevent several signals from turning up simultaneously *)
   4.160 -       Posix.Process.sleep(Time.fromSeconds 1);
   4.161 -       true)
   4.162 -     else if (thisLine = "% Proof not found. Time limit expired.\n")
   4.163 -     then
   4.164 -      (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
   4.165 -       TextIO.output (toParent,childCmd^"\n" );
   4.166 -       TextIO.flushOut toParent;
   4.167 -       TextIO.output (vamp_proof_file, thisLine);
   4.168 -       TextIO.closeOut vamp_proof_file;
   4.169 -
   4.170 -       TextIO.output (toParent, thisLine^"\n");
   4.171 -       TextIO.output (toParent, thmstring^"\n");
   4.172 -       TextIO.output (toParent, goalstring^"\n");
   4.173 -       TextIO.flushOut toParent;
   4.174 -       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.175 -       (* Attempt to prevent several signals from turning up simultaneously *)
   4.176 -       Posix.Process.sleep(Time.fromSeconds 1);
   4.177 -       true)
   4.178 +	TextIO.output (proof_file, thisLine);
   4.179 +	TextIO.closeOut proof_file;
   4.180 + 
   4.181 +	TextIO.output (toParent, thisLine^"\n");
   4.182 +	TextIO.output (toParent, thmstring^"\n");
   4.183 +	TextIO.output (toParent, goalstring^"\n");
   4.184 +	TextIO.flushOut toParent;
   4.185 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.186 +	(* Attempt to prevent several signals from turning up simultaneously *)
   4.187 +	Posix.Process.sleep(Time.fromSeconds 1);
   4.188 +	true)
   4.189       else
   4.190 -       (TextIO.output (vamp_proof_file, thisLine);
   4.191 -	TextIO.flushOut vamp_proof_file;
   4.192 +       (TextIO.output (proof_file, thisLine);
   4.193 +	TextIO.flushOut proof_file;
   4.194  	checkVampProofFound  (fromChild, toParent, ppid, thmstring,
   4.195  	   goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses))
   4.196    end
   4.197  
   4.198  
   4.199 +fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd,
   4.200 +                      thm, sg_num, clause_arr, num_of_clauses) = 
   4.201 + let val E_proof_file = TextIO.openAppend
   4.202 +	   (File.platform_path(File.tmp_path (Path.basic "eprover_proof")))
   4.203 +     val _ = File.write (File.tmp_path (Path.basic "eprover_checking_prf"))
   4.204 +			("checking if proof found, thm is: " ^ string_of_thm thm)
   4.205 +     val thisLine = TextIO.inputLine fromChild  
   4.206 + in   
   4.207 +     if thisLine = "" 
   4.208 +     then (TextIO.output (E_proof_file, ("No proof output seen \n"));
   4.209 +	    TextIO.closeOut E_proof_file;
   4.210 +	    false)
   4.211 +     else if thisLine = "# TSTP exit status: Unsatisfiable\n"
   4.212 +     then      
   4.213 +       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
   4.214 +       startTransfer (Recon_Parse.start_E, Recon_Parse.end_E)
   4.215 +             (fromChild, toParent, ppid, thmstring, goalstring,
   4.216 +	      childCmd, thm, sg_num, clause_arr, num_of_clauses))
   4.217 +     else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n"
   4.218 +     then  
   4.219 +       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
   4.220 +	TextIO.output (toParent,childCmd^"\n" );
   4.221 +	TextIO.flushOut toParent;
   4.222 +	TextIO.output (E_proof_file, thisLine);
   4.223 +	TextIO.closeOut E_proof_file;
   4.224 +
   4.225 +	TextIO.output (toParent, thisLine^"\n");
   4.226 +	TextIO.output (toParent, thmstring^"\n");
   4.227 +	TextIO.output (toParent, goalstring^"\n");
   4.228 +	TextIO.flushOut toParent;
   4.229 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.230 +	(* Attempt to prevent several signals from turning up simultaneously *)
   4.231 +	Posix.Process.sleep(Time.fromSeconds 1);
   4.232 +	 true)
   4.233 +     else if thisLine = "# Failure: Resource limit exceeded (time)\n" 
   4.234 +     then  
   4.235 +       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
   4.236 +	TextIO.output (toParent, thisLine^"\n");
   4.237 +	TextIO.output (toParent, thmstring^"\n");
   4.238 +	TextIO.output (toParent, goalstring^"\n");
   4.239 +	TextIO.flushOut toParent;
   4.240 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.241 +	TextIO.output (E_proof_file, "signalled parent\n");
   4.242 +	TextIO.closeOut E_proof_file;
   4.243 +	(* Attempt to prevent several signals from turning up simultaneously *)
   4.244 +	Posix.Process.sleep(Time.fromSeconds 1);
   4.245 +	true)
   4.246 +     else if thisLine = "# Failure: Resource limit exceeded (memory)\n"
   4.247 +     then
   4.248 +	(Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.249 +	 TextIO.output (toParent,childCmd^"\n" );
   4.250 +	 TextIO.flushOut toParent;
   4.251 +	 TextIO.output (toParent, thisLine);
   4.252 +	 TextIO.flushOut toParent;
   4.253 +	 true)
   4.254 +     else
   4.255 +	(TextIO.output (E_proof_file, thisLine);
   4.256 +	TextIO.flushOut E_proof_file;
   4.257 +	checkEProofFound  (fromChild, toParent, ppid, thmstring,goalstring,
   4.258 +	childCmd, thm, sg_num, clause_arr, num_of_clauses))
   4.259 + end
   4.260 +
   4.261 +
   4.262  (***********************************************************************)
   4.263  (*  Function used by the Isabelle process to read in a Vampire proof   *)
   4.264  (***********************************************************************)
   4.265  
   4.266  fun getVampInput instr =
   4.267      let val thisLine = TextIO.inputLine instr
   4.268 -	val _ = File.write (File.tmp_path (Path.basic "vampire_line")) thisLine
   4.269 +	val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
   4.270      in    (* reconstructed proof string *)
   4.271        if thisLine = "" then ("No output from reconstruction process.\n","","")
   4.272        else if String.sub (thisLine, 0) = #"[" orelse
   4.273 @@ -166,4 +215,79 @@
   4.274        else getVampInput instr
   4.275      end
   4.276  
   4.277 +
   4.278 +(*FIXME!!: The following code is a mess. It mostly refers to SPASS-specific things*)
   4.279 +
   4.280 +(***********************************************************************)
   4.281 +(*  Function used by the Isabelle process to read in an E proof   *)
   4.282 +(***********************************************************************)
   4.283 +
   4.284 +fun getEInput instr = 
   4.285 +    let val thisLine = TextIO.inputLine instr 
   4.286 +        val _ = File.write (File.tmp_path (Path.basic "eprover_line")) thisLine
   4.287 +    in 
   4.288 +      if thisLine = "" then ("No output from reconstruction process.\n","","")
   4.289 +      else if String.sub (thisLine, 0) = #"["
   4.290 +      then 
   4.291 +	let val reconstr = thisLine
   4.292 +	    val thmstring = TextIO.inputLine instr 
   4.293 +	    val goalstring = TextIO.inputLine instr   
   4.294 +	in
   4.295 +	    (reconstr, thmstring, goalstring)
   4.296 +	end
   4.297 +      else if String.isPrefix "SPASS beiseite:" thisLine (*FIXME: wrong!!*)
   4.298 +      then 
   4.299 +	 let val reconstr = thisLine
   4.300 +	     val thmstring = TextIO.inputLine instr
   4.301 +	     val goalstring = TextIO.inputLine instr
   4.302 +	 in
   4.303 +	     (reconstr, thmstring, goalstring)
   4.304 +	 end
   4.305 +
   4.306 +       else if String.isPrefix "# No proof" thisLine 
   4.307 +      then 
   4.308 +	 let val reconstr = thisLine
   4.309 +	     val thmstring = TextIO.inputLine instr
   4.310 +	     val goalstring = TextIO.inputLine instr
   4.311 +	 in
   4.312 +	     (reconstr, thmstring, goalstring)
   4.313 +	 end
   4.314 +
   4.315 +       else if String.isPrefix "# Failure" thisLine 
   4.316 +      then 
   4.317 +	 let val reconstr = thisLine
   4.318 +	     val thmstring = TextIO.inputLine instr
   4.319 +	     val goalstring = TextIO.inputLine instr
   4.320 +	 in
   4.321 +	     (reconstr, thmstring, goalstring)
   4.322 +	 end
   4.323 +      else if String.isPrefix  "Rules from"  thisLine
   4.324 +      then 
   4.325 +	   let val reconstr = thisLine
   4.326 +	       val thmstring = TextIO.inputLine instr
   4.327 +	       val goalstring = TextIO.inputLine instr
   4.328 +	   in
   4.329 +	       (reconstr, thmstring, goalstring)
   4.330 +	   end
   4.331 +      else if substring (thisLine, 0,5) = "Proof"
   4.332 +      then
   4.333 +	let val reconstr = thisLine
   4.334 +	    val thmstring = TextIO.inputLine instr
   4.335 +	    val goalstring = TextIO.inputLine instr
   4.336 +	in
   4.337 +          File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine;
   4.338 +          (reconstr, thmstring, goalstring)
   4.339 +        end
   4.340 +      else if substring (thisLine, 0,1) = "%"
   4.341 +      then
   4.342 +	let val reconstr = thisLine
   4.343 +	    val thmstring = TextIO.inputLine instr
   4.344 +	    val goalstring = TextIO.inputLine instr
   4.345 +	in
   4.346 +           File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine;
   4.347 +	   (reconstr, thmstring, goalstring)
   4.348 +	end
   4.349 +      else getEInput instr
   4.350 +     end
   4.351 +
   4.352  end;
     5.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Thu Sep 08 16:09:23 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Thu Sep 08 17:35:02 2005 +0200
     5.3 @@ -3,7 +3,6 @@
     5.4      Copyright   2004  University of Cambridge
     5.5  *)
     5.6  
     5.7 -(*use "Translate_Proof";*)
     5.8  (* Parsing functions *)
     5.9  
    5.10  (* Auxiliary functions *)
    5.11 @@ -115,6 +114,12 @@
    5.12            raise (GandalfError "Couldn't find a proof.")
    5.13  *)
    5.14  
    5.15 +val start_E = "# Proof object starts here."
    5.16 +val end_E   = "# Proof object ends here."
    5.17 +val start_V6 = "%================== Proof: ======================"
    5.18 +val end_V6   = "%==============  End of proof. =================="
    5.19 +
    5.20 +
    5.21  (*Identifies the start/end lines of an ATP's output*)
    5.22  fun extract_proof s =
    5.23    if cut_exists "Here is a proof with" s then
    5.24 @@ -122,14 +127,14 @@
    5.25       o snd o cut_after ":"
    5.26       o snd o cut_after "Here is a proof with"
    5.27       o fst o cut_after " ||  -> .") s
    5.28 -  else if cut_exists "%================== Proof: ======================" s then
    5.29 -    (kill_lines 0    (*Vampire 5.0*)
    5.30 -     o snd o cut_after "%================== Proof: ======================"
    5.31 -     o fst o cut_before "==============  End of proof. ==================") s
    5.32 -  else if cut_exists "# Proof object ends here." s then
    5.33 +  else if cut_exists start_V6 s then
    5.34 +    (kill_lines 0    (*Vampire 6.0*)
    5.35 +     o snd o cut_after start_V6
    5.36 +     o fst o cut_before end_V6) s
    5.37 +  else if cut_exists end_E s then
    5.38      (kill_lines 0    (*eproof*)
    5.39 -     o snd o cut_after "# Proof object starts here."
    5.40 -     o fst o cut_before "# Proof object ends here.") s
    5.41 +     o snd o cut_after start_E
    5.42 +     o fst o cut_before end_E) s
    5.43    else "??extract_proof failed" (*Couldn't find a proof*)
    5.44  
    5.45  fun several p = many (some p)
     6.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 08 16:09:23 2005 +0200
     6.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 08 17:35:02 2005 +0200
     6.3 @@ -137,13 +137,7 @@
     6.4  fun thmstrings [] str = str
     6.5  |   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
     6.6  
     6.7 -fun is_clasimp_ax clasimp_num n = n <=clasimp_num 
     6.8 -
     6.9 -
    6.10 -
    6.11 -fun retrieve_axioms clause_arr  [] = []
    6.12 -|   retrieve_axioms clause_arr  (x::xs) =  [Array.sub(clause_arr, x)]@
    6.13 - 						     (retrieve_axioms clause_arr  xs)
    6.14 +fun is_clasimp_ax clasimp_num n = n <= clasimp_num 
    6.15  
    6.16  fun subone x = x - 1
    6.17  
    6.18 @@ -160,7 +154,7 @@
    6.19  	val _ = TextIO.output(axnums,(numstr clasimp_nums))
    6.20  	val _ = TextIO.closeOut(axnums)*)
    6.21      in
    6.22 -	retrieve_axioms clause_arr clasimp_nums
    6.23 +	map (fn x =>  Array.sub(clause_arr, x)) clasimp_nums
    6.24      end
    6.25  
    6.26  
    6.27 @@ -187,9 +181,18 @@
    6.28        clasimp_names
    6.29     end
    6.30     
    6.31 - fun get_axiom_names_spass proof_steps thms clause_arr num_of_clauses  =
    6.32 -   get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) 
    6.33 -                       thms clause_arr num_of_clauses;
    6.34 +
    6.35 +fun get_axiom_names_spass proofstr thms clause_arr num_of_clauses =
    6.36 +  let (* parse spass proof into datatype *)
    6.37 +      val tokens = #1(lex proofstr)
    6.38 +      val proof_steps = parse tokens
    6.39 +      val _ = File.write (File.tmp_path (Path.basic "parsing_done")) 
    6.40 +                         ("Did parsing on "^proofstr)
    6.41 +      (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
    6.42 +  in
    6.43 +    get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) 
    6.44 +                    thms clause_arr num_of_clauses
    6.45 +  end;
    6.46      
    6.47   fun get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses  =
    6.48     get_axiom_names (get_linenums proofstr) thms clause_arr num_of_clauses;
    6.49 @@ -207,49 +210,49 @@
    6.50  
    6.51  fun addvars c (a,b)  = (a,b,c)
    6.52  
    6.53 - fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    6.54 -     let 
    6.55 -	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    6.56 -	val axioms = (List.filter is_axiom) proof_steps
    6.57 -	val step_nums = get_step_nums axioms []
    6.58 +fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    6.59 +  let 
    6.60 +     val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    6.61 +     val axioms = (List.filter is_axiom) proof_steps
    6.62 +     val step_nums = get_step_nums axioms []
    6.63  
    6.64 -	val clauses =(*(clasimp_cls)@*)( make_clauses thms)
    6.65 -	
    6.66 -	val vars = map thm_vars clauses
    6.67 -       
    6.68 -	val distvars = distinct (fold append vars [])
    6.69 -	val clause_terms = map prop_of clauses  
    6.70 -	val clause_frees = List.concat (map term_frees clause_terms)
    6.71 +     val clauses =(*(clasimp_cls)@*)( make_clauses thms)
    6.72 +     
    6.73 +     val vars = map thm_vars clauses
    6.74 +    
    6.75 +     val distvars = distinct (fold append vars [])
    6.76 +     val clause_terms = map prop_of clauses  
    6.77 +     val clause_frees = List.concat (map term_frees clause_terms)
    6.78  
    6.79 -	val frees = map lit_string_with_nums clause_frees;
    6.80 +     val frees = map lit_string_with_nums clause_frees;
    6.81  
    6.82 -	val distfrees = distinct frees
    6.83 +     val distfrees = distinct frees
    6.84  
    6.85 -	val metas = map Meson.make_meta_clause clauses
    6.86 -	val ax_strs = map #3 axioms
    6.87 +     val metas = map Meson.make_meta_clause clauses
    6.88 +     val ax_strs = map #3 axioms
    6.89  
    6.90 -	(* literals of -all- axioms, not just those used by spass *)
    6.91 -	val meta_strs = map ReconOrderClauses.get_meta_lits metas
    6.92 -       
    6.93 -	val metas_and_strs = ListPair.zip (metas,meta_strs)
    6.94 -	val _ = File.write(File.tmp_path (Path.basic "foo_clauses")) (onestr ax_strs)
    6.95 -	val _ = File.write(File.tmp_path (Path.basic "foo_metastrs")) (onestr meta_strs)
    6.96 +     (* literals of -all- axioms, not just those used by spass *)
    6.97 +     val meta_strs = map ReconOrderClauses.get_meta_lits metas
    6.98 +    
    6.99 +     val metas_and_strs = ListPair.zip (metas,meta_strs)
   6.100 +     val _ = File.write(File.tmp_path (Path.basic "foo_clauses")) (onestr ax_strs)
   6.101 +     val _ = File.write(File.tmp_path (Path.basic "foo_metastrs")) (onestr meta_strs)
   6.102  
   6.103 -	(* get list of axioms as thms with their variables *)
   6.104 +     (* get list of axioms as thms with their variables *)
   6.105  
   6.106 -	val ax_metas = get_assoc_snds ax_strs metas_and_strs []
   6.107 -	val ax_vars = map thm_vars ax_metas
   6.108 -	val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
   6.109 +     val ax_metas = get_assoc_snds ax_strs metas_and_strs []
   6.110 +     val ax_vars = map thm_vars ax_metas
   6.111 +     val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
   6.112  
   6.113 -	(* get list of extra axioms as thms with their variables *)
   6.114 -	val extra_metas = add_if_not_inlist metas ax_metas []
   6.115 -	val extra_vars = map thm_vars extra_metas
   6.116 -	val extra_with_vars = if (not (extra_metas = []) ) 
   6.117 -			      then ListPair.zip (extra_metas,extra_vars)
   6.118 -			      else []
   6.119 -     in
   6.120 -	(distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
   6.121 -     end;
   6.122 +     (* get list of extra axioms as thms with their variables *)
   6.123 +     val extra_metas = add_if_not_inlist metas ax_metas []
   6.124 +     val extra_vars = map thm_vars extra_metas
   6.125 +     val extra_with_vars = if (not (extra_metas = []) ) 
   6.126 +			   then ListPair.zip (extra_metas,extra_vars)
   6.127 +			   else []
   6.128 +  in
   6.129 +     (distfrees,distvars, extra_with_vars,ax_with_vars, ListPair.zip (step_nums,ax_metas))
   6.130 +  end;
   6.131                                              
   6.132  
   6.133  (*********************************************************************)
   6.134 @@ -257,122 +260,24 @@
   6.135  (* Get out reconstruction steps as a string to be sent to Isabelle   *)
   6.136  (*********************************************************************)
   6.137  
   6.138 -
   6.139  fun rules_to_string [] = "NONE"
   6.140    | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
   6.141 -                                  
   6.142 -
   6.143 -(*val  proofstr = "1242[0:Inp] ||  -> equal(const_List_Orev(tconst_fun(tconst_List_Olist(U),tconst_List_Olist(U)),const_List_Olist_ONil),const_List_Olist_ONil)**.\
   6.144 -\1279[0:Inp] ||  -> equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(U),tconst_nat),const_List_Olist_ONil),const_0)**.\
   6.145 -\1430[0:Inp] || equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Orev(tconst_fun(tconst_List_Olist(typ__Ha),tconst_List_Olist(typ__Ha)),const_List_Olist_ONil)),const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Olist_ONil))** -> .\
   6.146 -\1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\
   6.147 -\1454[0:Obv:1453.0] ||  -> .";*)
   6.148  
   6.149  fun subst_for a b = String.translate (fn c => str (if c=a then b else c));
   6.150  
   6.151  val remove_linebreaks = subst_for #"\n" #"\t";
   6.152  val restore_linebreaks = subst_for #"\t" #"\n";
   6.153  
   6.154 -fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   6.155 -  let val _ = File.append(File.tmp_path (Path.basic"thmstringfile"))
   6.156 -                  ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n  num of clauses is: "^(string_of_int num_of_clauses))
   6.157 -
   6.158 -     (***********************************)
   6.159 -     (* parse spass proof into datatype *)
   6.160 -     (***********************************)
   6.161 -      val tokens = #1(lex proofstr)
   6.162 -      val proof_steps = parse tokens
   6.163 -      val _ = File.write (File.tmp_path (Path.basic "parsing_done")) 
   6.164 -                         ("Did parsing on "^proofstr)
   6.165 -      val _ = File.write(File.tmp_path (Path.basic "parsing_thmstring"))
   6.166 -                        ("Parsing for thmstring: "^thmstring)
   6.167 -      (************************************)
   6.168 -      (* recreate original subgoal as thm *)
   6.169 -      (************************************)
   6.170 -    
   6.171 -      (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   6.172 -      (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   6.173 -      (* subgoal this is, and turn it into meta_clauses *)
   6.174 -      (* should prob add array and table here, so that we can get axioms*)
   6.175 -      (* produced from the clasimpset rather than the problem *)
   6.176 -
   6.177 -      val axiom_names = get_axiom_names_spass proof_steps thms clause_arr num_of_clauses
   6.178 -      val ax_str = "Rules from clasimpset used in proof found by SPASS: " ^ 
   6.179 -                   rules_to_string axiom_names 
   6.180 -      val _ = File.append(File.tmp_path (Path.basic "reconstrfile"))
   6.181 -                         ("reconstring is: "^ax_str^"  "^goalstring)       
   6.182 -  in 
   6.183 -       TextIO.output (toParent, ax_str^"\n");
   6.184 -       TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   6.185 -       TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   6.186 -       TextIO.flushOut toParent;
   6.187 -
   6.188 -       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   6.189 -      (* Attempt to prevent several signals from turning up simultaneously *)
   6.190 -       Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   6.191 -  end
   6.192 -  handle _ => 
   6.193 -  let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   6.194 -  in 
   6.195 -     TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" );
   6.196 -       TextIO.output (toParent, (remove_linebreaks thmstring)^"\n");
   6.197 -       TextIO.output (toParent, ( (remove_linebreaks goalstring)^"\n"));
   6.198 -       TextIO.flushOut toParent;
   6.199 -      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   6.200 -      (* Attempt to prevent several signals from turning up simultaneously *)
   6.201 -      Posix.Process.sleep(Time.fromSeconds 1); all_tac
   6.202 -  end
   6.203  
   6.204 -
   6.205 -fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   6.206 +fun proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses getax = 
   6.207   let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
   6.208 -               (" thmstring is: "^thmstring^"proofstr is: "^proofstr^
   6.209 -                "goalstr is: "^goalstring^" num of clauses is: "^
   6.210 -                (string_of_int num_of_clauses))
   6.211 -
   6.212 -    (***********************************)
   6.213 -    (* get vampire axiom names         *)
   6.214 -    (***********************************)
   6.215 -
   6.216 -     val axiom_names = get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses
   6.217 -     val ax_str = "Rules from clasimpset used in proof found by Vampire: " ^
   6.218 -                  rules_to_string axiom_names
   6.219 -    in 
   6.220 -	 File.append(File.tmp_path (Path.basic "reconstrfile")) 
   6.221 -	            ("reconstring is: "^ax_str^"  "^goalstring);
   6.222 -         TextIO.output (toParent, ax_str^"\n");
   6.223 -	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   6.224 -	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   6.225 -	 TextIO.flushOut toParent;
   6.226 +               ("thmstring is " ^ thmstring ^ 
   6.227 +                "\nproofstr is " ^ proofstr ^
   6.228 +                "\ngoalstr is " ^ goalstring ^
   6.229 +                "\nnum of clauses is " ^ string_of_int num_of_clauses)
   6.230  
   6.231 -	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   6.232 -	(* Attempt to prevent several signals from turning up simultaneously *)
   6.233 -	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   6.234 -    end
   6.235 -    handle _ => 
   6.236 -    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   6.237 -    in 
   6.238 -	TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   6.239 -	 TextIO.output (toParent, thmstring^"\n");
   6.240 -	 TextIO.output (toParent, goalstring^"\n");
   6.241 -	 TextIO.flushOut toParent;
   6.242 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   6.243 -	Posix.Process.sleep(Time.fromSeconds 1); all_tac
   6.244 -    end;
   6.245 -
   6.246 -
   6.247 -fun EString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   6.248 - let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
   6.249 -               (" thmstring is: "^thmstring^"proofstr is: "^proofstr^
   6.250 -                "goalstr is: "^goalstring^" num of clauses is: "^
   6.251 -                (string_of_int num_of_clauses))
   6.252 -
   6.253 -    (***********************************)
   6.254 -    (* get E axiom names         *)
   6.255 -    (***********************************)
   6.256 -
   6.257 -     val axiom_names = get_axiom_names_vamp_E proofstr  thms clause_arr  num_of_clauses
   6.258 -     val ax_str = "Rules from clasimpset used in proof found by E: " ^
   6.259 +     val axiom_names = getax proofstr thms clause_arr num_of_clauses
   6.260 +     val ax_str = "Rules from clasimpset used in automatic proof: " ^
   6.261                    rules_to_string axiom_names
   6.262      in 
   6.263  	 File.append(File.tmp_path (Path.basic "reconstrfile"))
   6.264 @@ -386,18 +291,29 @@
   6.265  	(* Attempt to prevent several signals from turning up simultaneously *)
   6.266  	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   6.267      end
   6.268 -    handle _ => 
   6.269 -    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   6.270 -    in 
   6.271 -	TextIO.output (toParent,"Proof found by E but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   6.272 -	 TextIO.output (toParent, thmstring^"\n");
   6.273 -	 TextIO.output (toParent, goalstring^"\n");
   6.274 -	 TextIO.flushOut toParent;
   6.275 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   6.276 -	(* Attempt to prevent several signals from turning up simultaneously *)
   6.277 -	Posix.Process.sleep(Time.fromSeconds 1); all_tac
   6.278 -    end;
   6.279 +    handle _ => (*FIXME: exn handler is too general!*)
   6.280 +     (File.write(File.tmp_path (Path.basic "proverString_handler")) "In exception handler";
   6.281 +      TextIO.output (toParent, "Proof found but translation failed : " ^ 
   6.282 +                     remove_linebreaks proofstr ^ "\n");
   6.283 +      TextIO.output (toParent, remove_linebreaks thmstring ^ "\n");
   6.284 +      TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
   6.285 +      TextIO.flushOut toParent;
   6.286 +      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   6.287 +      (* Attempt to prevent several signals from turning up simultaneously *)
   6.288 +      Posix.Process.sleep(Time.fromSeconds 1); all_tac);
   6.289  
   6.290 +fun proverString_to_lemmaString proofstr thmstring goalstring toParent ppid thms
   6.291 +      clause_arr num_of_clauses  = 
   6.292 +  proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms        
   6.293 +       clause_arr num_of_clauses get_axiom_names_vamp_E;
   6.294 +
   6.295 +fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms
   6.296 +      clause_arr  num_of_clauses  = 
   6.297 +  proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms        
   6.298 +       clause_arr num_of_clauses get_axiom_names_spass;
   6.299 +
   6.300 +
   6.301 +(**** Full proof reconstruction for SPASS (not really working) ****)
   6.302  
   6.303  fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   6.304    let val _ = File.write(File.tmp_path (Path.basic "thmstringfile")) 
   6.305 @@ -792,29 +708,15 @@
   6.306  (* be passed over to the watcher, e.g.  numcls25       *)
   6.307  (*******************************************************)
   6.308  
   6.309 -(* val str = "[S%x%P%R%Q%]1ExtraAxiom()[~ Q U%~ R U%][U%]2ExtraAxiom()[~ Q U%~ P U%][U%]3ExtraAxiom()[Q U%R U%][U%]1OrigAxiom()[S x%][]2OrigAxiom()[P U%R U%][U%]6OrigAxiom()[~ S U%~ P U%][U%]7OrigAxiom()[~ S U%~ R U%][U%]1Axiom()[S x%][]2Axiom()[R U%P U%][U%]6Axiom()[~ P U%~ S U%][U%]7Axiom()[~ R U%~ S U%][U%]8Binary((6,1),(1,0))[~ P x%][]9Binary((7,1),(1,0))[~ R x%][]19Binary((9,0),(2,0))[P x%][]25Binary((8,0),(19,0))[][]";
   6.310 -
   6.311 -val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
   6.312 -
   6.313 -val reconstr = "[P%Q%x%xa%]1OrigAxiom()[~ P U%][U%]3OrigAxiom()[Q U%][U%]5OrigAxiom()[P (x U)%~ Q (xa U)%][U%]9Binary((7,0),(3,0))[][]7Binary((1,0),(5,0))[~ Q (xa U)%][U%]5Axiom()[P (x U)%~ Q (xa U)%][U%]3Axiom()[Q U%][U%]1Axiom()[~ P U%][U%](ALL xb::'a::type.   (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) |    (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) &   P xb & ~ Q xb)";
   6.314 -
   6.315 -
   6.316 -val reconstr = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
   6.317 -
   6.318 -val thmstring = " (ALL xa::'a::type.   (~ (P::'a::type => bool) (x::'a::type) | P xa) & (~ P xa | P x)) & (((P::'a::type => bool) (xa::'a::type) | (ALL x::'a::type. P x)) &((ALL x::'a::type. ~ P x) | ~ P (xb::'a::type)))";
   6.319 -*)
   6.320 +fun apply_res_thm str goalstring  = 
   6.321 +  let val tokens = #1 (lex str);
   6.322 +      val _ = File.append (File.tmp_path (Path.basic "apply_res_1")) 
   6.323 +	 ("str is: "^str^" goalstr is: "^goalstring^"\n")	
   6.324 +      val (frees,recon_steps) = parse_step tokens 
   6.325 +      val isar_str = to_isar_proof (frees, recon_steps, goalstring)
   6.326 +      val foo = File.write (File.tmp_path (Path.basic "apply_res_2")) isar_str
   6.327 +  in 
   6.328 +     Pretty.writeln(Pretty.str isar_str)
   6.329 +  end 
   6.330  
   6.331 -fun apply_res_thm str goalstring  = let val tokens = #1 (lex str);
   6.332 -				val _ = File.append (File.tmp_path (Path.basic "applyres")) 
   6.333 -			           ("str is: "^str^" goalstr is: "^goalstring^"\n")	
   6.334 -                                   val (frees,recon_steps) = parse_step tokens 
   6.335 -                                   val isar_str = to_isar_proof (frees, recon_steps, goalstring)
   6.336 -                                   val foo =   TextIO.openOut (File.platform_path(File.tmp_path (Path.basic "foobar")));
   6.337 -                               in 
   6.338 -                                  TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str  isar_str); () 
   6.339 -                               end 
   6.340 -
   6.341 -
   6.342 -(* val reconstr = reconstr^"[P%]51Axiom()[~P%]52Axiom[P%][]53MRR((52,0),(51,0))[][]";
   6.343 -*)
   6.344  end;
     7.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Sep 08 16:09:23 2005 +0200
     7.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Sep 08 17:35:02 2005 +0200
     7.3 @@ -434,7 +434,7 @@
     7.4  			      prems_string^prover^thmstring^goalstring^childCmd) 
     7.5  		       val childDone = (case prover of
     7.6  			   "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  
     7.7 -			    | "E" => EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
     7.8 +			    | "E" => VampComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
     7.9  			  |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  )
    7.10  		    in
    7.11  		     if childDone      (**********************************************)