src/HOL/Tools/ATP/watcher.ML
author paulson
Mon Sep 19 15:12:13 2005 +0200 (2005-09-19)
changeset 17484 f6a225f97f0a
parent 17435 0eed5a1c00c1
child 17488 67376a311a2b
permissions -rw-r--r--
simplification of the Isabelle-ATP code; hooks for batch generation of problems
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
(*****************************************************************************************)
paulson@17305
    20
(*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
paulson@17305
    21
(*  callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list             *)
paulson@17305
    22
(*****************************************************************************************)
paulson@17305
    23
paulson@17305
    24
val callResProvers :
paulson@17422
    25
    TextIO.outstream * (string*string*string*string*string) list 
paulson@17305
    26
    -> unit
paulson@17305
    27
paulson@17305
    28
(************************************************************************)
paulson@17305
    29
(* Send message to watcher to kill currently running resolution provers *)
paulson@17305
    30
(************************************************************************)
paulson@17305
    31
paulson@17305
    32
val callSlayer : TextIO.outstream -> unit
paulson@17305
    33
paulson@17305
    34
(**********************************************************)
paulson@17305
    35
(* Start a watcher and set up signal handlers             *)
paulson@17305
    36
(**********************************************************)
paulson@17305
    37
paulson@17484
    38
val createWatcher : 
paulson@17484
    39
    thm * (ResClause.clause * thm) Array.array -> 
paulson@17484
    40
    TextIO.instream * TextIO.outstream * Posix.Process.pid
paulson@17305
    41
paulson@17305
    42
(**********************************************************)
paulson@17305
    43
(* Kill watcher process                                   *)
paulson@17305
    44
(**********************************************************)
paulson@17305
    45
paulson@17305
    46
val killWatcher : Posix.Process.pid -> unit
paulson@17305
    47
paulson@17305
    48
end
paulson@17305
    49
paulson@17305
    50
quigley@15642
    51
quigley@15642
    52
structure Watcher: WATCHER =
paulson@17484
    53
struct
quigley@15642
    54
wenzelm@16805
    55
open ReconPrelim Recon_Transfer
wenzelm@16805
    56
quigley@15642
    57
val goals_being_watched = ref 0;
quigley@15642
    58
quigley@16039
    59
(*****************************************)
quigley@16039
    60
(*  The result of calling createWatcher  *)
quigley@16039
    61
(*****************************************)
quigley@15642
    62
quigley@16039
    63
datatype proc = PROC of {
quigley@16039
    64
        pid : Posix.Process.pid,
quigley@16039
    65
        instr : TextIO.instream,
quigley@16039
    66
        outstr : TextIO.outstream
quigley@16039
    67
      };
quigley@16039
    68
quigley@16039
    69
(*****************************************)
quigley@16039
    70
(*  The result of calling executeToList  *)
quigley@16039
    71
(*****************************************)
quigley@16039
    72
quigley@16039
    73
datatype cmdproc = CMDPROC of {
quigley@16039
    74
        prover: string,             (* Name of the resolution prover used, e.g. Vampire, SPASS *)
quigley@16039
    75
        cmd:  string,              (* The file containing the goal for res prover to prove *)     
quigley@16039
    76
        goalstring: string,         (* string representation of subgoal*) 
quigley@16039
    77
        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
quigley@16039
    78
        instr : TextIO.instream,   (*  Input stream to child process *)
quigley@16039
    79
        outstr : TextIO.outstream  (*  Output stream from child process *)
quigley@16039
    80
      };
quigley@16039
    81
quigley@16039
    82
type signal = Posix.Signal.signal
quigley@16039
    83
datatype exit_status = datatype Posix.Process.exit_status
quigley@16039
    84
quigley@16039
    85
val fromStatus = Posix.Process.fromStatus
quigley@16039
    86
quigley@16039
    87
quigley@16039
    88
fun reap(pid, instr, outstr) =
paulson@17317
    89
  let val u = TextIO.closeIn instr;
paulson@17317
    90
      val u = TextIO.closeOut outstr;
paulson@17317
    91
      val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
paulson@17317
    92
  in
paulson@17317
    93
	  status
paulson@17317
    94
  end
quigley@16039
    95
quigley@16039
    96
fun fdReader (name : string, fd : Posix.IO.file_desc) =
quigley@16039
    97
	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
quigley@16039
    98
quigley@16039
    99
fun fdWriter (name, fd) =
quigley@16039
   100
          Posix.IO.mkTextWriter {
quigley@16039
   101
	      appendMode = false,
quigley@16039
   102
              initBlkMode = true,
quigley@16039
   103
              name = name,  
quigley@16039
   104
              chunkSize=4096,
paulson@17317
   105
              fd = fd};
quigley@16039
   106
quigley@16039
   107
fun openOutFD (name, fd) =
quigley@16039
   108
	  TextIO.mkOutstream (
quigley@16039
   109
	    TextIO.StreamIO.mkOutstream (
quigley@16039
   110
	      fdWriter (name, fd), IO.BLOCK_BUF));
quigley@16039
   111
quigley@16039
   112
fun openInFD (name, fd) =
quigley@16039
   113
	  TextIO.mkInstream (
quigley@16039
   114
	    TextIO.StreamIO.mkInstream (
quigley@16039
   115
	      fdReader (name, fd), ""));
quigley@16039
   116
quigley@16039
   117
fun killChild child_handle = Unix.reap child_handle 
quigley@16039
   118
quigley@16039
   119
fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
quigley@16039
   120
quigley@16039
   121
fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
quigley@16039
   122
paulson@17317
   123
fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
quigley@16039
   124
paulson@17422
   125
fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) = 
paulson@17317
   126
  (prover,(cmd, (instr,outstr)));
