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