Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
authorquigley
Mon May 23 00:18:51 2005 +0200 (2005-05-23)
changeset 16039dfe264950511
parent 16038 b645ff0c697c
child 16040 6e7616eba0b8
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
Changed watcher.ML so that the Unix.execute and Unix.reap functions are used instead of those in modUnix.ML, and
consequently removed modUnix.ML from Reconstruction.thy
src/HOL/Reconstruction.thy
src/HOL/Tools/ATP/modUnix.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Reconstruction.thy	Sun May 22 19:26:18 2005 +0200
     1.2 +++ b/src/HOL/Reconstruction.thy	Mon May 23 00:18:51 2005 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4   	  "Tools/ATP/recon_transfer_proof.ML"
     1.5  	  "Tools/ATP/VampireCommunication.ML"
     1.6  	  "Tools/ATP/SpassCommunication.ML"
     1.7 -	  "Tools/ATP/modUnix.ML"
     1.8 +	 (* "Tools/ATP/modUnix.ML"**)
     1.9  	  "Tools/ATP/watcher.sig"
    1.10  	  "Tools/ATP/watcher.ML"
    1.11  	  "Tools/ATP/res_clasimpset.ML"
     2.1 --- a/src/HOL/Tools/ATP/modUnix.ML	Sun May 22 19:26:18 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/modUnix.ML	Mon May 23 00:18:51 2005 +0200
     2.3 @@ -7,6 +7,10 @@
     2.4  (****** Slightly modified version of sml Unix structure *********)
     2.5  (****************************************************************)
     2.6  
     2.7 +
     2.8 +structure modUnix: MODUNIX =
     2.9 +  struct
    2.10 +
    2.11  type signal = Posix.Signal.signal
    2.12  datatype exit_status = datatype Posix.Process.exit_status
    2.13  
    2.14 @@ -272,3 +276,5 @@
    2.15                outstr = outstr
    2.16              })::procList))
    2.17            end;
    2.18 +
    2.19 +end;
     3.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Sun May 22 19:26:18 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon May 23 00:18:51 2005 +0200
     3.3 @@ -453,6 +453,10 @@
     3.4                                                in 
     3.5                                                    TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
     3.6                                                    TextIO.flushOut toParent;
     3.7 +						TextIO.output (toParent, thmstring^"\n");
     3.8 +                                         	   TextIO.flushOut toParent;
     3.9 +                                         	   TextIO.output (toParent, goalstring^"\n");
    3.10 +                                         	   TextIO.flushOut toParent;
    3.11              					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    3.12                                           	  (* Attempt to prevent several signals from turning up simultaneously *)
    3.13                                           	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
     4.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Sun May 22 19:26:18 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Mon May 23 00:18:51 2005 +0200
     4.3 @@ -1,4 +1,6 @@
     4.4 +
     4.5  (*  ID:         $Id$
     4.6 +
     4.7      Author:     Claire Quigley
     4.8      Copyright   2004  University of Cambridge
     4.9  *)
    4.10 @@ -10,32 +12,56 @@
    4.11  
    4.12  structure ResClasimp : RES_CLASIMP =
    4.13  struct
    4.14 -
    4.15 +fun has_name th = not((Thm.name_of_thm th )= "")
    4.16  fun has_name_pair (a,b) = not_equal a "";
    4.17  
    4.18  fun stick []  = []
    4.19  |   stick (x::xs)  = x@(stick xs )
    4.20  
    4.21 +fun filterlist p [] = []
    4.22 +|   filterlist p (x::xs) = if p x 
    4.23 +                           then 
    4.24 +                               (x::(filterlist p xs))
    4.25 +                           else
    4.26 +                               filterlist p xs
    4.27 +
    4.28 +
    4.29  (* changed, now it also finds out the name of the theorem. *)
    4.30  (* convert a theorem into CNF and then into Clause.clause format. *)
    4.31 -fun clausify_axiom_pairs thm =
    4.32 -    let val thm_name = Thm.name_of_thm thm
    4.33 -	val isa_clauses = ResAxioms.cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
    4.34 -        val isa_clauses' = ResAxioms.rm_Eps [] isa_clauses
    4.35 -        val clauses_n = length isa_clauses
    4.36 -	fun make_axiom_clauses _ [] []= []
    4.37 -	  | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss'
    4.38 -    in
    4.39 -	make_axiom_clauses 0 isa_clauses' isa_clauses		
    4.40 -    end;
    4.41 +
    4.42 +(* outputs a list of (thm,clause) pairs *)
    4.43  
    4.44  
    4.45 -fun clausify_rules_pairs [] err_list = ([],err_list)
    4.46 -  | clausify_rules_pairs (thm::thms) err_list =
    4.47 -    let val (ts,es) = clausify_rules_pairs thms err_list
    4.48 -    in
    4.49 -	((clausify_axiom_pairs thm)::ts,es) handle  _ => (ts,(thm::es))
    4.50 -    end;
    4.51 +(* for tracing: encloses each string element in brackets. *)
    4.52 +fun concat_with_stop [] = ""
    4.53 +  | concat_with_stop [x] =  x
    4.54 +  | concat_with_stop (x::xs) = x^ "." ^ concat_with_stop xs;
    4.55 +
    4.56 +fun remove_symb str = if String.isPrefix  "List.op @." str
    4.57 +                      then 
    4.58 +                          ((String.substring(str,0,5))^(String.extract (str, 10, NONE)))
    4.59 +                      else
    4.60 +                          str
    4.61 +
    4.62 +fun remove_spaces str = let val strlist = String.tokens Char.isSpace str
    4.63 +                            val spaceless = concat strlist
    4.64 +                            val strlist' = String.tokens Char.isPunct spaceless
    4.65 +                        in
    4.66 +                            concat_with_stop strlist'
    4.67 +                        end
    4.68 +
    4.69 +fun remove_symb_pair (str, thm) = let val newstr = remove_symb str
    4.70 +                                  in
    4.71 +                                    (newstr, thm)
    4.72 +                                  end
    4.73 +
    4.74 +
    4.75 +fun remove_spaces_pair (str, thm) = let val newstr = remove_spaces str
    4.76 +                                  in
    4.77 +                                    (newstr, thm)
    4.78 +                                  end
    4.79 +
    4.80 +
    4.81  
    4.82  
    4.83  (*Insert th into the result provided the name is not "".*)
    4.84 @@ -44,12 +70,14 @@
    4.85  
    4.86  fun write_out_clasimp filename = let
    4.87  					val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
    4.88 -					val named_claset = List.foldr add_nonempty []  claset_rules;
    4.89 -					val claset_cls_thms = #1( clausify_rules_pairs named_claset []);
    4.90 +					val named_claset = filterlist has_name_pair claset_rules;
    4.91 +					val claset_names = map remove_spaces_pair (named_claset)
    4.92 +					val claset_cls_thms = #1( ResAxioms.clausify_rules_pairs named_claset []);
    4.93 +
    4.94  
    4.95  					val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
    4.96 -					val named_simpset = map #2(List.filter has_name_pair simpset_rules);
    4.97 -					val simpset_cls_thms = #1 (clausify_rules_pairs named_simpset []);
    4.98 +					val named_simpset = map remove_spaces_pair (filterlist has_name_pair simpset_rules);
    4.99 +					val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
   4.100  
   4.101  					val cls_thms = (claset_cls_thms@simpset_cls_thms);
   4.102  					val cls_thms_list = stick cls_thms;
   4.103 @@ -79,3 +107,4 @@
   4.104  
   4.105  
   4.106  end;
   4.107 +
     5.1 --- a/src/HOL/Tools/ATP/watcher.ML	Sun May 22 19:26:18 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Mon May 23 00:18:51 2005 +0200
     5.3 @@ -25,7 +25,90 @@
     5.4  
     5.5  val goals_being_watched = ref 0;
     5.6  
     5.7 +(*****************************************)
     5.8 +(*  The result of calling createWatcher  *)
     5.9 +(*****************************************)
    5.10  
    5.11 +datatype proc = PROC of {
    5.12 +        pid : Posix.Process.pid,
    5.13 +        instr : TextIO.instream,
    5.14 +        outstr : TextIO.outstream
    5.15 +      };
    5.16 +
    5.17 +(*****************************************)
    5.18 +(*  The result of calling executeToList  *)
    5.19 +(*****************************************)
    5.20 +
    5.21 +datatype cmdproc = CMDPROC of {
    5.22 +        prover: string,             (* Name of the resolution prover used, e.g. Vampire, SPASS *)
    5.23 +        cmd:  string,              (* The file containing the goal for res prover to prove *)     
    5.24 +        thmstring: string,         (* string representation of subgoal after negation, skolemization*) 
    5.25 +        goalstring: string,         (* string representation of subgoal*) 
    5.26 +        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    5.27 +        instr : TextIO.instream,   (*  Input stream to child process *)
    5.28 +        outstr : TextIO.outstream  (*  Output stream from child process *)
    5.29 +      };
    5.30 +
    5.31 +type signal = Posix.Signal.signal
    5.32 +datatype exit_status = datatype Posix.Process.exit_status
    5.33 +
    5.34 +val fromStatus = Posix.Process.fromStatus
    5.35 +
    5.36 +
    5.37 +fun reap(pid, instr, outstr) =
    5.38 +        let
    5.39 +		val u = TextIO.closeIn instr;
    5.40 +	        val u = TextIO.closeOut outstr;
    5.41 +	
    5.42 +		val (_, status) =
    5.43 +			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    5.44 +	in
    5.45 +		status
    5.46 +	end
    5.47 +
    5.48 +fun fdReader (name : string, fd : Posix.IO.file_desc) =
    5.49 +	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    5.50 +
    5.51 +fun fdWriter (name, fd) =
    5.52 +          Posix.IO.mkTextWriter {
    5.53 +	      appendMode = false,
    5.54 +              initBlkMode = true,
    5.55 +              name = name,  
    5.56 +              chunkSize=4096,
    5.57 +              fd = fd
    5.58 +            };
    5.59 +
    5.60 +fun openOutFD (name, fd) =
    5.61 +	  TextIO.mkOutstream (
    5.62 +	    TextIO.StreamIO.mkOutstream (
    5.63 +	      fdWriter (name, fd), IO.BLOCK_BUF));
    5.64 +
    5.65 +fun openInFD (name, fd) =
    5.66 +	  TextIO.mkInstream (
    5.67 +	    TextIO.StreamIO.mkInstream (
    5.68 +	      fdReader (name, fd), ""));
    5.69 +
    5.70 +
    5.71 +
    5.72 +
    5.73 +
    5.74 +fun killChild child_handle = Unix.reap child_handle 
    5.75 +
    5.76 +fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
    5.77 +
    5.78 +fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
    5.79 +
    5.80 +fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
    5.81 +
    5.82 +fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = (prover,(cmd, (instr,outstr)));
    5.83 +
    5.84 +fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = proc_handle;
    5.85 +
    5.86 +fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (prover);
    5.87 +
    5.88 +fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (thmstring);
    5.89 +
    5.90 +fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (goalstring);
    5.91  
    5.92  fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
    5.93  
    5.94 @@ -92,7 +175,7 @@
    5.95                                                           val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    5.96                                                           (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    5.97                                                           (*** hyps/local axioms just now                                                ***)
    5.98 -                                                         val whole_prob_file = Unix.execute("/bin/cat", [(*clasimpfile,axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
    5.99 +                                                         val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
   5.100                                                           val dfg_create =if File.exists dfg_dir 
   5.101                                                                           then
   5.102                                                                               ((warning("dfg dir exists"));())
   5.103 @@ -100,8 +183,7 @@
   5.104                                                                                 File.mkdir dfg_dir; 
   5.105                                                           
   5.106                                                           val dfg_path = File.sysify_path dfg_dir;
   5.107 -                                                         val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X",
   5.108 -                                                                                       ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
   5.109 +                                                         val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X",   ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
   5.110                                                         (*val _ = Posix.Process.wait ()*)
   5.111                                                         (*val _ =Unix.reap exec_tptp2x*)
   5.112                                                           val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
   5.113 @@ -289,7 +371,7 @@
   5.114                        val _ = TextIO.output (outfile,goalstr )
   5.115                        val _ =  TextIO.closeOut outfile*)
   5.116                        fun killChildren [] = ()
   5.117 -                   |      killChildren  (childPid::children) = (killChild childPid; killChildren children)
   5.118 +                   |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
   5.119  
   5.120                       
   5.121             
   5.122 @@ -356,7 +438,7 @@
   5.123                                                                (*********************************)
   5.124                      |   checkChildren ((childProc::otherChildren), toParentStr) = 
   5.125                                              let val (childInput,childOutput) =  cmdstreamsOf childProc
   5.126 -                                                val childPid = cmdchildPid childProc
   5.127 +                                                val child_handle= cmdchildHandle childProc
   5.128                                                  (* childCmd is the .dfg file that the problem is in *)
   5.129                                                  val childCmd = fst(snd (cmdchildInfo childProc))
   5.130                                                  (* now get the number of the subgoal from the filename *)
   5.131 @@ -392,7 +474,7 @@
   5.132                                                         (**********************************************)
   5.133                                                         (* Remove this child and go on to check others*)
   5.134                                                         (**********************************************)
   5.135 -                                                       ( reap(childPid, childInput, childOutput);
   5.136 +                                                       ( Unix.reap child_handle;
   5.137                                                           checkChildren(otherChildren, toParentStr))
   5.138                                                      else 
   5.139                                                         (**********************************************)
   5.140 @@ -418,35 +500,58 @@
   5.141                  (* takes list of (string, string, string list, string)list proclist *)
   5.142                  (********************************************************************)
   5.143  
   5.144 -           (*** add subgoal id num to this *)
   5.145 +
   5.146 +  (*** add subgoal id num to this *)
   5.147                     fun execCmds  [] procList = procList
   5.148                     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
   5.149                                                       if (prover = "spass") 
   5.150                                                       then 
   5.151 -                                                         let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@["-FullRed=0"]@settings@[file]), procList)
   5.152 +                                                         let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   5.153 + 						             val (instr, outstr)=Unix.streamsOf childhandle
   5.154 +                                                             val newProcList =    (((CMDPROC{
   5.155 +            									  prover = prover,
   5.156 +   										  cmd = file,
   5.157 +  									          thmstring = thmstring,
   5.158 +  									          goalstring = goalstring,
   5.159 + 										  proc_handle = childhandle,
   5.160 +									          instr = instr,
   5.161 +   									          outstr = outstr })::procList))
   5.162 +  	                                                      val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child")));  
   5.163 +                                                val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file )
   5.164 +                                                val _ =  TextIO.closeOut outfile
   5.165                                                           in
   5.166                                                              execCmds cmds newProcList
   5.167                                                           end
   5.168                                                       else 
   5.169 -                                                         let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@settings@[file]), procList)
   5.170 +                                                         let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   5.171 + 						             val (instr, outstr)=Unix.streamsOf childhandle
   5.172 +							     val newProcList =    (((CMDPROC{
   5.173 +            									  prover = prover,
   5.174 +   										  cmd = file,
   5.175 +  									          thmstring = thmstring,
   5.176 +  									          goalstring = goalstring,
   5.177 + 										  proc_handle = childhandle,
   5.178 +									          instr = instr,
   5.179 +   									          outstr = outstr })::procList))
   5.180                                                           in
   5.181                                                              execCmds cmds newProcList
   5.182                                                           end
   5.183  
   5.184  
   5.185 +
   5.186                  (****************************************)                  
   5.187                  (* call resolution processes remotely   *)
   5.188                  (* settings should be a list of strings *)
   5.189                  (* e.g. ["-t 300", "-m 100000"]         *)
   5.190                  (****************************************)
   5.191    
   5.192 -                   fun execRemoteCmds  [] procList = procList
   5.193 +                 (*  fun execRemoteCmds  [] procList = procList
   5.194                     |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   5.195                                               let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   5.196                                                   in
   5.197                                                        execRemoteCmds  cmds newProcList
   5.198                                                   end
   5.199 -
   5.200 +*)
   5.201  
   5.202                     fun printList (outStr, []) = ()
   5.203                     |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   5.204 @@ -463,9 +568,9 @@
   5.205                            let    fun loop (procList) =  
   5.206                                   (
   5.207                                   let val cmdsFromIsa = pollParentInput ()
   5.208 -                                      fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
   5.209 +                                     fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
   5.210                                                    TextIO.flushOut toParentStr;
   5.211 -                                                   killChildren (map (cmdchildPid) procList);
   5.212 +                                                   killChildren (map (cmdchildHandle) procList);
   5.213                                                      ())
   5.214                                       
   5.215                                   in 
   5.216 @@ -476,11 +581,12 @@
   5.217                                            if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   5.218                                            then 
   5.219                                              (
   5.220 -                                              let val childPids = map cmdchildPid procList 
   5.221 +                                              let val child_handles = map cmdchildHandle procList 
   5.222                                                in
   5.223 -                                                 killChildren childPids;
   5.224 -                                                 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                       loop ([])
   5.225 +                                                 killChildren child_handles;
   5.226 +                                                 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                                              loop ([])
   5.227                                                end
   5.228 +                                                 
   5.229                                               )
   5.230                                            else
   5.231                                              ( 
   5.232 @@ -496,11 +602,12 @@
   5.233                                                      loop (newProcList') 
   5.234                                                    end
   5.235                                                    )
   5.236 -                                              else                         (************************)
   5.237 -                                                                           (* Execute remotely     *)
   5.238 -                                                  (                        (************************)
   5.239 +                                              else                         (*********************************)
   5.240 +                                                                           (* Execute remotely              *)
   5.241 + 									   (* (actually not remote for now )*)
   5.242 +                                                  (                        (*********************************)
   5.243                                                    let 
   5.244 -                                                    val newProcList = execRemoteCmds (valOf cmdsFromIsa) procList
   5.245 +                                                    val newProcList = execCmds (valOf cmdsFromIsa) procList
   5.246                                                      val parentID = Posix.ProcEnv.getppid()
   5.247                                                      val newProcList' =checkChildren (newProcList, toParentStr) 
   5.248                                                    in
   5.249 @@ -594,7 +701,19 @@
   5.250  (**********************************************************)
   5.251  (* Start a watcher and set up signal handlers             *)
   5.252  (**********************************************************)
   5.253 -fun killWatcher pid= killChild pid;
   5.254 +
   5.255 +fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   5.256 +
   5.257 +fun reapWatcher(pid, instr, outstr) =
   5.258 +        let
   5.259 +		val u = TextIO.closeIn instr;
   5.260 +	        val u = TextIO.closeOut outstr;
   5.261 +	
   5.262 +		val (_, status) =
   5.263 +			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
   5.264 +	in
   5.265 +		status
   5.266 +	end
   5.267  
   5.268  fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   5.269  			   val streams =snd mychild
   5.270 @@ -636,7 +755,7 @@
   5.271                                                                           val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   5.272                                                                           val _ =  TextIO.closeOut outfile
   5.273                                                                       in
   5.274 -                                                                         reap (childpid,childin, childout); ()
   5.275 +                                                                         reapWatcher (childpid,childin, childout); ()
   5.276                                                                       end)
   5.277                                                                   else
   5.278                                                                      ()
   5.279 @@ -655,7 +774,7 @@
   5.280                                                                                 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   5.281                                                                                 val _ =  TextIO.closeOut outfile
   5.282                                                                             in
   5.283 -                                                                              reap (childpid,childin, childout); ()
   5.284 +                                                                              reapWatcher (childpid,childin, childout); ()
   5.285                                                                             end )
   5.286                                                                        else
   5.287                                                                           ()
   5.288 @@ -674,7 +793,7 @@
   5.289                                                                                 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   5.290                                                                                 val _ =  TextIO.closeOut outfile
   5.291                                                                             in
   5.292 -                                                                              reap (childpid,childin, childout); ()
   5.293 +                                                                              reapWatcher (childpid,childin, childout); ()
   5.294                                                                             end )
   5.295                                                                        else
   5.296                                                                           ()
     6.1 --- a/src/HOL/Tools/res_atp.ML	Sun May 22 19:26:18 2005 +0200
     6.2 +++ b/src/HOL/Tools/res_atp.ML	Mon May 23 00:18:51 2005 +0200
     6.3 @@ -185,14 +185,14 @@
     6.4                             (* without paramodulation *)
     6.5                             (warning ("goalstring in call_res_tac is: "^goalstring));
     6.6                             (warning ("prob file in cal_res_tac is: "^probfile));
     6.7 -                                                       Watcher.callResProvers(childout,
     6.8 -                            [("spass",thmstr,goalstring,spass_home,  
     6.9 +                                                      (* Watcher.callResProvers(childout,
    6.10 +                            [("spass",thmstr,goalstring,(*spass_home*),  
    6.11                               "-DocProof", 
    6.12 -                             clasimpfile, axfile, hypsfile, probfile)]);
    6.13 +                             clasimpfile, axfile, hypsfile, probfile)]);*)
    6.14  
    6.15                              Watcher.callResProvers(childout,
    6.16 -                            [("spass",thmstr,goalstring,spass_home,  
    6.17 -                             "-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
    6.18 +                            [("spass",thmstr,goalstring(*,spass_home*),"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/spassshell",  
    6.19 +                             "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
    6.20                               clasimpfile, axfile, hypsfile, probfile)]);
    6.21  
    6.22                             (* with paramodulation *)
    6.23 @@ -302,6 +302,7 @@
    6.24          val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  
    6.25  
    6.26          (* cq: add write out clasimps to file *)
    6.27 +
    6.28          (* cq:create watcher and pass to isar_atp_aux *)
    6.29          (* tracing *) 
    6.30          (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
    6.31 @@ -373,8 +374,8 @@
    6.32  (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
    6.33  (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
    6.34  (*claset file and prob file*)
    6.35 -(* FIX*)
    6.36 -fun isar_local_thms (delta_cs, delta_ss_thms) =
    6.37 +(* FIX: update to work with clausify_axiom_pairs now in ResAxioms*)
    6.38 +(*fun isar_local_thms (delta_cs, delta_ss_thms) =
    6.39      let val thms_cs = get_thms_cs delta_cs
    6.40  	val thms_ss = get_thms_ss delta_ss_thms
    6.41  	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
    6.42 @@ -384,7 +385,7 @@
    6.43      in
    6.44  	(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
    6.45      end;
    6.46 -
    6.47 +*)
    6.48  
    6.49  
    6.50  
    6.51 @@ -404,7 +405,7 @@
    6.52            (warning ("initial thm in isar_atp: "^thmstring));
    6.53            (warning ("subgoals in isar_atp: "^prems_string));
    6.54      	  (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
    6.55 -          (isar_local_thms (d_cs,d_ss_thms); (warning("about to call isar_atp'"));
    6.56 +          ((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'"));
    6.57             isar_atp' (prems, thm))
    6.58      end;
    6.59  
     7.1 --- a/src/HOL/Tools/res_axioms.ML	Sun May 22 19:26:18 2005 +0200
     7.2 +++ b/src/HOL/Tools/res_axioms.ML	Mon May 23 00:18:51 2005 +0200
     7.3 @@ -11,19 +11,18 @@
     7.4    val elimRule_tac : thm -> Tactical.tactic
     7.5    val elimR2Fol : thm -> term
     7.6    val transform_elim : thm -> thm
     7.7 -  
     7.8 -  val clausify_axiom : thm -> ResClause.clause list
     7.9 +  val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list
    7.10    val cnf_axiom : (string * thm) -> thm list
    7.11    val meta_cnf_axiom : thm -> thm list
    7.12    val cnf_rule : thm -> thm list
    7.13    val cnf_classical_rules_thy : theory -> thm list list * thm list
    7.14 -  val clausify_classical_rules_thy : theory -> ResClause.clause list list * thm list
    7.15 + 
    7.16    val cnf_simpset_rules_thy : theory -> thm list list * thm list
    7.17 -  val clausify_simpset_rules_thy : theory -> ResClause.clause list list * thm list
    7.18 + 
    7.19    val rm_Eps : (term * term) list -> thm list -> term list
    7.20    val claset_rules_of_thy : theory -> (string * thm) list
    7.21    val simpset_rules_of_thy : theory -> (string * thm) list
    7.22 -  val clausify_rules : thm list -> thm list -> ResClause.clause list list * thm list
    7.23 +  val clausify_rules_pairs : (string * thm) list -> thm list -> (ResClause.clause * thm) list list * thm list
    7.24    val setup : (theory -> theory) list
    7.25    end;
    7.26  
    7.27 @@ -136,9 +135,13 @@
    7.28      let val tm = elimR2Fol th
    7.29  	val ctm = cterm_of (sign_of_thm th) tm	
    7.30      in
    7.31 +
    7.32  	prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th])
    7.33      end
    7.34 -  else th;
    7.35 + else th;;	
    7.36 +
    7.37 +
    7.38 +
    7.39  
    7.40  
    7.41  (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
    7.42 @@ -355,20 +358,6 @@
    7.43        in th' :: (rm_Eps epss' thms) end;
    7.44  
    7.45  
    7.46 -(* convert a theorem into CNF and then into Clause.clause format. *)
    7.47 -fun clausify_axiom th =
    7.48 -    let val name = Thm.name_of_thm th
    7.49 -	val isa_clauses = cnf_axiom (name, th)
    7.50 -	      (*"isa_clauses" are already in "standard" form. *)
    7.51 -        val isa_clauses' = rm_Eps [] isa_clauses
    7.52 -        val clauses_n = length isa_clauses
    7.53 -	fun make_axiom_clauses _ [] = []
    7.54 -	  | make_axiom_clauses i (cls::clss) = 
    7.55 -	      (ResClause.make_axiom_clause cls (name,i)) :: make_axiom_clauses (i+1) clss 
    7.56 -    in
    7.57 -	make_axiom_clauses 0 isa_clauses'		
    7.58 -    end;
    7.59 -  
    7.60  
    7.61  (**** Extract and Clausify theorems from a theory's claset and simpset ****)
    7.62  
    7.63 @@ -408,21 +397,26 @@
    7.64  
    7.65  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
    7.66  
    7.67 -(* classical rules *)
    7.68 -fun clausify_rules [] err_list = ([],err_list)
    7.69 -  | clausify_rules (th::thms) err_list =
    7.70 -    let val (ts,es) = clausify_rules thms err_list
    7.71 +(* outputs a list of (thm,clause) pairs *)
    7.72 +fun clausify_axiom_pairs (thm_name,thm) =
    7.73 +    let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
    7.74 +        val isa_clauses' = rm_Eps [] isa_clauses
    7.75 +        val clauses_n = length isa_clauses
    7.76 +	fun make_axiom_clauses _ [] []= []
    7.77 +	  | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss'
    7.78      in
    7.79 -	((clausify_axiom th)::ts,es) handle  _ => (ts,(th::es))
    7.80 +	make_axiom_clauses 0 isa_clauses' isa_clauses		
    7.81      end;
    7.82  
    7.83 -(* convert all classical rules from a given theory into Clause.clause format. *)
    7.84 -fun clausify_classical_rules_thy thy =
    7.85 -    clausify_rules (map #2 (claset_rules_of_thy thy)) [];
    7.86  
    7.87 -(* convert all simplifier rules from a given theory into Clause.clause format. *)
    7.88 -fun clausify_simpset_rules_thy thy =
    7.89 -    clausify_rules (map #2 (simpset_rules_of_thy thy)) [];
    7.90 +fun clausify_rules_pairs [] err_list = ([],err_list)
    7.91 +  | clausify_rules_pairs ((name,thm)::thms) err_list =
    7.92 +    let val (ts,es) = clausify_rules_pairs thms err_list
    7.93 +    in
    7.94 +	((clausify_axiom_pairs (name,thm))::ts,es) handle  _ => (ts,(thm::es))
    7.95 +    end;
    7.96 +(* classical rules *)
    7.97 +
    7.98  
    7.99  (*Setup function: takes a theory and installs ALL simprules and claset rules 
   7.100    into the clause cache*)
     8.1 --- a/src/HOL/Tools/res_clause.ML	Sun May 22 19:26:18 2005 +0200
     8.2 +++ b/src/HOL/Tools/res_clause.ML	Mon May 23 00:18:51 2005 +0200
     8.3 @@ -30,6 +30,7 @@
     8.4      val tptp_arity_clause : arityClause -> string
     8.5      val tptp_classrelClause : classrelClause -> string
     8.6      val tptp_clause : clause -> string list
     8.7 +    val clause_info : clause ->  string * string
     8.8      val tptp_clauses2str : string list -> string
     8.9      val typed : unit -> unit
    8.10      val untyped : unit -> unit
    8.11 @@ -643,6 +644,14 @@
    8.12  	cls_str :: (typ_clss 0 tfree_lits)
    8.13      end;
    8.14  
    8.15 +fun clause_info cls =
    8.16 +    let 
    8.17 +	val cls_id = string_of_clauseID cls
    8.18 +	val ax_name = string_of_axiomName cls
    8.19 +    in 
    8.20 +	((ax_name^""), cls_id)
    8.21 +    end;
    8.22 +
    8.23  
    8.24  fun clause2tptp cls =
    8.25      let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)