src/HOL/Tools/ATP/watcher.ML
author quigley
Mon Apr 04 18:39:45 2005 +0200 (2005-04-04)
changeset 15652 a9d65894962e
parent 15642 028059faa963
child 15658 2edb384bf61f
permissions -rw-r--r--
CVSfj


-------------------------------------------------------------------
---------------------------------------------------------------
Temporarily added until res_axioms.ML is altered.
quigley@15642
     1
quigley@15642
     2
 (*  Title:      Watcher.ML
quigley@15642
     3
     Author:     Claire Quigley
quigley@15642
     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";
quigley@15642
    18
use "SpassCommunication";
quigley@15642
    19
use "modUnix";*)
quigley@15642
    20
(*use "/homes/clq20/Jia_Code/TransStartIsar";*)
quigley@15642
    21
quigley@15652
    22
use "~~/src/HOL/Tools/ATP/VampireCommunication.ML";
quigley@15652
    23
use "~~/src/HOL/Tools/ATP/SpassCommunication.ML";
quigley@15642
    24
quigley@15642
    25
quigley@15652
    26
use "~~/src/HOL/Tools/ATP/modUnix.ML";
quigley@15642
    27
quigley@15642
    28
quigley@15642
    29
structure Watcher: WATCHER =
quigley@15642
    30
  struct
quigley@15642
    31
quigley@15642
    32
fun fst (a,b) = a;
quigley@15642
    33
fun snd (a,b) = b;
quigley@15642
    34
quigley@15642
    35
val goals_being_watched = ref 0;
quigley@15642
    36
quigley@15642
    37
fun remove y [] = []
quigley@15642
    38
|   remove y (x::xs) = (if y = x 
quigley@15642
    39
                       then 
quigley@15642
    40
                           remove y xs 
quigley@15642
    41
                       else ((x::(remove y  xs))))
quigley@15642
    42
quigley@15642
    43
quigley@15642
    44
quigley@15642
    45
fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
quigley@15642
    46
quigley@15642
    47
(********************************************************************************************)
quigley@15642
    48
(*  takes a list of arguments and sends them individually to the watcher process by pipe    *)
quigley@15642
    49
(********************************************************************************************)
quigley@15642
    50
quigley@15642
    51
fun outputArgs (toWatcherStr, []) = ()
quigley@15642
    52
|   outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); 
quigley@15642
    53
                                          TextIO.flushOut toWatcherStr;
quigley@15642
    54
                                         outputArgs (toWatcherStr, xs))
quigley@15642
    55
quigley@15642
    56
(********************************************************************************)
quigley@15642
    57
(*    gets individual args from instream and concatenates them into a list      *)
quigley@15642
    58
(********************************************************************************)
quigley@15642
    59
quigley@15642
    60
fun getArgs (fromParentStr, toParentStr,ys) =  let 
quigley@15642
    61
                                       val thisLine = TextIO.input fromParentStr
quigley@15642
    62
                                    in
quigley@15642
    63
                                        ((ys@[thisLine]))
quigley@15642
    64
                                    end
quigley@15642
    65
quigley@15642
    66
(********************************************************************************)
quigley@15642
    67
(*  Remove the \n character from the end of each filename                       *)
quigley@15642
    68
(********************************************************************************)
quigley@15642
    69
quigley@15642
    70
fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
quigley@15642
    71
                    in
quigley@15642
    72
quigley@15642
    73
                        if (String.isPrefix "\n"  (implode backList )) 
quigley@15642
    74
                        then 
quigley@15642
    75
                             (implode (rev ((tl backList))))
quigley@15642
    76
                        else
quigley@15642
    77
                           (cmdStr)
quigley@15642
    78
                    end
quigley@15642
    79
                            
quigley@15642
    80
(********************************************************************************)
quigley@15642
    81
(*  Send request to Watcher for a vampire to be called for filename in arg      *)
quigley@15642
    82
(********************************************************************************)
quigley@15642
    83
                    
quigley@15642
    84
fun callResProver (toWatcherStr,  arg) = (sendOutput (toWatcherStr, arg^"\n"); 
quigley@15642
    85
                                     TextIO.flushOut toWatcherStr
quigley@15642
    86
                                    
quigley@15642
    87
                                     )
quigley@15642
    88
quigley@15642
    89
(*****************************************************************************************)
quigley@15642
    90
(*  Send request to Watcher for multiple provers to be called for filenames in arg      *)
quigley@15642
    91
(*****************************************************************************************)
quigley@15642
    92
quigley@15642
    93
(* need to modify to send over hyps file too *)
quigley@15642
    94
fun callResProvers (toWatcherStr,  []) = (sendOutput (toWatcherStr, "End of calls\n"); 
quigley@15642
    95
                                     TextIO.flushOut toWatcherStr)
quigley@15642
    96
|   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,probfile)::args) =
quigley@15642
    97
                                                     let 
quigley@15642
    98
                                                        val dfg_dir = File.tmp_path (Path.basic "dfg");
quigley@15642
    99
                                                        (* need to check here if the directory exists and, if not, create it*)
