Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
authorpaulson
Fri Sep 09 17:47:37 2005 +0200 (2005-09-09)
changeset 173173f12de2e2e6e
parent 17316 fc7cc8137b97
child 17318 bc1c75855f3d
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Sep 09 12:18:15 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Sep 09 17:47:37 2005 +0200
     1.3 @@ -172,8 +172,7 @@
     1.4       (***********************************************)
     1.5    
     1.6        val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums 
     1.7 -      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
     1.8 -  
     1.9 +      val clasimp_names = map (ResClause.get_axiomName o #1) clasimp_names_cls
    1.10        val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    1.11                           (concat clasimp_names)
    1.12        val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    1.13 @@ -541,37 +540,22 @@
    1.14  (* then show for the last step *)
    1.15  
    1.16  (* replace ~ by not here *)
    1.17 -fun change_nots [] = []
    1.18 -|   change_nots (x::xs) = if x = "~" 
    1.19 -                          then 
    1.20 -                             ["\\", "<", "n", "o", "t", ">"]@(change_nots xs)
    1.21 -                          else (x::(change_nots xs))
    1.22 +val change_nots = String.translate (fn c => if c = #"~" then "\\<not>" else str c);
    1.23  
    1.24 -(*
    1.25 -fun clstrs_to_string [] str = str
    1.26 -|   clstrs_to_string (x::[]) str = str^x
    1.27 -|   clstrs_to_string (x::xs) str = clstrs_to_string xs (str^(x^"; "))
    1.28 -*)
    1.29 -fun clstrs_to_string [] str = implode (change_nots (explode str))
    1.30 -|   clstrs_to_string (x::[]) str = implode (change_nots (explode (str^x)))
    1.31 -|   clstrs_to_string (x::xs) str = implode (change_nots (explode (clstrs_to_string xs (str^(x^"; ")))))
    1.32 -
    1.33 -
    1.34 +fun clstrs_to_string xs = space_implode "; " (map change_nots xs);
    1.35  
    1.36  fun thmvars_to_quantstring [] str = str
    1.37  |   thmvars_to_quantstring (x::[]) str =str^x^". "
    1.38  |   thmvars_to_quantstring (x::xs) str = thmvars_to_quantstring xs (str^(x^" "))
    1.39  
    1.40  
    1.41 -fun clause_strs_to_isar clstrs [] =  "\"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\""
    1.42 -|   clause_strs_to_isar clstrs thmvars = "\"\\<And>"^(thmvars_to_quantstring thmvars "")^"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\""
    1.43 +fun clause_strs_to_isar clstrs [] =
    1.44 +      "\"\\<lbrakk>"^(clstrs_to_string clstrs)^"\\<rbrakk> \\<Longrightarrow> False\""
    1.45 +|   clause_strs_to_isar clstrs thmvars =
    1.46 +      "\"\\<And>"^(thmvars_to_quantstring thmvars "")^
    1.47 +      "\\<lbrakk>"^(clstrs_to_string clstrs)^"\\<rbrakk> \\<Longrightarrow> False\""
    1.48  
    1.49 -fun frees_to_string [] str = implode (change_nots (explode str))
    1.50 -|   frees_to_string (x::[]) str = implode (change_nots (explode (str^x)))
    1.51 -|   frees_to_string  (x::xs) str = implode (change_nots (explode (frees_to_string xs (str^(x^" ")))))
    1.52 -
    1.53 -fun frees_to_isar_str [] =  ""
    1.54 -|   frees_to_isar_str  clstrs = (frees_to_string clstrs "")
    1.55 +fun frees_to_isar_str clstrs = space_implode " " (map change_nots clstrs)
    1.56  
    1.57  
    1.58  (***********************************************************************)
     2.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Sep 09 12:18:15 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Sep 09 17:47:37 2005 +0200
     2.3 @@ -87,15 +87,12 @@
     2.4  
     2.5  
     2.6  fun reap(pid, instr, outstr) =
     2.7 -        let
     2.8 -		val u = TextIO.closeIn instr;
     2.9 -	        val u = TextIO.closeOut outstr;
    2.10 -	
    2.11 -		val (_, status) =
    2.12 -			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    2.13 -	in
    2.14 -		status
    2.15 -	end
    2.16 +  let val u = TextIO.closeIn instr;
    2.17 +      val u = TextIO.closeOut outstr;
    2.18 +      val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    2.19 +  in
    2.20 +	  status
    2.21 +  end
    2.22  
    2.23  fun fdReader (name : string, fd : Posix.IO.file_desc) =
    2.24  	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    2.25 @@ -106,8 +103,7 @@
    2.26                initBlkMode = true,
    2.27                name = name,  
    2.28                chunkSize=4096,
    2.29 -              fd = fd
    2.30 -            };
    2.31 +              fd = fd};
    2.32  
    2.33  fun openOutFD (name, fd) =
    2.34  	  TextIO.mkOutstream (
    2.35 @@ -125,38 +121,31 @@
    2.36  
    2.37  fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
    2.38  
    2.39 -fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
    2.40 -
    2.41 -fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = (prover,(cmd, (instr,outstr)));
    2.42 +fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
    2.43  
    2.44 -fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = proc_handle;
    2.45 +fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = 
    2.46 +  (prover,(cmd, (instr,outstr)));
    2.47  
    2.48 -fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (prover);
    2.49 -
    2.50 -fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (thmstring);
    2.51 +fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = 
    2.52 +  proc_handle;
    2.53  
    2.54 -fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (goalstring);
    2.55 -
    2.56 -fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
    2.57 +fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  =
    2.58 +  prover;
    2.59  
    2.60 -(********************************************************************************************)
    2.61 -(*  takes a list of arguments and sends them individually to the watcher process by pipe    *)
    2.62 -(********************************************************************************************)
    2.63 +fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = 
    2.64 +  thmstring;
    2.65  
    2.66 -fun outputArgs (toWatcherStr, []) = ()
    2.67 -|   outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); 
    2.68 -                                          TextIO.flushOut toWatcherStr;
    2.69 -                                         outputArgs (toWatcherStr, xs))
    2.70 +fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  =
    2.71 +  goalstring;
    2.72 +
    2.73  
    2.74  (********************************************************************************)
    2.75  (*    gets individual args from instream and concatenates them into a list      *)
    2.76  (********************************************************************************)
    2.77  
    2.78 -fun getArgs (fromParentStr, toParentStr,ys) =  let 
    2.79 -                                       val thisLine = TextIO.input fromParentStr
    2.80 -                                    in
    2.81 -                                        ((ys@[thisLine]))
    2.82 -                                    end
    2.83 +fun getArgs (fromParentStr, toParentStr, ys) =  
    2.84 +  let val thisLine = TextIO.input fromParentStr
    2.85 +  in ys@[thisLine] end
    2.86  
    2.87                              
    2.88  (********************************************************************************)
    2.89 @@ -164,7 +153,7 @@
    2.90  (********************************************************************************)
    2.91                      
    2.92  fun callResProver (toWatcherStr,  arg) = 
    2.93 -      (sendOutput (toWatcherStr, arg^"\n"); 
    2.94 +      (TextIO.output (toWatcherStr, arg^"\n"); 
    2.95         TextIO.flushOut toWatcherStr)
    2.96  
    2.97  (*****************************************************************************************)
    2.98 @@ -175,14 +164,14 @@
    2.99      
   2.100  (*Uses the $-character to separate items sent to watcher*)
   2.101  fun callResProvers (toWatcherStr,  []) = 
   2.102 -      (sendOutput (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
   2.103 +      (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
   2.104  |   callResProvers (toWatcherStr,
   2.105                      (prover,thmstring,goalstring, proverCmd,settings, 
   2.106                       axfile, hypsfile,probfile)  ::  args) =
   2.107        let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
   2.108                               (prover^thmstring^goalstring^proverCmd^settings^
   2.109                                hypsfile^probfile)
   2.110 -      in sendOutput (toWatcherStr,    
   2.111 +      in TextIO.output (toWatcherStr,    
   2.112              (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^
   2.113               settings^"$"^hypsfile^"$"^probfile^"\n"));
   2.114           goals_being_watched := (!goals_being_watched) + 1;
   2.115 @@ -196,7 +185,7 @@
   2.116  (* Send message to watcher to kill currently running vampires *)
   2.117  (**************************************************************)
   2.118  
   2.119 -fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 
   2.120 +fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n"); 
   2.121                              TextIO.flushOut toWatcherStr)
   2.122  
   2.123  
   2.124 @@ -262,7 +251,7 @@
   2.125  	     TextIO.flushOut toParentStr;
   2.126  	   (("","","","Kill children",[],"")::cmdList)
   2.127  	  )
   2.128 -     else  let val thisCmd = getCmd (thisLine) 
   2.129 +     else  let val thisCmd = getCmd thisLine 
   2.130  	       (*********************************************************)
   2.131  	       (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   2.132  	       (* i.e. put back into tuple format                       *)
   2.133 @@ -270,7 +259,7 @@
   2.134  	   in
   2.135  	     (*TextIO.output (toParentStr, thisCmd); 
   2.136  	       TextIO.flushOut toParentStr;*)
   2.137 -	       getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
   2.138 +	       getCmds (toParentStr, fromParentStr, (thisCmd::cmdList))
   2.139  	   end
   2.140    end
   2.141  	    
   2.142 @@ -302,16 +291,15 @@
   2.143      (** pipes for communication between parent and watcher **)
   2.144      val p1 = Posix.IO.pipe ()
   2.145      val p2 = Posix.IO.pipe ()
   2.146 -    fun closep () = (
   2.147 -	  Posix.IO.close (#outfd p1); 
   2.148 +    fun closep () = 
   2.149 +	 (Posix.IO.close (#outfd p1); 
   2.150  	  Posix.IO.close (#infd p1);
   2.151  	  Posix.IO.close (#outfd p2); 
   2.152 -	  Posix.IO.close (#infd p2)
   2.153 -	)
   2.154 +	  Posix.IO.close (#infd p2))
   2.155      (***********************************************************)
   2.156      (****** fork a watcher process and get it set up and going *)
   2.157      (***********************************************************)
   2.158 -    fun startWatcher (procList) =
   2.159 +    fun startWatcher procList =
   2.160       (case  Posix.Process.fork() (***************************************)
   2.161        of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   2.162  				    (***************************************)
   2.163 @@ -338,7 +326,7 @@
   2.164  	 (*************************************************************)
   2.165  
   2.166  	 fun pollParentInput () = 
   2.167 -	   let val pd = OS.IO.pollDesc (fromParentIOD)
   2.168 +	   let val pd = OS.IO.pollDesc fromParentIOD
   2.169  	   in 
   2.170  	     if isSome pd then 
   2.171  		 let val pd' = OS.IO.pollIn (valOf pd)
   2.172 @@ -356,7 +344,7 @@
   2.173  	       else NONE
   2.174  	   end
   2.175  		 
   2.176 -	  fun pollChildInput (fromStr) = 
   2.177 +	  fun pollChildInput fromStr = 
   2.178  	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
   2.179  			 ("In child_poll\n")
   2.180  	       val iod = getInIoDesc fromStr
   2.181 @@ -465,31 +453,13 @@
   2.182  
   2.183  (*** add subgoal id num to this *)
   2.184  	fun execCmds  [] procList = procList
   2.185 -	|   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =             let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child"))  ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   2.186 -	  in 
   2.187 -	    if prover = "spass"
   2.188 -	    then 
   2.189 -	      let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   2.190 -		       (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   2.191 -		  val (instr, outstr) = Unix.streamsOf childhandle
   2.192 -		  val newProcList =    (((CMDPROC{
   2.193 -				       prover = prover,
   2.194 -				       cmd = file,
   2.195 -				       thmstring = thmstring,
   2.196 -				       goalstring = goalstring,
   2.197 -				       proc_handle = childhandle,
   2.198 -				       instr = instr,
   2.199 -				       outstr = outstr })::procList))
   2.200 -		   val _ = File.append (File.tmp_path (Path.basic "exec_child"))  
   2.201 -			("\nexecuting command for goal:\n"^
   2.202 -			 goalstring^proverCmd^(concat settings)^file^
   2.203 -			 " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   2.204 -	      in
   2.205 -		 Posix.Process.sleep (Time.fromSeconds 1);
   2.206 -		 execCmds cmds newProcList
   2.207 -	      end
   2.208 -	    else 
   2.209 -	      let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   2.210 +	|   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =
   2.211 +	      let val _ = File.write (File.tmp_path (Path.basic "exec_child"))  
   2.212 +	                    (space_implode "\n" 
   2.213 +	                      (["About to execute command for goal:",
   2.214 +	                        goalstring, proverCmd] @ settings @
   2.215 +	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   2.216 +	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   2.217  		       (Unix.execute(proverCmd, (settings@[file])))
   2.218  		  val (instr, outstr) = Unix.streamsOf childhandle
   2.219  		  
   2.220 @@ -503,20 +473,18 @@
   2.221  				       outstr = outstr }) :: procList
   2.222       
   2.223  		  val _ = File.append (File.tmp_path (Path.basic "exec_child")) 
   2.224 -			    ("executing command for goal:\n"^
   2.225 -			     goalstring^proverCmd^(concat settings)^file^
   2.226 -			     " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   2.227 +			    ("\nFinished at " ^
   2.228 +			     Date.toString(Date.fromTimeLocal(Time.now())))
   2.229  	      in
   2.230  		Posix.Process.sleep (Time.fromSeconds 1); 
   2.231  		execCmds cmds newProcList
   2.232  	      end
   2.233 -	   end
   2.234  
   2.235  
   2.236       (****************************************)                  
   2.237       (* call resolution processes remotely   *)
   2.238       (* settings should be a list of strings *)
   2.239 -     (* e.g. ["-t 300", "-m 100000"]         *)
   2.240 +     (* e.g. ["-t300", "-m100000"]         *)
   2.241       (****************************************)
   2.242  
   2.243        (*  fun execRemoteCmds  [] procList = procList
   2.244 @@ -527,23 +495,19 @@
   2.245  				      end
   2.246  *)
   2.247  
   2.248 -	fun printList (outStr, []) = ()
   2.249 -	|   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   2.250 -
   2.251 -
   2.252       (**********************************************)                  
   2.253       (* Watcher Loop                               *)
   2.254       (**********************************************)
   2.255           val iterations_left = ref 1000;  (*200 seconds, 5 iterations per sec*)
   2.256  
   2.257  	 fun keepWatching (toParentStr, fromParentStr,procList) = 
   2.258 -	   let fun loop (procList) =  
   2.259 +	   let fun loop procList =  
   2.260  		let val _ = Posix.Process.sleep (Time.fromMilliseconds 200)
   2.261  		    val cmdsFromIsa = pollParentInput ()
   2.262  		    fun killchildHandler ()  = 
   2.263  			  (TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   2.264  			   TextIO.flushOut toParentStr;
   2.265 -			   killChildren (map (cmdchildHandle) procList);
   2.266 +			   killChildren (map cmdchildHandle procList);
   2.267  			   ())
   2.268  		in 
   2.269  		   (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   2.270 @@ -583,7 +547,7 @@
   2.271  			   loop newProcList'
   2.272  			 end
   2.273  		   else (* No new input from Isabelle *)
   2.274 -		     let val newProcList = checkChildren ((procList), toParentStr)
   2.275 +		     let val newProcList = checkChildren (procList, toParentStr)
   2.276  		     in
   2.277  		      (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
   2.278  		       loop newProcList
   2.279 @@ -625,7 +589,7 @@
   2.280      (*******************************)
   2.281  
   2.282      val procList = []
   2.283 -    val pid = startWatcher (procList)
   2.284 +    val pid = startWatcher procList
   2.285      (**************************************************)
   2.286      (* communication streams to watcher               *)
   2.287      (**************************************************)
   2.288 @@ -680,10 +644,10 @@
   2.289       val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   2.290       val _ = debug ("subgoals forked to createWatcher: "^prems_string);
   2.291  (*FIXME: do we need an E proofHandler??*)
   2.292 -     fun vampire_proofHandler (n) =
   2.293 +     fun vampire_proofHandler n =
   2.294  	(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   2.295  	 VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))               
   2.296 -     fun spass_proofHandler (n) = (
   2.297 +     fun spass_proofHandler n = (
   2.298         let val _ = File.append (File.tmp_path (Path.basic "spass_signal_in"))
   2.299                                 "Starting SPASS signal handler\n"
   2.300  	   val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
   2.301 @@ -717,7 +681,7 @@
   2.302  	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   2.303  	              ("Reaping a watcher, goals watched is: " ^
   2.304  	                 (string_of_int (!goals_being_watched))^"\n");
   2.305 -	             killWatcher (childpid); reapWatcher (childpid,childin, childout); ())
   2.306 +	             killWatcher childpid; reapWatcher (childpid,childin, childout); ())
   2.307  		else () ) 
   2.308  	(* print out a list of rules used from clasimpset*)
   2.309  	 else if substring (reconstr, 0,5) = "Rules"
   2.310 @@ -729,7 +693,7 @@
   2.311  	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   2.312  	              ("Reaping a watcher, goals watched is: " ^
   2.313  	                 (string_of_int (!goals_being_watched))^"\n");
   2.314 -	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   2.315 +	             killWatcher childpid;  reapWatcher (childpid,childin, childout);()
   2.316  		     )
   2.317  	       else () )
   2.318  	  (* if proof translation failed *)
   2.319 @@ -742,7 +706,7 @@
   2.320  	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   2.321  	              ("Reaping a watcher, goals watched is: " ^
   2.322  	                 (string_of_int (!goals_being_watched))^"\n");
   2.323 -	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   2.324 +	             killWatcher childpid;  reapWatcher (childpid,childin, childout);()
   2.325  		     )
   2.326  	       else () )
   2.327  
   2.328 @@ -755,7 +719,7 @@
   2.329  	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   2.330  	              ("Reaping a watcher, goals watched is: " ^
   2.331  	                 (string_of_int (!goals_being_watched))^"\n");
   2.332 -	             killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   2.333 +	             killWatcher childpid;  reapWatcher (childpid,childin, childout);()
   2.334  		     )
   2.335  	       else () )
   2.336  
   2.337 @@ -768,7 +732,7 @@
   2.338  	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   2.339  		     ("Reaping a watcher, goals watched is: " ^
   2.340  			(string_of_int (!goals_being_watched))^"\n");
   2.341 -		    killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   2.342 +		    killWatcher childpid;  reapWatcher (childpid,childin, childout);()
   2.343  		    )
   2.344  	       else () )
   2.345         end)
     3.1 --- a/src/HOL/Tools/res_atp.ML	Fri Sep 09 12:18:15 2005 +0200
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Sep 09 17:47:37 2005 +0200
     3.3 @@ -24,7 +24,7 @@
     3.4  
     3.5  val prover = ref "spass";   (* use spass as default prover *)
     3.6  val custom_spass =   (*specialized options for SPASS*)
     3.7 -      ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
     3.8 +      ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
     3.9             "-DocProof","-TimeLimit=60"];
    3.10  
    3.11  val axiom_file = File.tmp_path (Path.basic "axioms");
    3.12 @@ -147,6 +147,8 @@
    3.13              val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
    3.14              val _ = debug ("prob file in call_resolve_tac is " ^ probfile)
    3.15            in
    3.16 +            (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
    3.17 +              versions of Unix.execute treat them differently!*)
    3.18              if !prover = "spass"
    3.19              then
    3.20                let val optionline = 
    3.21 @@ -154,7 +156,7 @@
    3.22  		          (*Proof reconstruction works for only a limited set of 
    3.23  		            inference rules*)
    3.24                        then "-" ^ space_implode "%-" (!custom_spass)
    3.25 -                      else "-DocProof%-TimeLimit=60%-SOS" (*Auto mode*)
    3.26 +                      else "-DocProof%-TimeLimit=60%-SOS%-FullRed=0" (*Auto mode*)
    3.27                    val _ = debug ("SPASS option string is " ^ optionline)
    3.28                    val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    3.29                      (*We've checked that SPASS is there for ATP/spassshell to run.*)
    3.30 @@ -168,7 +170,7 @@
    3.31  	    then 
    3.32                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
    3.33                in
    3.34 -                ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000",
    3.35 +                ([("vampire", thmstr, goalstring, vampire, "-t60%-m100000",
    3.36                     axfile, hypsfile, probfile)] @
    3.37                   (make_atp_list xs sign (n+1)))
    3.38                end
     4.1 --- a/src/HOL/Tools/res_clause.ML	Fri Sep 09 12:18:15 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Sep 09 17:47:37 2005 +0200
     4.3 @@ -27,7 +27,7 @@
     4.4      val make_conjecture_clause_thm : Thm.thm -> clause
     4.5      val make_hypothesis_clause : Term.term -> clause
     4.6      val special_equal : bool ref
     4.7 -    val clause_info : clause ->  string * string
     4.8 +    val get_axiomName : clause ->  string
     4.9      val typed : unit -> unit
    4.10      val untyped : unit -> unit
    4.11      val num_of_clauses : clause -> int
    4.12 @@ -35,7 +35,7 @@
    4.13      val dfg_clauses2str : string list -> string
    4.14      val clause2dfg : clause -> string * string list
    4.15      val clauses2dfg : clause list -> string -> clause list -> clause list ->
    4.16 -                      (string * int) list -> (string * int) list -> string list -> string
    4.17 +             (string * int) list -> (string * int) list -> string list -> string
    4.18      val tfree_dfg_clause : string -> string
    4.19  
    4.20      val tptp_arity_clause : arityClause -> string
    4.21 @@ -70,8 +70,8 @@
    4.22  val tfree_prefix = "t_";
    4.23  
    4.24  val clause_prefix = "cls_"; 
    4.25 -
    4.26  val arclause_prefix = "arcls_" 
    4.27 +val clrelclause_prefix = "relcls_";
    4.28  
    4.29  val const_prefix = "c_";
    4.30  val tconst_prefix = "tc_"; 
    4.31 @@ -178,8 +178,8 @@
    4.32  val id_ref = ref 0;
    4.33  
    4.34  fun generate_id () = 
    4.35 -     let val id = !id_ref
    4.36 -    in id_ref := id + 1; id end;
    4.37 +  let val id = !id_ref
    4.38 +  in id_ref := id + 1; id end;
    4.39  
    4.40  
    4.41  
    4.42 @@ -196,13 +196,12 @@
    4.43  datatype type_literal = LTVar of string | LTFree of string;
    4.44  
    4.45  
    4.46 -datatype folTerm = UVar of string * fol_type| Fun of string * fol_type * folTerm list;
    4.47 +datatype folTerm = UVar of string * fol_type
    4.48 +                 | Fun of string * fol_type * folTerm list;
    4.49  datatype predicate = Predicate of pred_name * fol_type * folTerm list;
    4.50  
    4.51 -
    4.52  datatype literal = Literal of polarity * predicate * tag;
    4.53  
    4.54 -
    4.55  datatype typ_var = FOLTVar of indexname | FOLTFree of string;
    4.56  
    4.57  
    4.58 @@ -220,17 +219,20 @@
    4.59                      functions: (string*int) list};
    4.60  
    4.61  
    4.62 -
    4.63  exception CLAUSE of string;
    4.64  
    4.65  
    4.66 -
    4.67  (*** make clauses ***)
    4.68  
    4.69 +fun isFalse (Literal (pol,Predicate(a,_,[]),_)) =
    4.70 +      (pol andalso a = "c_False") orelse
    4.71 +      (not pol andalso a = "c_True")
    4.72 +  | isFalse _ = false;
    4.73 +
    4.74  fun make_clause (clause_id,axiom_name,kind,literals,
    4.75                   types_sorts,tvar_type_literals,
    4.76                   tfree_type_literals,tvars, predicates, functions) =
    4.77 -  if null literals 
    4.78 +  if forall isFalse literals 
    4.79    then error "Problem too trivial for resolution (empty clause)"
    4.80    else
    4.81       Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, 
    4.82 @@ -241,6 +243,20 @@
    4.83               functions = functions};
    4.84  
    4.85  
    4.86 +(** Some Clause destructor functions **)
    4.87 +
    4.88 +fun string_of_kind (Clause cls) = name_of_kind (#kind cls);
    4.89 +
    4.90 +fun get_axiomName (Clause cls) = #axiom_name cls;
    4.91 +
    4.92 +fun get_clause_id (Clause cls) = #clause_id cls;
    4.93 +
    4.94 +fun funcs_of_cls (Clause cls) = #functions cls;
    4.95 +
    4.96 +fun preds_of_cls (Clause cls) = #predicates cls;
    4.97 +
    4.98 +
    4.99 +
   4.100  (*Definitions of the current theory--to allow suppressing types.*)
   4.101  val curr_defs = ref Defs.empty;
   4.102  
   4.103 @@ -640,16 +656,6 @@
   4.104  	       | _ => classrelClauses_of_aux (sub, sups);
   4.105  
   4.106  
   4.107 -
   4.108 -(***** convert clauses to DFG format *****)
   4.109 -
   4.110 -fun string_of_clauseID (Clause cls) = 
   4.111 -    clause_prefix ^ string_of_int (#clause_id cls);
   4.112 -
   4.113 -fun string_of_kind (Clause cls) = name_of_kind (#kind cls);
   4.114 -
   4.115 -fun string_of_axiomName (Clause cls) = #axiom_name cls;
   4.116 -
   4.117  (****!!!! Changed for typed equality !!!!****)
   4.118  
   4.119  fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")";
   4.120 @@ -686,6 +692,12 @@
   4.121  	  else name ^ (ResLib.list_to_string terms_as_strings) 
   4.122        end;
   4.123  
   4.124 +
   4.125 +fun string_of_clausename (cls_id,ax_name) = 
   4.126 +    clause_prefix ^ ascii_of ax_name ^ "_" ^ string_of_int cls_id;
   4.127 +
   4.128 +fun string_of_type_clsname (cls_id,ax_name,idx) = 
   4.129 +    string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (string_of_int idx);
   4.130      
   4.131  
   4.132  (********************************)
   4.133 @@ -714,22 +726,14 @@
   4.134    | forall_close (vars,tvars) = ")"
   4.135  
   4.136  fun gen_dfg_cls (cls_id,ax_name,knd,lits,tvars,vars) = 
   4.137 -    let val ax_str = 
   4.138 -              if ax_name = "" then cls_id 
   4.139 -              else cls_id ^ "_" ^ ascii_of ax_name
   4.140 -    in
   4.141 -	"clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
   4.142 -	"or(" ^ lits ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
   4.143 -	ax_str ^  ")."
   4.144 -    end;
   4.145 +    "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
   4.146 +    "or(" ^ lits ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
   4.147 +    string_of_clausename (cls_id,ax_name) ^  ").";
   4.148  
   4.149 -fun gen_dfg_type_cls (cls_id,knd,tfree_lit,idx,tvars,vars) = 
   4.150 -    let val ax_str = cls_id ^ "_tcs" ^ (string_of_int idx)
   4.151 -    in
   4.152 -	"clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
   4.153 -	"or( " ^ tfree_lit ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
   4.154 -	ax_str ^  ")."
   4.155 -    end;
   4.156 +fun gen_dfg_type_cls (cls_id,ax_name,knd,tfree_lit,idx,tvars,vars) = 
   4.157 +    "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
   4.158 +    "or( " ^ tfree_lit ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
   4.159 +    string_of_type_clsname (cls_id,ax_name,idx) ^  ").";
   4.160  
   4.161  fun dfg_clause_aux (Clause cls) = 
   4.162    let val lits = map dfg_literal (#literals cls)
   4.163 @@ -767,8 +771,8 @@
   4.164  
   4.165  
   4.166  fun dfg_vars (Clause cls) =
   4.167 -    let val  lits =  (#literals cls)
   4.168 -        val  folterms = mergelist(map dfg_folterms lits)
   4.169 +    let val lits =  (#literals cls)
   4.170 +        val folterms = mergelist(map dfg_folterms lits)
   4.171          val vars =  ResLib.flat_noDup(map get_uvars folterms)	
   4.172      in 
   4.173          vars
   4.174 @@ -787,7 +791,8 @@
   4.175  	
   4.176  (* make this return funcs and preds too? *)
   4.177  
   4.178 -    fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms)
   4.179 +fun string_of_predicate (Predicate("equal",typ,terms)) =  
   4.180 +      string_of_equality(typ,terms)
   4.181    | string_of_predicate (Predicate(name,_,[])) = name 
   4.182    | string_of_predicate (Predicate(name,typ,terms)) = 
   4.183        let val terms_as_strings = map string_of_term terms
   4.184 @@ -810,26 +815,20 @@
   4.185               (*"lits" includes the typing assumptions (TVars)*)
   4.186          val vars = dfg_vars cls
   4.187          val tvars = dfg_tvars cls
   4.188 -	val cls_id = string_of_clauseID cls
   4.189 -	val ax_name = string_of_axiomName cls
   4.190  	val knd = string_of_kind cls
   4.191  	val lits_str = commas lits
   4.192 -	val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars, vars) 			
   4.193 +	val cls_id = get_clause_id cls
   4.194 +	val axname = get_axiomName cls
   4.195 +	val cls_str = gen_dfg_cls(cls_id,axname,knd,lits_str,tvars, vars) 			
   4.196          fun typ_clss k [] = []
   4.197            | typ_clss k (tfree :: tfrees) = 
   4.198 -              (gen_dfg_type_cls(cls_id,knd,tfree,k, tvars,vars)) :: 
   4.199 +              (gen_dfg_type_cls(cls_id,axname,knd,tfree,k, tvars,vars)) :: 
   4.200                (typ_clss (k+1) tfrees)
   4.201      in 
   4.202  	cls_str :: (typ_clss 0 tfree_lits)
   4.203      end;
   4.204  
   4.205 -fun clause_info cls = (string_of_axiomName cls, string_of_clauseID cls);
   4.206 -
   4.207 -fun funcs_of_cls (Clause cls) = #functions cls;
   4.208 -
   4.209 -fun preds_of_cls (Clause cls) = #predicates cls;
   4.210 -
   4.211 -fun string_of_arity (name, num) =  name ^"," ^ (string_of_int num) 
   4.212 +fun string_of_arity (name, num) =  name ^ "," ^ (string_of_int num) 
   4.213  
   4.214  fun string_of_preds preds = 
   4.215    "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n";
   4.216 @@ -865,8 +864,8 @@
   4.217  fun clause2dfg cls =
   4.218      let val (lits,tfree_lits) = dfg_clause_aux cls 
   4.219              (*"lits" includes the typing assumptions (TVars)*)
   4.220 -	val cls_id = string_of_clauseID cls
   4.221 -	val ax_name = string_of_axiomName cls
   4.222 +	val cls_id = get_clause_id cls
   4.223 +	val ax_name = get_axiomName cls
   4.224          val vars = dfg_vars cls
   4.225          val tvars = dfg_tvars cls
   4.226          val funcs = funcs_of_cls cls
   4.227 @@ -911,8 +910,8 @@
   4.228   | clauses2dfg (cls::clss) probname axioms conjectures funcs preds tfrees = 
   4.229       let val (lits,tfree_lits) = dfg_clause_aux cls
   4.230  	       (*"lits" includes the typing assumptions (TVars)*)
   4.231 -	 val cls_id = string_of_clauseID cls
   4.232 -	 val ax_name = string_of_axiomName cls
   4.233 +	 val cls_id = get_clause_id cls
   4.234 +	 val ax_name = get_axiomName cls
   4.235  	 val vars = dfg_vars cls
   4.236  	 val tvars = dfg_tvars cls
   4.237  	 val funcs' = distinct((funcs_of_cls cls)@funcs)
   4.238 @@ -973,28 +972,6 @@
   4.239      end;
   4.240  
   4.241  
   4.242 -val clrelclause_prefix = "relcls_";
   4.243 -
   4.244 -(* FIX later.  Doesn't seem to be used in clasimp *)
   4.245 -
   4.246 -(*fun tptp_classrelLits sub sup = 
   4.247 -    let val tvar = "(T)"
   4.248 -    in 
   4.249 -	case sup of NONE => "[++" ^ sub ^ tvar ^ "]"
   4.250 -		  | (SOME supcls) =>  "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]"
   4.251 -    end;
   4.252 -
   4.253 -
   4.254 -fun tptp_classrelClause (ClassrelClause cls) =
   4.255 -    let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls)
   4.256 -	val sub = #subclass cls
   4.257 -	val sup = #superclass cls
   4.258 -	val lits = tptp_classrelLits sub sup
   4.259 -    in
   4.260 -	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")."
   4.261 -    end; 
   4.262 -    *)
   4.263 -
   4.264  (********************************)
   4.265  (* code to produce TPTP files   *)
   4.266  (********************************)
   4.267 @@ -1015,13 +992,11 @@
   4.268   
   4.269  
   4.270  fun gen_tptp_cls (cls_id,ax_name,knd,lits) = 
   4.271 -    let val ax_str = (if ax_name = "" then "" else ("_" ^ ascii_of ax_name))
   4.272 -    in
   4.273 -	"input_clause(" ^ cls_id ^ ax_str ^ "," ^ knd ^ "," ^ lits ^ ")."
   4.274 -    end;
   4.275 +    "input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
   4.276 +    knd ^ "," ^ lits ^ ").";
   4.277  
   4.278 -fun gen_tptp_type_cls (cls_id,knd,tfree_lit,idx) = 
   4.279 -    "input_clause(" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ "," ^ 
   4.280 +fun gen_tptp_type_cls (cls_id,ax_name,knd,tfree_lit,idx) = 
   4.281 +    "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
   4.282      knd ^ ",[" ^ tfree_lit ^ "]).";
   4.283  
   4.284  fun tptp_clause_aux (Clause cls) = 
   4.285 @@ -1041,14 +1016,15 @@
   4.286  fun tptp_clause cls =
   4.287      let val (lits,tfree_lits) = tptp_clause_aux cls 
   4.288              (*"lits" includes the typing assumptions (TVars)*)
   4.289 -	val cls_id = string_of_clauseID cls
   4.290 -	val ax_name = string_of_axiomName cls
   4.291 +	val cls_id = get_clause_id cls
   4.292 +	val ax_name = get_axiomName cls
   4.293  	val knd = string_of_kind cls
   4.294  	val lits_str = ResLib.list_to_string' lits
   4.295  	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 			 
   4.296  	fun typ_clss k [] = []
   4.297            | typ_clss k (tfree :: tfrees) = 
   4.298 -              (gen_tptp_type_cls(cls_id,knd,tfree,k)) :: typ_clss (k+1) tfrees
   4.299 +              gen_tptp_type_cls(cls_id,ax_name,knd,tfree,k) :: 
   4.300 +              typ_clss (k+1) tfrees
   4.301      in 
   4.302  	cls_str :: (typ_clss 0 tfree_lits)
   4.303      end;
   4.304 @@ -1056,8 +1032,8 @@
   4.305  fun clause2tptp cls =
   4.306      let val (lits,tfree_lits) = tptp_clause_aux cls 
   4.307              (*"lits" includes the typing assumptions (TVars)*)
   4.308 -	val cls_id = string_of_clauseID cls
   4.309 -	val ax_name = string_of_axiomName cls
   4.310 +	val cls_id = get_clause_id cls
   4.311 +	val ax_name = get_axiomName cls
   4.312  	val knd = string_of_kind cls
   4.313  	val lits_str = ResLib.list_to_string' lits
   4.314  	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
   4.315 @@ -1105,12 +1081,10 @@
   4.316  	val knd = string_of_arKind arcls
   4.317  	val all_lits = concl_lit :: prems_lits
   4.318      in
   4.319 -	"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ (ResLib.list_to_string' all_lits) ^ ")."
   4.320 +	"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ 
   4.321 +	(ResLib.list_to_string' all_lits) ^ ")."
   4.322      end;
   4.323  
   4.324 -
   4.325 -val clrelclause_prefix = "relcls_";
   4.326 -
   4.327  fun tptp_classrelLits sub sup = 
   4.328      let val tvar = "(T)"
   4.329      in