Fixed the printing of the used theorems by maintaining separate lists for each subgoal.
authorpaulson
Fri Oct 06 15:39:29 2006 +0200 (2006-10-06)
changeset 20871da3a43cdbe8d
parent 20870 992bcbff055a
child 20872 528054ca23e3
Fixed the printing of the used theorems by maintaining separate lists for each subgoal.
Retains the ATP input files if debugging is on.
src/HOL/Tools/ATP/watcher.ML
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Oct 06 15:38:29 2006 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Oct 06 15:39:29 2006 +0200
     1.3 @@ -21,10 +21,10 @@
     1.4  (* Send message to watcher to kill resolution provers *)
     1.5  val callSlayer : TextIO.outstream -> unit
     1.6  
     1.7 -(* Start a watcher and set up signal handlers             *)
     1.8 +(* Start a watcher and set up signal handlers*)
     1.9  val createWatcher : 
    1.10 -    thm * string Array.array -> 
    1.11 -    TextIO.instream * TextIO.outstream * Posix.Process.pid
    1.12 +	thm * string Array.array list -> 
    1.13 +	TextIO.instream * TextIO.outstream * Posix.Process.pid
    1.14  val killWatcher : Posix.Process.pid -> unit
    1.15  val killChild  : ('a, 'b) Unix.proc -> OS.Process.status
    1.16  val setting_sep : char
    1.17 @@ -212,13 +212,13 @@
    1.18  			 Date.toString(Date.fromTimeLocal(Time.now())))
    1.19        in execCmds cmds newProcList end
    1.20  
    1.21 -fun checkChildren (th, names_arr, toParentStr, children) = 
    1.22 +fun checkChildren (th, thm_names_list, toParentStr, children) = 
    1.23    let fun check [] = []  (* no children to check *)
    1.24  	| check (child::children) = 
    1.25 -	   let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc =
    1.26 -		   child
    1.27 +	   let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
    1.28  	       val _ = trace ("\nprobfile = " ^ file)
    1.29 -	       val sgno = number_from_filename file
    1.30 +	       val sgno = number_from_filename file  (*subgoal number*)
    1.31 +	       val thm_names = List.nth(thm_names_list, sgno-1);
    1.32  	       val ppid = Posix.ProcEnv.getppid()
    1.33  	   in 
    1.34  	     if pollChild childIn
    1.35 @@ -226,15 +226,16 @@
    1.36  	       let val _ = trace ("\nInput available from child: " ^ file)
    1.37  		   val childDone = (case prover of
    1.38  		       "vampire" => AtpCommunication.checkVampProofFound
    1.39 -			    (childIn, toParentStr, ppid, file, names_arr)  
    1.40 +			    (childIn, toParentStr, ppid, file, thm_names)  
    1.41  		     | "E" => AtpCommunication.checkEProofFound
    1.42 -			    (childIn, toParentStr, ppid, file, names_arr)             
    1.43 +			    (childIn, toParentStr, ppid, file, thm_names)             
    1.44  		     | "spass" => AtpCommunication.checkSpassProofFound
    1.45 -			    (childIn, toParentStr, ppid, file, th, sgno,names_arr)  
    1.46 +			    (childIn, toParentStr, ppid, file, th, sgno, thm_names)  
    1.47  		     | _ => (trace ("\nBad prover! " ^ prover); true) )
    1.48  		in
    1.49  		 if childDone (*ATP has reported back (with success OR failure)*)
    1.50 -		 then (Unix.reap proc_handle;  OS.FileSys.remove file;
    1.51 +		 then (Unix.reap proc_handle;  
    1.52 +		       if !Output.show_debug_msgs then () else OS.FileSys.remove file;
    1.53  		       check children)
    1.54  		 else child :: check children
    1.55  	      end
    1.56 @@ -246,7 +247,7 @@
    1.57    end;
    1.58  
    1.59  
    1.60 -fun setupWatcher (th,names_arr) = 
    1.61 +fun setupWatcher (th,thm_names_list) = 
    1.62    let
    1.63      val p1 = Posix.IO.pipe()   (*pipes for communication between parent and watcher*)
    1.64      val p2 = Posix.IO.pipe()
    1.65 @@ -283,16 +284,16 @@
    1.66  		    if length procList < 40 then    (* Execute locally  *)                    
    1.67  		      let val _ = trace("\nCommands from parent: " ^ 
    1.68  					Int.toString(length cmds))
    1.69 -			  val newProcList' = checkChildren(th, names_arr, toParentStr, 
    1.70 +			  val newProcList' = checkChildren(th, thm_names_list, toParentStr, 
    1.71  						execCmds cmds procList) 
    1.72  		      in trace "\nCommands executed"; keepWatching newProcList' end
    1.73  		    else  (* Execute remotely [FIXME: NOT REALLY]  *)
    1.74 -		      let val newProcList' = checkChildren (th, names_arr, toParentStr, 
    1.75 +		      let val newProcList' = checkChildren (th, thm_names_list, toParentStr, 
    1.76  						execCmds cmds procList) 
    1.77  		      in keepWatching newProcList' end
    1.78  		| NONE => (* No new input from Isabelle *)
    1.79  		    (trace "\nNothing from parent...";  
    1.80 -		     keepWatching(checkChildren(th, names_arr, toParentStr, procList))))
    1.81 +		     keepWatching(checkChildren(th, thm_names_list, toParentStr, procList))))
    1.82  	     handle exn => (*FIXME: exn handler is too general!*)
    1.83  	       (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
    1.84  		keepWatching procList);
    1.85 @@ -351,8 +352,8 @@
    1.86  
    1.87  fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
    1.88  
    1.89 -fun createWatcher (th, names_arr) =
    1.90 - let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (th,names_arr)
    1.91 +fun createWatcher (th, thm_names_list) =
    1.92 + let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (th,thm_names_list)
    1.93       fun decr_watched() =
    1.94  	  (goals_being_watched := !goals_being_watched - 1;
    1.95  	   if !goals_being_watched = 0