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