(*  Title:      Watcher.ML

    ID:         $Id$

    Author:     Claire Quigley

    Copyright   2004  University of Cambridge

 *)

 (***************************************************************************)

 (*  The watcher process starts a resolution process when it receives a     *)

(*  message from Isabelle                                                  *)

(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)

(*  and removes dead processes.  Also possible to kill all the resolution  *)

(*  processes currently running.                                           *)

(*  Hardwired version of where to pick up the tptp files for the moment    *)

(***************************************************************************)

(*use "Proof_Transfer";

use "VampireCommunication";

use "SpassCommunication";*)

(*use "/homes/clq20/Jia_Code/TransStartIsar";*)

structure Watcher: WATCHER =

  struct

val goals_being_watched = ref 0;

(*****************************************)

(*  The result of calling createWatcher  *)

(*****************************************)

datatype proc = PROC of {

        pid : Posix.Process.pid,

        instr : TextIO.instream,

        outstr : TextIO.outstream

      };

(*****************************************)

(*  The result of calling executeToList  *)

(*****************************************)

datatype cmdproc = CMDPROC of {

        prover: string,             (* Name of the resolution prover used, e.g. Vampire, SPASS *)

        cmd:  string,              (* The file containing the goal for res prover to prove *)     

        thmstring: string,         (* string representation of subgoal after negation, skolemization*) 

        goalstring: string,         (* string representation of subgoal*) 

        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,

        instr : TextIO.instream,   (*  Input stream to child process *)

        outstr : TextIO.outstream  (*  Output stream from child process *)

      };

type signal = Posix.Signal.signal

datatype exit_status = datatype Posix.Process.exit_status

val fromStatus = Posix.Process.fromStatus

fun reap(pid, instr, outstr) =

        let

		val u = TextIO.closeIn instr;

	        val u = TextIO.closeOut outstr;

		val (_, status) =

			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])

	in

		status

	end

fun fdReader (name : string, fd : Posix.IO.file_desc) =

	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };

fun fdWriter (name, fd) =

          Posix.IO.mkTextWriter {

	      appendMode = false,

              initBlkMode = true,

              name = name,  

              chunkSize=4096,

              fd = fd

            };

fun openOutFD (name, fd) =

	  TextIO.mkOutstream (

	    TextIO.StreamIO.mkOutstream (

	      fdWriter (name, fd), IO.BLOCK_BUF));

fun openInFD (name, fd) =

	  TextIO.mkInstream (

	    TextIO.StreamIO.mkInstream (

	      fdReader (name, fd), ""));

fun killChild child_handle = Unix.reap child_handle 

fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));

fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);

fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);

fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = (prover,(cmd, (instr,outstr)));

fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = proc_handle;

fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (prover);

fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (thmstring);

fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (goalstring);

fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);

(********************************************************************************************)

(*  takes a list of arguments and sends them individually to the watcher process by pipe    *)

(********************************************************************************************)

fun outputArgs (toWatcherStr, []) = ()

|   outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); 

                                          TextIO.flushOut toWatcherStr;

                                         outputArgs (toWatcherStr, xs))

(********************************************************************************)

(*    gets individual args from instream and concatenates them into a list      *)

(********************************************************************************)

fun getArgs (fromParentStr, toParentStr,ys) =  let 

                                       val thisLine = TextIO.input fromParentStr

                                    in

                                        ((ys@[thisLine]))

                                    end

(********************************************************************************)

(*  Remove the \n character from the end of each filename                       *)

(********************************************************************************)

fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 

                    in

                        if (String.isPrefix "\n"  (implode backList )) 

                        then (implode (rev ((tl backList))))

                        else cmdStr

                    end

(********************************************************************************)

(*  Send request to Watcher for a vampire to be called for filename in arg      *)

(********************************************************************************)

fun callResProver (toWatcherStr,  arg) = (sendOutput (toWatcherStr, arg^"\n"); 

                                     TextIO.flushOut toWatcherStr)

(*****************************************************************************************)

(*  Send request to Watcher for multiple provers to be called for filenames in arg       *)

(*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)

(*****************************************************************************************)

(* need to modify to send over hyps file too *)

fun callResProvers (toWatcherStr,  []) = (sendOutput (toWatcherStr, "End of calls\n"); 

                                     TextIO.flushOut toWatcherStr)

