(*  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 _ = File.write (File.tmp_path (Path.basic "tog_comms"))

                              (prover^thmstring^goalstring^proverCmd^settings^

                               clasimpfile^hypsfile^probfile)

       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 _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                

                   ("Sep comms are: "^(implode str)^"**"^

                    prover^thmstring^goalstring^proverCmd^clasimpfile^hypsfile^file^"\n\n")

   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

     (*** 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_dir = File.tmp_path (Path.basic "dfg"); 

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

     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 tptp2X = getenv "TPTP2X_HOME" ^ "/tptp2X"

     val _ = if File.exists (File.unpack_platform_path tptp2X) then () 

 	    else error ("Could not find the file " ^ tptp2X)

     val bar = (fn s => (File.write (File.tmp_path (Path.basic "tptp2X-call")) s; system s)) 

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

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

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

 			(thmstring ^ "\n goals_watched" ^

 			string_of_int(!goals_being_watched) ^ newfile ^ "\n")

   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 _ = File.append (File.tmp_path (Path.basic"cmdStr")) cmdStr

        in

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

 	   then 

 	       let val newCmdStr = (rev(tl backList))

 	       in  File.write (File.tmp_path (Path.basic"backlist")) 

 	                      ("about to call sepfields with "^(implode newCmdStr));

 		   formatCmd (separateFields newCmdStr)

 	       end

 	   else formatCmd (separateFields (explode cmdStr))

        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 _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine

   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 *)