quigley@16039
   127
paulson@17422
   128
fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  = 
paulson@17317
   129
  proc_handle;
quigley@16039
   130
paulson@17422
   131
fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
paulson@17317
   132
  prover;
quigley@15642
   133
paulson@17422
   134
fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
paulson@17317
   135
  goalstring;
paulson@17317
   136
quigley@15642
   137
quigley@15642
   138
(********************************************************************************)
quigley@15642
   139
(*    gets individual args from instream and concatenates them into a list      *)
quigley@15642
   140
(********************************************************************************)
quigley@15642
   141
paulson@17317
   142
fun getArgs (fromParentStr, toParentStr, ys) =  
paulson@17317
   143
  let val thisLine = TextIO.input fromParentStr
paulson@17317
   144
  in ys@[thisLine] end
quigley@15642
   145
quigley@15642
   146
                            
quigley@15642
   147
(********************************************************************************)
quigley@15642
   148
(*  Send request to Watcher for a vampire to be called for filename in arg      *)
quigley@15642
   149
(********************************************************************************)
quigley@15642
   150
                    
paulson@17231
   151
fun callResProver (toWatcherStr,  arg) = 
paulson@17317
   152
      (TextIO.output (toWatcherStr, arg^"\n"); 
paulson@17231
   153
       TextIO.flushOut toWatcherStr)
quigley@15642
   154
quigley@15642
   155
(*****************************************************************************************)
quigley@16357
   156
(*  Send request to Watcher for multiple provers to be called for filenames in arg       *)
quigley@16357
   157