|   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) =

                                          let  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "tog_comms")));                                                                                    

                              val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^settings^clasimpfile^hypsfile^probfile) )

                              val _ =  TextIO.closeOut outfile

                                        in   (sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^

							             settings^"*"^clasimpfile^"*"^hypsfile^"*"^probfile^"\n"));

                                          goals_being_watched := (!goals_being_watched) + 1;

                                          TextIO.flushOut toWatcherStr;

                                          callResProvers (toWatcherStr,args))

                                        end   

(*

fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 

|   callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile, probfile)::args) =

                                            ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^clasimpfile^"*"^axfile^"*"^hypsfile^"*"^probfile^"\n")

     *)                                      

(**************************************************************)

(* Send message to watcher to kill currently running vampires *)

(**************************************************************)

fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 

                            TextIO.flushOut toWatcherStr)

(**************************************************************)

(* Remove \n token from a vampire goal filename and extract   *)

(* prover, proverCmd, settings and file from input string     *)

(**************************************************************)

 fun takeUntil ch [] res  = (res, [])

 |   takeUntil ch (x::xs) res = if   x = ch 

                                then

                                     (res, xs)

                                else

                                     takeUntil ch xs (res@[x])

 fun getSettings [] settings = settings

|    getSettings (xs) settings = let val (set, rest ) = takeUntil "%" xs []

                                 in

                                     getSettings rest (settings@[(implode set)])

                                 end

fun separateFields str = let val  outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field")))                                                                         

                              val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") )

                              val _ =  TextIO.closeOut outfile

                              val (prover, rest) = takeUntil "*" str []

                              val prover = implode prover

                              val (thmstring, rest) =  takeUntil "*" rest []

                              val thmstring = implode thmstring

                              val (goalstring, rest) =  takeUntil "*" rest []

                              val goalstring = implode goalstring

                              val (proverCmd, rest ) =  takeUntil "*" rest []

                              val proverCmd = implode proverCmd

                              val (settings, rest) =  takeUntil "*" rest []

                              val settings = getSettings settings []

			      val (clasimpfile, rest ) =  takeUntil "*" rest []

                              val clasimpfile = implode clasimpfile

  			      val (hypsfile, rest ) =  takeUntil "*" rest []

                              val hypsfile = implode hypsfile

                              val (file, rest) =  takeUntil "*" rest []

                              val file = implode file

                              val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "sep_comms")));                                                                                    

                              val _ = TextIO.output (outfile,("Sep comms are: "^(implode str)^"**"^prover^thmstring^goalstring^proverCmd^clasimpfile^hypsfile^file^"\n\n") )

                              val _ =  TextIO.closeOut outfile

                          in

                             (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file)

                          end

(***********************************************************************************)

(* do tptp2x and cat to turn clasimpfile, hypsfile and probfile into one .dfg file *)

(***********************************************************************************)

fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile ,probfile) = 

 let

		val dfg_dir = File.tmp_path (Path.basic "dfg"); 

  		(*** need to check here if the directory exists and, if not, create it***)

 		(*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)

		val probID = List.last(explode probfile)

    		val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))

    		(*** only include problem and clasimp for the moment, not sure how to refer to ***)

   		(*** hyps/local axioms just now                                                ***)

   		val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])

    		val dfg_create =

 		if File.exists dfg_dir 

     	        then

     	            ((warning("dfg dir exists"));())

 		else

 		     File.mkdir dfg_dir; 

   		val dfg_path = File.platform_path dfg_dir;

   		val bar = system ("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X -fdfg "^

                                 (File.platform_path wholefile)^" -d "^dfg_path)

    		val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"

                val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic"thmstring_in_watcher")));   

   		val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n"))

 		val _ =  TextIO.closeOut outfile

 	     in

 		(prover,thmstring,goalstring, proverCmd, settings,newfile)	

	     end;

(* remove \n from end of command and put back into tuple format *)

(*  val cmdStr = "spass*((ALL xa. (~ P x | P xa) & (~ P xa | P x)) & (P xa | (ALL x. P x)) & ((ALL x. ~ P x) | ~ P xb) [.])*(EX x. ALL y. P x = P y) --> (EX x. P x) = (ALL y. P y)*/homes/clq20/bin/SPASS*-DocProof*/local/scratch/clq20/27023/clasimp*/local/scratch/clq20/27023/hyps*/local/scratch/clq20/27023/prob_1\n" *)

