src/HOL/Tools/ATP/watcher.ML
author paulson
Wed Sep 07 09:54:31 2005 +0200 (2005-09-07)
changeset 17305 6cef3aedd661
parent 17235 8e55ad29b690
child 17306 5cde710a8a23
permissions -rw-r--r--
axioms now included in tptp files, no /bin/cat and various tidying
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
paulson@17305
    17
signature WATCHER =
paulson@17305
    18
sig
paulson@17305
    19
paulson@17305
    20
(*****************************************************************************************)
paulson@17305
    21
(*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
paulson@17305
    22
(*  callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list             *)
paulson@17305
    23
(*****************************************************************************************)
paulson@17305
    24
paulson@17305
    25
val callResProvers :
paulson@17305
    26
    TextIO.outstream * (string*string*string*string*string*string*string*string) list 
paulson@17305
    27
    -> unit
paulson@17305
    28
paulson@17305
    29
(************************************************************************)
paulson@17305
    30
(* Send message to watcher to kill currently running resolution provers *)
paulson@17305
    31
(************************************************************************)
paulson@17305
    32
paulson@17305
    33
val callSlayer : TextIO.outstream -> unit
paulson@17305
    34
paulson@17305
    35
(**********************************************************)
paulson@17305
    36
(* Start a watcher and set up signal handlers             *)
paulson@17305
    37
(**********************************************************)
paulson@17305
    38
paulson@17305
    39
val createWatcher : thm*(ResClause.clause * thm) Array.array *  int -> TextIO.instream * TextIO.outstream * Posix.Process.pid
paulson@17305
    40
paulson@17305
    41
(**********************************************************)
paulson@17305
    42
(* Kill watcher process                                   *)
paulson@17305
    43
(**********************************************************)
paulson@17305
    44
paulson@17305
    45
val killWatcher : Posix.Process.pid -> unit
paulson@17305
    46
paulson@17305
    47
end
paulson@17305
    48
paulson@17305
    49
quigley@15642
    50
quigley@15642
    51
quigley@15642
    52
structure Watcher: WATCHER =
quigley@15642
    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
        thmstring: string,         (* string representation of subgoal after negation, skolemization*) 
quigley@16039
    77
        goalstring: string,         (* string representation of subgoal*) 
quigley@16039
    78
        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
quigley@16039
    79
        instr : TextIO.instream,   (*  Input stream to child process *)
quigley@16039
    80
        outstr : TextIO.outstream  (*  Output stream from child process *)
quigley@16039
    81
      };
quigley@16039
    82
quigley@16039
    83
type signal = Posix.Signal.signal
quigley@16039
    84
datatype exit_status = datatype Posix.Process.exit_status
quigley@16039
    85
quigley@16039
    86
val fromStatus = Posix.Process.fromStatus
quigley@16039
    87
quigley@16039
    88
quigley@16039
    89
fun reap(pid, instr, outstr) =
quigley@16039
    90
        let
quigley@16039
    91
		val u = TextIO.closeIn instr;
quigley@16039
    92
	        val u = TextIO.closeOut outstr;
quigley@16039
    93
	
quigley@16039
    94
		val (_, status) =
quigley@16039
    95
			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
quigley@16039
    96
	in
quigley@16039
    97
		status
quigley@16039
    98
	end
quigley@16039
    99
quigley@16039
   100
fun fdReader (name : string, fd : Posix.IO.file_desc) =
quigley@16039
   101
	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
quigley@16039
   102
quigley@16039
   103
fun fdWriter (name, fd) =
quigley@16039
   104
          Posix.IO.mkTextWriter {
quigley@16039
   105
	      appendMode = false,
quigley@16039
   106
              initBlkMode = true,
quigley@16039
   107
              name = name,  
quigley@16039
   108
              chunkSize=4096,
quigley@16039
   109
              fd = fd
quigley@16039
   110
            };
quigley@16039
   111
quigley@16039
   112
fun openOutFD (name, fd) =
quigley@16039
   113
	  TextIO.mkOutstream (
quigley@16039
   114
	    TextIO.StreamIO.mkOutstream (
quigley@16039
   115
	      fdWriter (name, fd), IO.BLOCK_BUF));
quigley@16039
   116
quigley@16039
   117
fun openInFD (name, fd) =
quigley@16039
   118
	  TextIO.mkInstream (
quigley@16039
   119
	    TextIO.StreamIO.mkInstream (
quigley@16039
   120
	      fdReader (name, fd), ""));
quigley@16039
   121
quigley@16039
   122
fun killChild child_handle = Unix.reap child_handle 
quigley@16039
   123
quigley@16039
   124
fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
quigley@16039
   125
quigley@16039
   126
fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
quigley@16039
   127
quigley@16039
   128
fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
quigley@16039
   129
quigley@16039
   130
fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = (prover,(cmd, (instr,outstr)));
quigley@16039
   131
quigley@16039
   132
fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = proc_handle;
quigley@16039
   133
quigley@16039
   134
fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (prover);
quigley@16039
   135
quigley@16039
   136
fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (thmstring);
quigley@16039
   137
quigley@16039
   138
fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (goalstring);
quigley@15642
   139
quigley@15642
   140
fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
quigley@15642
   141
quigley@15642
   142
(********************************************************************************************)
quigley@15642
   143
(*  takes a list of arguments and sends them individually to the watcher process by pipe    *)
quigley@15642
   144
(********************************************************************************************)
quigley@15642
   145
quigley@15642
   146
fun outputArgs (toWatcherStr, []) = ()
quigley@15642
   147
|   outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); 
quigley@15642
   148
                                          TextIO.flushOut toWatcherStr;
quigley@15642
   149
                                         outputArgs (toWatcherStr, xs))
quigley@15642
   150
quigley@15642
   151
(********************************************************************************)
quigley@15642
   152
(*    gets individual args from instream and concatenates them into a list      *)
quigley@15642
   153
(********************************************************************************)
quigley@15642
   154
quigley@15642
   155
fun getArgs (fromParentStr, toParentStr,ys) =  let 
quigley@15642
   156
                                       val thisLine = TextIO.input fromParentStr
quigley@15642
   157
                                    in
quigley@15642
   158
                                        ((ys@[thisLine]))
quigley@15642
   159
                                    end
quigley@15642
   160
quigley@15642
   161
                            
quigley@15642
   162
(********************************************************************************)
quigley@15642
   163
(*  Send request to Watcher for a vampire to be called for filename in arg      *)
quigley@15642
   164
(********************************************************************************)
quigley@15642
   165
                    
paulson@17231
   166
fun callResProver (toWatcherStr,  arg) = 
paulson@17231
   167
      (sendOutput (toWatcherStr, arg^"\n"); 
paulson@17231
   168
       TextIO.flushOut toWatcherStr)
quigley@15642
   169
quigley@15642
   170
(*****************************************************************************************)
quigley@16357
   171
(*  Send request to Watcher for multiple provers to be called for filenames in arg       *)
quigley@16357
   172
