VAMPIRE_HOME, helper_path and various stylistic tweaks
authorpaulson
Tue Jun 21 13:34:24 2005 +0200 (2005-06-21)
changeset 165157896ea4f3a87
parent 16514 090c6a98c704
child 16516 0842635545c3
VAMPIRE_HOME, helper_path and various stylistic tweaks
src/HOL/Tools/ATP/recon_order_clauses.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_lib.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue Jun 21 11:08:31 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue Jun 21 13:34:24 2005 +0200
     1.3 @@ -66,11 +66,9 @@
     1.4                             (a_lhs = x_rhs) andalso (a_rhs = x_lhs)
     1.5                         end
     1.6  
     1.7 -fun equal_pair (a,b) = equal a b
     1.8 -
     1.9  fun is_var_pair (a,b) vars = (a mem vars) andalso (b mem vars)
    1.10  
    1.11 -fun var_equiv vars (a,b)  = (equal_pair (a,b)) orelse (is_var_pair (a,b) vars)
    1.12 +fun var_equiv vars (a,b)  = a=b orelse (is_var_pair (a,b) vars)
    1.13  
    1.14  fun all_true [] = false
    1.15  |   all_true xs = let val falselist = List.filter (equal false ) xs 
     2.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue Jun 21 11:08:31 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Tue Jun 21 13:34:24 2005 +0200
     2.3 @@ -262,17 +262,9 @@
     2.4  	      File.platform_path wholefile])
     2.5      
     2.6      val dfg_dir = File.tmp_path (Path.basic "dfg"); 
     2.7 -    (*** check if the directory exists and, if not, create it***)
     2.8 -    val dfg_create =
     2.9 -	  if File.exists dfg_dir then warning("dfg dir exists")
    2.10 -	  else File.mkdir dfg_dir; 
    2.11      val dfg_path = File.platform_path dfg_dir;
    2.12      
    2.13 -    val tptp2X = getenv "TPTP2X_HOME" ^ "/tptp2X"
    2.14 -
    2.15 -
    2.16 -  		(*** need to check here if the directory exists and, if not, create it***)
    2.17 -  		
    2.18 +    val tptp2X = ResLib.helper_path "TPTP2X_HOME" "tptp2X"  		
    2.19  
    2.20   		(*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    2.21  		val probID = List.last(explode probfile)
    2.22 @@ -281,33 +273,26 @@
    2.23      		(*** only include problem and clasimp for the moment, not sure how to refer to ***)
    2.24     		(*** hyps/local axioms just now                                                ***)
    2.25     		val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])
    2.26 -    		val dfg_create = 
    2.27 +                (*** check if the directory exists and, if not, create it***)
    2.28 +    		val _ = 
    2.29  		    if !SpassComm.spass
    2.30                      then 
    2.31 - 	     		if File.exists dfg_dir 
    2.32 -     	        	then
    2.33 -     	           	    ((warning("dfg dir exists"));())
    2.34 - 			else
    2.35 - 		    	    File.mkdir dfg_dir
    2.36 +			if File.exists dfg_dir then warning("dfg dir exists")
    2.37 +			else File.mkdir dfg_dir
    2.38  		    else
    2.39 -			(warning("not converting to dfg");())
    2.40 -   		val dfg_path = File.platform_path dfg_dir;
    2.41 +			warning("not converting to dfg")
    2.42     		
    2.43 -   		val bar = if !SpassComm.spass then system ("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X -fdfg "^
    2.44 -                                 (File.platform_path wholefile)^" -d "^dfg_path)
    2.45 -			  else
    2.46 -				7
    2.47 -
    2.48 +   		val _ = if !SpassComm.spass then 
    2.49 +   		            system (tptp2X ^ " -fdfg -d "^dfg_path^" "^
    2.50 +                                    File.platform_path wholefile)
    2.51 +			  else 7
    2.52      		val newfile =   if !SpassComm.spass 
    2.53  				then 
    2.54  					dfg_path^"/ax_prob"^"_"^(probID)^".dfg" 
    2.55  			        else
    2.56  					(File.platform_path wholefile)
    2.57 -				  
    2.58 -                val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic"thmstring_in_watcher")));   
    2.59 -   		val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n"))
    2.60 - 		val _ =  TextIO.closeOut outfile
    2.61 -
    2.62 + 		val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
    2.63 + 		           (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")
    2.64   	     in
    2.65   		(prover,thmstring,goalstring, proverCmd, settings,newfile)	
    2.66  	     end;
    2.67 @@ -804,121 +789,95 @@
    2.68  	end
    2.69  
    2.70  
    2.71 -fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
    2.72 -			   val streams =snd mychild
    2.73 -                           val childin = fst streams
    2.74 -                           val childout = snd streams
    2.75 -                           val childpid = fst mychild
    2.76 -                           val sign = sign_of_thm thm
    2.77 -                           val prems = prems_of thm
    2.78 -                           val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    2.79 -                           val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
    2.80 -                           fun vampire_proofHandler (n) =
    2.81 -                           (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    2.82 -                           VampComm.getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
    2.83 -                          
    2.84 -
    2.85 -fun spass_proofHandler (n) = (
    2.86 -                                 let  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
    2.87 -                                      val _ = TextIO.output (outfile, ("In signal handler now\n"))
    2.88 -                                      val _ =  TextIO.closeOut outfile
    2.89 -                                      val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
    2.90 -                                      val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
    2.91 -
    2.92 -                                      val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
    2.93 -                                      val _ =  TextIO.closeOut outfile
    2.94 -                                      in          (* if a proof has been found and sent back as a reconstruction proof *)
    2.95 -                                                  if ( (substring (reconstr, 0,1))= "[")
    2.96 -                                                  then 
    2.97 +fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) =
    2.98 +  let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
    2.99 +      val streams =snd mychild
   2.100 +      val childin = fst streams
   2.101 +      val childout = snd streams
   2.102 +      val childpid = fst mychild
   2.103 +      val sign = sign_of_thm thm
   2.104 +      val prems = prems_of thm
   2.105 +      val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   2.106 +      val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   2.107 +      fun vampire_proofHandler (n) =
   2.108 +	  (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   2.109 +	  VampComm.getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361")))               
   2.110  
   2.111 -                                                            (
   2.112 -                                                                 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   2.113 -                                                                 Recon_Transfer.apply_res_thm reconstr goalstring;
   2.114 -                                                                 Pretty.writeln(Pretty.str  (oct_char "361"));
   2.115 -                                                                 
   2.116 -                                                                 goals_being_watched := ((!goals_being_watched) - 1);
   2.117 -                                                         
   2.118 -                                                                 if ((!goals_being_watched) = 0)
   2.119 -                                                                 then 
   2.120 -                                                                    (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found")));
   2.121 -                                                                         val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   2.122 -                                                                         val _ =  TextIO.closeOut outfile
   2.123 -                                                                     in
   2.124 -                                                                         killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   2.125 -                                                                     end)
   2.126 -                                                                 else
   2.127 -                                                                    ()
   2.128 -                                                            )
   2.129 -                                                    (* if there's no proof, but a message from Spass *)
   2.130 -                                                    else if ((substring (reconstr, 0,5))= "SPASS")
   2.131 -                                                         then
   2.132 -                                                                 (
   2.133 -                                                                     goals_being_watched := (!goals_being_watched) -1;
   2.134 -                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   2.135 -                                                                      Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
   2.136 -                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   2.137 -                                                                      if (!goals_being_watched = 0)
   2.138 -                                                                      then 
   2.139 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   2.140 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   2.141 -                                                                               val _ =  TextIO.closeOut outfile
   2.142 -                                                                           in
   2.143 -                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   2.144 -                                                                           end )
   2.145 -                                                                      else
   2.146 -                                                                         ()
   2.147 -                                                                ) 
   2.148 -						   (* print out a list of rules used from clasimpset*)
   2.149 -                                                    else if ((substring (reconstr, 0,5))= "Rules")
   2.150 -                                                         then
   2.151 -                                                                 (
   2.152 -                                                                     goals_being_watched := (!goals_being_watched) -1;
   2.153 -                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   2.154 -                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
   2.155 -                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   2.156 -                                                                      if (!goals_being_watched = 0)
   2.157 -                                                                      then 
   2.158 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   2.159 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   2.160 -                                                                               val _ =  TextIO.closeOut outfile
   2.161 -                                                                           in
   2.162 -                                                                              killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   2.163 -                                                                           end )
   2.164 -                                                                      else
   2.165 -                                                                         ()
   2.166 -                                                                )
   2.167 -							
   2.168 -                                                          (* if proof translation failed *)
   2.169 -                                                          else if ((substring (reconstr, 0,5)) = "Proof")
   2.170 -                                                               then 
   2.171 -                                                                   (
   2.172 -                                                                     goals_being_watched := (!goals_being_watched) -1;
   2.173 -                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   2.174 -                                                                      Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   2.175 -                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   2.176 -                                                                      if (!goals_being_watched = 0)
   2.177 -                                                                      then 
   2.178 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
   2.179 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   2.180 -                                                                               val _ =  TextIO.closeOut outfile
   2.181 -                                                                           in
   2.182 -                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   2.183 -                                                                           end )
   2.184 -                                                                      else
   2.185 -                                                                         ()
   2.186 -                                                                )
   2.187 -
   2.188 -
   2.189 -                                                                else  (* add something here ?*)
   2.190 -                                                                   ()
   2.191 -                                                             
   2.192 -                                       end)
   2.193 -
   2.194 -
   2.195 -                        
   2.196 -                       in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   2.197 -                          IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   2.198 -                          (childin, childout, childpid)
   2.199 +      fun spass_proofHandler (n) = 
   2.200 +       let val _ = File.write (File.tmp_path (Path.basic "foo_signal1")) "In signal handler now\n"
   2.201 +	   val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
   2.202 +	   val _ = File.append (File.tmp_path (Path.basic "foo_signal")) 
   2.203 +		      ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))
   2.204 +       in  (* if a proof has been found and sent back as a reconstruction proof *)
   2.205 +	 if ( (substring (reconstr, 0,1))= "[")
   2.206 +	 then 
   2.207 +	   (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   2.208 +	    Recon_Transfer.apply_res_thm reconstr goalstring;
   2.209 +	    Pretty.writeln(Pretty.str  (oct_char "361"));
   2.210 +	    
   2.211 +	    goals_being_watched := ((!goals_being_watched) - 1);
   2.212 +     
   2.213 +	    if ((!goals_being_watched) = 0)
   2.214 +	    then 
   2.215 +		let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found"))
   2.216 +			       ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")
   2.217 +		in
   2.218 +		    killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   2.219 +		end
   2.220 +	    else ()
   2.221 +	   )
   2.222 +	 (* if there's no proof, but a message from Spass *)
   2.223 +	 else if ((substring (reconstr, 0,5))= "SPASS")
   2.224 +	 then
   2.225 +	   (goals_being_watched := (!goals_being_watched) -1;
   2.226 +	    Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   2.227 +	    Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
   2.228 +	    Pretty.writeln(Pretty.str  (oct_char "361"));
   2.229 +	    if (!goals_being_watched = 0)
   2.230 +	    then 
   2.231 +	      (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   2.232 +				("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   2.233 +	       killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
   2.234 +	    else ()
   2.235 +	  ) 
   2.236 +	  (* print out a list of rules used from clasimpset*)
   2.237 +	   else if ((substring (reconstr, 0,5))= "Rules")
   2.238 +	   then
   2.239 +	     (goals_being_watched := (!goals_being_watched) -1;
   2.240 +	      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   2.241 +	       Pretty.writeln(Pretty.str (goalstring^reconstr));
   2.242 +	       Pretty.writeln(Pretty.str  (oct_char "361"));
   2.243 +	       if (!goals_being_watched = 0)
   2.244 +	       then 
   2.245 +		  (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   2.246 +			       ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   2.247 +		   killWatcher (childpid);  reapWatcher (childpid,childin, childout);())
   2.248 +	       else ()
   2.249 +	     )
   2.250 +	  
   2.251 +	    (* if proof translation failed *)
   2.252 +	    else if ((substring (reconstr, 0,5)) = "Proof")
   2.253 +	    then 
   2.254 +	      (goals_being_watched := (!goals_being_watched) -1;
   2.255 +	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   2.256 +		Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   2.257 +		Pretty.writeln(Pretty.str  (oct_char "361"));
   2.258 +		if (!goals_being_watched = 0)
   2.259 +		then 
   2.260 +		  (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   2.261 +			       ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   2.262 +		    killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
   2.263 +		else
   2.264 +		   ()
   2.265 +	     )
   2.266 +	    else  (* add something here ?*)
   2.267 +		()
   2.268 +			    
   2.269 +      end
   2.270 +	    
   2.271 +  in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   2.272 +     IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   2.273 +     (childin, childout, childpid)
   2.274  
   2.275  
   2.276    end
     3.1 --- a/src/HOL/Tools/res_atp.ML	Tue Jun 21 11:08:31 2005 +0200
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Jun 21 13:34:24 2005 +0200
     3.3 @@ -153,18 +153,15 @@
     3.4  (* should be modified to allow other provers to be called            *)
     3.5  (*********************************************************************)
     3.6  (* now passing in list of skolemized thms and list of sgterms to go with them *)
     3.7 -fun call_resolve_tac  (thms: Thm.thm list list)  sign (sg_terms:  Term.term list) (childin, childout,pid) n  = let
     3.8 +fun call_resolve_tac  (thms: Thm.thm list list)  sign (sg_terms:  Term.term list) (childin, childout,pid) n  = 
     3.9 + let
    3.10     val axfile = (File.platform_path axiom_file)
    3.11     val hypsfile = (File.platform_path hyps_file)
    3.12     val clasimpfile = (File.platform_path clasimp_file)
    3.13 -   val spass_home = getenv "SPASS_HOME"
    3.14 -   val spass = spass_home ^ "/SPASS"
    3.15 -   val _ = if File.exists (File.unpack_platform_path spass) then () 
    3.16 -	   else error ("Could not find the file " ^ spass)
    3.17       
    3.18     fun make_atp_list [] sign n = []
    3.19     |   make_atp_list ((sko_thm, sg_term)::xs) sign  n = 
    3.20 -   let 
    3.21 +     let 
    3.22  	val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 
    3.23  	val thmproofstr = proofstring ( skothmstr)
    3.24  	val no_returns =List.filter   not_newline ( thmproofstr)
    3.25 @@ -178,26 +175,32 @@
    3.26  	val _ = warning ("goalstring in make_atp_lists is: "^goalstring)
    3.27  
    3.28  	val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    3.29 -	val _ = (warning ("prob file in cal_res_tac is: "^probfile))                                                                           
    3.30 -in
    3.31 -     if !SpassComm.spass 
    3.32 -       then if !full_spass 
    3.33 -            then
    3.34 +	val _ = (warning ("prob file in cal_res_tac is: "^probfile))      
    3.35 +     in
    3.36 +       if !SpassComm.spass 
    3.37 +       then 
    3.38 +         let val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    3.39 +         in  (*We've checked that SPASS is there for ATP/spassshell to run.*)
    3.40 +           if !full_spass 
    3.41 +            then (*Allow SPASS to run in Auto mode, using all its inference rules*)
    3.42     		([("spass", thmstr, goalstring (*,spass_home*), 
    3.43 -	    	 getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*),  
    3.44 +	    	 getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",  
    3.45  	     	"-DocProof%-TimeLimit=60", 
    3.46  	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    3.47 -  	    else	
    3.48 +  	    else (*Restrict SPASS to a small set of rules that we can parse*)
    3.49     		([("spass", thmstr, goalstring (*,spass_home*), 
    3.50  	     	getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*),  
    3.51  	     	"-Auto=0%-IORe%-IOFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", 
    3.52  	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    3.53 +	 end
    3.54       else
    3.55 -	   ([("vampire", thmstr, goalstring (*,spass_home*), 
    3.56 -	    	 "/homes/jm318/Vampire8/vkernel"(*( getenv "SPASS_HOME")^"/SPASS"*),  
    3.57 -	     	"-t 300%-m 100000", 
    3.58 -	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    3.59 -end
    3.60 +       let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
    3.61 +       in  
    3.62 +	   ([("vampire", thmstr, goalstring, vampire, "-t 300%-m 100000", 
    3.63 +	      clasimpfile, axfile, hypsfile, probfile)] @ 
    3.64 +	    (make_atp_list xs sign (n+1)))
    3.65 +       end
    3.66 +     end
    3.67  
    3.68  val thms_goals = ListPair.zip( thms, sg_terms) 
    3.69  val atp_list = make_atp_list  thms_goals sign 1
    3.70 @@ -228,14 +231,14 @@
    3.71  
    3.72  
    3.73  fun get_sko_thms tfrees sign sg_terms (childin, childout,pid)  thm n sko_thms  =
    3.74 -                       if (equal n 0) then 
    3.75 -				(call_resolve_tac  (rev sko_thms) sign  sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm)
    3.76 -			else
    3.77 -                           
    3.78 -               		( SELECT_GOAL
    3.79 -  				(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    3.80 -  				 METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees;
    3.81 -                                                    get_sko_thms  tfrees sign sg_terms (childin, childout, pid) thm  (n -1) (negs::sko_thms);dummy_tac))]) n thm )
    3.82 +    if n=0 then 
    3.83 +	     (call_resolve_tac  (rev sko_thms) sign  sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm)
    3.84 +     else
    3.85 +	
    3.86 +     ( SELECT_GOAL
    3.87 +	     (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    3.88 +	      METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees;
    3.89 +				 get_sko_thms  tfrees sign sg_terms (childin, childout, pid) thm  (n -1) (negs::sko_thms);dummy_tac))]) n thm )
    3.90  
    3.91  
    3.92  
    3.93 @@ -246,21 +249,19 @@
    3.94  (**********************************************)
    3.95  
    3.96  fun isar_atp_goal' thm n tfree_lits  (childin, childout, pid) = 
    3.97 -                  
    3.98 -                           (let val  prems = prems_of thm 
    3.99 -                              (*val sg_term = get_nth k prems*)
   3.100 -                                val sign = sign_of_thm thm
   3.101 -                                val thmstring = string_of_thm thm
   3.102 -                            in   
   3.103 -                                 
   3.104 -                		(warning("in isar_atp_goal'"));
   3.105 -                                (warning("thmstring in isar_atp_goal': "^thmstring));
   3.106 - 				(* go and call callResProvers with this subgoal *)
   3.107 - 				(* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
   3.108 - 				(* recursive call to pick up the remaining subgoals *)
   3.109 -                                (* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
   3.110 -                                get_sko_thms tfree_lits sign  prems (childin, childout, pid) thm n []
   3.111 -                            end);
   3.112 +    let val  prems = prems_of thm 
   3.113 +      (*val sg_term = get_nth k prems*)
   3.114 +	val sign = sign_of_thm thm
   3.115 +	val thmstring = string_of_thm thm
   3.116 +    in   
   3.117 +	warning("in isar_atp_goal'");
   3.118 +	warning("thmstring in isar_atp_goal': "^thmstring);
   3.119 +	(* go and call callResProvers with this subgoal *)
   3.120 +	(* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
   3.121 +	(* recursive call to pick up the remaining subgoals *)
   3.122 +	(* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
   3.123 +	get_sko_thms tfree_lits sign  prems (childin, childout, pid) thm n []
   3.124 +    end ;
   3.125  
   3.126  (*fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = 
   3.127                (if (!debug) then warning (string_of_thm thm) 
     4.1 --- a/src/HOL/Tools/res_lib.ML	Tue Jun 21 11:08:31 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_lib.ML	Tue Jun 21 13:34:24 2005 +0200
     4.3 @@ -8,90 +8,100 @@
     4.4  
     4.5  signature RES_LIB =
     4.6  sig
     4.7 -
     4.8 -	val flat_noDup : ''a list list -> ''a list
     4.9 -	val list2str_sep : string -> string list -> string
    4.10 -	val list_to_string : string list -> string
    4.11 -	val list_to_string' : string list -> string
    4.12 -	val no_BDD : string -> string
    4.13 -	val no_blanks : string -> string
    4.14 -	val no_blanks_dots : string -> string
    4.15 -	val no_blanks_dots_dashes : string -> string
    4.16 -	val no_dots : string -> string
    4.17 -	val no_rep_add : ''a -> ''a list -> ''a list
    4.18 -	val no_rep_app : ''a list -> ''a list -> ''a list
    4.19 -	val pair_ins : 'a -> 'b list -> ('a * 'b) list
    4.20 -	val rm_rep : ''a list -> ''a list
    4.21 -	val write_strs : TextIO.outstream -> TextIO.vector list -> unit
    4.22 -	val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
    4.23 -
    4.24 +val flat_noDup : ''a list list -> ''a list
    4.25 +val helper_path : string -> string -> string
    4.26 +val list2str_sep : string -> string list -> string
    4.27 +val list_to_string : string list -> string
    4.28 +val list_to_string' : string list -> string
    4.29 +val no_BDD : string -> string
    4.30 +val no_blanks : string -> string
    4.31 +val no_blanks_dots : string -> string
    4.32 +val no_blanks_dots_dashes : string -> string
    4.33 +val no_dots : string -> string
    4.34 +val no_rep_add : ''a -> ''a list -> ''a list
    4.35 +val no_rep_app : ''a list -> ''a list -> ''a list
    4.36 +val pair_ins : 'a -> 'b list -> ('a * 'b) list
    4.37 +val rm_rep : ''a list -> ''a list
    4.38 +val write_strs : TextIO.outstream -> TextIO.vector list -> unit
    4.39 +val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
    4.40  end;
    4.41  
    4.42  
    4.43  structure ResLib : RES_LIB =
    4.44  struct
    4.45  
    4.46 -	(* convert a list of strings into one single string; surrounded by brackets *)
    4.47 -	fun list_to_string strings =
    4.48 -	let
    4.49 -		fun str_of [s]      = s
    4.50 -		  | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
    4.51 -		  | str_of _        = ""
    4.52 -	in
    4.53 -		"(" ^ str_of strings ^ ")"
    4.54 -	end;
    4.55 +(* convert a list of strings into one single string; surrounded by brackets *)
    4.56 +fun list_to_string strings =
    4.57 +let
    4.58 +	fun str_of [s]      = s
    4.59 +	  | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
    4.60 +	  | str_of _        = ""
    4.61 +in
    4.62 +	"(" ^ str_of strings ^ ")"
    4.63 +end;
    4.64  
    4.65 -	fun list_to_string' strings =
    4.66 -	let
    4.67 -		fun str_of [s]      = s
    4.68 -		  | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
    4.69 -		  | str_of _        = ""
    4.70 -	in
    4.71 -		"[" ^ str_of strings ^ "]"
    4.72 -	end;
    4.73 +fun list_to_string' strings =
    4.74 +let
    4.75 +	fun str_of [s]      = s
    4.76 +	  | str_of (s1::ss) = s1 ^ "," ^ (str_of ss)
    4.77 +	  | str_of _        = ""
    4.78 +in
    4.79 +	"[" ^ str_of strings ^ "]"
    4.80 +end;
    4.81  
    4.82 -	(* remove some chars (not allowed by TPTP format) from a string *)
    4.83 -	fun no_blanks " " = "_"
    4.84 -	  | no_blanks c   = c;
    4.85 +(* remove some chars (not allowed by TPTP format) from a string *)
    4.86 +fun no_blanks " " = "_"
    4.87 +  | no_blanks c   = c;
    4.88 +
    4.89 +fun no_dots "." = "_dot_"
    4.90 +  | no_dots c   = c;
    4.91  
    4.92 -	fun no_dots "." = "_dot_"
    4.93 -	  | no_dots c   = c;
    4.94 +fun no_blanks_dots " " = "_"
    4.95 +  | no_blanks_dots "." = "_dot_"
    4.96 +  | no_blanks_dots c   = c;
    4.97  
    4.98 -	fun no_blanks_dots " " = "_"
    4.99 -	  | no_blanks_dots "." = "_dot_"
   4.100 -	  | no_blanks_dots c   = c;
   4.101 +fun no_blanks_dots_dashes " " = "_"
   4.102 +  | no_blanks_dots_dashes "." = "_dot_"
   4.103 +  | no_blanks_dots_dashes "'" = "_da_"
   4.104 +  | no_blanks_dots_dashes c   = c;
   4.105  
   4.106 -	fun no_blanks_dots_dashes " " = "_"
   4.107 -	  | no_blanks_dots_dashes "." = "_dot_"
   4.108 -	  | no_blanks_dots_dashes "'" = "_da_"
   4.109 -	  | no_blanks_dots_dashes c   = c;
   4.110 +fun no_BDD cs =
   4.111 +	implode (map no_blanks_dots_dashes (explode cs));
   4.112 +
   4.113 +fun no_rep_add x []     = [x]
   4.114 +  | no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z);
   4.115 +
   4.116 +fun no_rep_app l1 []     = l1
   4.117 +  | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
   4.118  
   4.119 -	fun no_BDD cs =
   4.120 -		implode (map no_blanks_dots_dashes (explode cs));
   4.121 +fun rm_rep []     = []
   4.122 +  | rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y);
   4.123  
   4.124 -	fun no_rep_add x []     = [x]
   4.125 -	  | no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z);
   4.126 +fun flat_noDup []     = []
   4.127 +  | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
   4.128  
   4.129 -	fun no_rep_app l1 []     = l1
   4.130 -	  | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
   4.131 +fun list2str_sep delim []      = delim
   4.132 +  | list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss);
   4.133  
   4.134 -	fun rm_rep []     = []
   4.135 -	  | rm_rep (x::y) = if x mem y then rm_rep y else x::(rm_rep y);
   4.136 +fun write_strs _   []      = ()
   4.137 +  | write_strs out (s::ss) = (TextIO.output (out, s); write_strs out ss);
   4.138  
   4.139 -	fun flat_noDup []     = []
   4.140 -	  | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
   4.141 -
   4.142 -	fun list2str_sep delim []      = delim
   4.143 -	  | list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss);
   4.144 +fun writeln_strs _   []      = ()
   4.145 +  | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
   4.146  
   4.147 -	fun write_strs _   []      = ()
   4.148 -	  | write_strs out (s::ss) = (TextIO.output (out, s); write_strs out ss);
   4.149 -
   4.150 -	fun writeln_strs _   []      = ()
   4.151 -	  | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
   4.152 -
   4.153 -	(* pair the first argument with each element in the second input list *)
   4.154 -	fun pair_ins x []      = []
   4.155 -	  | pair_ins x (y::ys) = (x, y) :: (pair_ins x ys);
   4.156 +(* pair the first argument with each element in the second input list *)
   4.157 +fun pair_ins x []      = []
   4.158 +  | pair_ins x (y::ys) = (x, y) :: (pair_ins x ys);
   4.159 +  
   4.160 +(*Return the path to a "helper" like SPASS or tptp2X, first checking that
   4.161 +  it exists. --lcp *)  
   4.162 +fun helper_path evar base =
   4.163 +  case getenv evar of
   4.164 +      "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
   4.165 +    | home => 
   4.166 +        let val path = home ^ "/" ^ base
   4.167 +        in  if File.exists (File.unpack_platform_path path) then path 
   4.168 +	    else error ("Could not find the file " ^ path)
   4.169 +	end;  
   4.170  
   4.171  end;