src/HOL/Tools/ATP/watcher.ML
author paulson
Thu Sep 29 12:44:25 2005 +0200 (2005-09-29)
changeset 17716 89932e53f31d
parent 17690 8ba7c3cd24a8
child 17746 af59c748371d
permissions -rw-r--r--
moved concat_with_and to watcher.ML
paulson@15789
     1
(*  Title:      Watcher.ML
paulson@15789
     2
    ID:         $Id$
paulson@15789
     3
    Author:     Claire Quigley
paulson@15789
     4
    Copyright   2004  University of Cambridge
quigley@15642
     5
 *)
quigley@15642
     6
quigley@15642
     7
 (***************************************************************************)
quigley@15642
     8
 (*  The watcher process starts a resolution process when it receives a     *)
quigley@15642
     9
(*  message from Isabelle                                                  *)
quigley@15642
    10
(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
quigley@15642
    11
(*  and removes dead processes.  Also possible to kill all the resolution  *)
quigley@15642
    12
(*  processes currently running.                                           *)
quigley@15642
    13
(*  Hardwired version of where to pick up the tptp files for the moment    *)
quigley@15642
    14
(***************************************************************************)
quigley@15642
    15
paulson@17305
    16
signature WATCHER =
paulson@17305
    17
sig
paulson@17305
    18
paulson@17305
    19
(*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
paulson@17568
    20
(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
paulson@17305
    21
paulson@17305
    22
val callResProvers :
paulson@17422
    23
    TextIO.outstream * (string*string*string*string*string) list 
paulson@17305
    24
    -> unit
paulson@17305
    25
paulson@17305
    26
(* Send message to watcher to kill currently running resolution provers *)
paulson@17305
    27
val callSlayer : TextIO.outstream -> unit
paulson@17305
    28
paulson@17305
    29
(* Start a watcher and set up signal handlers             *)
paulson@17484
    30
val createWatcher : 
paulson@17484
    31
    thm * (ResClause.clause * thm) Array.array -> 
paulson@17484
    32
    TextIO.instream * TextIO.outstream * Posix.Process.pid
paulson@17305
    33
paulson@17305
    34
(* Kill watcher process                                   *)
paulson@17305
    35
val killWatcher : Posix.Process.pid -> unit
paulson@17488
    36
val killWatcher' : int -> unit
paulson@17305
    37
end
paulson@17305
    38
paulson@17305
    39
quigley@15642
    40
quigley@15642
    41
structure Watcher: WATCHER =
paulson@17484
    42
struct
quigley@15642
    43
paulson@17488
    44
open Recon_Transfer
wenzelm@16805
    45
quigley@15642
    46
val goals_being_watched = ref 0;
quigley@15642
    47
paulson@17583
    48
val trace_path = Path.basic "watcher_trace";
paulson@17583
    49
paulson@17690
    50
fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
paulson@17690
    51
              else ();
paulson@17583
    52
quigley@16039
    53
(*  The result of calling createWatcher  *)
quigley@16039
    54
datatype proc = PROC of {
quigley@16039
    55
        pid : Posix.Process.pid,
quigley@16039
    56
        instr : TextIO.instream,
quigley@16039
    57
        outstr : TextIO.outstream
quigley@16039
    58
      };
quigley@16039
    59
quigley@16039
    60
(*  The result of calling executeToList  *)
quigley@16039
    61
datatype cmdproc = CMDPROC of {
paulson@17568
    62
        prover: string,       (* Name of the resolution prover used, e.g. Vampire*)
paulson@17568
    63
        cmd:  string,         (* The file containing the goal for res prover to prove *)     
paulson@17568
    64
        goalstring: string,   (* string representation of subgoal*) 
quigley@16039
    65
        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
quigley@16039
    66
        instr : TextIO.instream,   (*  Input stream to child process *)
paulson@17568
    67
        outstr : TextIO.outstream};  (*  Output stream from child process *)
quigley@16039
    68
quigley@16039
    69
type signal = Posix.Signal.signal
quigley@16039
    70
datatype exit_status = datatype Posix.Process.exit_status
quigley@16039
    71
quigley@16039
    72
val fromStatus = Posix.Process.fromStatus
quigley@16039
    73
quigley@16039
    74
fun reap(pid, instr, outstr) =
paulson@17317
    75
  let val u = TextIO.closeIn instr;
paulson@17317
    76
      val u = TextIO.closeOut outstr;
paulson@17317
    77
      val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
paulson@17568
    78
  in status end
quigley@16039
    79
quigley@16039
    80
fun fdReader (name : string, fd : Posix.IO.file_desc) =
quigley@16039
    81
	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
quigley@16039
    82
quigley@16039
    83
fun fdWriter (name, fd) =
quigley@16039
    84
          Posix.IO.mkTextWriter {
quigley@16039
    85
	      appendMode = false,
quigley@16039
    86
              initBlkMode = true,
quigley@16039
    87
              name = name,  
quigley@16039
    88
              chunkSize=4096,
paulson@17317
    89
              fd = fd};
quigley@16039
    90
quigley@16039
    91
fun openOutFD (name, fd) =
quigley@16039
    92
	  TextIO.mkOutstream (
quigley@16039
    93
	    TextIO.StreamIO.mkOutstream (
quigley@16039
    94
	      fdWriter (name, fd), IO.BLOCK_BUF));
quigley@16039
    95
quigley@16039
    96
fun openInFD (name, fd) =
quigley@16039
    97
	  TextIO.mkInstream (
quigley@16039
    98
	    TextIO.StreamIO.mkInstream (
quigley@16039
    99
	      fdReader (name, fd), ""));
quigley@16039
   100
quigley@16039
   101
fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
quigley@16039
   102
quigley@16039
   103
fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
quigley@16039
   104
paulson@17317
   105
fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
quigley@16039
   106
paulson@17422
   107
fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) = 
paulson@17317
   108
  (prover,(cmd, (instr,outstr)));
quigley@16039
   109
paulson@17422
   110
fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  = 
paulson@17317
   111
  proc_handle;
quigley@16039
   112
paulson@17422
   113
fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
paulson@17317
   114
  prover;
quigley@15642
   115
paulson@17422
   116
fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
paulson@17317
   117
  goalstring;
paulson@17317
   118
quigley@15642
   119
quigley@15642
   120
(*    gets individual args from instream and concatenates them into a list      *)
paulson@17317
   121
fun getArgs (fromParentStr, toParentStr, ys) =  
paulson@17317
   122
  let val thisLine = TextIO.input fromParentStr
paulson@17317
   123
  in ys@[thisLine] end
quigley@15642
   124
quigley@15642
   125
                            
quigley@15642
   126
(*  Send request to Watcher for a vampire to be called for filename in arg      *)
paulson@17568
   127
                   
paulson@17231
   128
fun callResProver (toWatcherStr,  arg) = 
paulson@17317
   129
      (TextIO.output (toWatcherStr, arg^"\n"); 
paulson@17231
   130
       TextIO.flushOut toWatcherStr)
quigley@15642
   131
quigley@15642
   132
(*****************************************************************************************)
quigley@16357
   133
(*  Send request to Watcher for multiple provers to be called for filenames in arg       *)
quigley@16357
   134
(*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
quigley@15642
   135
(*****************************************************************************************)
quigley@15642
   136
quigley@16357
   137
    
paulson@17305
   138
(*Uses the $-character to separate items sent to watcher*)
paulson@16475
   139
fun callResProvers (toWatcherStr,  []) = 
paulson@17317
   140
      (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
paulson@16475
   141
|   callResProvers (toWatcherStr,
paulson@17422
   142
                    (prover,goalstring, proverCmd,settings, 
paulson@17422
   143
                     probfile)  ::  args) =
paulson@17690
   144
      let val _ = trace (space_implode "\n" 
paulson@17690
   145
		         (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
paulson@17690
   146
			  probfile]))
paulson@17317
   147
      in TextIO.output (toWatcherStr,    
paulson@17422
   148
            (prover^"$"^goalstring^"$"^proverCmd^"$"^
paulson@17422
   149
             settings^"$"^probfile^"\n"));
paulson@16475
   150
         goals_being_watched := (!goals_being_watched) + 1;
paulson@16475
   151
	 TextIO.flushOut toWatcherStr;
paulson@16475
   152
	 callResProvers (toWatcherStr,args)
paulson@16475
   153
      end   
quigley@16357
   154
                                                
paulson@17305
   155
                                    
quigley@15642
   156
 
quigley@15642
   157
(**************************************************************)
quigley@15642
   158
(* Send message to watcher to kill currently running vampires *)
quigley@15642
   159
(**************************************************************)
quigley@15642
   160
paulson@17317
   161
fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n"); 
quigley@15642
   162
                            TextIO.flushOut toWatcherStr)
quigley@15642
   163
quigley@15642
   164
quigley@15642
   165
(**************************************************************)
quigley@15642
   166
(* Remove \n token from a vampire goal filename and extract   *)
quigley@15642
   167
(* prover, proverCmd, settings and file from input string     *)
quigley@15642
   168
(**************************************************************)
quigley@15642
   169
paulson@17305
   170
val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
quigley@15642
   171
paulson@17305
   172
fun getCmd cmdStr = 
paulson@17690
   173
  let val [prover,goalstring,proverCmd,settingstr,probfile] = 
paulson@17690
   174
            String.tokens (fn c => c = #"$") (remove_newlines cmdStr)
paulson@17690
   175
      val settings = String.tokens (fn c => c = #"%") settingstr
paulson@17690
   176
      val _ = trace ("getCmd: " ^ cmdStr ^
paulson@17690
   177
		    "\nprover" ^ prover ^ " goalstr:  "^goalstring^
paulson@17690
   178
		    "\nprovercmd: " ^ proverCmd^
paulson@17690
   179
		    "\nprob  " ^ probfile ^ "\n\n")
paulson@17690
   180
  in (prover,goalstring, proverCmd, settings, probfile) end
quigley@15642
   181
                      
quigley@15642
   182
(**************************************************************)
quigley@15642
   183
(* Get commands from Isabelle                                 *)
quigley@15642
   184
(**************************************************************)
quigley@15642
   185
fun getCmds (toParentStr,fromParentStr, cmdList) = 
paulson@16475
   186
  let val thisLine = TextIO.inputLine fromParentStr 
paulson@17690
   187
      val _ = trace("\nGot command from parent: " ^ thisLine)
paulson@16475
   188
  in
paulson@17568
   189
     if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
paulson@17422
   190
     else if thisLine = "Kill children\n"
paulson@17568
   191
     then (TextIO.output (toParentStr,thisLine ); 
paulson@17568
   192
	   TextIO.flushOut toParentStr;
paulson@17568
   193
	   (("","","Kill children",[],"")::cmdList)  )
paulson@17422
   194
     else let val thisCmd = getCmd thisLine 
paulson@17690
   195
	   in getCmds (toParentStr, fromParentStr, thisCmd::cmdList) end
paulson@16475
   196
  end
paulson@16475
   197
	    
quigley@16357
   198
                                                                  
quigley@15642
   199
(**************************************************************)
quigley@15642
   200
(*  Get Io-descriptor for polling of an input stream          *)
quigley@15642
   201
(**************************************************************)
quigley@15642
   202
quigley@15642
   203
fun getInIoDesc someInstr = 
quigley@15642
   204
    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
paulson@15702
   205
        val _ = TextIO.output (TextIO.stdOut, buf)
quigley@15642
   206
        val ioDesc = 
quigley@15642
   207
	    case rd
quigley@15642
   208
	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
quigley@15642
   209
	       | _ => NONE
quigley@15642
   210
     in (* since getting the reader will have terminated the stream, we need
quigley@15642
   211
	 * to build a new stream. *)
quigley@15642
   212
	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
quigley@15642
   213
	ioDesc
quigley@15642
   214
    end
quigley@15642
   215
quigley@15642
   216
quigley@15642
   217
(*************************************)
quigley@15642
   218
(*  Set up a Watcher Process         *)
quigley@15642
   219
(*************************************)
quigley@15642
   220
paulson@17422
   221
fun getProofCmd (a,c,d,e,f) = d
paulson@17422
   222
paulson@17716
   223
(* for tracing: encloses each string element in brackets. *)
paulson@17716
   224
val concat_with_and = space_implode " & " o map (enclose "(" ")");
paulson@17716
   225
paulson@17484
   226
fun prems_string_of th =
paulson@17716
   227
  concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
paulson@17484
   228
paulson@17525
   229
fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
paulson@17525
   230
paulson@17525
   231
fun killChildren procs = List.app (ignore o killChild) procs;
paulson@17502
   232
paulson@17568
   233
 (*************************************************************)
paulson@17568
   234
 (* take an instream and poll its underlying reader for input *)
paulson@17568
   235
 (*************************************************************)
paulson@17568
   236
 
paulson@17568
   237
 fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = 
paulson@17690
   238
   case OS.IO.pollDesc fromParentIOD of
paulson@17690
   239
      SOME pd =>
paulson@17690
   240
	 (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
paulson@17690
   241
	      [] => NONE
paulson@17690
   242
	    | pd''::_ => if OS.IO.isIn pd''
paulson@17690
   243
	 	         then SOME (getCmds (toParentStr, fromParentStr, []))
paulson@17690
   244
	 	         else NONE)
paulson@17568
   245
   | NONE => NONE;
paulson@17568
   246
paulson@17583
   247
(*get the number of the subgoal from the filename: the last digit string*)
paulson@17583
   248
fun number_from_filename s =
paulson@17583
   249
  case String.tokens (not o Char.isDigit) s of
paulson@17690
   250
      [] => (trace "\nWatcher could not read subgoal nunber!!"; raise ERROR)
paulson@17583
   251
    | numbers => valOf (Int.fromString (List.last numbers));
paulson@17583
   252
paulson@17484
   253
fun setupWatcher (thm,clause_arr) = 
paulson@16061
   254
  let
paulson@16061
   255
    (** pipes for communication between parent and watcher **)
paulson@16061
   256
    val p1 = Posix.IO.pipe ()
paulson@16061
   257
    val p2 = Posix.IO.pipe ()
paulson@17317
   258
    fun closep () = 
paulson@17317
   259
	 (Posix.IO.close (#outfd p1); 
paulson@16061
   260
	  Posix.IO.close (#infd p1);
paulson@16061
   261
	  Posix.IO.close (#outfd p2); 
paulson@17317
   262
	  Posix.IO.close (#infd p2))
paulson@16061
   263
    (***********************************************************)
paulson@16061
   264
    (****** fork a watcher process and get it set up and going *)
paulson@16061
   265
    (***********************************************************)
paulson@17317
   266
    fun startWatcher procList =
paulson@17234
   267
     (case  Posix.Process.fork() (***************************************)
paulson@17234
   268
      of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
paulson@17234
   269
				    (***************************************)
paulson@16061
   270
paulson@17234
   271
				      (*************************)
paulson@17234
   272
       | NONE => let                  (* child - i.e. watcher  *)
paulson@17690
   273
	  val oldchildin = #infd p1   (*************************)
paulson@17690
   274
	  val fromParent = Posix.FileSys.wordToFD 0w0
paulson@17690
   275
	  val oldchildout = #outfd p2
paulson@17690
   276
	  val toParent = Posix.FileSys.wordToFD 0w1
paulson@17690
   277
	  val fromParentIOD = Posix.FileSys.fdToIOD fromParent
paulson@17690
   278
	  val fromParentStr = openInFD ("_exec_in_parent", fromParent)
paulson@17690
   279
	  val toParentStr = openOutFD ("_exec_out_parent", toParent)
paulson@17690
   280
	  val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
paulson@17568
   281
	 
paulson@17317
   282
	  fun pollChildInput fromStr = 
paulson@17690
   283
	     case getInIoDesc fromStr of
paulson@17690
   284
	       SOME iod => 
paulson@17690
   285
		 (case OS.IO.pollDesc iod of
paulson@17690
   286
		    SOME pd =>
paulson@17690
   287
			let val pd' = OS.IO.pollIn pd
paulson@17690
   288
			in
paulson@17690
   289
			  case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
paulson@17690
   290
			      [] => false
paulson@17690
   291
			    | pd''::_ => OS.IO.isIn pd''
paulson@17690
   292
			end
paulson@17690
   293
		   | NONE => false)
paulson@17690
   294
	     | NONE => false
quigley@15642
   295
paulson@17690
   296
paulson@17690
   297
	  (* Check all ATP processes currently running for output                 *)
paulson@17690
   298
	  fun checkChildren ([], toParentStr) = []  (* no children to check *)
paulson@17690
   299
	  |   checkChildren (childProc::otherChildren, toParentStr) = 
paulson@17690
   300
	       let val _ = trace ("\nIn check child, length of queue:"^
paulson@17690
   301
			          Int.toString (length (childProc::otherChildren)))
paulson@17568
   302
		   val (childInput,childOutput) = cmdstreamsOf childProc
paulson@17568
   303
		   val child_handle = cmdchildHandle childProc
paulson@17690
   304
		   (* childCmd is the file that the problem is in *)
paulson@17234
   305
		   val childCmd = fst(snd (cmdchildInfo childProc))
paulson@17690
   306
		   val _ = trace ("\nchildCmd = " ^ childCmd)
paulson@17583
   307
		   val sg_num = number_from_filename childCmd
paulson@17234
   308
		   val childIncoming = pollChildInput childInput
paulson@17234
   309
		   val parentID = Posix.ProcEnv.getppid()
paulson@17234
   310
		   val prover = cmdProver childProc
paulson@17484
   311
		   val prems_string = prems_string_of thm
paulson@17234
   312
		   val goalstring = cmdGoal childProc							
paulson@17234
   313
	       in 
paulson@17690
   314
		 trace("\nsubgoals forked to checkChildren: " ^ goalstring);
paulson@17690
   315
		 if childIncoming
paulson@17234
   316
		 then 
paulson@17306
   317
		   (* check here for prover label on child*)
paulson@17690
   318
		   let val _ = trace ("\nInput available from child: " ^
paulson@17690
   319
				      childCmd ^ 
paulson@17690
   320
				      "\ngoalstring is " ^ goalstring ^ "\n\n")
paulson@17306
   321
		       val childDone = (case prover of
paulson@17488
   322
			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
paulson@17488
   323
			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
paulson@17484
   324
			  |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  )
paulson@17306
   325
		    in
paulson@17484
   326
		     if childDone
paulson@17306
   327
		     then (* child has found a proof and transferred it *)
paulson@17306
   328
			(* Remove this child and go on to check others*)
paulson@17306
   329
			(Unix.reap child_handle;
paulson@17716
   330
			 OS.FileSys.remove childCmd;
paulson@17306
   331
			 checkChildren(otherChildren, toParentStr))
paulson@17690
   332
		     else (* Keep this child and go on to check others  *)
paulson@17690
   333
		       childProc :: checkChildren (otherChildren, toParentStr)
paulson@17306
   334
		  end
paulson@17690
   335
		else (trace "\nNo child output";
paulson@17690
   336
		      childProc::(checkChildren (otherChildren, toParentStr)))
paulson@17234
   337
	       end
quigley@15642
   338
paulson@17234
   339
	
paulson@17234
   340
     (********************************************************************)                  
paulson@17234
   341
     (* call resolution processes                                        *)
paulson@17234
   342
     (* settings should be a list of strings                             *)
paulson@17234
   343
     (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
paulson@17234
   344
     (* takes list of (string, string, string list, string)list proclist *)
paulson@17234
   345
     (********************************************************************)
quigley@15642
   346
quigley@16039
   347
paulson@16061
   348
(*** add subgoal id num to this *)
paulson@17234
   349
	fun execCmds  [] procList = procList
paulson@17422
   350
	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
paulson@17690
   351
	      let val _ = trace 
paulson@17317
   352
	                    (space_implode "\n" 
paulson@17690
   353
	                      (["\nAbout to execute command for goal:",
paulson@17317
   354
	                        goalstring, proverCmd] @ settings @
paulson@17317
   355
	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
paulson@17317
   356
	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
paulson@17234
   357
		       (Unix.execute(proverCmd, (settings@[file])))
paulson@17234
   358
		  val (instr, outstr) = Unix.streamsOf childhandle
paulson@17234
   359
		  val newProcList = (CMDPROC{
paulson@17234
   360
				       prover = prover,
paulson@17234
   361
				       cmd = file,
paulson@17234
   362
				       goalstring = goalstring,
paulson@17234
   363
				       proc_handle = childhandle,
paulson@17234
   364
				       instr = instr,
paulson@17234
   365
				       outstr = outstr }) :: procList
paulson@17234
   366
     
paulson@17690
   367
		  val _ = trace ("\nFinished at " ^
paulson@17690
   368
			         Date.toString(Date.fromTimeLocal(Time.now())))
paulson@17690
   369
	      in execCmds cmds newProcList end
quigley@15642
   370
quigley@16039
   371
paulson@17234
   372
     (****************************************)                  
paulson@17234
   373
     (* call resolution processes remotely   *)
paulson@17234
   374
     (* settings should be a list of strings *)
paulson@17317
   375
     (* e.g. ["-t300", "-m100000"]         *)
paulson@17234
   376
     (****************************************)
paulson@16061
   377
paulson@17234
   378
      (*  fun execRemoteCmds  [] procList = procList
paulson@17422
   379
	|   execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList  =  
paulson@17422
   380
	      let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
paulson@17422
   381
		  in
paulson@17422
   382
		       execRemoteCmds  cmds newProcList
paulson@17422
   383
		  end
quigley@16039
   384
*)
quigley@15642
   385
paulson@17234
   386
     (**********************************************)                  
paulson@17234
   387
     (* Watcher Loop                               *)
paulson@17234
   388
     (**********************************************)
paulson@17583
   389
         val iterations_left = ref 500;  (*don't let it run forever*)
paulson@16061
   390
paulson@17568
   391
	 fun keepWatching (procList) = 
paulson@17317
   392
	   let fun loop procList =  
paulson@17690
   393
		let val _ = trace ("\nCalling pollParentInput: " ^ 
paulson@17690
   394
			           Int.toString (!iterations_left));
paulson@17568
   395
		    val cmdsFromIsa = pollParentInput 
paulson@17568
   396
		                       (fromParentIOD, fromParentStr, toParentStr)
paulson@17234
   397
		in 
paulson@17690
   398
		   OS.Process.sleep (Time.fromMilliseconds 100);
paulson@17306
   399
		   iterations_left := !iterations_left - 1;
paulson@17568
   400
		   if !iterations_left <= 0 
paulson@17690
   401
		   then 
paulson@17690
   402
		    (trace "\nTimeout: Killing proof processes";
paulson@17568
   403
	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
paulson@17502
   404
		     TextIO.flushOut toParentStr;
paulson@17583
   405
		     killChildren (map cmdchildHandle procList);
paulson@17583
   406
		     exit 0)
paulson@17306
   407
		   else if isSome cmdsFromIsa
paulson@17234
   408
		   then (*  deal with input from Isabelle *)
paulson@17306
   409
		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
paulson@17234
   410
		     then 
paulson@17234
   411
		       let val child_handles = map cmdchildHandle procList 
paulson@17234
   412
		       in
paulson@17234
   413
			  killChildren child_handles;
paulson@17306
   414
			  loop []
paulson@17234
   415
		       end
paulson@17234
   416
		     else
paulson@17306
   417
		       if length procList < 5     (********************)
paulson@17234
   418
		       then                        (* Execute locally  *)
paulson@17234
   419
			 let 
paulson@17234
   420
			   val newProcList = execCmds (valOf cmdsFromIsa) procList
paulson@17568
   421
			   val _ = Posix.ProcEnv.getppid()
paulson@17690
   422
			   val _ = trace "\nJust execed a child"
paulson@17484
   423
			   val newProcList' = checkChildren (newProcList, toParentStr) 
paulson@17234
   424
			 in
paulson@17690
   425
			   trace ("\nOff to keep watching: " ^ 
paulson@17690
   426
			          Int.toString (!iterations_left));
paulson@17306
   427
			   loop newProcList'
paulson@17234
   428
			 end
paulson@17234
   429
		       else  (* Execute remotely              *)
paulson@17234
   430
			     (* (actually not remote for now )*)
paulson@17234
   431
			 let 
paulson@17234
   432
			   val newProcList = execCmds (valOf cmdsFromIsa) procList
paulson@17568
   433
			   val _ = Posix.ProcEnv.getppid()
paulson@17234
   434
			   val newProcList' =checkChildren (newProcList, toParentStr) 
paulson@17234
   435
			 in
paulson@17306
   436
			   loop newProcList'
paulson@17234
   437
			 end
paulson@17234
   438
		   else (* No new input from Isabelle *)
paulson@17317
   439
		     let val newProcList = checkChildren (procList, toParentStr)
paulson@17234
   440
		     in
paulson@17690
   441
		       trace ("\nNo new input, still watching: " ^ 
paulson@17690
   442
			      Int.toString (!iterations_left));
paulson@17306
   443
		       loop newProcList
paulson@17234
   444
		     end
paulson@17234
   445
		 end
paulson@17234
   446
	   in  
paulson@17306
   447
	       loop procList
paulson@17234
   448
	   end
paulson@17234
   449
	   
quigley@15642
   450
paulson@17234
   451
	   in
paulson@17234
   452
	    (***************************)
paulson@17234
   453
	    (*** Sort out pipes ********)
paulson@17234
   454
	    (***************************)
quigley@15642
   455
paulson@17234
   456
	     Posix.IO.close (#outfd p1);
paulson@17234
   457
	     Posix.IO.close (#infd p2);
paulson@17234
   458
	     Posix.IO.dup2{old = oldchildin, new = fromParent};
paulson@17234
   459
	     Posix.IO.close oldchildin;
paulson@17234
   460
	     Posix.IO.dup2{old = oldchildout, new = toParent};
paulson@17234
   461
	     Posix.IO.close oldchildout;
paulson@17234
   462
paulson@17234
   463
	     (***************************)
paulson@17234
   464
	     (* start the watcher loop  *)
paulson@17234
   465
	     (***************************)
paulson@17568
   466
	     keepWatching (procList);
paulson@17234
   467
	     (****************************************************************************)
paulson@17234
   468
(* fake return value - actually want the watcher to loop until killed *)
paulson@17234
   469
	     (****************************************************************************)
paulson@17234
   470
	     Posix.Process.wordToPid 0w0
paulson@17234
   471
	   end);
paulson@17234
   472
     (* end case *)
quigley@15642
   473
quigley@15642
   474
paulson@16061
   475
    val _ = TextIO.flushOut TextIO.stdOut
quigley@15642
   476
paulson@16061
   477
    (*******************************)
paulson@16061
   478
    (***  set watcher going ********)
paulson@16061
   479
    (*******************************)
quigley@15642
   480
paulson@16061
   481
    val procList = []
paulson@17317
   482
    val pid = startWatcher procList
paulson@16061
   483
    (**************************************************)
paulson@16061
   484
    (* communication streams to watcher               *)
paulson@16061
   485
    (**************************************************)
quigley@15642
   486
paulson@16061
   487
    val instr = openInFD ("_exec_in", #infd p2)
paulson@16061
   488
    val outstr = openOutFD ("_exec_out", #outfd p1)
paulson@16061
   489
    
paulson@17568
   490
  in
paulson@17568
   491
   (*******************************)
paulson@17568
   492
   (* close the child-side fds    *)
paulson@17568
   493
   (*******************************)
paulson@17568
   494
    Posix.IO.close (#outfd p2);
paulson@17568
   495
    Posix.IO.close (#infd p1);
paulson@17568
   496
    (* set the fds close on exec *)
paulson@17568
   497
    Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
paulson@17568
   498
    Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
paulson@17568
   499
     
paulson@17568
   500
   (*******************************)
paulson@17568
   501
   (* return value                *)
paulson@17568
   502
   (*******************************)
paulson@17568
   503
    PROC{pid = pid, instr = instr, outstr = outstr}
paulson@17568
   504
  end;
quigley@15642
   505
quigley@15642
   506
quigley@15642
   507
quigley@15642
   508
(**********************************************************)
quigley@15642
   509
(* Start a watcher and set up signal handlers             *)
quigley@15642
   510
(**********************************************************)
quigley@16039
   511
paulson@17484
   512
fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
quigley@16039
   513
paulson@17488
   514
val killWatcher' = killWatcher o ResLib.pidOfInt;
paulson@17488
   515
quigley@16039
   516
fun reapWatcher(pid, instr, outstr) =
paulson@17484
   517
  (TextIO.closeIn instr; TextIO.closeOut outstr;
paulson@17484
   518
   Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
quigley@15642
   519
paulson@17484
   520
fun createWatcher (thm, clause_arr) =
paulson@17484
   521
 let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
paulson@17435
   522
     fun decr_watched() =
paulson@17502
   523
	  (goals_being_watched := !goals_being_watched - 1;
paulson@17435
   524
	   if !goals_being_watched = 0
paulson@17435
   525
	   then 
paulson@17716
   526
	     (debug ("\nReaping a watcher, childpid = "^
paulson@17690
   527
		     LargeWord.toString (Posix.Process.pidToWord childpid));
paulson@17484
   528
	      killWatcher childpid; reapWatcher (childpid,childin, childout))
paulson@17435
   529
	    else ())
paulson@17484
   530
     val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
paulson@17484
   531
     fun proofHandler n = 
paulson@17484
   532
       let val outcome = TextIO.inputLine childin
paulson@17484
   533
	   val goalstring = TextIO.inputLine childin
paulson@17484
   534
	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
paulson@17484
   535
		        "\"\ngoalstring = " ^ goalstring ^
paulson@17568
   536
		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
paulson@17502
   537
       in 
paulson@17502
   538
	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
paulson@17690
   539
	 then (priority (Recon_Transfer.apply_res_thm outcome goalstring);
paulson@17435
   540
	       decr_watched())
paulson@17484
   541
	 else if String.isPrefix "Invalid" outcome
paulson@17690
   542
	 then (priority (goalstring ^ "is not provable");
paulson@17484
   543
	       decr_watched())
paulson@17484
   544
	 else if String.isPrefix "Failure" outcome
paulson@17690
   545
	 then (priority (goalstring ^ "proof attempt failed");
paulson@17435
   546
	       decr_watched()) 
paulson@17216
   547
	(* print out a list of rules used from clasimpset*)
paulson@17484
   548
	 else if String.isPrefix "Success" outcome
paulson@17690
   549
	 then (priority (goalstring^outcome);
paulson@17435
   550
	       decr_watched())
paulson@17216
   551
	  (* if proof translation failed *)
paulson@17484
   552
	 else if String.isPrefix "Translation failed" outcome
paulson@17690
   553
	 then (priority (goalstring ^ outcome);
paulson@17435
   554
	       decr_watched())
paulson@17690
   555
	 else (priority "System error in proof handler";
paulson@17435
   556
	       decr_watched())
paulson@17484
   557
       end
paulson@17484
   558
 in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
paulson@17216
   559
    (childin, childout, childpid)
paulson@17216
   560
  end
quigley@15642
   561
quigley@15642
   562
end (* structure Watcher *)