src/HOL/Tools/ATP/watcher.ML

removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements

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

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";


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

fun separateFields str =
  let val _ = File.append (File.tmp_path (Path.basic "sep_field"))
                          ("In separateFields, str is: " ^ str ^ "\n\n") 
      val [prover,goalstring,proverCmd,settingstr,probfile] = 
          String.tokens (fn c => c = #"$") str
      val settings = String.tokens (fn c => c = #"%") settingstr
      val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
                  ("Sep comms are: "^ str ^"**"^
                   prover^" goalstr:  "^goalstring^
                   "\n provercmd: "^proverCmd^
                   "\n prob  "^probfile^"\n\n")
  in
     (prover,goalstring, proverCmd, settings, probfile)
  end

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

fun getCmd cmdStr = 
  let val cmdStr' = remove_newlines cmdStr
  in
      File.write (File.tmp_path (Path.basic"sepfields_call")) 
		 ("about to call separateFields with " ^ cmdStr');
      separateFields cmdStr'
  end;
                      
(**************************************************************)
(* Get commands from Isabelle                                 *)
(**************************************************************)

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" 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 
	       (*********************************************************)
	       (* thisCmd = (prover,proverCmd, settings, file)*)
	       (* i.e. put back into tuple format                       *)
	       (*********************************************************)
	   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

fun prems_string_of th =
  Meson.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 =>
       let val pd' = OS.IO.pollIn pd
	   val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
       in
	  if null pdl 
	  then NONE
	  else if OS.IO.isIn (hd pdl)
	       then SOME (getCmds (toParentStr, fromParentStr, []))
	       else NONE
       end
   | 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
      [] => (File.append (File.tmp_path trace_path) 
		    "\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 = 
	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
			 ("\nIn child_poll")
	       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)) 
		   in
		      if null pdl 
		      then
			(File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl\n"; 
			 NONE)
		      else if OS.IO.isIn (hd pdl)
		      then
			   let val inval = TextIO.inputLine fromStr
			       val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
			   in SOME inval end
		      else
                        (File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl \n";
                         NONE)
		   end
		 else NONE
		 end
	     else NONE
	   end

	(* Check all ATP processes currently running for output                 *)
						   (*********************************)
	 fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
						   (*********************************)
	 |   checkChildren ((childProc::otherChildren), toParentStr) = 
	       let val _ = File.append (File.tmp_path trace_path) 
			      ("\nIn check child, length of queue:"^
			        Int.toString (length (childProc::otherChildren)))
		   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 trace_path) 
			      ("\nchildCmd = " ^ childCmd)
		   val sg_num = number_from_filename childCmd
		   val childIncoming = pollChildInput childInput
		   val _ = File.append (File.tmp_path trace_path) 
			         "\nfinished polling child"
		   val parentID = Posix.ProcEnv.getppid()
		   val prover = cmdProver childProc
		   val prems_string = prems_string_of thm
		   val goalstring = cmdGoal childProc							
		   val _ =  File.append (File.tmp_path trace_path) 
		             ("\nsubgoals forked to checkChildren: " ^ goalstring)
	       in 
		 if isSome childIncoming
		 then 
		   (* check here for prover label on child*)
		   let val _ = File.append (File.tmp_path trace_path) 
			        ("\nInput available from childIncoming" ^
			         "\nchecking if proof found." ^
			         "\nchildCmd is " ^ 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;
			 checkChildren(otherChildren, toParentStr))
		     else 
			(**********************************************)
			(* Keep this child and go on to check others  *)
			(**********************************************)
		       (childProc::(checkChildren (otherChildren, toParentStr)))
		  end
		else
		  (File.append (File.tmp_path trace_path)
		               "\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 _ = File.write (File.tmp_path (Path.basic "exec_child"))  
	                    (space_implode "\n" 
	                      (["About 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 _ = File.append (File.tmp_path (Path.basic "exec_child")) 
			    ("\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 _ = File.append (File.tmp_path trace_path) 
			       ("\nCalling pollParentInput: " ^ 
			        Int.toString (!iterations_left));
		    val cmdsFromIsa = pollParentInput 
		                       (fromParentIOD, fromParentStr, toParentStr)
		in 
		   iterations_left := !iterations_left - 1;
		   if !iterations_left <= 0 
		   then (*Sadly, this code fails to terminate the watcher!*)
		    (File.append (File.tmp_path trace_path) 
			         "\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 _ = File.append (File.tmp_path trace_path)
			      "\nJust execed a child"
			   val newProcList' = checkChildren (newProcList, toParentStr) 
			 in
			   File.append (File.tmp_path trace_path) 
			       ("\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
		       File.append (File.tmp_path trace_path) 
			       ("\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 
	     (File.append (File.tmp_path (Path.basic "reap_found"))
	       ("Reaping a watcher, childpid = "^
		LargeWord.toString (Posix.Process.pidToWord childpid)^"\n");
	      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 (tracing (Recon_Transfer.apply_res_thm outcome goalstring);
	       decr_watched())
	 else if String.isPrefix "Invalid" outcome
	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "is not provable");
	       decr_watched())
	 else if String.isPrefix "Failure" outcome
	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "proof attempt failed");
	       decr_watched()) 
	(* print out a list of rules used from clasimpset*)
	 else if String.isPrefix "Success" outcome
	 then (tracing (goalstring^outcome);
	       decr_watched())
	  (* if proof translation failed *)
	 else if String.isPrefix "Translation failed" outcome
	 then (tracing (goalstring ^ Recon_Transfer.restore_linebreaks outcome);
	       decr_watched())
	 else  
	      (tracing "System error in proof handler";
	       decr_watched())
       end
 in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
    (childin, childout, childpid)
  end

end (* structure Watcher *)