massive tidy-up and simplification
authorpaulson
Thu Sep 15 17:46:00 2005 +0200 (2005-09-15)
changeset 174223b237822985d
parent 17421 0382f6877b98
child 17423 de6b33a4efda
massive tidy-up and simplification
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
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Thu Sep 15 17:45:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Thu Sep 15 17:46:00 2005 +0200
     1.3 @@ -10,9 +10,9 @@
     1.4  signature SPASS_COMM =
     1.5    sig
     1.6      val reconstruct : bool ref
     1.7 -    val getSpassInput : TextIO.instream -> string * string * string
     1.8 +    val getSpassInput : TextIO.instream -> string * string
     1.9      val checkSpassProofFound:  
    1.10 -          TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
    1.11 +          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    1.12            string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
    1.13    end;
    1.14  
    1.15 @@ -30,7 +30,7 @@
    1.16  (*  steps as a string to the input pipe of the main Isabelle process  *)
    1.17  (**********************************************************************)
    1.18  
    1.19 -fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
    1.20 +fun reconstruct_tac proofextract goalstring toParent ppid sg_num 
    1.21                      clause_arr num_of_clauses = 
    1.22   let val f = if !reconstruct then Recon_Transfer.spassString_to_reconString
    1.23                               else Recon_Transfer.spassString_to_lemmaString
    1.24 @@ -38,12 +38,11 @@
    1.25     SELECT_GOAL
    1.26      (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
    1.27               METAHYPS(fn negs => 
    1.28 -    f proofextract thmstring goalstring 
    1.29 -              toParent ppid negs clause_arr num_of_clauses)]) sg_num	
    1.30 +    f proofextract goalstring toParent ppid negs clause_arr num_of_clauses)]) sg_num	
    1.31   end;
    1.32  
    1.33  
    1.34 -fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, 
    1.35 +fun transferSpassInput (fromChild, toParent, ppid, goalstring, 
    1.36                          currentString, thm, sg_num,clause_arr, num_of_clauses) = 
    1.37   let val thisLine = TextIO.inputLine fromChild 
    1.38   in 
    1.39 @@ -55,10 +54,10 @@
    1.40        let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    1.41        in 
    1.42  	  File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract;
    1.43 -	  reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
    1.44 +	  reconstruct_tac proofextract goalstring toParent ppid sg_num 
    1.45  	      clause_arr num_of_clauses thm
    1.46        end
    1.47 -    else transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,
    1.48 +    else transferSpassInput (fromChild, toParent, ppid, goalstring,
    1.49  			     (currentString^thisLine), thm, sg_num, clause_arr, 
    1.50  			     num_of_clauses)
    1.51   end;
    1.52 @@ -70,7 +69,7 @@
    1.53  (*********************************************************************************)
    1.54  
    1.55   
    1.56 -fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
    1.57 +fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd,
    1.58                          thm, sg_num,clause_arr, num_of_clauses) = 
    1.59     let val thisLine = TextIO.inputLine fromChild  
    1.60     in                 
    1.61 @@ -78,15 +77,15 @@
    1.62        else if String.isPrefix "Here is a proof" thisLine then     
    1.63  	 (File.append (File.tmp_path (Path.basic "spass_transfer"))
    1.64  		      ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n");
    1.65 -	  transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, 
    1.66 +	  transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine, 
    1.67   	                     thm, sg_num,clause_arr, num_of_clauses);
    1.68  	  true) handle EOF => false
    1.69 -      else startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,
    1.70 +      else startSpassTransfer (fromChild, toParent, ppid, goalstring,
    1.71                                 childCmd, thm, sg_num,clause_arr, num_of_clauses)
    1.72      end
    1.73  
    1.74  
    1.75 -fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd,
    1.76 +fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd,
    1.77                            thm, sg_num, clause_arr, (num_of_clauses:int )) = 
    1.78   let val spass_proof_file = TextIO.openAppend
    1.79             (File.platform_path(File.tmp_path (Path.basic "spass_proof")))
    1.80 @@ -101,7 +100,7 @@
    1.81       else if thisLine = "SPASS beiseite: Proof found.\n"
    1.82       then      
    1.83         (File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
    1.84 -	startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,
    1.85 +	startSpassTransfer (fromChild, toParent, ppid, goalstring,
    1.86  	                    childCmd, thm, sg_num, clause_arr, num_of_clauses))
    1.87       else if thisLine = "SPASS beiseite: Completion found.\n"
    1.88       then  
    1.89 @@ -113,7 +112,6 @@
    1.90  	TextIO.closeOut spass_proof_file;
    1.91  
    1.92  	TextIO.output (toParent, thisLine^"\n");
    1.93 -	TextIO.output (toParent, thmstring^"\n");
    1.94  	TextIO.output (toParent, goalstring^"\n");
    1.95  	TextIO.flushOut toParent;
    1.96  	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.97 @@ -124,7 +122,6 @@
    1.98       then  
    1.99         (File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
   1.100          TextIO.output (toParent, thisLine^"\n");
   1.101 -	TextIO.output (toParent, thmstring^"\n");
   1.102  	TextIO.output (toParent, goalstring^"\n");
   1.103  	TextIO.flushOut toParent;
   1.104  	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.105 @@ -144,7 +141,7 @@
   1.106      else
   1.107         (TextIO.output (spass_proof_file, thisLine);
   1.108         TextIO.flushOut spass_proof_file;
   1.109 -       checkSpassProofFound  (fromChild, toParent, ppid, thmstring,goalstring,
   1.110 +       checkSpassProofFound  (fromChild, toParent, ppid, goalstring,
   1.111         childCmd, thm, sg_num, clause_arr, num_of_clauses))
   1.112   end
   1.113  
   1.114 @@ -157,22 +154,20 @@
   1.115      let val thisLine = TextIO.inputLine instr 
   1.116          val _ = File.write (File.tmp_path (Path.basic "spass_line")) thisLine
   1.117      in 
   1.118 -      if thisLine = "" then ("No output from reconstruction process.\n","","")
   1.119 +      if thisLine = "" then ("No output from reconstruction process.\n","")
   1.120        else if String.sub (thisLine, 0) = #"[" orelse
   1.121           String.isPrefix "SPASS beiseite:" thisLine orelse
   1.122           String.isPrefix  "Rules from" thisLine
   1.123        then 
   1.124 -	let val thmstring = TextIO.inputLine instr 
   1.125 -	    val goalstring = TextIO.inputLine instr   
   1.126 -	in (thisLine, thmstring, goalstring) end
   1.127 +	let val goalstring = TextIO.inputLine instr   
   1.128 +	in (thisLine, goalstring) end
   1.129        else if substring (thisLine,0,5) = "Proof" orelse
   1.130                String.sub (thisLine, 0) = #"%"
   1.131        then
   1.132 -	let val thmstring = TextIO.inputLine instr
   1.133 -	    val goalstring = TextIO.inputLine instr
   1.134 +	let val goalstring = TextIO.inputLine instr
   1.135  	in
   1.136            File.write (File.tmp_path (Path.basic "getSpassInput")) thisLine;
   1.137 -          (thisLine, thmstring, goalstring)
   1.138 +          (thisLine, goalstring)
   1.139          end
   1.140        else getSpassInput instr
   1.141       end
     2.1 --- a/src/HOL/Tools/ATP/VampCommunication.ML	Thu Sep 15 17:45:17 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/VampCommunication.ML	Thu Sep 15 17:46:00 2005 +0200
     2.3 @@ -9,14 +9,14 @@
     2.4  (***************************************************************************)
     2.5  signature VAMP_COMM =
     2.6    sig
     2.7 -    val getEInput : TextIO.instream -> string * string * string
     2.8 +    val getEInput : TextIO.instream -> string * string
     2.9      val checkEProofFound: 
    2.10 -          TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
    2.11 +          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    2.12            string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
    2.13  
    2.14 -    val getVampInput : TextIO.instream -> string * string * string
    2.15 +    val getVampInput : TextIO.instream -> string * string
    2.16      val checkVampProofFound: 
    2.17 -          TextIO.instream * TextIO.outstream * Posix.Process.pid * string *
    2.18 +          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    2.19            string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
    2.20    end;
    2.21  
    2.22 @@ -31,13 +31,13 @@
    2.23  (*  steps as a string to the input pipe of the main Isabelle process  *)
    2.24  (**********************************************************************)
    2.25  
    2.26 -fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
    2.27 +fun reconstruct_tac proofextract goalstring toParent ppid sg_num 
    2.28                      clause_arr num_of_clauses =
    2.29      SELECT_GOAL
    2.30        (EVERY1
    2.31          [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
    2.32  	 METAHYPS(fn negs =>
    2.33 -		     (Recon_Transfer.proverString_to_lemmaString proofextract thmstring 
    2.34 +		     (Recon_Transfer.proverString_to_lemmaString proofextract  
    2.35  		       goalstring toParent ppid negs clause_arr num_of_clauses))]) sg_num
    2.36  
    2.37  
    2.38 @@ -47,7 +47,7 @@
    2.39  (*********************************************************************************)
    2.40  
    2.41  fun startTransfer (startS,endS)
    2.42 -      (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
    2.43 +      (fromChild, toParent, ppid, goalstring,childCmd,
    2.44         thm, sg_num,clause_arr, num_of_clauses) =
    2.45   let val thisLine = TextIO.inputLine fromChild
    2.46       fun transferInput currentString =
    2.47 @@ -63,7 +63,7 @@
    2.48  	then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    2.49  	     in
    2.50  	       File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; 
    2.51 -	       reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  
    2.52 +	       reconstruct_tac proofextract goalstring toParent ppid sg_num  
    2.53  			       clause_arr num_of_clauses thm
    2.54  	     end
    2.55  	else transferInput (currentString^thisLine)
    2.56 @@ -78,12 +78,12 @@
    2.57       true) handle EOF => false
    2.58     else
    2.59        startTransfer (startS,endS)
    2.60 -                    (fromChild, toParent, ppid, thmstring, goalstring,
    2.61 +                    (fromChild, toParent, ppid, goalstring,
    2.62  		     childCmd, thm, sg_num,clause_arr, num_of_clauses)
    2.63   end
    2.64  
    2.65  
    2.66 -fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, 
    2.67 +fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, 
    2.68                           thm, sg_num, clause_arr, num_of_clauses) =
    2.69   let val proof_file = TextIO.openAppend
    2.70  	   (File.platform_path(File.tmp_path (Path.basic "atp_proof")))
    2.71 @@ -99,7 +99,7 @@
    2.72       then
    2.73         (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
    2.74  	startTransfer (Recon_Parse.start_V6, Recon_Parse.end_V6)
    2.75 -	      (fromChild, toParent, ppid, thmstring, goalstring,
    2.76 +	      (fromChild, toParent, ppid, goalstring,
    2.77  	       childCmd, thm, sg_num, clause_arr, num_of_clauses))
    2.78       else if (thisLine = "% Unprovable.\n" ) orelse
    2.79               (thisLine = "% Proof not found. Time limit expired.\n")
    2.80 @@ -111,7 +111,6 @@
    2.81  	TextIO.closeOut proof_file;
    2.82   
    2.83  	TextIO.output (toParent, thisLine^"\n");
    2.84 -	TextIO.output (toParent, thmstring^"\n");
    2.85  	TextIO.output (toParent, goalstring^"\n");
    2.86  	TextIO.flushOut toParent;
    2.87  	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    2.88 @@ -121,16 +120,16 @@
    2.89       else
    2.90         (TextIO.output (proof_file, thisLine);
    2.91  	TextIO.flushOut proof_file;
    2.92 -	checkVampProofFound  (fromChild, toParent, ppid, thmstring,
    2.93 +	checkVampProofFound  (fromChild, toParent, ppid, 
    2.94  	   goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses))
    2.95    end
    2.96  
    2.97  
    2.98 -fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd,
    2.99 +fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd,
   2.100                        thm, sg_num, clause_arr, num_of_clauses) = 
   2.101   let val E_proof_file = TextIO.openAppend
   2.102 -	   (File.platform_path(File.tmp_path (Path.basic "eprover_proof")))
   2.103 -     val _ = File.write (File.tmp_path (Path.basic "eprover_checking_prf"))
   2.104 +	   (File.platform_path(File.tmp_path (Path.basic "atp_proof")))
   2.105 +     val _ = File.write (File.tmp_path (Path.basic "atp_checking_prf"))
   2.106  			("checking if proof found, thm is: " ^ string_of_thm thm)
   2.107       val thisLine = TextIO.inputLine fromChild  
   2.108   in   
   2.109 @@ -140,20 +139,19 @@
   2.110  	    false)
   2.111       else if thisLine = "# TSTP exit status: Unsatisfiable\n"
   2.112       then      
   2.113 -       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
   2.114 +       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
   2.115         startTransfer (Recon_Parse.start_E, Recon_Parse.end_E)
   2.116 -             (fromChild, toParent, ppid, thmstring, goalstring,
   2.117 +             (fromChild, toParent, ppid, goalstring,
   2.118  	      childCmd, thm, sg_num, clause_arr, num_of_clauses))
   2.119       else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n"
   2.120       then  
   2.121 -       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
   2.122 +       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
   2.123  	TextIO.output (toParent,childCmd^"\n" );
   2.124  	TextIO.flushOut toParent;
   2.125  	TextIO.output (E_proof_file, thisLine);
   2.126  	TextIO.closeOut E_proof_file;
   2.127  
   2.128  	TextIO.output (toParent, thisLine^"\n");
   2.129 -	TextIO.output (toParent, thmstring^"\n");
   2.130  	TextIO.output (toParent, goalstring^"\n");
   2.131  	TextIO.flushOut toParent;
   2.132  	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.133 @@ -162,9 +160,8 @@
   2.134  	 true)
   2.135       else if thisLine = "# Failure: Resource limit exceeded (time)\n" 
   2.136       then  
   2.137 -       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
   2.138 +       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
   2.139  	TextIO.output (toParent, thisLine^"\n");
   2.140 -	TextIO.output (toParent, thmstring^"\n");
   2.141  	TextIO.output (toParent, goalstring^"\n");
   2.142  	TextIO.flushOut toParent;
   2.143  	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.144 @@ -184,7 +181,7 @@
   2.145       else
   2.146  	(TextIO.output (E_proof_file, thisLine);
   2.147  	TextIO.flushOut E_proof_file;
   2.148 -	checkEProofFound  (fromChild, toParent, ppid, thmstring,goalstring,
   2.149 +	checkEProofFound  (fromChild, toParent, ppid, goalstring,
   2.150  	childCmd, thm, sg_num, clause_arr, num_of_clauses))
   2.151   end
   2.152  
   2.153 @@ -197,21 +194,19 @@
   2.154      let val thisLine = TextIO.inputLine instr
   2.155  	val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
   2.156      in    (* reconstructed proof string *)
   2.157 -      if thisLine = "" then ("No output from reconstruction process.\n","","")
   2.158 +      if thisLine = "" then ("No output from reconstruction process.\n","")
   2.159        else if String.sub (thisLine, 0) = #"[" orelse
   2.160                thisLine = "% Unprovable.\n" orelse
   2.161                thisLine ="% Proof not found. Time limit expired.\n" orelse
   2.162                String.isPrefix "Rules from" thisLine
   2.163        then
   2.164 -	let val thmstring = TextIO.inputLine instr
   2.165 -	    val goalstring = TextIO.inputLine instr
   2.166 -	in (thisLine, thmstring, goalstring) end
   2.167 +	let val goalstring = TextIO.inputLine instr
   2.168 +	in (thisLine, goalstring) end
   2.169        else if thisLine = "Proof found but translation failed!"
   2.170        then
   2.171 -	 let val thmstring = TextIO.inputLine instr
   2.172 -	     val goalstring = TextIO.inputLine instr
   2.173 +	 let val goalstring = TextIO.inputLine instr
   2.174  	     val _ = debug "getVampInput: translation of proof failed"
   2.175 -	 in (thisLine, thmstring, goalstring) end
   2.176 +	 in (thisLine, goalstring) end
   2.177        else getVampInput instr
   2.178      end
   2.179  
   2.180 @@ -224,20 +219,18 @@
   2.181      let val thisLine = TextIO.inputLine instr
   2.182  	val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
   2.183      in    (* reconstructed proof string *)
   2.184 -      if thisLine = "" then ("No output from reconstruction process.\n","","")
   2.185 +      if thisLine = "" then ("No output from reconstruction process.\n","")
   2.186        else if String.isPrefix "# Problem is satisfiable" thisLine orelse
   2.187                String.isPrefix "# Cannot determine problem status" thisLine orelse
   2.188                String.isPrefix "# Failure:" thisLine
   2.189        then
   2.190 -	let val thmstring = TextIO.inputLine instr
   2.191 -	    val goalstring = TextIO.inputLine instr
   2.192 -	in (thisLine, thmstring, goalstring) end
   2.193 +	let val goalstring = TextIO.inputLine instr
   2.194 +	in (thisLine, goalstring) end
   2.195        else if thisLine = "Proof found but translation failed!"
   2.196        then
   2.197 -	 let val thmstring = TextIO.inputLine instr
   2.198 -	     val goalstring = TextIO.inputLine instr
   2.199 +	 let val goalstring = TextIO.inputLine instr
   2.200  	     val _ = debug "getEInput: translation of proof failed"
   2.201 -	 in (thisLine, thmstring, goalstring) end
   2.202 +	 in (thisLine, goalstring) end
   2.203        else getEInput instr
   2.204      end
   2.205  
     3.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Thu Sep 15 17:45:17 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Thu Sep 15 17:46:00 2005 +0200
     3.3 @@ -118,6 +118,8 @@
     3.4  val end_E   = "# Proof object ends here."
     3.5  val start_V6 = "%================== Proof: ======================"
     3.6  val end_V6   = "%==============  End of proof. =================="
     3.7 +val start_V8 = "=========== Refutation =========="
     3.8 +val end_V8 = "======= End of refutation ======="
     3.9  
    3.10  
    3.11  (*Identifies the start/end lines of an ATP's output*)
     4.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 15 17:45:17 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 15 17:46:00 2005 +0200
     4.3 @@ -134,9 +134,6 @@
     4.4  (*Flattens a list of list of strings to one string*)
     4.5  fun onestr ls = String.concat (map String.concat ls);
     4.6  
     4.7 -fun thmstrings [] str = str
     4.8 -|   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
     4.9 -
    4.10  fun is_clasimp_ax clasimp_num n = n <= clasimp_num 
    4.11  
    4.12  fun subone x = x - 1
    4.13 @@ -268,10 +265,9 @@
    4.14  val restore_linebreaks = subst_for #"\t" #"\n";
    4.15  
    4.16  
    4.17 -fun proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses getax = 
    4.18 - let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
    4.19 -               ("thmstring is " ^ thmstring ^ 
    4.20 -                "\nproofstr is " ^ proofstr ^
    4.21 +fun proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms clause_arr num_of_clauses getax = 
    4.22 + let val _ = File.append(File.tmp_path (Path.basic "spass_lemmastring"))
    4.23 +               ("proofstr is " ^ proofstr ^
    4.24                  "\ngoalstr is " ^ goalstring ^
    4.25                  "\nnum of clauses is " ^ string_of_int num_of_clauses)
    4.26  
    4.27 @@ -279,11 +275,10 @@
    4.28       val ax_str = "Rules from clasimpset used in automatic proof: " ^
    4.29                    rules_to_string axiom_names
    4.30      in 
    4.31 -	 File.append(File.tmp_path (Path.basic "reconstrfile"))
    4.32 +	 File.append(File.tmp_path (Path.basic "spass_lemmastring"))
    4.33  	            ("reconstring is: "^ax_str^"  "^goalstring);
    4.34           TextIO.output (toParent, ax_str^"\n");
    4.35  	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
    4.36 -	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
    4.37  	 TextIO.flushOut toParent;
    4.38  
    4.39  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    4.40 @@ -294,29 +289,28 @@
    4.41       (File.write(File.tmp_path (Path.basic "proverString_handler")) "In exception handler";
    4.42        TextIO.output (toParent, "Proof found but translation failed : " ^ 
    4.43                       remove_linebreaks proofstr ^ "\n");
    4.44 -      TextIO.output (toParent, remove_linebreaks thmstring ^ "\n");
    4.45        TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
    4.46        TextIO.flushOut toParent;
    4.47        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    4.48        (* Attempt to prevent several signals from turning up simultaneously *)
    4.49        Posix.Process.sleep(Time.fromSeconds 1); all_tac);
    4.50  
    4.51 -fun proverString_to_lemmaString proofstr thmstring goalstring toParent ppid thms
    4.52 +fun proverString_to_lemmaString proofstr goalstring toParent ppid thms
    4.53        clause_arr num_of_clauses  = 
    4.54 -  proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms        
    4.55 +  proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms        
    4.56         clause_arr num_of_clauses get_axiom_names_vamp_E;
    4.57  
    4.58 -fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms
    4.59 +fun spassString_to_lemmaString proofstr goalstring toParent ppid thms
    4.60        clause_arr  num_of_clauses  = 
    4.61 -  proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms        
    4.62 +  proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms        
    4.63         clause_arr num_of_clauses get_axiom_names_spass;
    4.64  
    4.65  
    4.66  (**** Full proof reconstruction for SPASS (not really working) ****)
    4.67  
    4.68 -fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    4.69 -  let val _ = File.write(File.tmp_path (Path.basic "thmstringfile")) 
    4.70 -                 (" thmstring is: "^thmstring^"proofstr is: "^proofstr)
    4.71 +fun spassString_to_reconString proofstr goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    4.72 +  let val _ = File.write(File.tmp_path (Path.basic "spass_reconstruction")) 
    4.73 +                 ("proofstr is: "^proofstr)
    4.74        val tokens = #1(lex proofstr)
    4.75  
    4.76    (***********************************)
    4.77 @@ -324,11 +318,9 @@
    4.78    (***********************************)
    4.79        val proof_steps = parse tokens
    4.80  
    4.81 -      val _ = File.write (File.tmp_path (Path.basic "foo_parse"))
    4.82 +      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))
    4.83                        ("Did parsing on "^proofstr)
    4.84      
    4.85 -      val _ = File.write (File.tmp_path (Path.basic "foo_thmstring_at_parse"))
    4.86 -                                ("Parsing for thmstring: "^thmstring)
    4.87    (************************************)
    4.88    (* recreate original subgoal as thm *)
    4.89    (************************************)
    4.90 @@ -340,16 +332,16 @@
    4.91        val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
    4.92        
    4.93        (*val numcls_string = numclstr ( vars, numcls) ""*)
    4.94 -      val _ = File.write (File.tmp_path (Path.basic "foo_axiom")) "got axioms"
    4.95 +      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction")) "got axioms"
    4.96  	
    4.97    (************************************)
    4.98    (* translate proof                  *)
    4.99    (************************************)
   4.100 -      val _ = File.write (File.tmp_path (Path.basic "foo_steps"))                                                                           
   4.101 +      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))                                                                           
   4.102                         ("about to translate proof, steps: "
   4.103                         ^(init_proofsteps_to_string proof_steps ""))
   4.104        val (newthm,proof) = translate_proof numcls  proof_steps vars
   4.105 -      val _ = File.write (File.tmp_path (Path.basic "foo_steps2"))                                                                       
   4.106 +      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))                                                                       
   4.107                         ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
   4.108    (***************************************************)
   4.109    (* transfer necessary steps as strings to Isabelle *)
   4.110 @@ -372,9 +364,6 @@
   4.111        val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   4.112    in 
   4.113         TextIO.output (toParent, reconstr^"\n");
   4.114 -       TextIO.flushOut toParent;
   4.115 -       TextIO.output (toParent, thmstring^"\n");
   4.116 -       TextIO.flushOut toParent;
   4.117         TextIO.output (toParent, goalstring^"\n");
   4.118         TextIO.flushOut toParent;
   4.119  
   4.120 @@ -383,19 +372,14 @@
   4.121         Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   4.122    end
   4.123    handle _ => 
   4.124 -  let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   4.125 -  in 
   4.126 -       TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^(remove_linebreaks proofstr) ^"\n");
   4.127 -      TextIO.flushOut toParent;
   4.128 -    TextIO.output (toParent, thmstring^"\n");
   4.129 -       TextIO.flushOut toParent;
   4.130 -       TextIO.output (toParent, goalstring^"\n");
   4.131 -       TextIO.flushOut toParent;
   4.132 -      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.133 -      (* Attempt to prevent several signals from turning up simultaneously *)
   4.134 -      Posix.Process.sleep(Time.fromSeconds 1); all_tac
   4.135 -  end
   4.136 -
   4.137 +   (File.append(File.tmp_path (Path.basic "spass_reconstruction")) "In exception handler";
   4.138 +    TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^
   4.139 +         (remove_linebreaks proofstr) ^"\n");
   4.140 +    TextIO.output (toParent, goalstring^"\n");
   4.141 +    TextIO.flushOut toParent;
   4.142 +    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.143 +    (* Attempt to prevent several signals from turning up simultaneously *)
   4.144 +    Posix.Process.sleep(Time.fromSeconds 1); all_tac)
   4.145  
   4.146  (**********************************************************************************)
   4.147  (* At other end, want to turn back into datatype so can apply reconstruct_proof.  *)
     5.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Sep 15 17:45:17 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Sep 15 17:46:00 2005 +0200
     5.3 @@ -23,7 +23,7 @@
     5.4  (*****************************************************************************************)
     5.5  
     5.6  val callResProvers :
     5.7 -    TextIO.outstream * (string*string*string*string*string*string*string*string) list 
     5.8 +    TextIO.outstream * (string*string*string*string*string) list 
     5.9      -> unit
    5.10  
    5.11  (************************************************************************)
    5.12 @@ -73,7 +73,6 @@
    5.13  datatype cmdproc = CMDPROC of {
    5.14          prover: string,             (* Name of the resolution prover used, e.g. Vampire, SPASS *)
    5.15          cmd:  string,              (* The file containing the goal for res prover to prove *)     
    5.16 -        thmstring: string,         (* string representation of subgoal after negation, skolemization*) 
    5.17          goalstring: string,         (* string representation of subgoal*) 
    5.18          proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    5.19          instr : TextIO.instream,   (*  Input stream to child process *)
    5.20 @@ -123,19 +122,16 @@
    5.21  
    5.22  fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
    5.23  
    5.24 -fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = 
    5.25 +fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) = 
    5.26    (prover,(cmd, (instr,outstr)));
    5.27  
    5.28 -fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = 
    5.29 +fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  = 
    5.30    proc_handle;
    5.31  
    5.32 -fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  =
    5.33 +fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
    5.34    prover;
    5.35  
    5.36 -fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = 
    5.37 -  thmstring;
    5.38 -
    5.39 -fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  =
    5.40 +fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
    5.41    goalstring;
    5.42  
    5.43  
    5.44 @@ -166,14 +162,14 @@
    5.45  fun callResProvers (toWatcherStr,  []) = 
    5.46        (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
    5.47  |   callResProvers (toWatcherStr,
    5.48 -                    (prover,thmstring,goalstring, proverCmd,settings, 
    5.49 -                     axfile, hypsfile,probfile)  ::  args) =
    5.50 +                    (prover,goalstring, proverCmd,settings, 
    5.51 +                     probfile)  ::  args) =
    5.52        let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
    5.53 -                             (prover^thmstring^goalstring^proverCmd^settings^
    5.54 -                              hypsfile^probfile)
    5.55 +                             (prover^goalstring^proverCmd^settings^
    5.56 +                              probfile)
    5.57        in TextIO.output (toWatcherStr,    
    5.58 -            (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^
    5.59 -             settings^"$"^hypsfile^"$"^probfile^"\n"));
    5.60 +            (prover^"$"^goalstring^"$"^proverCmd^"$"^
    5.61 +             settings^"$"^probfile^"\n"));
    5.62           goals_being_watched := (!goals_being_watched) + 1;
    5.63  	 TextIO.flushOut toWatcherStr;
    5.64  	 callResProvers (toWatcherStr,args)
    5.65 @@ -198,68 +194,52 @@
    5.66  fun separateFields str =
    5.67    let val _ = File.append (File.tmp_path (Path.basic "sep_field"))
    5.68                            ("In separateFields, str is: " ^ str ^ "\n\n") 
    5.69 -      val [prover,thmstring,goalstring,proverCmd,settingstr,hypsfile,probfile] = 
    5.70 +      val [prover,goalstring,proverCmd,settingstr,probfile] = 
    5.71            String.tokens (fn c => c = #"$") str
    5.72        val settings = String.tokens (fn c => c = #"%") settingstr
    5.73        val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
    5.74                    ("Sep comms are: "^ str ^"**"^
    5.75 -                   prover^" thmstring: "^thmstring^"\n goalstr:  "^goalstring^
    5.76 -                   " \n provercmd: "^proverCmd^
    5.77 -                   " \n hyps "^hypsfile^"\n prob  "^probfile^"\n\n")
    5.78 +                   prover^" goalstr:  "^goalstring^
    5.79 +                   "\n provercmd: "^proverCmd^
    5.80 +                   "\n prob  "^probfile^"\n\n")
    5.81    in
    5.82 -     (prover,thmstring,goalstring, proverCmd, settings, hypsfile, probfile)
    5.83 +     (prover,goalstring, proverCmd, settings, probfile)
    5.84    end
    5.85  
    5.86 -                      
    5.87 -fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, hypsfile ,probfile) = 
    5.88 -  let
    5.89 -    val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
    5.90 -	       (thmstring ^ "\n goals_watched" ^ 
    5.91 -	       (string_of_int(!goals_being_watched)) ^ probfile^"\n")
    5.92 -  in
    5.93 -    (prover, thmstring, goalstring, proverCmd, settings, probfile)	
    5.94 -  end;
    5.95 -
    5.96  val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
    5.97  
    5.98  fun getCmd cmdStr = 
    5.99    let val cmdStr' = remove_newlines cmdStr
   5.100    in
   5.101        File.write (File.tmp_path (Path.basic"sepfields_call")) 
   5.102 -		 ("about to call sepfields with " ^ cmdStr');
   5.103 -      formatCmd (separateFields cmdStr')
   5.104 +		 ("about to call separateFields with " ^ cmdStr');
   5.105 +      separateFields cmdStr'
   5.106    end;
   5.107                        
   5.108 -
   5.109 -fun getProofCmd (a,b,c,d,e,f) = d
   5.110 -
   5.111 -                        
   5.112  (**************************************************************)
   5.113  (* Get commands from Isabelle                                 *)
   5.114  (**************************************************************)
   5.115 -(* FIX: or perhaps do the tptp2x stuff here - so it's get commands and then format them, before passing them to spass *)
   5.116  
   5.117  fun getCmds (toParentStr,fromParentStr, cmdList) = 
   5.118    let val thisLine = TextIO.inputLine fromParentStr 
   5.119        val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
   5.120    in
   5.121 -     if (thisLine = "End of calls\n") 
   5.122 -     then cmdList
   5.123 -     else if (thisLine = "Kill children\n") 
   5.124 +     if thisLine = "End of calls\n" then cmdList
   5.125 +     else if thisLine = "Kill children\n"
   5.126       then 
   5.127  	 (   TextIO.output (toParentStr,thisLine ); 
   5.128  	     TextIO.flushOut toParentStr;
   5.129 -	   (("","","","Kill children",[],"")::cmdList)
   5.130 +	   (("","","Kill children",[],"")::cmdList)
   5.131  	  )
   5.132 -     else  let val thisCmd = getCmd thisLine 
   5.133 +     else let val thisCmd = getCmd thisLine 
   5.134  	       (*********************************************************)
   5.135 -	       (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   5.136 +	       (* thisCmd = (prover,proverCmd, settings, file)*)
   5.137  	       (* i.e. put back into tuple format                       *)
   5.138  	       (*********************************************************)
   5.139  	   in
   5.140  	     (*TextIO.output (toParentStr, thisCmd); 
   5.141  	       TextIO.flushOut toParentStr;*)
   5.142 -	       getCmds (toParentStr, fromParentStr, (thisCmd::cmdList))
   5.143 +	       getCmds (toParentStr, fromParentStr, thisCmd::cmdList)
   5.144  	   end
   5.145    end
   5.146  	    
   5.147 @@ -286,6 +266,8 @@
   5.148  (*  Set up a Watcher Process         *)
   5.149  (*************************************)
   5.150  
   5.151 +fun getProofCmd (a,c,d,e,f) = d
   5.152 +
   5.153  fun setupWatcher (thm,clause_arr, num_of_clauses) = 
   5.154    let
   5.155      (** pipes for communication between parent and watcher **)
   5.156 @@ -405,25 +387,24 @@
   5.157  			      ("finished polling child \n")
   5.158  		   val parentID = Posix.ProcEnv.getppid()
   5.159  		   val prover = cmdProver childProc
   5.160 -		   val thmstring = cmdThm childProc
   5.161  		   val sign = sign_of_thm thm
   5.162  		   val prems = prems_of thm
   5.163  		   val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   5.164  		   val _ = debug("subgoals forked to checkChildren: "^prems_string)
   5.165  		   val goalstring = cmdGoal childProc							
   5.166  		   val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
   5.167 -			      (prover^thmstring^goalstring^childCmd^"\n")
   5.168 +			      (prover^goalstring^childCmd^"\n")
   5.169  	       in 
   5.170  		 if isSome childIncoming
   5.171  		 then 
   5.172  		   (* check here for prover label on child*)
   5.173  		   let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) 
   5.174  			      ("subgoals forked to checkChildren:"^
   5.175 -			      prems_string^prover^thmstring^goalstring^childCmd) 
   5.176 +			      prems_string^prover^goalstring^childCmd) 
   5.177  		       val childDone = (case prover of
   5.178 -			   "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  
   5.179 -			    | "E" => VampComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
   5.180 -			  |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  )
   5.181 +			   "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  
   5.182 +			    | "E" => VampComm.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
   5.183 +			  |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  )
   5.184  		    in
   5.185  		     if childDone      (**********************************************)
   5.186  		     then (* child has found a proof and transferred it *)
   5.187 @@ -453,7 +434,7 @@
   5.188  
   5.189  (*** add subgoal id num to this *)
   5.190  	fun execCmds  [] procList = procList
   5.191 -	|   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =
   5.192 +	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   5.193  	      let val _ = File.write (File.tmp_path (Path.basic "exec_child"))  
   5.194  	                    (space_implode "\n" 
   5.195  	                      (["About to execute command for goal:",
   5.196 @@ -466,7 +447,6 @@
   5.197  		  val newProcList = (CMDPROC{
   5.198  				       prover = prover,
   5.199  				       cmd = file,
   5.200 -				       thmstring = thmstring,
   5.201  				       goalstring = goalstring,
   5.202  				       proc_handle = childhandle,
   5.203  				       instr = instr,
   5.204 @@ -488,11 +468,11 @@
   5.205       (****************************************)
   5.206  
   5.207        (*  fun execRemoteCmds  [] procList = procList
   5.208 -	|   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   5.209 -				  let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   5.210 -				      in
   5.211 -					   execRemoteCmds  cmds newProcList
   5.212 -				      end
   5.213 +	|   execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList  =  
   5.214 +	      let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   5.215 +		  in
   5.216 +		       execRemoteCmds  cmds newProcList
   5.217 +		  end
   5.218  *)
   5.219  
   5.220       (**********************************************)                  
   5.221 @@ -648,11 +628,11 @@
   5.222  	(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   5.223  	 VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))               
   5.224       fun spass_proofHandler n = (
   5.225 -       let val _ = File.append (File.tmp_path (Path.basic "spass_signal_in"))
   5.226 +       let val _ = File.append (File.tmp_path (Path.basic "spass_signal"))
   5.227                                 "Starting SPASS signal handler\n"
   5.228 -	   val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
   5.229 -	   val _ = File.append (File.tmp_path (Path.basic "spass_signal_out"))
   5.230 -		       ("In SPASS signal handler "^reconstr^thmstring^goalstring^
   5.231 +	   val (reconstr, goalstring) = SpassComm.getSpassInput childin
   5.232 +	   val _ = File.append (File.tmp_path (Path.basic "spass_signal"))
   5.233 +		       ("In SPASS signal handler "^reconstr^goalstring^
   5.234  		       "goals_being_watched: "^ string_of_int (!goals_being_watched))
   5.235         in (* if a proof has been found and sent back as a reconstruction proof *)
   5.236  	 if substring (reconstr, 0,1) = "["
     6.1 --- a/src/HOL/Tools/res_atp.ML	Thu Sep 15 17:45:17 2005 +0200
     6.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Sep 15 17:46:00 2005 +0200
     6.3 @@ -7,7 +7,6 @@
     6.4  
     6.5  signature RES_ATP =
     6.6  sig
     6.7 -  val axiom_file : Path.T
     6.8    val prover: string ref
     6.9    val custom_spass: string list ref
    6.10    val hook_count: int ref
    6.11 @@ -27,8 +26,6 @@
    6.12        ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
    6.13             "-DocProof","-TimeLimit=60"];
    6.14  
    6.15 -val axiom_file = File.tmp_path (Path.basic "axioms");
    6.16 -val hyps_file = File.tmp_path (Path.basic "hyps");
    6.17  val prob_file = File.tmp_path (Path.basic "prob");
    6.18  
    6.19  
    6.20 @@ -58,42 +55,18 @@
    6.21  
    6.22  
    6.23  (*********************************************************************)
    6.24 -(* convert clauses from "assume" to conjecture. write to file "hyps" *)
    6.25 -(* hypotheses of the goal currently being proved                     *)
    6.26 -(*********************************************************************)
    6.27 -(*perhaps have 2 different versions of this, depending on whether or not spass is set *)
    6.28 -fun isar_atp_h thms =
    6.29 -    let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
    6.30 -        val prems' = map repeat_someI_ex prems
    6.31 -        val prems'' = make_clauses prems'
    6.32 -        val prems''' = ResAxioms.rm_Eps [] prems''
    6.33 -        val clss = map ResClause.make_conjecture_clause prems'''
    6.34 -	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
    6.35 -	val tfree_lits = ResLib.flat_noDup tfree_litss
    6.36 -        (* tfree clause is different in tptp and dfg versions *)
    6.37 -	val tfree_clss = map ResClause.tfree_clause tfree_lits 
    6.38 -        val hypsfile = File.platform_path hyps_file
    6.39 -        val out = TextIO.openOut(hypsfile)
    6.40 -    in
    6.41 -        ResLib.writeln_strs out (tfree_clss @ tptp_clss);
    6.42 -        TextIO.closeOut out; debug hypsfile;
    6.43 -        tfree_lits
    6.44 -    end;
    6.45 -
    6.46 -
    6.47 -(*********************************************************************)
    6.48  (* write out a subgoal as tptp clauses to the file "probN"           *)
    6.49  (* where N is the number of this subgoal                             *)
    6.50  (*********************************************************************)
    6.51  
    6.52 -fun tptp_inputs_tfrees thms n tfrees axclauses =
    6.53 +fun tptp_inputs_tfrees thms n axclauses =
    6.54      let
    6.55        val _ = debug ("in tptp_inputs_tfrees 0")
    6.56        val clss = map (ResClause.make_conjecture_clause_thm) thms
    6.57        val _ = debug ("in tptp_inputs_tfrees 1")
    6.58        val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    6.59        val _ = debug ("in tptp_inputs_tfrees 2")
    6.60 -      val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees)
    6.61 +      val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss)
    6.62        val _ = debug ("in tptp_inputs_tfrees 3")
    6.63        val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
    6.64        val out = TextIO.openOut(probfile)
    6.65 @@ -110,14 +83,12 @@
    6.66  (* where N is the number of this subgoal                             *)
    6.67  (*********************************************************************)
    6.68  
    6.69 -fun dfg_inputs_tfrees thms n tfrees axclauses = 
    6.70 +fun dfg_inputs_tfrees thms n axclauses = 
    6.71      let val clss = map (ResClause.make_conjecture_clause_thm) thms
    6.72          val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    6.73          val _ = debug ("about to write out dfg prob file " ^ probfile)
    6.74 -       	(*val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
    6.75 -        val tfree_clss = map ResClause.tfree_dfg_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) *)   
    6.76          val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
    6.77 -                        axclauses [] [] [] tfrees   
    6.78 +                        axclauses [] [] []    
    6.79  	val out = TextIO.openOut(probfile)
    6.80      in
    6.81  	(ResLib.writeln_strs out [probN]; TextIO.closeOut out; debug probfile )
    6.82 @@ -129,23 +100,16 @@
    6.83  (* call prover with settings and problem file for the current subgoal *)
    6.84  (*********************************************************************)
    6.85  (* now passing in list of skolemized thms and list of sgterms to go with them *)
    6.86 -fun call_resolve_tac  (thms: thm list list)  sign (sg_terms:  term list) (childin, childout,pid) n  =
    6.87 +fun watcher_call_provers sign sg_terms (childin, childout,pid) =
    6.88    let
    6.89 -    val axfile = (File.platform_path axiom_file)
    6.90 -
    6.91 -    val hypsfile = (File.platform_path hyps_file)
    6.92 -
    6.93 -    fun make_atp_list [] sign n = []
    6.94 -      | make_atp_list ((sko_thm, sg_term)::xs) sign n =
    6.95 +    fun make_atp_list [] n = []
    6.96 +      | make_atp_list ((sg_term)::xs) n =
    6.97            let
    6.98 -            val thmstr = proofstring (Meson.concat_with_and (map string_of_thm sko_thm))
    6.99 -            val _ = debug ("thmstring in make_atp_lists is " ^ thmstr)
   6.100 -
   6.101              val goalstring = proofstring (Sign.string_of_term sign sg_term)
   6.102              val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
   6.103  
   6.104              val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
   6.105 -            val _ = debug ("prob file in call_resolve_tac is " ^ probfile)
   6.106 +            val _ = debug ("prob file in watcher_call_provers is " ^ probfile)
   6.107            in
   6.108              (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
   6.109                versions of Unix.execute treat them differently!*)
   6.110 @@ -161,93 +125,60 @@
   6.111                    val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
   6.112                      (*We've checked that SPASS is there for ATP/spassshell to run.*)
   6.113                in 
   6.114 -                  ([("spass", thmstr, goalstring,
   6.115 +                  ([("spass", goalstring,
   6.116                       getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
   6.117 -                     optionline, axfile, hypsfile, probfile)] @ 
   6.118 -                  (make_atp_list xs sign (n+1)))
   6.119 +                     optionline, probfile)] @ 
   6.120 +                  (make_atp_list xs (n+1)))
   6.121                end
   6.122              else if !prover = "vampire"
   6.123  	    then 
   6.124                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
   6.125                in
   6.126 -                ([("vampire", thmstr, goalstring, vampire, "-t60%-m100000",
   6.127 -                   axfile, hypsfile, probfile)] @
   6.128 -                 (make_atp_list xs sign (n+1)))
   6.129 +                ([("vampire", goalstring, vampire, "-t60%-m100000",
   6.130 +                   probfile)] @
   6.131 +                 (make_atp_list xs (n+1)))
   6.132                end
   6.133        	     else if !prover = "E"
   6.134        	     then
   6.135  	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
   6.136  	       in
   6.137 -		  ([("E", thmstr, goalstring, Eprover, 
   6.138 +		  ([("E", goalstring, Eprover, 
   6.139  		     "--tptp-in%-l5%-xAuto%-tAuto%--soft-cpu-limit=60",
   6.140 -		     axfile, hypsfile, probfile)] @
   6.141 -		   (make_atp_list xs sign (n+1)))
   6.142 +		     probfile)] @
   6.143 +		   (make_atp_list xs (n+1)))
   6.144  	       end
   6.145  	     else error ("Invalid prover name: " ^ !prover)
   6.146            end
   6.147  
   6.148 -    val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1
   6.149 +    val atp_list = make_atp_list sg_terms 1
   6.150    in
   6.151      Watcher.callResProvers(childout,atp_list);
   6.152 -    debug "Sent commands to watcher!";
   6.153 -    all_tac
   6.154 +    debug "Sent commands to watcher!"
   6.155    end
   6.156  
   6.157 -(**********************************************************)
   6.158 -(* write out the current subgoal as a tptp file, probN,   *)
   6.159 -(* then call all_tac - should be call_res_tac           *)
   6.160 -(**********************************************************)
   6.161 -
   6.162 -
   6.163 -fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms axclauses =
   6.164 -    if n=0 then 
   6.165 -       (call_resolve_tac  (rev sko_thms)
   6.166 -        sign  sg_terms (childin, childout, pid) (List.length sg_terms);
   6.167 -        all_tac thm)
   6.168 +(*We write out problem files for each subgoal, but work is repeated (skolemize)*)
   6.169 +fun write_problem_files axclauses thm n =
   6.170 +    if n=0 then ()
   6.171       else
   6.172 -	
   6.173 -      (SELECT_GOAL
   6.174 +       (SELECT_GOAL
   6.175          (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
   6.176            METAHYPS(fn negs => 
   6.177              (if !prover = "spass" 
   6.178 -             then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses
   6.179 -             else tptp_inputs_tfrees (make_clauses negs) n tfrees axclauses;
   6.180 -             get_sko_thms tfrees sign sg_terms (childin, childout, pid) 
   6.181 -                          thm (n-1) (negs::sko_thms) axclauses; 
   6.182 -             all_tac))]) n thm)
   6.183 -
   6.184 -
   6.185 -
   6.186 -(**********************************************)
   6.187 -(* recursively call atp_tac_g on all subgoals *)
   6.188 -(* sg_term is the nth subgoal as a term - used*)
   6.189 -(* in proof reconstruction                    *)
   6.190 -(**********************************************)
   6.191 +             then dfg_inputs_tfrees (make_clauses negs) n axclauses
   6.192 +             else tptp_inputs_tfrees (make_clauses negs) n axclauses;
   6.193 +             write_problem_files axclauses thm (n-1); 
   6.194 +             all_tac))]) n thm;
   6.195 +        ());
   6.196  
   6.197 -fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) axclauses =
   6.198 -  let val tfree_lits = isar_atp_h thms
   6.199 -      val prems = Thm.prems_of thm
   6.200 -      val sign = sign_of_thm thm
   6.201 -      val thmstring = string_of_thm thm
   6.202 -  in
   6.203 -    debug ("in isar_atp_aux");
   6.204 -    debug("thmstring in isar_atp_goal': " ^ thmstring);
   6.205 -    (* go and call callResProvers with this subgoal *)
   6.206 -    (* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
   6.207 -    (* recursive call to pick up the remaining subgoals *)
   6.208 -    (* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
   6.209 -    get_sko_thms tfree_lits sign prems (childin, childout, pid) 
   6.210 -                 thm n_subgoals []  axclauses
   6.211 -  end;
   6.212  
   6.213  (******************************************************************)
   6.214  (* called in Isar automatically                                   *)
   6.215  (* writes out the current clasimpset to a tptp file               *)
   6.216 -(* passes all subgoals on to isar_atp_aux for further processing  *)
   6.217  (* turns off xsymbol at start of function, restoring it at end    *)
   6.218  (******************************************************************)
   6.219  (*FIX changed to clasimp_file *)
   6.220 -val isar_atp' = setmp print_mode [] (fn (ctxt, thms, thm) =>
   6.221 +val isar_atp' = setmp print_mode [] 
   6.222 + (fn (ctxt, thms, thm) =>
   6.223    if Thm.no_prems thm then ()
   6.224    else
   6.225      let
   6.226 @@ -260,18 +191,34 @@
   6.227        (*set up variables for writing out the clasimps to a tptp file*)
   6.228        val (clause_arr, num_of_clauses, axclauses) =
   6.229          ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
   6.230 -      val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^ " clauses")
   6.231 -      val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr, num_of_clauses)
   6.232 +      val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^
   6.233 +                  " clauses")
   6.234 +      val (childin, childout, pid) = 
   6.235 +          Watcher.createWatcher (thm, clause_arr, num_of_clauses)
   6.236        val pid_string =
   6.237          string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
   6.238      in
   6.239        debug ("initial thms: " ^ thms_string);
   6.240        debug ("subgoals: " ^ prems_string);
   6.241        debug ("pid: "^ pid_string);
   6.242 -      isar_atp_aux thms thm (length prems) (childin, childout, pid) axclauses;
   6.243 -      ()
   6.244 +      write_problem_files axclauses thm (length prems);
   6.245 +      watcher_call_provers (sign_of_thm thm) (Thm.prems_of thm) (childin, childout, pid)
   6.246      end);
   6.247  
   6.248 +val isar_atp_writeonly = setmp print_mode [] 
   6.249 + (fn (ctxt, thms, thm) =>
   6.250 +  if Thm.no_prems thm then ()
   6.251 +  else
   6.252 +    let
   6.253 +      val thy = ProofContext.theory_of ctxt
   6.254 +      val prems = Thm.prems_of thm
   6.255 +
   6.256 +      (*set up variables for writing out the clasimps to a tptp file*)
   6.257 +      val (clause_arr, num_of_clauses, axclauses) =
   6.258 +        ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
   6.259 +    in
   6.260 +      write_problem_files axclauses thm (length prems)
   6.261 +    end);
   6.262  
   6.263  fun get_thms_cs claset =
   6.264    let val {safeEs, safeIs, hazEs, hazIs, ...} = rep_cs claset
     7.1 --- a/src/HOL/Tools/res_clause.ML	Thu Sep 15 17:45:17 2005 +0200
     7.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Sep 15 17:46:00 2005 +0200
     7.3 @@ -35,7 +35,7 @@
     7.4    val dfg_clauses2str : string list -> string
     7.5    val clause2dfg : clause -> string * string list
     7.6    val clauses2dfg : clause list -> string -> clause list -> clause list ->
     7.7 -	   (string * int) list -> (string * int) list -> string list -> string
     7.8 +	   (string * int) list -> (string * int) list -> string
     7.9    val tfree_dfg_clause : string -> string
    7.10  
    7.11    val tptp_arity_clause : arityClause -> string
    7.12 @@ -878,16 +878,16 @@
    7.13  
    7.14  
    7.15  fun tfree_dfg_clause tfree_lit =
    7.16 -  "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^ "tfree_tcs" ^ ")."
    7.17 +  "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ")."
    7.18  
    7.19  
    7.20 -fun gen_dfg_file probname axioms conjectures funcs preds tfrees= 
    7.21 +fun gen_dfg_file probname axioms conjectures funcs preds = 
    7.22      let val axstrs_tfrees = (map clause2dfg axioms)
    7.23  	val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
    7.24          val axstr = ResLib.list2str_sep delim axstrs
    7.25          val conjstrs_tfrees = (map clause2dfg conjectures)
    7.26  	val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
    7.27 -        val tfree_clss = map tfree_dfg_clause ((ResLib.flat_noDup atfrees) \\ tfrees) 
    7.28 +        val tfree_clss = map tfree_dfg_clause (ResLib.flat_noDup atfrees) 
    7.29          val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs)
    7.30          val funcstr = string_of_funcs funcs
    7.31          val predstr = string_of_preds preds
    7.32 @@ -898,14 +898,13 @@
    7.33         (string_of_conjectures conjstr) ^ (string_of_end ())
    7.34      end;
    7.35     
    7.36 -fun clauses2dfg [] probname axioms conjectures funcs preds tfrees = 
    7.37 +fun clauses2dfg [] probname axioms conjectures funcs preds = 
    7.38        let val funcs' = (ResLib.flat_noDup(map funcs_of_cls axioms)) @ funcs
    7.39  	  val preds' = (ResLib.flat_noDup(map preds_of_cls axioms)) @ preds
    7.40        in
    7.41 -	 gen_dfg_file probname axioms conjectures funcs' preds' tfrees 
    7.42 -	 (*(probname, axioms, conjectures, funcs, preds)*)
    7.43 +	 gen_dfg_file probname axioms conjectures funcs' preds' 
    7.44        end
    7.45 - | clauses2dfg (cls::clss) probname axioms conjectures funcs preds tfrees = 
    7.46 + | clauses2dfg (cls::clss) probname axioms conjectures funcs preds = 
    7.47       let val (lits,tfree_lits) = dfg_clause_aux cls
    7.48  	       (*"lits" includes the typing assumptions (TVars)*)
    7.49  	 val cls_id = get_clause_id cls
    7.50 @@ -920,17 +919,10 @@
    7.51  	 val conjectures' = 
    7.52  	     if knd = "conjecture" then (cls::conjectures) else conjectures
    7.53       in
    7.54 -	 clauses2dfg clss probname axioms' conjectures' funcs' preds' tfrees 
    7.55 +	 clauses2dfg clss probname axioms' conjectures' funcs' preds' 
    7.56       end;
    7.57  
    7.58  
    7.59 -fun fileout f str = let val out = TextIO.openOut f
    7.60 -    in
    7.61 -	ResLib.writeln_strs out str; TextIO.closeOut out
    7.62 -    end;
    7.63 -
    7.64 -
    7.65 -
    7.66  fun string_of_arClauseID (ArityClause arcls) =
    7.67      arclause_prefix ^ string_of_int(#clause_id arcls);
    7.68  
    7.69 @@ -997,7 +989,7 @@
    7.70      "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
    7.71      knd ^ ",[" ^ tfree_lit ^ "]).";
    7.72  
    7.73 -fun tptp_clause_aux (Clause cls) = 
    7.74 +fun tptp_type_lits (Clause cls) = 
    7.75      let val lits = map tptp_literal (#literals cls)
    7.76  	val tvar_lits_strs =
    7.77  	      if !keep_types 
    7.78 @@ -1012,7 +1004,7 @@
    7.79      end; 
    7.80  
    7.81  fun tptp_clause cls =
    7.82 -    let val (lits,tfree_lits) = tptp_clause_aux cls 
    7.83 +    let val (lits,tfree_lits) = tptp_type_lits cls 
    7.84              (*"lits" includes the typing assumptions (TVars)*)
    7.85  	val cls_id = get_clause_id cls
    7.86  	val ax_name = get_axiomName cls
    7.87 @@ -1028,7 +1020,7 @@
    7.88      end;
    7.89  
    7.90  fun clause2tptp cls =
    7.91 -    let val (lits,tfree_lits) = tptp_clause_aux cls 
    7.92 +    let val (lits,tfree_lits) = tptp_type_lits cls 
    7.93              (*"lits" includes the typing assumptions (TVars)*)
    7.94  	val cls_id = get_clause_id cls
    7.95  	val ax_name = get_axiomName cls