src/HOL/Tools/ATP/watcher.ML
changeset 15642 028059faa963
child 15652 a9d65894962e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Mar 31 19:29:26 2005 +0200
     1.3 @@ -0,0 +1,729 @@
     1.4 +
     1.5 + (*  Title:      Watcher.ML
     1.6 +     Author:     Claire Quigley
     1.7 +     Copyright   2004  University of Cambridge
     1.8 + *)
     1.9 +
    1.10 + (***************************************************************************)
    1.11 + (*  The watcher process starts a resolution process when it receives a     *)
    1.12 +(*  message from Isabelle                                                  *)
    1.13 +(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    1.14 +(*  and removes dead processes.  Also possible to kill all the resolution  *)
    1.15 +(*  processes currently running.                                           *)
    1.16 +(*  Hardwired version of where to pick up the tptp files for the moment    *)
    1.17 +(***************************************************************************)
    1.18 +
    1.19 +(*use "Proof_Transfer";
    1.20 +use "VampireCommunication";
    1.21 +use "SpassCommunication";
    1.22 +use "modUnix";*)
    1.23 +(*use "/homes/clq20/Jia_Code/TransStartIsar";*)
    1.24 +
    1.25 +use "~~/VampireCommunication";
    1.26 +use "~~/SpassCommunication";
    1.27 +
    1.28 +
    1.29 +use "~~/modUnix";
    1.30 +
    1.31 +
    1.32 +structure Watcher: WATCHER =
    1.33 +  struct
    1.34 +
    1.35 +fun fst (a,b) = a;
    1.36 +fun snd (a,b) = b;
    1.37 +
    1.38 +val goals_being_watched = ref 0;
    1.39 +
    1.40 +
    1.41 +fun remove y [] = []
    1.42 +|   remove y (x::xs) = (if y = x 
    1.43 +                       then 
    1.44 +                           remove y xs 
    1.45 +                       else ((x::(remove y  xs))))
    1.46 +
    1.47 +
    1.48 +
    1.49 +fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
    1.50 +
    1.51 +(********************************************************************************************)
    1.52 +(*  takes a list of arguments and sends them individually to the watcher process by pipe    *)
    1.53 +(********************************************************************************************)
    1.54 +
    1.55 +fun outputArgs (toWatcherStr, []) = ()
    1.56 +|   outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); 
    1.57 +                                          TextIO.flushOut toWatcherStr;
    1.58 +                                         outputArgs (toWatcherStr, xs))
    1.59 +
    1.60 +(********************************************************************************)
    1.61 +(*    gets individual args from instream and concatenates them into a list      *)
    1.62 +(********************************************************************************)
    1.63 +
    1.64 +fun getArgs (fromParentStr, toParentStr,ys) =  let 
    1.65 +                                       val thisLine = TextIO.input fromParentStr
    1.66 +                                    in
    1.67 +                                        ((ys@[thisLine]))
    1.68 +                                    end
    1.69 +
    1.70 +(********************************************************************************)
    1.71 +(*  Remove the \n character from the end of each filename                       *)
    1.72 +(********************************************************************************)
    1.73 +
    1.74 +fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
    1.75 +                    in
    1.76 +
    1.77 +                        if (String.isPrefix "\n"  (implode backList )) 
    1.78 +                        then 
    1.79 +                             (implode (rev ((tl backList))))
    1.80 +                        else
    1.81 +                           (cmdStr)
    1.82 +                    end
    1.83 +                            
    1.84 +(********************************************************************************)
    1.85 +(*  Send request to Watcher for a vampire to be called for filename in arg      *)
    1.86 +(********************************************************************************)
    1.87 +                    
    1.88 +fun callResProver (toWatcherStr,  arg) = (sendOutput (toWatcherStr, arg^"\n"); 
    1.89 +                                     TextIO.flushOut toWatcherStr
    1.90 +                                    
    1.91 +                                     )
    1.92 +
    1.93 +(*****************************************************************************************)
    1.94 +(*  Send request to Watcher for multiple provers to be called for filenames in arg      *)
    1.95 +(*****************************************************************************************)
    1.96 +
    1.97 +(* need to modify to send over hyps file too *)
    1.98 +fun callResProvers (toWatcherStr,  []) = (sendOutput (toWatcherStr, "End of calls\n"); 
    1.99 +                                     TextIO.flushOut toWatcherStr)
   1.100 +|   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,probfile)::args) =
   1.101 +                                                     let 
   1.102 +                                                        val dfg_dir = File.tmp_path (Path.basic "dfg");
   1.103 +                                                        (* need to check here if the directory exists and, if not, create it*)
   1.104 +                                                         val  outfile = TextIO.openAppend(" /thmstring_in_watcher");                                                                                    
   1.105 +                                                         val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
   1.106 +                                                         val _ =  TextIO.closeOut outfile
   1.107 +                                                         val dfg_create =if File.exists dfg_dir 
   1.108 +                                                                         then
   1.109 +                                                                             ()
   1.110 +                                                                         else
   1.111 +                                                                               File.mkdir dfg_dir; 
   1.112 +                                                         val probID = last(explode probfile)
   1.113 +                                                         val dfg_path = File.sysify_path dfg_dir;
   1.114 +                                                         val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v2.6.0/TPTP2X/tptp2X", ["-fdfg "^probfile^" -d "^dfg_path])
   1.115 +                                                       (*val _ = Posix.Process.wait ()*)
   1.116 +                                                       (*val _ =Unix.reap exec_tptp2x*)
   1.117 +                                                         val newfile = dfg_path^"/prob"^(probID)^".dfg"
   1.118 +                                       
   1.119 +                                                      in   
   1.120 +                                                         goals_being_watched := (!goals_being_watched) + 1;
   1.121 +                                                         OS.Process.sleep(Time.fromSeconds 1); 
   1.122 +                                                         (warning("dfg file is: "^newfile));
   1.123 +                                                         sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
   1.124 +                                                         TextIO.flushOut toWatcherStr;
   1.125 +                                                         Unix.reap exec_tptp2x; 
   1.126 +                                                         
   1.127 +                                                         callResProvers (toWatcherStr,args)
   1.128 +                                           
   1.129 +                                                     end
   1.130 +
   1.131 +fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
   1.132 +                                     
   1.133 +|   callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings, file)::args) =
   1.134 +                                            ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^file^"\n")
   1.135 +                                            
   1.136 +                                           )
   1.137 + 
   1.138 +(**************************************************************)
   1.139 +(* Send message to watcher to kill currently running vampires *)
   1.140 +(**************************************************************)
   1.141 +
   1.142 +fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 
   1.143 +                            TextIO.flushOut toWatcherStr)
   1.144 +
   1.145 +
   1.146 +
   1.147 +(**************************************************************)
   1.148 +(* Remove \n token from a vampire goal filename and extract   *)
   1.149 +(* prover, proverCmd, settings and file from input string     *)
   1.150 +(**************************************************************)
   1.151 +
   1.152 +
   1.153 + fun takeUntil ch [] res  = (res, [])
   1.154 + |   takeUntil ch (x::xs) res = if   x = ch 
   1.155 +                                then
   1.156 +                                     (res, xs)
   1.157 +                                else
   1.158 +                                     takeUntil ch xs (res@[x])
   1.159 +
   1.160 + fun getSettings [] settings = settings
   1.161 +|    getSettings (xs) settings = let val (set, rest ) = takeUntil "%" xs []
   1.162 +                                 in
   1.163 +                                     getSettings rest (settings@[(implode set)])
   1.164 +                                 end
   1.165 +
   1.166 +fun separateFields str = let val (prover, rest) = takeUntil "*" str []
   1.167 +                              val prover = implode prover
   1.168 +                              val (thmstring, rest) =  takeUntil "*" rest []
   1.169 +                              val thmstring = implode thmstring
   1.170 +                              val (goalstring, rest) =  takeUntil "*" rest []
   1.171 +                              val goalstring = implode goalstring
   1.172 +                              val (proverCmd, rest ) =  takeUntil "*" rest []
   1.173 +                              val proverCmd = implode proverCmd
   1.174 +                              
   1.175 +                              val (settings, rest) =  takeUntil "*" rest []
   1.176 +                              val settings = getSettings settings []
   1.177 +                              val (file, rest) =  takeUntil "*" rest []
   1.178 +                              val file = implode file
   1.179 +                              val  outfile = TextIO.openOut("sep_comms");                                                                                    
   1.180 +                              val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^file) )
   1.181 +                              val _ =  TextIO.closeOut outfile
   1.182 +                              
   1.183 +                          in
   1.184 +                             (prover,thmstring,goalstring, proverCmd, settings, file)
   1.185 +                          end
   1.186 +
   1.187 + 
   1.188 +
   1.189 + fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
   1.190 +                     in
   1.191 +
   1.192 +                         if (String.isPrefix "\n"  (implode backList )) 
   1.193 +                         then 
   1.194 +                             separateFields ((rev ((tl backList))))
   1.195 +                         else
   1.196 +                           (separateFields (explode cmdStr))
   1.197 +                     end
   1.198 +                      
   1.199 +
   1.200 +fun getProofCmd (a,b,c,d,e,f) = d
   1.201 +
   1.202 +
   1.203 +(**************************************************************)
   1.204 +(* Get commands from Isabelle                                 *)
   1.205 +(**************************************************************)
   1.206 +
   1.207 +fun getCmds (toParentStr,fromParentStr, cmdList) = 
   1.208 +                                       let val thisLine = TextIO.inputLine fromParentStr 
   1.209 +                                       in
   1.210 +                                          (if (thisLine = "End of calls\n") 
   1.211 +                                           then 
   1.212 +                                              (cmdList)
   1.213 +                                           else if (thisLine = "Kill children\n") 
   1.214 +                                                then 
   1.215 +                                                    (   TextIO.output (toParentStr,thisLine ); 
   1.216 +                                                        TextIO.flushOut toParentStr;
   1.217 +                                                      (("","","","Kill children",[],"")::cmdList)
   1.218 +                                                     )
   1.219 +                                              else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   1.220 +                                                    in
   1.221 +                                                      (*TextIO.output (toParentStr, thisCmd); 
   1.222 +                                                        TextIO.flushOut toParentStr;*)
   1.223 +                                                        getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
   1.224 +                                                    end
   1.225 +                                                    )
   1.226 +                                            )
   1.227 +                                        end
   1.228 +                                    
   1.229 +                                    
   1.230 +(**************************************************************)
   1.231 +(*  Get Io-descriptor for polling of an input stream          *)
   1.232 +(**************************************************************)
   1.233 +
   1.234 +
   1.235 +fun getInIoDesc someInstr = 
   1.236 +    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   1.237 +        val _ = print (TextIO.stdOut, buf)
   1.238 +        val ioDesc = 
   1.239 +	    case rd
   1.240 +	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
   1.241 +	       | _ => NONE
   1.242 +     in (* since getting the reader will have terminated the stream, we need
   1.243 +	 * to build a new stream. *)
   1.244 +	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
   1.245 +	ioDesc
   1.246 +    end
   1.247 +
   1.248 +
   1.249 +(*************************************)
   1.250 +(*  Set up a Watcher Process         *)
   1.251 +(*************************************)
   1.252 +
   1.253 +
   1.254 +
   1.255 +fun setupWatcher (the_goal) = let
   1.256 +          (** pipes for communication between parent and watcher **)
   1.257 +          val p1 = Posix.IO.pipe ()
   1.258 +          val p2 = Posix.IO.pipe ()
   1.259 +	  fun closep () = (
   1.260 +                Posix.IO.close (#outfd p1); 
   1.261 +                Posix.IO.close (#infd p1);
   1.262 +                Posix.IO.close (#outfd p2); 
   1.263 +                Posix.IO.close (#infd p2)
   1.264 +              )
   1.265 +          (***********************************************************)
   1.266 +          (****** fork a watcher process and get it set up and going *)
   1.267 +          (***********************************************************)
   1.268 +          fun startWatcher (procList) =
   1.269 +                   (case  Posix.Process.fork() (***************************************)
   1.270 +		 of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   1.271 +                                               (***************************************)
   1.272 + 
   1.273 +                                                 (*************************)
   1.274 +                  | NONE => let                  (* child - i.e. watcher  *)
   1.275 +		      val oldchildin = #infd p1  (*************************)
   1.276 +		      val fromParent = Posix.FileSys.wordToFD 0w0
   1.277 +		      val oldchildout = #outfd p2
   1.278 +		      val toParent = Posix.FileSys.wordToFD 0w1
   1.279 +                      val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   1.280 +                      val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   1.281 +                      val toParentStr = openOutFD ("_exec_out_parent", toParent)
   1.282 +                      val goalstr = string_of_thm (the_goal)
   1.283 +                       val  outfile = TextIO.openOut("goal_in_watcher");  
   1.284 +                      val _ = TextIO.output (outfile,goalstr )
   1.285 +                      val _ =  TextIO.closeOut outfile
   1.286 +                      fun killChildren [] = ()
   1.287 +                   |      killChildren  (childPid::children) = (killChild childPid; killChildren children)
   1.288 +
   1.289 +                     
   1.290 +           
   1.291 +                    (*************************************************************)
   1.292 +                    (* take an instream and poll its underlying reader for input *)
   1.293 +                    (*************************************************************)
   1.294 +
   1.295 +                    fun pollParentInput () = 
   1.296 +                           
   1.297 +                               let val pd = OS.IO.pollDesc (fromParentIOD)
   1.298 +                               in 
   1.299 +                               if (isSome pd ) then 
   1.300 +                                   let val pd' = OS.IO.pollIn (valOf pd)
   1.301 +                                       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
   1.302 +                                   in
   1.303 +                                      if null pdl 
   1.304 +                                      then
   1.305 +                                         NONE
   1.306 +                                      else if (OS.IO.isIn (hd pdl)) 
   1.307 +                                           then
   1.308 +                                              (SOME ( getCmds (toParentStr, fromParentStr, [])))
   1.309 +                                           else
   1.310 +                                               NONE
   1.311 +                                   end
   1.312 +                                 else
   1.313 +                                     NONE
   1.314 +                                 end
   1.315 +                            
   1.316 +                   
   1.317 +
   1.318 +                     fun pollChildInput (fromStr) = 
   1.319 +                           let val iod = getInIoDesc fromStr
   1.320 +                           in 
   1.321 +                           if isSome iod 
   1.322 +                           then 
   1.323 +                               let val pd = OS.IO.pollDesc (valOf iod)
   1.324 +                               in 
   1.325 +                               if (isSome pd ) then 
   1.326 +                                   let val pd' = OS.IO.pollIn (valOf pd)
   1.327 +                                       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
   1.328 +                                   in
   1.329 +                                      if null pdl 
   1.330 +                                      then
   1.331 +                                         NONE
   1.332 +                                      else if (OS.IO.isIn (hd pdl)) 
   1.333 +                                           then
   1.334 +                                               SOME (getCmd (TextIO.inputLine fromStr))
   1.335 +                                           else
   1.336 +                                               NONE
   1.337 +                                   end
   1.338 +                                 else
   1.339 +                                     NONE
   1.340 +                                 end
   1.341 +                             else 
   1.342 +                                 NONE
   1.343 +                            end
   1.344 +
   1.345 +
   1.346 +                   (****************************************************************************)
   1.347 +                   (* Check all vampire processes currently running for output                 *)
   1.348 +                   (****************************************************************************) 
   1.349 +                                                              (*********************************)
   1.350 +                    fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   1.351 +                                                              (*********************************)
   1.352 +                    |   checkChildren ((childProc::otherChildren), toParentStr) = 
   1.353 +                                            let val (childInput,childOutput) =  cmdstreamsOf childProc
   1.354 +                                                val childPid = cmdchildPid childProc
   1.355 +                                                val childCmd = fst(snd (cmdchildInfo childProc))
   1.356 +                                                val childIncoming = pollChildInput childInput
   1.357 +                                                val parentID = Posix.ProcEnv.getppid()
   1.358 +                                                val prover = cmdProver childProc
   1.359 +                                                val thmstring = cmdThm childProc
   1.360 +                                                val goalstring = cmdGoal childProc
   1.361 +                                                val  outfile = TextIO.openOut("child_comms");  
   1.362 +                                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
   1.363 +                                                val _ =  TextIO.closeOut outfile
   1.364 +                                            in 
   1.365 +                                              if (isSome childIncoming) 
   1.366 +                                              then 
   1.367 +                                                  (* check here for prover label on child*)
   1.368 +                                                   
   1.369 +                                                  let val  outfile = TextIO.openOut("child_incoming");  
   1.370 +                                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
   1.371 +                                                val _ =  TextIO.closeOut outfile
   1.372 +                                              val childDone = (case prover of
   1.373 +                                    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd)     ) )
   1.374 +                                                   in
   1.375 +                                                    if childDone      (**********************************************)
   1.376 +                                                    then              (* child has found a proof and transferred it *)
   1.377 +                                                                      (**********************************************)
   1.378 +
   1.379 +                                                       (**********************************************)
   1.380 +                                                       (* Remove this child and go on to check others*)
   1.381 +                                                       (**********************************************)
   1.382 +                                                       ( reap(childPid, childInput, childOutput);
   1.383 +                                                         checkChildren(otherChildren, toParentStr))
   1.384 +                                                    else 
   1.385 +                                                       (**********************************************)
   1.386 +                                                       (* Keep this child and go on to check others  *)
   1.387 +                                                       (**********************************************)
   1.388 +
   1.389 +                                                         (childProc::(checkChildren (otherChildren, toParentStr)))
   1.390 +                                                 end
   1.391 +                                               else
   1.392 +                                                   let val  outfile = TextIO.openOut("child_incoming");  
   1.393 +                                                val _ = TextIO.output (outfile,"No child output " )
   1.394 +                                                val _ =  TextIO.closeOut outfile
   1.395 +                                                 in
   1.396 +                                                    (childProc::(checkChildren (otherChildren, toParentStr)))
   1.397 +                                                 end
   1.398 +                                            end
   1.399 +
   1.400 +                   
   1.401 +                (********************************************************************)                  
   1.402 +                (* call resolution processes                                        *)
   1.403 +                (* settings should be a list of strings                             *)
   1.404 +                (* e.g. ["-t 300", "-m 100000"]                                     *)
   1.405 +                (* takes list of (string, string, string list, string)list proclist *)
   1.406 +                (********************************************************************)
   1.407 +
   1.408 +                   fun execCmds  [] procList = procList
   1.409 +                   |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
   1.410 +                                                     if (prover = "spass") 
   1.411 +                                                     then 
   1.412 +                                                         let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@["-FullRed=0"]@settings@[file]), procList)
   1.413 +                                                         in
   1.414 +                                                            execCmds cmds newProcList
   1.415 +                                                         end
   1.416 +                                                     else 
   1.417 +                                                         let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@settings@[file]), procList)
   1.418 +                                                         in
   1.419 +                                                            execCmds cmds newProcList
   1.420 +                                                         end
   1.421 +
   1.422 +
   1.423 +                (****************************************)                  
   1.424 +                (* call resolution processes remotely   *)
   1.425 +                (* settings should be a list of strings *)
   1.426 +                (* e.g. ["-t 300", "-m 100000"]         *)
   1.427 +                (****************************************)
   1.428 +  
   1.429 +                   fun execRemoteCmds  [] procList = procList
   1.430 +                   |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   1.431 +                                             let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   1.432 +                                                 in
   1.433 +                                                      execRemoteCmds  cmds newProcList
   1.434 +                                                 end
   1.435 +
   1.436 +
   1.437 +                   fun printList (outStr, []) = ()
   1.438 +                   |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   1.439 +
   1.440 +
   1.441 +                (**********************************************)                  
   1.442 +                (* Watcher Loop                               *)
   1.443 +                (**********************************************)
   1.444 +
   1.445 +
   1.446 +
   1.447 +   
   1.448 +                    fun keepWatching (toParentStr, fromParentStr,procList) = 
   1.449 +                          let    fun loop (procList) =  
   1.450 +                                 (
   1.451 +                                 let val cmdsFromIsa = pollParentInput ()
   1.452 +                                      fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
   1.453 +                                                  TextIO.flushOut toParentStr;
   1.454 +                                                   killChildren (map (cmdchildPid) procList);
   1.455 +                                                    ())
   1.456 +                                     
   1.457 +                                 in 
   1.458 +                                    (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   1.459 +                                                                                       (**********************************)
   1.460 +                                    if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
   1.461 +                                         (                                             (**********************************)                             
   1.462 +                                          if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   1.463 +                                          then 
   1.464 +                                            (
   1.465 +                                              let val childPids = map cmdchildPid procList 
   1.466 +                                              in
   1.467 +                                                 killChildren childPids;
   1.468 +                                                 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                       loop ([])
   1.469 +                                              end
   1.470 +                                             )
   1.471 +                                          else
   1.472 +                                            ( 
   1.473 +                                              if ((length procList)<2)    (********************)
   1.474 +                                              then                        (* Execute locally  *)
   1.475 +                                                 (                        (********************)
   1.476 +                                                  let 
   1.477 +                                                    val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.478 +                                                    val parentID = Posix.ProcEnv.getppid()
   1.479 +                                                    val newProcList' =checkChildren (newProcList, toParentStr) 
   1.480 +                                                  in
   1.481 +                                                    (*OS.Process.sleep (Time.fromSeconds 1);*)
   1.482 +                                                    loop (newProcList') 
   1.483 +                                                  end
   1.484 +                                                  )
   1.485 +                                              else                         (************************)
   1.486 +                                                                           (* Execute remotely     *)
   1.487 +                                                  (                        (************************)
   1.488 +                                                  let 
   1.489 +                                                    val newProcList = execRemoteCmds (valOf cmdsFromIsa) procList
   1.490 +                                                    val parentID = Posix.ProcEnv.getppid()
   1.491 +                                                    val newProcList' =checkChildren (newProcList, toParentStr) 
   1.492 +                                                  in
   1.493 +                                                    (*OS.Process.sleep (Time.fromSeconds 1);*)
   1.494 +                                                    loop (newProcList') 
   1.495 +                                                  end
   1.496 +                                                  )
   1.497 +
   1.498 +
   1.499 +
   1.500 +                                              )
   1.501 +                                           )                                              (******************************)
   1.502 +                                    else                                                  (* No new input from Isabelle *)
   1.503 +                                                                                          (******************************)
   1.504 +                                        (    let val newProcList = checkChildren ((procList), toParentStr)
   1.505 +                                             in
   1.506 +                                               OS.Process.sleep (Time.fromSeconds 1);
   1.507 +                                               loop (newProcList)
   1.508 +                                             end
   1.509 +                                         
   1.510 +                                         )
   1.511 +                                  end)
   1.512 +                          in  
   1.513 +                              loop (procList)
   1.514 +                          end
   1.515 +                      
   1.516 +          
   1.517 +                      in
   1.518 +                       (***************************)
   1.519 +                       (*** Sort out pipes ********)
   1.520 +                       (***************************)
   1.521 +
   1.522 +			Posix.IO.close (#outfd p1);
   1.523 +			Posix.IO.close (#infd p2);
   1.524 +			Posix.IO.dup2{old = oldchildin, new = fromParent};
   1.525 +                        Posix.IO.close oldchildin;
   1.526 +			Posix.IO.dup2{old = oldchildout, new = toParent};
   1.527 +                        Posix.IO.close oldchildout;
   1.528 +
   1.529 +                        (***************************)
   1.530 +                        (* start the watcher loop  *)
   1.531 +                        (***************************)
   1.532 +                        keepWatching (toParentStr, fromParentStr, procList);
   1.533 +
   1.534 +
   1.535 +                        (****************************************************************************)
   1.536 +                        (* fake return value - actually want the watcher to loop until killed       *)
   1.537 +                        (****************************************************************************)
   1.538 +                        Posix.Process.wordToPid 0w0
   1.539 +			
   1.540 +		      end);
   1.541 +		(* end case *)
   1.542 +
   1.543 +
   1.544 +          val _ = TextIO.flushOut TextIO.stdOut
   1.545 +
   1.546 +          (*******************************)
   1.547 +          (***  set watcher going ********)
   1.548 +          (*******************************)
   1.549 +
   1.550 +          val procList = []
   1.551 +          val pid = startWatcher (procList)
   1.552 +          (**************************************************)
   1.553 +          (* communication streams to watcher               *)
   1.554 +          (**************************************************)
   1.555 +
   1.556 +	  val instr = openInFD ("_exec_in", #infd p2)
   1.557 +          val outstr = openOutFD ("_exec_out", #outfd p1)
   1.558 +          
   1.559 +          in
   1.560 +           (*******************************)
   1.561 +           (* close the child-side fds    *)
   1.562 +           (*******************************)
   1.563 +            Posix.IO.close (#outfd p2);
   1.564 +            Posix.IO.close (#infd p1);
   1.565 +            (* set the fds close on exec *)
   1.566 +            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   1.567 +            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   1.568 +             
   1.569 +           (*******************************)
   1.570 +           (* return value                *)
   1.571 +           (*******************************)
   1.572 +            PROC{pid = pid,
   1.573 +              instr = instr,
   1.574 +              outstr = outstr
   1.575 +            }
   1.576 +         end;
   1.577 +
   1.578 +
   1.579 +
   1.580 +(**********************************************************)
   1.581 +(* Start a watcher and set up signal handlers             *)
   1.582 +(**********************************************************)
   1.583 +fun killWatcher pid= killChild pid;
   1.584 +
   1.585 +fun createWatcher (the_goal) = let val mychild = childInfo (setupWatcher(the_goal))
   1.586 +			   val streams =snd mychild
   1.587 +                           val childin = fst streams
   1.588 +                           val childout = snd streams
   1.589 +                           val childpid = fst mychild
   1.590 +                           
   1.591 +                           fun vampire_proofHandler (n:int) =
   1.592 +                           (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.593 +                           getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )                   
   1.594 +                          
   1.595 +                          (* fun spass_proofHandler (n:int) = (
   1.596 +                                                      let val (reconstr, thmstring, goalstring) = getSpassInput childin
   1.597 +                                                          val  outfile = TextIO.openOut("foo_signal");
   1.598 +
   1.599 +                                                         val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring))
   1.600 +                                                         val _ =  TextIO.closeOut outfile
   1.601 +                                                      in
   1.602 +                                                         Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.603 +                                                          Pretty.writeln(Pretty.str reconstr) ;
   1.604 +                                                         Pretty.writeln(Pretty.str  (oct_char "361"));
   1.605 +                                                         (*killWatcher childpid;*) () 
   1.606 +                                                      end)*)
   1.607 +
   1.608 +
   1.609 +(*
   1.610 +
   1.611 +fun spass_proofHandler (n:int) = (
   1.612 +                                                      let  val  outfile = TextIO.openOut("foo_signal1");
   1.613 +
   1.614 +                                                         val _ = TextIO.output (outfile, ("In signal handler now\n"))
   1.615 +                                                         val _ =  TextIO.closeOut outfile
   1.616 +                                                          val (reconstr, thmstring, goalstring) = getSpassInput childin
   1.617 +                                                         val  outfile = TextIO.openOut("foo_signal");
   1.618 +
   1.619 +                                                         val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring^goalstring))
   1.620 +                                                         val _ =  TextIO.closeOut outfile
   1.621 +                                                       in
   1.622 +                                                        if ( (substring (reconstr, 0,1))= "[")
   1.623 +                                                         then 
   1.624 +
   1.625 +                                                          let val thm = thm_of_string thmstring
   1.626 +                                                              val clauses = make_clauses [thm]
   1.627 +                                                              val numcls =  zip  (numlist (length clauses)) (map make_meta_clause clauses)
   1.628 +                                                         
   1.629 +                                                          in
   1.630 +                                                             Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.631 +                                                             apply_res_thm reconstr goalstring;
   1.632 +                                                             Pretty.writeln(Pretty.str  (oct_char "361"));
   1.633 +                                                             killWatcher childpid; () 
   1.634 +                                                          end
   1.635 +                                                       else
   1.636 +                                                           Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.637 +                                                              Pretty.writeln(Pretty.str (goalstring^reconstr));
   1.638 +                                                             Pretty.writeln(Pretty.str  (oct_char "361"));
   1.639 +                                                             (*killWatcher childpid; *) reap (childpid,childin, childout);()   
   1.640 +                                                      end )
   1.641 +*)
   1.642 +
   1.643 +fun spass_proofHandler (n:int) = (
   1.644 +                                 let  val  outfile = TextIO.openOut("foo_signal1");
   1.645 +                                      val _ = TextIO.output (outfile, ("In signal handler now\n"))
   1.646 +                                      val _ =  TextIO.closeOut outfile
   1.647 +                                      val (reconstr, thmstring, goalstring) = getSpassInput childin
   1.648 +                                      val  outfile = TextIO.openAppend("foo_signal");
   1.649 +
   1.650 +                                      val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   1.651 +                                      val _ =  TextIO.closeOut outfile
   1.652 +                                      in          (* if a proof has been found and sent back as a reconstruction proof *)
   1.653 +                                                  if ( (substring (reconstr, 0,1))= "[")
   1.654 +                                                  then 
   1.655 +
   1.656 +                                                            (
   1.657 +                                                                 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.658 +                                                                 apply_res_thm reconstr goalstring;
   1.659 +                                                                 Pretty.writeln(Pretty.str  (oct_char "361"));
   1.660 +                                                                 
   1.661 +                                                                 goals_being_watched := ((!goals_being_watched) - 1);
   1.662 +                                                         
   1.663 +                                                                 if ((!goals_being_watched) = 0)
   1.664 +                                                                 then 
   1.665 +                                                                    (let val  outfile = TextIO.openOut("foo_reap_found");
   1.666 +                                                                         val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.667 +                                                                         val _ =  TextIO.closeOut outfile
   1.668 +                                                                     in
   1.669 +                                                                         reap (childpid,childin, childout); ()
   1.670 +                                                                     end)
   1.671 +                                                                 else
   1.672 +                                                                    ()
   1.673 +                                                            )
   1.674 +                                                    (* if there's no proof, but a message from Spass *)
   1.675 +                                                    else if ((substring (reconstr, 0,5))= "SPASS")
   1.676 +                                                         then
   1.677 +                                                                 (
   1.678 +                                                                     goals_being_watched := (!goals_being_watched) -1;
   1.679 +                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.680 +                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
   1.681 +                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   1.682 +                                                                      if (!goals_being_watched = 0)
   1.683 +                                                                      then 
   1.684 +                                                                          (let val  outfile = TextIO.openOut("foo_reap_comp");
   1.685 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.686 +                                                                               val _ =  TextIO.closeOut outfile
   1.687 +                                                                           in
   1.688 +                                                                              reap (childpid,childin, childout); ()
   1.689 +                                                                           end )
   1.690 +                                                                      else
   1.691 +                                                                         ()
   1.692 +                                                                )
   1.693 +                                                          (* if proof translation failed *)
   1.694 +                                                          else if ((substring (reconstr, 0,5)) = "Proof")
   1.695 +                                                               then 
   1.696 +                                                                   (
   1.697 +                                                                     goals_being_watched := (!goals_being_watched) -1;
   1.698 +                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.699 +                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
   1.700 +                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   1.701 +                                                                      if (!goals_being_watched = 0)
   1.702 +                                                                      then 
   1.703 +                                                                          (let val  outfile = TextIO.openOut("foo_reap_comp");
   1.704 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.705 +                                                                               val _ =  TextIO.closeOut outfile
   1.706 +                                                                           in
   1.707 +                                                                              reap (childpid,childin, childout); ()
   1.708 +                                                                           end )
   1.709 +                                                                      else
   1.710 +                                                                         ()
   1.711 +                                                                )
   1.712 +
   1.713 +
   1.714 +                                                                else  (* add something here ?*)
   1.715 +                                                                   ()
   1.716 +                                                             
   1.717 +                                       end)
   1.718 +
   1.719 +
   1.720 +                        
   1.721 +                       in 
   1.722 +                          Signal.signal (Posix.Signal.usr1, Signal.SIG_HANDLE vampire_proofHandler);
   1.723 +                          Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE spass_proofHandler);
   1.724 +                          (childin, childout, childpid)
   1.725 +
   1.726 +                       end
   1.727 +
   1.728 +
   1.729 +
   1.730 +
   1.731 +
   1.732 +end (* structure Watcher *)