src/HOL/Tools/ATP/watcher.ML
changeset 17231 f42bc4f7afdf
parent 17216 df66d8feec63
child 17234 12a9393c5d77
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Sep 02 15:25:27 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Sep 02 15:25:44 2005 +0200
     1.3 @@ -143,8 +143,9 @@
     1.4  (*  Send request to Watcher for a vampire to be called for filename in arg      *)
     1.5  (********************************************************************************)
     1.6                      
     1.7 -fun callResProver (toWatcherStr,  arg) = (sendOutput (toWatcherStr, arg^"\n"); 
     1.8 -                                     TextIO.flushOut toWatcherStr)
     1.9 +fun callResProver (toWatcherStr,  arg) = 
    1.10 +      (sendOutput (toWatcherStr, arg^"\n"); 
    1.11 +       TextIO.flushOut toWatcherStr)
    1.12  
    1.13  (*****************************************************************************************)
    1.14  (*  Send request to Watcher for multiple provers to be called for filenames in arg       *)
    1.15 @@ -267,34 +268,12 @@
    1.16      (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    1.17      (*** hyps/local axioms just now                                                ***)
    1.18      val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])
    1.19 -    (*** check if the directory exists and, if not, create it***)
    1.20 -   (* val _ = 
    1.21 -	if !SpassComm.spass
    1.22 -	then 
    1.23 -	    if File.exists dfg_dir then warning("dfg dir exists")
    1.24 -	    else File.mkdir dfg_dir
    1.25 -	else
    1.26 -	    warning("not converting to dfg")
    1.27 -    
    1.28 -    val _ = if !SpassComm.spass then 
    1.29 -		system (ResLib.helper_path "TPTP2X_HOME" "tptp2X" ^ 
    1.30 -		        " -fdfg -d " ^ dfg_path ^ " " ^
    1.31 -			File.platform_path wholefile)
    1.32 -	      else 7
    1.33 -    val newfile =   if !SpassComm.spass 
    1.34 -		    then 
    1.35 -			    dfg_path^"/ax_prob"^"_"^(probID)^".dfg" 
    1.36 -
    1.37 -		    else
    1.38 -			    (File.platform_path wholefile)*)
    1.39  
    1.40      (* if using spass prob_n already contains whole DFG file, otherwise need to mash axioms*)
    1.41      (* from clasimpset onto problem file *)
    1.42      val newfile =   if !SpassComm.spass 
    1.43 -		    then 
    1.44 -			 probfile
    1.45 -                    else 
    1.46 -			(File.platform_path wholefile)
    1.47 +		    then probfile
    1.48 +                    else (File.platform_path wholefile)
    1.49  
    1.50      val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
    1.51  	       (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")
    1.52 @@ -366,7 +345,6 @@
    1.53  (*  Get Io-descriptor for polling of an input stream          *)
    1.54  (**************************************************************)
    1.55  
    1.56 -
    1.57  fun getInIoDesc someInstr = 
    1.58      let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
    1.59          val _ = TextIO.output (TextIO.stdOut, buf)
    1.60 @@ -385,8 +363,6 @@
    1.61  (*  Set up a Watcher Process         *)
    1.62  (*************************************)
    1.63  
    1.64 -
    1.65 -
    1.66  fun setupWatcher (thm,clause_arr, num_of_clauses) = 
    1.67    let
    1.68      (** pipes for communication between parent and watcher **)
    1.69 @@ -451,13 +427,10 @@
    1.70  			  then
    1.71  			     NONE
    1.72  			  else if (OS.IO.isIn (hd pdl)) 
    1.73 -			       then
    1.74 -				  (SOME ( getCmds (toParentStr, fromParentStr, [])))
    1.75 -			       else
    1.76 -				   NONE
    1.77 +			       then SOME (getCmds (toParentStr, fromParentStr, []))
    1.78 +			       else NONE
    1.79  		       end
    1.80 -		     else
    1.81 -			 NONE
    1.82 +		     else NONE
    1.83  		 end
    1.84  		      
    1.85  	       fun pollChildInput (fromStr) = 
    1.86 @@ -472,7 +445,6 @@
    1.87  		     if (isSome pd ) then 
    1.88  			 let val pd' = OS.IO.pollIn (valOf pd)
    1.89  			     val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
    1.90 -			     
    1.91  			 in
    1.92  			    if null pdl 
    1.93  			    then
    1.94 @@ -534,7 +506,9 @@
    1.95  		      if (isSome childIncoming) 
    1.96  		      then 
    1.97  			  (* check here for prover label on child*)
    1.98 -			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))  ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) 
    1.99 +			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) 
   1.100 +			             ("subgoals forked to checkChildren:"^
   1.101 +			             prems_string^prover^thmstring^goalstring^childCmd) 
   1.102  		              val childDone = (case prover of
   1.103  	                          "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )                                              
   1.104                                   |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   1.105 @@ -709,13 +683,10 @@
   1.106  		  (* start the watcher loop  *)
   1.107  		  (***************************)
   1.108  		  keepWatching (toParentStr, fromParentStr, procList);
   1.109 -
   1.110 -
   1.111  		  (****************************************************************************)
   1.112 -		  (* fake return value - actually want the watcher to loop until killed       *)
   1.113 +   (* fake return value - actually want the watcher to loop until killed *)
   1.114  		  (****************************************************************************)
   1.115  		  Posix.Process.wordToPid 0w0
   1.116 -		  
   1.117  		end);
   1.118  	  (* end case *)
   1.119  
   1.120 @@ -770,11 +741,9 @@
   1.121  	  status
   1.122    end
   1.123  
   1.124 -
   1.125 -
   1.126  fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) =
   1.127   let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   1.128 -     val streams =snd mychild
   1.129 +     val streams = snd mychild
   1.130       val childin = fst streams
   1.131       val childout = snd streams
   1.132       val childpid = fst mychild
   1.133 @@ -795,24 +764,24 @@
   1.134  	   val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   1.135  	   val _ =  TextIO.closeOut outfile
   1.136         in (* if a proof has been found and sent back as a reconstruction proof *)
   1.137 -	 if ( (substring (reconstr, 0,1))= "[")
   1.138 +	 if substring (reconstr, 0,1) = "["
   1.139  	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.140  	       Recon_Transfer.apply_res_thm reconstr goalstring;
   1.141  	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.142  	       
   1.143  	       goals_being_watched := ((!goals_being_watched) - 1);
   1.144         
   1.145 -	       if ((!goals_being_watched) = 0)
   1.146 +	       if (!goals_being_watched) = 0
   1.147  	       then 
   1.148 -		  (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found")));
   1.149 -		       val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.150 -		       val _ =  TextIO.closeOut outfile
   1.151 +		  let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found"))
   1.152 +                                   ("Reaping a watcher, goals watched is: "^
   1.153 +                                    (string_of_int (!goals_being_watched))^"\n")
   1.154  		   in
   1.155  		       killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   1.156 -		   end)
   1.157 +		   end
   1.158  		else () )
   1.159  	 (* if there's no proof, but a message from Spass *)
   1.160 -	 else if ((substring (reconstr, 0,5))= "SPASS")
   1.161 +	 else if substring (reconstr, 0,5) = "SPASS"
   1.162  	 then (goals_being_watched := (!goals_being_watched) -1;
   1.163  	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.164  	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
   1.165 @@ -824,7 +793,7 @@
   1.166  	             killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
   1.167  		else () ) 
   1.168  	(* print out a list of rules used from clasimpset*)
   1.169 -	 else if ((substring (reconstr, 0,5))= "Rules")
   1.170 +	 else if substring (reconstr, 0,5) = "Rules"
   1.171  	 then (goals_being_watched := (!goals_being_watched) -1;
   1.172  	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.173  	       Pretty.writeln(Pretty.str (goalstring^reconstr));
   1.174 @@ -837,7 +806,7 @@
   1.175  		     )
   1.176  	       else () )
   1.177  	  (* if proof translation failed *)
   1.178 -	 else if ((substring (reconstr, 0,5)) = "Proof")
   1.179 +	 else if substring (reconstr, 0,5) = "Proof"
   1.180  	 then (goals_being_watched := (!goals_being_watched) -1;
   1.181  	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.182  	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   1.183 @@ -850,7 +819,7 @@
   1.184  		     )
   1.185  	       else () )
   1.186  
   1.187 -	 else if ((substring (reconstr, 0,1)) = "%")
   1.188 +	 else if substring (reconstr, 0,1) = "%"
   1.189  	 then (goals_being_watched := (!goals_being_watched) -1;
   1.190  	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.191  	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   1.192 @@ -866,15 +835,15 @@
   1.193  	 else  (* add something here ?*)
   1.194  	      (goals_being_watched := (!goals_being_watched) -1;
   1.195  	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.196 -		Pretty.writeln(Pretty.str ("Ran out of options in handler"));
   1.197 -		Pretty.writeln(Pretty.str  (oct_char "361"));
   1.198 -		if (!goals_being_watched = 0)
   1.199 -	        then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.200 -	              ("Reaping a watcher, goals watched is: " ^
   1.201 -	                 (string_of_int (!goals_being_watched))^"\n");
   1.202 -	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   1.203 -		     )
   1.204 -	        else () )
   1.205 +	       Pretty.writeln(Pretty.str ("Ran out of options in handler"));
   1.206 +	       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.207 +	       if (!goals_being_watched = 0)
   1.208 +	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.209 +		     ("Reaping a watcher, goals watched is: " ^
   1.210 +			(string_of_int (!goals_being_watched))^"\n");
   1.211 +		    killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   1.212 +		    )
   1.213 +	       else () )
   1.214         end)
   1.215  
   1.216   in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);