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