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