Progress on eprover linkup, also massive tidying
authorpaulson
Wed Sep 07 18:14:26 2005 +0200 (2005-09-07)
changeset 173065cde710a8a23
parent 17305 6cef3aedd661
child 17307 a6d206750d6d
Progress on eprover linkup, also massive tidying
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
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/ECommunication.ML	Wed Sep 07 09:54:31 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/ECommunication.ML	Wed Sep 07 18:14:26 2005 +0200
     1.3 @@ -21,16 +21,7 @@
     1.4  
     1.5  val E = ref false;
     1.6  
     1.7 -(***********************************)
     1.8 -(*  Write E   output to a file *)
     1.9 -(***********************************)
    1.10 -
    1.11 -fun logEInput (instr, fd) = 
    1.12 -  let val thisLine = TextIO.inputLine instr 
    1.13 -  in if thisLine = "# Proof object ends here.\n" 
    1.14 -     then TextIO.output (fd, thisLine)
    1.15 -     else (TextIO.output (fd, thisLine); logEInput (instr,fd))
    1.16 -  end;
    1.17 +exception EOF;
    1.18  
    1.19  (**********************************************************************)
    1.20  (*  Reconstruct the E proof w.r.t. thmstring (string version of   *)
    1.21 @@ -47,153 +38,134 @@
    1.22                toParent ppid negs clause_arr  num_of_clauses ))]) sg_num	
    1.23  
    1.24  
    1.25 -fun transferEInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr,  num_of_clauses) = 
    1.26 -  let val thisLine = TextIO.inputLine fromChild 
    1.27 -  in 
    1.28 -     if thisLine = "# Proof object ends here.\n"
    1.29 -     then 
    1.30 -       let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    1.31 -       in 
    1.32 -	   File.write (File.tmp_path (Path.basic"extracted-prf-E")) proofextract;
    1.33 -	   reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
    1.34 -	       clause_arr num_of_clauses thm
    1.35 -       end
    1.36 -     else transferEInput (fromChild, toParent, ppid,thmstring, goalstring,
    1.37 -                              (currentString^thisLine), thm, sg_num, clause_arr,  
    1.38 -                              num_of_clauses)
    1.39 -  end;
    1.40 +fun transferEInput (fromChild, toParent, ppid,thmstring,goalstring, 
    1.41 +                    currentString, thm, sg_num,clause_arr, num_of_clauses) = 
    1.42 + let val thisLine = TextIO.inputLine fromChild 
    1.43 + in 
    1.44 +     File.append (File.tmp_path (Path.basic "eprover_transfer"))
    1.45 +		      ("transferEInput input line: " ^ thisLine);        
    1.46 +    if thisLine = "" (*end of file?*)
    1.47 +    then (File.write (File.tmp_path (Path.basic"eprover_extraction_failed")) currentString;
    1.48 +	  raise EOF)                    
    1.49 +    else if thisLine = "# Proof object ends here.\n"
    1.50 +    then 
    1.51 +      let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    1.52 +      in 
    1.53 +	  File.write (File.tmp_path (Path.basic"eprover_extracted_prf")) proofextract;
    1.54 +	  reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
    1.55 +	      clause_arr num_of_clauses thm
    1.56 +      end
    1.57 +    else transferEInput (fromChild, toParent, ppid,thmstring, goalstring,
    1.58 +			     (currentString^thisLine), thm, sg_num, clause_arr, 
    1.59 +			     num_of_clauses)
    1.60 + end;
    1.61  
    1.62  
    1.63  (*********************************************************************************)
    1.64 -(*  Inspect the output of an E process to see if it has found a proof,      *)
    1.65 +(*  Inspect the output of an E process to see if it has found a proof,     *)
    1.66  (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    1.67  (*********************************************************************************)
    1.68  
    1.69   
    1.70  fun startETransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
    1.71                      thm, sg_num,clause_arr, num_of_clauses) = 
    1.72 -  if isSome (TextIO.canInput(fromChild, 5))
    1.73 -  then
    1.74      let val thisLine = TextIO.inputLine fromChild  
    1.75      in                 
    1.76 -      if String.isPrefix "# Proof object starts" thisLine 
    1.77 +      if thisLine = "" then false
    1.78 +      else if String.isPrefix "# Proof object starts" thisLine 
    1.79        then     
    1.80 -	 (File.append (File.tmp_path (Path.basic "transfer-E"))
    1.81 -		      ("about to transfer proof, thm is: " ^ string_of_thm thm);
    1.82 +	 (File.append (File.tmp_path (Path.basic "eprover_transfer"))
    1.83 +		      ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n");
    1.84  	  transferEInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, 
    1.85 -			      thm, sg_num,clause_arr,  num_of_clauses);
    1.86 -	  true)
    1.87 +			      thm, sg_num,clause_arr, num_of_clauses);
    1.88 +	  true) handle EOF => false
    1.89        else startETransfer (fromChild, toParent, ppid, thmstring, goalstring,
    1.90  			       childCmd, thm, sg_num,clause_arr, num_of_clauses)
    1.91       end
    1.92 -   else false
    1.93  
    1.94  
    1.95 -fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr,  num_of_clauses) = 
    1.96 -  let val E_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "E_proof")))
    1.97 -        val _ = File.write (File.tmp_path (Path.basic "checking-prf-E"))
    1.98 -                           ("checking if proof found, thm is: " ^ string_of_thm thm)
    1.99 -  in 
   1.100 -  if (isSome (TextIO.canInput(fromChild, 5)))
   1.101 -  then
   1.102 -  let val thisLine = TextIO.inputLine fromChild  
   1.103 -      in if (*thisLine = "# Problem is unsatisfiable (or provable), constructing proof object\n"*)
   1.104 -             thisLine = "# TSTP exit status: Unsatisfiable\n"
   1.105 -	 then      
   1.106 -	    let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   1.107 -		val _ = TextIO.output (outfile, thisLine)
   1.108 -	
   1.109 -		val _ = TextIO.closeOut outfile
   1.110 -	    in 
   1.111 -	       startETransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses) 
   1.112 -	    end
   1.113 -	 else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n"
   1.114 -	 then  
   1.115 -	    let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); 
   1.116 -		val _ = TextIO.output (outfile, thisLine)
   1.117 -		val _ =  TextIO.closeOut outfile
   1.118 -	    in
   1.119 -	      TextIO.output (toParent,childCmd^"\n" );
   1.120 -	      TextIO.flushOut toParent;
   1.121 -	      TextIO.output (E_proof_file, thisLine);
   1.122 -	      TextIO.flushOut E_proof_file;
   1.123 -	      TextIO.closeOut E_proof_file;
   1.124 -	      (*TextIO.output (toParent, thisLine);
   1.125 -	      TextIO.flushOut toParent;
   1.126 -	      TextIO.output (toParent, "bar\n");
   1.127 -	      TextIO.flushOut toParent;*)
   1.128 +fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd,
   1.129 +                      thm, sg_num, clause_arr, num_of_clauses) = 
   1.130 + let val E_proof_file = TextIO.openAppend
   1.131 +	   (File.platform_path(File.tmp_path (Path.basic "eprover_proof")))
   1.132 +     val _ = File.write (File.tmp_path (Path.basic "eprover_checking_prf"))
   1.133 +			("checking if proof found, thm is: " ^ string_of_thm thm)
   1.134 +     val thisLine = TextIO.inputLine fromChild  
   1.135 + in   
   1.136 +     if thisLine = "" 
   1.137 +     then (TextIO.output (E_proof_file, ("No proof output seen \n"));
   1.138 +	    TextIO.closeOut E_proof_file;
   1.139 +	    false)
   1.140 +     else if (*thisLine = "# Problem is unsatisfiable (or provable), constructing proof object\n"*)
   1.141 +	 thisLine = "# TSTP exit status: Unsatisfiable\n"
   1.142 +     then      
   1.143 +       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
   1.144 +	startETransfer (fromChild, toParent, ppid, thmstring,goalstring,
   1.145 +			childCmd, thm, sg_num, clause_arr, num_of_clauses))
   1.146 +     else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n"
   1.147 +     then  
   1.148 +       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
   1.149 +	TextIO.output (toParent,childCmd^"\n" );
   1.150 +	TextIO.flushOut toParent;
   1.151 +	TextIO.output (E_proof_file, thisLine);
   1.152 +	TextIO.closeOut E_proof_file;
   1.153  
   1.154 -	      TextIO.output (toParent, thisLine^"\n");
   1.155 -	      TextIO.flushOut toParent;
   1.156 -	      TextIO.output (toParent, thmstring^"\n");
   1.157 -	      TextIO.flushOut toParent;
   1.158 -	      TextIO.output (toParent, goalstring^"\n");
   1.159 -	      TextIO.flushOut toParent;
   1.160 -	      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.161 -	      (* Attempt to prevent several signals from turning up simultaneously *)
   1.162 -	      Posix.Process.sleep(Time.fromSeconds 1);
   1.163 -	       true  
   1.164 -	    end
   1.165 -	   else if thisLine = "# Failure: Resource limit exceeded (time)\n" 
   1.166 -	   then  
   1.167 -	     let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                          	(*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   1.168 -	     val _ = TextIO.output (outfile, thisLine)
   1.169 - 	     in TextIO.output (toParent, thisLine^"\n");
   1.170 -		TextIO.flushOut toParent;
   1.171 -		TextIO.output (toParent, thmstring^"\n");
   1.172 -		TextIO.flushOut toParent;
   1.173 -		TextIO.output (toParent, goalstring^"\n");
   1.174 -		TextIO.flushOut toParent;
   1.175 -		Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.176 -		TextIO.output (outfile, ("signalled parent\n"));TextIO.closeOut outfile;
   1.177 -	        (* Attempt to prevent several signals from turning up simultaneously *)
   1.178 -	        Posix.Process.sleep(Time.fromSeconds 1);
   1.179 -		true 
   1.180 -	     end
   1.181 -	  else if thisLine = "# Failure: Resource limit exceeded (memory)\n"                                                            		                 
   1.182 -	  then
   1.183 -             (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.184 -	      TextIO.output (toParent,childCmd^"\n" );
   1.185 -	      TextIO.flushOut toParent;
   1.186 -	      TextIO.output (toParent, thisLine);
   1.187 -	      TextIO.flushOut toParent;
   1.188 -	      true)
   1.189 -	  else
   1.190 -	     (TextIO.output (E_proof_file, thisLine);
   1.191 -	     TextIO.flushOut E_proof_file;
   1.192 -	     checkEProofFound  (fromChild, toParent, ppid, thmstring,goalstring,
   1.193 -	     childCmd, thm, sg_num, clause_arr,  num_of_clauses))
   1.194 -	 end
   1.195 -    else 
   1.196 -	(TextIO.output (E_proof_file, ("No proof output seen \n"));
   1.197 -	 TextIO.closeOut E_proof_file;
   1.198 -	 false)
   1.199 +	TextIO.output (toParent, thisLine^"\n");
   1.200 +	TextIO.output (toParent, thmstring^"\n");
   1.201 +	TextIO.output (toParent, goalstring^"\n");
   1.202 +	TextIO.flushOut toParent;
   1.203 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.204 +	(* Attempt to prevent several signals from turning up simultaneously *)
   1.205 +	Posix.Process.sleep(Time.fromSeconds 1);
   1.206 +	 true)
   1.207 +     else if thisLine = "# Failure: Resource limit exceeded (time)\n" 
   1.208 +     then  
   1.209 +       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
   1.210 +	TextIO.output (toParent, thisLine^"\n");
   1.211 +	TextIO.output (toParent, thmstring^"\n");
   1.212 +	TextIO.output (toParent, goalstring^"\n");
   1.213 +	TextIO.flushOut toParent;
   1.214 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.215 +	TextIO.output (E_proof_file, "signalled parent\n");
   1.216 +	TextIO.closeOut E_proof_file;
   1.217 +	(* Attempt to prevent several signals from turning up simultaneously *)
   1.218 +	Posix.Process.sleep(Time.fromSeconds 1);
   1.219 +	true)
   1.220 +     else if thisLine = "# Failure: Resource limit exceeded (memory)\n"                                                            		                 
   1.221 +     then
   1.222 +	(Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.223 +	 TextIO.output (toParent,childCmd^"\n" );
   1.224 +	 TextIO.flushOut toParent;
   1.225 +	 TextIO.output (toParent, thisLine);
   1.226 +	 TextIO.flushOut toParent;
   1.227 +	 true)
   1.228 +     else
   1.229 +	(TextIO.output (E_proof_file, thisLine);
   1.230 +	TextIO.flushOut E_proof_file;
   1.231 +	checkEProofFound  (fromChild, toParent, ppid, thmstring,goalstring,
   1.232 +	childCmd, thm, sg_num, clause_arr, num_of_clauses))
   1.233   end
   1.234  
   1.235  
   1.236    
   1.237  (***********************************************************************)
   1.238 -(*  Function used by the Isabelle process to read in a E proof   *)
   1.239 +(*  Function used by the Isabelle process to read in an E proof   *)
   1.240  (***********************************************************************)
   1.241  
   1.242  fun getEInput instr = 
   1.243 -  if isSome (TextIO.canInput(instr, 2))
   1.244 -  then
   1.245      let val thisLine = TextIO.inputLine instr 
   1.246 -	val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_thisLine")));
   1.247 -	val _ = TextIO.output (outfile, thisLine)
   1.248 -	val _ =  TextIO.closeOut outfile
   1.249 +        val _ = File.write (File.tmp_path (Path.basic "eprover_line")) thisLine
   1.250      in 
   1.251 -      if substring (thisLine, 0,1) = "["
   1.252 +      if thisLine = "" then ("No output from reconstruction process.\n","","")
   1.253 +      else if String.sub (thisLine, 0) = #"["
   1.254        then 
   1.255 -	(*Pretty.writeln(Pretty.str thisLine)*)
   1.256  	let val reconstr = thisLine
   1.257  	    val thmstring = TextIO.inputLine instr 
   1.258  	    val goalstring = TextIO.inputLine instr   
   1.259  	in
   1.260  	    (reconstr, thmstring, goalstring)
   1.261  	end
   1.262 -      else if String.isPrefix "SPASS beiseite:" thisLine 
   1.263 +      else if String.isPrefix "SPASS beiseite:" thisLine (*FIXME: wrong!!*)
   1.264        then 
   1.265  	 let val reconstr = thisLine
   1.266  	     val thmstring = TextIO.inputLine instr
   1.267 @@ -219,9 +191,6 @@
   1.268  	 in
   1.269  	     (reconstr, thmstring, goalstring)
   1.270  	 end
   1.271 -
   1.272 -
   1.273 -
   1.274        else if String.isPrefix  "Rules from"  thisLine
   1.275        then 
   1.276  	   let val reconstr = thisLine
   1.277 @@ -250,7 +219,4 @@
   1.278  	end
   1.279        else getEInput instr
   1.280       end
   1.281 -  else 
   1.282 -      ("No output from reconstruction process.\n","","")
   1.283 -
   1.284  end;
     2.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Wed Sep 07 09:54:31 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Wed Sep 07 18:14:26 2005 +0200
     2.3 @@ -11,27 +11,18 @@
     2.4    sig
     2.5      val reconstruct : bool ref
     2.6      val getSpassInput : TextIO.instream -> string * string * string
     2.7 -    val checkSpassProofFound:  TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
     2.8 -                               string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array  * int -> bool
     2.9 -    
    2.10 +    val checkSpassProofFound:  
    2.11 +          TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
    2.12 +          string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
    2.13    end;
    2.14  
    2.15  structure SpassComm : SPASS_COMM =
    2.16  struct
    2.17  
    2.18  (* switch for whether to reconstruct a proof found, or just list the lemmas used *)
    2.19 -val reconstruct = ref true;
    2.20 -
    2.21 -(***********************************)
    2.22 -(*  Write Spass   output to a file *)
    2.23 -(***********************************)
    2.24 +val reconstruct = ref false;
    2.25  
    2.26 -fun logSpassInput (instr, fd) = 
    2.27 -  let val thisLine = TextIO.inputLine instr 
    2.28 -  in if thisLine = "--------------------------SPASS-STOP------------------------------\n" 
    2.29 -     then TextIO.output (fd, thisLine)
    2.30 -     else (TextIO.output (fd, thisLine); logSpassInput (instr,fd))
    2.31 -  end;
    2.32 +exception EOF;
    2.33  
    2.34  (**********************************************************************)
    2.35  (*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
    2.36 @@ -40,148 +31,121 @@
    2.37  (**********************************************************************)
    2.38  
    2.39  fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
    2.40 -                    clause_arr  (num_of_clauses:int ) = 
    2.41 - (*FIXME: foo is never used!*)
    2.42 - let val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3")));
    2.43 - in
    2.44 +                    clause_arr num_of_clauses = 
    2.45 + let val f = if !reconstruct then Recon_Transfer.spassString_to_reconString
    2.46 +                             else Recon_Transfer.spassString_to_lemmaString
    2.47 + in                             
    2.48     SELECT_GOAL
    2.49      (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
    2.50               METAHYPS(fn negs => 
    2.51 -    (if !reconstruct 
    2.52 -     then Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring 
    2.53 -              toParent ppid negs clause_arr num_of_clauses 
    2.54 -     else Recon_Transfer.spassString_to_lemmaString proofextract thmstring goalstring 
    2.55 -              toParent ppid negs clause_arr  num_of_clauses ))]) sg_num	
    2.56 - end ;
    2.57 +    f proofextract thmstring goalstring 
    2.58 +              toParent ppid negs clause_arr num_of_clauses)]) sg_num	
    2.59 + end;
    2.60  
    2.61  
    2.62 -fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr,  num_of_clauses) = 
    2.63 -  let val thisLine = TextIO.inputLine fromChild 
    2.64 -  in 
    2.65 -     if thisLine = "--------------------------SPASS-STOP------------------------------\n"
    2.66 -     then 
    2.67 -       let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    2.68 -       in 
    2.69 -	   File.write (File.tmp_path (Path.basic"foobar2")) proofextract;
    2.70 -	   reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
    2.71 -	       clause_arr num_of_clauses thm
    2.72 -       end
    2.73 -     else transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,
    2.74 -                              (currentString^thisLine), thm, sg_num, clause_arr,  
    2.75 -                              num_of_clauses)
    2.76 -  end;
    2.77 +fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, 
    2.78 +                        currentString, thm, sg_num,clause_arr, num_of_clauses) = 
    2.79 + let val thisLine = TextIO.inputLine fromChild 
    2.80 + in 
    2.81 +    if thisLine = "" (*end of file?*)
    2.82 +    then (File.write (File.tmp_path (Path.basic"eprover_extraction_failed")) currentString;
    2.83 +	  raise EOF)                    
    2.84 +    else if thisLine = "--------------------------SPASS-STOP------------------------------\n"
    2.85 +    then 
    2.86 +      let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    2.87 +      in 
    2.88 +	  File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract;
    2.89 +	  reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
    2.90 +	      clause_arr num_of_clauses thm
    2.91 +      end
    2.92 +    else transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,
    2.93 +			     (currentString^thisLine), thm, sg_num, clause_arr, 
    2.94 +			     num_of_clauses)
    2.95 + end;
    2.96  
    2.97  
    2.98  (*********************************************************************************)
    2.99 -(*  Inspect the output of a Spass   process to see if it has found a proof,      *)
   2.100 +(*  Inspect the output of a Spass   process to see if it has found a proof,     *)
   2.101  (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   2.102  (*********************************************************************************)
   2.103  
   2.104   
   2.105 -fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = 
   2.106 -(*let val _ = Posix.Process.wait ()
   2.107 -in*)
   2.108 -                                       
   2.109 -   if (isSome (TextIO.canInput(fromChild, 5)))
   2.110 -   then
   2.111 +fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
   2.112 +                        thm, sg_num,clause_arr, num_of_clauses) = 
   2.113     let val thisLine = TextIO.inputLine fromChild  
   2.114     in                 
   2.115 -     if String.isPrefix "Here is a proof" thisLine then     
   2.116 -       let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_transfer")))
   2.117 -	   val _=  TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm))
   2.118 -	   val _ =  TextIO.closeOut outfile
   2.119 -       in
   2.120 - 	 transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, 
   2.121 - 	                     thm, sg_num,clause_arr,  num_of_clauses);
   2.122 - 	 true
   2.123 -       end     
   2.124 -     else startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,
   2.125 -                              childCmd, thm, sg_num,clause_arr, num_of_clauses)
   2.126 +      if thisLine = "" then false
   2.127 +      else if String.isPrefix "Here is a proof" thisLine then     
   2.128 +	 (File.append (File.tmp_path (Path.basic "spass_transfer"))
   2.129 +		      ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n");
   2.130 +	  transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, 
   2.131 + 	                     thm, sg_num,clause_arr, num_of_clauses);
   2.132 +	  true) handle EOF => false
   2.133 +      else startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,
   2.134 +                               childCmd, thm, sg_num,clause_arr, num_of_clauses)
   2.135      end
   2.136 -     else false
   2.137 - (*  end*)
   2.138 -
   2.139  
   2.140  
   2.141 -fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr,  (num_of_clauses:int )) = 
   2.142 -  let val spass_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "spass_proof")))
   2.143 -      val _ = File.write(File.tmp_path (Path.basic "foo_checkspass"))
   2.144 -                 ("checking if proof found, thm is: "^(string_of_thm thm))
   2.145 -  in 
   2.146 -  if (isSome (TextIO.canInput(fromChild, 5)))
   2.147 -  then
   2.148 -  let val thisLine = TextIO.inputLine fromChild  
   2.149 -      in if thisLine = "SPASS beiseite: Proof found.\n"
   2.150 -	 then      
   2.151 -	    let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   2.152 -		val _ = TextIO.output (outfile, thisLine)
   2.153 -	
   2.154 -		val _ = TextIO.closeOut outfile
   2.155 -	    in 
   2.156 -	       startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses) 
   2.157 -	    end
   2.158 -	 else if thisLine= "SPASS beiseite: Completion found.\n"
   2.159 -	 then  
   2.160 -	    let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   2.161 -		val _ = TextIO.output (outfile, thisLine)
   2.162 -
   2.163 -		val _ =  TextIO.closeOut outfile
   2.164 -	    in
   2.165 -	      TextIO.output (toParent,childCmd^"\n" );
   2.166 -	      TextIO.flushOut toParent;
   2.167 -	      TextIO.output (spass_proof_file, thisLine);
   2.168 -	      TextIO.flushOut spass_proof_file;
   2.169 -	      TextIO.closeOut spass_proof_file;
   2.170 -	      (*TextIO.output (toParent, thisLine);
   2.171 -	      TextIO.flushOut toParent;
   2.172 -	      TextIO.output (toParent, "bar\n");
   2.173 -	      TextIO.flushOut toParent;*)
   2.174 +fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd,
   2.175 +                          thm, sg_num, clause_arr, (num_of_clauses:int )) = 
   2.176 + let val spass_proof_file = TextIO.openAppend
   2.177 +           (File.platform_path(File.tmp_path (Path.basic "spass_proof")))
   2.178 +     val _ = File.write(File.tmp_path (Path.basic "spass_checking_prf"))
   2.179 +		("checking if proof found, thm is: "^(string_of_thm thm))
   2.180 +     val thisLine = TextIO.inputLine fromChild  
   2.181 + in    
   2.182 +     if thisLine = "" 
   2.183 +     then (TextIO.output (spass_proof_file, ("No proof output seen \n"));
   2.184 +	   TextIO.closeOut spass_proof_file;
   2.185 +	   false)
   2.186 +     else if thisLine = "SPASS beiseite: Proof found.\n"
   2.187 +     then      
   2.188 +       (File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
   2.189 +	startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,
   2.190 +	                    childCmd, thm, sg_num, clause_arr, num_of_clauses))
   2.191 +     else if thisLine = "SPASS beiseite: Completion found.\n"
   2.192 +     then  
   2.193 +       (File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
   2.194 +	TextIO.output (toParent,childCmd^"\n" );
   2.195 +	TextIO.flushOut toParent;
   2.196 +	TextIO.output (spass_proof_file, thisLine);
   2.197 +	TextIO.flushOut spass_proof_file;
   2.198 +	TextIO.closeOut spass_proof_file;
   2.199  
   2.200 -	      TextIO.output (toParent, thisLine^"\n");
   2.201 -	      TextIO.flushOut toParent;
   2.202 -	      TextIO.output (toParent, thmstring^"\n");
   2.203 -	      TextIO.flushOut toParent;
   2.204 -	      TextIO.output (toParent, goalstring^"\n");
   2.205 -	      TextIO.flushOut toParent;
   2.206 -	      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.207 -	      (* Attempt to prevent several signals from turning up simultaneously *)
   2.208 -	      Posix.Process.sleep(Time.fromSeconds 1);
   2.209 -	       true  
   2.210 -	    end
   2.211 -	   else if thisLine = "SPASS beiseite: Ran out of time.\n" 
   2.212 -	   then  
   2.213 -	     let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                          	(*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   2.214 -	     val _ = TextIO.output (outfile, thisLine)
   2.215 - 	     in TextIO.output (toParent, thisLine^"\n");
   2.216 -		TextIO.flushOut toParent;
   2.217 -		TextIO.output (toParent, thmstring^"\n");
   2.218 -		TextIO.flushOut toParent;
   2.219 -		TextIO.output (toParent, goalstring^"\n");
   2.220 -		TextIO.flushOut toParent;
   2.221 -		Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.222 -		TextIO.output (outfile, ("signalled parent\n"));TextIO.closeOut outfile;
   2.223 -	        (* Attempt to prevent several signals from turning up simultaneously *)
   2.224 -	        Posix.Process.sleep(Time.fromSeconds 1);
   2.225 -		true 
   2.226 -	     end
   2.227 -	  else if thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"                                                            		                 
   2.228 -	  then
   2.229 -             (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.230 -	      TextIO.output (toParent,childCmd^"\n" );
   2.231 -	      TextIO.flushOut toParent;
   2.232 -	      TextIO.output (toParent, thisLine);
   2.233 -	      TextIO.flushOut toParent;
   2.234 -	      true)
   2.235 -	  else
   2.236 -	     (TextIO.output (spass_proof_file, thisLine);
   2.237 -	     TextIO.flushOut spass_proof_file;
   2.238 -	     checkSpassProofFound  (fromChild, toParent, ppid, thmstring,goalstring,
   2.239 -	     childCmd, thm, sg_num, clause_arr,  num_of_clauses))
   2.240 -	 end
   2.241 -    else 
   2.242 -	(TextIO.output (spass_proof_file, ("No proof output seen \n"));
   2.243 -	 TextIO.closeOut spass_proof_file;
   2.244 -	 false)
   2.245 +	TextIO.output (toParent, thisLine^"\n");
   2.246 +	TextIO.output (toParent, thmstring^"\n");
   2.247 +	TextIO.output (toParent, goalstring^"\n");
   2.248 +	TextIO.flushOut toParent;
   2.249 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.250 +	(* Attempt to prevent several signals from turning up simultaneously *)
   2.251 +	Posix.Process.sleep(Time.fromSeconds 1);
   2.252 +	true)
   2.253 +     else if thisLine = "SPASS beiseite: Ran out of time.\n" 
   2.254 +     then  
   2.255 +       (File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
   2.256 +        TextIO.output (toParent, thisLine^"\n");
   2.257 +	TextIO.output (toParent, thmstring^"\n");
   2.258 +	TextIO.output (toParent, goalstring^"\n");
   2.259 +	TextIO.flushOut toParent;
   2.260 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.261 +	TextIO.output (spass_proof_file, "signalled parent\n");
   2.262 +	TextIO.closeOut spass_proof_file;
   2.263 +	(* Attempt to prevent several signals from turning up simultaneously *)
   2.264 +	Posix.Process.sleep(Time.fromSeconds 1);
   2.265 +	true)
   2.266 +    else if thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"                                                            		                 
   2.267 +    then
   2.268 +       (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.269 +	TextIO.output (toParent,childCmd^"\n" );
   2.270 +	TextIO.flushOut toParent;
   2.271 +	TextIO.output (toParent, thisLine);
   2.272 +	TextIO.flushOut toParent;
   2.273 +	true)
   2.274 +    else
   2.275 +       (TextIO.output (spass_proof_file, thisLine);
   2.276 +       TextIO.flushOut spass_proof_file;
   2.277 +       checkSpassProofFound  (fromChild, toParent, ppid, thmstring,goalstring,
   2.278 +       childCmd, thm, sg_num, clause_arr, num_of_clauses))
   2.279   end
   2.280  
   2.281    
   2.282 @@ -190,60 +154,28 @@
   2.283  (***********************************************************************)
   2.284  
   2.285  fun getSpassInput instr = 
   2.286 -  if isSome (TextIO.canInput(instr, 2))
   2.287 -  then
   2.288      let val thisLine = TextIO.inputLine instr 
   2.289 -	val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_thisLine")));
   2.290 -	val _ = TextIO.output (outfile, thisLine)
   2.291 -	val _ =  TextIO.closeOut outfile
   2.292 +        val _ = File.write (File.tmp_path (Path.basic "spass_line")) thisLine
   2.293      in 
   2.294 -      if substring (thisLine, 0,1) = "["
   2.295 -      then 
   2.296 -	(*Pretty.writeln(Pretty.str thisLine)*)
   2.297 -	let val reconstr = thisLine
   2.298 -	    val thmstring = TextIO.inputLine instr 
   2.299 -	    val goalstring = TextIO.inputLine instr   
   2.300 -	in
   2.301 -	    (reconstr, thmstring, goalstring)
   2.302 -	end
   2.303 -      else if String.isPrefix "SPASS beiseite:" thisLine 
   2.304 +      if thisLine = "" then ("No output from reconstruction process.\n","","")
   2.305 +      else if String.sub (thisLine, 0) = #"[" orelse
   2.306 +         String.isPrefix "SPASS beiseite:" thisLine orelse
   2.307 +         String.isPrefix  "Rules from" thisLine
   2.308        then 
   2.309 -	 let val reconstr = thisLine
   2.310 -	     val thmstring = TextIO.inputLine instr
   2.311 -	     val goalstring = TextIO.inputLine instr
   2.312 -	 in
   2.313 -	     (reconstr, thmstring, goalstring)
   2.314 -	 end
   2.315 -      else if String.isPrefix  "Rules from"  thisLine
   2.316 -      then 
   2.317 -	   let val reconstr = thisLine
   2.318 -	       val thmstring = TextIO.inputLine instr
   2.319 -	       val goalstring = TextIO.inputLine instr
   2.320 -	   in
   2.321 -	       (reconstr, thmstring, goalstring)
   2.322 -	   end
   2.323 -      else if substring (thisLine, 0,5) = "Proof"
   2.324 +	let val thmstring = TextIO.inputLine instr 
   2.325 +	    val goalstring = TextIO.inputLine instr   
   2.326 +	in (thisLine, thmstring, goalstring) end
   2.327 +      else if substring (thisLine,0,5) = "Proof" orelse
   2.328 +              String.sub (thisLine, 0) = #"%"
   2.329        then
   2.330 -	let val reconstr = thisLine
   2.331 -	    val thmstring = TextIO.inputLine instr
   2.332 +	let val thmstring = TextIO.inputLine instr
   2.333  	    val goalstring = TextIO.inputLine instr
   2.334  	in
   2.335 -          File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine;
   2.336 -          (reconstr, thmstring, goalstring)
   2.337 +          File.write (File.tmp_path (Path.basic "getSpassInput")) thisLine;
   2.338 +          (thisLine, thmstring, goalstring)
   2.339          end
   2.340 -      else if substring (thisLine, 0,1) = "%"
   2.341 -      then
   2.342 -	let val reconstr = thisLine
   2.343 -	    val thmstring = TextIO.inputLine instr
   2.344 -	    val goalstring = TextIO.inputLine instr
   2.345 -	in
   2.346 -           File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine;
   2.347 -	   (reconstr, thmstring, goalstring)
   2.348 -	end
   2.349        else getSpassInput instr
   2.350       end
   2.351 -  else 
   2.352 -      ("No output from reconstruction process.\n","","")
   2.353  
   2.354  
   2.355  end;
     3.1 --- a/src/HOL/Tools/ATP/VampCommunication.ML	Wed Sep 07 09:54:31 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/VampCommunication.ML	Wed Sep 07 18:14:26 2005 +0200
     3.3 @@ -18,16 +18,7 @@
     3.4  structure VampComm : VAMP_COMM =
     3.5  struct
     3.6  
     3.7 -(***********************************)
     3.8 -(*  Write Vampire output to a file *)
     3.9 -(***********************************)
    3.10 -
    3.11 -fun logVampInput (instr, fd) =
    3.12 -    let val thisLine = TextIO.inputLine instr
    3.13 -    in if (thisLine = "%==============  End of proof. ==================\n" )
    3.14 -       then TextIO.output (fd, thisLine)
    3.15 -       else (TextIO.output (fd, thisLine); logVampInput (instr,fd))
    3.16 -    end;
    3.17 +exception EOF;
    3.18  
    3.19  (**********************************************************************)
    3.20  (*  Reconstruct the Vampire proof w.r.t. thmstring (string version of   *)
    3.21 @@ -45,13 +36,17 @@
    3.22  		       goalstring toParent ppid negs clause_arr  num_of_clauses ))]) sg_num
    3.23  
    3.24  
    3.25 -fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr,  num_of_clauses) =
    3.26 +fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, 
    3.27 +                       currentString, thm, sg_num,clause_arr, num_of_clauses) =
    3.28    let val thisLine = TextIO.inputLine fromChild
    3.29    in
    3.30 -    if (thisLine = "%==============  End of proof. ==================\n" )
    3.31 +    if thisLine = "" (*end of file?*)
    3.32 +    then (File.write (File.tmp_path (Path.basic"vampire_extraction_failed")) currentString;
    3.33 +	  raise EOF)                    
    3.34 +    else if (thisLine = "%==============  End of proof. ==================\n" )
    3.35      then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    3.36  	 in
    3.37 -	   File.write (File.tmp_path (Path.basic"extracted-prf-vamp")) proofextract; 
    3.38 +	   File.write (File.tmp_path (Path.basic"vampire_extracted_prf")) proofextract; 
    3.39  	   reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  
    3.40  	                   clause_arr num_of_clauses thm
    3.41  	 end
    3.42 @@ -61,190 +56,114 @@
    3.43  
    3.44  
    3.45  (*********************************************************************************)
    3.46 -(*  Inspect the output of a Vampire process to see if it has found a proof,      *)
    3.47 +(*  Inspect the output of a Vampire process to see if it has found a proof,     *)
    3.48  (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    3.49  (*********************************************************************************)
    3.50  
    3.51  
    3.52  fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
    3.53                         thm, sg_num,clause_arr, num_of_clauses) =
    3.54 -    if isSome (TextIO.canInput(fromChild, 5))
    3.55 -    then
    3.56 -       let val thisLine = TextIO.inputLine fromChild
    3.57 -       in
    3.58 -         if (thisLine = "%================== Proof: ======================\n")
    3.59 -         then
    3.60 -          (File.append (File.tmp_path (Path.basic "transfer-vamp"))
    3.61 -                       ("about to transfer proof, thm is: " ^ string_of_thm thm);
    3.62 -           transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,
    3.63 -                              thisLine, thm, sg_num,clause_arr,  num_of_clauses);
    3.64 -           true)
    3.65 -         else
    3.66 -            startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,
    3.67 -                               childCmd, thm, sg_num,clause_arr, num_of_clauses)
    3.68 -       end
    3.69 -    else false
    3.70 -
    3.71 -
    3.72 -fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr,  num_of_clauses) =
    3.73 -    let val vamp_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "vamp_proof")))
    3.74 -        val _ = File.write (File.tmp_path (Path.basic "checking-prf-vamp"))
    3.75 -                           ("checking if proof found, thm is: " ^ string_of_thm thm)
    3.76 +    let val thisLine = TextIO.inputLine fromChild
    3.77      in
    3.78 -      if (isSome (TextIO.canInput(fromChild, 5)))
    3.79 +      if thisLine = "" then false
    3.80 +      else if (thisLine = "%================== Proof: ======================\n")
    3.81        then
    3.82 -        (
    3.83 -         let val thisLine = TextIO.inputLine fromChild
    3.84 -         in if (thisLine = "% Proof found. Thanks to Tanya!\n" )
    3.85 -            then
    3.86 -               let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));   
    3.87 -                        val _ = TextIO.output (outfile, (thisLine))
    3.88 -
    3.89 -                        val _ =  TextIO.closeOut outfile
    3.90 -               in
    3.91 -                 startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses)
    3.92 -               end
    3.93 -            else if (thisLine = "% Unprovable.\n" )
    3.94 -            then
    3.95 -               let    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
    3.96 -                           val _ = TextIO.output (outfile, (thisLine))
    3.97 -
    3.98 -                           val _ =  TextIO.closeOut outfile
    3.99 -               in
   3.100 -
   3.101 -                 TextIO.output (toParent,childCmd^"\n" );
   3.102 -                 TextIO.flushOut toParent;
   3.103 -                 TextIO.output (vamp_proof_file, (thisLine));
   3.104 -                 TextIO.flushOut vamp_proof_file;
   3.105 -                 TextIO.closeOut vamp_proof_file;
   3.106 -                 (*TextIO.output (toParent, thisLine);
   3.107 -                  TextIO.flushOut toParent;
   3.108 -                  TextIO.output (toParent, "bar\n");
   3.109 -                  TextIO.flushOut toParent;*)
   3.110 -
   3.111 -                 TextIO.output (toParent, thisLine^"\n");
   3.112 -                 TextIO.flushOut toParent;
   3.113 -                 TextIO.output (toParent, thmstring^"\n");
   3.114 -                 TextIO.flushOut toParent;
   3.115 -                 TextIO.output (toParent, goalstring^"\n");
   3.116 -                 TextIO.flushOut toParent;
   3.117 -                 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.118 -                 (* Attempt to prevent several signals from turning up simultaneously *)
   3.119 -                 Posix.Process.sleep(Time.fromSeconds 1);
   3.120 -                 true
   3.121 -               end
   3.122 -            else if (thisLine = "% Proof not found. Time limit expired.\n")
   3.123 -            then
   3.124 -              (let    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   3.125 -                           val _ = TextIO.output (outfile, (thisLine))
   3.126 -
   3.127 -                           val _ =  TextIO.closeOut outfile
   3.128 -               in
   3.129 -
   3.130 -                 TextIO.output (toParent,childCmd^"\n" );
   3.131 -                 TextIO.flushOut toParent;
   3.132 -                 TextIO.output (vamp_proof_file, (thisLine));
   3.133 -                 TextIO.flushOut vamp_proof_file;
   3.134 -                 TextIO.closeOut vamp_proof_file;
   3.135 -                 (*TextIO.output (toParent, thisLine);
   3.136 -                  TextIO.flushOut toParent;
   3.137 -                  TextIO.output (toParent, "bar\n");
   3.138 -                  TextIO.flushOut toParent;*)
   3.139 -
   3.140 -                 TextIO.output (toParent, thisLine^"\n");
   3.141 -                 TextIO.flushOut toParent;
   3.142 -                 TextIO.output (toParent, thmstring^"\n");
   3.143 -                 TextIO.flushOut toParent;
   3.144 -                 TextIO.output (toParent, goalstring^"\n");
   3.145 -                 TextIO.flushOut toParent;
   3.146 -                 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.147 -                 (* Attempt to prevent several signals from turning up simultaneously *)
   3.148 -                 Posix.Process.sleep(Time.fromSeconds 1);
   3.149 -                 true
   3.150 -               end
   3.151 -              )
   3.152 -
   3.153 -            else
   3.154 -              (TextIO.output (vamp_proof_file, (thisLine));
   3.155 -               TextIO.flushOut vamp_proof_file;
   3.156 -               checkVampProofFound  (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses))
   3.157 -
   3.158 -         end
   3.159 -           )
   3.160 +       (File.append (File.tmp_path (Path.basic "vampire_transfer"))
   3.161 +		    ("about to transfer proof, thm is: " ^ string_of_thm thm);
   3.162 +	transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,
   3.163 +			   thisLine, thm, sg_num,clause_arr, num_of_clauses);
   3.164 +	true) handle EOF => false
   3.165        else
   3.166 -        (TextIO.output (vamp_proof_file, ("No proof output seen \n"));TextIO.closeOut vamp_proof_file;false)
   3.167 +	 startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,
   3.168 +			    childCmd, thm, sg_num,clause_arr, num_of_clauses)
   3.169      end
   3.170  
   3.171  
   3.172 +fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, 
   3.173 +                         thm, sg_num, clause_arr, num_of_clauses) =
   3.174 + let val vamp_proof_file = TextIO.openAppend
   3.175 +	   (File.platform_path(File.tmp_path (Path.basic "vampire_proof")))
   3.176 +     val _ = File.write (File.tmp_path (Path.basic "vampire_checking_prf"))
   3.177 +			("checking if proof found, thm is: " ^ string_of_thm thm)
   3.178 +     val thisLine = TextIO.inputLine fromChild
   3.179 + in   
   3.180 +     if thisLine = "" 
   3.181 +     then (TextIO.output (vamp_proof_file, ("No proof output seen \n"));
   3.182 +	   TextIO.closeOut vamp_proof_file;
   3.183 +	   false)
   3.184 +     else if thisLine = "% Proof found. Thanks to Tanya!\n"
   3.185 +     then
   3.186 +      (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
   3.187 +       startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,
   3.188 +			  childCmd, thm, sg_num, clause_arr, num_of_clauses))
   3.189 +     else if (thisLine = "% Unprovable.\n" )
   3.190 +     then
   3.191 +      (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
   3.192 +       TextIO.output (toParent,childCmd^"\n" );
   3.193 +       TextIO.flushOut toParent;
   3.194 +       TextIO.output (vamp_proof_file, thisLine);
   3.195 +       TextIO.closeOut vamp_proof_file;
   3.196 +       (*TextIO.output (toParent, thisLine);
   3.197 +	TextIO.flushOut toParent;
   3.198 +	TextIO.output (toParent, "bar\n");
   3.199 +	TextIO.flushOut toParent;*)
   3.200 +
   3.201 +       TextIO.output (toParent, thisLine^"\n");
   3.202 +       TextIO.output (toParent, thmstring^"\n");
   3.203 +       TextIO.output (toParent, goalstring^"\n");
   3.204 +       TextIO.flushOut toParent;
   3.205 +       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.206 +       (* Attempt to prevent several signals from turning up simultaneously *)
   3.207 +       Posix.Process.sleep(Time.fromSeconds 1);
   3.208 +       true)
   3.209 +     else if (thisLine = "% Proof not found. Time limit expired.\n")
   3.210 +     then
   3.211 +      (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
   3.212 +       TextIO.output (toParent,childCmd^"\n" );
   3.213 +       TextIO.flushOut toParent;
   3.214 +       TextIO.output (vamp_proof_file, thisLine);
   3.215 +       TextIO.closeOut vamp_proof_file;
   3.216 +
   3.217 +       TextIO.output (toParent, thisLine^"\n");
   3.218 +       TextIO.output (toParent, thmstring^"\n");
   3.219 +       TextIO.output (toParent, goalstring^"\n");
   3.220 +       TextIO.flushOut toParent;
   3.221 +       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.222 +       (* Attempt to prevent several signals from turning up simultaneously *)
   3.223 +       Posix.Process.sleep(Time.fromSeconds 1);
   3.224 +       true)
   3.225 +     else
   3.226 +       (TextIO.output (vamp_proof_file, thisLine);
   3.227 +	TextIO.flushOut vamp_proof_file;
   3.228 +	checkVampProofFound  (fromChild, toParent, ppid, thmstring,
   3.229 +	   goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses))
   3.230 +  end
   3.231 +
   3.232 +
   3.233  (***********************************************************************)
   3.234 -(*  Function used by the Isabelle process to read in a vamp proof   *)
   3.235 +(*  Function used by the Isabelle process to read in a Vampire proof   *)
   3.236  (***********************************************************************)
   3.237  
   3.238  fun getVampInput instr =
   3.239 -    if (isSome (TextIO.canInput(instr, 2)))
   3.240 -    then
   3.241 -      let val thisLine = TextIO.inputLine instr
   3.242 -          val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
   3.243 +    let val thisLine = TextIO.inputLine instr
   3.244 +	val _ = File.write (File.tmp_path (Path.basic "vampire_line")) thisLine
   3.245 +    in    (* reconstructed proof string *)
   3.246 +      if thisLine = "" then ("No output from reconstruction process.\n","","")
   3.247 +      else if String.sub (thisLine, 0) = #"[" orelse
   3.248 +              thisLine = "% Unprovable.\n" orelse
   3.249 +              thisLine ="% Proof not found. Time limit expired.\n" orelse
   3.250 +              String.isPrefix "Rules from" thisLine
   3.251 +      then
   3.252 +	let val thmstring = TextIO.inputLine instr
   3.253 +	    val goalstring = TextIO.inputLine instr
   3.254 +	in (thisLine, thmstring, goalstring) end
   3.255 +      else if thisLine = "Proof found but translation failed!"
   3.256 +      then
   3.257 +	 let val thmstring = TextIO.inputLine instr
   3.258 +	     val goalstring = TextIO.inputLine instr
   3.259 +	     val _ = debug "getVampInput: translation of proof failed"
   3.260 +	 in (thisLine, thmstring, goalstring) end
   3.261 +      else getVampInput instr
   3.262 +    end
   3.263  
   3.264 -                                                                                                                                                                            val _ =  TextIO.closeOut outfile
   3.265 -      in    (* reconstructed proof string *)
   3.266 -        if ( (substring (thisLine, 0,1))= "[")
   3.267 -        then
   3.268 -          (*Pretty.writeln(Pretty.str (thisLine))*)
   3.269 -          let val reconstr = thisLine
   3.270 -              val thmstring = TextIO.inputLine instr
   3.271 -              val goalstring = TextIO.inputLine instr
   3.272 -          in
   3.273 -            (reconstr, thmstring, goalstring)
   3.274 -          end
   3.275 -        else if (thisLine = "% Unprovable.\n" )
   3.276 -        then
   3.277 -          (
   3.278 -           let val reconstr = thisLine
   3.279 -               val thmstring = TextIO.inputLine instr
   3.280 -               val goalstring = TextIO.inputLine instr
   3.281 -           in
   3.282 -             (reconstr, thmstring, goalstring)
   3.283 -           end
   3.284 -             )
   3.285 -        else  if (thisLine = "% Proof not found. Time limit expired.\n")
   3.286 -        then
   3.287 -          (
   3.288 -           let val reconstr = thisLine
   3.289 -               val thmstring = TextIO.inputLine instr
   3.290 -               val goalstring = TextIO.inputLine instr
   3.291 -           in
   3.292 -             (reconstr, thmstring, goalstring)
   3.293 -           end
   3.294 -             )
   3.295 -        else if (String.isPrefix   "Rules from"  thisLine)
   3.296 -        then
   3.297 -          (
   3.298 -           let val reconstr = thisLine
   3.299 -               val thmstring = TextIO.inputLine instr
   3.300 -               val goalstring = TextIO.inputLine instr
   3.301 -           in
   3.302 -             (reconstr, thmstring, goalstring)
   3.303 -           end
   3.304 -             )
   3.305 -
   3.306 -        else if (thisLine = "Proof found but translation failed!")
   3.307 -        then
   3.308 -          (
   3.309 -           let val reconstr = thisLine
   3.310 -               val thmstring = TextIO.inputLine instr
   3.311 -               val goalstring = TextIO.inputLine instr
   3.312 -               val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_getVamp")));
   3.313 -                    val _ = TextIO.output (outfile, (thisLine))
   3.314 -                    val _ =  TextIO.closeOut outfile
   3.315 -           in
   3.316 -             (reconstr, thmstring, goalstring)
   3.317 -           end
   3.318 -             )
   3.319 -        else
   3.320 -          getVampInput instr
   3.321 -
   3.322 -      end
   3.323 -    else
   3.324 -      ("No output from reconstruction process.\n","","")
   3.325  end;
     4.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Wed Sep 07 09:54:31 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Wed Sep 07 18:14:26 2005 +0200
     4.3 @@ -25,7 +25,6 @@
     4.4  (* Parser combinators *)
     4.5  
     4.6  exception Noparse;
     4.7 -exception SPASSError of string;
     4.8  exception VampError of string;
     4.9  
    4.10  
    4.11 @@ -118,47 +117,22 @@
    4.12            raise (GandalfError "Couldn't find a proof.")
    4.13  *)
    4.14  
    4.15 -val proofstring =
    4.16 -"0:00:00.00 for the reduction.\
    4.17 -\\
    4.18 -\Here is a proof with depth 3, length 7 :\
    4.19 -\1[0:Inp] ||  -> P(xa)*.\
    4.20 -\2[0:Inp] ||  -> Q(xb)*.\
    4.21 -\3[0:Inp] || R(U)* -> .\
    4.22 -\4[0:Inp] || Q(U) P(V) -> R(x(V,U))*.\
    4.23 -\9[0:Res:4.2,3.0] || Q(U)*+ P(V)* -> .\
    4.24 -\11[0:Res:2.0,9.0] || P(U)* -> .\
    4.25 -\12[0:Res:1.0,11.0] ||  -> .\
    4.26 -\Formulae used in the proof :\
    4.27 -\\
    4.28 -\--------------------------SPASS-STOP------------------------------"
    4.29 -
    4.30 -fun extract_proof s
    4.31 -      = if cut_exists "Here is a proof with" s then
    4.32 -          (kill_lines 0
    4.33 -           o snd o cut_after ":"
    4.34 -           o snd o cut_after "Here is a proof with"
    4.35 -           o fst o cut_after " ||  -> .") s
    4.36 -        else if cut_exists "%================== Proof: ======================" s then
    4.37 -          (kill_lines 0
    4.38 -           o snd o cut_after "%================== Proof: ======================"
    4.39 -           o fst o cut_before "==============  End of proof. ==================") s
    4.40 -        else
    4.41 -          raise SPASSError "Couldn't find a proof."
    4.42 -
    4.43 -(*fun extract_proof s
    4.44 -      = if cut_exists "Here is a proof with" s then
    4.45 -          (kill_lines 0
    4.46 -           o snd o cut_after ":"
    4.47 -           o snd o cut_after "Here is a proof with"
    4.48 -           o fst o cut_after " ||  -> .") s
    4.49 -        else
    4.50 -          raise SPASSError "Couldn't find a proof."
    4.51 -*)
    4.52 -
    4.53 -
    4.54 -
    4.55 -
    4.56 +(*Identifies the start/end lines of an ATP's output*)
    4.57 +fun extract_proof s =
    4.58 +  if cut_exists "Here is a proof with" s then
    4.59 +    (kill_lines 0
    4.60 +     o snd o cut_after ":"
    4.61 +     o snd o cut_after "Here is a proof with"
    4.62 +     o fst o cut_after " ||  -> .") s
    4.63 +  else if cut_exists "%================== Proof: ======================" s then
    4.64 +    (kill_lines 0    (*Vampire 5.0*)
    4.65 +     o snd o cut_after "%================== Proof: ======================"
    4.66 +     o fst o cut_before "==============  End of proof. ==================") s
    4.67 +  else if cut_exists "# Proof object ends here." s then
    4.68 +    (kill_lines 0    (*eproof*)
    4.69 +     o snd o cut_after "# Proof object starts here."
    4.70 +     o fst o cut_before "# Proof object ends here.") s
    4.71 +  else "??extract_proof failed" (*Couldn't find a proof*)
    4.72  
    4.73  fun several p = many (some p)
    4.74        fun collect (h, t) = h ^ (fold_rev (fn s1 => fn s2 => s1 ^ s2) t "")
    4.75 @@ -358,12 +332,6 @@
    4.76       
    4.77  exception NOTERM
    4.78  
    4.79 -
    4.80 -fun implode_with_space [] = implode []
    4.81 -|   implode_with_space [x] = implode [x]
    4.82 -|   implode_with_space (x::[y]) = x^" "^y
    4.83 -|   implode_with_space (x::xs) =  (x^" "^(implode_with_space xs))
    4.84 -
    4.85  (* FIX - should change the stars and pluses to many rather than explicit patterns *)
    4.86  
    4.87  fun trim_prefix a b =
    4.88 @@ -499,87 +467,22 @@
    4.89  
    4.90  (*and arglist input = (    nterm >> (fn (a) => (a))
    4.91                       ||  nterm ++ many (a (Other ",") ++ nterm >> snd)
    4.92 -                      >> (fn (a, b) => (a^" "^(implode_with_space b)))) input*)
    4.93 +                      >> (fn (a, b) => (a^" "^(space_implode " " b)))) input*)
    4.94  
    4.95  and arglist input = (   nterm ++ many (a (Other ",") ++ nterm >> snd)
    4.96 -                      >> (fn (a, b) => (a^" "^(implode_with_space b))) 
    4.97 +                      >> (fn (a, b) => (a^" "^(space_implode " " b))) 
    4.98                        ||    nterm >> (fn (a) => (a)))input
    4.99  
   4.100   val clause =  term
   4.101  
   4.102 -
   4.103 -
   4.104 - (*val line = number ++ justification ++ a (Other "|") ++ 
   4.105 -            a (Other "|") ++ clause ++ a (Other ".")
   4.106 -          >> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c))*)
   4.107 -
   4.108 -
   4.109  (* not entirely sure nterm is right here, but I don't think you get negative things before the ||s *)
   4.110   val line = number ++ justification ++ many( nterm) ++ a (Other "|") ++ 
   4.111              a (Other "|") ++ clause ++ a (Other ".")
   4.112            >> (fn (a, (z, (w, (_,( _, (c, _)))))) => (a, z,(w@ c)))
   4.113         
   4.114 -
   4.115 -
   4.116   val lines = many line
   4.117   val alllines = (lines ++ finished) >> fst
   4.118      
   4.119   val parse = fst o alllines
   4.120 - val s = proofstring;
   4.121 - 
   4.122 - 
   4.123 -
   4.124 -
   4.125 -fun dropUntilNot ch []   = ( [])
   4.126 - |   dropUntilNot ch (x::xs)  = if  not(x = ch )
   4.127 -                                then
   4.128 -                                     (x::xs)
   4.129 -                                else
   4.130 -                                     dropUntilNot ch xs
   4.131 -
   4.132 -
   4.133 -fun remove_spaces str  []  = str
   4.134 -|   remove_spaces str (x::[]) = if x = " " 
   4.135 -                                then 
   4.136 -                                    str 
   4.137 -                                else 
   4.138 -                                    (str^x)
   4.139 -|   remove_spaces str (x::xs) = 
   4.140 -      let val (first, rest) = ReconOrderClauses.takeUntil " " (x::xs) []
   4.141 -	  val (next) = dropUntilNot " " rest 
   4.142 -      in 
   4.143 -	  if next = []
   4.144 -	  then 
   4.145 -	       (str^(implode first)) 
   4.146 -	  else remove_spaces  (str^(implode first)^" ") next 
   4.147 -      end
   4.148 -
   4.149 -
   4.150 -fun remove_space_strs clsstrs = map (remove_spaces "") (map explode clsstrs)
   4.151 -
   4.152 -
   4.153 -fun all_spaces xs = List.filter  (not_equal " " ) xs
   4.154 -
   4.155 -fun just_change_space []  = []
   4.156 -|   just_change_space ((clausenum, step, strs)::xs) =
   4.157 -      let val newstrs = remove_space_strs strs
   4.158 -      in
   4.159 -	 if (all_spaces newstrs = [] ) (* all type_info *)
   4.160 -	 then    
   4.161 -	    (clausenum, step, newstrs)::(just_change_space xs)
   4.162 -	 else 
   4.163 -	     (clausenum, step, newstrs)::(just_change_space xs) 
   4.164 -      end;
   4.165 -
   4.166 -fun change_space []  = []
   4.167 -|   change_space ((clausenum, step, strs)::xs) = 
   4.168 -      let val newstrs = remove_space_strs strs
   4.169 -      in
   4.170 -	 if (all_spaces newstrs = [] ) (* all type_info *)
   4.171 -	 then    
   4.172 -	    (clausenum, step, T_info, newstrs)::(change_space xs)
   4.173 -	 else 
   4.174 -	     (clausenum, step, P_info, newstrs)::(change_space xs) 
   4.175 -      end
   4.176  
   4.177  end;
     5.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 07 09:54:31 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 07 18:14:26 2005 +0200
     5.3 @@ -175,12 +175,10 @@
     5.4  (* get names of clasimp axioms used                  *)
     5.5  (*****************************************************)
     5.6  
     5.7 - fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
     5.8 + fun get_axiom_names step_nums thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
     5.9     let 
    5.10       (* not sure why this is necessary again, but seems to be *)
    5.11        val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    5.12 -      val axioms = get_init_axioms proof_steps
    5.13 -      val step_nums = get_step_nums axioms []
    5.14    
    5.15       (***********************************************)
    5.16       (* here need to add the clauses from clause_arr*)
    5.17 @@ -195,47 +193,14 @@
    5.18     in
    5.19        clasimp_names
    5.20     end
    5.21 -    
    5.22 - fun get_axiom_names_vamp proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    5.23 -   let 
    5.24 -     (* not sure why this is necessary again, but seems to be *)
    5.25 -      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    5.26 -      val step_nums =get_linenums proofstr
    5.27 -  
    5.28 -     (***********************************************)
    5.29 -     (* here need to add the clauses from clause_arr*)
    5.30 -     (***********************************************)
    5.31 -  
    5.32 -      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
    5.33 -      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
    5.34 -  
    5.35 -      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    5.36 -                         (concat clasimp_names)
    5.37 -      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    5.38 -   in
    5.39 -      clasimp_names
    5.40 -   end
    5.41 +   
    5.42 + fun get_axiom_names_spass proof_steps thms clause_arr num_of_clauses  =
    5.43 +   get_axiom_names (get_step_nums (get_init_axioms proof_steps) []) 
    5.44 +                       thms clause_arr num_of_clauses;
    5.45      
    5.46 -
    5.47 -fun get_axiom_names_E proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    5.48 -   let 
    5.49 -     (* not sure why this is necessary again, but seems to be *)
    5.50 -      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    5.51 -      val step_nums =get_linenums proofstr
    5.52 -  
    5.53 -     (***********************************************)
    5.54 -     (* here need to add the clauses from clause_arr*)
    5.55 -     (***********************************************)
    5.56 -  
    5.57 -      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
    5.58 -      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
    5.59 -  
    5.60 -      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    5.61 -                         (concat clasimp_names)
    5.62 -      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    5.63 -   in
    5.64 -      clasimp_names
    5.65 -   end
    5.66 + fun get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses  =
    5.67 +   get_axiom_names (get_linenums proofstr) thms clause_arr num_of_clauses;
    5.68 +    
    5.69  
    5.70  (***********************************************)
    5.71  (* get axioms for reconstruction               *)
    5.72 @@ -255,19 +220,6 @@
    5.73  	val axioms = get_init_axioms proof_steps
    5.74  	val step_nums = get_step_nums axioms []
    5.75  
    5.76 -       (***********************************************)
    5.77 -       (* here need to add the clauses from clause_arr*)
    5.78 -       (***********************************************)
    5.79 -
    5.80 -       (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
    5.81 -	val clasimp_names = map #1 clasimp_names_cls
    5.82 -	val clasimp_cls = map #2 clasimp_names_cls
    5.83 -	val _ = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
    5.84 -	 val _ = TextIO.output (outfile,clasimp_namestr)
    5.85 -	 
    5.86 -	 val _ =  TextIO.closeOut outfile
    5.87 -*)
    5.88 -
    5.89  	val clauses =(*(clasimp_cls)@*)( make_clauses thms)
    5.90  	
    5.91  	val vars = map thm_vars clauses
    5.92 @@ -302,20 +254,8 @@
    5.93  	val extra_with_vars = if (not (extra_metas = []) ) 
    5.94  			      then ListPair.zip (extra_metas,extra_vars)
    5.95  			      else []
    5.96 -       (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    5.97 -       val _ = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas")))
    5.98 -
    5.99 -       val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
   5.100 -       val _ =  TextIO.closeOut outfile
   5.101 -      val foo_metas =  File.platform_path(File.tmp_path (Path.basic "foo_metas"))
   5.102 -      val foo_metas2 =   File.platform_path(File.tmp_path (Path.basic "foo_metas2"))
   5.103 -	val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", "  <", foo_metas, "  >", foo_metas2])
   5.104 -     val infile = TextIO.openIn(File.platform_path(File.tmp_path (Path.basic "foo_metas2")))
   5.105 -    val ax_metas_str = TextIO.inputLine (infile)
   5.106 -    val _ = TextIO.closeIn infile
   5.107 -       val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
   5.108       in
   5.109 -	(distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
   5.110 +	(distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
   5.111       end;
   5.112                                              
   5.113  
   5.114 @@ -329,9 +269,6 @@
   5.115    | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
   5.116                                    
   5.117  
   5.118 -val dummy_tac = PRIMITIVE(fn thm => thm );
   5.119 -
   5.120 -
   5.121  (*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)**.\
   5.122  \1279[0:Inp] ||  -> equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(U),tconst_nat),const_List_Olist_ONil),const_0)**.\
   5.123  \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))** -> .\
   5.124 @@ -351,10 +288,10 @@
   5.125       (* parse spass proof into datatype *)
   5.126       (***********************************)
   5.127        val tokens = #1(lex proofstr)
   5.128 -      val proof_steps1 = parse tokens
   5.129 -      val proof_steps = just_change_space proof_steps1
   5.130 -      val _ = File.write (File.tmp_path (Path.basic "foo_parse")) ("Did parsing on "^proofstr)
   5.131 -      val _ = File.write(File.tmp_path (Path.basic "foo_thmstring_at_parse"))
   5.132 +      val proof_steps = parse tokens
   5.133 +      val _ = File.write (File.tmp_path (Path.basic "parsing_done")) 
   5.134 +                         ("Did parsing on "^proofstr)
   5.135 +      val _ = File.write(File.tmp_path (Path.basic "parsing_thmstring"))
   5.136                          ("Parsing for thmstring: "^thmstring)
   5.137        (************************************)
   5.138        (* recreate original subgoal as thm *)
   5.139 @@ -366,22 +303,20 @@
   5.140        (* should prob add array and table here, so that we can get axioms*)
   5.141        (* produced from the clasimpset rather than the problem *)
   5.142  
   5.143 -      val (axiom_names) = get_axiom_names proof_steps  thms clause_arr  num_of_clauses
   5.144 +      val axiom_names = get_axiom_names_spass proof_steps thms clause_arr num_of_clauses
   5.145        val ax_str = "Rules from clasimpset used in proof found by SPASS: " ^ 
   5.146                     rules_to_string axiom_names 
   5.147        val _ = File.append(File.tmp_path (Path.basic "reconstrfile"))
   5.148                           ("reconstring is: "^ax_str^"  "^goalstring)       
   5.149    in 
   5.150         TextIO.output (toParent, ax_str^"\n");
   5.151 -       TextIO.flushOut toParent;
   5.152         TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   5.153 -       TextIO.flushOut toParent;
   5.154         TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   5.155         TextIO.flushOut toParent;
   5.156  
   5.157         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   5.158        (* Attempt to prevent several signals from turning up simultaneously *)
   5.159 -       Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   5.160 +       Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   5.161    end
   5.162    handle _ => 
   5.163    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   5.164 @@ -394,7 +329,7 @@
   5.165         TextIO.flushOut toParent;
   5.166        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   5.167        (* Attempt to prevent several signals from turning up simultaneously *)
   5.168 -      Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   5.169 +      Posix.Process.sleep(Time.fromSeconds 1); all_tac
   5.170    end
   5.171  
   5.172  
   5.173 @@ -408,34 +343,29 @@
   5.174      (* get vampire axiom names         *)
   5.175      (***********************************)
   5.176  
   5.177 -     val (axiom_names) = get_axiom_names_vamp proofstr  thms clause_arr  num_of_clauses
   5.178 +     val axiom_names = get_axiom_names_vamp_E proofstr  thms clause_arr  num_of_clauses
   5.179       val ax_str = "Rules from clasimpset used in proof found by Vampire: " ^
   5.180                    rules_to_string axiom_names
   5.181      in 
   5.182  	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
   5.183           TextIO.output (toParent, ax_str^"\n");
   5.184 -	 TextIO.flushOut toParent;
   5.185  	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   5.186 -	 TextIO.flushOut toParent;
   5.187  	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   5.188  	 TextIO.flushOut toParent;
   5.189  
   5.190  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   5.191  	(* Attempt to prevent several signals from turning up simultaneously *)
   5.192 -	 Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   5.193 +	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   5.194      end
   5.195      handle _ => 
   5.196      let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   5.197      in 
   5.198  	TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   5.199 -	TextIO.flushOut toParent;
   5.200  	 TextIO.output (toParent, thmstring^"\n");
   5.201 -	 TextIO.flushOut toParent;
   5.202  	 TextIO.output (toParent, goalstring^"\n");
   5.203  	 TextIO.flushOut toParent;
   5.204  	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   5.205 -	(* Attempt to prevent several signals from turning up simultaneously *)
   5.206 -	Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   5.207 +	Posix.Process.sleep(Time.fromSeconds 1); all_tac
   5.208      end;
   5.209  
   5.210  
   5.211 @@ -446,42 +376,35 @@
   5.212                  (string_of_int num_of_clauses))
   5.213  
   5.214      (***********************************)
   5.215 -    (* get vampire axiom names         *)
   5.216 +    (* get E axiom names         *)
   5.217      (***********************************)
   5.218  
   5.219 -     val (axiom_names) = get_axiom_names_E proofstr  thms clause_arr  num_of_clauses
   5.220 +     val axiom_names = get_axiom_names_vamp_E proofstr  thms clause_arr  num_of_clauses
   5.221       val ax_str = "Rules from clasimpset used in proof found by E: " ^
   5.222                    rules_to_string axiom_names
   5.223      in 
   5.224  	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
   5.225           TextIO.output (toParent, ax_str^"\n");
   5.226  	 TextIO.flushOut toParent;
   5.227 -	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   5.228 -	 TextIO.flushOut toParent;
   5.229  	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   5.230  	 TextIO.flushOut toParent;
   5.231  
   5.232  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   5.233  	(* Attempt to prevent several signals from turning up simultaneously *)
   5.234 -	 Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   5.235 +	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   5.236      end
   5.237      handle _ => 
   5.238      let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   5.239      in 
   5.240 -	TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   5.241 -	TextIO.flushOut toParent;
   5.242 +	TextIO.output (toParent,"Proof found by E but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   5.243  	 TextIO.output (toParent, thmstring^"\n");
   5.244 -	 TextIO.flushOut toParent;
   5.245  	 TextIO.output (toParent, goalstring^"\n");
   5.246  	 TextIO.flushOut toParent;
   5.247  	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   5.248  	(* Attempt to prevent several signals from turning up simultaneously *)
   5.249 -	Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   5.250 +	Posix.Process.sleep(Time.fromSeconds 1); all_tac
   5.251      end;
   5.252  
   5.253 -(* val proofstr = "1582[0:Inp] || -> v_P*.\
   5.254 -                 \1583[0:Inp] || v_P* -> .\
   5.255 -		 \1584[0:MRR:1583.0,1582.0] || -> ."; *)
   5.256  
   5.257  fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   5.258    let val _ = File.write(File.tmp_path (Path.basic "thmstringfile")) 
   5.259 @@ -491,8 +414,7 @@
   5.260    (***********************************)
   5.261    (* parse spass proof into datatype *)
   5.262    (***********************************)
   5.263 -      val proof_steps1 = parse tokens
   5.264 -      val proof_steps = just_change_space proof_steps1
   5.265 +      val proof_steps = parse tokens
   5.266  
   5.267        val _ = File.write (File.tmp_path (Path.basic "foo_parse"))
   5.268                        ("Did parsing on "^proofstr)
   5.269 @@ -550,7 +472,7 @@
   5.270  
   5.271         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   5.272        (* Attempt to prevent several signals from turning up simultaneously *)
   5.273 -       Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   5.274 +       Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   5.275    end
   5.276    handle _ => 
   5.277    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   5.278 @@ -563,7 +485,7 @@
   5.279         TextIO.flushOut toParent;
   5.280        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   5.281        (* Attempt to prevent several signals from turning up simultaneously *)
   5.282 -      Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   5.283 +      Posix.Process.sleep(Time.fromSeconds 1); all_tac
   5.284    end
   5.285  
   5.286  
   5.287 @@ -643,8 +565,9 @@
   5.288  
   5.289  
   5.290  (** change this to allow P (x U) *)
   5.291 - fun arglist_step input = ( word ++ many  word >> (fn (a, b) => (a^" "^(implode_with_space b)))
   5.292 -                           ||word >> (fn (a) => (a)))input
   5.293 + fun arglist_step input = 
   5.294 +   ( word ++ many word >> (fn (a, b) => (a^" "^(space_implode " " b)))
   5.295 +    ||word >> (fn (a) => (a)))input
   5.296                  
   5.297  
   5.298  fun literal_step input = (word ++ a (Other "(") ++ arglist_step ++  a (Other ")")
     6.1 --- a/src/HOL/Tools/ATP/watcher.ML	Wed Sep 07 09:54:31 2005 +0200
     6.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Sep 07 18:14:26 2005 +0200
     6.3 @@ -328,76 +328,63 @@
     6.4  	   val sign = sign_of_thm thm
     6.5  	   val prems = prems_of thm
     6.6  	   val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
     6.7 -	   val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
     6.8 -	  (* tracing *)
     6.9 -	 (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
    6.10 -	   val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
    6.11 -	   val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
    6.12 -	   val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
    6.13 -	   val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
    6.14 -	   val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
    6.15 -		    *)
    6.16 -	   (*val goalstr = string_of_thm (the_goal)
    6.17 -	    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher")));  
    6.18 -	   val _ = TextIO.output (outfile,goalstr )
    6.19 -	   val _ =  TextIO.closeOut outfile*)
    6.20 +	   val _ = debug ("subgoals forked to startWatcher: "^prems_string);
    6.21  	   fun killChildren [] = ()
    6.22 -	|      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
    6.23 +	|      killChildren  (child_handle::children) =
    6.24 +	         (killChild child_handle; killChildren children)
    6.25  
    6.26  	 (*************************************************************)
    6.27  	 (* take an instream and poll its underlying reader for input *)
    6.28  	 (*************************************************************)
    6.29  
    6.30  	 fun pollParentInput () = 
    6.31 -	    let val pd = OS.IO.pollDesc (fromParentIOD)
    6.32 -	    in 
    6.33 -	      if (isSome pd ) then 
    6.34 -		  let val pd' = OS.IO.pollIn (valOf pd)
    6.35 -		      val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
    6.36 -		      val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
    6.37 -			("In parent_poll\n")	
    6.38 -		  in
    6.39 -		     if null pdl 
    6.40 -		     then
    6.41 -			NONE
    6.42 -		     else if (OS.IO.isIn (hd pdl)) 
    6.43 -			  then SOME (getCmds (toParentStr, fromParentStr, []))
    6.44 -			  else NONE
    6.45 -		  end
    6.46 -		else NONE
    6.47 -	    end
    6.48 +	   let val pd = OS.IO.pollDesc (fromParentIOD)
    6.49 +	   in 
    6.50 +	     if isSome pd then 
    6.51 +		 let val pd' = OS.IO.pollIn (valOf pd)
    6.52 +		     val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
    6.53 +		     val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
    6.54 +		       ("In parent_poll\n")	
    6.55 +		 in
    6.56 +		    if null pdl 
    6.57 +		    then
    6.58 +		       NONE
    6.59 +		    else if (OS.IO.isIn (hd pdl)) 
    6.60 +			 then SOME (getCmds (toParentStr, fromParentStr, []))
    6.61 +			 else NONE
    6.62 +		 end
    6.63 +	       else NONE
    6.64 +	   end
    6.65  		 
    6.66  	  fun pollChildInput (fromStr) = 
    6.67 -	    let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
    6.68 -			  ("In child_poll\n")
    6.69 -		val iod = getInIoDesc fromStr
    6.70 -	    in 
    6.71 -	      if isSome iod 
    6.72 -	      then 
    6.73 -		let val pd = OS.IO.pollDesc (valOf iod)
    6.74 -		in 
    6.75 -		if (isSome pd ) then 
    6.76 -		    let val pd' = OS.IO.pollIn (valOf pd)
    6.77 -			val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
    6.78 -		    in
    6.79 -		       if null pdl 
    6.80 -		       then
    6.81 -			 ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
    6.82 -			  ("Null pdl \n");NONE)
    6.83 -		       else if (OS.IO.isIn (hd pdl)) 
    6.84 -			    then
    6.85 -				(let val inval =  (TextIO.inputLine fromStr)
    6.86 -				     val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
    6.87 -				 in
    6.88 -				       SOME inval
    6.89 -				 end)
    6.90 -			    else
    6.91 -				  ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
    6.92 -			  ("Null pdl \n");NONE)
    6.93 -		    end
    6.94 -		  else  NONE
    6.95 -		  end
    6.96 -	      else NONE
    6.97 +	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
    6.98 +			 ("In child_poll\n")
    6.99 +	       val iod = getInIoDesc fromStr
   6.100 +	   in 
   6.101 +	     if isSome iod 
   6.102 +	     then 
   6.103 +	       let val pd = OS.IO.pollDesc (valOf iod)
   6.104 +	       in 
   6.105 +	       if isSome pd then 
   6.106 +		   let val pd' = OS.IO.pollIn (valOf pd)
   6.107 +		       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   6.108 +		   in
   6.109 +		      if null pdl 
   6.110 +		      then
   6.111 +			(File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl\n"; 
   6.112 +			 NONE)
   6.113 +		      else if OS.IO.isIn (hd pdl)
   6.114 +		      then
   6.115 +			   let val inval =  (TextIO.inputLine fromStr)
   6.116 +			       val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
   6.117 +			   in SOME inval end
   6.118 +		      else
   6.119 +                        (File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl \n";
   6.120 +                         NONE)
   6.121 +		   end
   6.122 +		 else NONE
   6.123 +		 end
   6.124 +	     else NONE
   6.125  	end
   6.126  
   6.127  
   6.128 @@ -434,37 +421,37 @@
   6.129  		   val sign = sign_of_thm thm
   6.130  		   val prems = prems_of thm
   6.131  		   val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   6.132 -		   val _ = warning("subgoals forked to checkChildren: "^prems_string)
   6.133 +		   val _ = debug("subgoals forked to checkChildren: "^prems_string)
   6.134  		   val goalstring = cmdGoal childProc							
   6.135  		   val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
   6.136  			      (prover^thmstring^goalstring^childCmd^"\n")
   6.137  	       in 
   6.138 -		 if (isSome childIncoming) 
   6.139 +		 if isSome childIncoming
   6.140  		 then 
   6.141 -		     (* check here for prover label on child*)
   6.142 -		     let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) 
   6.143 -				("subgoals forked to checkChildren:"^
   6.144 -				prems_string^prover^thmstring^goalstring^childCmd) 
   6.145 -			 val childDone = (case prover of
   6.146 -			     "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )     
   6.147 -                              | "E" => (EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )              
   6.148 -			    |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   6.149 -		      in
   6.150 -		       if childDone      (**********************************************)
   6.151 -		       then (* child has found a proof and transferred it *)
   6.152 -			  (* Remove this child and go on to check others*)
   6.153 -			  (**********************************************)
   6.154 -			  (Unix.reap child_handle;
   6.155 -			   checkChildren(otherChildren, toParentStr))
   6.156 -		       else 
   6.157 -			  (**********************************************)
   6.158 -			  (* Keep this child and go on to check others  *)
   6.159 -			  (**********************************************)
   6.160 -			 (childProc::(checkChildren (otherChildren, toParentStr)))
   6.161 -		    end
   6.162 -		  else
   6.163 -		    (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   6.164 -		     childProc::(checkChildren (otherChildren, toParentStr)))
   6.165 +		   (* check here for prover label on child*)
   6.166 +		   let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) 
   6.167 +			      ("subgoals forked to checkChildren:"^
   6.168 +			      prems_string^prover^thmstring^goalstring^childCmd) 
   6.169 +		       val childDone = (case prover of
   6.170 +			   "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  
   6.171 +			    | "E" => EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
   6.172 +			  |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  )
   6.173 +		    in
   6.174 +		     if childDone      (**********************************************)
   6.175 +		     then (* child has found a proof and transferred it *)
   6.176 +			(* Remove this child and go on to check others*)
   6.177 +			(**********************************************)
   6.178 +			(Unix.reap child_handle;
   6.179 +			 checkChildren(otherChildren, toParentStr))
   6.180 +		     else 
   6.181 +			(**********************************************)
   6.182 +			(* Keep this child and go on to check others  *)
   6.183 +			(**********************************************)
   6.184 +		       (childProc::(checkChildren (otherChildren, toParentStr)))
   6.185 +		  end
   6.186 +		else
   6.187 +		  (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   6.188 +		   childProc::(checkChildren (otherChildren, toParentStr)))
   6.189  	       end
   6.190  
   6.191  	
   6.192 @@ -480,7 +467,7 @@
   6.193  	fun execCmds  [] procList = procList
   6.194  	|   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =             let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child"))  ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   6.195  	  in 
   6.196 -	    if (prover = "spass") 
   6.197 +	    if prover = "spass"
   6.198  	    then 
   6.199  	      let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   6.200  		       (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   6.201 @@ -495,7 +482,8 @@
   6.202  				       outstr = outstr })::procList))
   6.203  		   val _ = File.append (File.tmp_path (Path.basic "exec_child"))  
   6.204  			("\nexecuting command for goal:\n"^
   6.205 -			 goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   6.206 +			 goalstring^proverCmd^(concat settings)^file^
   6.207 +			 " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   6.208  	      in
   6.209  		 Posix.Process.sleep (Time.fromSeconds 1);
   6.210  		 execCmds cmds newProcList
   6.211 @@ -546,31 +534,33 @@
   6.212       (**********************************************)                  
   6.213       (* Watcher Loop                               *)
   6.214       (**********************************************)
   6.215 +         val iterations_left = ref 1000;  (*200 seconds, 5 iterations per sec*)
   6.216  
   6.217  	 fun keepWatching (toParentStr, fromParentStr,procList) = 
   6.218  	   let fun loop (procList) =  
   6.219  		let val _ = Posix.Process.sleep (Time.fromMilliseconds 200)
   6.220  		    val cmdsFromIsa = pollParentInput ()
   6.221 -		    fun killchildHandler (n:int)  = 
   6.222 -			  (TextIO.output(toParentStr, "Killing child proof processes!\n");
   6.223 +		    fun killchildHandler ()  = 
   6.224 +			  (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   6.225  			   TextIO.flushOut toParentStr;
   6.226  			   killChildren (map (cmdchildHandle) procList);
   6.227  			   ())
   6.228  		in 
   6.229  		   (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   6.230 -								      (**********************************)
   6.231 -		   if (isSome cmdsFromIsa) 
   6.232 +		   iterations_left := !iterations_left - 1;
   6.233 +		   if !iterations_left = 0 then killchildHandler ()
   6.234 +		   else if isSome cmdsFromIsa
   6.235  		   then (*  deal with input from Isabelle *)
   6.236 -		     if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   6.237 +		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
   6.238  		     then 
   6.239  		       let val child_handles = map cmdchildHandle procList 
   6.240  		       in
   6.241  			  killChildren child_handles;
   6.242  			  (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)    
   6.243 -			  loop ([])
   6.244 +			  loop []
   6.245  		       end
   6.246  		     else
   6.247 -		       if ((length procList)<10)    (********************)
   6.248 +		       if length procList < 5     (********************)
   6.249  		       then                        (* Execute locally  *)
   6.250  			 let 
   6.251  			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   6.252 @@ -578,10 +568,10 @@
   6.253  			      val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
   6.254  			   val newProcList' =checkChildren (newProcList, toParentStr) 
   6.255  
   6.256 -			   val _ = warning("off to keep watching...")
   6.257 +			   val _ = debug("off to keep watching...")
   6.258  			  val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
   6.259  			 in
   6.260 -			   loop (newProcList') 
   6.261 +			   loop newProcList'
   6.262  			 end
   6.263  		       else  (* Execute remotely              *)
   6.264  			     (* (actually not remote for now )*)
   6.265 @@ -590,17 +580,17 @@
   6.266  			   val parentID = Posix.ProcEnv.getppid()
   6.267  			   val newProcList' =checkChildren (newProcList, toParentStr) 
   6.268  			 in
   6.269 -			   loop (newProcList') 
   6.270 +			   loop newProcList'
   6.271  			 end
   6.272  		   else (* No new input from Isabelle *)
   6.273  		     let val newProcList = checkChildren ((procList), toParentStr)
   6.274  		     in
   6.275  		      (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
   6.276 -		       loop (newProcList)
   6.277 +		       loop newProcList
   6.278  		     end
   6.279  		 end
   6.280  	   in  
   6.281 -	       loop (procList)
   6.282 +	       loop procList
   6.283  	   end
   6.284  	   
   6.285  
   6.286 @@ -678,7 +668,8 @@
   6.287  	  status
   6.288    end
   6.289  
   6.290 -fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) =
   6.291 +
   6.292 +fun createWatcher (thm,clause_arr, num_of_clauses) =
   6.293   let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   6.294       val streams = snd mychild
   6.295       val childin = fst streams
   6.296 @@ -687,34 +678,33 @@
   6.297       val sign = sign_of_thm thm
   6.298       val prems = prems_of thm
   6.299       val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   6.300 -     val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   6.301 +     val _ = debug ("subgoals forked to createWatcher: "^prems_string);
   6.302 +(*FIXME: do we need an E proofHandler??*)
   6.303       fun vampire_proofHandler (n) =
   6.304  	(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   6.305  	 VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))               
   6.306       fun spass_proofHandler (n) = (
   6.307 -       let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
   6.308 -	   val _ = TextIO.output (outfile, ("In signal handler now\n"))
   6.309 -	   val _ =  TextIO.closeOut outfile
   6.310 +       let val _ = File.append (File.tmp_path (Path.basic "spass_signal_in"))
   6.311 +                               "Starting SPASS signal handler\n"
   6.312  	   val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
   6.313 -	   val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
   6.314 -   
   6.315 -	   val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   6.316 -	   val _ =  TextIO.closeOut outfile
   6.317 +	   val _ = File.append (File.tmp_path (Path.basic "spass_signal_out"))
   6.318 +		       ("In SPASS signal handler "^reconstr^thmstring^goalstring^
   6.319 +		       "goals_being_watched: "^ string_of_int (!goals_being_watched))
   6.320         in (* if a proof has been found and sent back as a reconstruction proof *)
   6.321  	 if substring (reconstr, 0,1) = "["
   6.322  	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   6.323  	       Recon_Transfer.apply_res_thm reconstr goalstring;
   6.324  	       Pretty.writeln(Pretty.str  (oct_char "361"));
   6.325  	       
   6.326 -	       goals_being_watched := ((!goals_being_watched) - 1);
   6.327 +	       goals_being_watched := (!goals_being_watched) - 1;
   6.328         
   6.329 -	       if (!goals_being_watched) = 0
   6.330 +	       if !goals_being_watched = 0
   6.331  	       then 
   6.332 -		  let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found"))
   6.333 -                                   ("Reaping a watcher, goals watched is: "^
   6.334 -                                    (string_of_int (!goals_being_watched))^"\n")
   6.335 +		  let val _ = File.write (File.tmp_path (Path.basic "reap_found"))
   6.336 +                                   ("Reaping a watcher, goals watched now "^
   6.337 +                                    string_of_int (!goals_being_watched)^"\n")
   6.338  		   in
   6.339 -		       killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   6.340 +		       killWatcher childpid; reapWatcher (childpid,childin, childout); ()
   6.341  		   end
   6.342  		else () )
   6.343  	 (* if there's no proof, but a message from Spass *)
     7.1 --- a/src/HOL/Tools/res_atp.ML	Wed Sep 07 09:54:31 2005 +0200
     7.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Sep 07 18:14:26 2005 +0200
     7.3 @@ -8,9 +8,7 @@
     7.4  signature RES_ATP =
     7.5  sig
     7.6    val axiom_file : Path.T
     7.7 -  val full_spass: bool ref
     7.8 -  val spass: bool ref
     7.9 -  val vampire: bool ref
    7.10 +  val prover: string ref
    7.11    val custom_spass: string list ref
    7.12    val hook_count: int ref
    7.13  end;
    7.14 @@ -24,9 +22,7 @@
    7.15  
    7.16  fun debug_tac tac = (debug "testing"; tac);
    7.17  
    7.18 -val vampire = ref false;   (* use Vampire as default prover? *)
    7.19 -val spass = ref true;      (* use spass as default prover *)
    7.20 -val full_spass = ref true;  (*specifies Auto mode: SPASS can use all inference rules*)
    7.21 +val prover = ref "spass";   (* use spass as default prover *)
    7.22  val custom_spass =   (*specialized options for SPASS*)
    7.23        ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
    7.24             "-DocProof","-TimeLimit=60"];
    7.25 @@ -130,8 +126,7 @@
    7.26  
    7.27  
    7.28  (*********************************************************************)
    7.29 -(* call SPASS with settings and problem file for the current subgoal *)
    7.30 -(* should be modified to allow other provers to be called            *)
    7.31 +(* call prover with settings and problem file for the current subgoal *)
    7.32  (*********************************************************************)
    7.33  (* now passing in list of skolemized thms and list of sgterms to go with them *)
    7.34  fun call_resolve_tac  (thms: thm list list)  sign (sg_terms:  term list) (childin, childout,pid) n  =
    7.35 @@ -152,12 +147,14 @@
    7.36              val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
    7.37              val _ = debug ("prob file in call_resolve_tac is " ^ probfile)
    7.38            in
    7.39 -            if !spass
    7.40 +            if !prover = "spass"
    7.41              then
    7.42 -              let val optionline = (*Custom SPASS options, or default?*)
    7.43 -		      if !full_spass (*Auto mode: all SPASS inference rules*)
    7.44 -                      then "-DocProof%-TimeLimit=60%-SOS"
    7.45 -                      else "-" ^ space_implode "%-" (!custom_spass)
    7.46 +              let val optionline = 
    7.47 +		      if !SpassComm.reconstruct 
    7.48 +		          (*Proof reconstruction works for only a limited set of 
    7.49 +		            inference rules*)
    7.50 +                      then "-" ^ space_implode "%-" (!custom_spass)
    7.51 +                      else "-DocProof%-TimeLimit=60%-SOS" (*Auto mode*)
    7.52                    val _ = debug ("SPASS option string is " ^ optionline)
    7.53                    val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    7.54                      (*We've checked that SPASS is there for ATP/spassshell to run.*)
    7.55 @@ -167,7 +164,7 @@
    7.56                       optionline, axfile, hypsfile, probfile)] @ 
    7.57                    (make_atp_list xs sign (n+1)))
    7.58                end
    7.59 -            else if !vampire 
    7.60 +            else if !prover = "vampire"
    7.61  	    then 
    7.62                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
    7.63                in
    7.64 @@ -175,14 +172,16 @@
    7.65                     axfile, hypsfile, probfile)] @
    7.66                   (make_atp_list xs sign (n+1)))
    7.67                end
    7.68 -      	     else
    7.69 -             let val Eprover = ResLib.helper_path "E_HOME" "eproof"
    7.70 -              in
    7.71 -                ([("E", thmstr, goalstring, Eprover, "--tptp-in -l5",
    7.72 -                   axfile, hypsfile, probfile)] @
    7.73 -                 (make_atp_list xs sign (n+1)))
    7.74 -              end
    7.75 -
    7.76 +      	     else if !prover = "E"
    7.77 +      	     then
    7.78 +	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
    7.79 +	       in
    7.80 +		  ([("E", thmstr, goalstring, Eprover, 
    7.81 +		     "--tptp-in%-l5%-xAuto%-tAuto%--soft-cpu-limit=60",
    7.82 +		     axfile, hypsfile, probfile)] @
    7.83 +		   (make_atp_list xs sign (n+1)))
    7.84 +	       end
    7.85 +	     else error ("Invalid prover name: " ^ !prover)
    7.86            end
    7.87  
    7.88      val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1
    7.89 @@ -205,15 +204,15 @@
    7.90          all_tac thm)
    7.91       else
    7.92  	
    7.93 -     ( SELECT_GOAL
    7.94 +      (SELECT_GOAL
    7.95          (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
    7.96            METAHYPS(fn negs => 
    7.97 -            (if !spass 
    7.98 +            (if !prover = "spass" 
    7.99               then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses
   7.100               else tptp_inputs_tfrees (make_clauses negs) n tfrees axclauses;
   7.101               get_sko_thms tfrees sign sg_terms (childin, childout, pid) 
   7.102 -                          thm  (n -1) (negs::sko_thms) axclauses; 
   7.103 -             all_tac))]) n thm )
   7.104 +                          thm (n-1) (negs::sko_thms) axclauses; 
   7.105 +             all_tac))]) n thm)
   7.106  
   7.107  
   7.108  
   7.109 @@ -223,36 +222,20 @@
   7.110  (* in proof reconstruction                    *)
   7.111  (**********************************************)
   7.112  
   7.113 -fun isar_atp_goal' thm n tfree_lits (childin, childout, pid)  axclauses =
   7.114 -  let
   7.115 -    val prems = Thm.prems_of thm
   7.116 -    (*val sg_term = get_nth k prems*)
   7.117 -    val sign = sign_of_thm thm
   7.118 -    val thmstring = string_of_thm thm
   7.119 +fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) axclauses =
   7.120 +  let val tfree_lits = isar_atp_h thms
   7.121 +      val prems = Thm.prems_of thm
   7.122 +      val sign = sign_of_thm thm
   7.123 +      val thmstring = string_of_thm thm
   7.124    in
   7.125 -    debug("in isar_atp_goal'");
   7.126 +    debug ("in isar_atp_aux");
   7.127      debug("thmstring in isar_atp_goal': " ^ thmstring);
   7.128      (* go and call callResProvers with this subgoal *)
   7.129      (* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
   7.130      (* recursive call to pick up the remaining subgoals *)
   7.131      (* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
   7.132 -    get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n []  axclauses
   7.133 -  end;
   7.134 -
   7.135 -
   7.136 -(**************************************************)
   7.137 -(* convert clauses from "assume" to conjecture.   *)
   7.138 -(* i.e. apply make_clauses and then get tptp for  *)
   7.139 -(* any hypotheses in the goal produced by assume  *)
   7.140 -(* statements;                                    *)
   7.141 -(* write to file "hyps"                           *)
   7.142 -(**************************************************)
   7.143 -
   7.144 -fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) axclauses =
   7.145 -  let val tfree_lits = isar_atp_h thms
   7.146 -  in
   7.147 -    debug ("in isar_atp_aux");
   7.148 -    isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid)  axclauses
   7.149 +    get_sko_thms tfree_lits sign prems (childin, childout, pid) 
   7.150 +                 thm n_subgoals []  axclauses
   7.151    end;
   7.152  
   7.153  (******************************************************************)
   7.154 @@ -270,7 +253,6 @@
   7.155        val thy = ProofContext.theory_of ctxt
   7.156        val prems = Thm.prems_of thm
   7.157        val thms_string = Meson.concat_with_and (map string_of_thm thms)
   7.158 -      val thm_string = string_of_thm thm
   7.159        val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
   7.160  
   7.161        (*set up variables for writing out the clasimps to a tptp file*)
   7.162 @@ -282,7 +264,6 @@
   7.163          string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
   7.164      in
   7.165        debug ("initial thms: " ^ thms_string);
   7.166 -      debug ("initial thm: " ^ thm_string);
   7.167        debug ("subgoals: " ^ prems_string);
   7.168        debug ("pid: "^ pid_string);
   7.169        isar_atp_aux thms thm (length prems) (childin, childout, pid) axclauses;