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