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