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