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