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