improved process handling. tidied
authorpaulson
Wed Oct 05 11:18:06 2005 +0200 (2005-10-05)
changeset 17764fde495b9e24b
parent 17763 6f933b702f44
child 17765 e3cd31bc2e40
improved process handling. tidied
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_lib.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Oct 05 10:56:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Oct 05 11:18:06 2005 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4      let val consts = consts_in_goal goal
     1.5  	fun relevant_axioms_aux1 cs k =
     1.6  	    let val thms1 = axioms_having_consts cs thmTab
     1.7 -		val cs1 = ResLib.flat_noDup (map consts_of_thm thms1)
     1.8 +		val cs1 = foldl (op union_string) [] (map consts_of_thm thms1)
     1.9  	    in
    1.10  		if ((cs1 subset cs) orelse n <= k) then (k,thms1) 
    1.11  		else (relevant_axioms_aux1 (cs1 union cs) (k+1))
     2.1 --- a/src/HOL/Tools/ATP/watcher.ML	Wed Oct 05 10:56:06 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Oct 05 11:18:06 2005 +0200
     2.3 @@ -4,14 +4,11 @@
     2.4      Copyright   2004  University of Cambridge
     2.5   *)
     2.6  
     2.7 - (***************************************************************************)
     2.8 - (*  The watcher process starts a resolution process when it receives a     *)
     2.9 +(*  The watcher process starts a resolution process when it receives a     *)
    2.10  (*  message from Isabelle                                                  *)
    2.11  (*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    2.12  (*  and removes dead processes.  Also possible to kill all the resolution  *)
    2.13  (*  processes currently running.                                           *)
    2.14 -(*  Hardwired version of where to pick up the tptp files for the moment    *)
    2.15 -(***************************************************************************)
    2.16  
    2.17  signature WATCHER =
    2.18  sig
    2.19 @@ -23,17 +20,15 @@
    2.20      TextIO.outstream * (string*string*string*string*string) list 
    2.21      -> unit
    2.22  
    2.23 -(* Send message to watcher to kill currently running resolution provers *)
    2.24 +(* Send message to watcher to kill resolution provers *)
    2.25  val callSlayer : TextIO.outstream -> unit
    2.26  
    2.27  (* Start a watcher and set up signal handlers             *)
    2.28  val createWatcher : 
    2.29      thm * (ResClause.clause * thm) Array.array -> 
    2.30      TextIO.instream * TextIO.outstream * Posix.Process.pid
    2.31 -
    2.32 -(* Kill watcher process                                   *)
    2.33  val killWatcher : Posix.Process.pid -> unit
    2.34 -val killWatcher' : int -> unit
    2.35 +val setting_sep : char
    2.36  end
    2.37  
    2.38  
    2.39 @@ -41,6 +36,10 @@
    2.40  structure Watcher: WATCHER =
    2.41  struct
    2.42  
    2.43 +(*Field separators, used to pack items onto a text line*)
    2.44 +val command_sep = #"\t"
    2.45 +and setting_sep = #"%";
    2.46 +
    2.47  open Recon_Transfer
    2.48  
    2.49  val goals_being_watched = ref 0;
    2.50 @@ -134,8 +133,6 @@
    2.51  (*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
    2.52  (*****************************************************************************************)
    2.53  
    2.54 -    
    2.55 -(*Uses the $-character to separate items sent to watcher*)
    2.56  fun callResProvers (toWatcherStr,  []) = 
    2.57        (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
    2.58  |   callResProvers (toWatcherStr,
    2.59 @@ -144,9 +141,11 @@
    2.60        let val _ = trace (space_implode "\n" 
    2.61  		         (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
    2.62  			  probfile]))
    2.63 -      in TextIO.output (toWatcherStr,    
    2.64 -                        prover^"$"^proverCmd^"$"^ settings^"$"^probfile^"$\n");
    2.65 -         TextIO.output (toWatcherStr, String.toString goalstring^"\n");
    2.66 +      in TextIO.output (toWatcherStr,
    2.67 +                        (*Uses a special character to separate items sent to watcher*)
    2.68 +      	                space_implode (str command_sep)
    2.69 +                          [prover, proverCmd, settings, probfile,
    2.70 +                           String.toString goalstring ^ "\n"]);
    2.71                (*goalstring is a single string literal, with all specials escaped.*)
    2.72           goals_being_watched := (!goals_being_watched) + 1;
    2.73  	 TextIO.flushOut toWatcherStr;
    2.74 @@ -155,31 +154,29 @@
    2.75                                                  
    2.76                                      
    2.77   
    2.78 -(**************************************************************)
    2.79 -(* Send message to watcher to kill currently running vampires *)
    2.80 -(**************************************************************)
    2.81  
    2.82 -fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n"); 
    2.83 +(*Send message to watcher to kill currently running vampires. NOT USED and possibly
    2.84 +  buggy. Note that killWatcher kills the entire process group anyway.*)
    2.85 +fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n"); 
    2.86                              TextIO.flushOut toWatcherStr)
    2.87  
    2.88                      
    2.89  (**************************************************************)
    2.90  (* Get commands from Isabelle                                 *)
    2.91  (**************************************************************)
    2.92 -fun getCmds (toParentStr,fromParentStr, cmdList) = 
    2.93 +fun getCmds (toParentStr, fromParentStr, cmdList) = 
    2.94    let val thisLine = TextIO.inputLine fromParentStr 
    2.95 -      val _ = trace("\nGot command from parent: " ^ thisLine)
    2.96    in
    2.97 +     trace("\nGot command from parent: " ^ thisLine);
    2.98       if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
    2.99       else if thisLine = "Kill children\n"
   2.100 -     then (TextIO.output (toParentStr,thisLine ); 
   2.101 +     then (TextIO.output (toParentStr,thisLine); 
   2.102  	   TextIO.flushOut toParentStr;
   2.103 -	   (("","","Kill children",[],"")::cmdList)  )
   2.104 +	   [("","","Kill children",[],"")])
   2.105       else
   2.106 -       let val [prover,proverCmd,settingstr,probfile,_] = 
   2.107 -                   String.tokens (fn c => c = #"$") thisLine
   2.108 -           val settings = String.tokens (fn c => c = #"%") settingstr
   2.109 -	   val goalstring = TextIO.inputLine fromParentStr 
   2.110 +       let val [prover,proverCmd,settingstr,probfile,goalstring] = 
   2.111 +                   String.tokens (fn c => c = command_sep) thisLine
   2.112 +           val settings = String.tokens (fn c => c = setting_sep) settingstr
   2.113         in
   2.114             trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd^
   2.115                    "  problem file: " ^ probfile ^ 
   2.116 @@ -187,6 +184,9 @@
   2.117             getCmds (toParentStr, fromParentStr, 
   2.118                      (prover, goalstring, proverCmd, settings, probfile)::cmdList) 
   2.119         end
   2.120 +       handle Bind => 
   2.121 +          (trace "getCmds: command parsing failed!";
   2.122 +           getCmds (toParentStr, fromParentStr, cmdList))
   2.123    end
   2.124  	    
   2.125                                                                    
   2.126 @@ -212,8 +212,6 @@
   2.127  (*  Set up a Watcher Process         *)
   2.128  (*************************************)
   2.129  
   2.130 -fun getProofCmd (a,c,d,e,f) = d
   2.131 -
   2.132  (* for tracing: encloses each string element in brackets. *)
   2.133  val concat_with_and = space_implode " & " o map (enclose "(" ")");
   2.134  
   2.135 @@ -246,40 +244,34 @@
   2.136  
   2.137  fun setupWatcher (thm,clause_arr) = 
   2.138    let
   2.139 -    (** pipes for communication between parent and watcher **)
   2.140 -    val p1 = Posix.IO.pipe ()
   2.141 +    val p1 = Posix.IO.pipe ()   (** pipes for communication between parent and watcher **)
   2.142      val p2 = Posix.IO.pipe ()
   2.143      fun closep () = 
   2.144 -	 (Posix.IO.close (#outfd p1); 
   2.145 -	  Posix.IO.close (#infd p1);
   2.146 -	  Posix.IO.close (#outfd p2); 
   2.147 -	  Posix.IO.close (#infd p2))
   2.148 -    (***********************************************************)
   2.149 -    (****** fork a watcher process and get it set up and going *)
   2.150 -    (***********************************************************)
   2.151 +	 (Posix.IO.close (#outfd p1); Posix.IO.close (#infd p1);
   2.152 +	  Posix.IO.close (#outfd p2); Posix.IO.close (#infd p2))
   2.153 +    (****** fork a watcher process and get it set up and going ******)
   2.154      fun startWatcher procList =
   2.155 -     (case  Posix.Process.fork() (***************************************)
   2.156 -      of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   2.157 -				    (***************************************)
   2.158 -
   2.159 -				      (*************************)
   2.160 -       | NONE => let                  (* child - i.e. watcher  *)
   2.161 -	  val oldchildin = #infd p1   (*************************)
   2.162 +     (case  Posix.Process.fork() 
   2.163 +      of SOME pid => pid (* parent - i.e. main Isabelle process *)
   2.164 +       | NONE => let                (* child - i.e. watcher  *)
   2.165 +	  val oldchildin = #infd p1  
   2.166  	  val fromParent = Posix.FileSys.wordToFD 0w0
   2.167  	  val oldchildout = #outfd p2
   2.168  	  val toParent = Posix.FileSys.wordToFD 0w1
   2.169  	  val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   2.170  	  val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   2.171  	  val toParentStr = openOutFD ("_exec_out_parent", toParent)
   2.172 -	  val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   2.173 +	  val pid = Posix.ProcEnv.getpid()
   2.174 +	  val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
   2.175 +                   (*set process group id: allows killing all children*)
   2.176 +	  val () = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   2.177  	 
   2.178  	  fun pollChildInput fromStr = 
   2.179  	     case getInIoDesc fromStr of
   2.180  	       SOME iod => 
   2.181  		 (case OS.IO.pollDesc iod of
   2.182  		    SOME pd =>
   2.183 -			let val pd' = OS.IO.pollIn pd
   2.184 -			in
   2.185 +			let val pd' = OS.IO.pollIn pd in
   2.186  			  case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
   2.187  			      [] => false
   2.188  			    | pd''::_ => OS.IO.isIn pd''
   2.189 @@ -287,7 +279,6 @@
   2.190  		   | NONE => false)
   2.191  	     | NONE => false
   2.192  
   2.193 -
   2.194  	  (* Check all ATP processes currently running for output                 *)
   2.195  	  fun checkChildren ([], toParentStr) = []  (* no children to check *)
   2.196  	  |   checkChildren (childProc::otherChildren, toParentStr) = 
   2.197 @@ -295,8 +286,7 @@
   2.198  			          Int.toString (length (childProc::otherChildren)))
   2.199  		   val (childInput,childOutput) = cmdstreamsOf childProc
   2.200  		   val child_handle = cmdchildHandle childProc
   2.201 -		   (* childCmd is the file that the problem is in *)
   2.202 -		   val childCmd = fst(snd (cmdchildInfo childProc))
   2.203 +		   val childCmd = #1(#2(cmdchildInfo childProc)) (*name of problem file*)
   2.204  		   val _ = trace ("\nchildCmd = " ^ childCmd)
   2.205  		   val sg_num = number_from_filename childCmd
   2.206  		   val childIncoming = pollChildInput childInput
   2.207 @@ -307,10 +297,8 @@
   2.208  	       in 
   2.209  		 trace("\nsubgoals forked to checkChildren: " ^ goalstring);
   2.210  		 if childIncoming
   2.211 -		 then 
   2.212 -		   (* check here for prover label on child*)
   2.213 -		   let val _ = trace ("\nInput available from child: " ^
   2.214 -				      childCmd ^ 
   2.215 +		 then (* check here for prover label on child*)
   2.216 +		   let val _ = trace ("\nInput available from child: " ^ childCmd ^ 
   2.217  				      "\ngoalstring is " ^ goalstring)
   2.218  		       val childDone = (case prover of
   2.219  			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
   2.220 @@ -331,138 +319,90 @@
   2.221  	       end
   2.222  
   2.223  	
   2.224 -     (********************************************************************)                  
   2.225 -     (* call resolution processes                                        *)
   2.226 -     (* settings should be a list of strings                             *)
   2.227 -     (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
   2.228 -     (* takes list of (string, string, string list, string)list proclist *)
   2.229 -     (********************************************************************)
   2.230 -
   2.231 -
   2.232 -(*** add subgoal id num to this *)
   2.233 -	fun execCmds  [] procList = procList
   2.234 -	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   2.235 -	      let val _ = trace 
   2.236 -	                    (space_implode "\n" 
   2.237 -	                      (["\nAbout to execute command for goal:",
   2.238 -	                        goalstring, proverCmd] @ settings @
   2.239 -	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   2.240 +	(* call resolution processes                                        *)
   2.241 +	(* settings should be a list of strings  ["-t 300", "-m 100000"]    *)
   2.242 +	(* takes list of (string, string, string list, string)list proclist *)
   2.243 +	fun execCmds [] procList = procList
   2.244 +	|   execCmds ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   2.245 +	      let val _ = trace (space_implode "\n" 
   2.246 +				 (["\nAbout to execute command for goal:",
   2.247 +				   goalstring, proverCmd] @ settings @
   2.248 +				  [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   2.249  	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   2.250 -		       (Unix.execute(proverCmd, (settings@[file])))
   2.251 +		       Unix.execute(proverCmd, settings@[file])
   2.252  		  val (instr, outstr) = Unix.streamsOf childhandle
   2.253 -		  val newProcList = (CMDPROC{
   2.254 -				       prover = prover,
   2.255 -				       cmd = file,
   2.256 -				       goalstring = goalstring,
   2.257 -				       proc_handle = childhandle,
   2.258 -				       instr = instr,
   2.259 -				       outstr = outstr }) :: procList
   2.260 +		  val newProcList = CMDPROC{prover = prover,
   2.261 +					    cmd = file,
   2.262 +					    goalstring = goalstring,
   2.263 +					    proc_handle = childhandle,
   2.264 +					    instr = instr,
   2.265 +					    outstr = outstr} :: procList
   2.266       
   2.267  		  val _ = trace ("\nFinished at " ^
   2.268  			         Date.toString(Date.fromTimeLocal(Time.now())))
   2.269  	      in execCmds cmds newProcList end
   2.270  
   2.271 -
   2.272 -     (****************************************)                  
   2.273 -     (* call resolution processes remotely   *)
   2.274 -     (* settings should be a list of strings *)
   2.275 -     (* e.g. ["-t300", "-m100000"]         *)
   2.276 -     (****************************************)
   2.277 -
   2.278 -      (*  fun execRemoteCmds  [] procList = procList
   2.279 -	|   execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList  =  
   2.280 -	      let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   2.281 -		  in
   2.282 -		       execRemoteCmds  cmds newProcList
   2.283 -		  end
   2.284 -*)
   2.285 -
   2.286 -     (**********************************************)                  
   2.287 -     (* Watcher Loop                               *)
   2.288 -     (**********************************************)
   2.289 -         val iterations_left = ref 500;  (*don't let it run forever*)
   2.290 +         (******** Watcher Loop ********)
   2.291 +         val limit = ref 500;  (*don't let it run forever*)
   2.292  
   2.293  	 fun keepWatching (procList) = 
   2.294  	   let fun loop procList =  
   2.295 -		let val _ = trace ("\nCalling pollParentInput: " ^ 
   2.296 -			           Int.toString (!iterations_left));
   2.297 -		    val cmdsFromIsa = pollParentInput 
   2.298 -		                       (fromParentIOD, fromParentStr, toParentStr)
   2.299 -		in 
   2.300 -		   OS.Process.sleep (Time.fromMilliseconds 100);
   2.301 -		   iterations_left := !iterations_left - 1;
   2.302 -		   if !iterations_left <= 0 
   2.303 -		   then 
   2.304 -		    (trace "\nTimeout: Killing proof processes";
   2.305 -	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   2.306 -		     TextIO.flushOut toParentStr;
   2.307 -		     killChildren (map cmdchildHandle procList);
   2.308 -		     exit 0)
   2.309 -		   else if isSome cmdsFromIsa
   2.310 -		   then (*  deal with input from Isabelle *)
   2.311 -		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
   2.312 -		     then 
   2.313 +	      let val _ = trace ("\nCalling pollParentInput: " ^ Int.toString (!limit));
   2.314 +		  val cmdsFromIsa = pollParentInput 
   2.315 +				     (fromParentIOD, fromParentStr, toParentStr)
   2.316 +	      in 
   2.317 +		 OS.Process.sleep (Time.fromMilliseconds 100);
   2.318 +		 limit := !limit - 1;
   2.319 +		 if !limit = 0 
   2.320 +		 then 
   2.321 +		  (trace "\nTimeout: Killing proof processes";
   2.322 +		   TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   2.323 +		   TextIO.flushOut toParentStr;
   2.324 +		   killChildren (map cmdchildHandle procList);
   2.325 +		   exit 0)
   2.326 +		 else case cmdsFromIsa of
   2.327 +		     SOME [(_,_,"Kill children",_,_)] => 
   2.328  		       let val child_handles = map cmdchildHandle procList 
   2.329 -		       in
   2.330 -			  killChildren child_handles;
   2.331 -			  loop []
   2.332 -		       end
   2.333 -		     else
   2.334 -		       if length procList < 5     (********************)
   2.335 +		       in  killChildren child_handles; loop []  end
   2.336 +		   | SOME cmds => (*  deal with commands from Isabelle process *)
   2.337 +		       if length procList < 40
   2.338  		       then                        (* Execute locally  *)
   2.339  			 let 
   2.340 -			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   2.341 -			   val _ = Posix.ProcEnv.getppid()
   2.342 -			   val _ = trace "\nJust execed a child"
   2.343 +			   val newProcList = execCmds cmds procList
   2.344  			   val newProcList' = checkChildren (newProcList, toParentStr) 
   2.345  			 in
   2.346 -			   trace ("\nOff to keep watching: " ^ 
   2.347 -			          Int.toString (!iterations_left));
   2.348 -			   loop newProcList'
   2.349 +			   trace "\nJust execed a child"; loop newProcList'
   2.350  			 end
   2.351 -		       else  (* Execute remotely              *)
   2.352 -			     (* (actually not remote for now )*)
   2.353 +		       else  (* Execute remotely [FIXME: NOT REALLY]  *)
   2.354  			 let 
   2.355 -			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   2.356 -			   val _ = Posix.ProcEnv.getppid()
   2.357 -			   val newProcList' =checkChildren (newProcList, toParentStr) 
   2.358 -			 in
   2.359 -			   loop newProcList'
   2.360 -			 end
   2.361 -		   else (* No new input from Isabelle *)
   2.362 -		     let val newProcList = checkChildren (procList, toParentStr)
   2.363 -		     in
   2.364 -		       trace ("\nNo new input, still watching: " ^ 
   2.365 -			      Int.toString (!iterations_left));
   2.366 -		       loop newProcList
   2.367 -		     end
   2.368 -		 end
   2.369 +			   val newProcList = execCmds cmds procList
   2.370 +			   val newProcList' = checkChildren (newProcList, toParentStr) 
   2.371 +			 in loop newProcList' end
   2.372 +		   | NONE => (* No new input from Isabelle *)
   2.373 +		       let val newProcList = checkChildren (procList, toParentStr)
   2.374 +		       in
   2.375 +			 trace "\nNo new input, still watching"; loop newProcList
   2.376 +		       end
   2.377 +	       end
   2.378  	   in  
   2.379  	       loop procList
   2.380  	   end
   2.381  	   
   2.382  
   2.383 -	   in
   2.384 -	    (***************************)
   2.385 -	    (*** Sort out pipes ********)
   2.386 -	    (***************************)
   2.387 +	 in
   2.388 +	  (*** Sort out pipes ********)
   2.389 +	   Posix.IO.close (#outfd p1);
   2.390 +	   Posix.IO.close (#infd p2);
   2.391 +	   Posix.IO.dup2{old = oldchildin, new = fromParent};
   2.392 +	   Posix.IO.close oldchildin;
   2.393 +	   Posix.IO.dup2{old = oldchildout, new = toParent};
   2.394 +	   Posix.IO.close oldchildout;
   2.395  
   2.396 -	     Posix.IO.close (#outfd p1);
   2.397 -	     Posix.IO.close (#infd p2);
   2.398 -	     Posix.IO.dup2{old = oldchildin, new = fromParent};
   2.399 -	     Posix.IO.close oldchildin;
   2.400 -	     Posix.IO.dup2{old = oldchildout, new = toParent};
   2.401 -	     Posix.IO.close oldchildout;
   2.402 -
   2.403 -	     (***************************)
   2.404 -	     (* start the watcher loop  *)
   2.405 -	     (***************************)
   2.406 -	     keepWatching (procList);
   2.407 -	     (****************************************************************************)
   2.408 -(* fake return value - actually want the watcher to loop until killed *)
   2.409 -	     (****************************************************************************)
   2.410 -	     Posix.Process.wordToPid 0w0
   2.411 -	   end);
   2.412 +	   (* start the watcher loop  *)
   2.413 +	   keepWatching (procList);
   2.414 +	   (* fake return value - actually want the watcher to loop until killed *)
   2.415 +	   Posix.Process.wordToPid 0w0
   2.416 +	 end);
   2.417       (* end case *)
   2.418  
   2.419  
   2.420 @@ -503,9 +443,7 @@
   2.421  (* Start a watcher and set up signal handlers             *)
   2.422  (**********************************************************)
   2.423  
   2.424 -fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   2.425 -
   2.426 -val killWatcher' = killWatcher o ResLib.pidOfInt;
   2.427 +fun killWatcher pid = Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
   2.428  
   2.429  fun reapWatcher(pid, instr, outstr) =
   2.430    (TextIO.closeIn instr; TextIO.closeOut outstr;
     3.1 --- a/src/HOL/Tools/res_atp.ML	Wed Oct 05 10:56:06 2005 +0200
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Oct 05 11:18:06 2005 +0200
     3.3 @@ -50,6 +50,8 @@
     3.4  (* a special version of repeat_RS *)
     3.5  fun repeat_someI_ex th = repeat_RS th someI_ex;
     3.6  
     3.7 +fun writeln_strs _   []      = ()
     3.8 +  | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
     3.9  
    3.10  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
    3.11  fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
    3.12 @@ -61,8 +63,8 @@
    3.13        val arity_cls = map ResClause.tptp_arity_clause arity_clauses
    3.14        val out = TextIO.openOut(pf n)
    3.15      in
    3.16 -      ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    3.17 -      ResLib.writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
    3.18 +      writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    3.19 +      writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
    3.20        TextIO.closeOut out
    3.21      end;
    3.22  
    3.23 @@ -74,7 +76,7 @@
    3.24                          axclauses [] [] []    
    3.25  	val out = TextIO.openOut(pf n)
    3.26      in
    3.27 -	ResLib.writeln_strs out [probN]; TextIO.closeOut out
    3.28 +	writeln_strs out [probN]; TextIO.closeOut out
    3.29      end;
    3.30  
    3.31  
    3.32 @@ -82,19 +84,20 @@
    3.33  (* call prover with settings and problem file for the current subgoal *)
    3.34  (*********************************************************************)
    3.35  (* now passing in list of skolemized thms and list of sgterms to go with them *)
    3.36 -fun watcher_call_provers sign sg_terms (childin, childout,pid) =
    3.37 +fun watcher_call_provers sign sg_terms (childin, childout, pid) =
    3.38    let
    3.39      fun make_atp_list [] n = []
    3.40        | make_atp_list (sg_term::xs) n =
    3.41            let
    3.42              val goalstring = Sign.string_of_term sign sg_term
    3.43 -            val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
    3.44              val probfile = prob_pathname n
    3.45              val time = Int.toString (!time_limit)
    3.46 -            val _ = debug ("problem file in watcher_call_provers is " ^ probfile)
    3.47            in
    3.48 +            debug ("goalstring in make_atp_lists is\n" ^ goalstring);
    3.49 +            debug ("problem file in watcher_call_provers is " ^ probfile);
    3.50              (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
    3.51                versions of Unix.execute treat them differently!*)
    3.52 +            (*options are separated by Watcher.setting_sep, currently #"%"*)
    3.53              if !prover = "spass"
    3.54              then
    3.55                let val optionline = 
    3.56 @@ -165,7 +168,8 @@
    3.57  	    ())
    3.58        in writenext (length prems); clause_arr end;
    3.59  
    3.60 -val last_watcher_pid = ref (NONE : Posix.Process.pid option);
    3.61 +val last_watcher_pid =
    3.62 +  ref (NONE : (TextIO.instream * TextIO.outstream * Posix.Process.pid) option);
    3.63  
    3.64  
    3.65  (*writes out the current clasimpset to a tptp file;
    3.66 @@ -175,8 +179,13 @@
    3.67    if Thm.no_prems th then ()
    3.68    else
    3.69      let
    3.70 +      val _ = (*Set up signal handler to tidy away dead processes*)
    3.71 +	      IsaSignal.signal (IsaSignal.chld, 
    3.72 +	        IsaSignal.SIG_HANDLE (fn _ =>
    3.73 +		  (Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []);
    3.74 +		   debug "Child signal received\n")));  
    3.75        val _ = (case !last_watcher_pid of NONE => ()
    3.76 -               | SOME pid => (*FIXME: should kill ATP processes too; at least they time out*)
    3.77 +               | SOME (_, childout, pid) => 
    3.78                    (debug ("Killing old watcher, pid = " ^ 
    3.79                            Int.toString (ResLib.intOfPid pid));
    3.80                     Watcher.killWatcher pid))
    3.81 @@ -184,7 +193,7 @@
    3.82        val clause_arr = write_problem_files prob_pathname (ctxt,th)
    3.83        val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr)
    3.84      in
    3.85 -      last_watcher_pid := SOME pid;
    3.86 +      last_watcher_pid := SOME (childin, childout, pid);
    3.87        debug ("proof state: " ^ string_of_thm th);
    3.88        debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
    3.89        watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
    3.90 @@ -208,9 +217,9 @@
    3.91          handle Proof.STATE _ => error "No goal present";
    3.92      val thy = ProofContext.theory_of ctxt;
    3.93    in
    3.94 -    debug ("initial thm in isar_atp: " ^ 
    3.95 +    debug ("initial thm in isar_atp:\n" ^ 
    3.96             Pretty.string_of (ProofContext.pretty_thm ctxt goal));
    3.97 -    debug ("subgoals in isar_atp: " ^ 
    3.98 +    debug ("subgoals in isar_atp:\n" ^ 
    3.99             Pretty.string_of (ProofContext.pretty_term ctxt
   3.100               (Logic.mk_conjunction_list (Thm.prems_of goal))));
   3.101      debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal));
     4.1 --- a/src/HOL/Tools/res_clause.ML	Wed Oct 05 10:56:06 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Oct 05 11:18:06 2005 +0200
     4.3 @@ -32,7 +32,6 @@
     4.4    val isTaut : clause -> bool
     4.5    val num_of_clauses : clause -> int
     4.6  
     4.7 -  val dfg_clauses2str : string list -> string
     4.8    val clause2dfg : clause -> string * string list
     4.9    val clauses2dfg : clause list -> string -> clause list -> clause list ->
    4.10  	   (string * int) list -> (string * int) list -> string
    4.11 @@ -41,7 +40,6 @@
    4.12    val tptp_arity_clause : arityClause -> string
    4.13    val tptp_classrelClause : classrelClause -> string
    4.14    val tptp_clause : clause -> string list
    4.15 -  val tptp_clauses2str : string list -> string
    4.16    val clause2tptp : clause -> string * string list
    4.17    val tfree_clause : string -> string
    4.18    val schematic_var_prefix : string
    4.19 @@ -293,11 +291,11 @@
    4.20  	  val funcs' = ResLib.flat_noDup funcslist
    4.21  	  val t = make_fixed_type_const a
    4.22        in    
    4.23 -	  ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs') )
    4.24 +	  ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs'))
    4.25        end
    4.26    | type_of (TFree (a, s)) = 
    4.27        let val t = make_fixed_type_var a
    4.28 -      in (t, ([((FOLTFree a),s)],[(t,0)]) ) end
    4.29 +      in (t, ([((FOLTFree a),s)],[(t,0)])) end
    4.30    | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], []))
    4.31  
    4.32  
    4.33 @@ -617,7 +615,7 @@
    4.34  	 val conclLit = make_TConsLit(true,(res,tcons,tvars))
    4.35           val tvars_srts = ListPair.zip (tvars,args)
    4.36  	 val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts)
    4.37 -         val false_tvars_srts' = ResLib.pair_ins false tvars_srts'
    4.38 +         val false_tvars_srts' = map (pair false) tvars_srts'
    4.39  	 val premLits = map make_TVarLit false_tvars_srts'
    4.40       in
    4.41  	 make_arity_clause (cls_id,Axiom,conclLit,premLits)
    4.42 @@ -773,7 +771,7 @@
    4.43  |   uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT));
    4.44  
    4.45  fun mergelist [] = []
    4.46 -|   mergelist (x::xs ) = x @ mergelist xs
    4.47 +|   mergelist (x::xs) = x @ mergelist xs
    4.48  
    4.49  fun dfg_vars (Clause cls) =
    4.50      let val lits = #literals cls
    4.51 @@ -861,9 +859,6 @@
    4.52  
    4.53  fun string_of_end () = "end_problem.\n%------------------------------------------------------------------------------";
    4.54  
    4.55 -val delim = "\n";
    4.56 -val dfg_clauses2str = ResLib.list2str_sep delim; 
    4.57 -     
    4.58  
    4.59  fun clause2dfg cls =
    4.60      let val (lits,tfree_lits) = dfg_clause_aux cls 
    4.61 @@ -890,16 +885,16 @@
    4.62  fun gen_dfg_file probname axioms conjectures funcs preds = 
    4.63      let val axstrs_tfrees = (map clause2dfg axioms)
    4.64  	val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
    4.65 -        val axstr = ResLib.list2str_sep delim axstrs
    4.66 +        val axstr = (space_implode "\n" axstrs) ^ "\n\n"
    4.67          val conjstrs_tfrees = (map clause2dfg conjectures)
    4.68  	val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
    4.69          val tfree_clss = map tfree_dfg_clause (ResLib.flat_noDup atfrees) 
    4.70 -        val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs)
    4.71 +        val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n"
    4.72          val funcstr = string_of_funcs funcs
    4.73          val predstr = string_of_preds preds
    4.74      in
    4.75         (string_of_start probname) ^ (string_of_descrip ()) ^ 
    4.76 -       (string_of_symbols funcstr predstr ) ^  
    4.77 +       (string_of_symbols funcstr predstr) ^  
    4.78         (string_of_axioms axstr) ^
    4.79         (string_of_conjectures conjstr) ^ (string_of_end ())
    4.80      end;
    4.81 @@ -1042,9 +1037,6 @@
    4.82  fun tfree_clause tfree_lit =
    4.83      "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).";
    4.84  
    4.85 -val delim = "\n";
    4.86 -val tptp_clauses2str = ResLib.list2str_sep delim; 
    4.87 -     
    4.88  
    4.89  fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
    4.90        let val pol = if b then "++" else "--"
     5.1 --- a/src/HOL/Tools/res_lib.ML	Wed Oct 05 10:56:06 2005 +0200
     5.2 +++ b/src/HOL/Tools/res_lib.ML	Wed Oct 05 11:18:06 2005 +0200
     5.3 @@ -10,12 +10,8 @@
     5.4  sig
     5.5  val flat_noDup : ''a list list -> ''a list
     5.6  val helper_path : string -> string -> string
     5.7 -val list2str_sep : string -> string list -> string
     5.8  val no_rep_add : ''a -> ''a list -> ''a list
     5.9  val no_rep_app : ''a list -> ''a list -> ''a list
    5.10 -val pair_ins : 'a -> 'b list -> ('a * 'b) list
    5.11 -val write_strs : TextIO.outstream -> TextIO.vector list -> unit
    5.12 -val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
    5.13  val intOfPid : Posix.Process.pid -> Int.int
    5.14  val pidOfInt : Int.int -> Posix.Process.pid
    5.15  end;
    5.16 @@ -33,19 +29,7 @@
    5.17  fun flat_noDup []     = []
    5.18    | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
    5.19  
    5.20 -fun list2str_sep delim []      = delim
    5.21 -  | list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss);
    5.22 -
    5.23 -fun write_strs _   []      = ()
    5.24 -  | write_strs out (s::ss) = (TextIO.output (out, s); write_strs out ss);
    5.25 -
    5.26 -fun writeln_strs _   []      = ()
    5.27 -  | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
    5.28 -
    5.29 -(* pair the first argument with each element in the second input list *)
    5.30 -fun pair_ins x []      = []
    5.31 -  | pair_ins x (y::ys) = (x, y) :: (pair_ins x ys);
    5.32 -  
    5.33 + 
    5.34  (*Return the path to a "helper" like SPASS or tptp2X, first checking that
    5.35    it exists. --lcp *)  
    5.36  fun helper_path evar base =