(*FIX:  are the two getCmd procs getting confused?  Why do I have two anyway? *)

 fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 

                         val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic"cmdStr")));   

   		val _ = TextIO.output (outfile, (cmdStr))

 		val _ =  TextIO.closeOut outfile

                     in

                         if (String.isPrefix "\n"  (implode backList )) 

                         then 

                            ( let 

              val newCmdStr = (rev(tl backList))

              val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic"backlist")));   

   		val _ = TextIO.output (outfile, ("about to call sepfields with "^(implode newCmdStr)))

 		val _ =  TextIO.closeOut outfile 

				 val cmdtuple = separateFields newCmdStr

                             in 

 				 formatCmd cmdtuple

			     end)

                         else

                          ( let 

			      val cmdtuple =(separateFields (explode cmdStr))

			   in

 				formatCmd cmdtuple

			   end)

                     end

fun getProofCmd (a,b,c,d,e,f) = d

(**************************************************************)

(* Get commands from Isabelle                                 *)

(**************************************************************)

(* FIX: or perhaps do the tptp2x stuff here - so it's get commands and then format them, before passing them to spass *)

fun getCmds (toParentStr,fromParentStr, cmdList) = 

                                       let val thisLine = TextIO.inputLine fromParentStr 

                                           val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "parent_comms")));                                                                                    

                              val _ = TextIO.output (outfile,(thisLine) )

                              val _ =  TextIO.closeOut outfile

                                       in

                                          (if (thisLine = "End of calls\n") 

                                           then 

                                              (cmdList)

                                           else if (thisLine = "Kill children\n") 

                                                then 

                                                    (   TextIO.output (toParentStr,thisLine ); 

                                                        TextIO.flushOut toParentStr;

                                                      (("","","","Kill children",[],"")::cmdList)

                                                     )

                                              else (let val thisCmd = getCmd (thisLine) 

							(*********************************************************)

                                                        (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)

						        (* i.e. put back into tuple format                       *)

							(*********************************************************)

                                                    in

                                                      (*TextIO.output (toParentStr, thisCmd); 

                                                        TextIO.flushOut toParentStr;*)

                                                        getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))

                                                    end

                                                    )

                                            )

                                        end

(**************************************************************)

(*  Get Io-descriptor for polling of an input stream          *)

(**************************************************************)

fun getInIoDesc someInstr = 

    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)

        val _ = TextIO.output (TextIO.stdOut, buf)

        val ioDesc = 

	    case rd

	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod

	       | _ => NONE

     in (* since getting the reader will have terminated the stream, we need

	 * to build a new stream. *)

	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));

	ioDesc

    end

(*************************************)

(*  Set up a Watcher Process         *)

(*************************************)