quigley@15652
   100
                                                         val  outfile = TextIO.openAppend("thmstring_in_watcher");                                                                                    
quigley@15642
   101
                                                         val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
quigley@15642
   102
                                                         val _ =  TextIO.closeOut outfile
quigley@15642
   103
                                                         val dfg_create =if File.exists dfg_dir 
quigley@15642
   104
                                                                         then
quigley@15642
   105
                                                                             ()
quigley@15642
   106
                                                                         else
quigley@15642
   107
                                                                               File.mkdir dfg_dir; 
quigley@15642
   108
                                                         val probID = last(explode probfile)
quigley@15642
   109
                                                         val dfg_path = File.sysify_path dfg_dir;
quigley@15642
   110
                                                         val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v2.6.0/TPTP2X/tptp2X", ["-fdfg "^probfile^" -d "^dfg_path])
quigley@15642
   111
                                                       (*val _ = Posix.Process.wait ()*)
quigley@15642
   112
                                                       (*val _ =Unix.reap exec_tptp2x*)
quigley@15642
   113
                                                         val newfile = dfg_path^"/prob"^(probID)^".dfg"
quigley@15642
   114
                                       
quigley@15642
   115
                                                      in   
quigley@15642
   116
                                                         goals_being_watched := (!goals_being_watched) + 1;
quigley@15642
   117
                                                         OS.Process.sleep(Time.fromSeconds 1); 
quigley@15642
   118
                                                         (warning("dfg file is: "^newfile));
quigley@15642
   119
                                                         sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
quigley@15642
   120
                                                         TextIO.flushOut toWatcherStr;
quigley@15642
   121
                                                         Unix.reap exec_tptp2x; 
quigley@15642
   122
                                                         
quigley@15642
   123
                                                         callResProvers (toWatcherStr,args)
quigley@15642
   124
                                           
quigley@15642
   125
                                                     end
quigley@15642
   126
quigley@15642
   127
fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
quigley@15642
   128
                                     
quigley@15642
   129
|   callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings, file)::args) =
quigley@15642
   130
                                            ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^file^"\n")
quigley@15642
   131
                                            
quigley@15642
   132
                                           )
quigley@15642
   133
 
quigley@15642
   134
(**************************************************************)
quigley@15642
   135
(* Send message to watcher to kill currently running vampires *)
quigley@15642
   136
(**************************************************************)
quigley@15642
   137
quigley@15642
   138
fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 
quigley@15642
   139
                            TextIO.flushOut toWatcherStr)
quigley@15642
   140
quigley@15642
   141
quigley@15642
   142
quigley@15642
   143
(**************************************************************)
quigley@15642
   144
(* Remove \n token from a vampire goal filename and extract   *)
quigley@15642
   145
(* prover, proverCmd, settings and file from input string     *)
quigley@15642
   146
(**************************************************************)
quigley@15642
   147
quigley@15642
   148
quigley@15642
   149
 fun takeUntil ch [] res  = (res, [])
quigley@15642
   150
 |   takeUntil ch (x::xs) res = if   x = ch 
quigley@15642
   151
                                then
quigley@15642
   152
                                     (res, xs)
quigley@15642
   153
                                else
quigley@15642
   154
                                     takeUntil ch xs (res@[x])
quigley@15642
   155
quigley@15642
   156
 fun getSettings [] settings = settings
quigley@15642
   157
|    getSettings (xs) settings = let val (set, rest ) = takeUntil "%" xs []
quigley@15642
   158
                                 in
quigley@15642
   159
                                     getSettings rest (settings@[(implode set)])
quigley@15642
   160
                                 end
quigley@15642
   161
quigley@15642
   162
fun separateFields str = let val (prover, rest) = takeUntil "*" str []
quigley@15642
   163
                              val prover = implode prover
quigley@15642
   164
                              val (thmstring, rest) =  takeUntil "*" rest []
quigley@15642
   165
                              val thmstring = implode thmstring
quigley@15642
   166
                              val (goalstring, rest) =  takeUntil "*" rest []
quigley@15642
   167
                              val goalstring = implode goalstring
quigley@15642
   168
                              val (proverCmd, rest ) =  takeUntil "*" rest []
quigley@15642
   169
                              val proverCmd = implode proverCmd
quigley@15642
   170
                              
quigley@15642
   171
                              val (settings, rest) =  takeUntil "*" rest []
quigley@15642
   172
                              val settings = getSettings settings []
quigley@15642
   173
                              val (file, rest) =  takeUntil "*" rest []
quigley@15642
   174
                              val file = implode file
quigley@15642
   175
                              val  outfile = TextIO.openOut("sep_comms");                                                                                    
quigley@15642
   176
                              val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^file) )
quigley@15642
   177
                              val _ =  TextIO.closeOut outfile
quigley@15642
   178
                              
quigley@15642
   179
                          in
quigley@15642
   180
                             (prover,thmstring,goalstring, proverCmd, settings, file)
quigley@15642
   181
                          end
quigley@15642
   182
