simplification of the Isabelle-ATP code; hooks for batch generation of problems
authorpaulson
Mon Sep 19 15:12:13 2005 +0200 (2005-09-19)
changeset 17484f6a225f97f0a
parent 17483 c6005bfc1630
child 17485 c39871c52977
simplification of the Isabelle-ATP code; hooks for batch generation of problems
src/HOL/IsaMakefile
src/HOL/Reconstruction.thy
src/HOL/Tools/ATP/AtpCommunication.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/res_clasimpset.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 19 14:20:45 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Sep 19 15:12:13 2005 +0200
     1.3 @@ -93,8 +93,7 @@
     1.4    Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
     1.5    ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
     1.6    Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML		\
     1.7 -  Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/SpassCommunication.ML		\
     1.8 -  Tools/ATP/VampCommunication.ML						\
     1.9 +  Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML		\
    1.10    Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML			\
    1.11    Tools/ATP/recon_prelim.ML Tools/ATP/recon_transfer_proof.ML			\
    1.12    Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML		\
     2.1 --- a/src/HOL/Reconstruction.thy	Mon Sep 19 14:20:45 2005 +0200
     2.2 +++ b/src/HOL/Reconstruction.thy	Mon Sep 19 15:12:13 2005 +0200
     2.3 @@ -20,8 +20,7 @@
     2.4    "Tools/ATP/recon_translate_proof.ML"
     2.5    "Tools/ATP/recon_parse.ML"
     2.6    "Tools/ATP/recon_transfer_proof.ML"
     2.7 -  "Tools/ATP/VampCommunication.ML"
     2.8 -  "Tools/ATP/SpassCommunication.ML"
     2.9 +  "Tools/ATP/AtpCommunication.ML"
    2.10    "Tools/ATP/watcher.ML"
    2.11    "Tools/ATP/res_clasimpset.ML"
    2.12    "Tools/res_atp.ML"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Mon Sep 19 15:12:13 2005 +0200
     3.3 @@ -0,0 +1,311 @@
     3.4 +(*  Title:      VampCommunication.ml
     3.5 +    ID:         $Id$
     3.6 +    Author:     Claire Quigley
     3.7 +    Copyright   2004  University of Cambridge
     3.8 +*)
     3.9 +
    3.10 +(***************************************************************************)
    3.11 +(*  Code to deal with the transfer of proofs from a Vampire process          *)
    3.12 +(***************************************************************************)
    3.13 +signature ATP_COMMUNICATION =
    3.14 +  sig
    3.15 +    val reconstruct : bool ref
    3.16 +    val checkEProofFound: 
    3.17 +          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    3.18 +          string * string * thm * int * (ResClause.clause * thm) Array.array -> bool
    3.19 +    val checkVampProofFound: 
    3.20 +          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    3.21 +          string * string * thm * int * (ResClause.clause * thm) Array.array -> bool
    3.22 +    val checkSpassProofFound:  
    3.23 +          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    3.24 +          string * string * thm * int * (ResClause.clause * thm) Array.array -> bool
    3.25 +  end;
    3.26 +
    3.27 +structure AtpCommunication : ATP_COMMUNICATION =
    3.28 +struct
    3.29 +
    3.30 +(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
    3.31 +val reconstruct = ref false;
    3.32 +
    3.33 +exception EOF;
    3.34 +
    3.35 +val start_E = "# Proof object starts here."
    3.36 +val end_E   = "# Proof object ends here."
    3.37 +val start_V6 = "%================== Proof: ======================"
    3.38 +val end_V6   = "%==============  End of proof. =================="
    3.39 +val start_V8 = "=========== Refutation =========="
    3.40 +val end_V8 = "======= End of refutation ======="
    3.41 +
    3.42 +(*Identifies the start/end lines of an ATP's output*)
    3.43 +local open Recon_Parse in
    3.44 +fun extract_proof s =
    3.45 +  if cut_exists "Here is a proof with" s then
    3.46 +    (kill_lines 0
    3.47 +     o snd o cut_after ":"
    3.48 +     o snd o cut_after "Here is a proof with"
    3.49 +     o fst o cut_after " ||  -> .") s
    3.50 +  else if cut_exists start_V8 s then
    3.51 +    (kill_lines 0    (*Vampire 8.0*)
    3.52 +     o snd o cut_after start_V8
    3.53 +     o fst o cut_before end_V8) s
    3.54 +  else if cut_exists end_E s then
    3.55 +    (kill_lines 0    (*eproof*)
    3.56 +     o snd o cut_after start_E
    3.57 +     o fst o cut_before end_E) s
    3.58 +  else "??extract_proof failed" (*Couldn't find a proof*)
    3.59 +end;
    3.60 +
    3.61 +(**********************************************************************)
    3.62 +(*  Reconstruct the Vampire/E proof w.r.t. thmstring (string version of   *)
    3.63 +(*  Isabelle goal to be proved), then transfer the reconstruction     *)
    3.64 +(*  steps as a string to the input pipe of the main Isabelle process  *)
    3.65 +(**********************************************************************)
    3.66 +
    3.67 +fun reconstruct_tac proofextract goalstring toParent ppid sg_num clause_arr =
    3.68 +    SELECT_GOAL
    3.69 +      (EVERY1
    3.70 +        [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
    3.71 +	 METAHYPS(fn negs =>
    3.72 +		     (Recon_Transfer.prover_lemma_list proofextract  
    3.73 +		       goalstring toParent ppid negs clause_arr))]) sg_num
    3.74 +
    3.75 +
    3.76 +(*********************************************************************************)
    3.77 +(*  Inspect the output of an ATP process to see if it has found a proof,     *)
    3.78 +(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    3.79 +(*********************************************************************************)
    3.80 +
    3.81 +fun startTransfer (startS,endS)
    3.82 +      (fromChild, toParent, ppid, goalstring, childCmd, thm, sg_num, clause_arr) =
    3.83 + let val thisLine = TextIO.inputLine fromChild
    3.84 +     fun transferInput currentString =
    3.85 +      let val thisLine = TextIO.inputLine fromChild
    3.86 +      in
    3.87 +	if thisLine = "" (*end of file?*)
    3.88 +	then (File.write (File.tmp_path (Path.basic"extraction_failed")) 
    3.89 +	                 ("start bracket: " ^ startS ^
    3.90 +	                  "\nend bracket: " ^ endS ^
    3.91 +	                  "\naccumulated text: " ^ currentString);
    3.92 +	      raise EOF)                    
    3.93 +	else if String.isPrefix endS thisLine
    3.94 +	then let val proofextract = extract_proof (currentString^thisLine)
    3.95 +	     in
    3.96 +	       File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; 
    3.97 +	       reconstruct_tac proofextract goalstring toParent ppid sg_num  
    3.98 +			       clause_arr thm
    3.99 +	     end
   3.100 +	else transferInput (currentString^thisLine)
   3.101 +      end
   3.102 + in
   3.103 +   if thisLine = "" then false
   3.104 +   else if String.isPrefix startS thisLine
   3.105 +   then
   3.106 +    (File.append (File.tmp_path (Path.basic "transfer_start"))
   3.107 +		 ("about to transfer proof, thm is: " ^ string_of_thm thm);
   3.108 +     transferInput thisLine;
   3.109 +     true) handle EOF => false
   3.110 +   else
   3.111 +      startTransfer (startS,endS)
   3.112 +                    (fromChild, toParent, ppid, goalstring,
   3.113 +		     childCmd, thm, sg_num,clause_arr)
   3.114 + end
   3.115 +
   3.116 +(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
   3.117 +fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, 
   3.118 +                         thm, sg_num, clause_arr) =
   3.119 + let val proof_file = TextIO.openAppend
   3.120 +	   (File.platform_path(File.tmp_path (Path.basic "vampire_proof")))
   3.121 +     val _ = File.write (File.tmp_path (Path.basic "vampire_checking_prf"))
   3.122 +			("checking if proof found, thm is: " ^ string_of_thm thm)
   3.123 +     val thisLine = TextIO.inputLine fromChild
   3.124 + in   
   3.125 +     File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
   3.126 +     if thisLine = "" 
   3.127 +     then (TextIO.output (proof_file, "No proof output seen \n");
   3.128 +	   TextIO.closeOut proof_file;
   3.129 +	   false)
   3.130 +     else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine
   3.131 +     then
   3.132 +       startTransfer (start_V8, end_V8)
   3.133 +	      (fromChild, toParent, ppid, goalstring,
   3.134 +	       childCmd, thm, sg_num, clause_arr)
   3.135 +     else if (String.isPrefix "Satisfiability detected" thisLine) orelse
   3.136 +             (String.isPrefix "Refutation not found" thisLine)
   3.137 +     then
   3.138 +       (TextIO.output (toParent, "Failure\n");
   3.139 +	TextIO.output (toParent, goalstring^"\n");
   3.140 +	TextIO.flushOut toParent;
   3.141 +	TextIO.output (proof_file, thisLine);
   3.142 +	TextIO.closeOut proof_file;
   3.143 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.144 +	(* Attempt to prevent several signals from turning up simultaneously *)
   3.145 +	Posix.Process.sleep(Time.fromSeconds 1);
   3.146 +	true)
   3.147 +     else
   3.148 +       (TextIO.output (proof_file, thisLine);
   3.149 +	TextIO.flushOut proof_file;
   3.150 +	checkVampProofFound  (fromChild, toParent, ppid, 
   3.151 +	   goalstring,childCmd, thm, sg_num, clause_arr))
   3.152 +  end
   3.153 +
   3.154 +
   3.155 +(*Called from watcher. Returns true if the E process has returned a verdict.*)
   3.156 +fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd,
   3.157 +                      thm, sg_num, clause_arr) = 
   3.158 + let val E_proof_file = TextIO.openAppend
   3.159 +	   (File.platform_path(File.tmp_path (Path.basic "e_proof")))
   3.160 +     val _ = File.write (File.tmp_path (Path.basic "e_checking_prf"))
   3.161 +			("checking if proof found. childCmd is " ^ childCmd ^
   3.162 +			 "\nthm is: " ^ string_of_thm thm)
   3.163 +     val thisLine = TextIO.inputLine fromChild  
   3.164 + in   
   3.165 +     File.write (File.tmp_path (Path.basic "e_response")) thisLine;
   3.166 +     if thisLine = "" 
   3.167 +     then (TextIO.output (E_proof_file, "No proof output seen \n");
   3.168 +	    TextIO.closeOut E_proof_file;
   3.169 +	    false)
   3.170 +     else if thisLine = "# TSTP exit status: Unsatisfiable\n"
   3.171 +     then      
   3.172 +       startTransfer (start_E, end_E)
   3.173 +             (fromChild, toParent, ppid, goalstring,
   3.174 +	      childCmd, thm, sg_num, clause_arr)
   3.175 +     else if String.isPrefix "# Problem is satisfiable" thisLine
   3.176 +     then  
   3.177 +       (TextIO.output (toParent, "Invalid\n");
   3.178 +	TextIO.output (toParent, goalstring^"\n");
   3.179 +	TextIO.flushOut toParent;
   3.180 +	TextIO.output (E_proof_file, thisLine);
   3.181 +	TextIO.closeOut E_proof_file;
   3.182 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.183 +	(* Attempt to prevent several signals from turning up simultaneously *)
   3.184 +	Posix.Process.sleep(Time.fromSeconds 1);
   3.185 +	true)
   3.186 +     else if String.isPrefix "# Failure: Resource limit exceeded" thisLine
   3.187 +     then  (*In fact, E distingishes "out of time" and "out of memory"*)
   3.188 +       (File.write (File.tmp_path (Path.basic "e_response")) thisLine;
   3.189 +	TextIO.output (toParent, "Failure\n");
   3.190 +	TextIO.output (toParent, goalstring^"\n");
   3.191 +	TextIO.flushOut toParent;
   3.192 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.193 +	TextIO.output (E_proof_file, "signalled parent\n");
   3.194 +	TextIO.closeOut E_proof_file;
   3.195 +	(* Attempt to prevent several signals from turning up simultaneously *)
   3.196 +	Posix.Process.sleep(Time.fromSeconds 1);
   3.197 +	true)
   3.198 +     else
   3.199 +	(TextIO.output (E_proof_file, thisLine);
   3.200 +	TextIO.flushOut E_proof_file;
   3.201 +	checkEProofFound  (fromChild, toParent, ppid, goalstring,
   3.202 +	childCmd, thm, sg_num, clause_arr))
   3.203 + end
   3.204 +
   3.205 +
   3.206 +(**********************************************************************)
   3.207 +(*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
   3.208 +(*  Isabelle goal to be proved), then transfer the reconstruction     *)
   3.209 +(*  steps as a string to the input pipe of the main Isabelle process  *)
   3.210 +(**********************************************************************)
   3.211 +
   3.212 +fun spass_reconstruct_tac proofextract goalstring toParent ppid sg_num 
   3.213 +                    clause_arr = 
   3.214 + let val f = if !reconstruct then Recon_Transfer.spass_reconstruct
   3.215 +                             else Recon_Transfer.spass_lemma_list
   3.216 + in                             
   3.217 +   SELECT_GOAL
   3.218 +    (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
   3.219 +             METAHYPS(fn negs => 
   3.220 +    f proofextract goalstring toParent ppid negs clause_arr)]) sg_num	
   3.221 + end;
   3.222 +
   3.223 +
   3.224 +fun transferSpassInput (fromChild, toParent, ppid, goalstring, 
   3.225 +                        currentString, thm, sg_num, clause_arr) = 
   3.226 + let val thisLine = TextIO.inputLine fromChild 
   3.227 + in 
   3.228 +    if thisLine = "" (*end of file?*)
   3.229 +    then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString;
   3.230 +	  raise EOF)                    
   3.231 +    else if thisLine = "--------------------------SPASS-STOP------------------------------\n"
   3.232 +    then 
   3.233 +      let val proofextract = extract_proof (currentString^thisLine)
   3.234 +      in 
   3.235 +	  File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract;
   3.236 +	  spass_reconstruct_tac proofextract goalstring toParent ppid sg_num 
   3.237 +	      clause_arr thm
   3.238 +      end
   3.239 +    else transferSpassInput (fromChild, toParent, ppid, goalstring,
   3.240 +			     (currentString^thisLine), thm, sg_num, clause_arr)
   3.241 + end;
   3.242 +
   3.243 +
   3.244 +(*********************************************************************************)
   3.245 +(*  Inspect the output of a Spass   process to see if it has found a proof,     *)
   3.246 +(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   3.247 +(*********************************************************************************)
   3.248 +
   3.249 + 
   3.250 +fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd,
   3.251 +                        thm, sg_num,clause_arr) = 
   3.252 +   let val thisLine = TextIO.inputLine fromChild  
   3.253 +   in                 
   3.254 +      if thisLine = "" then false
   3.255 +      else if String.isPrefix "Here is a proof" thisLine then     
   3.256 +	 (File.append (File.tmp_path (Path.basic "spass_transfer"))
   3.257 +		      ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n");
   3.258 +	  transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine, 
   3.259 + 	                     thm, sg_num,clause_arr);
   3.260 +	  true) handle EOF => false
   3.261 +      else startSpassTransfer (fromChild, toParent, ppid, goalstring,
   3.262 +                               childCmd, thm, sg_num,clause_arr)
   3.263 +    end
   3.264 +
   3.265 +
   3.266 +(*Called from watcher. Returns true if the E process has returned a verdict.*)
   3.267 +fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd,
   3.268 +                          thm, sg_num, clause_arr) = 
   3.269 + let val spass_proof_file = TextIO.openAppend
   3.270 +           (File.platform_path(File.tmp_path (Path.basic "spass_proof")))
   3.271 +     val _ = File.write(File.tmp_path (Path.basic "spass_checking_prf"))
   3.272 +		("checking if proof found, thm is: "^(string_of_thm thm))
   3.273 +     val thisLine = TextIO.inputLine fromChild  
   3.274 + in    
   3.275 +     File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
   3.276 +     if thisLine = "" 
   3.277 +     then (TextIO.output (spass_proof_file, ("No proof output seen \n"));
   3.278 +	   TextIO.closeOut spass_proof_file;
   3.279 +	   false)
   3.280 +     else if thisLine = "SPASS beiseite: Proof found.\n"
   3.281 +     then      
   3.282 +        startSpassTransfer (fromChild, toParent, ppid, goalstring,
   3.283 +	                    childCmd, thm, sg_num, clause_arr)
   3.284 +     else if thisLine = "SPASS beiseite: Completion found.\n"
   3.285 +     then  
   3.286 +       (TextIO.output (spass_proof_file, thisLine);
   3.287 +	TextIO.closeOut spass_proof_file;
   3.288 +	TextIO.output (toParent, "Invalid\n");
   3.289 +	TextIO.output (toParent, goalstring^"\n");
   3.290 +	TextIO.flushOut toParent;
   3.291 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.292 +	(* Attempt to prevent several signals from turning up simultaneously *)
   3.293 +	Posix.Process.sleep(Time.fromSeconds 1);
   3.294 +	true)
   3.295 +     else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   3.296 +             thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   3.297 +     then  
   3.298 +       (TextIO.output (toParent, "Failure\n");
   3.299 +	TextIO.output (toParent, goalstring^"\n");
   3.300 +	TextIO.flushOut toParent;
   3.301 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.302 +	TextIO.output (spass_proof_file, "signalled parent\n");
   3.303 +	TextIO.closeOut spass_proof_file;
   3.304 +	(* Attempt to prevent several signals from turning up simultaneously *)
   3.305 +	Posix.Process.sleep(Time.fromSeconds 1);
   3.306 +	true)
   3.307 +    else
   3.308 +       (TextIO.output (spass_proof_file, thisLine);
   3.309 +       TextIO.flushOut spass_proof_file;
   3.310 +       checkSpassProofFound  (fromChild, toParent, ppid, goalstring,
   3.311 +       childCmd, thm, sg_num, clause_arr))
   3.312 + end
   3.313 +
   3.314 +end;
     4.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Mon Sep 19 14:20:45 2005 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,176 +0,0 @@
     4.4 -(*  Title:      SpassCommunication.ml
     4.5 -    ID:         $Id$
     4.6 -    Author:     Claire Quigley
     4.7 -    Copyright   2004  University of Cambridge
     4.8 -*)
     4.9 -
    4.10 -(***************************************************************************)
    4.11 -(*  Code to deal with the transfer of proofs from a Spass process          *)
    4.12 -(***************************************************************************)
    4.13 -signature SPASS_COMM =
    4.14 -  sig
    4.15 -    val reconstruct : bool ref
    4.16 -    val getSpassInput : TextIO.instream -> string * string
    4.17 -    val checkSpassProofFound:  
    4.18 -          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    4.19 -          string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
    4.20 -  end;
    4.21 -
    4.22 -structure SpassComm : SPASS_COMM =
    4.23 -struct
    4.24 -
    4.25 -(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
    4.26 -val reconstruct = ref false;
    4.27 -
    4.28 -exception EOF;
    4.29 -
    4.30 -(**********************************************************************)
    4.31 -(*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
    4.32 -(*  Isabelle goal to be proved), then transfer the reconstruction     *)
    4.33 -(*  steps as a string to the input pipe of the main Isabelle process  *)
    4.34 -(**********************************************************************)
    4.35 -
    4.36 -fun reconstruct_tac proofextract goalstring toParent ppid sg_num 
    4.37 -                    clause_arr num_of_clauses = 
    4.38 - let val f = if !reconstruct then Recon_Transfer.spassString_to_reconString
    4.39 -                             else Recon_Transfer.spassString_to_lemmaString
    4.40 - in                             
    4.41 -   SELECT_GOAL
    4.42 -    (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
    4.43 -             METAHYPS(fn negs => 
    4.44 -    f proofextract goalstring toParent ppid negs clause_arr num_of_clauses)]) sg_num	
    4.45 - end;
    4.46 -
    4.47 -
    4.48 -fun transferSpassInput (fromChild, toParent, ppid, goalstring, 
    4.49 -                        currentString, thm, sg_num,clause_arr, num_of_clauses) = 
    4.50 - let val thisLine = TextIO.inputLine fromChild 
    4.51 - in 
    4.52 -    if thisLine = "" (*end of file?*)
    4.53 -    then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString;
    4.54 -	  raise EOF)                    
    4.55 -    else if thisLine = "--------------------------SPASS-STOP------------------------------\n"
    4.56 -    then 
    4.57 -      let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    4.58 -      in 
    4.59 -	  File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract;
    4.60 -	  reconstruct_tac proofextract goalstring toParent ppid sg_num 
    4.61 -	      clause_arr num_of_clauses thm
    4.62 -      end
    4.63 -    else transferSpassInput (fromChild, toParent, ppid, goalstring,
    4.64 -			     (currentString^thisLine), thm, sg_num, clause_arr, 
    4.65 -			     num_of_clauses)
    4.66 - end;
    4.67 -
    4.68 -
    4.69 -(*********************************************************************************)
    4.70 -(*  Inspect the output of a Spass   process to see if it has found a proof,     *)
    4.71 -(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    4.72 -(*********************************************************************************)
    4.73 -
    4.74 - 
    4.75 -fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd,
    4.76 -                        thm, sg_num,clause_arr, num_of_clauses) = 
    4.77 -   let val thisLine = TextIO.inputLine fromChild  
    4.78 -   in                 
    4.79 -      if thisLine = "" then false
    4.80 -      else if String.isPrefix "Here is a proof" thisLine then     
    4.81 -	 (File.append (File.tmp_path (Path.basic "spass_transfer"))
    4.82 -		      ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n");
    4.83 -	  transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine, 
    4.84 - 	                     thm, sg_num,clause_arr, num_of_clauses);
    4.85 -	  true) handle EOF => false
    4.86 -      else startSpassTransfer (fromChild, toParent, ppid, goalstring,
    4.87 -                               childCmd, thm, sg_num,clause_arr, num_of_clauses)
    4.88 -    end
    4.89 -
    4.90 -
    4.91 -fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd,
    4.92 -                          thm, sg_num, clause_arr, (num_of_clauses:int )) = 
    4.93 - let val spass_proof_file = TextIO.openAppend
    4.94 -           (File.platform_path(File.tmp_path (Path.basic "spass_proof")))
    4.95 -     val _ = File.write(File.tmp_path (Path.basic "spass_checking_prf"))
    4.96 -		("checking if proof found, thm is: "^(string_of_thm thm))
    4.97 -     val thisLine = TextIO.inputLine fromChild  
    4.98 - in    
    4.99 -     if thisLine = "" 
   4.100 -     then (TextIO.output (spass_proof_file, ("No proof output seen \n"));
   4.101 -	   TextIO.closeOut spass_proof_file;
   4.102 -	   false)
   4.103 -     else if thisLine = "SPASS beiseite: Proof found.\n"
   4.104 -     then      
   4.105 -       (File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
   4.106 -	startSpassTransfer (fromChild, toParent, ppid, goalstring,
   4.107 -	                    childCmd, thm, sg_num, clause_arr, num_of_clauses))
   4.108 -     else if thisLine = "SPASS beiseite: Completion found.\n"
   4.109 -     then  
   4.110 -       (File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
   4.111 -	TextIO.output (toParent,childCmd^"\n" );
   4.112 -	TextIO.flushOut toParent;
   4.113 -	TextIO.output (spass_proof_file, thisLine);
   4.114 -	TextIO.flushOut spass_proof_file;
   4.115 -	TextIO.closeOut spass_proof_file;
   4.116 -
   4.117 -	TextIO.output (toParent, thisLine^"\n");
   4.118 -	TextIO.output (toParent, goalstring^"\n");
   4.119 -	TextIO.flushOut toParent;
   4.120 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.121 -	(* Attempt to prevent several signals from turning up simultaneously *)
   4.122 -	Posix.Process.sleep(Time.fromSeconds 1);
   4.123 -	true)
   4.124 -     else if thisLine = "SPASS beiseite: Ran out of time.\n" 
   4.125 -     then  
   4.126 -       (File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
   4.127 -        TextIO.output (toParent, thisLine^"\n");
   4.128 -	TextIO.output (toParent, goalstring^"\n");
   4.129 -	TextIO.flushOut toParent;
   4.130 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.131 -	TextIO.output (spass_proof_file, "signalled parent\n");
   4.132 -	TextIO.closeOut spass_proof_file;
   4.133 -	(* Attempt to prevent several signals from turning up simultaneously *)
   4.134 -	Posix.Process.sleep(Time.fromSeconds 1);
   4.135 -	true)
   4.136 -    else if thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"                                                            		                 
   4.137 -    then
   4.138 -       (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.139 -	TextIO.output (toParent,childCmd^"\n" );
   4.140 -	TextIO.flushOut toParent;
   4.141 -	TextIO.output (toParent, thisLine);
   4.142 -	TextIO.flushOut toParent;
   4.143 -	true)
   4.144 -    else
   4.145 -       (TextIO.output (spass_proof_file, thisLine);
   4.146 -       TextIO.flushOut spass_proof_file;
   4.147 -       checkSpassProofFound  (fromChild, toParent, ppid, goalstring,
   4.148 -       childCmd, thm, sg_num, clause_arr, num_of_clauses))
   4.149 - end
   4.150 -
   4.151 -  
   4.152 -(***********************************************************************)
   4.153 -(*  Function used by the Isabelle process to read in a spass proof   *)
   4.154 -(***********************************************************************)
   4.155 -
   4.156 -fun getSpassInput instr = 
   4.157 -    let val thisLine = TextIO.inputLine instr 
   4.158 -        val _ = File.write (File.tmp_path (Path.basic "spass_line")) thisLine
   4.159 -    in 
   4.160 -      if thisLine = "" then ("No output from reconstruction process.\n","")
   4.161 -      else if String.sub (thisLine, 0) = #"[" orelse
   4.162 -         String.isPrefix "SPASS beiseite:" thisLine orelse
   4.163 -         String.isPrefix  "Rules from" thisLine
   4.164 -      then 
   4.165 -	let val goalstring = TextIO.inputLine instr   
   4.166 -	in (thisLine, goalstring) end
   4.167 -      else if substring (thisLine,0,5) = "Proof" orelse
   4.168 -              String.sub (thisLine, 0) = #"%"
   4.169 -      then
   4.170 -	let val goalstring = TextIO.inputLine instr
   4.171 -	in
   4.172 -          File.write (File.tmp_path (Path.basic "getSpassInput")) thisLine;
   4.173 -          (thisLine, goalstring)
   4.174 -        end
   4.175 -      else getSpassInput instr
   4.176 -     end
   4.177 -
   4.178 -
   4.179 -end;
     5.1 --- a/src/HOL/Tools/ATP/VampCommunication.ML	Mon Sep 19 14:20:45 2005 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,236 +0,0 @@
     5.4 -(*  Title:      VampCommunication.ml
     5.5 -    ID:         $Id$
     5.6 -    Author:     Claire Quigley
     5.7 -    Copyright   2004  University of Cambridge
     5.8 -*)
     5.9 -
    5.10 -(***************************************************************************)
    5.11 -(*  Code to deal with the transfer of proofs from a Vampire process          *)
    5.12 -(***************************************************************************)
    5.13 -signature VAMP_COMM =
    5.14 -  sig
    5.15 -    val getEInput : TextIO.instream -> string * string
    5.16 -    val checkEProofFound: 
    5.17 -          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    5.18 -          string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
    5.19 -
    5.20 -    val getVampInput : TextIO.instream -> string * string
    5.21 -    val checkVampProofFound: 
    5.22 -          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    5.23 -          string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
    5.24 -  end;
    5.25 -
    5.26 -structure VampComm : VAMP_COMM =
    5.27 -struct
    5.28 -
    5.29 -exception EOF;
    5.30 -
    5.31 -(**********************************************************************)
    5.32 -(*  Reconstruct the Vampire/E proof w.r.t. thmstring (string version of   *)
    5.33 -(*  Isabelle goal to be proved), then transfer the reconstruction     *)
    5.34 -(*  steps as a string to the input pipe of the main Isabelle process  *)
    5.35 -(**********************************************************************)
    5.36 -
    5.37 -fun reconstruct_tac proofextract goalstring toParent ppid sg_num 
    5.38 -                    clause_arr num_of_clauses =
    5.39 -    SELECT_GOAL
    5.40 -      (EVERY1
    5.41 -        [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
    5.42 -	 METAHYPS(fn negs =>
    5.43 -		     (Recon_Transfer.proverString_to_lemmaString proofextract  
    5.44 -		       goalstring toParent ppid negs clause_arr num_of_clauses))]) sg_num
    5.45 -
    5.46 -
    5.47 -(*********************************************************************************)
    5.48 -(*  Inspect the output of an ATP process to see if it has found a proof,     *)
    5.49 -(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    5.50 -(*********************************************************************************)
    5.51 -
    5.52 -fun startTransfer (startS,endS)
    5.53 -      (fromChild, toParent, ppid, goalstring,childCmd,
    5.54 -       thm, sg_num,clause_arr, num_of_clauses) =
    5.55 - let val thisLine = TextIO.inputLine fromChild
    5.56 -     fun transferInput currentString =
    5.57 -      let val thisLine = TextIO.inputLine fromChild
    5.58 -      in
    5.59 -	if thisLine = "" (*end of file?*)
    5.60 -	then (File.write (File.tmp_path (Path.basic"extraction_failed")) 
    5.61 -	                 ("start bracket: " ^ startS ^
    5.62 -	                  "\nend bracket: " ^ endS ^
    5.63 -	                  "\naccumulated text: " ^ currentString);
    5.64 -	      raise EOF)                    
    5.65 -	else if String.isPrefix endS thisLine
    5.66 -	then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    5.67 -	     in
    5.68 -	       File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; 
    5.69 -	       reconstruct_tac proofextract goalstring toParent ppid sg_num  
    5.70 -			       clause_arr num_of_clauses thm
    5.71 -	     end
    5.72 -	else transferInput (currentString^thisLine)
    5.73 -      end
    5.74 - in
    5.75 -   if thisLine = "" then false
    5.76 -   else if String.isPrefix startS thisLine
    5.77 -   then
    5.78 -    (File.append (File.tmp_path (Path.basic "transfer_start"))
    5.79 -		 ("about to transfer proof, thm is: " ^ string_of_thm thm);
    5.80 -     transferInput thisLine;
    5.81 -     true) handle EOF => false
    5.82 -   else
    5.83 -      startTransfer (startS,endS)
    5.84 -                    (fromChild, toParent, ppid, goalstring,
    5.85 -		     childCmd, thm, sg_num,clause_arr, num_of_clauses)
    5.86 - end
    5.87 -
    5.88 -
    5.89 -fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, 
    5.90 -                         thm, sg_num, clause_arr, num_of_clauses) =
    5.91 - let val proof_file = TextIO.openAppend
    5.92 -	   (File.platform_path(File.tmp_path (Path.basic "atp_proof")))
    5.93 -     val _ = File.write (File.tmp_path (Path.basic "atp_checking_prf"))
    5.94 -			("checking if proof found, thm is: " ^ string_of_thm thm)
    5.95 -     val thisLine = TextIO.inputLine fromChild
    5.96 - in   
    5.97 -     if thisLine = "" 
    5.98 -     then (TextIO.output (proof_file, "No proof output seen \n");
    5.99 -	   TextIO.closeOut proof_file;
   5.100 -	   false)
   5.101 -     else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine
   5.102 -     then
   5.103 -       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
   5.104 -	startTransfer (Recon_Parse.start_V8, Recon_Parse.end_V8)
   5.105 -	      (fromChild, toParent, ppid, goalstring,
   5.106 -	       childCmd, thm, sg_num, clause_arr, num_of_clauses))
   5.107 -     else if (String.isPrefix "Satisfiability detected" thisLine) orelse
   5.108 -             (String.isPrefix "Refutation not found" thisLine)
   5.109 -     then
   5.110 -       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
   5.111 -	TextIO.output (toParent,childCmd^"\n");
   5.112 -	TextIO.flushOut toParent;
   5.113 -	TextIO.output (proof_file, thisLine);
   5.114 -	TextIO.closeOut proof_file;
   5.115 - 
   5.116 -	TextIO.output (toParent, thisLine^"\n");
   5.117 -	TextIO.output (toParent, goalstring^"\n");
   5.118 -	TextIO.flushOut toParent;
   5.119 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   5.120 -	(* Attempt to prevent several signals from turning up simultaneously *)
   5.121 -	Posix.Process.sleep(Time.fromSeconds 1);
   5.122 -	true)
   5.123 -     else
   5.124 -       (TextIO.output (proof_file, thisLine);
   5.125 -	TextIO.flushOut proof_file;
   5.126 -	checkVampProofFound  (fromChild, toParent, ppid, 
   5.127 -	   goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses))
   5.128 -  end
   5.129 -
   5.130 -
   5.131 -fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd,
   5.132 -                      thm, sg_num, clause_arr, num_of_clauses) = 
   5.133 - let val E_proof_file = TextIO.openAppend
   5.134 -	   (File.platform_path(File.tmp_path (Path.basic "atp_proof")))
   5.135 -     val _ = File.write (File.tmp_path (Path.basic "atp_checking_prf"))
   5.136 -			("checking if proof found, thm is: " ^ string_of_thm thm)
   5.137 -     val thisLine = TextIO.inputLine fromChild  
   5.138 - in   
   5.139 -     if thisLine = "" 
   5.140 -     then (TextIO.output (E_proof_file, ("No proof output seen \n"));
   5.141 -	    TextIO.closeOut E_proof_file;
   5.142 -	    false)
   5.143 -     else if thisLine = "# TSTP exit status: Unsatisfiable\n"
   5.144 -     then      
   5.145 -       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
   5.146 -       startTransfer (Recon_Parse.start_E, Recon_Parse.end_E)
   5.147 -             (fromChild, toParent, ppid, goalstring,
   5.148 -	      childCmd, thm, sg_num, clause_arr, num_of_clauses))
   5.149 -     else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n"
   5.150 -     then  
   5.151 -       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
   5.152 -	TextIO.output (toParent,childCmd^"\n" );
   5.153 -	TextIO.flushOut toParent;
   5.154 -	TextIO.output (E_proof_file, thisLine);
   5.155 -	TextIO.closeOut E_proof_file;
   5.156 -
   5.157 -	TextIO.output (toParent, thisLine^"\n");
   5.158 -	TextIO.output (toParent, goalstring^"\n");
   5.159 -	TextIO.flushOut toParent;
   5.160 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   5.161 -	(* Attempt to prevent several signals from turning up simultaneously *)
   5.162 -	Posix.Process.sleep(Time.fromSeconds 1);
   5.163 -	 true)
   5.164 -     else if thisLine = "# Failure: Resource limit exceeded (time)\n" 
   5.165 -     then  
   5.166 -       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
   5.167 -	TextIO.output (toParent, thisLine^"\n");
   5.168 -	TextIO.output (toParent, goalstring^"\n");
   5.169 -	TextIO.flushOut toParent;
   5.170 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   5.171 -	TextIO.output (E_proof_file, "signalled parent\n");
   5.172 -	TextIO.closeOut E_proof_file;
   5.173 -	(* Attempt to prevent several signals from turning up simultaneously *)
   5.174 -	Posix.Process.sleep(Time.fromSeconds 1);
   5.175 -	true)
   5.176 -     else if thisLine = "# Failure: Resource limit exceeded (memory)\n"
   5.177 -     then
   5.178 -	(Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   5.179 -	 TextIO.output (toParent,childCmd^"\n" );
   5.180 -	 TextIO.output (toParent, thisLine);
   5.181 -	 TextIO.flushOut toParent;
   5.182 -	 true)
   5.183 -     else
   5.184 -	(TextIO.output (E_proof_file, thisLine);
   5.185 -	TextIO.flushOut E_proof_file;
   5.186 -	checkEProofFound  (fromChild, toParent, ppid, goalstring,
   5.187 -	childCmd, thm, sg_num, clause_arr, num_of_clauses))
   5.188 - end
   5.189 -
   5.190 -
   5.191 -(***********************************************************************)
   5.192 -(*  Function used by the Isabelle process to read in a Vampire proof   *)
   5.193 -(***********************************************************************)
   5.194 -
   5.195 -fun getVampInput instr =
   5.196 -    let val thisLine = TextIO.inputLine instr
   5.197 -	val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
   5.198 -    in    (* reconstructed proof string *)
   5.199 -      if thisLine = "" then ("No output from reconstruction process.\n","")
   5.200 -      else if String.sub (thisLine, 0) = #"[" orelse (*FIXME: for SPASS?*)
   5.201 -              String.isPrefix "Satisfiability detected" thisLine orelse
   5.202 -              String.isPrefix "Refutation not found" thisLine orelse
   5.203 -              String.isPrefix "Rules from" thisLine
   5.204 -      then
   5.205 -	let val goalstring = TextIO.inputLine instr
   5.206 -	in (thisLine, goalstring) end
   5.207 -      else if thisLine = "Proof found but translation failed!"
   5.208 -      then
   5.209 -	 let val goalstring = TextIO.inputLine instr
   5.210 -	     val _ = debug "getVampInput: translation of proof failed"
   5.211 -	 in (thisLine, goalstring) end
   5.212 -      else getVampInput instr
   5.213 -    end
   5.214 -
   5.215 -
   5.216 -(***********************************************************************)
   5.217 -(*  Function used by the Isabelle process to read in an E proof   *)
   5.218 -(***********************************************************************)
   5.219 -
   5.220 -fun getEInput instr =
   5.221 -    let val thisLine = TextIO.inputLine instr
   5.222 -	val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
   5.223 -    in    (* reconstructed proof string *)
   5.224 -      if thisLine = "" then ("No output from reconstruction process.\n","")
   5.225 -      else if String.isPrefix "# Problem is satisfiable" thisLine orelse
   5.226 -              String.isPrefix "# Cannot determine problem status" thisLine orelse
   5.227 -              String.isPrefix "# Failure:" thisLine
   5.228 -      then
   5.229 -	let val goalstring = TextIO.inputLine instr
   5.230 -	in (thisLine, goalstring) end
   5.231 -      else if thisLine = "Proof found but translation failed!"
   5.232 -      then
   5.233 -	 let val goalstring = TextIO.inputLine instr
   5.234 -	     val _ = debug "getEInput: translation of proof failed"
   5.235 -	 in (thisLine, goalstring) end
   5.236 -      else getEInput instr
   5.237 -    end
   5.238 -
   5.239 -end;
     6.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Mon Sep 19 14:20:45 2005 +0200
     6.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Mon Sep 19 15:12:13 2005 +0200
     6.3 @@ -66,9 +66,6 @@
     6.4  fun finished input = if input = [] then (0, input) else raise Noparse;
     6.5  
     6.6  
     6.7 -
     6.8 -
     6.9 -
    6.10    (* Parsing the output from gandalf *)
    6.11  datatype token = Word of string
    6.12                 | Number of int
    6.13 @@ -105,39 +102,6 @@
    6.14      fun kill_lines 0 = Library.I
    6.15        | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";
    6.16  
    6.17 -    (*fun extract_proof s
    6.18 -      = if cut_exists "EMPTY CLAUSE DERIVED" s then
    6.19 -          (kill_lines 6
    6.20 -           o snd o cut_after "EMPTY CLAUSE DERIVED"
    6.21 -           o fst o cut_after "contradiction.\n") s
    6.22 -        else
    6.23 -          raise (GandalfError "Couldn't find a proof.")
    6.24 -*)
    6.25 -
    6.26 -val start_E = "# Proof object starts here."
    6.27 -val end_E   = "# Proof object ends here."
    6.28 -val start_V6 = "%================== Proof: ======================"
    6.29 -val end_V6   = "%==============  End of proof. =================="
    6.30 -val start_V8 = "=========== Refutation =========="
    6.31 -val end_V8 = "======= End of refutation ======="
    6.32 -
    6.33 -
    6.34 -(*Identifies the start/end lines of an ATP's output*)
    6.35 -fun extract_proof s =
    6.36 -  if cut_exists "Here is a proof with" s then
    6.37 -    (kill_lines 0
    6.38 -     o snd o cut_after ":"
    6.39 -     o snd o cut_after "Here is a proof with"
    6.40 -     o fst o cut_after " ||  -> .") s
    6.41 -  else if cut_exists start_V8 s then
    6.42 -    (kill_lines 0    (*Vampire 8.0*)
    6.43 -     o snd o cut_after start_V8
    6.44 -     o fst o cut_before end_V8) s
    6.45 -  else if cut_exists end_E s then
    6.46 -    (kill_lines 0    (*eproof*)
    6.47 -     o snd o cut_after start_E
    6.48 -     o fst o cut_before end_E) s
    6.49 -  else "??extract_proof failed" (*Couldn't find a proof*)
    6.50  
    6.51  fun several p = many (some p)
    6.52        fun collect (h, t) = h ^ (fold_rev (fn s1 => fn s2 => s1 ^ s2) t "")
    6.53 @@ -163,17 +127,6 @@
    6.54       fun lex s =  alltokens  (explode s)
    6.55  
    6.56  
    6.57 -
    6.58 -(*String contains multiple lines, terminated with newline characters.
    6.59 -  A list consisting of the first number in each line is returned. *)
    6.60 -fun get_linenums proofstr = 
    6.61 -  let val numerics = String.tokens (not o Char.isDigit)
    6.62 -      fun firstno [] = NONE
    6.63 -        | firstno (x::xs) = Int.fromString x
    6.64 -      val lines = String.tokens (fn c => c = #"\n") proofstr
    6.65 -  in  List.mapPartial (firstno o numerics) lines  end
    6.66 -
    6.67 -
    6.68  (************************************************************)
    6.69  
    6.70  (**************************************************)
     7.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Sep 19 14:20:45 2005 +0200
     7.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Sep 19 15:12:13 2005 +0200
     7.3 @@ -39,12 +39,10 @@
     7.4  (*|   proofstep_to_string (Rewrite((a,b),(c,d))) =
     7.5        "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"*)
     7.6  
     7.7 -fun list_to_string [] liststr = liststr
     7.8 -|   list_to_string (x::[]) liststr = liststr^(string_of_int x)
     7.9 -|   list_to_string (x::xs) liststr = list_to_string xs (liststr^(string_of_int x)^",")
    7.10  
    7.11 -
    7.12 -fun proof_to_string (num,(step,clause_strs, thmvars)) = (string_of_int num)^(proofstep_to_string step)^"["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]"
    7.13 +fun proof_to_string (num,(step,clause_strs, thmvars)) =
    7.14 + (string_of_int num)^(proofstep_to_string step)^
    7.15 + "["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]"
    7.16   
    7.17  
    7.18  fun proofs_to_string [] str = str
    7.19 @@ -55,7 +53,9 @@
    7.20  
    7.21  
    7.22  
    7.23 -fun init_proofstep_to_string (num, step, clause_strs) = (string_of_int num)^" "^(proofstep_to_string step)^" "^(clause_strs_to_string clause_strs "")^" "
    7.24 +fun init_proofstep_to_string (num, step, clause_strs) =
    7.25 + (string_of_int num)^" "^(proofstep_to_string step)^" "^
    7.26 + (clause_strs_to_string clause_strs "")^" "
    7.27  
    7.28  fun init_proofsteps_to_string [] str = str
    7.29  |   init_proofsteps_to_string (x::xs) str = let val newstr = init_proofstep_to_string x 
    7.30 @@ -144,12 +144,11 @@
    7.31  
    7.32  (* retrieve the axioms that were obtained from the clasimpset *)
    7.33  
    7.34 -fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) clasimp_num step_nums = 
    7.35 -    let val realnums = map subone step_nums	
    7.36 -	val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
    7.37 -(*	val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))     
    7.38 -	val _ = TextIO.output(axnums,(numstr clasimp_nums))
    7.39 -	val _ = TextIO.closeOut(axnums)*)
    7.40 +fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) step_nums = 
    7.41 +    let val clasimp_nums = List.filter (is_clasimp_ax (Array.length clause_arr - 1)) 
    7.42 +	                   (map subone step_nums)
    7.43 +(*	val _ = File.write (File.tmp_path (Path.basic "axnums")) 
    7.44 +                     (numstr clasimp_nums) *)
    7.45      in
    7.46  	map (fn x =>  Array.sub(clause_arr, x)) clasimp_nums
    7.47      end
    7.48 @@ -159,7 +158,7 @@
    7.49  (* get names of clasimp axioms used                  *)
    7.50  (*****************************************************)
    7.51  
    7.52 - fun get_axiom_names step_nums thms clause_arr num_of_clauses =
    7.53 + fun get_axiom_names step_nums thms clause_arr =
    7.54     let 
    7.55       (* not sure why this is necessary again, but seems to be *)
    7.56        val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    7.57 @@ -168,7 +167,7 @@
    7.58       (* here need to add the clauses from clause_arr*)
    7.59       (***********************************************)
    7.60    
    7.61 -      val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums 
    7.62 +      val clasimp_names_cls = get_clasimp_cls clause_arr step_nums 
    7.63        val clasimp_names = map (ResClause.get_axiomName o #1) clasimp_names_cls
    7.64        val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    7.65                           (concat clasimp_names)
    7.66 @@ -178,20 +177,30 @@
    7.67     end
    7.68     
    7.69  
    7.70 -fun get_axiom_names_spass proofstr thms clause_arr num_of_clauses =
    7.71 +fun get_axiom_names_spass proofstr thms clause_arr =
    7.72    let (* parse spass proof into datatype *)
    7.73 +      val _ = File.write (File.tmp_path (Path.basic "parsing_progress")) 
    7.74 +                         ("Started parsing:\n" ^ proofstr)
    7.75        val tokens = #1(lex proofstr)
    7.76        val proof_steps = parse tokens
    7.77 -      val _ = File.write (File.tmp_path (Path.basic "parsing_done")) 
    7.78 -                         ("Did parsing on "^proofstr)
    7.79 +      val _ = File.append (File.tmp_path (Path.basic "parsing_progress")) "\nFinished!"
    7.80        (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
    7.81    in
    7.82      get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) 
    7.83 -                    thms clause_arr num_of_clauses
    7.84 +                    thms clause_arr
    7.85    end;
    7.86      
    7.87 - fun get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses  =
    7.88 -   get_axiom_names (get_linenums proofstr) thms clause_arr num_of_clauses;
    7.89 + (*String contains multiple lines, terminated with newline characters.
    7.90 +  A list consisting of the first number in each line is returned. *)
    7.91 +fun get_linenums proofstr = 
    7.92 +  let val numerics = String.tokens (not o Char.isDigit)
    7.93 +      fun firstno [] = NONE
    7.94 +        | firstno (x::xs) = Int.fromString x
    7.95 +      val lines = String.tokens (fn c => c = #"\n") proofstr
    7.96 +  in  List.mapPartial (firstno o numerics) lines  end
    7.97 +
    7.98 +fun get_axiom_names_vamp_E proofstr thms clause_arr  =
    7.99 +   get_axiom_names (get_linenums proofstr) thms clause_arr;
   7.100      
   7.101  
   7.102  (***********************************************)
   7.103 @@ -206,13 +215,13 @@
   7.104  
   7.105  fun addvars c (a,b)  = (a,b,c)
   7.106  
   7.107 -fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
   7.108 +fun get_axioms_used proof_steps thms clause_arr  =
   7.109    let 
   7.110       val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   7.111       val axioms = (List.filter is_axiom) proof_steps
   7.112       val step_nums = get_step_nums axioms []
   7.113  
   7.114 -     val clauses =(*(clasimp_cls)@*)( make_clauses thms)
   7.115 +     val clauses = make_clauses thms    (*FIXME: must this be repeated??*)
   7.116       
   7.117       val vars = map thm_vars clauses
   7.118      
   7.119 @@ -265,19 +274,19 @@
   7.120  val restore_linebreaks = subst_for #"\t" #"\n";
   7.121  
   7.122  
   7.123 -fun proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms clause_arr num_of_clauses getax = 
   7.124 - let val _ = File.append(File.tmp_path (Path.basic "spass_lemmastring"))
   7.125 +fun prover_lemma_list_aux proofstr goalstring toParent ppid thms clause_arr getax = 
   7.126 + let val _ = File.append(File.tmp_path (Path.basic "prover_lemmastring"))
   7.127                 ("proofstr is " ^ proofstr ^
   7.128                  "\ngoalstr is " ^ goalstring ^
   7.129 -                "\nnum of clauses is " ^ string_of_int num_of_clauses)
   7.130 +                "\nnum of clauses is " ^ string_of_int (Array.length clause_arr))
   7.131  
   7.132 -     val axiom_names = getax proofstr thms clause_arr num_of_clauses
   7.133 -     val ax_str = "Rules from clasimpset used in automatic proof: " ^
   7.134 -                  rules_to_string axiom_names
   7.135 +     val axiom_names = getax proofstr thms clause_arr
   7.136 +     val ax_str = rules_to_string axiom_names
   7.137      in 
   7.138 -	 File.append(File.tmp_path (Path.basic "spass_lemmastring"))
   7.139 -	            ("reconstring is: "^ax_str^"  "^goalstring);
   7.140 -         TextIO.output (toParent, ax_str^"\n");
   7.141 +	 File.append(File.tmp_path (Path.basic "prover_lemmastring"))
   7.142 +	            ("\nlemma list is: " ^ ax_str);
   7.143 +         TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
   7.144 +                  ax_str ^ "\n");
   7.145  	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   7.146  	 TextIO.flushOut toParent;
   7.147  
   7.148 @@ -285,9 +294,10 @@
   7.149  	(* Attempt to prevent several signals from turning up simultaneously *)
   7.150  	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   7.151      end
   7.152 -    handle _ => (*FIXME: exn handler is too general!*)
   7.153 -     (File.write(File.tmp_path (Path.basic "proverString_handler")) "In exception handler";
   7.154 -      TextIO.output (toParent, "Proof found but translation failed : " ^ 
   7.155 +    handle exn => (*FIXME: exn handler is too general!*)
   7.156 +     (File.write(File.tmp_path (Path.basic "proverString_handler")) 
   7.157 +         ("In exception handler: " ^ Toplevel.exn_message exn);
   7.158 +      TextIO.output (toParent, "Translation failed for the proof: " ^ 
   7.159                       remove_linebreaks proofstr ^ "\n");
   7.160        TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
   7.161        TextIO.flushOut toParent;
   7.162 @@ -295,21 +305,19 @@
   7.163        (* Attempt to prevent several signals from turning up simultaneously *)
   7.164        Posix.Process.sleep(Time.fromSeconds 1); all_tac);
   7.165  
   7.166 -fun proverString_to_lemmaString proofstr goalstring toParent ppid thms
   7.167 -      clause_arr num_of_clauses  = 
   7.168 -  proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms        
   7.169 -       clause_arr num_of_clauses get_axiom_names_vamp_E;
   7.170 +fun prover_lemma_list proofstr goalstring toParent ppid thms clause_arr  = 
   7.171 +  prover_lemma_list_aux proofstr goalstring toParent ppid thms        
   7.172 +       clause_arr get_axiom_names_vamp_E;
   7.173  
   7.174 -fun spassString_to_lemmaString proofstr goalstring toParent ppid thms
   7.175 -      clause_arr  num_of_clauses  = 
   7.176 -  proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms        
   7.177 -       clause_arr num_of_clauses get_axiom_names_spass;
   7.178 +fun spass_lemma_list proofstr goalstring toParent ppid thms clause_arr = 
   7.179 +  prover_lemma_list_aux proofstr goalstring toParent ppid thms        
   7.180 +       clause_arr get_axiom_names_spass;
   7.181  
   7.182  
   7.183  (**** Full proof reconstruction for SPASS (not really working) ****)
   7.184  
   7.185 -fun spassString_to_reconString proofstr goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   7.186 -  let val _ = File.write(File.tmp_path (Path.basic "spass_reconstruction")) 
   7.187 +fun spass_reconstruct proofstr goalstring toParent ppid thms clause_arr = 
   7.188 +  let val _ = File.write(File.tmp_path (Path.basic "prover_reconstruction")) 
   7.189                   ("proofstr is: "^proofstr)
   7.190        val tokens = #1(lex proofstr)
   7.191  
   7.192 @@ -318,7 +326,7 @@
   7.193    (***********************************)
   7.194        val proof_steps = parse tokens
   7.195  
   7.196 -      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))
   7.197 +      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))
   7.198                        ("Did parsing on "^proofstr)
   7.199      
   7.200    (************************************)
   7.201 @@ -329,19 +337,19 @@
   7.202        (* subgoal this is, and turn it into meta_clauses *)
   7.203        (* should prob add array and table here, so that we can get axioms*)
   7.204        (* produced from the clasimpset rather than the problem *)
   7.205 -      val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   7.206 +      val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr
   7.207        
   7.208        (*val numcls_string = numclstr ( vars, numcls) ""*)
   7.209 -      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction")) "got axioms"
   7.210 +      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) "got axioms"
   7.211  	
   7.212    (************************************)
   7.213    (* translate proof                  *)
   7.214    (************************************)
   7.215 -      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))                                                                           
   7.216 +      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))                                                                           
   7.217                         ("about to translate proof, steps: "
   7.218                         ^(init_proofsteps_to_string proof_steps ""))
   7.219        val (newthm,proof) = translate_proof numcls  proof_steps vars
   7.220 -      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))                                                                       
   7.221 +      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))                                                                       
   7.222                         ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
   7.223    (***************************************************)
   7.224    (* transfer necessary steps as strings to Isabelle *)
   7.225 @@ -371,9 +379,10 @@
   7.226        (* Attempt to prevent several signals from turning up simultaneously *)
   7.227         Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   7.228    end
   7.229 -  handle _ => 
   7.230 -   (File.append(File.tmp_path (Path.basic "spass_reconstruction")) "In exception handler";
   7.231 -    TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^
   7.232 +  handle exn => (*FIXME: exn handler is too general!*)
   7.233 +   (File.append(File.tmp_path (Path.basic "prover_reconstruction"))
   7.234 +       ("In exception handler: " ^ Toplevel.exn_message exn);
   7.235 +    TextIO.output (toParent,"Translation failed for the proof:"^
   7.236           (remove_linebreaks proofstr) ^"\n");
   7.237      TextIO.output (toParent, goalstring^"\n");
   7.238      TextIO.flushOut toParent;
     8.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Mon Sep 19 14:20:45 2005 +0200
     8.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Mon Sep 19 15:12:13 2005 +0200
     8.3 @@ -112,8 +112,8 @@
     8.4    val use_simpset: bool ref
     8.5    val use_nameless: bool ref
     8.6    val get_clasimp_lemmas : 
     8.7 -         theory -> term -> 
     8.8 -         (ResClause.clause * thm) Array.array * int * ResClause.clause list 
     8.9 +         Proof.context -> term -> 
    8.10 +         (ResClause.clause * thm) Array.array * ResClause.clause list 
    8.11    end;
    8.12  
    8.13  structure ResClasimp : RES_CLASIMP =
    8.14 @@ -155,16 +155,16 @@
    8.15  (*Write out the claset and simpset rules of the supplied theory.
    8.16    FIXME: argument "goal" is a hack to allow relevance filtering.
    8.17    To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
    8.18 -fun get_clasimp_lemmas thy goal = 
    8.19 +fun get_clasimp_lemmas ctxt goal = 
    8.20      let val claset_rules = 
    8.21                map put_name_pair
    8.22  	        (ReduceAxiomsN.relevant_filter (!relevant) goal 
    8.23 -		  (ResAxioms.claset_rules_of_thy thy));
    8.24 +		  (ResAxioms.claset_rules_of_ctxt ctxt));
    8.25  	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs claset_rules []);
    8.26  
    8.27  	val simpset_rules =
    8.28  	      ReduceAxiomsN.relevant_filter (!relevant) goal 
    8.29 -                (ResAxioms.simpset_rules_of_thy thy);
    8.30 +                (ResAxioms.simpset_rules_of_ctxt ctxt);
    8.31  	val named_simpset = map put_name_pair simpset_rules
    8.32  	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
    8.33  
    8.34 @@ -184,7 +184,7 @@
    8.35  	(*********************************************************)
    8.36  	val clause_arr = Array.fromList whole_list;
    8.37    in
    8.38 -	(clause_arr, List.length whole_list, clauses)
    8.39 +	(clause_arr, clauses)
    8.40    end;
    8.41  
    8.42  
     9.1 --- a/src/HOL/Tools/ATP/watcher.ML	Mon Sep 19 14:20:45 2005 +0200
     9.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Mon Sep 19 15:12:13 2005 +0200
     9.3 @@ -13,7 +13,6 @@
     9.4  (*  Hardwired version of where to pick up the tptp files for the moment    *)
     9.5  (***************************************************************************)
     9.6  
     9.7 -
     9.8  signature WATCHER =
     9.9  sig
    9.10  
    9.11 @@ -36,7 +35,9 @@
    9.12  (* Start a watcher and set up signal handlers             *)
    9.13  (**********************************************************)
    9.14  
    9.15 -val createWatcher : thm*(ResClause.clause * thm) Array.array *  int -> TextIO.instream * TextIO.outstream * Posix.Process.pid
    9.16 +val createWatcher : 
    9.17 +    thm * (ResClause.clause * thm) Array.array -> 
    9.18 +    TextIO.instream * TextIO.outstream * Posix.Process.pid
    9.19  
    9.20  (**********************************************************)
    9.21  (* Kill watcher process                                   *)
    9.22 @@ -48,9 +49,8 @@
    9.23  
    9.24  
    9.25  
    9.26 -
    9.27  structure Watcher: WATCHER =
    9.28 -  struct
    9.29 +struct
    9.30  
    9.31  open ReconPrelim Recon_Transfer
    9.32  
    9.33 @@ -268,7 +268,10 @@
    9.34  
    9.35  fun getProofCmd (a,c,d,e,f) = d
    9.36  
    9.37 -fun setupWatcher (thm,clause_arr, num_of_clauses) = 
    9.38 +fun prems_string_of th =
    9.39 +  Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
    9.40 +
    9.41 +fun setupWatcher (thm,clause_arr) = 
    9.42    let
    9.43      (** pipes for communication between parent and watcher **)
    9.44      val p1 = Posix.IO.pipe ()
    9.45 @@ -295,10 +298,7 @@
    9.46  	   val fromParentIOD = Posix.FileSys.fdToIOD fromParent
    9.47  	   val fromParentStr = openInFD ("_exec_in_parent", fromParent)
    9.48  	   val toParentStr = openOutFD ("_exec_out_parent", toParent)
    9.49 -	   val sign = sign_of_thm thm
    9.50 -	   val prems = prems_of thm
    9.51 -	   val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    9.52 -	   val _ = debug ("subgoals forked to startWatcher: "^prems_string);
    9.53 +	   val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
    9.54  	   fun killChildren [] = ()
    9.55  	|      killChildren  (child_handle::children) =
    9.56  	         (killChild child_handle; killChildren children)
    9.57 @@ -367,46 +367,45 @@
    9.58  	 |   checkChildren ((childProc::otherChildren), toParentStr) = 
    9.59  	       let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
    9.60  			      ("In check child, length of queue:"^
    9.61 -			       (string_of_int (length (childProc::otherChildren)))^"\n")
    9.62 +			       string_of_int (length (childProc::otherChildren)))
    9.63  		   val (childInput,childOutput) =  cmdstreamsOf childProc
    9.64  		   val child_handle= cmdchildHandle childProc
    9.65  		   (* childCmd is the .dfg file that the problem is in *)
    9.66  		   val childCmd = fst(snd (cmdchildInfo childProc))
    9.67 -		   val _ = File.append (File.tmp_path (Path.basic "child_command")) 
    9.68 -			      (childCmd^"\n")
    9.69 +		   val _ = File.append (File.tmp_path (Path.basic "child_check")) 
    9.70 +			      ("\nchildCmd = " ^ childCmd)
    9.71  		   (* now get the number of the subgoal from the filename *)
    9.72  		   val path_parts = String.tokens(fn c => c = #"/") childCmd
    9.73  		   val digits = String.translate 
    9.74  		                  (fn c => if Char.isDigit c then str c else "")
    9.75  		                  (List.last path_parts);
    9.76 -		   val sg_num = (case Int.fromString digits of SOME n => n
    9.77 -                                  | NONE => error ("Watcher could not read subgoal nunber: " ^ childCmd));
    9.78 -
    9.79 +		   val sg_num =
    9.80 +		     (case Int.fromString digits of SOME n => n
    9.81 +                        | NONE => (File.append (File.tmp_path (Path.basic "child_check")) 
    9.82 +                                   "\nWatcher could not read subgoal nunber!!";
    9.83 +                                   raise ERROR));
    9.84  		   val childIncoming = pollChildInput childInput
    9.85 -		   val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) 
    9.86 -			      ("finished polling child \n")
    9.87 +		   val _ = File.append (File.tmp_path (Path.basic "child_check")) 
    9.88 +			         "\nfinished polling child"
    9.89  		   val parentID = Posix.ProcEnv.getppid()
    9.90  		   val prover = cmdProver childProc
    9.91 -		   val sign = sign_of_thm thm
    9.92 -		   val prems = prems_of thm
    9.93 -		   val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    9.94 -		   val _ = debug("subgoals forked to checkChildren: "^prems_string)
    9.95 +		   val prems_string = prems_string_of thm
    9.96  		   val goalstring = cmdGoal childProc							
    9.97 -		   val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
    9.98 -			      (prover^goalstring^childCmd^"\n")
    9.99 +		   val _ =  File.append (File.tmp_path (Path.basic "child_check")) 
   9.100 +		             ("\nsubgoals forked to checkChildren: " ^ 
   9.101 +		              space_implode "\n" [prems_string,prover,goalstring])
   9.102  	       in 
   9.103  		 if isSome childIncoming
   9.104  		 then 
   9.105  		   (* check here for prover label on child*)
   9.106 -		   let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) 
   9.107 -			      ("subgoals forked to checkChildren:"^
   9.108 -			      prems_string^prover^goalstring^childCmd) 
   9.109 +		   let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
   9.110 +			         "\nInput available from childIncoming" 
   9.111  		       val childDone = (case prover of
   9.112 -			   "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  
   9.113 -			    | "E" => VampComm.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
   9.114 -			  |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  )
   9.115 +			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  
   9.116 +			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)             
   9.117 +			  |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  )
   9.118  		    in
   9.119 -		     if childDone      (**********************************************)
   9.120 +		     if childDone
   9.121  		     then (* child has found a proof and transferred it *)
   9.122  			(* Remove this child and go on to check others*)
   9.123  			(**********************************************)
   9.124 @@ -419,7 +418,8 @@
   9.125  		       (childProc::(checkChildren (otherChildren, toParentStr)))
   9.126  		  end
   9.127  		else
   9.128 -		  (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   9.129 +		  (File.append (File.tmp_path (Path.basic "child_check"))
   9.130 +		               "No child output";
   9.131  		   childProc::(checkChildren (otherChildren, toParentStr)))
   9.132  	       end
   9.133  
   9.134 @@ -509,12 +509,12 @@
   9.135  			 let 
   9.136  			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   9.137  			   val parentID = Posix.ProcEnv.getppid()
   9.138 -			      val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
   9.139 -			   val newProcList' =checkChildren (newProcList, toParentStr) 
   9.140 -
   9.141 -			   val _ = debug("off to keep watching...")
   9.142 -			  val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
   9.143 +			      val _ = File.append (File.tmp_path (Path.basic "prekeep_watch"))
   9.144 +			      "Just execed a child\n"
   9.145 +			   val newProcList' = checkChildren (newProcList, toParentStr) 
   9.146  			 in
   9.147 +			   File.append (File.tmp_path (Path.basic "keep_watch")) 
   9.148 +			       "Off to keep watching...\n";
   9.149  			   loop newProcList'
   9.150  			 end
   9.151  		       else  (* Execute remotely              *)
   9.152 @@ -529,7 +529,7 @@
   9.153  		   else (* No new input from Isabelle *)
   9.154  		     let val newProcList = checkChildren (procList, toParentStr)
   9.155  		     in
   9.156 -		      (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
   9.157 +		      (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...2\n ");
   9.158  		       loop newProcList
   9.159  		     end
   9.160  		 end
   9.161 @@ -602,20 +602,14 @@
   9.162  (* Start a watcher and set up signal handlers             *)
   9.163  (**********************************************************)
   9.164  
   9.165 -fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   9.166 +fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   9.167  
   9.168  fun reapWatcher(pid, instr, outstr) =
   9.169 -  let val u = TextIO.closeIn instr;
   9.170 -      val u = TextIO.closeOut outstr;
   9.171 -      val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
   9.172 -  in
   9.173 -	  status
   9.174 -  end
   9.175 +  (TextIO.closeIn instr; TextIO.closeOut outstr;
   9.176 +   Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
   9.177  
   9.178 -
   9.179 -fun createWatcher (thm,clause_arr, num_of_clauses) =
   9.180 - let val (childpid,(childin,childout)) =
   9.181 -           childInfo (setupWatcher(thm,clause_arr, num_of_clauses))
   9.182 +fun createWatcher (thm, clause_arr) =
   9.183 + let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
   9.184       fun decr_watched() =
   9.185  	  (goals_being_watched := (!goals_being_watched) - 1;
   9.186  	   if !goals_being_watched = 0
   9.187 @@ -623,63 +617,54 @@
   9.188  	     (File.append (File.tmp_path (Path.basic "reap_found"))
   9.189  	       ("Reaping a watcher, childpid = "^
   9.190  		LargeWord.toString (Posix.Process.pidToWord childpid)^"\n");
   9.191 -	      killWatcher childpid; reapWatcher (childpid,childin, childout); ())
   9.192 +	      killWatcher childpid; reapWatcher (childpid,childin, childout))
   9.193  	    else ())
   9.194 -     val sign = sign_of_thm thm
   9.195 -     val prems = prems_of thm
   9.196 -     val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   9.197 -     val _ = debug ("subgoals forked to createWatcher: "^prems_string);
   9.198 -(*FIXME: do we need an E proofHandler??*)
   9.199 -     fun vampire_proofHandler n =
   9.200 -	(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   9.201 -	 VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))               
   9.202 -     fun spass_proofHandler n = (
   9.203 -       let val _ = File.append (File.tmp_path (Path.basic "spass_signal"))
   9.204 -                               "Starting SPASS signal handler\n"
   9.205 -	   val (reconstr, goalstring) = SpassComm.getSpassInput childin
   9.206 -	   val _ = File.append (File.tmp_path (Path.basic "spass_signal"))
   9.207 -		       ("In SPASS signal handler "^reconstr^goalstring^
   9.208 -		       "goals_being_watched: "^ string_of_int (!goals_being_watched))
   9.209 +     val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
   9.210 +     fun proofHandler n = 
   9.211 +       let val outcome = TextIO.inputLine childin
   9.212 +	   val goalstring = TextIO.inputLine childin
   9.213 +	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
   9.214 +		        "\"\ngoalstring = " ^ goalstring ^
   9.215 +		        "\ngoals_being_watched: "^ string_of_int (!goals_being_watched))
   9.216         in (* if a proof has been found and sent back as a reconstruction proof *)
   9.217 -	 if substring (reconstr, 0,1) = "["
   9.218 +	 if String.isPrefix "[" outcome
   9.219  	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   9.220 -	       Recon_Transfer.apply_res_thm reconstr goalstring;
   9.221 +	       Recon_Transfer.apply_res_thm outcome goalstring;
   9.222  	       Pretty.writeln(Pretty.str  (oct_char "361"));
   9.223  	       decr_watched())
   9.224 -	 (* if there's no proof, but a message from Spass *)
   9.225 -	 else if substring (reconstr, 0,5) = "SPASS"
   9.226 +	 (* if there's no proof, but a message from the signalling process*)
   9.227 +	 else if String.isPrefix "Invalid" outcome
   9.228  	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   9.229 -	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
   9.230 +	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) 
   9.231 +	       ^ "is not provable"));
   9.232 +	       Pretty.writeln(Pretty.str  (oct_char "361"));
   9.233 +	       decr_watched())
   9.234 +	 else if String.isPrefix "Failure" outcome
   9.235 +	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   9.236 +	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) 
   9.237 +	       ^ "proof attempt failed"));
   9.238  	       Pretty.writeln(Pretty.str  (oct_char "361"));
   9.239  	       decr_watched()) 
   9.240  	(* print out a list of rules used from clasimpset*)
   9.241 -	 else if substring (reconstr, 0,5) = "Rules"
   9.242 +	 else if String.isPrefix "Success" outcome
   9.243  	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   9.244 -	       Pretty.writeln(Pretty.str (goalstring^reconstr));
   9.245 +	       Pretty.writeln(Pretty.str (goalstring^outcome));
   9.246  	       Pretty.writeln(Pretty.str  (oct_char "361"));
   9.247  	       decr_watched())
   9.248  	  (* if proof translation failed *)
   9.249 -	 else if substring (reconstr, 0,5) = "Proof"
   9.250 +	 else if String.isPrefix "Translation failed" outcome
   9.251  	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   9.252 -	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   9.253 -	       Pretty.writeln(Pretty.str  (oct_char "361"));
   9.254 -	       decr_watched())
   9.255 -	 else if substring (reconstr, 0,1) = "%"
   9.256 -	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   9.257 -	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   9.258 +	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks outcome)));
   9.259  	       Pretty.writeln(Pretty.str  (oct_char "361"));
   9.260  	       decr_watched())
   9.261 -	 else  (* add something here ?*)
   9.262 +	 else  
   9.263  	      (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   9.264 -	       Pretty.writeln(Pretty.str ("Ran out of options in handler"));
   9.265 +	       Pretty.writeln(Pretty.str ("System error in proof handler"));
   9.266  	       Pretty.writeln(Pretty.str  (oct_char "361"));
   9.267  	       decr_watched())
   9.268 -       end)
   9.269 -
   9.270 - in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   9.271 -    IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   9.272 +       end
   9.273 + in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
   9.274      (childin, childout, childpid)
   9.275 -
   9.276    end
   9.277  
   9.278  end (* structure Watcher *)
    10.1 --- a/src/HOL/Tools/res_atp.ML	Mon Sep 19 14:20:45 2005 +0200
    10.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Sep 19 15:12:13 2005 +0200
    10.3 @@ -9,24 +9,30 @@
    10.4  sig
    10.5    val prover: string ref
    10.6    val custom_spass: string list ref
    10.7 +  val destdir: string ref
    10.8    val hook_count: int ref
    10.9 +  val problem_name: string ref
   10.10  end;
   10.11  
   10.12  structure ResAtp: RES_ATP =
   10.13  struct
   10.14  
   10.15 -
   10.16  val call_atp = ref false;
   10.17  val hook_count = ref 0;
   10.18  
   10.19 -fun debug_tac tac = (debug "testing"; tac);
   10.20 -
   10.21  val prover = ref "E";   (* use E as the default prover *)
   10.22  val custom_spass =   (*specialized options for SPASS*)
   10.23        ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
   10.24             "-DocProof","-TimeLimit=60"];
   10.25  
   10.26 -val prob_file = File.tmp_path (Path.basic "prob");
   10.27 +val destdir = ref "";   (*Empty means write files to /tmp*)
   10.28 +val problem_name = ref "prob";
   10.29 +
   10.30 +fun prob_pathname() = 
   10.31 +  if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
   10.32 +  else if File.exists (File.unpack_platform_path (!destdir))
   10.33 +  then !destdir ^ "/" ^ !problem_name
   10.34 +  else error ("No such directory: " ^ !destdir);
   10.35  
   10.36  
   10.37  (**** for Isabelle/ML interface  ****)
   10.38 @@ -68,7 +74,7 @@
   10.39        val _ = debug ("in tptp_inputs_tfrees 2")
   10.40        val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss)
   10.41        val _ = debug ("in tptp_inputs_tfrees 3")
   10.42 -      val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
   10.43 +      val probfile = prob_pathname() ^ "_" ^ string_of_int n
   10.44        val out = TextIO.openOut(probfile)
   10.45      in
   10.46        ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
   10.47 @@ -85,7 +91,7 @@
   10.48  
   10.49  fun dfg_inputs_tfrees thms n axclauses = 
   10.50      let val clss = map (ResClause.make_conjecture_clause_thm) thms
   10.51 -        val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
   10.52 +        val probfile = prob_pathname() ^ "_" ^ (string_of_int n)
   10.53          val _ = debug ("about to write out dfg prob file " ^ probfile)
   10.54          val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
   10.55                          axclauses [] [] []    
   10.56 @@ -108,7 +114,7 @@
   10.57              val goalstring = proofstring (Sign.string_of_term sign sg_term)
   10.58              val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
   10.59  
   10.60 -            val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
   10.61 +            val probfile = prob_pathname() ^ "_" ^ string_of_int n
   10.62              val _ = debug ("prob file in watcher_call_provers is " ^ probfile)
   10.63            in
   10.64              (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
   10.65 @@ -116,7 +122,7 @@
   10.66              if !prover = "spass"
   10.67              then
   10.68                let val optionline = 
   10.69 -		      if !SpassComm.reconstruct 
   10.70 +		      if !AtpCommunication.reconstruct 
   10.71  		          (*Proof reconstruction works for only a limited set of 
   10.72  		            inference rules*)
   10.73                        then "-" ^ space_implode "%-" (!custom_spass)
   10.74 @@ -170,30 +176,31 @@
   10.75          ());
   10.76  
   10.77  
   10.78 +(*FIXME: WHAT IS THMS FOR????*)
   10.79 +
   10.80  (******************************************************************)
   10.81  (* called in Isar automatically                                   *)
   10.82  (* writes out the current clasimpset to a tptp file               *)
   10.83  (* turns off xsymbol at start of function, restoring it at end    *)
   10.84  (******************************************************************)
   10.85  (*FIX changed to clasimp_file *)
   10.86 -val isar_atp' = setmp print_mode [] 
   10.87 +val isar_atp = setmp print_mode [] 
   10.88   (fn (ctxt, thms, thm) =>
   10.89    if Thm.no_prems thm then ()
   10.90    else
   10.91      let
   10.92 -      val _= debug ("in isar_atp'")
   10.93 +      val _= debug ("in isar_atp")
   10.94        val thy = ProofContext.theory_of ctxt
   10.95        val prems = Thm.prems_of thm
   10.96        val thms_string = Meson.concat_with_and (map string_of_thm thms)
   10.97        val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
   10.98  
   10.99        (*set up variables for writing out the clasimps to a tptp file*)
  10.100 -      val (clause_arr, num_of_clauses, axclauses) =
  10.101 -        ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
  10.102 -      val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^
  10.103 -                  " clauses")
  10.104 -      val (childin, childout, pid) = 
  10.105 -          Watcher.createWatcher (thm, clause_arr, num_of_clauses)
  10.106 +      val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
  10.107 +              (*FIXME: hack!! need to consider relevance for all prems*)
  10.108 +      val _ = debug ("claset and simprules total clauses = " ^ 
  10.109 +                     string_of_int (Array.length clause_arr))
  10.110 +      val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr)
  10.111        val pid_string =
  10.112          string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
  10.113      in
  10.114 @@ -205,43 +212,17 @@
  10.115      end);
  10.116  
  10.117  val isar_atp_writeonly = setmp print_mode [] 
  10.118 - (fn (ctxt, thms, thm) =>
  10.119 + (fn (ctxt, thms: thm list, thm) =>
  10.120    if Thm.no_prems thm then ()
  10.121    else
  10.122 -    let
  10.123 -      val thy = ProofContext.theory_of ctxt
  10.124 -      val prems = Thm.prems_of thm
  10.125 -
  10.126 -      (*set up variables for writing out the clasimps to a tptp file*)
  10.127 -      val (clause_arr, num_of_clauses, axclauses) =
  10.128 -        ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
  10.129 +    let val prems = Thm.prems_of thm
  10.130 +        val (_, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
  10.131      in
  10.132        write_problem_files axclauses thm (length prems)
  10.133      end);
  10.134  
  10.135 -fun get_thms_cs claset =
  10.136 -  let val {safeEs, safeIs, hazEs, hazIs, ...} = rep_cs claset
  10.137 -  in safeEs @ safeIs @ hazEs @ hazIs end;
  10.138  
  10.139 -fun append_name name [] _ = []
  10.140 -  | append_name name (thm :: thms) k =
  10.141 -      Thm.name_thm ((name ^ "_" ^ string_of_int k), thm) :: append_name name thms (k + 1);
  10.142 -
  10.143 -fun append_names (name :: names) (thms :: thmss) =
  10.144 -  append_name name thms 0 :: append_names names thmss;
  10.145 -
  10.146 -fun get_thms_ss [] = []
  10.147 -  | get_thms_ss thms =
  10.148 -      let
  10.149 -        val names = map Thm.name_of_thm thms
  10.150 -        val thms' = map (mksimps mksimps_pairs) thms
  10.151 -        val thms'' = append_names names thms'
  10.152 -      in
  10.153 -        ResLib.flat_noDup thms''
  10.154 -      end;
  10.155 -
  10.156 -
  10.157 -(* convert locally declared rules to axiom clauses *)
  10.158 +(* convert locally declared rules to axiom clauses: UNUSED *)
  10.159  
  10.160  fun subtract_simpset thy ctxt =
  10.161    let
  10.162 @@ -265,12 +246,7 @@
  10.163      val proof = Toplevel.proof_of state
  10.164      val (ctxt, (_, goal)) = Proof.get_goal proof
  10.165          handle Proof.STATE _ => error "No goal present";
  10.166 -
  10.167      val thy = ProofContext.theory_of ctxt;
  10.168 -
  10.169 -    (* FIXME presently unused *)
  10.170 -    val ss_thms = subtract_simpset thy ctxt;
  10.171 -    val cs_thms = subtract_claset thy ctxt;
  10.172    in
  10.173      debug ("initial thm in isar_atp: " ^ 
  10.174             Pretty.string_of (ProofContext.pretty_thm ctxt goal));
  10.175 @@ -278,10 +254,12 @@
  10.176             Pretty.string_of (ProofContext.pretty_term ctxt
  10.177               (Logic.mk_conjunction_list (Thm.prems_of goal))));
  10.178      debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
  10.179 +    debug ("current theory: " ^ Context.theory_name thy);
  10.180      hook_count := !hook_count +1;
  10.181      debug ("in hook for time: " ^(string_of_int (!hook_count)) );
  10.182      ResClause.init thy;
  10.183 -    isar_atp' (ctxt, ProofContext.prems_of ctxt, goal)
  10.184 +    if !destdir = "" then isar_atp (ctxt, ProofContext.prems_of ctxt, goal)
  10.185 +    else isar_atp_writeonly (ctxt, ProofContext.prems_of ctxt, goal)
  10.186    end);
  10.187  
  10.188  val call_atpP =
    11.1 --- a/src/HOL/Tools/res_axioms.ML	Mon Sep 19 14:20:45 2005 +0200
    11.2 +++ b/src/HOL/Tools/res_axioms.ML	Mon Sep 19 15:12:13 2005 +0200
    11.3 @@ -18,7 +18,10 @@
    11.4    val rm_Eps : (term * term) list -> thm list -> term list
    11.5    val claset_rules_of_thy : theory -> (string * thm) list
    11.6    val simpset_rules_of_thy : theory -> (string * thm) list
    11.7 -  val clausify_rules_pairs : (string*thm) list -> thm list -> (ResClause.clause*thm) list list * thm list
    11.8 +  val claset_rules_of_ctxt: Proof.context -> (string * thm) list
    11.9 +  val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
   11.10 +  val clausify_rules_pairs : 
   11.11 +        (string*thm) list -> thm list -> (ResClause.clause*thm) list list * thm list
   11.12    val clause_setup : (theory -> theory) list
   11.13    val meson_method_setup : (theory -> theory) list
   11.14    end;
   11.15 @@ -357,19 +360,31 @@
   11.16  val tag_intro = preserve_name (fn th => th RS tagI);
   11.17  val tag_elim  = preserve_name (fn th => tagD RS th);
   11.18  
   11.19 -fun claset_rules_of_thy thy =
   11.20 -  let val cs = rep_cs (claset_of thy)
   11.21 -      val intros = (#safeIs cs) @ (#hazIs cs)
   11.22 -      val elims  = (#safeEs cs) @ (#hazEs cs)
   11.23 +fun rules_of_claset cs =
   11.24 +  let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
   11.25 +      val intros = safeIs @ hazIs
   11.26 +      val elims  = safeEs @ hazEs
   11.27    in
   11.28 +     debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ 
   11.29 +            " elims: " ^ Int.toString(length elims));
   11.30       if tagging_enabled 
   11.31       then map pairname (map tag_intro intros @ map tag_elim elims)
   11.32 -     else map pairname (intros @  elims)
   11.33 +     else map pairname (intros @ elims)
   11.34    end;
   11.35  
   11.36 -fun simpset_rules_of_thy thy =
   11.37 -    let val rules = #rules (fst (rep_ss (simpset_of thy)))
   11.38 -    in map (fn r => (#name r, #thm r)) (Net.entries rules) end;
   11.39 +fun rules_of_simpset ss =
   11.40 +  let val ({rules,...}, _) = rep_ss ss
   11.41 +      val simps = Net.entries rules
   11.42 +  in 
   11.43 +      debug ("rules_of_simpset: " ^ Int.toString(length simps));
   11.44 +      map (fn r => (#name r, #thm r)) simps
   11.45 +  end;
   11.46 +
   11.47 +fun claset_rules_of_thy thy = rules_of_claset (claset_of thy);
   11.48 +fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy);
   11.49 +
   11.50 +fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt);
   11.51 +fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt);
   11.52  
   11.53  
   11.54  (**** Translate a set of classical/simplifier rules into CNF (still as type "thm")  ****)