fun setupWatcher (thm,clause_arr, num_of_clauses) = 

  let

    (** pipes for communication between parent and watcher **)

    val p1 = Posix.IO.pipe ()

    val p2 = Posix.IO.pipe ()

    fun closep () = (

	  Posix.IO.close (#outfd p1); 

	  Posix.IO.close (#infd p1);

	  Posix.IO.close (#outfd p2); 

	  Posix.IO.close (#infd p2)

	)

    (***********************************************************)

    (****** fork a watcher process and get it set up and going *)

    (***********************************************************)

    fun startWatcher (procList) =

	     (case  Posix.Process.fork() (***************************************)

	   of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)

					 (***************************************)

					   (*************************)

	    | NONE => let                  (* child - i.e. watcher  *)

		val oldchildin = #infd p1  (*************************)

		val fromParent = Posix.FileSys.wordToFD 0w0

		val oldchildout = #outfd p2

		val toParent = Posix.FileSys.wordToFD 0w1

		val fromParentIOD = Posix.FileSys.fdToIOD fromParent

		val fromParentStr = openInFD ("_exec_in_parent", fromParent)

		val toParentStr = openOutFD ("_exec_out_parent", toParent)

		val sign = sign_of_thm thm

		val prems = prems_of thm

		val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 

		val _ = (warning ("subgoals forked to startWatcher: "^prems_string));

	       (* tracing *)

	      (*val tenth_ax = fst( Array.sub(clause_arr, 1))  

		val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)

		val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)

		val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         

		val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         

		val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       

			 *)

		(*val goalstr = string_of_thm (the_goal)

		 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher")));  

		val _ = TextIO.output (outfile,goalstr )

		val _ =  TextIO.closeOut outfile*)

		fun killChildren [] = ()

	     |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)

	      (*************************************************************)

	      (* take an instream and poll its underlying reader for input *)

	      (*************************************************************)

	      fun pollParentInput () = 

			 let val pd = OS.IO.pollDesc (fromParentIOD)

			 in 

			 if (isSome pd ) then 

			     let val pd' = OS.IO.pollIn (valOf pd)

				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 

				 val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 

			           ("In parent_poll\n")	

			     in

				if null pdl 

				then

				   NONE

				else if (OS.IO.isIn (hd pdl)) 

				     then

					(SOME ( getCmds (toParentStr, fromParentStr, [])))

				     else

					 NONE

			     end

			   else

			       NONE

			   end

	       fun pollChildInput (fromStr) = 

		     let val iod = getInIoDesc fromStr

		     in 

		     if isSome iod 

		     then 

			 let val pd = OS.IO.pollDesc (valOf iod)

			 in 

			 if (isSome pd ) then 

			     let val pd' = OS.IO.pollIn (valOf pd)

				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 

                                 val _ = File.append (File.tmp_path (Path.basic "child_poll")) 

			           ("In child_poll\n")

			     in

				if null pdl 

				then

				   NONE

				else if (OS.IO.isIn (hd pdl)) 

				     then

					 SOME ((*getCmd*) (TextIO.inputLine fromStr))

				     else

					 NONE

			     end

			   else

			       NONE

			   end

		       else 

			   NONE

		      end

	     (****************************************************************************)

	     (* Check all vampire processes currently running for output                 *)

	     (****************************************************************************) 

							(*********************************)

	      fun checkChildren ([], toParentStr) = []  (*** no children to check ********)

							(*********************************)

	      |   checkChildren ((childProc::otherChildren), toParentStr) = 

		    let val _ = File.append (File.tmp_path (Path.basic "child_check")) 

			           ("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n")

                        val (childInput,childOutput) =  cmdstreamsOf childProc

			val child_handle= cmdchildHandle childProc

			(* childCmd is the .dfg file that the problem is in *)

			val childCmd = fst(snd (cmdchildInfo childProc))

                        val _ = File.append (File.tmp_path (Path.basic "child_command")) 

			           (childCmd^"\n")

			(* now get the number of the subgoal from the filename *)

			val sg_num = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))

			val childIncoming = pollChildInput childInput

 			val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) 

			           ("finished polling child \n")

			val parentID = Posix.ProcEnv.getppid()

			val prover = cmdProver childProc

			val thmstring = cmdThm childProc

			val sign = sign_of_thm thm

			val prems = prems_of thm

			val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 

			val _ = warning("subgoals forked to checkChildren: "^prems_string)

			val goalstring = cmdGoal childProc							

			val _ = File.append (File.tmp_path (Path.basic "child_comms")) 

			           (prover^thmstring^goalstring^childCmd^"\n")

		    in 

		      if (isSome childIncoming) 

		      then 

			  (* check here for prover label on child*)

			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))  ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) 

		      val childDone = (case prover of

	    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )

			   in

			    if childDone      (**********************************************)

			    then              (* child has found a proof and transferred it *)

					      (**********************************************)

			       (**********************************************)

			       (* Remove this child and go on to check others*)

			       (**********************************************)

			       ( Unix.reap child_handle;

				 checkChildren(otherChildren, toParentStr))

			    else 

			       (**********************************************)

			       (* Keep this child and go on to check others  *)

			       (**********************************************)

				 (childProc::(checkChildren (otherChildren, toParentStr)))

			 end

		       else

			 (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";

			  childProc::(checkChildren (otherChildren, toParentStr)))

		    end

	  (********************************************************************)                  

	  (* call resolution processes                                        *)

	  (* settings should be a list of strings                             *)

	  (* e.g. ["-t 300", "-m 100000"]                                     *)

	  (* takes list of (string, string, string list, string)list proclist *)

	  (********************************************************************)