quigley@15642
   183
 
quigley@15642
   184
quigley@15642
   185
 fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
quigley@15642
   186
                     in
quigley@15642
   187
quigley@15642
   188
                         if (String.isPrefix "\n"  (implode backList )) 
quigley@15642
   189
                         then 
quigley@15642
   190
                             separateFields ((rev ((tl backList))))
quigley@15642
   191
                         else
quigley@15642
   192
                           (separateFields (explode cmdStr))
quigley@15642
   193
                     end
quigley@15642
   194
                      
quigley@15642
   195
quigley@15642
   196
fun getProofCmd (a,b,c,d,e,f) = d
quigley@15642
   197
quigley@15642
   198
quigley@15642
   199
(**************************************************************)
quigley@15642
   200
(* Get commands from Isabelle                                 *)
quigley@15642
   201
(**************************************************************)
quigley@15642
   202
quigley@15642
   203
fun getCmds (toParentStr,fromParentStr, cmdList) = 
quigley@15642
   204
                                       let val thisLine = TextIO.inputLine fromParentStr 
quigley@15642
   205
                                       in
quigley@15642
   206
                                          (if (thisLine = "End of calls\n") 
quigley@15642
   207
                                           then 
quigley@15642
   208
                                              (cmdList)
quigley@15642
   209
                                           else if (thisLine = "Kill children\n") 
quigley@15642
   210
                                                then 
quigley@15642
   211
                                                    (   TextIO.output (toParentStr,thisLine ); 
quigley@15642
   212
                                                        TextIO.flushOut toParentStr;
quigley@15642
   213
                                                      (("","","","Kill children",[],"")::cmdList)
quigley@15642
   214
                                                     )
quigley@15642
   215
                                              else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
quigley@15642
   216
                                                    in
quigley@15642
   217
                                                      (*TextIO.output (toParentStr, thisCmd); 
quigley@15642
   218
                                                        TextIO.flushOut toParentStr;*)
quigley@15642
   219
                                                        getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
quigley@15642
   220
                                                    end
quigley@15642
   221
                                                    )
quigley@15642
   222
                                            )
quigley@15642
   223
                                        end
quigley@15642
   224
                                    
quigley@15642
   225
                                    
quigley@15642
   226
(**************************************************************)
quigley@15642
   227
(*  Get Io-descriptor for polling of an input stream          *)
quigley@15642
   228
(**************************************************************)
quigley@15642
   229
quigley@15642
   230
quigley@15642
   231
fun getInIoDesc someInstr = 
quigley@15642
   232
    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
quigley@15642
   233
        val _ = print (TextIO.stdOut, buf)
quigley@15642
   234
        val ioDesc = 
quigley@15642
   235
	    case rd
quigley@15642
   236
	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
quigley@15642
   237
	       | _ => NONE
quigley@15642
   238
     in (* since getting the reader will have terminated the stream, we need
quigley@15642
   239
	 * to build a new stream. *)
quigley@15642
   240
	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
quigley@15642
   241
	ioDesc
quigley@15642
   242
    end
quigley@15642
   243
quigley@15642
   244
quigley@15642
   245
(*************************************)
quigley@15642
   246
(*  Set up a Watcher Process         *)
quigley@15642
   247
(*************************************)
quigley@15642
   248
quigley@15642
   249
quigley@15642
   250
quigley@15642
   251
fun setupWatcher (the_goal) = let
quigley@15642
   252
          (** pipes for communication between parent and watcher **)
quigley@15642
   253
          val p1 = Posix.IO.pipe ()
quigley@15642
   254
          val p2 = Posix.IO.pipe ()
