src/HOL/Tools/ATP/watcher.ML
author wenzelm
Sun Jun 05 11:31:23 2005 +0200 (2005-06-05)
changeset 16260 4a1f36eafe17
parent 16185 bb71c91e781e
child 16357 f1275d2a1dee
permissions -rw-r--r--
File.platform_path vs. File.shell_path;
     1 (*  Title:      Watcher.ML
     2 
     3     ID:         $Id$
     4     Author:     Claire Quigley
     5     Copyright   2004  University of Cambridge
     6  *)
     7 
     8  (***************************************************************************)
     9  (*  The watcher process starts a resolution process when it receives a     *)
    10 (*  message from Isabelle                                                  *)
    11 (*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    12 (*  and removes dead processes.  Also possible to kill all the resolution  *)
    13 (*  processes currently running.                                           *)
    14 (*  Hardwired version of where to pick up the tptp files for the moment    *)
    15 (***************************************************************************)
    16 
    17 (*use "Proof_Transfer";
    18 use "VampireCommunication";
    19 use "SpassCommunication";*)
    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 (*  The result of calling createWatcher  *)
    30 (*****************************************)
    31 
    32 datatype proc = PROC of {
    33         pid : Posix.Process.pid,
    34         instr : TextIO.instream,
    35         outstr : TextIO.outstream
    36       };
    37 
    38 (*****************************************)
    39 (*  The result of calling executeToList  *)
    40 (*****************************************)
    41 
    42 datatype cmdproc = CMDPROC of {
    43         prover: string,             (* Name of the resolution prover used, e.g. Vampire, SPASS *)
    44         cmd:  string,              (* The file containing the goal for res prover to prove *)     
    45         thmstring: string,         (* string representation of subgoal after negation, skolemization*) 
    46         goalstring: string,         (* string representation of subgoal*) 
    47         proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    48         instr : TextIO.instream,   (*  Input stream to child process *)
    49         outstr : TextIO.outstream  (*  Output stream from child process *)
    50       };
    51 
    52 type signal = Posix.Signal.signal
    53 datatype exit_status = datatype Posix.Process.exit_status
    54 
    55 val fromStatus = Posix.Process.fromStatus
    56 
    57 
    58 fun reap(pid, instr, outstr) =
    59         let
    60 		val u = TextIO.closeIn instr;
    61 	        val u = TextIO.closeOut outstr;
    62 	
    63 		val (_, status) =
    64 			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    65 	in
    66 		status
    67 	end
    68 
    69 fun fdReader (name : string, fd : Posix.IO.file_desc) =
    70 	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    71 
    72 fun fdWriter (name, fd) =
    73           Posix.IO.mkTextWriter {
    74 	      appendMode = false,
    75               initBlkMode = true,
    76               name = name,  
    77               chunkSize=4096,
    78               fd = fd
    79             };
    80 
    81 fun openOutFD (name, fd) =
    82 	  TextIO.mkOutstream (
    83 	    TextIO.StreamIO.mkOutstream (
    84 	      fdWriter (name, fd), IO.BLOCK_BUF));
    85 
    86 fun openInFD (name, fd) =
    87 	  TextIO.mkInstream (
    88 	    TextIO.StreamIO.mkInstream (
    89 	      fdReader (name, fd), ""));
    90 
    91 
    92 
    93 
    94 
    95 fun killChild child_handle = Unix.reap child_handle 
    96 
    97 fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
    98 
    99 fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
   100 
   101 fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
   102 
   103 fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = (prover,(cmd, (instr,outstr)));
   104 
   105 fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = proc_handle;
   106 
   107 fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (prover);
   108 
   109 fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (thmstring);
   110 
   111 fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (goalstring);
   112 
   113 fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
   114 
   115 (********************************************************************************************)
   116 (*  takes a list of arguments and sends them individually to the watcher process by pipe    *)
   117 (********************************************************************************************)
   118 
   119 fun outputArgs (toWatcherStr, []) = ()
   120 |   outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); 
   121                                           TextIO.flushOut toWatcherStr;
   122                                          outputArgs (toWatcherStr, xs))
   123 
   124 (********************************************************************************)
   125 (*    gets individual args from instream and concatenates them into a list      *)
   126 (********************************************************************************)
   127 
   128 fun getArgs (fromParentStr, toParentStr,ys) =  let 
   129                                        val thisLine = TextIO.input fromParentStr
   130                                     in
   131                                         ((ys@[thisLine]))
   132                                     end
   133 
   134 (********************************************************************************)
   135 (*  Remove the \n character from the end of each filename                       *)
   136 (********************************************************************************)
   137 
   138 fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
   139                     in
   140                         if (String.isPrefix "\n"  (implode backList )) 
   141                         then (implode (rev ((tl backList))))
   142                         else cmdStr
   143                     end
   144                             
   145 (********************************************************************************)
   146 (*  Send request to Watcher for a vampire to be called for filename in arg      *)
   147 (********************************************************************************)
   148                     
   149 fun callResProver (toWatcherStr,  arg) = (sendOutput (toWatcherStr, arg^"\n"); 
   150                                      TextIO.flushOut toWatcherStr)
   151 
   152 (*****************************************************************************************)
   153 (*  Send request to Watcher for multiple provers to be called for filenames in arg      *)
   154 (*****************************************************************************************)
   155 
   156 (* need to modify to send over hyps file too *)
   157 fun callResProvers (toWatcherStr,  []) =
   158       (sendOutput (toWatcherStr, "End of calls\n"); 
   159        TextIO.flushOut toWatcherStr)
   160 |   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) =
   161       let val dfg_dir = File.tmp_path (Path.basic "dfg"); 
   162 	 (*** need to check here if the directory exists and, if not, create it***)
   163 	  val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))                                                                     
   164 	              (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n")
   165 	 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
   166 	 val probID = ReconOrderClauses.last(explode probfile)
   167 	  val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
   168 	  (*** only include problem and clasimp for the moment, not sure how to refer to ***)
   169 
   170 	  (*** hyps/local axioms just now (*,axfile, hypsfile,*)                                               ***)
   171 	  val whole_prob_file = system ("cat " ^ clasimpfile ^" "^ probfile ^ " > " ^ File.shell_path wholefile)
   172 
   173 	  val dfg_create = if File.exists dfg_dir 
   174 			   then warning("dfg dir exists")
   175 			   else File.mkdir dfg_dir; 
   176 	  
   177 	  val dfg_path = File.platform_path dfg_dir;
   178 	 (* val exec_tptp2x = 
   179 	        Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X",  
   180 	                     ["-fdfg", "-d " ^ dfg_path, File.platform_path wholefile]) *)
   181         val tptp_home = getenv "TPTP2X_HOME" ^ "/tptp2X"
   182        
   183         val systemcall = system (tptp_home ^ " -fdfg -d " ^ File.shell_path dfg_dir ^ " " ^ File.shell_path wholefile)
   184         val _ =  warning("systemcall is "^ (string_of_int systemcall))
   185 	(*val _ = Posix.Process.wait ()*)
   186 	(*val _ =Unix.reap exec_tptp2x*)
   187 	  val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
   188  
   189        in   
   190 	  goals_being_watched := (!goals_being_watched) + 1;
   191 	  Posix.Process.sleep(Time.fromSeconds 1); 
   192 	  (warning ("probfile is: "^probfile));
   193 	  (warning("dfg file is: "^newfile));
   194 	  (warning ("wholefile is: "^(File.platform_path wholefile)));
   195 	  sendOutput (toWatcherStr,
   196 	       prover ^ "*" ^ thmstring ^ "*" ^ goalstring ^ "*" ^ proverCmd ^ 
   197 	       "*" ^ settings ^ "*" ^ newfile ^ "\n");
   198  (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
   199 	  TextIO.flushOut toWatcherStr;
   200 	  (*Unix.reap exec_tptp2x;*)
   201 	  if File.exists
   202 	        (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg")))
   203 	  then callResProvers (toWatcherStr, args)
   204 	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^
   205 	              " -fdfg " ^ File.platform_path wholefile ^ " -d " ^ dfg_path)
   206       end
   207 (*
   208 fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
   209                                      
   210 |   callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile, probfile)::args) =
   211                                             ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^clasimpfile^"*"^axfile^"*"^hypsfile^"*"^probfile^"\n")
   212                                             
   213      *)                                      
   214  
   215 (**************************************************************)
   216 (* Send message to watcher to kill currently running vampires *)
   217 (**************************************************************)
   218 
   219 fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 
   220                             TextIO.flushOut toWatcherStr)
   221 
   222 
   223 
   224 (**************************************************************)
   225 (* Remove \n token from a vampire goal filename and extract   *)
   226 (* prover, proverCmd, settings and file from input string     *)
   227 (**************************************************************)
   228 
   229 
   230  fun takeUntil ch [] res  = (res, [])
   231  |   takeUntil ch (x::xs) res = if   x = ch 
   232                                 then
   233                                      (res, xs)
   234                                 else
   235                                      takeUntil ch xs (res@[x])
   236 
   237  fun getSettings [] settings = settings
   238 |    getSettings (xs) settings = let val (set, rest ) = takeUntil "%" xs []
   239                                  in
   240                                      getSettings rest (settings@[(implode set)])
   241                                  end
   242 
   243 fun separateFields str =
   244   let val (prover, rest) = takeUntil "*" str []
   245       val prover = implode prover
   246       val (thmstring, rest) =  takeUntil "*" rest []
   247       val thmstring = implode thmstring
   248       val (goalstring, rest) =  takeUntil "*" rest []
   249       val goalstring = implode goalstring
   250       val (proverCmd, rest ) =  takeUntil "*" rest []
   251       val proverCmd = implode proverCmd
   252       
   253       val (settings, rest) =  takeUntil "*" rest []
   254       val settings = getSettings settings []
   255       val (file, rest) =  takeUntil "*" rest []
   256       val file = implode file
   257       val _ = File.write (File.tmp_path (Path.basic "sep_comms"))
   258                 (prover^thmstring^goalstring^proverCmd^file) 
   259   in
   260      (prover,thmstring,goalstring, proverCmd, settings, file)
   261   end
   262 
   263  
   264 
   265  fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
   266                      in
   267 
   268                          if (String.isPrefix "\n"  (implode backList )) 
   269                          then 
   270                              separateFields ((rev ((tl backList))))
   271                          else
   272                            (separateFields (explode cmdStr))
   273                      end
   274                       
   275 
   276 fun getProofCmd (a,b,c,d,e,f) = d
   277 
   278 
   279 (**************************************************************)
   280 (* Get commands from Isabelle                                 *)
   281 (**************************************************************)
   282 
   283 fun getCmds (toParentStr,fromParentStr, cmdList) = 
   284        let val thisLine = TextIO.inputLine fromParentStr 
   285        in
   286 	  (if (thisLine = "End of calls\n") 
   287 	   then 
   288 	      (cmdList)
   289 	   else if (thisLine = "Kill children\n") 
   290 		then 
   291 		    (   TextIO.output (toParentStr,thisLine ); 
   292 			TextIO.flushOut toParentStr;
   293 		      (("","","","Kill children",[],"")::cmdList)
   294 		     )
   295 	      else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   296 		    in
   297 		      (*TextIO.output (toParentStr, thisCmd); 
   298 			TextIO.flushOut toParentStr;*)
   299 			getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
   300 		    end
   301 		    )
   302 	    )
   303 	end
   304                                     
   305                                     
   306 (**************************************************************)
   307 (*  Get Io-descriptor for polling of an input stream          *)
   308 (**************************************************************)
   309 
   310 
   311 fun getInIoDesc someInstr = 
   312     let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   313         val _ = TextIO.output (TextIO.stdOut, buf)
   314         val ioDesc = 
   315 	    case rd
   316 	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
   317 	       | _ => NONE
   318      in (* since getting the reader will have terminated the stream, we need
   319 	 * to build a new stream. *)
   320 	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
   321 	ioDesc
   322     end
   323 
   324 
   325 (*************************************)
   326 (*  Set up a Watcher Process         *)
   327 (*************************************)
   328 
   329 
   330 
   331 fun setupWatcher (thm,clause_arr, num_of_clauses) = 
   332   let
   333     (** pipes for communication between parent and watcher **)
   334     val p1 = Posix.IO.pipe ()
   335     val p2 = Posix.IO.pipe ()
   336     fun closep () = (
   337 	  Posix.IO.close (#outfd p1); 
   338 	  Posix.IO.close (#infd p1);
   339 	  Posix.IO.close (#outfd p2); 
   340 	  Posix.IO.close (#infd p2)
   341 	)
   342     (***********************************************************)
   343     (****** fork a watcher process and get it set up and going *)
   344     (***********************************************************)
   345     fun startWatcher (procList) =
   346 	     (case  Posix.Process.fork() (***************************************)
   347 	   of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   348 					 (***************************************)
   349 
   350 					   (*************************)
   351 	    | NONE => let                  (* child - i.e. watcher  *)
   352 		val oldchildin = #infd p1  (*************************)
   353 		val fromParent = Posix.FileSys.wordToFD 0w0
   354 		val oldchildout = #outfd p2
   355 		val toParent = Posix.FileSys.wordToFD 0w1
   356 		val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   357 		val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   358 		val toParentStr = openOutFD ("_exec_out_parent", toParent)
   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 startWatcher: "^prems_string));
   363 	       (* tracing *)
   364 	      (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
   365 		val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
   366 		val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
   367 		val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
   368 		val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
   369 		val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
   370 			 *)
   371 		(*val goalstr = string_of_thm (the_goal)
   372 		 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher")));  
   373 		val _ = TextIO.output (outfile,goalstr )
   374 		val _ =  TextIO.closeOut outfile*)
   375 		fun killChildren [] = ()
   376 	     |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
   377 
   378 	       
   379      
   380 	      (*************************************************************)
   381 	      (* take an instream and poll its underlying reader for input *)
   382 	      (*************************************************************)
   383 
   384 	      fun pollParentInput () = 
   385 		     
   386 			 let val pd = OS.IO.pollDesc (fromParentIOD)
   387 			 in 
   388 			 if (isSome pd ) then 
   389 			     let val pd' = OS.IO.pollIn (valOf pd)
   390 				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   391 			     in
   392 				if null pdl 
   393 				then
   394 				   NONE
   395 				else if (OS.IO.isIn (hd pdl)) 
   396 				     then
   397 					(SOME ( getCmds (toParentStr, fromParentStr, [])))
   398 				     else
   399 					 NONE
   400 			     end
   401 			   else
   402 			       NONE
   403 			   end
   404 		      
   405 	     
   406 
   407 	       fun pollChildInput (fromStr) = 
   408 		     let val iod = getInIoDesc fromStr
   409 		     in 
   410 		     if isSome iod 
   411 		     then 
   412 			 let val pd = OS.IO.pollDesc (valOf iod)
   413 			 in 
   414 			 if (isSome pd ) then 
   415 			     let val pd' = OS.IO.pollIn (valOf pd)
   416 				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   417 			     in
   418 				if null pdl 
   419 				then
   420 				   NONE
   421 				else if (OS.IO.isIn (hd pdl)) 
   422 				     then
   423 					 SOME (getCmd (TextIO.inputLine fromStr))
   424 				     else
   425 					 NONE
   426 			     end
   427 			   else
   428 			       NONE
   429 			   end
   430 		       else 
   431 			   NONE
   432 		      end
   433 
   434 
   435 	     (****************************************************************************)
   436 	     (* Check all vampire processes currently running for output                 *)
   437 	     (****************************************************************************) 
   438 							(*********************************)
   439 	      fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   440 							(*********************************)
   441 	      |   checkChildren ((childProc::otherChildren), toParentStr) = 
   442 		    let val (childInput,childOutput) =  cmdstreamsOf childProc
   443 			val child_handle= cmdchildHandle childProc
   444 			(* childCmd is the .dfg file that the problem is in *)
   445 			val childCmd = fst(snd (cmdchildInfo childProc))
   446 			(* now get the number of the subgoal from the filename *)
   447 			val sg_num = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
   448 			val childIncoming = pollChildInput childInput
   449 			val parentID = Posix.ProcEnv.getppid()
   450 			val prover = cmdProver childProc
   451 			val thmstring = cmdThm childProc
   452 			val sign = sign_of_thm thm
   453 			val prems = prems_of thm
   454 			val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   455 			val _ = warning("subgoals forked to checkChildren: "^prems_string)
   456 			val goalstring = cmdGoal childProc							
   457 			val _ = File.write (File.tmp_path (Path.basic "child_comms")) 
   458 			           (prover^thmstring^goalstring^childCmd)
   459 		    in 
   460 		      if (isSome childIncoming) 
   461 		      then 
   462 			  (* check here for prover label on child*)
   463 			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))  ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) 
   464 		      val childDone = (case prover of
   465 	    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   466 			   in
   467 			    if childDone      (**********************************************)
   468 			    then              (* child has found a proof and transferred it *)
   469 					      (**********************************************)
   470 
   471 			       (**********************************************)
   472 			       (* Remove this child and go on to check others*)
   473 			       (**********************************************)
   474 			       ( Unix.reap child_handle;
   475 				 checkChildren(otherChildren, toParentStr))
   476 			    else 
   477 			       (**********************************************)
   478 			       (* Keep this child and go on to check others  *)
   479 			       (**********************************************)
   480 
   481 				 (childProc::(checkChildren (otherChildren, toParentStr)))
   482 			 end
   483 		       else
   484 			 (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   485 			  childProc::(checkChildren (otherChildren, toParentStr)))
   486 		    end
   487 
   488 	     
   489 	  (********************************************************************)                  
   490 	  (* call resolution processes                                        *)
   491 	  (* settings should be a list of strings                             *)
   492 	  (* e.g. ["-t 300", "-m 100000"]                                     *)
   493 	  (* takes list of (string, string, string list, string)list proclist *)
   494 	  (********************************************************************)
   495 
   496 
   497 (*** add subgoal id num to this *)
   498 	     fun execCmds  [] procList = procList
   499 	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
   500 		   if (prover = "spass") 
   501 		   then 
   502 		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   503 			   val (instr, outstr)=Unix.streamsOf childhandle
   504 			   val newProcList =    (((CMDPROC{
   505 						prover = prover,
   506 						cmd = file,
   507 						thmstring = thmstring,
   508 						goalstring = goalstring,
   509 						proc_handle = childhandle,
   510 						instr = instr,
   511 						outstr = outstr })::procList))
   512 			    val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:"^goalstring^proverCmd^(concat settings)^file)
   513 		       in
   514 			  execCmds cmds newProcList
   515 		       end
   516 		   else 
   517 		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   518 			   val (instr, outstr)=Unix.streamsOf childhandle
   519 			   val newProcList =    (((CMDPROC{
   520 						prover = prover,
   521 						cmd = file,
   522 						thmstring = thmstring,
   523 						goalstring = goalstring,
   524 						proc_handle = childhandle,
   525 						instr = instr,
   526 						outstr = outstr })::procList))
   527 		       in
   528 			  execCmds cmds newProcList
   529 		       end
   530 
   531 
   532 
   533 	  (****************************************)                  
   534 	  (* call resolution processes remotely   *)
   535 	  (* settings should be a list of strings *)
   536 	  (* e.g. ["-t 300", "-m 100000"]         *)
   537 	  (****************************************)
   538 
   539 	   (*  fun execRemoteCmds  [] procList = procList
   540 	     |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   541 				       let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   542 					   in
   543 						execRemoteCmds  cmds newProcList
   544 					   end
   545 *)
   546 
   547 	     fun printList (outStr, []) = ()
   548 	     |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   549 
   550 
   551 	  (**********************************************)                  
   552 	  (* Watcher Loop                               *)
   553 	  (**********************************************)
   554 
   555 
   556 
   557 
   558 	      fun keepWatching (toParentStr, fromParentStr,procList) = 
   559 		    let    fun loop (procList) =  
   560 			   (
   561 			   let val cmdsFromIsa = pollParentInput ()
   562 			       fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
   563 					    TextIO.flushOut toParentStr;
   564 					     killChildren (map (cmdchildHandle) procList);
   565 					      ())
   566 			       
   567 			   in 
   568 			      (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   569 										 (**********************************)
   570 			      if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
   571 				   (                                             (**********************************)                             
   572 				    if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   573 				    then 
   574 				      (
   575 					let val child_handles = map cmdchildHandle procList 
   576 					in
   577 					   killChildren child_handles;
   578 					   (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                                              loop ([])
   579 					end
   580 					   
   581 				       )
   582 				    else
   583 				      ( 
   584 					if ((length procList)<10)    (********************)
   585 					then                        (* Execute locally  *)
   586 					   (                        (********************)
   587 					    let 
   588 					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   589 					      val parentID = Posix.ProcEnv.getppid()
   590 					      val newProcList' =checkChildren (newProcList, toParentStr) 
   591 					    in
   592 					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   593 					      loop (newProcList') 
   594 					    end
   595 					    )
   596 					else                         (*********************************)
   597 								     (* Execute remotely              *)
   598 								     (* (actually not remote for now )*)
   599 					    (                        (*********************************)
   600 					    let 
   601 					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   602 					      val parentID = Posix.ProcEnv.getppid()
   603 					      val newProcList' =checkChildren (newProcList, toParentStr) 
   604 					    in
   605 					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   606 					      loop (newProcList') 
   607 					    end
   608 					    )
   609 
   610 
   611 
   612 					)
   613 				     )                                              (******************************)
   614 			      else                                                  (* No new input from Isabelle *)
   615 										    (******************************)
   616 				  (    let val newProcList = checkChildren ((procList), toParentStr)
   617 				       in
   618 					 Posix.Process.sleep (Time.fromSeconds 1);
   619 					 loop (newProcList)
   620 				       end
   621 				   
   622 				   )
   623 			    end)
   624 		    in  
   625 			loop (procList)
   626 		    end
   627 		
   628     
   629 		in
   630 		 (***************************)
   631 		 (*** Sort out pipes ********)
   632 		 (***************************)
   633 
   634 		  Posix.IO.close (#outfd p1);
   635 		  Posix.IO.close (#infd p2);
   636 		  Posix.IO.dup2{old = oldchildin, new = fromParent};
   637 		  Posix.IO.close oldchildin;
   638 		  Posix.IO.dup2{old = oldchildout, new = toParent};
   639 		  Posix.IO.close oldchildout;
   640 
   641 		  (***************************)
   642 		  (* start the watcher loop  *)
   643 		  (***************************)
   644 		  keepWatching (toParentStr, fromParentStr, procList);
   645 
   646 
   647 		  (****************************************************************************)
   648 		  (* fake return value - actually want the watcher to loop until killed       *)
   649 		  (****************************************************************************)
   650 		  Posix.Process.wordToPid 0w0
   651 		  
   652 		end);
   653 	  (* end case *)
   654 
   655 
   656     val _ = TextIO.flushOut TextIO.stdOut
   657 
   658     (*******************************)
   659     (***  set watcher going ********)
   660     (*******************************)
   661 
   662     val procList = []
   663     val pid = startWatcher (procList)
   664     (**************************************************)
   665     (* communication streams to watcher               *)
   666     (**************************************************)
   667 
   668     val instr = openInFD ("_exec_in", #infd p2)
   669     val outstr = openOutFD ("_exec_out", #outfd p1)
   670     
   671     in
   672      (*******************************)
   673      (* close the child-side fds    *)
   674      (*******************************)
   675       Posix.IO.close (#outfd p2);
   676       Posix.IO.close (#infd p1);
   677       (* set the fds close on exec *)
   678       Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   679       Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   680        
   681      (*******************************)
   682      (* return value                *)
   683      (*******************************)
   684       PROC{pid = pid,
   685 	instr = instr,
   686 	outstr = outstr
   687       }
   688    end;
   689 
   690 
   691 
   692 (**********************************************************)
   693 (* Start a watcher and set up signal handlers             *)
   694 (**********************************************************)
   695 
   696 fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   697 
   698 fun reapWatcher(pid, instr, outstr) =
   699         let
   700 		val u = TextIO.closeIn instr;
   701 	        val u = TextIO.closeOut outstr;
   702 	
   703 		val (_, status) =
   704 			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
   705 	in
   706 		status
   707 	end
   708 
   709 
   710 fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   711 			   val streams =snd mychild
   712                            val childin = fst streams
   713                            val childout = snd streams
   714                            val childpid = fst mychild
   715                            val sign = sign_of_thm thm
   716                            val prems = prems_of thm
   717                            val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   718                            val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   719                            fun vampire_proofHandler (n) =
   720                            (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   721                            getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
   722                           
   723 
   724 fun spass_proofHandler (n) = (
   725                                  let  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
   726                                       val _ = TextIO.output (outfile, ("In signal handler now\n"))
   727                                       val _ =  TextIO.closeOut outfile
   728                                       val (reconstr, thmstring, goalstring) = SpassComm.getSpassInput childin
   729                                       val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
   730 
   731                                       val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   732                                       val _ =  TextIO.closeOut outfile
   733                                       in          (* if a proof has been found and sent back as a reconstruction proof *)
   734                                                   if ( (substring (reconstr, 0,1))= "[")
   735                                                   then 
   736 
   737                                                             (
   738                                                                  Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   739                                                                  Recon_Transfer.apply_res_thm reconstr goalstring;
   740                                                                  Pretty.writeln(Pretty.str  (oct_char "361"));
   741                                                                  
   742                                                                  goals_being_watched := ((!goals_being_watched) - 1);
   743                                                          
   744                                                                  if ((!goals_being_watched) = 0)
   745                                                                  then 
   746                                                                     (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found")));
   747                                                                          val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   748                                                                          val _ =  TextIO.closeOut outfile
   749                                                                      in
   750                                                                          killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   751                                                                      end)
   752                                                                  else
   753                                                                     ()
   754                                                             )
   755                                                     (* if there's no proof, but a message from Spass *)
   756                                                     else if ((substring (reconstr, 0,5))= "SPASS")
   757                                                          then
   758                                                                  (
   759                                                                      goals_being_watched := (!goals_being_watched) -1;
   760                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   761                                                                       Pretty.writeln(Pretty.str (goalstring^reconstr));
   762                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   763                                                                       if (!goals_being_watched = 0)
   764                                                                       then 
   765                                                                           (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   766                                                                                val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   767                                                                                val _ =  TextIO.closeOut outfile
   768                                                                            in
   769                                                                               killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   770                                                                            end )
   771                                                                       else
   772                                                                          ()
   773                                                                 ) 
   774 						   (* print out a list of rules used from clasimpset*)
   775                                                     else if ((substring (reconstr, 0,5))= "Rules")
   776                                                          then
   777                                                                  (
   778                                                                      goals_being_watched := (!goals_being_watched) -1;
   779                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   780                                                                       Pretty.writeln(Pretty.str (goalstring^reconstr));
   781                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   782                                                                       if (!goals_being_watched = 0)
   783                                                                       then 
   784                                                                           (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   785                                                                                val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   786                                                                                val _ =  TextIO.closeOut outfile
   787                                                                            in
   788                                                                               killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   789                                                                            end )
   790                                                                       else
   791                                                                          ()
   792                                                                 )
   793 							
   794                                                           (* if proof translation failed *)
   795                                                           else if ((substring (reconstr, 0,5)) = "Proof")
   796                                                                then 
   797                                                                    (
   798                                                                      goals_being_watched := (!goals_being_watched) -1;
   799                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   800                                                                       Pretty.writeln(Pretty.str (goalstring^reconstr));
   801                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   802                                                                       if (!goals_being_watched = 0)
   803                                                                       then 
   804                                                                           (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   805                                                                                val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   806                                                                                val _ =  TextIO.closeOut outfile
   807                                                                            in
   808                                                                               killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   809                                                                            end )
   810                                                                       else
   811                                                                          ()
   812                                                                 )
   813 
   814 
   815                                                                 else  (* add something here ?*)
   816                                                                    ()
   817                                                              
   818                                        end)
   819 
   820 
   821                         
   822                        in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   823                           IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   824                           (childin, childout, childpid)
   825 
   826 
   827   end
   828 
   829 
   830 
   831 
   832 
   833 end (* structure Watcher *)