src/HOL/Tools/watcher.ML

filtering out some package theorems

(*  Title:      HOL/Tools/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.                                           *)

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) list -> unit

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

(* Start a watcher and set up signal handlers*)
val createWatcher : 
	Proof.context * thm * string Vector.vector list ->
	TextIO.instream * TextIO.outstream * Posix.Process.pid
val killWatcher : Posix.Process.pid -> unit
val killChild  : ('a, 'b) Unix.proc -> OS.Process.status
val command_sep : char
val setting_sep : char
val reapAll : unit -> unit
end



structure Watcher: WATCHER =
struct

(*Field separators, used to pack items onto a text line*)
val command_sep = #"\t"
and setting_sep = #"%";

val goals_being_watched = ref 0;

val trace_path = Path.basic "watcher_trace";

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

(*Representation of a watcher process*)
type proc = {pid : Posix.Process.pid,
             instr : TextIO.instream,
             outstr : TextIO.outstream};

(*Representation of a child (ATP) process*)
type cmdproc = {
        prover: string,       (* Name of the resolution prover used, e.g. "spass"*)
        file:  string,        (* The file containing the goal for the ATP to prove *)
        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
        instr : TextIO.instream,     (*Output of the child process *)
        outstr : TextIO.outstream};  (*Input to the child process *)


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


(*  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*)
fun callResProvers (toWatcherStr,  []) =
      (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
  | callResProvers (toWatcherStr,
                    (prover,proverCmd,settings,probfile)  ::  args) =
      (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile]));
       (*Uses a special character to separate items sent to watcher*)
       TextIO.output (toWatcherStr,
          space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
       inc goals_being_watched;
       TextIO.flushOut toWatcherStr;
       callResProvers (toWatcherStr,args))


(*Send message to watcher to kill currently running vampires. NOT USED and possibly
  buggy. Note that killWatcher kills the entire process group anyway.*)
fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
                            TextIO.flushOut toWatcherStr)


(* Get commands from Isabelle*)
fun getCmds (toParentStr, fromParentStr, cmdList) =
  let val thisLine = the_default "" (TextIO.inputLine fromParentStr)
  in
     trace("\nGot command from parent: " ^ thisLine);
     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",[],"")])
     else
       let val [prover,proverCmd,settingstr,probfile,_] =
                   String.tokens (fn c => c = command_sep) thisLine
           val settings = String.tokens (fn c => c = setting_sep) settingstr
       in
           trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd ^
                  "\n  problem file: " ^ probfile);
           getCmds (toParentStr, fromParentStr,
                    (prover, proverCmd, settings, probfile)::cmdList)
       end
       handle Bind =>
          (trace "\ngetCmds: command parsing failed!";
           getCmds (toParentStr, fromParentStr, cmdList))
  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

fun pollChild 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


(*************************************)
(*  Set up a Watcher Process         *)
(*************************************)

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