quigley@15642
   255
	  fun closep () = (
quigley@15642
   256
                Posix.IO.close (#outfd p1); 
quigley@15642
   257
                Posix.IO.close (#infd p1);
quigley@15642
   258
                Posix.IO.close (#outfd p2); 
quigley@15642
   259
                Posix.IO.close (#infd p2)
quigley@15642
   260
              )
quigley@15642
   261
          (***********************************************************)
quigley@15642
   262
          (****** fork a watcher process and get it set up and going *)
quigley@15642
   263
          (***********************************************************)
quigley@15642
   264
          fun startWatcher (procList) =
quigley@15642
   265
                   (case  Posix.Process.fork() (***************************************)
quigley@15642
   266
		 of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
quigley@15642
   267
                                               (***************************************)
quigley@15642
   268
 
quigley@15642
   269
                                                 (*************************)
quigley@15642
   270
                  | NONE => let                  (* child - i.e. watcher  *)
quigley@15642
   271
		      val oldchildin = #infd p1  (*************************)
quigley@15642
   272
		      val fromParent = Posix.FileSys.wordToFD 0w0
quigley@15642
   273
		      val oldchildout = #outfd p2
quigley@15642
   274
		      val toParent = Posix.FileSys.wordToFD 0w1
quigley@15642
   275
                      val fromParentIOD = Posix.FileSys.fdToIOD fromParent
quigley@15642
   276
                      val fromParentStr = openInFD ("_exec_in_parent", fromParent)
quigley@15642
   277
                      val toParentStr = openOutFD ("_exec_out_parent", toParent)
quigley@15642
   278
                      val goalstr = string_of_thm (the_goal)
quigley@15642
   279
                       val  outfile = TextIO.openOut("goal_in_watcher");  
quigley@15642
   280
                      val _ = TextIO.output (outfile,goalstr )
quigley@15642
   281
                      val _ =  TextIO.closeOut outfile
quigley@15642
   282
                      fun killChildren [] = ()
quigley@15642
   283
                   |      killChildren  (childPid::children) = (killChild childPid; killChildren children)
quigley@15642
   284
quigley@15642
   285
                     
quigley@15642
   286
           
quigley@15642
   287
                    (*************************************************************)
quigley@15642
   288
                    (* take an instream and poll its underlying reader for input *)
quigley@15642
   289
                    (*************************************************************)
quigley@15642
   290
quigley@15642
   291
                    fun pollParentInput () = 
quigley@15642
   292
                           
quigley@15642
   293
                               let val pd = OS.IO.pollDesc (fromParentIOD)
quigley@15642
   294
                               in 
quigley@15642
   295
                               if (isSome pd ) then 
quigley@15642
   296
                                   let val pd' = OS.IO.pollIn (valOf pd)
quigley@15642
   297
                                       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
quigley@15642
   298
                                   in
quigley@15642
   299
                                      if null pdl 
quigley@15642
   300
                                      then
quigley@15642
   301
                                         NONE
quigley@15642
   302
                                      else if (OS.IO.isIn (hd pdl)) 
quigley@15642
   303
                                           then
quigley@15642
   304
                                              (SOME ( getCmds (toParentStr, fromParentStr, [])))
quigley@15642
   305
                                           else
quigley@15642
   306
                                               NONE
quigley@15642
   307
                                   end
quigley@15642
   308
                                 else
quigley@15642
   309
                                     NONE
quigley@15642
   310
                                 end
quigley@15642
   311
                            
quigley@15642
   312
                   
quigley@15642
   313
quigley@15642
   314
                     fun pollChildInput (fromStr) = 
quigley@15642
   315
                           let val iod = getInIoDesc fromStr
quigley@15642
   316
                           in 
quigley@15642
   317
                           if isSome iod 
quigley@15642
   318
                           then 
quigley@15642
   319
                               let val pd = OS.IO.pollDesc (valOf iod)
quigley@15642
   320
                               in 
quigley@15642
   321
                               if (isSome pd ) then 
quigley@15642
   322
                                   let val pd' = OS.IO.pollIn (valOf pd)
quigley@15642
   323
                                       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
quigley@15642
   324
                                   in
quigley@15642
   325
                                      if null pdl 
quigley@15642
   326
                                      then
quigley@15642
   327
                                         NONE
quigley@15642
   328
                                      else if (OS.IO.isIn (hd pdl)) 
quigley@15642
   329
                                           then
quigley@15642
   330
                                               SOME (getCmd (TextIO.inputLine fromStr))
quigley@15642
   331
                                           else
quigley@15642
   332
                                               NONE
quigley@15642
   333
                                   end
quigley@15642
   334
                                 else
quigley@15642
   335
                                     NONE
quigley@15642
   336
                                 end
quigley@15642
   337
                             else 
quigley@15642
   338
                                 NONE
quigley@15642
   339
                            end
quigley@15642
   340
quigley@15642
   341
quigley@15642
   342
                   (****************************************************************************)
quigley@15642
   343
                   (* Check all vampire processes currently running for output                 *)
quigley@15642
   344
                   (****************************************************************************) 
quigley@15642
   345
                                                              (*********************************)
quigley@15642
   346
                    fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
quigley@15642
   347
                                                              (*********************************)
quigley@15642
   348
                    |   checkChildren ((childProc::otherChildren), toParentStr) = 
quigley@15642
   349
                                            let val (childInput,childOutput) =  cmdstreamsOf childProc
quigley@15642
   350
                                                val childPid = cmdchildPid childProc
quigley@15642
   351
                                                val childCmd = fst(snd (cmdchildInfo childProc))
quigley@15642
   352
                                                val childIncoming = pollChildInput childInput
quigley@15642
   353
                                                val parentID = Posix.ProcEnv.getppid()
quigley@15642
   354
                                                val prover = cmdProver childProc
quigley@15642
   355
                                                val thmstring = cmdThm childProc
quigley@15642
   356
                                                val goalstring = cmdGoal childProc
quigley@15642
   357
                                                val  outfile = TextIO.openOut("child_comms");  
quigley@15642
   358
                                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
quigley@15642
   359
                                                val _ =  TextIO.closeOut outfile
quigley@15642
   360
                                            in 
quigley@15642
   361
                                              if (isSome childIncoming) 
quigley@15642
   362
                                              then 
quigley@15642
   363
                                                  (* check here for prover label on child*)
quigley@15642
   364
                                                   
quigley@15642
   365
                                                  let val  outfile = TextIO.openOut("child_incoming");  
quigley@15642
   366
                                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
quigley@15642
   367
                                                val _ =  TextIO.closeOut outfile
quigley@15642
   368
                                              val childDone = (case prover of
quigley@15642
   369
                                    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd)     ) )
quigley@15642
   370
                                                   in
quigley@15642
   371
                                                    if childDone      (**********************************************)
quigley@15642
   372
                                                    then              (* child has found a proof and transferred it *)
quigley@15642
   373
                                                                      (**********************************************)
quigley@15642
   374
quigley@15642
   375
                                                       (**********************************************)
quigley@15642
   376
                                                       (* Remove this child and go on to check others*)
quigley@15642
   377
                                                       (**********************************************)
quigley@15642
   378
                                                       ( reap(childPid, childInput, childOutput);
quigley@15642
   379
                                                         checkChildren(otherChildren, toParentStr))
quigley@15642
   380
                                                    else 
quigley@15642
   381
                                                       (**********************************************)
quigley@15642
   382
                                                       (* Keep this child and go on to check others  *)
quigley@15642
   383
                                                       (**********************************************)
quigley@15642
   384
quigley@15642
   385
                                                         (childProc::(checkChildren (otherChildren, toParentStr)))
quigley@15642
   386
                                                 end
quigley@15642
   387
                                               else
quigley@15652
   388
                                                   let val  outfile = TextIO.openAppend("child_incoming");  
quigley@15642
   389
                                                val _ = TextIO.output (outfile,"No child output " )
quigley@15642
   390
                                                val _ =  TextIO.closeOut outfile
quigley@15642
   391
                                                 in
quigley@15642
   392
                                                    (childProc::(checkChildren (otherChildren, toParentStr)))
quigley@15642
   393
                                                 end
quigley@15642
   394
                                            end
quigley@15642
   395
quigley@15642
   396
                   
quigley@15642
   397
                (********************************************************************)                  
quigley@15642
   398
                (* call resolution processes                                        *)
quigley@15642
   399
                (* settings should be a list of strings                             *)
quigley@15642
   400
                (* e.g. ["-t 300", "-m 100000"]                                     *)
quigley@15642
   401
                (* takes list of (string, string, string list, string)list proclist *)
quigley@15642
   402
                (********************************************************************)
quigley@15642
   403
quigley@15642
   404
                   fun execCmds  [] procList = procList
quigley@15642
   405
                   |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
quigley@15642
   406
                                                     if (prover = "spass") 
quigley@15642
   407
                                                     then 
quigley@15642
   408
                                                         let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@["-FullRed=0"]@settings@[file]), procList)
quigley@15642
   409
                                                         in
quigley@15642
   410
                                                            execCmds cmds newProcList
quigley@15642
   411
                                                         end
quigley@15642
   412
                                                     else 
quigley@15642
   413
                                                         let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@settings@[file]), procList)
