src/HOL/Tools/ATP/watcher.ML
author paulson
Thu Sep 01 11:45:54 2005 +0200 (2005-09-01)
changeset 17216 df66d8feec63
parent 17150 ce2a1aeb42aa
child 17231 f42bc4f7afdf
permissions -rw-r--r--
improved formatting
     1 (*  Title:      Watcher.ML
     2     ID:         $Id$
     3     Author:     Claire Quigley
     4     Copyright   2004  University of Cambridge
     5  *)
     6 
     7  (***************************************************************************)
     8  (*  The watcher process starts a resolution process when it receives a     *)
     9 (*  message from Isabelle                                                  *)
    10 (*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    11 (*  and removes dead processes.  Also possible to kill all the resolution  *)
    12 (*  processes currently running.                                           *)
    13 (*  Hardwired version of where to pick up the tptp files for the moment    *)
    14 (***************************************************************************)
    15 
    16 (*use "Proof_Transfer";
    17 use "VampireCommunication";
    18 use "SpassCommunication";*)
    19 (*use "/homes/clq20/Jia_Code/TransStartIsar";*)
    20 
    21 
    22 structure Watcher: WATCHER =
    23   struct
    24 
    25 open ReconPrelim Recon_Transfer
    26 
    27 val goals_being_watched = ref 0;
    28 
    29 (*****************************************)
    30 (*  The result of calling createWatcher  *)
    31 (*****************************************)
    32 
    33 datatype proc = PROC of {
    34         pid : Posix.Process.pid,
    35         instr : TextIO.instream,
    36         outstr : TextIO.outstream
    37       };
    38 
    39 (*****************************************)
    40 (*  The result of calling executeToList  *)
    41 (*****************************************)
    42 
    43 datatype cmdproc = CMDPROC of {
    44         prover: string,             (* Name of the resolution prover used, e.g. Vampire, SPASS *)
    45         cmd:  string,              (* The file containing the goal for res prover to prove *)     
    46         thmstring: string,         (* string representation of subgoal after negation, skolemization*) 
    47         goalstring: string,         (* string representation of subgoal*) 
    48         proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    49         instr : TextIO.instream,   (*  Input stream to child process *)
    50         outstr : TextIO.outstream  (*  Output stream from child process *)
    51       };
    52 
    53 type signal = Posix.Signal.signal
    54 datatype exit_status = datatype Posix.Process.exit_status
    55 
    56 val fromStatus = Posix.Process.fromStatus
    57 
    58 
    59 fun reap(pid, instr, outstr) =
    60         let
    61 		val u = TextIO.closeIn instr;
    62 	        val u = TextIO.closeOut outstr;
    63 	
    64 		val (_, status) =
    65 			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    66 	in
    67 		status
    68 	end
    69 
    70 fun fdReader (name : string, fd : Posix.IO.file_desc) =
    71 	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    72 
    73 fun fdWriter (name, fd) =
    74           Posix.IO.mkTextWriter {
    75 	      appendMode = false,
    76               initBlkMode = true,
    77               name = name,  
    78               chunkSize=4096,
    79               fd = fd
    80             };
    81 
    82 fun openOutFD (name, fd) =
    83 	  TextIO.mkOutstream (
    84 	    TextIO.StreamIO.mkOutstream (
    85 	      fdWriter (name, fd), IO.BLOCK_BUF));
    86 
    87 fun openInFD (name, fd) =
    88 	  TextIO.mkInstream (
    89 	    TextIO.StreamIO.mkInstream (
    90 	      fdReader (name, fd), ""));
    91 
    92 fun killChild child_handle = Unix.reap child_handle 
    93 
    94 fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
    95 
    96 fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
    97 
    98 fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
    99 
   100 fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = (prover,(cmd, (instr,outstr)));
   101 
   102 fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = proc_handle;
   103 
   104 fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (prover);
   105 
   106 fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (thmstring);
   107 
   108 fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (goalstring);
   109 
   110 fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
   111 
   112 (********************************************************************************************)
   113 (*  takes a list of arguments and sends them individually to the watcher process by pipe    *)
   114 (********************************************************************************************)
   115 
   116 fun outputArgs (toWatcherStr, []) = ()
   117 |   outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); 
   118                                           TextIO.flushOut toWatcherStr;
   119                                          outputArgs (toWatcherStr, xs))
   120 
   121 (********************************************************************************)
   122 (*    gets individual args from instream and concatenates them into a list      *)
   123 (********************************************************************************)
   124 
   125 fun getArgs (fromParentStr, toParentStr,ys) =  let 
   126                                        val thisLine = TextIO.input fromParentStr
   127                                     in
   128                                         ((ys@[thisLine]))
   129                                     end
   130 
   131 (********************************************************************************)
   132 (*  Remove the \n character from the end of each filename                       *)
   133 (********************************************************************************)
   134 
   135 (*fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
   136                     in
   137                         if (String.isPrefix "\n"  (implode backList )) 
   138                         then (implode (rev ((tl backList))))
   139                         else cmdStr
   140                     end*)
   141                             
   142 (********************************************************************************)
   143 (*  Send request to Watcher for a vampire to be called for filename in arg      *)
   144 (********************************************************************************)
   145                     
   146 fun callResProver (toWatcherStr,  arg) = (sendOutput (toWatcherStr, arg^"\n"); 
   147                                      TextIO.flushOut toWatcherStr)
   148 
   149 (*****************************************************************************************)
   150 (*  Send request to Watcher for multiple provers to be called for filenames in arg       *)
   151 (*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
   152 (*****************************************************************************************)
   153 
   154     
   155 (* need to modify to send over hyps file too *)
   156 fun callResProvers (toWatcherStr,  []) = 
   157       (sendOutput (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
   158 |   callResProvers (toWatcherStr,
   159                     (prover,thmstring,goalstring, proverCmd,settings,clasimpfile, 
   160                      axfile, hypsfile,probfile)  ::  args) =
   161       let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
   162                              (prover^thmstring^goalstring^proverCmd^settings^
   163                               clasimpfile^hypsfile^probfile)
   164       in sendOutput (toWatcherStr,    
   165             (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^
   166              settings^"$"^clasimpfile^"$"^hypsfile^"$"^probfile^"\n"));
   167          goals_being_watched := (!goals_being_watched) + 1;
   168 	 TextIO.flushOut toWatcherStr;
   169 	 callResProvers (toWatcherStr,args)
   170       end   
   171                                                 
   172 
   173 (*
   174 fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
   175                                      
   176 |   callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile, probfile)::args) =
   177                                             ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^clasimpfile^"*"^axfile^"*"^hypsfile^"*"^probfile^"\n")
   178                                             
   179      *)                                      
   180  
   181 (**************************************************************)
   182 (* Send message to watcher to kill currently running vampires *)
   183 (**************************************************************)
   184 
   185 fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 
   186                             TextIO.flushOut toWatcherStr)
   187 
   188 
   189 
   190 (**************************************************************)
   191 (* Remove \n token from a vampire goal filename and extract   *)
   192 (* prover, proverCmd, settings and file from input string     *)
   193 (**************************************************************)
   194 
   195 
   196  fun takeUntil ch [] res  = (res, [])
   197  |   takeUntil ch (x::xs) res = 
   198         if   x = ch then (res, xs)
   199 	else takeUntil ch xs (res@[x])
   200 
   201  fun getSettings [] settings = settings
   202 |    getSettings (xs) settings = 
   203        let val (set, rest ) = takeUntil "%" xs []
   204        in
   205 	   getSettings rest (settings@[(implode set)])
   206        end
   207 
   208 fun separateFields str =
   209   let val  outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field")))                                                                         
   210       val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") )
   211       val _ =  TextIO.closeOut outfile
   212       val (prover, rest) = takeUntil "$" str []
   213       val prover = implode prover
   214 
   215       val (thmstring, rest) =  takeUntil "$" rest []
   216       val thmstring = implode thmstring
   217 
   218       val (goalstring, rest) =  takeUntil "$" rest []
   219       val goalstring = implode goalstring
   220 
   221       val (proverCmd, rest ) =  takeUntil "$" rest []
   222       val proverCmd = implode proverCmd
   223       
   224       val (settings, rest) =  takeUntil "$" rest []
   225       val settings = getSettings settings []
   226 
   227       val (clasimpfile, rest ) =  takeUntil "$" rest []
   228       val clasimpfile = implode clasimpfile
   229       
   230       val (hypsfile, rest ) =  takeUntil "$" rest []
   231       val hypsfile = implode hypsfile
   232 
   233       val (file, rest) =  takeUntil "$" rest []
   234       val file = implode file
   235 
   236       val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
   237                   ("Sep comms are: "^(implode str)^"**"^
   238                    prover^" thmstring: "^thmstring^"\n goalstr:  "^goalstring^" \n provercmd: "^proverCmd^" \n  clasimp "^clasimpfile^" \n hyps "^hypsfile^"\n prob  "^file^"\n\n")
   239   in
   240      (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file)
   241   end
   242 
   243                       
   244 (***********************************************************************************)
   245 (* do tptp2x and cat to turn clasimpfile, hypsfile and probfile into one .dfg file *)
   246 (***********************************************************************************)
   247 
   248 fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile ,probfile) = 
   249   let
   250     (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
   251     val probID = List.last(explode probfile)
   252     val wholefile = File.tmp_path (Path.basic ("ax_prob_" ^ probID))
   253     
   254     (*** only include problem and clasimp for the moment, not sure 
   255 	 how to refer to hyps/local axioms just now ***)
   256     val whole_prob_file = Unix.execute("/bin/cat", 
   257 	     [clasimpfile,(*axfile, hypsfile,*)probfile,  ">",
   258 	      File.platform_path wholefile])
   259     
   260     val dfg_dir = File.tmp_path (Path.basic "dfg"); 
   261     val dfg_path = File.platform_path dfg_dir;
   262     
   263     (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
   264     val probID = List.last(explode probfile)
   265     val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
   266 
   267     (*** only include problem and clasimp for the moment, not sure how to refer to ***)
   268     (*** hyps/local axioms just now                                                ***)
   269     val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])
   270     (*** check if the directory exists and, if not, create it***)
   271    (* val _ = 
   272 	if !SpassComm.spass
   273 	then 
   274 	    if File.exists dfg_dir then warning("dfg dir exists")
   275 	    else File.mkdir dfg_dir
   276 	else
   277 	    warning("not converting to dfg")
   278     
   279     val _ = if !SpassComm.spass then 
   280 		system (ResLib.helper_path "TPTP2X_HOME" "tptp2X" ^ 
   281 		        " -fdfg -d " ^ dfg_path ^ " " ^
   282 			File.platform_path wholefile)
   283 	      else 7
   284     val newfile =   if !SpassComm.spass 
   285 		    then 
   286 			    dfg_path^"/ax_prob"^"_"^(probID)^".dfg" 
   287 
   288 		    else
   289 			    (File.platform_path wholefile)*)
   290 
   291     (* if using spass prob_n already contains whole DFG file, otherwise need to mash axioms*)
   292     (* from clasimpset onto problem file *)
   293     val newfile =   if !SpassComm.spass 
   294 		    then 
   295 			 probfile
   296                     else 
   297 			(File.platform_path wholefile)
   298 
   299     val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
   300 	       (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")
   301   in
   302     (prover,thmstring,goalstring, proverCmd, settings,newfile)	
   303   end;
   304 
   305 
   306 
   307 (* remove \n from end of command and put back into tuple format *)
   308              
   309 
   310 (*  val cmdStr = "spass*((ALL xa. (~ P x | P xa) & (~ P xa | P x)) & (P xa | (ALL x. P x)) & ((ALL x. ~ P x) | ~ P xb) [.])*(EX x. ALL y. P x = P y) --> (EX x. P x) = (ALL y. P y)*/homes/clq20/bin/SPASS*-DocProof*/local/scratch/clq20/27023/clasimp*/local/scratch/clq20/27023/hyps*/local/scratch/clq20/27023/prob_1\n"
   311 
   312 val cmdStr = "vampire*(length (rev xs) = length xs  [.]) & (length (rev (a # xs)) ~= length (a # xs) [.])*length (rev []) = length []*/homes/jm318/Vampire8/vkernel*-t 300%-m 100000*/local/scratch/clq20/23523/clasimp*/local/scratch/clq20/23523/hyps*/local/scratch/clq20/23523/prob_1\n"
   313  *)
   314 
   315 (*FIX:  are the two getCmd procs getting confused?  Why do I have two anyway? *)
   316 
   317  fun getCmd cmdStr = 
   318        let val backList = rev(explode cmdStr)
   319 	   val _ = File.append (File.tmp_path (Path.basic"cmdStr")) cmdStr
   320        in
   321 	   if (String.isPrefix "\n"  (implode backList )) 
   322 	   then 
   323 	       let val newCmdStr = (rev(tl backList))
   324 	       in  File.write (File.tmp_path (Path.basic"backlist")) 
   325 	                      ("about to call sepfields with "^(implode newCmdStr));
   326 		   formatCmd (separateFields newCmdStr)
   327 	       end
   328 	   else formatCmd (separateFields (explode cmdStr))
   329        end
   330                       
   331 
   332 fun getProofCmd (a,b,c,d,e,f) = d
   333 
   334                         
   335 (**************************************************************)
   336 (* Get commands from Isabelle                                 *)
   337 (**************************************************************)
   338 (* FIX: or perhaps do the tptp2x stuff here - so it's get commands and then format them, before passing them to spass *)
   339 
   340 fun getCmds (toParentStr,fromParentStr, cmdList) = 
   341   let val thisLine = TextIO.inputLine fromParentStr 
   342       val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
   343   in
   344      if (thisLine = "End of calls\n") 
   345      then cmdList
   346      else if (thisLine = "Kill children\n") 
   347      then 
   348 	 (   TextIO.output (toParentStr,thisLine ); 
   349 	     TextIO.flushOut toParentStr;
   350 	   (("","","","Kill children",[],"")::cmdList)
   351 	  )
   352      else  let val thisCmd = getCmd (thisLine) 
   353 	       (*********************************************************)
   354 	       (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   355 	       (* i.e. put back into tuple format                       *)
   356 	       (*********************************************************)
   357 	   in
   358 	     (*TextIO.output (toParentStr, thisCmd); 
   359 	       TextIO.flushOut toParentStr;*)
   360 	       getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
   361 	   end
   362   end
   363 	    
   364                                                                   
   365 (**************************************************************)
   366 (*  Get Io-descriptor for polling of an input stream          *)
   367 (**************************************************************)
   368 
   369 
   370 fun getInIoDesc someInstr = 
   371     let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   372         val _ = TextIO.output (TextIO.stdOut, buf)
   373         val ioDesc = 
   374 	    case rd
   375 	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
   376 	       | _ => NONE
   377      in (* since getting the reader will have terminated the stream, we need
   378 	 * to build a new stream. *)
   379 	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
   380 	ioDesc
   381     end
   382 
   383 
   384 (*************************************)
   385 (*  Set up a Watcher Process         *)
   386 (*************************************)
   387 
   388 
   389 
   390 fun setupWatcher (thm,clause_arr, num_of_clauses) = 
   391   let
   392     (** pipes for communication between parent and watcher **)
   393     val p1 = Posix.IO.pipe ()
   394     val p2 = Posix.IO.pipe ()
   395     fun closep () = (
   396 	  Posix.IO.close (#outfd p1); 
   397 	  Posix.IO.close (#infd p1);
   398 	  Posix.IO.close (#outfd p2); 
   399 	  Posix.IO.close (#infd p2)
   400 	)
   401     (***********************************************************)
   402     (****** fork a watcher process and get it set up and going *)
   403     (***********************************************************)
   404     fun startWatcher (procList) =
   405 	     (case  Posix.Process.fork() (***************************************)
   406 	   of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   407 					 (***************************************)
   408 
   409 					   (*************************)
   410 	    | NONE => let                  (* child - i.e. watcher  *)
   411 		val oldchildin = #infd p1  (*************************)
   412 		val fromParent = Posix.FileSys.wordToFD 0w0
   413 		val oldchildout = #outfd p2
   414 		val toParent = Posix.FileSys.wordToFD 0w1
   415 		val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   416 		val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   417 		val toParentStr = openOutFD ("_exec_out_parent", toParent)
   418 		val sign = sign_of_thm thm
   419 		val prems = prems_of thm
   420 		val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   421 		val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
   422 	       (* tracing *)
   423 	      (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
   424 		val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
   425 		val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
   426 		val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
   427 		val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
   428 		val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
   429 			 *)
   430 		(*val goalstr = string_of_thm (the_goal)
   431 		 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher")));  
   432 		val _ = TextIO.output (outfile,goalstr )
   433 		val _ =  TextIO.closeOut outfile*)
   434 		fun killChildren [] = ()
   435 	     |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
   436 
   437 	      (*************************************************************)
   438 	      (* take an instream and poll its underlying reader for input *)
   439 	      (*************************************************************)
   440 
   441 	      fun pollParentInput () = 
   442 		 let val pd = OS.IO.pollDesc (fromParentIOD)
   443 		 in 
   444 		   if (isSome pd ) then 
   445 		       let val pd' = OS.IO.pollIn (valOf pd)
   446 			   val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   447 			   val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
   448 			     ("In parent_poll\n")	
   449 		       in
   450 			  if null pdl 
   451 			  then
   452 			     NONE
   453 			  else if (OS.IO.isIn (hd pdl)) 
   454 			       then
   455 				  (SOME ( getCmds (toParentStr, fromParentStr, [])))
   456 			       else
   457 				   NONE
   458 		       end
   459 		     else
   460 			 NONE
   461 		 end
   462 		      
   463 	       fun pollChildInput (fromStr) = 
   464 		 let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
   465 			       ("In child_poll\n")
   466 		     val iod = getInIoDesc fromStr
   467 		 in 
   468 		   if isSome iod 
   469 		   then 
   470 		     let val pd = OS.IO.pollDesc (valOf iod)
   471 		     in 
   472 		     if (isSome pd ) then 
   473 			 let val pd' = OS.IO.pollIn (valOf pd)
   474 			     val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   475 			     
   476 			 in
   477 			    if null pdl 
   478 			    then
   479 			      ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
   480 			       ("Null pdl \n");NONE)
   481 			    else if (OS.IO.isIn (hd pdl)) 
   482 				 then
   483 				     (let val inval =  (TextIO.inputLine fromStr)
   484 					  val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
   485 				      in
   486 					    SOME inval
   487 				      end)
   488 				 else
   489 				       ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
   490 			       ("Null pdl \n");NONE)
   491 			 end
   492 		       else  NONE
   493 		       end
   494 		   else NONE
   495 	     end
   496 
   497 
   498 	     (****************************************************************************)
   499 	     (* Check all vampire processes currently running for output                 *)
   500 	     (****************************************************************************) 
   501 							(*********************************)
   502 	      fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   503 							(*********************************)
   504 	      |   checkChildren ((childProc::otherChildren), toParentStr) = 
   505 		    let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
   506 			           ("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n")
   507                         val (childInput,childOutput) =  cmdstreamsOf childProc
   508 			val child_handle= cmdchildHandle childProc
   509 			(* childCmd is the .dfg file that the problem is in *)
   510 			val childCmd = fst(snd (cmdchildInfo childProc))
   511                         val _ = File.append (File.tmp_path (Path.basic "child_command")) 
   512 			           (childCmd^"\n")
   513 			(* now get the number of the subgoal from the filename *)
   514 			val sg_num = (*if (!SpassComm.spass )
   515 				     then 
   516 					int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
   517 				     else*)
   518 					int_of_string(hd (rev(explode childCmd)))
   519 
   520 			val childIncoming = pollChildInput childInput
   521  			val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) 
   522 			           ("finished polling child \n")
   523 			val parentID = Posix.ProcEnv.getppid()
   524 			val prover = cmdProver childProc
   525 			val thmstring = cmdThm childProc
   526 			val sign = sign_of_thm thm
   527 			val prems = prems_of thm
   528 			val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   529 			val _ = warning("subgoals forked to checkChildren: "^prems_string)
   530 			val goalstring = cmdGoal childProc							
   531 			val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
   532 			           (prover^thmstring^goalstring^childCmd^"\n")
   533 		    in 
   534 		      if (isSome childIncoming) 
   535 		      then 
   536 			  (* check here for prover label on child*)
   537 			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))  ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) 
   538 		              val childDone = (case prover of
   539 	                          "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )                                              
   540                                  |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   541 			   in
   542 			    if childDone      (**********************************************)
   543 			    then (* child has found a proof and transferred it *)
   544 			       (* Remove this child and go on to check others*)
   545 			       (**********************************************)
   546 			       (Unix.reap child_handle;
   547 				checkChildren(otherChildren, toParentStr))
   548 			    else 
   549 			       (**********************************************)
   550 			       (* Keep this child and go on to check others  *)
   551 			       (**********************************************)
   552 			      (childProc::(checkChildren (otherChildren, toParentStr)))
   553 			 end
   554 		       else
   555 			 (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   556 			  childProc::(checkChildren (otherChildren, toParentStr)))
   557 		    end
   558 
   559 	     
   560 	  (********************************************************************)                  
   561 	  (* call resolution processes                                        *)
   562 	  (* settings should be a list of strings                             *)
   563 	  (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
   564 	  (* takes list of (string, string, string list, string)list proclist *)
   565 	  (********************************************************************)
   566 
   567 
   568 (*** add subgoal id num to this *)
   569 	     fun execCmds  [] procList = procList
   570 	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =             let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child"))  ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   571 	       in 
   572 		 if (prover = "spass") 
   573 		 then 
   574 		   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   575 		            (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   576 		       val (instr, outstr) = Unix.streamsOf childhandle
   577 		       val newProcList =    (((CMDPROC{
   578 					    prover = prover,
   579 					    cmd = file,
   580 					    thmstring = thmstring,
   581 					    goalstring = goalstring,
   582 					    proc_handle = childhandle,
   583 					    instr = instr,
   584 					    outstr = outstr })::procList))
   585 			val _ = File.append (File.tmp_path (Path.basic "exec_child"))  
   586 			     ("\nexecuting command for goal:\n"^
   587 			      goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   588 		   in
   589 		      Posix.Process.sleep (Time.fromSeconds 1);execCmds cmds newProcList
   590 		   end
   591 		 else 
   592 		   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   593 		            (Unix.execute(proverCmd, (settings@[file])))
   594 		       val (instr, outstr) = Unix.streamsOf childhandle
   595 		       
   596 		       val newProcList = (CMDPROC{
   597 					    prover = prover,
   598 					    cmd = file,
   599 					    thmstring = thmstring,
   600 					    goalstring = goalstring,
   601 					    proc_handle = childhandle,
   602 					    instr = instr,
   603 					    outstr = outstr }) :: procList
   604 	  
   605 		       val _ = File.append (File.tmp_path (Path.basic "exec_child")) 
   606 		                 ("executing command for goal:\n"^
   607 		                  goalstring^proverCmd^(concat settings)^file^
   608 		                  " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   609 		   in
   610 		     Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList
   611 		   end
   612 		end
   613 
   614 
   615 	  (****************************************)                  
   616 	  (* call resolution processes remotely   *)
   617 	  (* settings should be a list of strings *)
   618 	  (* e.g. ["-t 300", "-m 100000"]         *)
   619 	  (****************************************)
   620 
   621 	   (*  fun execRemoteCmds  [] procList = procList
   622 	     |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   623 				       let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   624 					   in
   625 						execRemoteCmds  cmds newProcList
   626 					   end
   627 *)
   628 
   629 	     fun printList (outStr, []) = ()
   630 	     |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   631 
   632 
   633 	  (**********************************************)                  
   634 	  (* Watcher Loop                               *)
   635 	  (**********************************************)
   636 
   637 	      fun keepWatching (toParentStr, fromParentStr,procList) = 
   638 		let fun loop (procList) =  
   639 		     let val cmdsFromIsa = pollParentInput ()
   640 			 fun killchildHandler (n:int)  = 
   641 			       (TextIO.output(toParentStr, "Killing child proof processes!\n");
   642 				TextIO.flushOut toParentStr;
   643 				killChildren (map (cmdchildHandle) procList);
   644 				())
   645 		     in 
   646 			(*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   647 									   (**********************************)
   648 			if (isSome cmdsFromIsa) 
   649 			then (*  deal with input from Isabelle *)
   650 			  if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   651 			  then 
   652 			    let val child_handles = map cmdchildHandle procList 
   653 			    in
   654 			       killChildren child_handles;
   655 			       (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)    
   656 			       loop ([])
   657 			    end
   658 			  else
   659 			    if ((length procList)<10)    (********************)
   660 			    then                        (* Execute locally  *)
   661 			      let 
   662 				val newProcList = execCmds (valOf cmdsFromIsa) procList
   663 				val parentID = Posix.ProcEnv.getppid()
   664 				   val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
   665 				val newProcList' =checkChildren (newProcList, toParentStr) 
   666 
   667 				val _ = warning("off to keep watching...")
   668 			       val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
   669 			      in
   670 				(*Posix.Process.sleep (Time.fromSeconds 1);*)
   671 				loop (newProcList') 
   672 			      end
   673 			    else  (* Execute remotely              *)
   674                                   (* (actually not remote for now )*)
   675 			      let 
   676 				val newProcList = execCmds (valOf cmdsFromIsa) procList
   677 				val parentID = Posix.ProcEnv.getppid()
   678 				val newProcList' =checkChildren (newProcList, toParentStr) 
   679 			      in
   680 				(*Posix.Process.sleep (Time.fromSeconds 1);*)
   681 				loop (newProcList') 
   682 			      end
   683 			else (* No new input from Isabelle *)
   684 			  let val newProcList = checkChildren ((procList), toParentStr)
   685 			  in
   686 			    (*Posix.Process.sleep (Time.fromSeconds 1);*)
   687 			   (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
   688 			    loop (newProcList)
   689 			  end
   690 		      end
   691 		in  
   692 		    loop (procList)
   693 		end
   694 		
   695     
   696 		in
   697 		 (***************************)
   698 		 (*** Sort out pipes ********)
   699 		 (***************************)
   700 
   701 		  Posix.IO.close (#outfd p1);
   702 		  Posix.IO.close (#infd p2);
   703 		  Posix.IO.dup2{old = oldchildin, new = fromParent};
   704 		  Posix.IO.close oldchildin;
   705 		  Posix.IO.dup2{old = oldchildout, new = toParent};
   706 		  Posix.IO.close oldchildout;
   707 
   708 		  (***************************)
   709 		  (* start the watcher loop  *)
   710 		  (***************************)
   711 		  keepWatching (toParentStr, fromParentStr, procList);
   712 
   713 
   714 		  (****************************************************************************)
   715 		  (* fake return value - actually want the watcher to loop until killed       *)
   716 		  (****************************************************************************)
   717 		  Posix.Process.wordToPid 0w0
   718 		  
   719 		end);
   720 	  (* end case *)
   721 
   722 
   723     val _ = TextIO.flushOut TextIO.stdOut
   724 
   725     (*******************************)
   726     (***  set watcher going ********)
   727     (*******************************)
   728 
   729     val procList = []
   730     val pid = startWatcher (procList)
   731     (**************************************************)
   732     (* communication streams to watcher               *)
   733     (**************************************************)
   734 
   735     val instr = openInFD ("_exec_in", #infd p2)
   736     val outstr = openOutFD ("_exec_out", #outfd p1)
   737     
   738     in
   739      (*******************************)
   740      (* close the child-side fds    *)
   741      (*******************************)
   742       Posix.IO.close (#outfd p2);
   743       Posix.IO.close (#infd p1);
   744       (* set the fds close on exec *)
   745       Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   746       Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   747        
   748      (*******************************)
   749      (* return value                *)
   750      (*******************************)
   751       PROC{pid = pid,
   752 	instr = instr,
   753 	outstr = outstr
   754       }
   755    end;
   756 
   757 
   758 
   759 (**********************************************************)
   760 (* Start a watcher and set up signal handlers             *)
   761 (**********************************************************)
   762 
   763 fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   764 
   765 fun reapWatcher(pid, instr, outstr) =
   766   let val u = TextIO.closeIn instr;
   767       val u = TextIO.closeOut outstr;
   768       val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
   769   in
   770 	  status
   771   end
   772 
   773 
   774 
   775 fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) =
   776  let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   777      val streams =snd mychild
   778      val childin = fst streams
   779      val childout = snd streams
   780      val childpid = fst mychild
   781      val sign = sign_of_thm thm
   782      val prems = prems_of thm
   783      val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   784      val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   785      fun vampire_proofHandler (n) =
   786 	(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   787 	 VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))               
   788      fun spass_proofHandler (n) = (
   789        let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
   790 	   val _ = TextIO.output (outfile, ("In signal handler now\n"))
   791 	   val _ =  TextIO.closeOut outfile
   792 	   val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
   793 	   val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
   794    
   795 	   val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   796 	   val _ =  TextIO.closeOut outfile
   797        in (* if a proof has been found and sent back as a reconstruction proof *)
   798 	 if ( (substring (reconstr, 0,1))= "[")
   799 	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   800 	       Recon_Transfer.apply_res_thm reconstr goalstring;
   801 	       Pretty.writeln(Pretty.str  (oct_char "361"));
   802 	       
   803 	       goals_being_watched := ((!goals_being_watched) - 1);
   804        
   805 	       if ((!goals_being_watched) = 0)
   806 	       then 
   807 		  (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found")));
   808 		       val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   809 		       val _ =  TextIO.closeOut outfile
   810 		   in
   811 		       killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   812 		   end)
   813 		else () )
   814 	 (* if there's no proof, but a message from Spass *)
   815 	 else if ((substring (reconstr, 0,5))= "SPASS")
   816 	 then (goals_being_watched := (!goals_being_watched) -1;
   817 	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   818 	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
   819 	       Pretty.writeln(Pretty.str  (oct_char "361"));
   820 	       if (!goals_being_watched = 0)
   821 	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   822 	              ("Reaping a watcher, goals watched is: " ^
   823 	                 (string_of_int (!goals_being_watched))^"\n");
   824 	             killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
   825 		else () ) 
   826 	(* print out a list of rules used from clasimpset*)
   827 	 else if ((substring (reconstr, 0,5))= "Rules")
   828 	 then (goals_being_watched := (!goals_being_watched) -1;
   829 	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   830 	       Pretty.writeln(Pretty.str (goalstring^reconstr));
   831 	       Pretty.writeln(Pretty.str  (oct_char "361"));
   832 	       if (!goals_being_watched = 0)
   833 	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   834 	              ("Reaping a watcher, goals watched is: " ^
   835 	                 (string_of_int (!goals_being_watched))^"\n");
   836 	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   837 		     )
   838 	       else () )
   839 	  (* if proof translation failed *)
   840 	 else if ((substring (reconstr, 0,5)) = "Proof")
   841 	 then (goals_being_watched := (!goals_being_watched) -1;
   842 	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   843 	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   844 	       Pretty.writeln(Pretty.str  (oct_char "361"));
   845 	       if (!goals_being_watched = 0)
   846 	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   847 	              ("Reaping a watcher, goals watched is: " ^
   848 	                 (string_of_int (!goals_being_watched))^"\n");
   849 	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   850 		     )
   851 	       else () )
   852 
   853 	 else if ((substring (reconstr, 0,1)) = "%")
   854 	 then (goals_being_watched := (!goals_being_watched) -1;
   855 	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   856 	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   857 	       Pretty.writeln(Pretty.str  (oct_char "361"));
   858 	       if (!goals_being_watched = 0)
   859 	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   860 	              ("Reaping a watcher, goals watched is: " ^
   861 	                 (string_of_int (!goals_being_watched))^"\n");
   862 	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   863 		     )
   864 	       else () )
   865 
   866 	 else  (* add something here ?*)
   867 	      (goals_being_watched := (!goals_being_watched) -1;
   868 	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   869 		Pretty.writeln(Pretty.str ("Ran out of options in handler"));
   870 		Pretty.writeln(Pretty.str  (oct_char "361"));
   871 		if (!goals_being_watched = 0)
   872 	        then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   873 	              ("Reaping a watcher, goals watched is: " ^
   874 	                 (string_of_int (!goals_being_watched))^"\n");
   875 	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   876 		     )
   877 	        else () )
   878        end)
   879 
   880  in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   881     IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   882     (childin, childout, childpid)
   883 
   884   end
   885 
   886 end (* structure Watcher *)