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