src/HOL/Tools/ATP/watcher.ML
changeset 17435 0eed5a1c00c1
parent 17422 3b237822985d
child 17484 f6a225f97f0a
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Sep 16 11:38:49 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Sep 16 11:39:09 2005 +0200
     1.3 @@ -614,14 +614,20 @@
     1.4  
     1.5  
     1.6  fun createWatcher (thm,clause_arr, num_of_clauses) =
     1.7 - let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
     1.8 -     val streams = snd mychild
     1.9 -     val childin = fst streams
    1.10 -     val childout = snd streams
    1.11 -     val childpid = fst mychild
    1.12 + let val (childpid,(childin,childout)) =
    1.13 +           childInfo (setupWatcher(thm,clause_arr, num_of_clauses))
    1.14 +     fun decr_watched() =
    1.15 +	  (goals_being_watched := (!goals_being_watched) - 1;
    1.16 +	   if !goals_being_watched = 0
    1.17 +	   then 
    1.18 +	     (File.append (File.tmp_path (Path.basic "reap_found"))
    1.19 +	       ("Reaping a watcher, childpid = "^
    1.20 +		LargeWord.toString (Posix.Process.pidToWord childpid)^"\n");
    1.21 +	      killWatcher childpid; reapWatcher (childpid,childin, childout); ())
    1.22 +	    else ())
    1.23       val sign = sign_of_thm thm
    1.24       val prems = prems_of thm
    1.25 -     val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    1.26 +     val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    1.27       val _ = debug ("subgoals forked to createWatcher: "^prems_string);
    1.28  (*FIXME: do we need an E proofHandler??*)
    1.29       fun vampire_proofHandler n =
    1.30 @@ -639,82 +645,35 @@
    1.31  	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.32  	       Recon_Transfer.apply_res_thm reconstr goalstring;
    1.33  	       Pretty.writeln(Pretty.str  (oct_char "361"));
    1.34 -	       
    1.35 -	       goals_being_watched := (!goals_being_watched) - 1;
    1.36 -       
    1.37 -	       if !goals_being_watched = 0
    1.38 -	       then 
    1.39 -		  let val _ = File.write (File.tmp_path (Path.basic "reap_found"))
    1.40 -                                   ("Reaping a watcher, goals watched now "^
    1.41 -                                    string_of_int (!goals_being_watched)^"\n")
    1.42 -		   in
    1.43 -		       killWatcher childpid; reapWatcher (childpid,childin, childout); ()
    1.44 -		   end
    1.45 -		else () )
    1.46 +	       decr_watched())
    1.47  	 (* if there's no proof, but a message from Spass *)
    1.48  	 else if substring (reconstr, 0,5) = "SPASS"
    1.49 -	 then (goals_being_watched := (!goals_being_watched) -1;
    1.50 -	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.51 +	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.52  	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
    1.53  	       Pretty.writeln(Pretty.str  (oct_char "361"));
    1.54 -	       if (!goals_being_watched = 0)
    1.55 -	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
    1.56 -	              ("Reaping a watcher, goals watched is: " ^
    1.57 -	                 (string_of_int (!goals_being_watched))^"\n");
    1.58 -	             killWatcher childpid; reapWatcher (childpid,childin, childout); ())
    1.59 -		else () ) 
    1.60 +	       decr_watched()) 
    1.61  	(* print out a list of rules used from clasimpset*)
    1.62  	 else if substring (reconstr, 0,5) = "Rules"
    1.63 -	 then (goals_being_watched := (!goals_being_watched) -1;
    1.64 -	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.65 +	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.66  	       Pretty.writeln(Pretty.str (goalstring^reconstr));
    1.67  	       Pretty.writeln(Pretty.str  (oct_char "361"));
    1.68 -	       if (!goals_being_watched = 0)
    1.69 -	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
    1.70 -	              ("Reaping a watcher, goals watched is: " ^
    1.71 -	                 (string_of_int (!goals_being_watched))^"\n");
    1.72 -	             killWatcher childpid;  reapWatcher (childpid,childin, childout);()
    1.73 -		     )
    1.74 -	       else () )
    1.75 +	       decr_watched())
    1.76  	  (* if proof translation failed *)
    1.77  	 else if substring (reconstr, 0,5) = "Proof"
    1.78 -	 then (goals_being_watched := (!goals_being_watched) -1;
    1.79 -	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.80 +	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.81  	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
    1.82  	       Pretty.writeln(Pretty.str  (oct_char "361"));
    1.83 -	       if (!goals_being_watched = 0)
    1.84 -	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
    1.85 -	              ("Reaping a watcher, goals watched is: " ^
    1.86 -	                 (string_of_int (!goals_being_watched))^"\n");
    1.87 -	             killWatcher childpid;  reapWatcher (childpid,childin, childout);()
    1.88 -		     )
    1.89 -	       else () )
    1.90 -
    1.91 +	       decr_watched())
    1.92  	 else if substring (reconstr, 0,1) = "%"
    1.93 -	 then (goals_being_watched := (!goals_being_watched) -1;
    1.94 -	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.95 +	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.96  	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
    1.97  	       Pretty.writeln(Pretty.str  (oct_char "361"));
    1.98 -	       if (!goals_being_watched = 0)
    1.99 -	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.100 -	              ("Reaping a watcher, goals watched is: " ^
   1.101 -	                 (string_of_int (!goals_being_watched))^"\n");
   1.102 -	             killWatcher childpid;  reapWatcher (childpid,childin, childout);()
   1.103 -		     )
   1.104 -	       else () )
   1.105 -
   1.106 +	       decr_watched())
   1.107  	 else  (* add something here ?*)
   1.108 -	      (goals_being_watched := (!goals_being_watched) -1;
   1.109 -	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.110 +	      (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.111  	       Pretty.writeln(Pretty.str ("Ran out of options in handler"));
   1.112  	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.113 -	       if (!goals_being_watched = 0)
   1.114 -	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.115 -		     ("Reaping a watcher, goals watched is: " ^
   1.116 -			(string_of_int (!goals_being_watched))^"\n");
   1.117 -		    killWatcher childpid;  reapWatcher (childpid,childin, childout);()
   1.118 -		    )
   1.119 -	       else () )
   1.120 +	       decr_watched())
   1.121         end)
   1.122  
   1.123   in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);