src/HOL/Tools/ATP/watcher.ML
author paulson
Fri May 27 12:12:05 2005 +0200 (2005-05-27)
changeset 16100 f80fc4bff933
parent 16091 3683f0486a11
child 16156 2f6fc19aba1e
permissions -rw-r--r--
Now uses File.write and File.append
     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,  []) =
   157       (sendOutput (toWatcherStr, "End of calls\n"); 
   158        TextIO.flushOut toWatcherStr)
   159 |   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) =
   160       let val dfg_dir = File.tmp_path (Path.basic "dfg"); 
   161 	 (*** need to check here if the directory exists and, if not, create it***)
   162 	  val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))                                                                     
   163 	              (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n")
   164 	 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
   165 	  val probID = ReconOrderClauses.last(explode probfile)
   166 	  val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
   167 	  (*** only include problem and clasimp for the moment, not sure how to refer to ***)
   168 	  (*** hyps/local axioms just now                                                ***)
   169           (*FIXME: find a way that works for SML/NJ too: it regards > as a filename!*)
   170 	  val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
   171 	  val dfg_create = if File.exists dfg_dir 
   172 			   then warning("dfg dir exists")
   173 			   else File.mkdir dfg_dir; 
   174 	  
   175 	  val dfg_path = File.sysify_path dfg_dir;
   176 	  val tptp2x_args = ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile]
   177 	  val exec_tptp2x = 
   178  	      Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X", tptp2x_args)
   179 	(*val _ = Posix.Process.wait ()*)
   180 	(*val _ =Unix.reap exec_tptp2x*)
   181 	  val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
   182  
   183        in   
   184 	  goals_being_watched := (!goals_being_watched) + 1;
   185 	  Posix.Process.sleep(Time.fromSeconds 4); 
   186 	  (warning ("probfile is: "^probfile));
   187 	  (warning("dfg file is: "^newfile));
   188 	  (warning ("wholefile is: "^(File.sysify_path wholefile)));
   189 	  sendOutput (toWatcherStr,
   190 	       prover ^ "*" ^ thmstring ^ "*" ^ goalstring ^ "*" ^ proverCmd ^ 
   191 	       "*" ^ settings ^ "*" ^ newfile ^ "\n");
   192  (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
   193 	  TextIO.flushOut toWatcherStr;
   194 	  Unix.reap exec_tptp2x;
   195 	  if File.exists
   196 	        (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg")))
   197 	  then callResProvers (toWatcherStr, args)
   198 	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X " ^
   199 	              space_implode " " tptp2x_args)
   200       end
   201 (*
   202 fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
   203                                      
   204 |   callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile, probfile)::args) =
   205                                             ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^clasimpfile^"*"^axfile^"*"^hypsfile^"*"^probfile^"\n")
   206                                             
   207      *)                                      
   208  
   209 (**************************************************************)
   210 (* Send message to watcher to kill currently running vampires *)
   211 (**************************************************************)
   212 
   213 fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 
   214                             TextIO.flushOut toWatcherStr)
   215 
   216 
   217 
   218 (**************************************************************)
   219 (* Remove \n token from a vampire goal filename and extract   *)
   220 (* prover, proverCmd, settings and file from input string     *)
   221 (**************************************************************)
   222 
   223 
   224  fun takeUntil ch [] res  = (res, [])
   225  |   takeUntil ch (x::xs) res = if   x = ch 
   226                                 then
   227                                      (res, xs)
   228                                 else
   229                                      takeUntil ch xs (res@[x])
   230 
   231  fun getSettings [] settings = settings
   232 |    getSettings (xs) settings = let val (set, rest ) = takeUntil "%" xs []
   233                                  in
   234                                      getSettings rest (settings@[(implode set)])
   235                                  end
   236 
   237 fun separateFields str =
   238   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 _ = File.write (File.tmp_path (Path.basic "sep_comms"))
   252                 (prover^thmstring^goalstring^proverCmd^file) 
   253   in
   254      (prover,thmstring,goalstring, proverCmd, settings, file)
   255   end
   256 
   257  
   258 
   259  fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
   260                      in
   261 
   262                          if (String.isPrefix "\n"  (implode backList )) 
   263                          then 
   264                              separateFields ((rev ((tl backList))))
   265                          else
   266                            (separateFields (explode cmdStr))
   267                      end
   268                       
   269 
   270 fun getProofCmd (a,b,c,d,e,f) = d
   271 
   272 
   273 (**************************************************************)
   274 (* Get commands from Isabelle                                 *)
   275 (**************************************************************)
   276 
   277 fun getCmds (toParentStr,fromParentStr, cmdList) = 
   278        let val thisLine = TextIO.inputLine fromParentStr 
   279        in
   280 	  (if (thisLine = "End of calls\n") 
   281 	   then 
   282 	      (cmdList)
   283 	   else if (thisLine = "Kill children\n") 
   284 		then 
   285 		    (   TextIO.output (toParentStr,thisLine ); 
   286 			TextIO.flushOut toParentStr;
   287 		      (("","","","Kill children",[],"")::cmdList)
   288 		     )
   289 	      else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   290 		    in
   291 		      (*TextIO.output (toParentStr, thisCmd); 
   292 			TextIO.flushOut toParentStr;*)
   293 			getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
   294 		    end
   295 		    )
   296 	    )
   297 	end
   298                                     
   299                                     
   300 (**************************************************************)
   301 (*  Get Io-descriptor for polling of an input stream          *)
   302 (**************************************************************)
   303 
   304 
   305 fun getInIoDesc someInstr = 
   306     let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   307         val _ = TextIO.output (TextIO.stdOut, buf)
   308         val ioDesc = 
   309 	    case rd
   310 	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
   311 	       | _ => NONE
   312      in (* since getting the reader will have terminated the stream, we need
   313 	 * to build a new stream. *)
   314 	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
   315 	ioDesc
   316     end
   317 
   318 
   319 (*************************************)
   320 (*  Set up a Watcher Process         *)
   321 (*************************************)
   322 
   323 
   324 
   325 fun setupWatcher (thm,clause_arr, num_of_clauses) = 
   326   let
   327     (** pipes for communication between parent and watcher **)
   328     val p1 = Posix.IO.pipe ()
   329     val p2 = Posix.IO.pipe ()
   330     fun closep () = (
   331 	  Posix.IO.close (#outfd p1); 
   332 	  Posix.IO.close (#infd p1);
   333 	  Posix.IO.close (#outfd p2); 
   334 	  Posix.IO.close (#infd p2)
   335 	)
   336     (***********************************************************)
   337     (****** fork a watcher process and get it set up and going *)
   338     (***********************************************************)
   339     fun startWatcher (procList) =
   340 	     (case  Posix.Process.fork() (***************************************)
   341 	   of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   342 					 (***************************************)
   343 
   344 					   (*************************)
   345 	    | NONE => let                  (* child - i.e. watcher  *)
   346 		val oldchildin = #infd p1  (*************************)
   347 		val fromParent = Posix.FileSys.wordToFD 0w0
   348 		val oldchildout = #outfd p2
   349 		val toParent = Posix.FileSys.wordToFD 0w1
   350 		val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   351 		val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   352 		val toParentStr = openOutFD ("_exec_out_parent", toParent)
   353 		val sign = sign_of_thm thm
   354 		val prems = prems_of thm
   355 		val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   356 		val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
   357 	       (* tracing *)
   358 	      (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
   359 		val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
   360 		val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
   361 		val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
   362 		val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
   363 		val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
   364 			 *)
   365 		(*val goalstr = string_of_thm (the_goal)
   366 		 val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));  
   367 		val _ = TextIO.output (outfile,goalstr )
   368 		val _ =  TextIO.closeOut outfile*)
   369 		fun killChildren [] = ()
   370 	     |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
   371 
   372 	       
   373      
   374 	      (*************************************************************)
   375 	      (* take an instream and poll its underlying reader for input *)
   376 	      (*************************************************************)
   377 
   378 	      fun pollParentInput () = 
   379 		     
   380 			 let val pd = OS.IO.pollDesc (fromParentIOD)
   381 			 in 
   382 			 if (isSome pd ) then 
   383 			     let val pd' = OS.IO.pollIn (valOf pd)
   384 				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
   385 			     in
   386 				if null pdl 
   387 				then
   388 				   NONE
   389 				else if (OS.IO.isIn (hd pdl)) 
   390 				     then
   391 					(SOME ( getCmds (toParentStr, fromParentStr, [])))
   392 				     else
   393 					 NONE
   394 			     end
   395 			   else
   396 			       NONE
   397 			   end
   398 		      
   399 	     
   400 
   401 	       fun pollChildInput (fromStr) = 
   402 		     let val iod = getInIoDesc fromStr
   403 		     in 
   404 		     if isSome iod 
   405 		     then 
   406 			 let val pd = OS.IO.pollDesc (valOf iod)
   407 			 in 
   408 			 if (isSome pd ) then 
   409 			     let val pd' = OS.IO.pollIn (valOf pd)
   410 				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
   411 			     in
   412 				if null pdl 
   413 				then
   414 				   NONE
   415 				else if (OS.IO.isIn (hd pdl)) 
   416 				     then
   417 					 SOME (getCmd (TextIO.inputLine fromStr))
   418 				     else
   419 					 NONE
   420 			     end
   421 			   else
   422 			       NONE
   423 			   end
   424 		       else 
   425 			   NONE
   426 		      end
   427 
   428 
   429 	     (****************************************************************************)
   430 	     (* Check all vampire processes currently running for output                 *)
   431 	     (****************************************************************************) 
   432 							(*********************************)
   433 	      fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   434 							(*********************************)
   435 	      |   checkChildren ((childProc::otherChildren), toParentStr) = 
   436 		    let val (childInput,childOutput) =  cmdstreamsOf childProc
   437 			val child_handle= cmdchildHandle childProc
   438 			(* childCmd is the .dfg file that the problem is in *)
   439 			val childCmd = fst(snd (cmdchildInfo childProc))
   440 			(* now get the number of the subgoal from the filename *)
   441 			val sg_num = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
   442 			val childIncoming = pollChildInput childInput
   443 			val parentID = Posix.ProcEnv.getppid()
   444 			val prover = cmdProver childProc
   445 			val thmstring = cmdThm childProc
   446 			val sign = sign_of_thm thm
   447 			val prems = prems_of thm
   448 			val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   449 			val _ = warning("subgoals forked to checkChildren: "^prems_string)
   450 			val goalstring = cmdGoal childProc							
   451 			val _ = File.write (File.tmp_path (Path.basic "child_comms")) 
   452 			           (prover^thmstring^goalstring^childCmd)
   453 		    in 
   454 		      if (isSome childIncoming) 
   455 		      then 
   456 			  (* check here for prover label on child*)
   457 			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))  ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) 
   458 		      val childDone = (case prover of
   459 	    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   460 			   in
   461 			    if childDone      (**********************************************)
   462 			    then              (* child has found a proof and transferred it *)
   463 					      (**********************************************)
   464 
   465 			       (**********************************************)
   466 			       (* Remove this child and go on to check others*)
   467 			       (**********************************************)
   468 			       ( Unix.reap child_handle;
   469 				 checkChildren(otherChildren, toParentStr))
   470 			    else 
   471 			       (**********************************************)
   472 			       (* Keep this child and go on to check others  *)
   473 			       (**********************************************)
   474 
   475 				 (childProc::(checkChildren (otherChildren, toParentStr)))
   476 			 end
   477 		       else
   478 			 (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   479 			  childProc::(checkChildren (otherChildren, toParentStr)))
   480 		    end
   481 
   482 	     
   483 	  (********************************************************************)                  
   484 	  (* call resolution processes                                        *)
   485 	  (* settings should be a list of strings                             *)
   486 	  (* e.g. ["-t 300", "-m 100000"]                                     *)
   487 	  (* takes list of (string, string, string list, string)list proclist *)
   488 	  (********************************************************************)
   489 
   490 
   491 (*** add subgoal id num to this *)
   492 	     fun execCmds  [] procList = procList
   493 	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
   494 		   if (prover = "spass") 
   495 		   then 
   496 		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   497 			   val (instr, outstr)=Unix.streamsOf childhandle
   498 			   val newProcList =    (((CMDPROC{
   499 						prover = prover,
   500 						cmd = file,
   501 						thmstring = thmstring,
   502 						goalstring = goalstring,
   503 						proc_handle = childhandle,
   504 						instr = instr,
   505 						outstr = outstr })::procList))
   506 			    val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:"^goalstring^proverCmd^(concat settings)^file)
   507 		       in
   508 			  execCmds cmds newProcList
   509 		       end
   510 		   else 
   511 		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   512 			   val (instr, outstr)=Unix.streamsOf childhandle
   513 			   val newProcList =    (((CMDPROC{
   514 						prover = prover,
   515 						cmd = file,
   516 						thmstring = thmstring,
   517 						goalstring = goalstring,
   518 						proc_handle = childhandle,
   519 						instr = instr,
   520 						outstr = outstr })::procList))
   521 		       in
   522 			  execCmds cmds newProcList
   523 		       end
   524 
   525 
   526 
   527 	  (****************************************)                  
   528 	  (* call resolution processes remotely   *)
   529 	  (* settings should be a list of strings *)
   530 	  (* e.g. ["-t 300", "-m 100000"]         *)
   531 	  (****************************************)
   532 
   533 	   (*  fun execRemoteCmds  [] procList = procList
   534 	     |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   535 				       let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   536 					   in
   537 						execRemoteCmds  cmds newProcList
   538 					   end
   539 *)
   540 
   541 	     fun printList (outStr, []) = ()
   542 	     |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   543 
   544 
   545 	  (**********************************************)                  
   546 	  (* Watcher Loop                               *)
   547 	  (**********************************************)
   548 
   549 
   550 
   551 
   552 	      fun keepWatching (toParentStr, fromParentStr,procList) = 
   553 		    let    fun loop (procList) =  
   554 			   (
   555 			   let val cmdsFromIsa = pollParentInput ()
   556 			       fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
   557 					    TextIO.flushOut toParentStr;
   558 					     killChildren (map (cmdchildHandle) procList);
   559 					      ())
   560 			       
   561 			   in 
   562 			      (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   563 										 (**********************************)
   564 			      if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
   565 				   (                                             (**********************************)                             
   566 				    if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   567 				    then 
   568 				      (
   569 					let val child_handles = map cmdchildHandle procList 
   570 					in
   571 					   killChildren child_handles;
   572 					   (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                                              loop ([])
   573 					end
   574 					   
   575 				       )
   576 				    else
   577 				      ( 
   578 					if ((length procList)<10)    (********************)
   579 					then                        (* Execute locally  *)
   580 					   (                        (********************)
   581 					    let 
   582 					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   583 					      val parentID = Posix.ProcEnv.getppid()
   584 					      val newProcList' =checkChildren (newProcList, toParentStr) 
   585 					    in
   586 					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   587 					      loop (newProcList') 
   588 					    end
   589 					    )
   590 					else                         (*********************************)
   591 								     (* Execute remotely              *)
   592 								     (* (actually not remote for now )*)
   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 
   604 
   605 
   606 					)
   607 				     )                                              (******************************)
   608 			      else                                                  (* No new input from Isabelle *)
   609 										    (******************************)
   610 				  (    let val newProcList = checkChildren ((procList), toParentStr)
   611 				       in
   612 					 Posix.Process.sleep (Time.fromSeconds 1);
   613 					 loop (newProcList)
   614 				       end
   615 				   
   616 				   )
   617 			    end)
   618 		    in  
   619 			loop (procList)
   620 		    end
   621 		
   622     
   623 		in
   624 		 (***************************)
   625 		 (*** Sort out pipes ********)
   626 		 (***************************)
   627 
   628 		  Posix.IO.close (#outfd p1);
   629 		  Posix.IO.close (#infd p2);
   630 		  Posix.IO.dup2{old = oldchildin, new = fromParent};
   631 		  Posix.IO.close oldchildin;
   632 		  Posix.IO.dup2{old = oldchildout, new = toParent};
   633 		  Posix.IO.close oldchildout;
   634 
   635 		  (***************************)
   636 		  (* start the watcher loop  *)
   637 		  (***************************)
   638 		  keepWatching (toParentStr, fromParentStr, procList);
   639 
   640 
   641 		  (****************************************************************************)
   642 		  (* fake return value - actually want the watcher to loop until killed       *)
   643 		  (****************************************************************************)
   644 		  Posix.Process.wordToPid 0w0
   645 		  
   646 		end);
   647 	  (* end case *)
   648 
   649 
   650     val _ = TextIO.flushOut TextIO.stdOut
   651 
   652     (*******************************)
   653     (***  set watcher going ********)
   654     (*******************************)
   655 
   656     val procList = []
   657     val pid = startWatcher (procList)
   658     (**************************************************)
   659     (* communication streams to watcher               *)
   660     (**************************************************)
   661 
   662     val instr = openInFD ("_exec_in", #infd p2)
   663     val outstr = openOutFD ("_exec_out", #outfd p1)
   664     
   665     in
   666      (*******************************)
   667      (* close the child-side fds    *)
   668      (*******************************)
   669       Posix.IO.close (#outfd p2);
   670       Posix.IO.close (#infd p1);
   671       (* set the fds close on exec *)
   672       Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   673       Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   674        
   675      (*******************************)
   676      (* return value                *)
   677      (*******************************)
   678       PROC{pid = pid,
   679 	instr = instr,
   680 	outstr = outstr
   681       }
   682    end;
   683 
   684 
   685 
   686 (**********************************************************)
   687 (* Start a watcher and set up signal handlers             *)
   688 (**********************************************************)
   689 
   690 fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   691 
   692 fun reapWatcher(pid, instr, outstr) =
   693         let
   694 		val u = TextIO.closeIn instr;
   695 	        val u = TextIO.closeOut outstr;
   696 	
   697 		val (_, status) =
   698 			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
   699 	in
   700 		status
   701 	end
   702 
   703 fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = 
   704   let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   705       val streams =snd mychild
   706       val childin = fst streams
   707       val childout = snd streams
   708       val childpid = fst mychild
   709       val sign = sign_of_thm thm
   710       val prems = prems_of thm
   711       val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   712       val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   713       fun vampire_proofHandler (n) =
   714 	    (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   715 	    getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
   716      
   717 
   718       fun spass_proofHandler (n) = (
   719 	let val _ = File.write (File.tmp_path (Path.basic "foo_signal1")) "In signal handler now\n"
   720 	    val (reconstr, thmstring, goalstring) = getSpassInput childin
   721 	    val _ = File.append (File.tmp_path (Path.basic "foo_signal"))
   722 	              ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))
   723         in (* if a proof has been found and sent back as a reconstruction proof *)
   724 	  if ( (substring (reconstr, 0,1))= "[")
   725 	  then 
   726 	    (
   727 	     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   728 	     Recon_Transfer.apply_res_thm reconstr goalstring;
   729 	     Pretty.writeln(Pretty.str  (oct_char "361"));
   730 	     
   731 	     goals_being_watched := ((!goals_being_watched) - 1);
   732      
   733 	     if ((!goals_being_watched) = 0)
   734 	     then 
   735 		(let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found"))
   736 		     ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")
   737 		 in
   738 		     reapWatcher (childpid,childin, childout); ()
   739 		 end)
   740 	     else ()
   741 	    )
   742 	    (* if there's no proof, but a message from Spass *)
   743 	    else if ((substring (reconstr, 0,5))= "SPASS")
   744 		 then
   745 		    (goals_being_watched := (!goals_being_watched) -1;
   746 		     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   747 		      Pretty.writeln(Pretty.str (goalstring^reconstr));
   748 		      Pretty.writeln(Pretty.str  (oct_char "361"));
   749 		      if (!goals_being_watched = 0)
   750 		      then 
   751 			  (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   752 			       ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   753 			   reapWatcher (childpid,childin, childout); ())
   754 		      else
   755 			 ()
   756 		)
   757 		  (* if proof translation failed *)
   758 		  else if ((substring (reconstr, 0,5)) = "Proof")
   759 		  then 
   760 		     (goals_being_watched := (!goals_being_watched) -1;
   761 		      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   762 		       Pretty.writeln(Pretty.str (goalstring^reconstr));
   763 		       Pretty.writeln(Pretty.str  (oct_char "361"));
   764 		       if (!goals_being_watched = 0)
   765 		       then 
   766 			  (File.write(File.tmp_path (Path.basic "foo_reap_comp"))
   767 			      ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   768 			   reapWatcher (childpid,childin, childout); ())		       
   769 		       else ())
   770 	 	  else () (* add something here ?*)
   771 	     end)
   772 
   773 
   774    
   775   in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   776      IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   777      (childin, childout, childpid)
   778 
   779   end
   780 
   781 
   782 
   783 
   784 
   785 end (* structure Watcher *)