(*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
quigley@15642
   173
(*****************************************************************************************)
quigley@15642
   174
quigley@16357
   175
    
paulson@17305
   176
(*Uses the $-character to separate items sent to watcher*)
paulson@16475
   177
fun callResProvers (toWatcherStr,  []) = 
paulson@16475
   178
      (sendOutput (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
paulson@16475
   179
|   callResProvers (toWatcherStr,
paulson@17305
   180
                    (prover,thmstring,goalstring, proverCmd,settings, 
paulson@16475
   181
                     axfile, hypsfile,probfile)  ::  args) =
paulson@16475
   182
      let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
paulson@16475
   183
                             (prover^thmstring^goalstring^proverCmd^settings^
paulson@17305
   184
                              hypsfile^probfile)
paulson@16475
   185
      in sendOutput (toWatcherStr,    
quigley@16675
   186
            (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^
paulson@17305
   187
             settings^"$"^hypsfile^"$"^probfile^"\n"));
paulson@16475
   188
         goals_being_watched := (!goals_being_watched) + 1;
paulson@16475
   189
	 TextIO.flushOut toWatcherStr;
paulson@16475
   190
	 callResProvers (toWatcherStr,args)
paulson@16475
   191
      end   
quigley@16357
   192
                                                
paulson@17305
   193
                                    
quigley@15642
   194
 
quigley@15642
   195
(**************************************************************)
quigley@15642
   196
(* Send message to watcher to kill currently running vampires *)
quigley@15642
   197
(**************************************************************)
quigley@15642
   198
quigley@15642
   199
fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 
quigley@15642
   200
                            TextIO.flushOut toWatcherStr)
quigley@15642
   201
quigley@15642
   202
quigley@15642
   203
quigley@15642
   204
(**************************************************************)
quigley@15642
   205
(* Remove \n token from a vampire goal filename and extract   *)
quigley@15642
   206
(* prover, proverCmd, settings and file from input string     *)
quigley@15642
   207
(**************************************************************)
quigley@15642
   208
paulson@16475
   209
fun separateFields str =
paulson@17305
   210
  let val _ = File.append (File.tmp_path (Path.basic "sep_field"))
paulson@17305
   211
                          ("In separateFields, str is: " ^ str ^ "\n\n") 
paulson@17305
   212
      val [prover,thmstring,goalstring,proverCmd,settingstr,hypsfile,probfile] = 
paulson@17305
   213
          String.tokens (fn c => c = #"$") str
paulson@17305
   214
      val settings = String.tokens (fn c => c = #"%") settingstr
paulson@16475
   215
      val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
paulson@17305
   216
                  ("Sep comms are: "^ str ^"**"^
paulson@17234
   217
                   prover^" thmstring: "^thmstring^"\n goalstr:  "^goalstring^
paulson@17305
   218
                   " \n provercmd: "^proverCmd^
paulson@17305
   219
                   " \n hyps "^hypsfile^"\n prob  "^probfile^"\n\n")
paulson@16475
   220
  in
paulson@17305
   221
     (prover,thmstring,goalstring, proverCmd, settings, hypsfile, probfile)
paulson@16475
   222
  end
paulson@16475
   223
quigley@16357
   224
                      
paulson@17305
   225
fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, hypsfile ,probfile) = 
paulson@16475
   226
  let
paulson@16561
   227
    val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
paulson@17305
   228
	       (thmstring ^ "\n goals_watched" ^ 
paulson@17305
   229
	       (string_of_int(!goals_being_watched)) ^ probfile^"\n")
paulson@16561
   230
  in
paulson@17305
   231
    (prover, thmstring, goalstring, proverCmd, settings, probfile)	
paulson@16561
   232
  end;
quigley@16478
   233
paulson@17305
   234
val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
quigley@15642
   235
paulson@17305
   236
fun getCmd cmdStr = 
paulson@17305
   237
  let val cmdStr' = remove_newlines cmdStr
paulson@17305
   238
  in
paulson@17305
   239
      File.write (File.tmp_path (Path.basic"sepfields_call")) 
paulson@17305
   240
		 ("about to call sepfields with " ^ cmdStr');
paulson@17305
   241
      formatCmd (separateFields cmdStr')
paulson@17305
   242
  end;
quigley@15642
   243
                      
quigley@15642
   244
quigley@15642
   245
fun getProofCmd (a,b,c,d,e,f) = d
quigley@15642
   246
quigley@16357
   247
                        
quigley@15642
   248
(**************************************************************)
quigley@15642
   249
(* Get commands from Isabelle                                 *)
quigley@15642
   250
(**************************************************************)
quigley@16357
   251
(* FIX: or perhaps do the tptp2x stuff here - so it's get commands and then format them, before passing them to spass *)
quigley@15642
   252
quigley@15642
   253
fun getCmds (toParentStr,fromParentStr, cmdList) = 
paulson@16475
   254
  let val thisLine = TextIO.inputLine fromParentStr 
paulson@16475
   255
      val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
paulson@16475
   256
  in
paulson@16475
   257
     if (thisLine = "End of calls\n") 
paulson@16475
   258
     then cmdList
paulson@16475
   259
     else if (thisLine = "Kill children\n") 
paulson@16475
   260
     then 
paulson@16475
   261
	 (   TextIO.output (toParentStr,thisLine ); 
paulson@16475
   262
	     TextIO.flushOut toParentStr;
paulson@16475
   263
	   (("","","","Kill children",[],"")::cmdList)
paulson@16475
   264
	  )
paulson@16475
   265
     else  let val thisCmd = getCmd (thisLine) 
paulson@16475
   266
	       (*********************************************************)
paulson@16475
   267
	       (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
paulson@16475
   268
	       (* i.e. put back into tuple format                       *)
paulson@16475
   269
	       (*********************************************************)
paulson@16475
   270
	   in
paulson@16475
   271
	     (*TextIO.output (toParentStr, thisCmd); 
paulson@16475
   272
	       TextIO.flushOut toParentStr;*)
paulson@16475
   273
	       getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
paulson@16475
   274
	   end
paulson@16475
   275
  end
paulson@16475
   276
	    
quigley@16357
   277
                                                                  
quigley@15642
   278
(**************************************************************)
quigley@15642
   279
(*  Get Io-descriptor for polling of an input stream          *)
quigley@15642
   280
(**************************************************************)
quigley@15642
   281
quigley@15642
   282
fun getInIoDesc someInstr = 
quigley@15642
   283
    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
paulson@15702
   284
        val _ = TextIO.output (TextIO.stdOut, buf)
quigley@15642
   285
        val ioDesc = 
quigley@15642
   286
	    case rd
quigley@15642
   287
	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
quigley@15642
   288
	       | _ => NONE
quigley@15642
   289
     in (* since getting the reader will have terminated the stream, we need
quigley@15642
   290
	 * to build a new stream. *)
quigley@15642
   291
	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
quigley@15642
   292
	ioDesc
quigley@15642
   293
    end
quigley@15642
   294
quigley@15642
   295
quigley@15642
   296
(*************************************)
quigley@15642
   297
(*  Set up a Watcher Process         *)
quigley@15642
   298
(*************************************)
quigley@15642
   299
paulson@16061
   300
fun setupWatcher (thm,clause_arr, num_of_clauses) = 
paulson@16061
   301
  let
paulson@16061
   302
    (** pipes for communication between parent and watcher **)
paulson@16061
   303
    val p1 = Posix.IO.pipe ()
paulson@16061
   304
    val p2 = Posix.IO.pipe ()
paulson@16061
   305
    fun closep () = (
paulson@16061
   306
	  Posix.IO.close (#outfd p1); 
paulson@16061
   307
	  Posix.IO.close (#infd p1);
paulson@16061
   308
	  Posix.IO.close (#outfd p2); 
paulson@16061
   309
	  Posix.IO.close (#infd p2)
paulson@16061
   310
	)
paulson@16061
   311
    (***********************************************************)
paulson@16061
   312
    (****** fork a watcher process and get it set up and going *)
paulson@16061
   313
    (***********************************************************)
paulson@16061
   314
    fun startWatcher (procList) =
paulson@17234
   315
     (case  Posix.Process.fork() (***************************************)
paulson@17234
   316
      of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
paulson@17234
   317
				    (***************************************)
paulson@16061
   318
paulson@17234
   319
				      (*************************)
paulson@17234
   320
       | NONE => let                  (* child - i.e. watcher  *)
paulson@17234
   321
	   val oldchildin = #infd p1  (*************************)
paulson@17234
   322
	   val fromParent = Posix.FileSys.wordToFD 0w0
paulson@17234
   323
	   val oldchildout = #outfd p2
paulson@17234
   324
	   val toParent = Posix.FileSys.wordToFD 0w1
paulson@17234
   325
	   val fromParentIOD = Posix.FileSys.fdToIOD fromParent
paulson@17234
   326
	   val fromParentStr = openInFD ("_exec_in_parent", fromParent)
paulson@17234
   327
	   val toParentStr = openOutFD ("_exec_out_parent", toParent)
paulson@17234
   328
	   val sign = sign_of_thm thm
paulson@17234
   329
	   val prems = prems_of thm
paulson@17234
   330
	   val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
paulson@17234
   331
	   val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
paulson@17234
   332
	  (* tracing *)
paulson@17234
   333
	 (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
paulson@17234
   334
	   val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
paulson@17234
   335
	   val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
paulson@17234
   336
	   val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
paulson@17234
   337
	   val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
paulson@17234
   338
	   val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
paulson@17234
   339
		    *)
paulson@17234
   340
	   (*val goalstr = string_of_thm (the_goal)
paulson@17234
   341
	    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher")));  
paulson@17234
   342
	   val _ = TextIO.output (outfile,goalstr )
paulson@17234
   343
	   val _ =  TextIO.closeOut outfile*)
paulson@17234
   344
	   fun killChildren [] = ()
paulson@17234
   345
	|      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
quigley@15642
   346
paulson@17234
   347
	 (*************************************************************)
paulson@17234
   348
	 (* take an instream and poll its underlying reader for input *)
paulson@17234
   349
	 (*************************************************************)
quigley@15642
   350
paulson@17234
   351
	 fun pollParentInput () = 
paulson@17234
   352
	    let val pd = OS.IO.pollDesc (fromParentIOD)
paulson@17234
   353
	    in 
paulson@17234
   354
	      if (isSome pd ) then 
paulson@17234
   355
		  let val pd' = OS.IO.pollIn (valOf pd)
paulson@17234
   356
		      val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
paulson@17234
   357
		      val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
paulson@17234
   358
			("In parent_poll\n")	
paulson@17234
   359
		  in
paulson@17234
   360
		     if null pdl 
paulson@17234
   361
		     then
paulson@17234
   362
			NONE
paulson@17234
   363
		     else if (OS.IO.isIn (hd pdl)) 
paulson@17234
   364
			  then SOME (getCmds (toParentStr, fromParentStr, []))
paulson@17234
   365
			  else NONE
paulson@17234
   366
		  end
paulson@17234
   367
		else NONE
paulson@17234
   368
	    end
paulson@17234
   369
		 
paulson@17234
   370
	  fun pollChildInput (fromStr) = 
paulson@17234
   371
	    let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
paulson@17234
   372
			  ("In child_poll\n")
paulson@17234
   373
		val iod = getInIoDesc fromStr
paulson@17234
   374
	    in 
paulson@17234
   375
	      if isSome iod 
paulson@17234
   376
	      then 
paulson@17234
   377
		let val pd = OS.IO.pollDesc (valOf iod)
paulson@17234
   378
		in 
paulson@17234
   379
		if (isSome pd ) then 
paulson@17234
   380
		    let val pd' = OS.IO.pollIn (valOf pd)
paulson@17234
   381
			val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
paulson@17234
   382
		    in
paulson@17234
   383
		       if null pdl 
paulson@17234
   384
		       then
paulson@17234
   385
			 ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
paulson@17234
   386
			  ("Null pdl \n");NONE)
paulson@17234
   387
		       else if (OS.IO.isIn (hd pdl)) 
paulson@17216
   388
			    then
paulson@17234
   389
				(let val inval =  (TextIO.inputLine fromStr)
paulson@17234
   390
				     val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
paulson@17234
   391
				 in
paulson@17234
   392
				       SOME inval
paulson@17234
   393
				 end)
paulson@17234
   394
			    else
paulson@17234
   395
				  ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
paulson@17234
   396
			  ("Null pdl \n");NONE)
paulson@17234
   397
		    end
paulson@17234
   398
		  else  NONE
paulson@17234
   399
		  end
paulson@17234
   400
	      else NONE
paulson@17234
   401
	end
quigley@15642
   402
quigley@15642
   403
paulson@17234
   404
	(****************************************************************************)
paulson@17234
   405
	(* Check all vampire processes currently running for output                 *)
paulson@17234
   406
	(****************************************************************************) 
paulson@17234
   407
						   (*********************************)
paulson@17234
   408
	 fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
paulson@17234
   409
						   (*********************************)
paulson@17234
   410
	 |   checkChildren ((childProc::otherChildren), toParentStr) = 
paulson@17234
   411
	       let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
paulson@17305
   412
			      ("In check child, length of queue:"^
paulson@17305
   413
			       (string_of_int (length (childProc::otherChildren)))^"\n")
paulson@17234
   414
		   val (childInput,childOutput) =  cmdstreamsOf childProc
paulson@17234
   415
		   val child_handle= cmdchildHandle childProc
paulson@17234
   416
		   (* childCmd is the .dfg file that the problem is in *)
paulson@17234
   417
		   val childCmd = fst(snd (cmdchildInfo childProc))
paulson@17234
   418
		   val _ = File.append (File.tmp_path (Path.basic "child_command")) 
paulson@17234
   419
			      (childCmd^"\n")
paulson@17234
   420
		   (* now get the number of the subgoal from the filename *)
paulson@17305
   421
		   val path_parts = String.tokens(fn c => c = #"/") childCmd
paulson@17305
   422
		   val digits = String.translate 
paulson@17305
   423
		                  (fn c => if Char.isDigit c then str c else "")
paulson@17305
   424
		                  (List.last path_parts);
paulson@17305
   425
		   val sg_num = (case Int.fromString digits of SOME n => n
paulson@17305
   426
                                  | NONE => error ("Watcher could not read subgoal nunber: " ^ childCmd));
quigley@16520
   427
paulson@17234
   428
		   val childIncoming = pollChildInput childInput
paulson@17234
   429
		   val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) 
paulson@17234
   430
			      ("finished polling child \n")
paulson@17234
   431
		   val parentID = Posix.ProcEnv.getppid()
paulson@17234
   432
		   val prover = cmdProver childProc
paulson@17234
   433
		   val thmstring = cmdThm childProc
paulson@17234
   434
		   val sign = sign_of_thm thm
paulson@17234
   435
		   val prems = prems_of thm
paulson@17234
   436
		   val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
paulson@17234
   437
		   val _ = warning("subgoals forked to checkChildren: "^prems_string)
paulson@17234
   438
		   val goalstring = cmdGoal childProc							
paulson@17234
   439
		   val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
paulson@17234
   440
			      (prover^thmstring^goalstring^childCmd^"\n")
paulson@17234
   441
	       in 
paulson@17234
   442
		 if (isSome childIncoming) 
paulson@17234
   443
		 then 
paulson@17234
   444
		     (* check here for prover label on child*)
paulson@17234
   445
		     let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) 
paulson@17234
   446
				("subgoals forked to checkChildren:"^
paulson@17234
   447
				prems_string^prover^thmstring^goalstring^childCmd) 
paulson@17234
   448
			 val childDone = (case prover of
quigley@17235
   449
			     "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )     
quigley@17235
   450
                              | "E" => (EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )              
paulson@17234
   451
			    |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
paulson@17234
   452
		      in
paulson@17234
   453
		       if childDone      (**********************************************)
paulson@17234
   454
		       then (* child has found a proof and transferred it *)
paulson@17234
   455
			  (* Remove this child and go on to check others*)
paulson@17234
   456
			  (**********************************************)
paulson@17234
   457
			  (Unix.reap child_handle;
paulson@17234
   458
			   checkChildren(otherChildren, toParentStr))
paulson@17234
   459
		       else 
paulson@17234
   460
			  (**********************************************)
paulson@17234
   461
			  (* Keep this child and go on to check others  *)
paulson@17234
   462
			  (**********************************************)
paulson@17234
   463
			 (childProc::(checkChildren (otherChildren, toParentStr)))
paulson@16061
   464
		    end
paulson@17234
   465
		  else
paulson@17234
   466
		    (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
paulson@17234
   467
		     childProc::(checkChildren (otherChildren, toParentStr)))
paulson@17234
   468
	       end
quigley@15642
   469
paulson@17234
   470
	
paulson@17234
   471
     (********************************************************************)                  
paulson@17234
   472
     (* call resolution processes                                        *)
paulson@17234
   473
     (* settings should be a list of strings                             *)
paulson@17234
   474
     (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
paulson@17234
   475
     (* takes list of (string, string, string list, string)list proclist *)
paulson@17234
   476
     (********************************************************************)
quigley@15642
   477
quigley@16039
   478
paulson@16061
   479
(*** add subgoal id num to this *)
paulson@17234
   480
	fun execCmds  [] procList = procList
paulson@17234
   481
	|   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =             let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child"))  ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
paulson@17234
   482
	  in 
paulson@17234
   483
	    if (prover = "spass") 
paulson@17234
   484
	    then 
paulson@17234
   485
	      let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
paulson@17234
   486
		       (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
paulson@17234
   487
		  val (instr, outstr) = Unix.streamsOf childhandle
paulson@17234
   488
		  val newProcList =    (((CMDPROC{
paulson@17234
   489
				       prover = prover,
paulson@17234
   490
				       cmd = file,
paulson@17234
   491
				       thmstring = thmstring,
paulson@17234
   492
				       goalstring = goalstring,
paulson@17234
   493
				       proc_handle = childhandle,
paulson@17234
   494
				       instr = instr,
paulson@17234
   495
				       outstr = outstr })::procList))
paulson@17234
   496
		   val _ = File.append (File.tmp_path (Path.basic "exec_child"))  
paulson@17234
   497
			("\nexecuting command for goal:\n"^
paulson@17234
   498
			 goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
paulson@17234
   499
	      in
paulson@17234
   500
		 Posix.Process.sleep (Time.fromSeconds 1);
paulson@17234
   501
		 execCmds cmds newProcList
paulson@17234
   502
	      end
paulson@17234
   503
	    else 
paulson@17234
   504
	      let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
paulson@17234
   505
		       (Unix.execute(proverCmd, (settings@[file])))
paulson@17234
   506
		  val (instr, outstr) = Unix.streamsOf childhandle
paulson@17234
   507
		  
paulson@17234
   508
		  val newProcList = (CMDPROC{
paulson@17234
   509
				       prover = prover,
paulson@17234
   510
				       cmd = file,
paulson@17234
   511
				       thmstring = thmstring,
paulson@17234
   512
				       goalstring = goalstring,
paulson@17234
   513
				       proc_handle = childhandle,
paulson@17234
   514
				       instr = instr,
paulson@17234
   515
				       outstr = outstr }) :: procList
paulson@17234
   516
     
paulson@17234
   517
		  val _ = File.append (File.tmp_path (Path.basic "exec_child")) 
paulson@17234
   518
			    ("executing command for goal:\n"^
paulson@17234
   519
			     goalstring^proverCmd^(concat settings)^file^
paulson@17234
   520
			     " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
paulson@17234
   521
	      in
paulson@17234
   522
		Posix.Process.sleep (Time.fromSeconds 1); 
paulson@17234
   523
		execCmds cmds newProcList
paulson@17234
   524
	      end
paulson@17234
   525
	   end
quigley@15642
   526
quigley@16039
   527
paulson@17234
   528
     (****************************************)                  
paulson@17234
   529
     (* call resolution processes remotely   *)
paulson@17234
   530
     (* settings should be a list of strings *)
paulson@17234
   531
     (* e.g. ["-t 300", "-m 100000"]         *)
paulson@17234
   532
     (****************************************)
paulson@16061
   533
paulson@17234
   534
      (*  fun execRemoteCmds  [] procList = procList
paulson@17234
   535
	|   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
paulson@17234
   536
				  let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
paulson@17234
   537
				      in
paulson@17234
   538
					   execRemoteCmds  cmds newProcList
paulson@17234
   539
				      end
quigley@16039
   540
*)
quigley@15642
   541
paulson@17234
   542
	fun printList (outStr, []) = ()
paulson@17234
   543
	|   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
quigley@15642
   544
quigley@15642
   545
paulson@17234
   546
     (**********************************************)                  
paulson@17234
   547
     (* Watcher Loop                               *)
paulson@17234
   548
     (**********************************************)
paulson@16061
   549
paulson@17234
   550
	 fun keepWatching (toParentStr, fromParentStr,procList) = 
paulson@17234
   551
	   let fun loop (procList) =  
paulson@17234
   552
		let val _ = Posix.Process.sleep (Time.fromMilliseconds 200)
paulson@17234
   553
		    val cmdsFromIsa = pollParentInput ()
paulson@17234
   554
		    fun killchildHandler (n:int)  = 
paulson@17234
   555
			  (TextIO.output(toParentStr, "Killing child proof processes!\n");
paulson@17234
   556
			   TextIO.flushOut toParentStr;
paulson@17234
   557
			   killChildren (map (cmdchildHandle) procList);
paulson@17234
   558
			   ())
paulson@17234
   559
		in 
paulson@17234
   560
		   (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
paulson@17234
   561
								      (**********************************)
paulson@17234
   562
		   if (isSome cmdsFromIsa) 
paulson@17234
   563
		   then (*  deal with input from Isabelle *)
paulson@17234
   564
		     if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
paulson@17234
   565
		     then 
paulson@17234
   566
		       let val child_handles = map cmdchildHandle procList 
paulson@17234
   567
		       in
paulson@17234
   568
			  killChildren child_handles;
paulson@17234
   569
			  (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)    
paulson@17234
   570
			  loop ([])
paulson@17234
   571
		       end
paulson@17234
   572
		     else
paulson@17234
   573
		       if ((length procList)<10)    (********************)
paulson@17234
   574
		       then                        (* Execute locally  *)
paulson@17234
   575
			 let 
paulson@17234
   576
			   val newProcList = execCmds (valOf cmdsFromIsa) procList
paulson@17234
   577
			   val parentID = Posix.ProcEnv.getppid()
paulson@17234
   578
			      val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
paulson@17234
   579
			   val newProcList' =checkChildren (newProcList, toParentStr) 
quigley@16357
   580
paulson@17234
   581
			   val _ = warning("off to keep watching...")
paulson@17234
   582
			  val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
paulson@17234
   583
			 in
paulson@17234
   584
			   loop (newProcList') 
paulson@17234
   585
			 end
paulson@17234
   586
		       else  (* Execute remotely              *)
paulson@17234
   587
			     (* (actually not remote for now )*)
paulson@17234
   588
			 let 
paulson@17234
   589
			   val newProcList = execCmds (valOf cmdsFromIsa) procList
paulson@17234
   590
			   val parentID = Posix.ProcEnv.getppid()
paulson@17234
   591
			   val newProcList' =checkChildren (newProcList, toParentStr) 
paulson@17234
   592
			 in
paulson@17234
   593
			   loop (newProcList') 
paulson@17234
   594
			 end
paulson@17234
   595
		   else (* No new input from Isabelle *)
paulson@17234
   596
		     let val newProcList = checkChildren ((procList), toParentStr)
paulson@17234
   597
		     in
paulson@17234
   598
		      (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
paulson@17234
   599
		       loop (newProcList)
paulson@17234
   600
		     end
paulson@17234
   601
		 end
paulson@17234
   602
	   in  
paulson@17234
   603
	       loop (procList)
paulson@17234
   604
	   end
paulson@17234
   605
	   
quigley@15642
   606
paulson@17234
   607
	   in
paulson@17234
   608
	    (***************************)
paulson@17234
   609
	    (*** Sort out pipes ********)
paulson@17234
   610
	    (***************************)
quigley@15642
   611
paulson@17234
   612
	     Posix.IO.close (#outfd p1);
paulson@17234
   613
	     Posix.IO.close (#infd p2);
paulson@17234
   614
	     Posix.IO.dup2{old = oldchildin, new = fromParent};
paulson@17234
   615
	     Posix.IO.close oldchildin;
paulson@17234
   616
	     Posix.IO.dup2{old = oldchildout, new = toParent};
paulson@17234
   617
	     Posix.IO.close oldchildout;
paulson@17234
   618
paulson@17234
   619
	     (***************************)
paulson@17234
   620
	     (* start the watcher loop  *)
paulson@17234
   621
	     (***************************)
paulson@17234
   622
	     keepWatching (toParentStr, fromParentStr, procList);
paulson@17234
   623
	     (****************************************************************************)
paulson@17234
   624
(* fake return value - actually want the watcher to loop until killed *)
paulson@17234
   625
	     (****************************************************************************)
paulson@17234
   626
	     Posix.Process.wordToPid 0w0
paulson@17234
   627
	   end);
paulson@17234
   628
     (* end case *)
quigley@15642
   629
quigley@15642
   630
paulson@16061
   631
    val _ = TextIO.flushOut TextIO.stdOut
quigley@15642
   632
paulson@16061
   633
    (*******************************)
paulson@16061
   634
    (***  set watcher going ********)
paulson@16061
   635
    (*******************************)
quigley@15642
   636
paulson@16061
   637
    val procList = []
paulson@16061
   638
    val pid = startWatcher (procList)
paulson@16061
   639
    (**************************************************)
paulson@16061
   640
    (* communication streams to watcher               *)
paulson@16061
   641
    (**************************************************)
quigley@15642
   642
paulson@16061
   643
    val instr = openInFD ("_exec_in", #infd p2)
paulson@16061
   644
    val outstr = openOutFD ("_exec_out", #outfd p1)
paulson@16061
   645
    
paulson@16061
   646
    in
paulson@16061
   647
     (*******************************)
paulson@16061
   648
     (* close the child-side fds    *)
paulson@16061
   649
     (*******************************)
paulson@16061
   650
      Posix.IO.close (#outfd p2);
paulson@16061
   651
      Posix.IO.close (#infd p1);
paulson@16061
   652
      (* set the fds close on exec *)
paulson@16061
   653
      Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
paulson@16061
   654
      Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
paulson@16061
   655
       
paulson@16061
   656
     (*******************************)
paulson@16061
   657
     (* return value                *)
paulson@16061
   658
     (*******************************)
paulson@16061
   659
      PROC{pid = pid,
paulson@16061
   660
	instr = instr,
paulson@16061
   661
	outstr = outstr
paulson@16061
   662
      }
paulson@16061
   663
   end;
quigley@15642
   664
quigley@15642
   665
quigley@15642
   666
quigley@15642
   667
(**********************************************************)
quigley@15642
   668
(* Start a watcher and set up signal handlers             *)
quigley@15642
   669
(**********************************************************)
quigley@16039
   670
quigley@16039
   671
fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
quigley@16039
   672
quigley@16039
   673
fun reapWatcher(pid, instr, outstr) =
paulson@17216
   674
  let val u = TextIO.closeIn instr;
paulson@17216
   675
      val u = TextIO.closeOut outstr;
paulson@17216
   676
      val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
paulson@17216
   677
  in
paulson@17216
   678
	  status
paulson@16100
   679
  end
quigley@15642
   680
paulson@17216
   681
fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) =
paulson@17216
   682
 let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
paulson@17231
   683
     val streams = snd mychild
paulson@17216
   684
     val childin = fst streams
paulson@17216
   685
     val childout = snd streams
paulson@17216
   686
     val childpid = fst mychild
paulson@17216
   687
     val sign = sign_of_thm thm
paulson@17216
   688
     val prems = prems_of thm
paulson@17216
   689
     val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
paulson@17216
   690
     val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
paulson@17216
   691
     fun vampire_proofHandler (n) =
paulson@17216
   692
	(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17216
   693
	 VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))               
paulson@17216
   694
     fun spass_proofHandler (n) = (
paulson@17216
   695
       let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
paulson@17216
   696
	   val _ = TextIO.output (outfile, ("In signal handler now\n"))
paulson@17216
   697
	   val _ =  TextIO.closeOut outfile
paulson@17216
   698
	   val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
paulson@17216
   699
	   val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
paulson@17216
   700
   
paulson@17216
   701
	   val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
paulson@17216
   702
	   val _ =  TextIO.closeOut outfile
paulson@17216
   703
       in (* if a proof has been found and sent back as a reconstruction proof *)
paulson@17231
   704
	 if substring (reconstr, 0,1) = "["
paulson@17216
   705
	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17216
   706
	       Recon_Transfer.apply_res_thm reconstr goalstring;
paulson@17216
   707
	       Pretty.writeln(Pretty.str  (oct_char "361"));
paulson@17216
   708
	       
paulson@17216
   709
	       goals_being_watched := ((!goals_being_watched) - 1);
paulson@17216
   710
       
paulson@17231
   711
	       if (!goals_being_watched) = 0
paulson@17216
   712
	       then 
paulson@17231
   713
		  let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found"))
paulson@17231
   714
                                   ("Reaping a watcher, goals watched is: "^
paulson@17231
   715
                                    (string_of_int (!goals_being_watched))^"\n")
paulson@17216
   716
		   in
paulson@17216
   717
		       killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
paulson@17231
   718
		   end
paulson@17216
   719
		else () )
paulson@17216
   720
	 (* if there's no proof, but a message from Spass *)
paulson@17231
   721
	 else if substring (reconstr, 0,5) = "SPASS"
paulson@17216
   722
	 then (goals_being_watched := (!goals_being_watched) -1;
paulson@17216
   723
	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17216
   724
	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
paulson@17216
   725
	       Pretty.writeln(Pretty.str  (oct_char "361"));
paulson@17216
   726
	       if (!goals_being_watched = 0)
paulson@17216
   727
	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
paulson@17216
   728
	              ("Reaping a watcher, goals watched is: " ^
paulson@17216
   729
	                 (string_of_int (!goals_being_watched))^"\n");
paulson@17216
   730
	             killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
paulson@17216
   731
		else () ) 
paulson@17216
   732
	(* print out a list of rules used from clasimpset*)
paulson@17231
   733
	 else if substring (reconstr, 0,5) = "Rules"
paulson@17216
   734
	 then (goals_being_watched := (!goals_being_watched) -1;
paulson@17216
   735
	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17216
   736
	       Pretty.writeln(Pretty.str (goalstring^reconstr));
paulson@17216
   737
	       Pretty.writeln(Pretty.str  (oct_char "361"));
paulson@17216
   738
	       if (!goals_being_watched = 0)
paulson@17216
   739
	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
paulson@17216
   740
	              ("Reaping a watcher, goals watched is: " ^
paulson@17216
   741
	                 (string_of_int (!goals_being_watched))^"\n");
paulson@17216
   742
	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
paulson@17216
   743
		     )
paulson@17216
   744
	       else () )
paulson@17216
   745
	  (* if proof translation failed *)
paulson@17231
   746
	 else if substring (reconstr, 0,5) = "Proof"
paulson@17216
   747
	 then (goals_being_watched := (!goals_being_watched) -1;
paulson@17216
   748
	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17216
   749
	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
paulson@17216
   750
	       Pretty.writeln(Pretty.str  (oct_char "361"));
paulson@17216
   751
	       if (!goals_being_watched = 0)
paulson@17216
   752
	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
paulson@17216
   753
	              ("Reaping a watcher, goals watched is: " ^
paulson@17216
   754
	                 (string_of_int (!goals_being_watched))^"\n");
paulson@17216
   755
	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
paulson@17216
   756
		     )
paulson@17216
   757
	       else () )
quigley@15642
   758
paulson@17231
   759
	 else if substring (reconstr, 0,1) = "%"
paulson@17216
   760
	 then (goals_being_watched := (!goals_being_watched) -1;
paulson@17216
   761
	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17216
   762
	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
paulson@17216
   763
	       Pretty.writeln(Pretty.str  (oct_char "361"));
paulson@17216
   764
	       if (!goals_being_watched = 0)
paulson@17216
   765
	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
paulson@17216
   766
	              ("Reaping a watcher, goals watched is: " ^
paulson@17216
   767
	                 (string_of_int (!goals_being_watched))^"\n");
paulson@17216
   768
	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
paulson@17216
   769
		     )
paulson@17216
   770
	       else () )
paulson@17216
   771
paulson@17216
   772
	 else  (* add something here ?*)
paulson@17216
   773
	      (goals_being_watched := (!goals_being_watched) -1;
paulson@17216
   774
	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
paulson@17231
   775
	       Pretty.writeln(Pretty.str ("Ran out of options in handler"));
paulson@17231
   776
	       Pretty.writeln(Pretty.str  (oct_char "361"));
paulson@17231
   777
	       if (!goals_being_watched = 0)
paulson@17231
   778
	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
paulson@17231
   779
		     ("Reaping a watcher, goals watched is: " ^
paulson@17231
   780
			(string_of_int (!goals_being_watched))^"\n");
paulson@17231
   781
		    killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
paulson@17231
   782
		    )
paulson@17231
   783
	       else () )
paulson@17216
   784
       end)
paulson@17216
   785
paulson@17216
   786
 in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
paulson@17216
   787
    IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
paulson@17216
   788
    (childin, childout, childpid)
paulson@17216
   789
paulson@17216
   790
  end
quigley@15642
   791
quigley@15642
   792
end (* structure Watcher *)