quigley@15642
   414
                                                         in
quigley@15642
   415
                                                            execCmds cmds newProcList
quigley@15642
   416
                                                         end
quigley@15642
   417
quigley@15642
   418
quigley@15642
   419
                (****************************************)                  
quigley@15642
   420
                (* call resolution processes remotely   *)
quigley@15642
   421
                (* settings should be a list of strings *)
quigley@15642
   422
                (* e.g. ["-t 300", "-m 100000"]         *)
quigley@15642
   423
                (****************************************)
quigley@15642
   424
  
quigley@15642
   425
                   fun execRemoteCmds  [] procList = procList
quigley@15642
   426
                   |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
quigley@15642
   427
                                             let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
quigley@15642
   428
                                                 in
quigley@15642
   429
                                                      execRemoteCmds  cmds newProcList
quigley@15642
   430
                                                 end
quigley@15642
   431
quigley@15642
   432
quigley@15642
   433
                   fun printList (outStr, []) = ()
quigley@15642
   434
                   |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
quigley@15642
   435
quigley@15642
   436
quigley@15642
   437
                (**********************************************)                  
quigley@15642
   438
                (* Watcher Loop                               *)
quigley@15642
   439
                (**********************************************)
quigley@15642
   440
quigley@15642
   441
quigley@15642
   442
quigley@15642
   443
   
quigley@15642
   444
                    fun keepWatching (toParentStr, fromParentStr,procList) = 
quigley@15642
   445
                          let    fun loop (procList) =  
quigley@15642
   446
                                 (
quigley@15642
   447
                                 let val cmdsFromIsa = pollParentInput ()
quigley@15642
   448
                                      fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
quigley@15642
   449
                                                  TextIO.flushOut toParentStr;
quigley@15642
   450
                                                   killChildren (map (cmdchildPid) procList);
quigley@15642
   451
                                                    ())
quigley@15642
   452
                                     
quigley@15642
   453
                                 in 
