src/HOL/Tools/ATP/watcher.ML
author quigley
Tue May 31 12:42:36 2005 +0200 (2005-05-31)
changeset 16156 2f6fc19aba1e
parent 16100 f80fc4bff933
child 16185 bb71c91e781e
permissions -rw-r--r--
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
ruleset.
     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 (*****************************************************************************************)
   155 
   156 (* need to modify to send over hyps file too *)
   157 fun callResProvers (toWatcherStr,  []) =
   158       (sendOutput (toWatcherStr, "End of calls\n"); 
   159        TextIO.flushOut toWatcherStr)
   160 |   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) =
   161       let val dfg_dir = File.tmp_path (Path.basic "dfg"); 
   162 	 (*** need to check here if the directory exists and, if not, create it***)
   163 	  val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))                                                                     
   164 	              (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n")
   165 	 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
   166 	 val probID = ReconOrderClauses.last(explode probfile)
   167 	  val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
   168 	  (*** only include problem and clasimp for the moment, not sure how to refer to ***)
   169 
   170 	  (*** hyps/local axioms just now (*,axfile, hypsfile,*)                                               ***)
   171 	  val whole_prob_file = system ("/bin/cat " ^ clasimpfile ^" "^ probfile ^ " > " ^ (File.sysify_path wholefile))
   172 
   173 	  val dfg_create = if File.exists dfg_dir 
   174 			   then warning("dfg dir exists")
   175 			   else File.mkdir dfg_dir; 
   176 	  
   177 	  val dfg_path = File.sysify_path dfg_dir;
   178 	  val exec_tptp2x = 
   179 	        Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X",  
   180 	                     ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile])
   181 	(*val _ = Posix.Process.wait ()*)
   182 	(*val _ =Unix.reap exec_tptp2x*)
   183 	  val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
   184  
   185        in   
   186 	  goals_being_watched := (!goals_being_watched) + 1;
   187 	  Posix.Process.sleep(Time.fromSeconds 1); 
   188 	  (warning ("probfile is: "^probfile));
   189 	  (warning("dfg file is: "^newfile));
   190 	  (warning ("wholefile is: "^(File.sysify_path wholefile)));
   191 	  sendOutput (toWatcherStr,
   192 	       prover ^ "*" ^ thmstring ^ "*" ^ goalstring ^ "*" ^ proverCmd ^ 
   193 	       "*" ^ settings ^ "*" ^ newfile ^ "\n");
   194  (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
   195 	  TextIO.flushOut toWatcherStr;
   196 	  Unix.reap exec_tptp2x;
   197 	  if File.exists
   198 	        (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg")))
   199 	  then callResProvers (toWatcherStr, args)
   200 	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^
   201 	              " -fdfg " ^ File.sysify_path wholefile ^ " -d " ^ dfg_path)
   202       end
   203 (*
   204 fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
   205                                      
   206 |   callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile, probfile)::args) =
   207                                             ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^clasimpfile^"*"^axfile^"*"^hypsfile^"*"^probfile^"\n")
   208                                             
   209      *)                                      
   210  
   211 (**************************************************************)
   212 (* Send message to watcher to kill currently running vampires *)
   213 (**************************************************************)
   214 
   215 fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 
   216                             TextIO.flushOut toWatcherStr)
   217 
   218 
   219 
   220 (**************************************************************)
   221 (* Remove \n token from a vampire goal filename and extract   *)
   222 (* prover, proverCmd, settings and file from input string     *)
   223 (**************************************************************)
   224 
   225 
   226  fun takeUntil ch [] res  = (res, [])
   227  |   takeUntil ch (x::xs) res = if   x = ch 
   228                                 then
   229                                      (res, xs)
   230                                 else
   231                                      takeUntil ch xs (res@[x])
   232 
   233  fun getSettings [] settings = settings
   234 |    getSettings (xs) settings = let val (set, rest ) = takeUntil "%" xs []
   235                                  in
   236                                      getSettings rest (settings@[(implode set)])
   237                                  end
   238 
   239 fun separateFields str =
   240   let val (prover, rest) = takeUntil "*" str []
   241       val prover = implode prover
   242       val (thmstring, rest) =  takeUntil "*" rest []
   243       val thmstring = implode thmstring
   244       val (goalstring, rest) =  takeUntil "*" rest []
   245       val goalstring = implode goalstring
   246       val (proverCmd, rest ) =  takeUntil "*" rest []
   247       val proverCmd = implode proverCmd
   248       
   249       val (settings, rest) =  takeUntil "*" rest []
   250       val settings = getSettings settings []
   251       val (file, rest) =  takeUntil "*" rest []
   252       val file = implode file
   253       val _ = File.write (File.tmp_path (Path.basic "sep_comms"))
   254                 (prover^thmstring^goalstring^proverCmd^file) 
   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 2000)) 
   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 2000)) 
   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 			val _ = File.write (File.tmp_path (Path.basic "child_comms")) 
   454 			           (prover^thmstring^goalstring^childCmd)
   455 		    in 
   456 		      if (isSome childIncoming) 
   457 		      then 
   458 			  (* check here for prover label on child*)
   459 			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))  ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) 
   460 		      val childDone = (case prover of
   461 	    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   462 			   in
   463 			    if childDone      (**********************************************)
   464 			    then              (* child has found a proof and transferred it *)
   465 					      (**********************************************)
   466 
   467 			       (**********************************************)
   468 			       (* Remove this child and go on to check others*)
   469 			       (**********************************************)
   470 			       ( Unix.reap child_handle;
   471 				 checkChildren(otherChildren, toParentStr))
   472 			    else 
   473 			       (**********************************************)
   474 			       (* Keep this child and go on to check others  *)
   475 			       (**********************************************)
   476 
   477 				 (childProc::(checkChildren (otherChildren, toParentStr)))
   478 			 end
   479 		       else
   480 			 (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   481 			  childProc::(checkChildren (otherChildren, toParentStr)))
   482 		    end
   483 
   484 	     
   485 	  (********************************************************************)                  
   486 	  (* call resolution processes                                        *)
   487 	  (* settings should be a list of strings                             *)
   488 	  (* e.g. ["-t 300", "-m 100000"]                                     *)
   489 	  (* takes list of (string, string, string list, string)list proclist *)
   490 	  (********************************************************************)
   491 
   492 
   493 (*** add subgoal id num to this *)
   494 	     fun execCmds  [] procList = procList
   495 	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
   496 		   if (prover = "spass") 
   497 		   then 
   498 		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   499 			   val (instr, outstr)=Unix.streamsOf childhandle
   500 			   val newProcList =    (((CMDPROC{
   501 						prover = prover,
   502 						cmd = file,
   503 						thmstring = thmstring,
   504 						goalstring = goalstring,
   505 						proc_handle = childhandle,
   506 						instr = instr,
   507 						outstr = outstr })::procList))
   508 			    val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:"^goalstring^proverCmd^(concat settings)^file)
   509 		       in
   510 			  execCmds cmds newProcList
   511 		       end
   512 		   else 
   513 		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   514 			   val (instr, outstr)=Unix.streamsOf childhandle
   515 			   val newProcList =    (((CMDPROC{
   516 						prover = prover,
   517 						cmd = file,
   518 						thmstring = thmstring,
   519 						goalstring = goalstring,
   520 						proc_handle = childhandle,
   521 						instr = instr,
   522 						outstr = outstr })::procList))
   523 		       in
   524 			  execCmds cmds newProcList
   525 		       end
   526 
   527 
   528 
   529 	  (****************************************)                  
   530 	  (* call resolution processes remotely   *)
   531 	  (* settings should be a list of strings *)
   532 	  (* e.g. ["-t 300", "-m 100000"]         *)
   533 	  (****************************************)
   534 
   535 	   (*  fun execRemoteCmds  [] procList = procList
   536 	     |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   537 				       let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   538 					   in
   539 						execRemoteCmds  cmds newProcList
   540 					   end
   541 *)
   542 
   543 	     fun printList (outStr, []) = ()
   544 	     |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   545 
   546 
   547 	  (**********************************************)                  
   548 	  (* Watcher Loop                               *)
   549 	  (**********************************************)
   550 
   551 
   552 
   553 
   554 	      fun keepWatching (toParentStr, fromParentStr,procList) = 
   555 		    let    fun loop (procList) =  
   556 			   (
   557 			   let val cmdsFromIsa = pollParentInput ()
   558 			       fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
   559 					    TextIO.flushOut toParentStr;
   560 					     killChildren (map (cmdchildHandle) procList);
   561 					      ())
   562 			       
   563 			   in 
   564 			      (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   565 										 (**********************************)
   566 			      if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
   567 				   (                                             (**********************************)                             
   568 				    if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   569 				    then 
   570 				      (
   571 					let val child_handles = map cmdchildHandle procList 
   572 					in
   573 					   killChildren child_handles;
   574 					   (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                                              loop ([])
   575 					end
   576 					   
   577 				       )
   578 				    else
   579 				      ( 
   580 					if ((length procList)<10)    (********************)
   581 					then                        (* Execute locally  *)
   582 					   (                        (********************)
   583 					    let 
   584 					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   585 					      val parentID = Posix.ProcEnv.getppid()
   586 					      val newProcList' =checkChildren (newProcList, toParentStr) 
   587 					    in
   588 					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   589 					      loop (newProcList') 
   590 					    end
   591 					    )
   592 					else                         (*********************************)
   593 								     (* Execute remotely              *)
   594 								     (* (actually not remote for now )*)
   595 					    (                        (*********************************)
   596 					    let 
   597 					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   598 					      val parentID = Posix.ProcEnv.getppid()
   599 					      val newProcList' =checkChildren (newProcList, toParentStr) 
   600 					    in
   601 					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   602 					      loop (newProcList') 
   603 					    end
   604 					    )
   605 
   606 
   607 
   608 					)
   609 				     )                                              (******************************)
   610 			      else                                                  (* No new input from Isabelle *)
   611 										    (******************************)
   612 				  (    let val newProcList = checkChildren ((procList), toParentStr)
   613 				       in
   614 					 Posix.Process.sleep (Time.fromSeconds 1);
   615 					 loop (newProcList)
   616 				       end
   617 				   
   618 				   )
   619 			    end)
   620 		    in  
   621 			loop (procList)
   622 		    end
   623 		
   624     
   625 		in
   626 		 (***************************)
   627 		 (*** Sort out pipes ********)
   628 		 (***************************)
   629 
   630 		  Posix.IO.close (#outfd p1);
   631 		  Posix.IO.close (#infd p2);
   632 		  Posix.IO.dup2{old = oldchildin, new = fromParent};
   633 		  Posix.IO.close oldchildin;
   634 		  Posix.IO.dup2{old = oldchildout, new = toParent};
   635 		  Posix.IO.close oldchildout;
   636 
   637 		  (***************************)
   638 		  (* start the watcher loop  *)
   639 		  (***************************)
   640 		  keepWatching (toParentStr, fromParentStr, procList);
   641 
   642 
   643 		  (****************************************************************************)
   644 		  (* fake return value - actually want the watcher to loop until killed       *)
   645 		  (****************************************************************************)
   646 		  Posix.Process.wordToPid 0w0
   647 		  
   648 		end);
   649 	  (* end case *)
   650 
   651 
   652     val _ = TextIO.flushOut TextIO.stdOut
   653 
   654     (*******************************)
   655     (***  set watcher going ********)
   656     (*******************************)
   657 
   658     val procList = []
   659     val pid = startWatcher (procList)
   660     (**************************************************)
   661     (* communication streams to watcher               *)
   662     (**************************************************)
   663 
   664     val instr = openInFD ("_exec_in", #infd p2)
   665     val outstr = openOutFD ("_exec_out", #outfd p1)
   666     
   667     in
   668      (*******************************)
   669      (* close the child-side fds    *)
   670      (*******************************)
   671       Posix.IO.close (#outfd p2);
   672       Posix.IO.close (#infd p1);
   673       (* set the fds close on exec *)
   674       Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   675       Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   676        
   677      (*******************************)
   678      (* return value                *)
   679      (*******************************)
   680       PROC{pid = pid,
   681 	instr = instr,
   682 	outstr = outstr
   683       }
   684    end;
   685 
   686 
   687 
   688 (**********************************************************)
   689 (* Start a watcher and set up signal handlers             *)
   690 (**********************************************************)
   691 
   692 fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   693 
   694 fun reapWatcher(pid, instr, outstr) =
   695         let
   696 		val u = TextIO.closeIn instr;
   697 	        val u = TextIO.closeOut outstr;
   698 	
   699 		val (_, status) =
   700 			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
   701 	in
   702 		status
   703 	end
   704 
   705 
   706 fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   707 			   val streams =snd mychild
   708                            val childin = fst streams
   709                            val childout = snd streams
   710                            val childpid = fst mychild
   711                            val sign = sign_of_thm thm
   712                            val prems = prems_of thm
   713                            val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   714                            val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   715                            fun vampire_proofHandler (n) =
   716                            (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   717                            getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
   718                           
   719 
   720 fun spass_proofHandler (n) = (
   721                                  let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
   722                                       val _ = TextIO.output (outfile, ("In signal handler now\n"))
   723                                       val _ =  TextIO.closeOut outfile
   724                                       val (reconstr, thmstring, goalstring) = SpassComm.getSpassInput childin
   725                                       val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
   726 
   727                                       val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   728                                       val _ =  TextIO.closeOut outfile
   729                                       in          (* if a proof has been found and sent back as a reconstruction proof *)
   730                                                   if ( (substring (reconstr, 0,1))= "[")
   731                                                   then 
   732 
   733                                                             (
   734                                                                  Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   735                                                                  Recon_Transfer.apply_res_thm reconstr goalstring;
   736                                                                  Pretty.writeln(Pretty.str  (oct_char "361"));
   737                                                                  
   738                                                                  goals_being_watched := ((!goals_being_watched) - 1);
   739                                                          
   740                                                                  if ((!goals_being_watched) = 0)
   741                                                                  then 
   742                                                                     (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_found")));
   743                                                                          val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   744                                                                          val _ =  TextIO.closeOut outfile
   745                                                                      in
   746                                                                          killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   747                                                                      end)
   748                                                                  else
   749                                                                     ()
   750                                                             )
   751                                                     (* if there's no proof, but a message from Spass *)
   752                                                     else if ((substring (reconstr, 0,5))= "SPASS")
   753                                                          then
   754                                                                  (
   755                                                                      goals_being_watched := (!goals_being_watched) -1;
   756                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   757                                                                       Pretty.writeln(Pretty.str (goalstring^reconstr));
   758                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   759                                                                       if (!goals_being_watched = 0)
   760                                                                       then 
   761                                                                           (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   762                                                                                val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   763                                                                                val _ =  TextIO.closeOut outfile
   764                                                                            in
   765                                                                               killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   766                                                                            end )
   767                                                                       else
   768                                                                          ()
   769                                                                 ) 
   770 						   (* print out a list of rules used from clasimpset*)
   771                                                     else if ((substring (reconstr, 0,5))= "Rules")
   772                                                          then
   773                                                                  (
   774                                                                      goals_being_watched := (!goals_being_watched) -1;
   775                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   776                                                                       Pretty.writeln(Pretty.str (goalstring^reconstr));
   777                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   778                                                                       if (!goals_being_watched = 0)
   779                                                                       then 
   780                                                                           (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   781                                                                                val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   782                                                                                val _ =  TextIO.closeOut outfile
   783                                                                            in
   784                                                                               killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   785                                                                            end )
   786                                                                       else
   787                                                                          ()
   788                                                                 )
   789 							
   790                                                           (* if proof translation failed *)
   791                                                           else if ((substring (reconstr, 0,5)) = "Proof")
   792                                                                then 
   793                                                                    (
   794                                                                      goals_being_watched := (!goals_being_watched) -1;
   795                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   796                                                                       Pretty.writeln(Pretty.str (goalstring^reconstr));
   797                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   798                                                                       if (!goals_being_watched = 0)
   799                                                                       then 
   800                                                                           (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   801                                                                                val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   802                                                                                val _ =  TextIO.closeOut outfile
   803                                                                            in
   804                                                                               killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   805                                                                            end )
   806                                                                       else
   807                                                                          ()
   808                                                                 )
   809 
   810 
   811                                                                 else  (* add something here ?*)
   812                                                                    ()
   813                                                              
   814                                        end)
   815 
   816 
   817                         
   818                        in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   819                           IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   820                           (childin, childout, childpid)
   821 
   822 
   823   end
   824 
   825 
   826 
   827 
   828 
   829 end (* structure Watcher *)