# File watcher.ML

    (*  Title:      Watcher.ML
        ID:         $Id: watcher.ML,v 1.49 2005/09/29 10:44:25 paulson Exp $
        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    *)
    (***************************************************************************)

    signature WATCHER =
    sig

    (*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
    (* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)

    val callResProvers :
        TextIO.outstream * (string*string*string*string*string) list
        -> unit

    (* Send message to watcher to kill currently running resolution provers *)
    val callSlayer : TextIO.outstream -> unit

    (* Start a watcher and set up signal handlers             *)
    val createWatcher :
        thm * (ResClause.clause * thm) Array.array ->
        TextIO.instream * TextIO.outstream * Posix.Process.pid

    (* Kill watcher process                                   *)
    val killWatcher : Posix.Process.pid -> unit
    val killWatcher' : int -> unit
    end

    structure Watcher: WATCHER =
    struct

    open Recon_Transfer

    val goals_being_watched = ref 0;

    val trace_path = Path.basic "watcher_trace";

    fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s
                  else ();

    (*  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*)
            cmd:  string,         (* The file containing the goal for res prover to prove *)
            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 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,proc_handle,goalstring,instr,outstr}) =
      (prover,(cmd, (instr,outstr)));

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

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

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

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

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

    fun callResProver (toWatcherStr,  arg) =
          (TextIO.output (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*)
    (*****************************************************************************************)

    (*Uses the $-character to separate items sent to watcher*)
    fun callResProvers (toWatcherStr,  []) =
          (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
    |   callResProvers (toWatcherStr,
                        (prover,goalstring, proverCmd,settings,
                         probfile)  ::  args) =
          let val _ = trace (space_implode "\n"
    		         (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
    			  probfile]))
          in TextIO.output (toWatcherStr,
                (prover^"$"^goalstring^"$"^proverCmd^"$"^
                 settings^"$"^probfile^"\n"));
             goals_being_watched := (!goals_being_watched) + 1;
    	 TextIO.flushOut toWatcherStr;
    	 callResProvers (toWatcherStr,args)
          end

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

    fun callSlayer toWatcherStr = (TextIO.output (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     *)
    (**************************************************************)

    val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);

    fun getCmd cmdStr =
      let val [prover,goalstring,proverCmd,settingstr,probfile] =
                String.tokens (fn c => c = #"$") (remove_newlines cmdStr)
          val settings = String.tokens (fn c => c = #"%") settingstr
          val _ = trace ("getCmd: " ^ cmdStr ^
    		    "\nprover" ^ prover ^ " goalstr:  "^goalstring^
    		    "\nprovercmd: " ^ proverCmd^
    		    "\nprob  " ^ probfile ^ "\n\n")
      in (prover,goalstring, proverCmd, settings, probfile) end

    (**************************************************************)
    (* Get commands from Isabelle                                 *)
    (**************************************************************)
    fun getCmds (toParentStr,fromParentStr, cmdList) =
      let val thisLine = TextIO.inputLine fromParentStr
          val _ = trace("\nGot command from parent: " ^ thisLine)
      in
         if thisLine = "End of calls\n" orelse thisLine = "" 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
    	   in 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 getProofCmd (a,c,d,e,f) = d

    (* for tracing: encloses each string element in brackets. *)
    val concat_with_and = space_implode " & " o map (enclose "(" ")");

    fun prems_string_of th =
      concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))

    fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);

    fun killChildren procs = List.app (ignore o killChild) procs;

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

     fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) =
       case OS.IO.pollDesc fromParentIOD of
          SOME pd =>
    	 (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
    	      [] => NONE
    	    | pd''::_ => if OS.IO.isIn pd''
    	 	         then SOME (getCmds (toParentStr, fromParentStr, []))
    	 	         else NONE)
       | NONE => NONE;

    (*get the number of the subgoal from the filename: the last digit string*)
    fun number_from_filename s =
      case String.tokens (not o Char.isDigit) s of
          [] => (trace "\nWatcher could not read subgoal nunber!!"; raise ERROR)
        | numbers => valOf (Int.fromString (List.last numbers));

    fun setupWatcher (thm,clause_arr) =
      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 _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);

    	  fun pollChildInput fromStr =
    	     case getInIoDesc fromStr of
    	       SOME iod =>
    		 (case OS.IO.pollDesc iod of
    		    SOME pd =>
    			let val pd' = OS.IO.pollIn pd
    			in
    			  case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
    			      [] => false
    			    | pd''::_ => OS.IO.isIn pd''
    			end
    		   | NONE => false)
    	     | NONE => false

    	  (* Check all ATP processes currently running for output                 *)
    	  fun checkChildren ([], toParentStr) = []  (* no children to check *)
    	  |   checkChildren (childProc::otherChildren, toParentStr) =
    	       let val _ = trace ("\nIn check child, length of queue:"^
    			          Int.toString (length (childProc::otherChildren)))
    		   val (childInput,childOutput) = cmdstreamsOf childProc
    		   val child_handle = cmdchildHandle childProc
    		   (* childCmd is the file that the problem is in *)
    		   val childCmd = fst(snd (cmdchildInfo childProc))
    		   val _ = trace ("\nchildCmd = " ^ childCmd)
    		   val sg_num = number_from_filename childCmd
    		   val childIncoming = pollChildInput childInput
    		   val parentID = Posix.ProcEnv.getppid()
    		   val prover = cmdProver childProc
    		   val prems_string = prems_string_of thm
    		   val goalstring = cmdGoal childProc
    	       in
    		 trace("\nsubgoals forked to checkChildren: " ^ goalstring);
    		 if childIncoming
    		 then
    		   (* check here for prover label on child*)
    		   let val _ = trace ("\nInput available from child: " ^
    				      childCmd ^
    				      "\ngoalstring is " ^ goalstring ^ "\n\n")
    		       val childDone = (case prover of
    			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)
    			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)
    			  |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  )
    		    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;
    			 OS.FileSys.remove childCmd;
    			 checkChildren(otherChildren, toParentStr))
    		     else (* Keep this child and go on to check others  *)
    		       childProc :: checkChildren (otherChildren, toParentStr)
    		  end
    		else (trace "\nNo child output";
    		      childProc::(checkChildren (otherChildren, toParentStr)))
    	       end

         (********************************************************************)
         (* call resolution processes                                        *)
         (* settings should be a list of strings                             *)
         (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
         (* takes list of (string, string, string list, string)list proclist *)
         (********************************************************************)

    (*** add subgoal id num to this *)
    	fun execCmds  [] procList = procList
    	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
    	      let val _ = trace
    	                    (space_implode "\n"
    	                      (["\nAbout to execute command for goal:",
    	                        goalstring, proverCmd] @ settings @
    	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
    	          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,
    				       goalstring = goalstring,
    				       proc_handle = childhandle,
    				       instr = instr,
    				       outstr = outstr }) :: procList

    		  val _ = trace ("\nFinished at " ^
    			         Date.toString(Date.fromTimeLocal(Time.now())))
    	      in execCmds cmds newProcList end

         (****************************************)
         (* call resolution processes remotely   *)
         (* settings should be a list of strings *)
         (* e.g. ["-t300", "-m100000"]         *)
         (****************************************)

          (*  fun execRemoteCmds  [] procList = procList
    	|   execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList  =
    	      let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
    		  in
    		       execRemoteCmds  cmds newProcList
    		  end
    *)

         (**********************************************)
         (* Watcher Loop                               *)
         (**********************************************)
             val iterations_left = ref 500;  (*don't let it run forever*)

    	 fun keepWatching (procList) =
    	   let fun loop procList =
    		let val _ = trace ("\nCalling pollParentInput: " ^
    			           Int.toString (!iterations_left));
    		    val cmdsFromIsa = pollParentInput
    		                       (fromParentIOD, fromParentStr, toParentStr)
    		in
    		   OS.Process.sleep (Time.fromMilliseconds 100);
    		   iterations_left := !iterations_left - 1;
    		   if !iterations_left <= 0
    		   then
    		    (trace "\nTimeout: Killing proof processes";
    	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
    		     TextIO.flushOut toParentStr;
    		     killChildren (map cmdchildHandle procList);
    		     exit 0)
    		   else 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;
    			  loop []
    		       end
    		     else
    		       if length procList < 5     (********************)
    		       then                        (* Execute locally  *)
    			 let
    			   val newProcList = execCmds (valOf cmdsFromIsa) procList
    			   val _ = Posix.ProcEnv.getppid()
    			   val _ = trace "\nJust execed a child"
    			   val newProcList' = checkChildren (newProcList, toParentStr)
    			 in
    			   trace ("\nOff to keep watching: " ^
    			          Int.toString (!iterations_left));
    			   loop newProcList'
    			 end
    		       else  (* Execute remotely              *)
    			     (* (actually not remote for now )*)
    			 let
    			   val newProcList = execCmds (valOf cmdsFromIsa) procList
    			   val _ = Posix.ProcEnv.getppid()
    			   val newProcList' =checkChildren (newProcList, toParentStr)
    			 in
    			   loop newProcList'
    			 end
    		   else (* No new input from Isabelle *)
    		     let val newProcList = checkChildren (procList, toParentStr)
    		     in
    		       trace ("\nNo new input, still watching: " ^
    			      Int.toString (!iterations_left));
    		       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 (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);

    val killWatcher' = killWatcher o ResLib.pidOfInt;

    fun reapWatcher(pid, instr, outstr) =
      (TextIO.closeIn instr; TextIO.closeOut outstr;
       Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())

    fun createWatcher (thm, clause_arr) =
     let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
         fun decr_watched() =
    	  (goals_being_watched := !goals_being_watched - 1;
    	   if !goals_being_watched = 0
    	   then
    	     (debug ("\nReaping a watcher, childpid = "^
    		     LargeWord.toString (Posix.Process.pidToWord childpid));
    	      killWatcher childpid; reapWatcher (childpid,childin, childout))
    	    else ())
         val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
         fun proofHandler n =
           let val outcome = TextIO.inputLine childin
    	   val goalstring = TextIO.inputLine childin
    	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^
    		        "\"\ngoalstring = " ^ goalstring ^
    		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
           in
    	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
    	 then (priority (Recon_Transfer.apply_res_thm outcome goalstring);
    	       decr_watched())
    	 else if String.isPrefix "Invalid" outcome
    	 then (priority (goalstring ^ "is not provable");
    	       decr_watched())
    	 else if String.isPrefix "Failure" outcome
    	 then (priority (goalstring ^ "proof attempt failed");
    	       decr_watched())
    	(* print out a list of rules used from clasimpset*)
    	 else if String.isPrefix "Success" outcome
    	 then (priority (goalstring^outcome);
    	       decr_watched())
    	  (* if proof translation failed *)
    	 else if String.isPrefix "Translation failed" outcome
    	 then (priority (goalstring ^ outcome);
    	       decr_watched())
    	 else (priority "System error in proof handler";
    	       decr_watched())
           end
     in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
        (childin, childout, childpid)
      end

    end (* structure Watcher *)