src/HOL/Tools/ATP/watcher.ML
author paulson
Tue Jun 21 13:34:24 2005 +0200 (2005-06-21)
changeset 16515 7896ea4f3a87
parent 16478 d0a1f6231e2f
child 16520 7a9cda53bfa2
permissions -rw-r--r--
VAMPIRE_HOME, helper_path and various stylistic tweaks
     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 = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
   518 			val childIncoming = pollChildInput childInput
   519  			val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) 
   520 			           ("finished polling child \n")
   521 			val parentID = Posix.ProcEnv.getppid()
   522 			val prover = cmdProver childProc
   523 			val thmstring = cmdThm childProc
   524 			val sign = sign_of_thm thm
   525 			val prems = prems_of thm
   526 			val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   527 			val _ = warning("subgoals forked to checkChildren: "^prems_string)
   528 			val goalstring = cmdGoal childProc							
   529 			val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
   530 			           (prover^thmstring^goalstring^childCmd^"\n")
   531 		    in 
   532 		      if (isSome childIncoming) 
   533 		      then 
   534 			  (* check here for prover label on child*)
   535 			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))  ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) 
   536 		              val childDone = (case prover of
   537 	                          "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )                                              
   538                                  |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   539 			   in
   540 			    if childDone      (**********************************************)
   541 			    then              (* child has found a proof and transferred it *)
   542 					      (**********************************************)
   543 
   544 			       (**********************************************)
   545 			       (* Remove this child and go on to check others*)
   546 			       (**********************************************)
   547 			       ( Unix.reap child_handle;
   548 				 checkChildren(otherChildren, toParentStr))
   549 			    else 
   550 			       (**********************************************)
   551 			       (* Keep this child and go on to check others  *)
   552 			       (**********************************************)
   553 
   554 				 (childProc::(checkChildren (otherChildren, toParentStr)))
   555 			 end
   556 		       else
   557 			 (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   558 			  childProc::(checkChildren (otherChildren, toParentStr)))
   559 		    end
   560 
   561 	     
   562 	  (********************************************************************)                  
   563 	  (* call resolution processes                                        *)
   564 	  (* settings should be a list of strings                             *)
   565 	  (* e.g. ["-t 300", "-m 100000"]                                     *)
   566 	  (* takes list of (string, string, string list, string)list proclist *)
   567 	  (********************************************************************)
   568 
   569 
   570 (*** add subgoal id num to this *)
   571 	     fun execCmds  [] procList = procList
   572 	     |   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()))))
   573 	       in 
   574 		 if (prover = "spass") 
   575 		   then 
   576 		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   577 			   val (instr, outstr)=Unix.streamsOf childhandle
   578 			   val newProcList =    (((CMDPROC{
   579 						prover = prover,
   580 						cmd = file,
   581 						thmstring = thmstring,
   582 						goalstring = goalstring,
   583 						proc_handle = childhandle,
   584 						instr = instr,
   585 						outstr = outstr })::procList))
   586 			    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()))))
   587 		       in
   588 			  Posix.Process.sleep (Time.fromSeconds 1);execCmds cmds newProcList
   589 		       end
   590 		   else 
   591 		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (settings@[file])))
   592 			   val (instr, outstr)=Unix.streamsOf childhandle
   593                            
   594 			   val newProcList =    (((CMDPROC{
   595 						prover = prover,
   596 						cmd = file,
   597 						thmstring = thmstring,
   598 						goalstring = goalstring,
   599 						proc_handle = childhandle,
   600 						instr = instr,
   601 						outstr = outstr })::procList))
   602               
   603                            val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^(TextIO.input instr)^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   604 		       in
   605 			 Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList
   606 		       end
   607 		end
   608 
   609 
   610 	  (****************************************)                  
   611 	  (* call resolution processes remotely   *)
   612 	  (* settings should be a list of strings *)
   613 	  (* e.g. ["-t 300", "-m 100000"]         *)
   614 	  (****************************************)
   615 
   616 	   (*  fun execRemoteCmds  [] procList = procList
   617 	     |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   618 				       let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   619 					   in
   620 						execRemoteCmds  cmds newProcList
   621 					   end
   622 *)
   623 
   624 	     fun printList (outStr, []) = ()
   625 	     |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   626 
   627 
   628 	  (**********************************************)                  
   629 	  (* Watcher Loop                               *)
   630 	  (**********************************************)
   631 
   632 
   633 
   634 
   635 	      fun keepWatching (toParentStr, fromParentStr,procList) = 
   636 		    let    fun loop (procList) =  
   637 			   (
   638 			   let val cmdsFromIsa = pollParentInput ()
   639 			       fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
   640 					    TextIO.flushOut toParentStr;
   641 					     killChildren (map (cmdchildHandle) procList);
   642 					      ())
   643 			       
   644 			   in 
   645 			      (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   646 										 (**********************************)
   647 			      if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
   648 				   (                                             (**********************************)                             
   649 				    if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   650 				    then 
   651 				      (
   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);*)                                                              loop ([])
   656 					end
   657 					   
   658 				       )
   659 				    else
   660 				      ( 
   661 					if ((length procList)<10)    (********************)
   662 					then                        (* Execute locally  *)
   663 					   (                        (********************)
   664 					    let 
   665 					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   666 					      val parentID = Posix.ProcEnv.getppid()
   667           					 val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
   668 					      val newProcList' =checkChildren (newProcList, toParentStr) 
   669 
   670 					      val _ = warning("off to keep watching...")
   671 					     val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
   672 					    in
   673 					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   674 					      loop (newProcList') 
   675 					    end
   676 					    )
   677 					else                         (*********************************)
   678 								     (* Execute remotely              *)
   679 								     (* (actually not remote for now )*)
   680 					    (                        (*********************************)
   681 					    let 
   682 					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   683 					      val parentID = Posix.ProcEnv.getppid()
   684 					      val newProcList' =checkChildren (newProcList, toParentStr) 
   685 					    in
   686 					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   687 					      loop (newProcList') 
   688 					    end
   689 					    )
   690 
   691 
   692 
   693 					)
   694 				     )                                              (******************************)
   695 			      else                                                  (* No new input from Isabelle *)
   696 										    (******************************)
   697 				  (    let val newProcList = checkChildren ((procList), toParentStr)
   698 				       in
   699 					 (*Posix.Process.sleep (Time.fromSeconds 1);*)
   700 					(File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
   701 					 loop (newProcList)
   702 				       end
   703 				   
   704 				   )
   705 			    end)
   706 		    in  
   707 			loop (procList)
   708 		    end
   709 		
   710     
   711 		in
   712 		 (***************************)
   713 		 (*** Sort out pipes ********)
   714 		 (***************************)
   715 
   716 		  Posix.IO.close (#outfd p1);
   717 		  Posix.IO.close (#infd p2);
   718 		  Posix.IO.dup2{old = oldchildin, new = fromParent};
   719 		  Posix.IO.close oldchildin;
   720 		  Posix.IO.dup2{old = oldchildout, new = toParent};
   721 		  Posix.IO.close oldchildout;
   722 
   723 		  (***************************)
   724 		  (* start the watcher loop  *)
   725 		  (***************************)
   726 		  keepWatching (toParentStr, fromParentStr, procList);
   727 
   728 
   729 		  (****************************************************************************)
   730 		  (* fake return value - actually want the watcher to loop until killed       *)
   731 		  (****************************************************************************)
   732 		  Posix.Process.wordToPid 0w0
   733 		  
   734 		end);
   735 	  (* end case *)
   736 
   737 
   738     val _ = TextIO.flushOut TextIO.stdOut
   739 
   740     (*******************************)
   741     (***  set watcher going ********)
   742     (*******************************)
   743 
   744     val procList = []
   745     val pid = startWatcher (procList)
   746     (**************************************************)
   747     (* communication streams to watcher               *)
   748     (**************************************************)
   749 
   750     val instr = openInFD ("_exec_in", #infd p2)
   751     val outstr = openOutFD ("_exec_out", #outfd p1)
   752     
   753     in
   754      (*******************************)
   755      (* close the child-side fds    *)
   756      (*******************************)
   757       Posix.IO.close (#outfd p2);
   758       Posix.IO.close (#infd p1);
   759       (* set the fds close on exec *)
   760       Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   761       Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   762        
   763      (*******************************)
   764      (* return value                *)
   765      (*******************************)
   766       PROC{pid = pid,
   767 	instr = instr,
   768 	outstr = outstr
   769       }
   770    end;
   771 
   772 
   773 
   774 (**********************************************************)
   775 (* Start a watcher and set up signal handlers             *)
   776 (**********************************************************)
   777 
   778 fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   779 
   780 fun reapWatcher(pid, instr, outstr) =
   781         let
   782 		val u = TextIO.closeIn instr;
   783 	        val u = TextIO.closeOut outstr;
   784 	
   785 		val (_, status) =
   786 			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
   787 	in
   788 		status
   789 	end
   790 
   791 
   792 fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) =
   793   let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   794       val streams =snd mychild
   795       val childin = fst streams
   796       val childout = snd streams
   797       val childpid = fst mychild
   798       val sign = sign_of_thm thm
   799       val prems = prems_of thm
   800       val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   801       val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   802       fun vampire_proofHandler (n) =
   803 	  (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   804 	  VampComm.getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361")))               
   805 
   806       fun spass_proofHandler (n) = 
   807        let val _ = File.write (File.tmp_path (Path.basic "foo_signal1")) "In signal handler now\n"
   808 	   val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
   809 	   val _ = File.append (File.tmp_path (Path.basic "foo_signal")) 
   810 		      ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))
   811        in  (* if a proof has been found and sent back as a reconstruction proof *)
   812 	 if ( (substring (reconstr, 0,1))= "[")
   813 	 then 
   814 	   (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   815 	    Recon_Transfer.apply_res_thm reconstr goalstring;
   816 	    Pretty.writeln(Pretty.str  (oct_char "361"));
   817 	    
   818 	    goals_being_watched := ((!goals_being_watched) - 1);
   819      
   820 	    if ((!goals_being_watched) = 0)
   821 	    then 
   822 		let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found"))
   823 			       ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")
   824 		in
   825 		    killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   826 		end
   827 	    else ()
   828 	   )
   829 	 (* if there's no proof, but a message from Spass *)
   830 	 else if ((substring (reconstr, 0,5))= "SPASS")
   831 	 then
   832 	   (goals_being_watched := (!goals_being_watched) -1;
   833 	    Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   834 	    Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
   835 	    Pretty.writeln(Pretty.str  (oct_char "361"));
   836 	    if (!goals_being_watched = 0)
   837 	    then 
   838 	      (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   839 				("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   840 	       killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
   841 	    else ()
   842 	  ) 
   843 	  (* print out a list of rules used from clasimpset*)
   844 	   else if ((substring (reconstr, 0,5))= "Rules")
   845 	   then
   846 	     (goals_being_watched := (!goals_being_watched) -1;
   847 	      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   848 	       Pretty.writeln(Pretty.str (goalstring^reconstr));
   849 	       Pretty.writeln(Pretty.str  (oct_char "361"));
   850 	       if (!goals_being_watched = 0)
   851 	       then 
   852 		  (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   853 			       ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   854 		   killWatcher (childpid);  reapWatcher (childpid,childin, childout);())
   855 	       else ()
   856 	     )
   857 	  
   858 	    (* if proof translation failed *)
   859 	    else if ((substring (reconstr, 0,5)) = "Proof")
   860 	    then 
   861 	      (goals_being_watched := (!goals_being_watched) -1;
   862 	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   863 		Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   864 		Pretty.writeln(Pretty.str  (oct_char "361"));
   865 		if (!goals_being_watched = 0)
   866 		then 
   867 		  (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   868 			       ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   869 		    killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
   870 		else
   871 		   ()
   872 	     )
   873 	    else  (* add something here ?*)
   874 		()
   875 			    
   876       end
   877 	    
   878   in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   879      IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   880      (childin, childout, childpid)
   881 
   882 
   883   end
   884 
   885 
   886 
   887 
   888 
   889 end (* structure Watcher *)