src/HOL/Tools/ATP/watcher.ML
changeset 17216 df66d8feec63
parent 17150 ce2a1aeb42aa
child 17231 f42bc4f7afdf
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Sep 01 00:46:14 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Sep 01 11:45:54 2005 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Watcher.ML
     1.5 -
     1.6      ID:         $Id$
     1.7      Author:     Claire Quigley
     1.8      Copyright   2004  University of Cambridge
     1.9 @@ -90,10 +89,6 @@
    1.10  	    TextIO.StreamIO.mkInstream (
    1.11  	      fdReader (name, fd), ""));
    1.12  
    1.13 -
    1.14 -
    1.15 -
    1.16 -
    1.17  fun killChild child_handle = Unix.reap child_handle 
    1.18  
    1.19  fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
    1.20 @@ -199,17 +194,16 @@
    1.21  
    1.22  
    1.23   fun takeUntil ch [] res  = (res, [])
    1.24 - |   takeUntil ch (x::xs) res = if   x = ch 
    1.25 -                                then
    1.26 -                                     (res, xs)
    1.27 -                                else
    1.28 -                                     takeUntil ch xs (res@[x])
    1.29 + |   takeUntil ch (x::xs) res = 
    1.30 +        if   x = ch then (res, xs)
    1.31 +	else takeUntil ch xs (res@[x])
    1.32  
    1.33   fun getSettings [] settings = settings
    1.34 -|    getSettings (xs) settings = let val (set, rest ) = takeUntil "%" xs []
    1.35 -                                 in
    1.36 -                                     getSettings rest (settings@[(implode set)])
    1.37 -                                 end
    1.38 +|    getSettings (xs) settings = 
    1.39 +       let val (set, rest ) = takeUntil "%" xs []
    1.40 +       in
    1.41 +	   getSettings rest (settings@[(implode set)])
    1.42 +       end
    1.43  
    1.44  fun separateFields str =
    1.45    let val  outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field")))                                                                         
    1.46 @@ -440,8 +434,6 @@
    1.47  		fun killChildren [] = ()
    1.48  	     |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
    1.49  
    1.50 -	       
    1.51 -     
    1.52  	      (*************************************************************)
    1.53  	      (* take an instream and poll its underlying reader for input *)
    1.54  	      (*************************************************************)
    1.55 @@ -469,44 +461,38 @@
    1.56  		 end
    1.57  		      
    1.58  	       fun pollChildInput (fromStr) = 
    1.59 -
    1.60 -		     let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
    1.61 -			           ("In child_poll\n")
    1.62 -                       val iod = getInIoDesc fromStr
    1.63 +		 let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
    1.64 +			       ("In child_poll\n")
    1.65 +		     val iod = getInIoDesc fromStr
    1.66 +		 in 
    1.67 +		   if isSome iod 
    1.68 +		   then 
    1.69 +		     let val pd = OS.IO.pollDesc (valOf iod)
    1.70  		     in 
    1.71 -
    1.72 -		 
    1.73 -
    1.74 -		     if isSome iod 
    1.75 -		     then 
    1.76 -			 let val pd = OS.IO.pollDesc (valOf iod)
    1.77 -			 in 
    1.78 -			 if (isSome pd ) then 
    1.79 -			     let val pd' = OS.IO.pollIn (valOf pd)
    1.80 -				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
    1.81 -                                 
    1.82 -			     in
    1.83 -				if null pdl 
    1.84 -				then
    1.85 -				  ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
    1.86 -			           ("Null pdl \n");NONE)
    1.87 -				else if (OS.IO.isIn (hd pdl)) 
    1.88 -				     then
    1.89 -					 (let val inval =  (TextIO.inputLine fromStr)
    1.90 -                              	              val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
    1.91 -					  in
    1.92 -						SOME inval
    1.93 -					  end)
    1.94 -				     else
    1.95 -					   ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
    1.96 -			           ("Null pdl \n");NONE)
    1.97 -			     end
    1.98 -			   else
    1.99 -			       NONE
   1.100 -			   end
   1.101 -		       else 
   1.102 -			   NONE
   1.103 -		 end
   1.104 +		     if (isSome pd ) then 
   1.105 +			 let val pd' = OS.IO.pollIn (valOf pd)
   1.106 +			     val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   1.107 +			     
   1.108 +			 in
   1.109 +			    if null pdl 
   1.110 +			    then
   1.111 +			      ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
   1.112 +			       ("Null pdl \n");NONE)
   1.113 +			    else if (OS.IO.isIn (hd pdl)) 
   1.114 +				 then
   1.115 +				     (let val inval =  (TextIO.inputLine fromStr)
   1.116 +					  val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
   1.117 +				      in
   1.118 +					    SOME inval
   1.119 +				      end)
   1.120 +				 else
   1.121 +				       ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
   1.122 +			       ("Null pdl \n");NONE)
   1.123 +			 end
   1.124 +		       else  NONE
   1.125 +		       end
   1.126 +		   else NONE
   1.127 +	     end
   1.128  
   1.129  
   1.130  	     (****************************************************************************)
   1.131 @@ -554,20 +540,16 @@
   1.132                                   |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   1.133  			   in
   1.134  			    if childDone      (**********************************************)
   1.135 -			    then              (* child has found a proof and transferred it *)
   1.136 -					      (**********************************************)
   1.137 -
   1.138 -			       (**********************************************)
   1.139 +			    then (* child has found a proof and transferred it *)
   1.140  			       (* Remove this child and go on to check others*)
   1.141  			       (**********************************************)
   1.142 -			       ( Unix.reap child_handle;
   1.143 -				 checkChildren(otherChildren, toParentStr))
   1.144 +			       (Unix.reap child_handle;
   1.145 +				checkChildren(otherChildren, toParentStr))
   1.146  			    else 
   1.147  			       (**********************************************)
   1.148  			       (* Keep this child and go on to check others  *)
   1.149  			       (**********************************************)
   1.150 -
   1.151 -				 (childProc::(checkChildren (otherChildren, toParentStr)))
   1.152 +			      (childProc::(checkChildren (otherChildren, toParentStr)))
   1.153  			 end
   1.154  		       else
   1.155  			 (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   1.156 @@ -611,16 +593,19 @@
   1.157  		            (Unix.execute(proverCmd, (settings@[file])))
   1.158  		       val (instr, outstr) = Unix.streamsOf childhandle
   1.159  		       
   1.160 -		       val newProcList =    (((CMDPROC{
   1.161 +		       val newProcList = (CMDPROC{
   1.162  					    prover = prover,
   1.163  					    cmd = file,
   1.164  					    thmstring = thmstring,
   1.165  					    goalstring = goalstring,
   1.166  					    proc_handle = childhandle,
   1.167  					    instr = instr,
   1.168 -					    outstr = outstr })::procList))
   1.169 +					    outstr = outstr }) :: procList
   1.170  	  
   1.171 -		       val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   1.172 +		       val _ = File.append (File.tmp_path (Path.basic "exec_child")) 
   1.173 +		                 ("executing command for goal:\n"^
   1.174 +		                  goalstring^proverCmd^(concat settings)^file^
   1.175 +		                  " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   1.176  		   in
   1.177  		     Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList
   1.178  		   end
   1.179 @@ -649,83 +634,63 @@
   1.180  	  (* Watcher Loop                               *)
   1.181  	  (**********************************************)
   1.182  
   1.183 -
   1.184 -
   1.185 -
   1.186  	      fun keepWatching (toParentStr, fromParentStr,procList) = 
   1.187 -		    let    fun loop (procList) =  
   1.188 -			   (
   1.189 -			   let val cmdsFromIsa = pollParentInput ()
   1.190 -			       fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
   1.191 -					    TextIO.flushOut toParentStr;
   1.192 -					     killChildren (map (cmdchildHandle) procList);
   1.193 -					      ())
   1.194 -			       
   1.195 -			   in 
   1.196 -			      (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   1.197 -										 (**********************************)
   1.198 -			      if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
   1.199 -				   (                                             (**********************************)                             
   1.200 -				    if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   1.201 -				    then 
   1.202 -				      (
   1.203 -					let val child_handles = map cmdchildHandle procList 
   1.204 -					in
   1.205 -					   killChildren child_handles;
   1.206 -					   (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                                              loop ([])
   1.207 -					end
   1.208 -					   
   1.209 -				       )
   1.210 -				    else
   1.211 -				      ( 
   1.212 -					if ((length procList)<10)    (********************)
   1.213 -					then                        (* Execute locally  *)
   1.214 -					   (                        (********************)
   1.215 -					    let 
   1.216 -					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.217 -					      val parentID = Posix.ProcEnv.getppid()
   1.218 -          					 val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
   1.219 -					      val newProcList' =checkChildren (newProcList, toParentStr) 
   1.220 +		let fun loop (procList) =  
   1.221 +		     let val cmdsFromIsa = pollParentInput ()
   1.222 +			 fun killchildHandler (n:int)  = 
   1.223 +			       (TextIO.output(toParentStr, "Killing child proof processes!\n");
   1.224 +				TextIO.flushOut toParentStr;
   1.225 +				killChildren (map (cmdchildHandle) procList);
   1.226 +				())
   1.227 +		     in 
   1.228 +			(*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   1.229 +									   (**********************************)
   1.230 +			if (isSome cmdsFromIsa) 
   1.231 +			then (*  deal with input from Isabelle *)
   1.232 +			  if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   1.233 +			  then 
   1.234 +			    let val child_handles = map cmdchildHandle procList 
   1.235 +			    in
   1.236 +			       killChildren child_handles;
   1.237 +			       (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)    
   1.238 +			       loop ([])
   1.239 +			    end
   1.240 +			  else
   1.241 +			    if ((length procList)<10)    (********************)
   1.242 +			    then                        (* Execute locally  *)
   1.243 +			      let 
   1.244 +				val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.245 +				val parentID = Posix.ProcEnv.getppid()
   1.246 +				   val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
   1.247 +				val newProcList' =checkChildren (newProcList, toParentStr) 
   1.248  
   1.249 -					      val _ = warning("off to keep watching...")
   1.250 -					     val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
   1.251 -					    in
   1.252 -					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   1.253 -					      loop (newProcList') 
   1.254 -					    end
   1.255 -					    )
   1.256 -					else                         (*********************************)
   1.257 -								     (* Execute remotely              *)
   1.258 -								     (* (actually not remote for now )*)
   1.259 -					    (                        (*********************************)
   1.260 -					    let 
   1.261 -					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.262 -					      val parentID = Posix.ProcEnv.getppid()
   1.263 -					      val newProcList' =checkChildren (newProcList, toParentStr) 
   1.264 -					    in
   1.265 -					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   1.266 -					      loop (newProcList') 
   1.267 -					    end
   1.268 -					    )
   1.269 -
   1.270 -
   1.271 -
   1.272 -					)
   1.273 -				     )                                              (******************************)
   1.274 -			      else                                                  (* No new input from Isabelle *)
   1.275 -										    (******************************)
   1.276 -				  (    let val newProcList = checkChildren ((procList), toParentStr)
   1.277 -				       in
   1.278 -					 (*Posix.Process.sleep (Time.fromSeconds 1);*)
   1.279 -					(File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
   1.280 -					 loop (newProcList)
   1.281 -				       end
   1.282 -				   
   1.283 -				   )
   1.284 -			    end)
   1.285 -		    in  
   1.286 -			loop (procList)
   1.287 -		    end
   1.288 +				val _ = warning("off to keep watching...")
   1.289 +			       val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
   1.290 +			      in
   1.291 +				(*Posix.Process.sleep (Time.fromSeconds 1);*)
   1.292 +				loop (newProcList') 
   1.293 +			      end
   1.294 +			    else  (* Execute remotely              *)
   1.295 +                                  (* (actually not remote for now )*)
   1.296 +			      let 
   1.297 +				val newProcList = execCmds (valOf cmdsFromIsa) procList
   1.298 +				val parentID = Posix.ProcEnv.getppid()
   1.299 +				val newProcList' =checkChildren (newProcList, toParentStr) 
   1.300 +			      in
   1.301 +				(*Posix.Process.sleep (Time.fromSeconds 1);*)
   1.302 +				loop (newProcList') 
   1.303 +			      end
   1.304 +			else (* No new input from Isabelle *)
   1.305 +			  let val newProcList = checkChildren ((procList), toParentStr)
   1.306 +			  in
   1.307 +			    (*Posix.Process.sleep (Time.fromSeconds 1);*)
   1.308 +			   (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
   1.309 +			    loop (newProcList)
   1.310 +			  end
   1.311 +		      end
   1.312 +		in  
   1.313 +		    loop (procList)
   1.314 +		end
   1.315  		
   1.316      
   1.317  		in
   1.318 @@ -798,176 +763,124 @@
   1.319  fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   1.320  
   1.321  fun reapWatcher(pid, instr, outstr) =
   1.322 -        let
   1.323 -		val u = TextIO.closeIn instr;
   1.324 -	        val u = TextIO.closeOut outstr;
   1.325 -	
   1.326 -		val (_, status) =
   1.327 -			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
   1.328 -	in
   1.329 -		status
   1.330 -	end
   1.331 -
   1.332 -
   1.333 -
   1.334 -fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   1.335 -			   val streams =snd mychild
   1.336 -                           val childin = fst streams
   1.337 -                           val childout = snd streams
   1.338 -                           val childpid = fst mychild
   1.339 -                           val sign = sign_of_thm thm
   1.340 -                           val prems = prems_of thm
   1.341 -                           val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.342 -                           val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   1.343 -                           fun vampire_proofHandler (n) =
   1.344 -                           (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.345 -                           VampComm.getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
   1.346 -                          
   1.347 -
   1.348 -fun spass_proofHandler (n) = (
   1.349 -                                 let  val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
   1.350 -                                      val _ = TextIO.output (outfile, ("In signal handler now\n"))
   1.351 -                                      val _ =  TextIO.closeOut outfile
   1.352 -                                      val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
   1.353 -                                      val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
   1.354 -
   1.355 -                                      val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   1.356 -                                      val _ =  TextIO.closeOut outfile
   1.357 -                                      in          (* if a proof has been found and sent back as a reconstruction proof *)
   1.358 -                                                  if ( (substring (reconstr, 0,1))= "[")
   1.359 -                                                  then 
   1.360 -
   1.361 -                                                            (
   1.362 -                                                                 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.363 -                                                                 Recon_Transfer.apply_res_thm reconstr goalstring;
   1.364 -                                                                 Pretty.writeln(Pretty.str  (oct_char "361"));
   1.365 -                                                                 
   1.366 -                                                                 goals_being_watched := ((!goals_being_watched) - 1);
   1.367 -                                                         
   1.368 -                                                                 if ((!goals_being_watched) = 0)
   1.369 -                                                                 then 
   1.370 -                                                                    (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found")));
   1.371 -                                                                         val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.372 -                                                                         val _ =  TextIO.closeOut outfile
   1.373 -                                                                     in
   1.374 -                                                                         killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   1.375 -                                                                     end)
   1.376 -                                                                 else
   1.377 -                                                                    ()
   1.378 -                                                            )
   1.379 -                                                    (* if there's no proof, but a message from Spass *)
   1.380 -                                                    else if ((substring (reconstr, 0,5))= "SPASS")
   1.381 -                                                         then
   1.382 -                                                                 (
   1.383 -                                                                     goals_being_watched := (!goals_being_watched) -1;
   1.384 -                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.385 -                                                                      Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
   1.386 -                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   1.387 -                                                                      if (!goals_being_watched = 0)
   1.388 -                                                                      then 
   1.389 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   1.390 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.391 -                                                                               val _ =  TextIO.closeOut outfile
   1.392 -                                                                           in
   1.393 -                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   1.394 -                                                                           end )
   1.395 -                                                                      else
   1.396 -                                                                         ()
   1.397 -                                                                ) 
   1.398 -						   (* print out a list of rules used from clasimpset*)
   1.399 -                                                    else if ((substring (reconstr, 0,5))= "Rules")
   1.400 -                                                         then
   1.401 -                                                                 (
   1.402 -                                                                     goals_being_watched := (!goals_being_watched) -1;
   1.403 -                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.404 -                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
   1.405 -                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   1.406 -                                                                      if (!goals_being_watched = 0)
   1.407 -                                                                      then 
   1.408 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   1.409 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.410 -                                                                               val _ =  TextIO.closeOut outfile
   1.411 -                                                                           in
   1.412 -                                                                              killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   1.413 -                                                                           end )
   1.414 -                                                                      else
   1.415 -                                                                         ()
   1.416 -                                                                )
   1.417 -							
   1.418 -                                                          (* if proof translation failed *)
   1.419 -                                                          else if ((substring (reconstr, 0,5)) = "Proof")
   1.420 -                                                               then 
   1.421 -                                                                   (
   1.422 -                                                                      goals_being_watched := (!goals_being_watched) -1;
   1.423 -                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.424 -                                                                       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   1.425 -                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.426 -                                                                       if (!goals_being_watched = 0)
   1.427 -                                                                       then 
   1.428 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
   1.429 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.430 -                                                                               val _ =  TextIO.closeOut outfile
   1.431 -                                                                            in
   1.432 -                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   1.433 -                                                                            end )
   1.434 -                                                                       else
   1.435 -                                                                          ( )
   1.436 -                                                                      )
   1.437 -
   1.438 -							        else if ((substring (reconstr, 0,1)) = "%")
   1.439 -                                                               then 
   1.440 -                                                                   (
   1.441 -                                                                      goals_being_watched := (!goals_being_watched) -1;
   1.442 -                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.443 -                                                                       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   1.444 -                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.445 -                                                                       if (!goals_being_watched = 0)
   1.446 -                                                                       then 
   1.447 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
   1.448 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.449 -                                                                               val _ =  TextIO.closeOut outfile
   1.450 -                                                                            in
   1.451 -                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   1.452 -                                                                            end )
   1.453 -                                                                       else
   1.454 -                                                                          ( )
   1.455 -                                                                      )
   1.456 -
   1.457 -
   1.458 -                                                                else  (* add something here ?*)
   1.459 -                                                                   (
   1.460 -                                                                      goals_being_watched := (!goals_being_watched) -1;
   1.461 -                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.462 -                                                                       Pretty.writeln(Pretty.str ("Ran out of options in handler"));
   1.463 -                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.464 -                                                                       if (!goals_being_watched = 0)
   1.465 -                                                                       then 
   1.466 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
   1.467 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.468 -                                                                               val _ =  TextIO.closeOut outfile
   1.469 -                                                                            in
   1.470 -                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   1.471 -                                                                            end )
   1.472 -                                                                       else
   1.473 -                                                                          ( )
   1.474 -                                                                      )
   1.475 -                                                                     
   1.476 -                                                                           
   1.477 -                                                            
   1.478 -                                       end)
   1.479 -
   1.480 -
   1.481 -                        
   1.482 -                       in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   1.483 -                          IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   1.484 -                          (childin, childout, childpid)
   1.485 -
   1.486 -
   1.487 -
   1.488 +  let val u = TextIO.closeIn instr;
   1.489 +      val u = TextIO.closeOut outstr;
   1.490 +      val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
   1.491 +  in
   1.492 +	  status
   1.493    end
   1.494  
   1.495  
   1.496  
   1.497 +fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) =
   1.498 + let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   1.499 +     val streams =snd mychild
   1.500 +     val childin = fst streams
   1.501 +     val childout = snd streams
   1.502 +     val childpid = fst mychild
   1.503 +     val sign = sign_of_thm thm
   1.504 +     val prems = prems_of thm
   1.505 +     val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.506 +     val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   1.507 +     fun vampire_proofHandler (n) =
   1.508 +	(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.509 +	 VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))               
   1.510 +     fun spass_proofHandler (n) = (
   1.511 +       let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
   1.512 +	   val _ = TextIO.output (outfile, ("In signal handler now\n"))
   1.513 +	   val _ =  TextIO.closeOut outfile
   1.514 +	   val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
   1.515 +	   val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
   1.516 +   
   1.517 +	   val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   1.518 +	   val _ =  TextIO.closeOut outfile
   1.519 +       in (* if a proof has been found and sent back as a reconstruction proof *)
   1.520 +	 if ( (substring (reconstr, 0,1))= "[")
   1.521 +	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.522 +	       Recon_Transfer.apply_res_thm reconstr goalstring;
   1.523 +	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.524 +	       
   1.525 +	       goals_being_watched := ((!goals_being_watched) - 1);
   1.526 +       
   1.527 +	       if ((!goals_being_watched) = 0)
   1.528 +	       then 
   1.529 +		  (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found")));
   1.530 +		       val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.531 +		       val _ =  TextIO.closeOut outfile
   1.532 +		   in
   1.533 +		       killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   1.534 +		   end)
   1.535 +		else () )
   1.536 +	 (* if there's no proof, but a message from Spass *)
   1.537 +	 else if ((substring (reconstr, 0,5))= "SPASS")
   1.538 +	 then (goals_being_watched := (!goals_being_watched) -1;
   1.539 +	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.540 +	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
   1.541 +	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.542 +	       if (!goals_being_watched = 0)
   1.543 +	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.544 +	              ("Reaping a watcher, goals watched is: " ^
   1.545 +	                 (string_of_int (!goals_being_watched))^"\n");
   1.546 +	             killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
   1.547 +		else () ) 
   1.548 +	(* print out a list of rules used from clasimpset*)
   1.549 +	 else if ((substring (reconstr, 0,5))= "Rules")
   1.550 +	 then (goals_being_watched := (!goals_being_watched) -1;
   1.551 +	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.552 +	       Pretty.writeln(Pretty.str (goalstring^reconstr));
   1.553 +	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.554 +	       if (!goals_being_watched = 0)
   1.555 +	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.556 +	              ("Reaping a watcher, goals watched is: " ^
   1.557 +	                 (string_of_int (!goals_being_watched))^"\n");
   1.558 +	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   1.559 +		     )
   1.560 +	       else () )
   1.561 +	  (* if proof translation failed *)
   1.562 +	 else if ((substring (reconstr, 0,5)) = "Proof")
   1.563 +	 then (goals_being_watched := (!goals_being_watched) -1;
   1.564 +	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.565 +	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   1.566 +	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.567 +	       if (!goals_being_watched = 0)
   1.568 +	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.569 +	              ("Reaping a watcher, goals watched is: " ^
   1.570 +	                 (string_of_int (!goals_being_watched))^"\n");
   1.571 +	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   1.572 +		     )
   1.573 +	       else () )
   1.574  
   1.575 +	 else if ((substring (reconstr, 0,1)) = "%")
   1.576 +	 then (goals_being_watched := (!goals_being_watched) -1;
   1.577 +	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.578 +	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   1.579 +	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.580 +	       if (!goals_being_watched = 0)
   1.581 +	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.582 +	              ("Reaping a watcher, goals watched is: " ^
   1.583 +	                 (string_of_int (!goals_being_watched))^"\n");
   1.584 +	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   1.585 +		     )
   1.586 +	       else () )
   1.587 +
   1.588 +	 else  (* add something here ?*)
   1.589 +	      (goals_being_watched := (!goals_being_watched) -1;
   1.590 +	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.591 +		Pretty.writeln(Pretty.str ("Ran out of options in handler"));
   1.592 +		Pretty.writeln(Pretty.str  (oct_char "361"));
   1.593 +		if (!goals_being_watched = 0)
   1.594 +	        then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.595 +	              ("Reaping a watcher, goals watched is: " ^
   1.596 +	                 (string_of_int (!goals_being_watched))^"\n");
   1.597 +	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   1.598 +		     )
   1.599 +	        else () )
   1.600 +       end)
   1.601 +
   1.602 + in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   1.603 +    IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   1.604 +    (childin, childout, childpid)
   1.605 +
   1.606 +  end
   1.607  
   1.608  end (* structure Watcher *)