(*** add subgoal id num to this *)

	     fun execCmds  [] procList = procList

	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =             let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child"))  ("About to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))

	       in 

		 if (prover = "spass") 

		   then 

		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))

			   val (instr, outstr)=Unix.streamsOf childhandle

			   val newProcList =    (((CMDPROC{

						prover = prover,

						cmd = file,

						thmstring = thmstring,

						goalstring = goalstring,

						proc_handle = childhandle,

						instr = instr,

						outstr = outstr })::procList))

			    val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))

		       in

			  Posix.Process.sleep (Time.fromSeconds 1);execCmds cmds newProcList

		       end

		   else 

		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (settings@[file])))

			   val (instr, outstr)=Unix.streamsOf childhandle

			   val newProcList =    (((CMDPROC{

						prover = prover,

						cmd = file,

						thmstring = thmstring,

						goalstring = goalstring,

						proc_handle = childhandle,

						instr = instr,

						outstr = outstr })::procList))

		       in

			 Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList

		       end

		end

	  (****************************************)                  

	  (* call resolution processes remotely   *)

	  (* settings should be a list of strings *)

	  (* e.g. ["-t 300", "-m 100000"]         *)

	  (****************************************)

	   (*  fun execRemoteCmds  [] procList = procList

	     |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  

				       let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)

					   in

						execRemoteCmds  cmds newProcList

					   end

*)

	     fun printList (outStr, []) = ()

	     |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  

	  (**********************************************)                  

	  (* Watcher Loop                               *)

	  (**********************************************)

	      fun keepWatching (toParentStr, fromParentStr,procList) = 

		    let    fun loop (procList) =  

			   (

			   let val cmdsFromIsa = pollParentInput ()

			       fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");

					    TextIO.flushOut toParentStr;

					     killChildren (map (cmdchildHandle) procList);

					      ())

			   in 

			      (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)

										 (**********************************)

			      if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)

				   (                                             (**********************************)                             

				    if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )

				    then 

				      (

					let val child_handles = map cmdchildHandle procList 

					in

					   killChildren child_handles;

					   (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                                              loop ([])

					end

				       )

				    else

				      ( 

					if ((length procList)<10)    (********************)

					then                        (* Execute locally  *)

					   (                        (********************)

					    let 

					      val newProcList = execCmds (valOf cmdsFromIsa) procList

					      val parentID = Posix.ProcEnv.getppid()

          					 val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")

					      val newProcList' =checkChildren (newProcList, toParentStr) 

					      val _ = warning("off to keep watching...")

					     val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")

					    in

					      (*Posix.Process.sleep (Time.fromSeconds 1);*)

					      loop (newProcList') 

					    end

					    )

					else                         (*********************************)

								     (* Execute remotely              *)

								     (* (actually not remote for now )*)

					    (                        (*********************************)

					    let 

					      val newProcList = execCmds (valOf cmdsFromIsa) procList

					      val parentID = Posix.ProcEnv.getppid()

					      val newProcList' =checkChildren (newProcList, toParentStr) 

					    in

					      (*Posix.Process.sleep (Time.fromSeconds 1);*)

					      loop (newProcList') 

					    end

					    )

					)

				     )                                              (******************************)

			      else                                                  (* No new input from Isabelle *)

										    (******************************)

				  (    let val newProcList = checkChildren ((procList), toParentStr)

				       in

					 (*Posix.Process.sleep (Time.fromSeconds 1);*)

					(File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");

					 loop (newProcList)

				       end

				   )

			    end)

		    in  

			loop (procList)

		    end

		in

		 (***************************)

		 (*** Sort out pipes ********)

		 (***************************)

		  Posix.IO.close (#outfd p1);

		  Posix.IO.close (#infd p2);

		  Posix.IO.dup2{old = oldchildin, new = fromParent};

		  Posix.IO.close oldchildin;

		  Posix.IO.dup2{old = oldchildout, new = toParent};

		  Posix.IO.close oldchildout;

		  (***************************)

		  (* start the watcher loop  *)

		  (***************************)

		  keepWatching (toParentStr, fromParentStr, procList);

		  (****************************************************************************)

		  (* fake return value - actually want the watcher to loop until killed       *)

		  (****************************************************************************)

		  Posix.Process.wordToPid 0w0

		end);

	  (* end case *)

    val _ = TextIO.flushOut TextIO.stdOut

    (*******************************)

    (***  set watcher going ********)

    (*******************************)

    val procList = []

    val pid = startWatcher (procList)

    (**************************************************)

    (* communication streams to watcher               *)

    (**************************************************)

    val instr = openInFD ("_exec_in", #infd p2)

    val outstr = openOutFD ("_exec_out", #outfd p1)

    in

     (*******************************)

     (* close the child-side fds    *)

     (*******************************)

      Posix.IO.close (#outfd p2);

      Posix.IO.close (#infd p1);

      (* set the fds close on exec *)

      Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);

      Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);

     (*******************************)

     (* return value                *)

     (*******************************)

      PROC{pid = pid,

	instr = instr,

	outstr = outstr

      }

   end;

(**********************************************************)

(* Start a watcher and set up signal handlers             *)

(**********************************************************)

fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);

fun reapWatcher(pid, instr, outstr) =

        let

		val u = TextIO.closeIn instr;

	        val u = TextIO.closeOut outstr;

		val (_, status) =

			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])

	in

		status

	end

fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))

			   val streams =snd mychild

                           val childin = fst streams

                           val childout = snd streams

                           val childpid = fst mychild

                           val sign = sign_of_thm thm

                           val prems = prems_of thm

                           val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 

                           val _ = (warning ("subgoals forked to createWatcher: "^prems_string));

                           fun vampire_proofHandler (n) =

                           (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));

                           getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               

