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