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