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