(*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
quigley@15642
   158
(*****************************************************************************************)
quigley@15642
   159
quigley@16357
   160
    
paulson@17305
   161
(*Uses the $-character to separate items sent to watcher*)
paulson@16475
   162
fun callResProvers (toWatcherStr,  []) = 
paulson@17317
   163
      (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
paulson@16475
   164
|   callResProvers (toWatcherStr,
paulson@17422
   165
                    (prover,goalstring, proverCmd,settings, 
paulson@17422
   166
                     probfile)  ::  args) =
paulson@16475
   167
      let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
paulson@17422
   168
                             (prover^goalstring^proverCmd^settings^
paulson@17422
   169
                              probfile)
paulson@17317
   170
      in TextIO.output (toWatcherStr,    
paulson@17422
   171
            (prover^"$"^goalstring^"$"^proverCmd^"$"^
paulson@17422
   172
             settings^"$"^probfile^"\n"));
paulson@16475
   173
         goals_being_watched := (!goals_being_watched) + 1;
paulson@16475
   174
	 TextIO.flushOut toWatcherStr;
paulson@16475
   175
	 callResProvers (toWatcherStr,args)
paulson@16475
   176
      end   
quigley@16357
   177
                                                
paulson@17305
   178
                                    
quigley@15642
   179
 
quigley@15642
   180
(**************************************************************)
quigley@15642
   181
(* Send message to watcher to kill currently running vampires *)
quigley@15642
   182
(**************************************************************)
quigley@15642
   183
paulson@17317
   184
fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n"); 
quigley@15642
   185
                            TextIO.flushOut toWatcherStr)
quigley@15642
   186
quigley@15642
   187
quigley@15642
   188
quigley@15642
   189
(**************************************************************)
quigley@15642
   190
(* Remove \n token from a vampire goal filename and extract   *)
quigley@15642
   191
(* prover, proverCmd, settings and file from input string     *)
quigley@15642
   192
(**************************************************************)
quigley@15642
   193
paulson@16475
   194
fun separateFields str =
paulson@17305
   195
  let val _ = File.append (File.tmp_path (Path.basic "sep_field"))
paulson@17305
   196
                          ("In separateFields, str is: " ^ str ^ "\n\n") 
paulson@17422
   197
      val [prover,goalstring,proverCmd,settingstr,probfile] = 
paulson@17305
   198
          String.tokens (fn c => c = #"$") str
paulson@17305
   199
      val settings = String.tokens (fn c => c = #"%") settingstr
paulson@16475
   200
      val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
paulson@17305
   201
                  ("Sep comms are: "^ str ^"**"^
paulson@17422
   202
                   prover^" goalstr:  "^goalstring^
paulson@17422
   203
                   "\n provercmd: "^proverCmd^
paulson@17422
   204
                   "\n prob  "^probfile^"\n\n")
paulson@16475
   205
  in
paulson@17422
   206
     (prover,goalstring, proverCmd, settings, probfile)
paulson@16475
   207
  end
paulson@16475
   208
paulson@17305
   209
val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
quigley@15642
   210
paulson@17305
   211
fun getCmd cmdStr = 
paulson@17305
   212
  let val cmdStr' = remove_newlines cmdStr
paulson@17305
   213
  in
paulson@17305
   214
      File.write (File.tmp_path (Path.basic"sepfields_call")) 
paulson@17422
   215
		 ("about to call separateFields with " ^ cmdStr');
paulson@17422
   216
      separateFields cmdStr'
paulson@17305
   217
  end;
quigley@15642
   218
                      
quigley@15642
   219
(**************************************************************)
quigley@15642
   220
(* Get commands from Isabelle                                 *)
quigley@15642
   221
(**************************************************************)
quigley@15642
   222
quigley@15642
   223
fun getCmds (toParentStr,fromParentStr, cmdList) = 
paulson@16475
   224
  let val thisLine = TextIO.inputLine fromParentStr 
paulson@16475
   225
      val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
paulson@16475
   226
  in
paulson@17422
   227
     if thisLine = "End of calls\n" then cmdList
paulson@17422
   228
     else if thisLine = "Kill children\n"
paulson@16475
   229
     then 
paulson@16475
   230
	 (   TextIO.output (toParentStr,thisLine ); 
paulson@16475
   231
	     TextIO.flushOut toParentStr;
paulson@17422
   232
	   (("","","Kill children",[],"")::cmdList)
paulson@16475
   233
	  )
paulson@17422
   234
     else let val thisCmd = getCmd thisLine 
paulson@16475
   235
	       (*********************************************************)
paulson@17422
   236
	       (* thisCmd = (prover,proverCmd, settings, file)*)
paulson@16475
   237
	       (* i.e. put back into tuple format                       *)
paulson@16475
   238
	       (*********************************************************)
paulson@16475
   239
	   in
paulson@16475
   240
	     (*TextIO.output (toParentStr, thisCmd); 
paulson@16475
   241
	       TextIO.flushOut toParentStr;*)
paulson@17422
   242
	       getCmds (toParentStr, fromParentStr, thisCmd::cmdList)
paulson@16475
   243
	   end
paulson@16475
   244
  end
paulson@16475
   245
	    
quigley@16357
   246
                                                                  
quigley@15642
   247
(**************************************************************)
quigley@15642
   248
(*  Get Io-descriptor for polling of an input stream          *)
quigley@15642
   249
(**************************************************************)
quigley@15642
   250
quigley@15642
   251
fun getInIoDesc someInstr = 
quigley@15642
   252
    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
paulson@15702
   253
        val _ = TextIO.output (TextIO.stdOut, buf)
quigley@15642
   254
        val ioDesc = 
quigley@15642
   255
	    case rd
quigley@15642
   256
	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
quigley@15642
   257
	       | _ => NONE
quigley@15642
   258
     in (* since getting the reader will have terminated the stream, we need
quigley@15642
   259
	 * to build a new stream. *)
quigley@15642
   260
	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
quigley@15642
   261
	ioDesc
quigley@15642
   262
    end
quigley@15642
   263
quigley@15642
   264
quigley@15642
   265
(*************************************)
quigley@15642
   266
(*  Set up a Watcher Process         *)
quigley@15642
   267
(*************************************)
quigley@15642
   268
paulson@17422
   269
fun getProofCmd (a,c,d,e,f) = d
paulson@17422
   270
paulson@17484
   271
fun prems_string_of th =
paulson@17484
   272
  Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
paulson@17484
   273
paulson@17484
   274
fun setupWatcher (thm,clause_arr) = 
paulson@16061
   275
  let
paulson@16061
   276
    (** pipes for communication between parent and watcher **)
paulson@16061
   277
    val p1 = Posix.IO.pipe ()
paulson@16061
   278
    val p2 = Posix.IO.pipe ()
paulson@17317
   279
    fun closep () = 
paulson@17317
   280
	 (Posix.IO.close (#outfd p1); 
paulson@16061
   281
	  Posix.IO.close (#infd p1);
paulson@16061
   282
	  Posix.IO.close (#outfd p2); 
paulson@17317
   283
	  Posix.IO.close (#infd p2))
paulson@16061
   284
    (***********************************************************)
paulson@16061
   285
    (****** fork a watcher process and get it set up and going *)
paulson@16061
   286
    (***********************************************************)
paulson@17317
   287
    fun startWatcher procList =
paulson@17234
   288
     (case  Posix.Process.fork() (***************************************)
paulson@17234
   289
      of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
paulson@17234
   290
				    (***************************************)
paulson@16061
   291
paulson@17234
   292
				      (*************************)
paulson@17234
   293
       | NONE => let                  (* child - i.e. watcher  *)
paulson@17234
   294
	   val oldchildin = #infd p1  (*************************)
paulson@17234
   295
	   val fromParent = Posix.FileSys.wordToFD 0w0
paulson@17234
   296
	   val oldchildout = #outfd p2
paulson@17234
   297
	   val toParent = Posix.FileSys.wordToFD 0w1
paulson@17234
   298
	   val fromParentIOD = Posix.FileSys.fdToIOD fromParent
paulson@17234
   299
	   val fromParentStr = openInFD ("_exec_in_parent", fromParent)
paulson@17234
   300
	   val toParentStr = openOutFD ("_exec_out_parent", toParent)
paulson@17484
   301
	   val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
paulson@17234
   302
	   fun killChildren [] = ()
paulson@17306
   303
	|      killChildren  (child_handle::children) =
paulson@17306
   304
	         (killChild child_handle; killChildren children)
quigley@15642
   305
paulson@17234
   306
	 (*************************************************************)
paulson@17234
   307
	 (* take an instream and poll its underlying reader for input *)
paulson@17234
   308
	 (*************************************************************)
quigley@15642
   309
paulson@17234
   310
	 fun pollParentInput () = 
paulson@17317
   311
	   let val pd = OS.IO.pollDesc fromParentIOD
paulson@17306
   312
	   in 
paulson@17306
   313
	     if isSome pd then 
paulson@17306
   314
		 let val pd' = OS.IO.pollIn (valOf pd)
paulson@17306
   315
		     val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
paulson@17306
   316
		     val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
paulson@17306
   317
		       ("In parent_poll\n")	
paulson@17306
   318
		 in
paulson@17306
   319
		    if null pdl 
paulson@17306
   320
		    then
paulson@17306
   321
		       NONE
paulson@17306
   322
		    else if (OS.IO.isIn (hd pdl)) 
paulson@17306
   323
			 then SOME (getCmds (toParentStr, fromParentStr, []))
paulson@17306
   324
			 else NONE
paulson@17306
   325
		 end
paulson@17306
   326
	       else NONE
paulson@17306
   327
	   end
paulson@17234
   328
		 
paulson@17317
   329
	  fun pollChildInput fromStr = 
paulson@17306
   330
	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
paulson@17306
   331
			 ("In child_poll\n")
paulson@17306
   332
	       val iod = getInIoDesc fromStr
paulson@17306
   333
	   in 
paulson@17306
   334
	     if isSome iod 
paulson@17306
   335
	     then 
paulson@17306
   336
	       let val pd = OS.IO.pollDesc (valOf iod)
paulson@17306
   337
	       in 
paulson@17306
   338
	       if isSome pd then 
paulson@17306
   339
		   let val pd' = OS.IO.pollIn (valOf pd)
paulson@17306
   340
		       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
paulson@17306
   341
		   in
paulson@17306
   342
		      if null pdl 
paulson@17306
   343
		      then
paulson@17306
   344
			(File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl\n"; 
paulson@17306
   345
			 NONE)
paulson@17306
   346
		      else if OS.IO.isIn (hd pdl)
paulson@17306
   347
		      then
paulson@17306
   348
			   let val inval =  (TextIO.inputLine fromStr)
paulson@17306
   349
			       val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
paulson@17306
   350
			   in SOME inval end
paulson@17306
   351
		      else
paulson@17306
   352
                        (File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl \n";
paulson@17306
   353
                         NONE)
paulson@17306
   354
		   end
paulson@17306
   355
		 else NONE
paulson@17306
   356
		 end
paulson@17306
   357
	     else NONE
paulson@17234
   358
	end
quigley@15642
   359
quigley@15642
   360
paulson@17234
   361
	(****************************************************************************)
paulson@17234
   362
	(* Check all vampire processes currently running for output                 *)
paulson@17234
   363
	(****************************************************************************) 
paulson@17234
   364
						   (*********************************)
paulson@17234
   365
	 fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
paulson@17234
   366
						   (*********************************)
paulson@17234
   367
	 |   checkChildren ((childProc::otherChildren), toParentStr) = 
paulson@17234
   368
	       let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
paulson@17305
   369
			      ("In check child, length of queue:"^
paulson@17484
   370
			       string_of_int (length (childProc::otherChildren)))
paulson@17234
   371
		   val (childInput,childOutput) =  cmdstreamsOf childProc
paulson@17234
   372
		   val child_handle= cmdchildHandle childProc
paulson@17234
   373
		   (* childCmd is the .dfg file that the problem is in *)
paulson@17234
   374
		   val childCmd = fst(snd (cmdchildInfo childProc))
paulson@17484
   375
		   val _ = File.append (File.tmp_path (Path.basic "child_check")) 
paulson@17484
   376
			      ("\nchildCmd = " ^ childCmd)
paulson@17234
   377
		   (* now get the number of the subgoal from the filename *)
paulson@17305
   378
		   val path_parts = String.tokens(fn c => c = #"/") childCmd
paulson@17305
   379
		   val digits = String.translate 
paulson@17305
   380
		                  (fn c => if Char.isDigit c then str c else "")
paulson@17305
   381
		                  (List.last path_parts);
paulson@17484
   382
		   val sg_num =
paulson@17484
   383
		     (case Int.fromString digits of SOME n => n
paulson@17484
   384
                        | NONE => (File.append (File.tmp_path (Path.basic "child_check")) 
paulson@17484
   385
                                   "\nWatcher could not read subgoal nunber!!";
paulson@17484
   386
                                   raise ERROR));
paulson@17234
   387
		   val childIncoming = pollChildInput childInput
paulson@17484
   388
		   val _ = File.append (File.tmp_path (Path.basic "child_check")) 
paulson@17484
   389
			         "\nfinished polling child"
paulson@17234
   390
		   val parentID = Posix.ProcEnv.getppid()
paulson@17234
   391
		   val prover = cmdProver childProc
paulson@17484
   392
		   val prems_string = prems_string_of thm
paulson@17234
   393
		   val goalstring = cmdGoal childProc							
paulson@17484
   394
		   val _ =  File.append (File.tmp_path (Path.basic "child_check")) 
paulson@17484
   395
		             ("\nsubgoals forked to checkChildren: " ^ 
paulson@17484
   396
		              space_implode "\n" [prems_string,prover,goalstring])
paulson@17234
   397
	       in 
paulson@17306
   398
		 if isSome childIncoming
paulson@17234
   399
		 then 
paulson@17306
   400
		   (* check here for prover label on child*)
paulson@17484
   401
		   let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
paulson@17484
   402
			         "\nInput available from childIncoming" 
paulson@17306
   403
		       val childDone = (case prover of
paulson@17484
   404
			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  
paulson@17484
   405
			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)             
paulson@17484
   406
			  |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  )
paulson@17306
   407
		    in
paulson@17484
   408
		     if childDone
paulson@17306
   409
		     then (* child has found a proof and transferred it *)
paulson@17306
   410
			(* Remove this child and go on to check others*)
paulson@17306
   411
			(**********************************************)
paulson@17306
   412
			(Unix.reap child_handle;
paulson@17306
   413
			 checkChildren(otherChildren, toParentStr))
paulson@17306
   414
		     else 
paulson@17306
   415
			(**********************************************)
paulson@17306
   416
			(* Keep this child and go on to check others  *)
paulson@17306
   417
			(**********************************************)
paulson@17306
   418
		       (childProc::(checkChildren (otherChildren, toParentStr)))
paulson@17306
   419
		  end
paulson@17306
   420
		else
paulson@17484
   421
		  (File.append (File.tmp_path (Path.basic "child_check"))
paulson@17484
   422
		               "No child output";
paulson@17306
   423
		   childProc::(checkChildren (otherChildren, toParentStr)))
paulson@17234
   424
	       end
quigley@15642
   425
paulson@17234
   426
	
paulson@17234
   427
     (********************************************************************)                  
paulson@17234
   428
     (* call resolution processes                                        *)
paulson@17234
   429
     (* settings should be a list of strings                             *)
paulson@17234
   430
     (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
paulson@17234
   431
     (* takes list of (string, string, string list, string)list proclist *)
paulson@17234
   432
     (********************************************************************)
quigley@15642
   433
quigley@16039
   434
paulson@16061
   435
(*** add subgoal id num to this *)
paulson@17234
   436
	fun execCmds  [] procList = procList
paulson@17422
   437
	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
paulson@17317
   438
	      let val _ = File.write (File.tmp_path (Path.basic "exec_child"))  
paulson@17317
   439
	                    (space_implode "\n" 
paulson@17317
   440
	                      (["About to execute command for goal:",
paulson@17317
   441
	                        goalstring, proverCmd] @ settings @
paulson@17317
   442
	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
paulson@17317
   443
	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
paulson@17234
   444
		       (Unix.execute(proverCmd, (settings@[file])))
paulson@17234
   445
		  val (instr, outstr) = Unix.streamsOf childhandle
paulson@17234
   446
		  
paulson@17234
   447
		  val newProcList = (CMDPROC{
paulson@17234
   448
				       prover = prover,
paulson@17234
   449
				       cmd = file,
paulson@17234
   450
				       goalstring = goalstring,
paulson@17234
   451
				       proc_handle = childhandle,
paulson@17234
   452
				       instr = instr,
paulson@17234
   453
				       outstr = outstr }) :: procList
paulson@17234
   454
     
paulson@17234
   455
		  val _ = File.append (File.tmp_path (Path.basic "exec_child")) 
paulson@17317
   456
			    ("\nFinished at " ^
paulson@17317
   457
			     Date.toString(Date.fromTimeLocal(Time.now())))
paulson@17234
   458
	      in
paulson@17234
   459
		Posix.Process.sleep (Time.fromSeconds 1); 
paulson@17234
   460
		execCmds cmds newProcList
paulson@17234
   461
	      end
quigley@15642
   462
quigley@16039
   463
paulson@17234
   464
     (****************************************)                  
paulson@17234
   465
     (* call resolution processes remotely   *)
paulson@17234
   466
     (* settings should be a list of strings *)
paulson@17317
   467
     (* e.g. ["-t300", "-m100000"]         *)
paulson@17234
   468
     (****************************************)
paulson@16061
   469
paulson@17234
   470
      (*  fun execRemoteCmds  [] procList = procList
paulson@17422
   471
	|   execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList  =  
paulson@17422
   472
	      let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
paulson@17422
   473
		  in
paulson@17422
   474
		       execRemoteCmds  cmds newProcList
paulson@17422
   475
		  end
quigley@16039
   476
*)
quigley@15642
   477
paulson@17234
   478
     (**********************************************)                  
paulson@17234
   479
     (* Watcher Loop                               *)
paulson@17234
   480
     (**********************************************)
paulson@17306
   481
         val iterations_left = ref 1000;  (*200 seconds, 5 iterations per sec*)
paulson@16061
   482
paulson@17234
   483
	 fun keepWatching (toParentStr, fromParentStr,procList) = 
paulson@17317
   484
	   let fun loop procList =  
paulson@17234
   485
		let val _ = Posix.Process.sleep (Time.fromMilliseconds 200)
paulson@17234
   486
		    val cmdsFromIsa = pollParentInput ()
paulson@17306
   487
		    fun killchildHandler ()  = 
paulson@17306
   488
			  (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
paulson@17234
   489
			   TextIO.flushOut toParentStr;
paulson@17317
   490
			   killChildren (map cmdchildHandle procList);
paulson@17234
   491
			   ())
paulson@17234
   492
		in 
paulson@17234
   493
		   (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
paulson@17306
   494
		   iterations_left := !iterations_left - 1;
paulson@17306
   495
		   if !iterations_left = 0 then killchildHandler ()
paulson@17306
   496
		   else if isSome cmdsFromIsa
paulson@17234
   497
		   then (*  deal with input from Isabelle *)
paulson@17306
   498
		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
paulson@17234
   499
		     then 
paulson@17234
   500
		       let val child_handles = map cmdchildHandle procList 
paulson@17234
   501
		       in
paulson@17234
   502
			  killChildren child_handles;
paulson@17234
   503
			  (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)    
paulson@17306
   504
			  loop []
paulson@17234
   505
		       end
paulson@17234
   506
		     else
paulson@17306
   507
		       if length procList < 5     (********************)
paulson@17234
   508
		       then                        (* Execute locally  *)
paulson@17234
   509
			 let 
paulson@17234
   510
			   val newProcList = execCmds (valOf cmdsFromIsa) procList
paulson@17234
   511
			   val parentID = Posix.ProcEnv.getppid()
paulson@17484
   512
			      val _ = File.append (File.tmp_path (Path.basic "prekeep_watch"))
paulson@17484
   513
			      "Just execed a child\n"
paulson@17484
   514
			   val newProcList' = checkChildren (newProcList, toParentStr) 
paulson@17234
   515
			 in
paulson@17484
   516
			   File.append (File.tmp_path (Path.basic "keep_watch")) 
paulson@17484
   517
			       "Off to keep watching...\n";
paulson@17306
   518
			   loop newProcList'
paulson@17234
   519
			 end
paulson@17234
   520
		       else  (* Execute remotely              *)
paulson@17234
   521
			     (* (actually not remote for now )*)
paulson@17234
   522
			 let 
paulson@17234
   523
			   val newProcList = execCmds (valOf cmdsFromIsa) procList
paulson@17234
   524
			   val parentID = Posix.ProcEnv.getppid()
paulson@17234
   525
			   val newProcList' =checkChildren (newProcList, toParentStr) 
paulson@17234
   526
			 in
paulson@17306
   527
			   loop newProcList'
paulson@17234
   528
			 end
paulson@17234
   529
		   else (* No new input from Isabelle *)
paulson@17317
   530
		     let val newProcList = checkChildren (procList, toParentStr)
paulson@17234
   531
		     in
paulson@17484
   532
		      (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...2\n ");
paulson@17306
   533
		       loop newProcList
paulson@17234
   534
		     end
paulson@17234
   535
		 end
paulson@17234
   536
	   in  
paulson@17306
   537
	       loop procList
paulson@17234
   538
	   end
paulson@17234
   539
	   
quigley@15642
   540
paulson@17234
   541
	   in
paulson@17234
   542
	    (***************************)
paulson@17234
   543
	    (*** Sort out pipes ********)
paulson@17234
   544
	    (***************************)
quigley@15642
   545
paulson@17234
   546
	     Posix.IO.close (#outfd p1);
paulson@17234
   547
	     Posix.IO.close (#infd p2);
paulson@17234
   548
	     Posix.IO.dup2{old = oldchildin, new = fromParent};
paulson@17234
   549
	     Posix.IO.close oldchildin;
paulson@17234
   550
	     Posix.IO.dup2{old = oldchildout, new = toParent};
paulson@17234
   551
	     Posix.IO.close oldchildout;
paulson@17234
   552
paulson@17234
   553
	     (***************************)
paulson@17234
   554
	     (* start the watcher loop  *)
paulson@17234
   555
	     (***************************)
paulson@17234
   556
	     keepWatching (toParentStr, fromParentStr, procList);
paulson@17234
   557
	     (****************************************************************************)
paulson@17234
   558
(* fake return value - actually want the watcher to loop until killed *)
paulson@17234
   559
	     (****************************************************************************)
paulson@17234
   560
	     Posix.Process.wordToPid 0w0
paulson@17234
   561
	   end);
paulson@17234
   562
     (* end case *)
quigley@15642
   563
quigley@15642
   564
paulson@16061
   565
    val _ = TextIO.flushOut TextIO.stdOut
quigley@15642
   566
paulson@16061
   567
    (*******************************)
paulson@16061
   568
    (***  set watcher going ********)
paulson@16061
   569
    (*******************************)
quigley@15642
   570
paulson@16061
   571
    val procList = []
paulson@17317
   572
    val pid = startWatcher procList
paulson@16061
   573
    (**************************************************)
paulson@16061
   574
    (* communication streams to watcher               *)
paulson@16061
   575
    (**************************************************)
quigley@15642
   576
paulson@16061
   577
    val instr = openInFD ("_exec_in", #infd p2)
paulson@16061
   578
    val outstr = openOutFD ("_exec_out", #outfd p1)
paulson@16061
   579
    
paulson@16061
   580
    in
paulson@16061
   581
     (*******************************)
paulson@16061
   582
     (* close the child-side fds    *)
paulson@16061
   583
     (*******************************)
paulson@16061
   584
      Posix.IO.close (#outfd p2);
paulson@16061
   585
      Posix.IO.close (#infd p1);
paulson@16061
   586
      (* set the fds close on exec *)
paulson@16061
   587
      Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
paulson@16061
   588
      Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
paulson@16061
   589
       
paulson@16061
   590
     (*******************************)
paulson@16061
   591
     (* return value                *)
paulson@16061
   592
     (*******************************)
paulson@16061
   593
      PROC{pid = pid,
paulson@16061
   594
	instr = instr,
paulson@16061
   595
	outstr = outstr
paulson@16061
   596
      }
paulson@16061
   597
   end;
quigley@15642
   598
quigley@15642
   599
quigley@15642
   600
quigley@15642
   601
(**********************************************************)
quigley@15642
   602
(* Start a watcher and set up signal handlers             *)
quigley@15642
   603
(**********************************************************)
quigley@16039
   604
paulson@17484
   605
fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
quigley@16039
   606
quigley@16039
   607
fun reapWatcher(pid, instr, outstr) =
paulson@17484
   608
  (TextIO.closeIn instr; TextIO.closeOut outstr;
paulson@17484
   609
   Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
quigley@15642
   610
paulson@17484
   611
fun createWatcher (thm, clause_arr) =
paulson@17484
   612
 let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
paulson@17435
   613
     fun decr_watched() =
paulson@17435
   614
	  (goals_being_watched := (!goals_being_watched) - 1;
paulson@17435
   615
	   if !goals_being_watched = 0
paulson@17435
   616
	   then 
paulson@17435
   617
	     (File.append (File.tmp_path (Path.basic "reap_found"))
paulson@17435
   618
	       ("Reaping a watcher, childpid = "^
paulson@17435
   619
		LargeWord.toString (Posix.Process.pidToWord childpid)^"\n");
paulson@17484
   620
	      killWatcher childpid; reapWatcher (childpid,childin, childout))
paulson@17435
   621
	    else ())
paulson@17484
   622
     val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
paulson@17484
   623
     fun proofHandler n = 
paulson@17484
   624
       let val outcome = TextIO.inputLine childin
paulson@17484
   625
	   val goalstring = TextIO.inputLine childin
paulson@17484
   626
	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
paulson@17484
   627
		        "\"\ngoalstring = " ^ goalstring ^
paulson@17484
   628
		        "\ngoals_being_watched: "^ string_of_int (!goals_being_watched))
paulson@17216
   629
       in (* if a proof has been found and sent back as a reconstruction proof *)
paulson@17484
   630
	 if String.isPrefix "[" outcome
paulson@17216
   631
	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17484
   632
	       Recon_Transfer.apply_res_thm outcome goalstring;
paulson@17216
   633
	       Pretty.writeln(Pretty.str  (oct_char "361"));
paulson@17435
   634
	       decr_watched())
paulson@17484
   635
	 (* if there's no proof, but a message from the signalling process*)
paulson@17484
   636
	 else if String.isPrefix "Invalid" outcome
paulson@17435
   637
	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17484
   638
	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) 
paulson@17484
   639
	       ^ "is not provable"));
paulson@17484
   640
	       Pretty.writeln(Pretty.str  (oct_char "361"));
paulson@17484
   641
	       decr_watched())
paulson@17484
   642
	 else if String.isPrefix "Failure" outcome
paulson@17484
   643
	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17484
   644
	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring) 
paulson@17484
   645
	       ^ "proof attempt failed"));
paulson@17216
   646
	       Pretty.writeln(Pretty.str  (oct_char "361"));
paulson@17435
   647
	       decr_watched()) 
paulson@17216
   648
	(* print out a list of rules used from clasimpset*)
paulson@17484
   649
	 else if String.isPrefix "Success" outcome
paulson@17435
   650
	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17484
   651
	       Pretty.writeln(Pretty.str (goalstring^outcome));
paulson@17216
   652
	       Pretty.writeln(Pretty.str  (oct_char "361"));
paulson@17435
   653
	       decr_watched())
paulson@17216
   654
	  (* if proof translation failed *)
paulson@17484
   655
	 else if String.isPrefix "Translation failed" outcome
paulson@17435
   656
	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17484
   657
	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks outcome)));
paulson@17216
   658
	       Pretty.writeln(Pretty.str  (oct_char "361"));
paulson@17435
   659
	       decr_watched())
paulson@17484
   660
	 else  
paulson@17435
   661
	      (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17484
   662
	       Pretty.writeln(Pretty.str ("System error in proof handler"));
paulson@17231
   663
	       Pretty.writeln(Pretty.str  (oct_char "361"));
paulson@17435
   664
	       decr_watched())
paulson@17484
   665
       end
paulson@17484
   666
 in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
paulson@17216
   667
    (childin, childout, childpid)
paulson@17216
   668
  end
quigley@15642
   669
quigley@15642
   670
end (* structure Watcher *)