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