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