quigley@15642
   454
                                    (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
quigley@15642
   455
                                                                                       (**********************************)
quigley@15642
   456
                                    if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
quigley@15642
   457
                                         (                                             (**********************************)                             
quigley@15642
   458
                                          if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
quigley@15642
   459
                                          then 
quigley@15642
   460
                                            (
quigley@15642
   461
                                              let val childPids = map cmdchildPid procList 
quigley@15642
   462
                                              in
quigley@15642
   463
                                                 killChildren childPids;
quigley@15642
   464
                                                 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                       loop ([])
quigley@15642
   465
                                              end
quigley@15642
   466
                                             )
quigley@15642
   467
                                          else
quigley@15642
   468
                                            ( 
quigley@15642
   469
                                              if ((length procList)<2)    (********************)
quigley@15642
   470
                                              then                        (* Execute locally  *)
quigley@15642
   471
                                                 (                        (********************)
quigley@15642
   472
                                                  let 
quigley@15642
   473
                                                    val newProcList = execCmds (valOf cmdsFromIsa) procList
quigley@15642
   474
                                                    val parentID = Posix.ProcEnv.getppid()
quigley@15642
   475
                                                    val newProcList' =checkChildren (newProcList, toParentStr) 
quigley@15642
   476
                                                  in
quigley@15642
   477
                                                    (*OS.Process.sleep (Time.fromSeconds 1);*)
quigley@15642
   478
                                                    loop (newProcList') 
quigley@15642
   479
                                                  end
quigley@15642
   480
                                                  )
quigley@15642
   481
                                              else                         (************************)
quigley@15642
   482
                                                                           (* Execute remotely     *)
quigley@15642
   483
                                                  (                        (************************)
quigley@15642
   484
                                                  let 
quigley@15642
   485
                                                    val newProcList = execRemoteCmds (valOf cmdsFromIsa) procList
quigley@15642
   486
                                                    val parentID = Posix.ProcEnv.getppid()
quigley@15642
   487
                                                    val newProcList' =checkChildren (newProcList, toParentStr) 
quigley@15642
   488
                                                  in
quigley@15642
   489
                                                    (*OS.Process.sleep (Time.fromSeconds 1);*)
quigley@15642
   490
                                                    loop (newProcList') 
quigley@15642
   491
                                                  end
quigley@15642
   492
                                                  )
quigley@15642
   493
quigley@15642
   494
quigley@15642
   495
quigley@15642
   496
                                              )
quigley@15642
   497
                                           )                                              (******************************)
quigley@15642
   498
                                    else                                                  (* No new input from Isabelle *)
quigley@15642
   499
                                                                                          (******************************)
quigley@15642
   500
                                        (    let val newProcList = checkChildren ((procList), toParentStr)
quigley@15642
   501
                                             in
quigley@15642
   502
                                               OS.Process.sleep (Time.fromSeconds 1);
quigley@15642
   503
                                               loop (newProcList)
quigley@15642
   504
                                             end
quigley@15642
   505
                                         
quigley@15642
   506
                                         )
quigley@15642
   507
                                  end)
quigley@15642
   508
                          in  
quigley@15642
   509
                              loop (procList)
quigley@15642
   510
                          end
quigley@15642
   511
                      
quigley@15642
   512
          
quigley@15642
   513
                      in
quigley@15642
   514
                       (***************************)
quigley@15642
   515
                       (*** Sort out pipes ********)
quigley@15642
   516
                       (***************************)
quigley@15642
   517
quigley@15642
   518
			Posix.IO.close (#outfd p1);
quigley@15642
   519
			Posix.IO.close (#infd p2);
quigley@15642
   520
			Posix.IO.dup2{old = oldchildin, new = fromParent};
quigley@15642
   521
                        Posix.IO.close oldchildin;
quigley@15642
   522
			Posix.IO.dup2{old = oldchildout, new = toParent};
quigley@15642
   523
                        Posix.IO.close oldchildout;
quigley@15642
   524
quigley@15642
   525
                        (***************************)
quigley@15642
   526
                        (* start the watcher loop  *)
quigley@15642
   527
                        (***************************)
quigley@15642
   528
                        keepWatching (toParentStr, fromParentStr, procList);
quigley@15642
   529
quigley@15642
   530
quigley@15642
   531
                        (****************************************************************************)
quigley@15642
   532
                        (* fake return value - actually want the watcher to loop until killed       *)
quigley@15642
   533
                        (****************************************************************************)
quigley@15642
   534
                        Posix.Process.wordToPid 0w0
quigley@15642
   535
			
quigley@15642
   536
		      end);
quigley@15642
   537
		(* end case *)
quigley@15642
   538
quigley@15642
   539
quigley@15642
   540
          val _ = TextIO.flushOut TextIO.stdOut
quigley@15642
   541
quigley@15642
   542
          (*******************************)
quigley@15642
   543
          (***  set watcher going ********)
quigley@15642
   544
          (*******************************)
quigley@15642
   545
quigley@15642
   546
          val procList = []
quigley@15642
   547
          val pid = startWatcher (procList)
quigley@15642
   548
          (**************************************************)
quigley@15642
   549
          (* communication streams to watcher               *)
quigley@15642
   550
          (**************************************************)
quigley@15642
   551
quigley@15642
   552
	  val instr = openInFD ("_exec_in", #infd p2)
quigley@15642
   553
          val outstr = openOutFD ("_exec_out", #outfd p1)
quigley@15642
   554
          
quigley@15642
   555
          in
quigley@15642
   556
           (*******************************)
quigley@15642
   557
           (* close the child-side fds    *)
quigley@15642
   558
           (*******************************)
quigley@15642
   559
            Posix.IO.close (#outfd p2);
quigley@15642
   560
            Posix.IO.close (#infd p1);
quigley@15642
   561
            (* set the fds close on exec *)
quigley@15642
   562
            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
quigley@15642
   563
            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
quigley@15642
   564
             
quigley@15642
   565
           (*******************************)
quigley@15642
   566
           (* return value                *)
quigley@15642
   567
           (*******************************)
quigley@15642
   568
            PROC{pid = pid,
quigley@15642
   569
              instr = instr,
quigley@15642
   570
              outstr = outstr
quigley@15642
   571
            }
quigley@15642
   572
         end;
quigley@15642
   573
quigley@15642
   574
quigley@15642
   575
quigley@15642
   576
(**********************************************************)
quigley@15642
   577
(* Start a watcher and set up signal handlers             *)
quigley@15642
   578
(**********************************************************)
quigley@15642
   579
fun killWatcher pid= killChild pid;
quigley@15642
   580
quigley@15642
   581
fun createWatcher (the_goal) = let val mychild = childInfo (setupWatcher(the_goal))
quigley@15642
   582
			   val streams =snd mychild
quigley@15642
   583
                           val childin = fst streams
quigley@15642
   584
                           val childout = snd streams
quigley@15642
   585
                           val childpid = fst mychild
quigley@15642
   586
                           
quigley@15642
   587
                           fun vampire_proofHandler (n:int) =
quigley@15642
   588
                           (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
quigley@15642
   589
                           getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )                   
quigley@15642
   590
                          
quigley@15642
   591
                          (* fun spass_proofHandler (n:int) = (
quigley@15642
   592
                                                      let val (reconstr, thmstring, goalstring) = getSpassInput childin
quigley@15642
   593
                                                          val  outfile = TextIO.openOut("foo_signal");
quigley@15642
   594
quigley@15642
   595
                                                         val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring))
quigley@15642
   596
                                                         val _ =  TextIO.closeOut outfile
quigley@15642
   597
                                                      in
quigley@15642
   598
                                                         Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
quigley@15642
   599
                                                          Pretty.writeln(Pretty.str reconstr) ;
quigley@15642
   600
                                                         Pretty.writeln(Pretty.str  (oct_char "361"));
quigley@15642
   601
                                                         (*killWatcher childpid;*) () 
quigley@15642
   602
                                                      end)*)
quigley@15642
   603
quigley@15642
   604
quigley@15642
   605
(*
quigley@15642
   606
quigley@15642
   607
fun spass_proofHandler (n:int) = (
quigley@15642
   608
                                                      let  val  outfile = TextIO.openOut("foo_signal1");
quigley@15642
   609
quigley@15642
   610
                                                         val _ = TextIO.output (outfile, ("In signal handler now\n"))
quigley@15642
   611
                                                         val _ =  TextIO.closeOut outfile
quigley@15642
   612
                                                          val (reconstr, thmstring, goalstring) = getSpassInput childin
quigley@15642
   613
                                                         val  outfile = TextIO.openOut("foo_signal");
quigley@15642
   614
quigley@15642
   615
                                                         val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring^goalstring))
quigley@15642
   616
                                                         val _ =  TextIO.closeOut outfile
quigley@15642
   617
                                                       in
quigley@15642
   618
                                                        if ( (substring (reconstr, 0,1))= "[")
quigley@15642
   619
                                                         then 
quigley@15642
   620
quigley@15642
   621
                                                          let val thm = thm_of_string thmstring
quigley@15642
   622
                                                              val clauses = make_clauses [thm]
quigley@15642
   623
                                                              val numcls =  zip  (numlist (length clauses)) (map make_meta_clause clauses)
quigley@15642
   624
                                                         
quigley@15642
   625
                                                          in
quigley@15642
   626
                                                             Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
quigley@15642
   627
                                                             apply_res_thm reconstr goalstring;
quigley@15642
   628
                                                             Pretty.writeln(Pretty.str  (oct_char "361"));
quigley@15642
   629
                                                             killWatcher childpid; () 
quigley@15642
   630
                                                          end
quigley@15642
   631
                                                       else
quigley@15642
   632
                                                           Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
quigley@15642
   633
                                                              Pretty.writeln(Pretty.str (goalstring^reconstr));
quigley@15642
   634
                                                             Pretty.writeln(Pretty.str  (oct_char "361"));
quigley@15642
   635
                                                             (*killWatcher childpid; *) reap (childpid,childin, childout);()   
quigley@15642
   636
                                                      end )
quigley@15642
   637
*)
quigley@15642
   638
quigley@15642
   639
fun spass_proofHandler (n:int) = (
quigley@15642
   640
                                 let  val  outfile = TextIO.openOut("foo_signal1");
quigley@15642
   641
                                      val _ = TextIO.output (outfile, ("In signal handler now\n"))
quigley@15642
   642
                                      val _ =  TextIO.closeOut outfile
quigley@15642
   643
                                      val (reconstr, thmstring, goalstring) = getSpassInput childin
quigley@15642
   644
                                      val  outfile = TextIO.openAppend("foo_signal");
quigley@15642
   645
quigley@15642
   646
                                      val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
quigley@15642
   647
                                      val _ =  TextIO.closeOut outfile
quigley@15642
   648
                                      in          (* if a proof has been found and sent back as a reconstruction proof *)
quigley@15642
   649
                                                  if ( (substring (reconstr, 0,1))= "[")
quigley@15642
   650
                                                  then 
quigley@15642
   651
quigley@15642
   652
                                                            (
quigley@15642
   653
                                                                 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
quigley@15642
   654
                                                                 apply_res_thm reconstr goalstring;
quigley@15642
   655
                                                                 Pretty.writeln(Pretty.str  (oct_char "361"));
quigley@15642
   656
                                                                 
quigley@15642
   657
                                                                 goals_being_watched := ((!goals_being_watched) - 1);
quigley@15642
   658
                                                         
quigley@15642
   659
                                                                 if ((!goals_being_watched) = 0)
quigley@15642
   660
                                                                 then 
quigley@15642
   661
                                                                    (let val  outfile = TextIO.openOut("foo_reap_found");
quigley@15642
   662
                                                                         val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
quigley@15642
   663
                                                                         val _ =  TextIO.closeOut outfile
quigley@15642
   664
                                                                     in
quigley@15642
   665
                                                                         reap (childpid,childin, childout); ()
quigley@15642
   666
                                                                     end)
quigley@15642
   667
                                                                 else
quigley@15642
   668
                                                                    ()
quigley@15642
   669
                                                            )
quigley@15642
   670
                                                    (* if there's no proof, but a message from Spass *)
quigley@15642
   671
                                                    else if ((substring (reconstr, 0,5))= "SPASS")
quigley@15642
   672
                                                         then
quigley@15642
   673
                                                                 (
quigley@15642
   674
                                                                     goals_being_watched := (!goals_being_watched) -1;
quigley@15642
   675
                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
quigley@15642
   676
                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
quigley@15642
   677
                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
quigley@15642
   678
                                                                      if (!goals_being_watched = 0)
quigley@15642
   679
                                                                      then 
quigley@15642
   680
                                                                          (let val  outfile = TextIO.openOut("foo_reap_comp");
quigley@15642
   681
                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
quigley@15642
   682
                                                                               val _ =  TextIO.closeOut outfile
quigley@15642
   683
                                                                           in
quigley@15642
   684
                                                                              reap (childpid,childin, childout); ()
quigley@15642
   685
                                                                           end )
quigley@15642
   686
                                                                      else
quigley@15642
   687
                                                                         ()
quigley@15642
   688
                                                                )
quigley@15642
   689
                                                          (* if proof translation failed *)
quigley@15642
   690
                                                          else if ((substring (reconstr, 0,5)) = "Proof")
quigley@15642
   691
                                                               then 
quigley@15642
   692
                                                                   (
quigley@15642
   693
                                                                     goals_being_watched := (!goals_being_watched) -1;
quigley@15642
   694
                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
quigley@15642
   695
                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
quigley@15642
   696
                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
quigley@15642
   697
                                                                      if (!goals_being_watched = 0)
quigley@15642
   698
                                                                      then 
quigley@15642
   699
                                                                          (let val  outfile = TextIO.openOut("foo_reap_comp");
quigley@15642
   700
                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
quigley@15642
   701
                                                                               val _ =  TextIO.closeOut outfile
quigley@15642
   702
                                                                           in
quigley@15642
   703
                                                                              reap (childpid,childin, childout); ()
quigley@15642
   704
                                                                           end )
quigley@15642
   705
                                                                      else
quigley@15642
   706
                                                                         ()
quigley@15642
   707
                                                                )
quigley@15642
   708
quigley@15642
   709
quigley@15642
   710
                                                                else  (* add something here ?*)
quigley@15642
   711
                                                                   ()
quigley@15642
   712
                                                             
quigley@15642
   713
                                       end)
quigley@15642
   714
quigley@15642
   715
quigley@15642
   716
                        
quigley@15642
   717
                       in 
quigley@15642
   718
                          Signal.signal (Posix.Signal.usr1, Signal.SIG_HANDLE vampire_proofHandler);
quigley@15642
   719
                          Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE spass_proofHandler);
quigley@15642
   720
                          (childin, childout, childpid)
quigley@15642
   721
quigley@15642
   722
                       end
quigley@15642
   723
quigley@15642
   724
quigley@15642
   725
quigley@15642
   726
quigley@15642
   727
quigley@15642
   728
end (* structure Watcher *)