fun spass_proofHandler (n) = (

                                 let  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));

                                      val _ = TextIO.output (outfile, ("In signal handler now\n"))

                                      val _ =  TextIO.closeOut outfile

                                      val (reconstr, thmstring, goalstring) = SpassComm.getSpassInput childin

                                      val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));

                                      val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))

                                      val _ =  TextIO.closeOut outfile

                                      in          (* if a proof has been found and sent back as a reconstruction proof *)

                                                  if ( (substring (reconstr, 0,1))= "[")

                                                  then 

                                                            (

                                                                 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));

                                                                 Recon_Transfer.apply_res_thm reconstr goalstring;

                                                                 Pretty.writeln(Pretty.str  (oct_char "361"));

                                                                 goals_being_watched := ((!goals_being_watched) - 1);

                                                                 if ((!goals_being_watched) = 0)

                                                                 then 

                                                                    (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found")));

                                                                         val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))

                                                                         val _ =  TextIO.closeOut outfile

                                                                     in

                                                                         killWatcher (childpid); reapWatcher (childpid,childin, childout); ()

                                                                     end)

                                                                 else

                                                                    ()

                                                            )

                                                    (* if there's no proof, but a message from Spass *)

                                                    else if ((substring (reconstr, 0,5))= "SPASS")

                                                         then

                                                                 (

                                                                     goals_being_watched := (!goals_being_watched) -1;

                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));

                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));

                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));

                                                                      if (!goals_being_watched = 0)

                                                                      then 

                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));

                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))

                                                                               val _ =  TextIO.closeOut outfile

                                                                           in

                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()

                                                                           end )

                                                                      else

                                                                         ()

                                                                ) 

						   (* print out a list of rules used from clasimpset*)

                                                    else if ((substring (reconstr, 0,5))= "Rules")

                                                         then

                                                                 (

                                                                     goals_being_watched := (!goals_being_watched) -1;

                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));

                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));

                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));

                                                                      if (!goals_being_watched = 0)

                                                                      then 

                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));

                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))

                                                                               val _ =  TextIO.closeOut outfile

                                                                           in

                                                                              killWatcher (childpid);  reapWatcher (childpid,childin, childout);()

                                                                           end )

                                                                      else

                                                                         ()

                                                                )

                                                          (* if proof translation failed *)

                                                          else if ((substring (reconstr, 0,5)) = "Proof")

                                                               then 

                                                                   (

                                                                     goals_being_watched := (!goals_being_watched) -1;

                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));

                                                                      Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));

                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));

                                                                      if (!goals_being_watched = 0)

                                                                      then 

                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));

                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))

                                                                               val _ =  TextIO.closeOut outfile

                                                                           in

                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()

                                                                           end )

                                                                      else

                                                                         ()

                                                                )

                                                                else  (* add something here ?*)

                                                                   ()

                                       end)

                       in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);

                          IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);

                          (childin, childout, childpid)

  end

end (* structure Watcher *)