val killChildren = List.app (ignore o killChild o #proc_handle) : cmdproc list -> unit;

fun killWatcher (toParentStr, procList) =
      (trace "\nWatcher timeout: Killing proof processes";
       TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
       TextIO.flushOut toParentStr;
       killChildren procList;
       Posix.Process.exit 0w0);

(* 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 =
  let val numbers = "xxx" :: String.tokens (not o Char.isDigit) s 
  in  valOf (Int.fromString (List.last numbers))  end
  handle Option => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
                    error ("Watcher could not read subgoal nunber! " ^ s));

(*Call ATP.  Settings should be a list of strings  ["-t 300", "-m 100000"],
  which we convert below to ["-t", "300", "-m", "100000"] using String.tokens.
  Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and
  Vampire will reject the switches.*)
fun execCmds [] procList = procList
  | execCmds ((prover,proverCmd,settings,file)::cmds) procList  =
      let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
          val settings' = List.concat (map (String.tokens Char.isSpace) settings)
	  val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  =
	       Unix.execute(proverCmd, settings' @ [file])
	  val (instr, outstr) = Unix.streamsOf childhandle
	  val newProcList = {prover=prover, file=file, proc_handle=childhandle,
			     instr=instr, outstr=outstr} :: procList
	  val _ = trace ("\nFinished at " ^
			 Date.toString(Date.fromTimeLocal(Time.now())))
      in execCmds cmds newProcList end

fun checkChildren (ctxt, th, thm_names_list) toParentStr children =
  let fun check [] = []  (* no children to check *)
	| check (child::children) =
	   let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
	       val _ = trace ("\nprobfile = " ^ file)
	       val i = number_from_filename file  (*subgoal number*)
	       val thm_names = List.nth(thm_names_list, i-1);
	       val ppid = Posix.ProcEnv.getppid()
	   in
	     if pollChild childIn
	     then (* check here for prover label on child*)
	       let val _ = trace ("\nInput available from child: " ^ file)
		   val childDone = (case prover of
		       "vampire" => ResReconstruct.checkVampProofFound
			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
		     | "E" => ResReconstruct.checkEProofFound
			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
		     | "spass" => ResReconstruct.checkSpassProofFound
			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
		     | _ => (trace ("\nBad prover! " ^ prover); true) )
		in
		 if childDone (*ATP has reported back (with success OR failure)*)
		 then (Unix.reap proc_handle;
		       if !Output.debugging then () else OS.FileSys.remove file;
		       check children)
		 else child :: check children
	      end
	    else (trace "\nNo child output";  child :: check children)
	   end
  in
    trace ("\nIn checkChildren, length of queue: " ^  Int.toString(length children));
    check children
  end;


fun setupWatcher (ctxt, th, thm_names_list) =
  let
    val checkc = checkChildren (ctxt, th, thm_names_list)
    val p1 = Posix.IO.pipe()   (*pipes for communication between parent and watcher*)
    val p2 = Posix.IO.pipe()
    (****** 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 pid = Posix.ProcEnv.getpid()
	    val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
		     (*set process group id: allows killing all children*)
	    val () = trace "\nsubgoals forked to startWatcher"
	    val limit = ref 200;  (*don't let watcher run forever*)
	    (*Watcher Loop : Check running ATP processes for output*)
	    fun keepWatching procList =
	      (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^
				"  length(procList) = " ^ Int.toString(length procList));
	       OS.Process.sleep (Time.fromMilliseconds 100);  limit := !limit - 1;
	       if !limit < 0 then killWatcher (toParentStr, procList)
	       else
	       case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of
		  SOME [(_,"Kill children",_,_)] =>
		    (trace "\nReceived Kill command";
		     killChildren procList; keepWatching [])
		| SOME cmds => (*  deal with commands from Isabelle process *)
		      let val _ = trace("\nCommands from parent: " ^
					Int.toString(length cmds))
			  val newProcList' = checkc toParentStr (execCmds cmds procList)
		      in trace "\nCommands executed"; keepWatching newProcList' end
		| NONE => (* No new input from Isabelle *)
		    (trace "\nNothing from parent...";
		     keepWatching(checkc toParentStr procList)))
	     handle exn => (*FIXME: exn handler is too general!*)
	       (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
		keepWatching procList);
	  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;
	    keepWatching (procList)
	  end;

    val _ = TextIO.flushOut TextIO.stdOut
    val pid = startWatcher []
    (* 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]);
    {pid = pid, instr = instr, outstr = outstr}
  end;



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

(*Signal handler to tidy away zombie processes*)
fun reapAll() =
     (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
	  SOME _ => reapAll() | NONE => ())
     handle OS.SysErr _ => ()

(*FIXME: does the main process need something like this?
    IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*)

fun killWatcher pid =
  (goals_being_watched := 0;
   Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
   reapAll());

fun reapWatcher(pid, instr, outstr) = ignore
  (TextIO.closeIn instr; TextIO.closeOut outstr;
   Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
  handle OS.SysErr _ => ()

fun string_of_subgoal th i =
    string_of_cterm (List.nth(cprems_of th, i-1))
    handle Subscript => "Subgoal number out of range!"

fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))

fun read_proof probfile =
  let val p = ResReconstruct.txt_path probfile
      val _ = trace("\nReading proof from file " ^ Path.implode p)
      val msg = File.read p 
      val _ = trace("\nProof:\n" ^ msg)
  in  if !Output.debugging then () else File.rm p;  msg  end;

(*Non-successful outcomes*)
fun report i s = priority ("Subgoal " ^ Int.toString i ^ ": " ^ s);

(*Successful outcome: auto-insertion of commands into the PG buffer. Thanks to D Aspinall!!*)
fun report_success i s sgtx = 
  let val sgline = "Subgoal " ^ string_of_int i ^ ":"
      val outlines = 
	case split_lines s of
	    [] => ["Received bad string: " ^ s]
	  | line::lines => ["  Try this command:", (*Markup.enclose Markup.sendback*) line, ""]
	                   @ lines
  in priority (cat_lines (sgline::sgtx::outlines)) end;
  
fun createWatcher (ctxt, th, thm_names_list) =
 let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
     fun decr_watched() =
	  (goals_being_watched := !goals_being_watched - 1;
	   if !goals_being_watched = 0
	   then
	     (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid));
	      killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
	    else ())
     fun proofHandler _ =
       let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid)
           val outcome  = valOf (TextIO.inputLine childin)
                          handle Option => error "watcher: \"outcome\" line is missing"
	   val probfile = valOf (TextIO.inputLine childin)
                          handle Option => error "watcher: \"probfile\" line is missing"
	   val i = number_from_filename probfile
	   val text = "\n" ^ string_of_subgoal th i
       in
	 Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
		       "\"\nprobfile = " ^ probfile ^
		       "\nGoals being watched: "^  Int.toString (!goals_being_watched)));
	 if String.isPrefix "Invalid" outcome
	 then (report i ("Subgoal is not provable:" ^ text);
	       decr_watched())
	 else if String.isPrefix "Failure" outcome
	 then (report i ("Proof attempt failed:" ^ text);
	       decr_watched())
	(* print out a list of rules used from clasimpset*)
	 else if String.isPrefix "Success" outcome
	 then (report_success i (read_proof probfile) text;
	       decr_watched())
	  (* if proof translation failed *)
	 else if String.isPrefix "Translation failed" outcome
	 then (report i (outcome ^ text);
	       decr_watched())
	 else (report i "System error in proof handler";
	       decr_watched())
       end
 in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));
    IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
    (childin, childout, childpid)
  end

end (* structure Watcher *)