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