# HG changeset patch # User quigley # Date 1116800331 -7200 # Node ID dfe26495051168ad2c21e74003ecd8dd30b5b700 # Parent b645ff0c697c95d9c56331b723aeeebc4c8d864b 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 diff -r b645ff0c697c -r dfe264950511 src/HOL/Reconstruction.thy --- a/src/HOL/Reconstruction.thy Sun May 22 19:26:18 2005 +0200 +++ b/src/HOL/Reconstruction.thy Mon May 23 00:18:51 2005 +0200 @@ -21,7 +21,7 @@ "Tools/ATP/recon_transfer_proof.ML" "Tools/ATP/VampireCommunication.ML" "Tools/ATP/SpassCommunication.ML" - "Tools/ATP/modUnix.ML" + (* "Tools/ATP/modUnix.ML"**) "Tools/ATP/watcher.sig" "Tools/ATP/watcher.ML" "Tools/ATP/res_clasimpset.ML" diff -r b645ff0c697c -r dfe264950511 src/HOL/Tools/ATP/modUnix.ML --- a/src/HOL/Tools/ATP/modUnix.ML Sun May 22 19:26:18 2005 +0200 +++ b/src/HOL/Tools/ATP/modUnix.ML Mon May 23 00:18:51 2005 +0200 @@ -7,6 +7,10 @@ (****** Slightly modified version of sml Unix structure *********) (****************************************************************) + +structure modUnix: MODUNIX = + struct + type signal = Posix.Signal.signal datatype exit_status = datatype Posix.Process.exit_status @@ -272,3 +276,5 @@ outstr = outstr })::procList)) end; + +end; diff -r b645ff0c697c -r dfe264950511 src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Sun May 22 19:26:18 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Mon May 23 00:18:51 2005 +0200 @@ -453,6 +453,10 @@ in TextIO.output (toParent,"Proof found but translation failed!" ^"\n"); TextIO.flushOut toParent; + TextIO.output (toParent, thmstring^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, goalstring^"\n"); + TextIO.flushOut toParent; Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); (* Attempt to prevent several signals from turning up simultaneously *) Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac diff -r b645ff0c697c -r dfe264950511 src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Sun May 22 19:26:18 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Mon May 23 00:18:51 2005 +0200 @@ -1,4 +1,6 @@ + (* ID: $Id$ + Author: Claire Quigley Copyright 2004 University of Cambridge *) @@ -10,32 +12,56 @@ structure ResClasimp : RES_CLASIMP = struct - +fun has_name th = not((Thm.name_of_thm th )= "") fun has_name_pair (a,b) = not_equal a ""; fun stick [] = [] | stick (x::xs) = x@(stick xs ) +fun filterlist p [] = [] +| filterlist p (x::xs) = if p x + then + (x::(filterlist p xs)) + else + filterlist p xs + + (* changed, now it also finds out the name of the theorem. *) (* convert a theorem into CNF and then into Clause.clause format. *) -fun clausify_axiom_pairs thm = - let val thm_name = Thm.name_of_thm thm - val isa_clauses = ResAxioms.cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *) - val isa_clauses' = ResAxioms.rm_Eps [] isa_clauses - val clauses_n = length isa_clauses - fun make_axiom_clauses _ [] []= [] - | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss' - in - make_axiom_clauses 0 isa_clauses' isa_clauses - end; + +(* outputs a list of (thm,clause) pairs *) -fun clausify_rules_pairs [] err_list = ([],err_list) - | clausify_rules_pairs (thm::thms) err_list = - let val (ts,es) = clausify_rules_pairs thms err_list - in - ((clausify_axiom_pairs thm)::ts,es) handle _ => (ts,(thm::es)) - end; +(* for tracing: encloses each string element in brackets. *) +fun concat_with_stop [] = "" + | concat_with_stop [x] = x + | concat_with_stop (x::xs) = x^ "." ^ concat_with_stop xs; + +fun remove_symb str = if String.isPrefix "List.op @." str + then + ((String.substring(str,0,5))^(String.extract (str, 10, NONE))) + else + str + +fun remove_spaces str = let val strlist = String.tokens Char.isSpace str + val spaceless = concat strlist + val strlist' = String.tokens Char.isPunct spaceless + in + concat_with_stop strlist' + end + +fun remove_symb_pair (str, thm) = let val newstr = remove_symb str + in + (newstr, thm) + end + + +fun remove_spaces_pair (str, thm) = let val newstr = remove_spaces str + in + (newstr, thm) + end + + (*Insert th into the result provided the name is not "".*) @@ -44,12 +70,14 @@ fun write_out_clasimp filename = let val claset_rules = ResAxioms.claset_rules_of_thy (the_context()); - val named_claset = List.foldr add_nonempty [] claset_rules; - val claset_cls_thms = #1( clausify_rules_pairs named_claset []); + val named_claset = filterlist has_name_pair claset_rules; + val claset_names = map remove_spaces_pair (named_claset) + val claset_cls_thms = #1( ResAxioms.clausify_rules_pairs named_claset []); + val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context()); - val named_simpset = map #2(List.filter has_name_pair simpset_rules); - val simpset_cls_thms = #1 (clausify_rules_pairs named_simpset []); + val named_simpset = map remove_spaces_pair (filterlist has_name_pair simpset_rules); + val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []); val cls_thms = (claset_cls_thms@simpset_cls_thms); val cls_thms_list = stick cls_thms; @@ -79,3 +107,4 @@ end; + diff -r b645ff0c697c -r dfe264950511 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Sun May 22 19:26:18 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Mon May 23 00:18:51 2005 +0200 @@ -25,7 +25,90 @@ val goals_being_watched = ref 0; +(*****************************************) +(* The result of calling createWatcher *) +(*****************************************) +datatype proc = PROC of { + pid : Posix.Process.pid, + instr : TextIO.instream, + outstr : TextIO.outstream + }; + +(*****************************************) +(* The result of calling executeToList *) +(*****************************************) + +datatype cmdproc = CMDPROC of { + prover: string, (* Name of the resolution prover used, e.g. Vampire, SPASS *) + cmd: string, (* The file containing the goal for res prover to prove *) + thmstring: string, (* string representation of subgoal after negation, skolemization*) + goalstring: string, (* string representation of subgoal*) + proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc, + instr : TextIO.instream, (* Input stream to child process *) + outstr : TextIO.outstream (* Output stream from child process *) + }; + +type signal = Posix.Signal.signal +datatype exit_status = datatype Posix.Process.exit_status + +val fromStatus = Posix.Process.fromStatus + + +fun reap(pid, instr, outstr) = + let + val u = TextIO.closeIn instr; + val u = TextIO.closeOut outstr; + + val (_, status) = + Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) + in + status + end + +fun fdReader (name : string, fd : Posix.IO.file_desc) = + Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd }; + +fun fdWriter (name, fd) = + Posix.IO.mkTextWriter { + appendMode = false, + initBlkMode = true, + name = name, + chunkSize=4096, + fd = fd + }; + +fun openOutFD (name, fd) = + TextIO.mkOutstream ( + TextIO.StreamIO.mkOutstream ( + fdWriter (name, fd), IO.BLOCK_BUF)); + +fun openInFD (name, fd) = + TextIO.mkInstream ( + TextIO.StreamIO.mkInstream ( + fdReader (name, fd), "")); + + + + + +fun killChild child_handle = Unix.reap child_handle + +fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr)); + +fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr); + +fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr); + +fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = (prover,(cmd, (instr,outstr))); + +fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = proc_handle; + +fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = (prover); + +fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = (thmstring); + +fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr}) = (goalstring); fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr); @@ -92,7 +175,7 @@ val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID)) (*** only include problem and clasimp for the moment, not sure how to refer to ***) (*** hyps/local axioms just now ***) - val whole_prob_file = Unix.execute("/bin/cat", [(*clasimpfile,axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)]) + val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)]) val dfg_create =if File.exists dfg_dir then ((warning("dfg dir exists"));()) @@ -100,8 +183,7 @@ File.mkdir dfg_dir; val dfg_path = File.sysify_path dfg_dir; - val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X", - ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path]) + val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X", ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path]) (*val _ = Posix.Process.wait ()*) (*val _ =Unix.reap exec_tptp2x*) val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg" @@ -289,7 +371,7 @@ val _ = TextIO.output (outfile,goalstr ) val _ = TextIO.closeOut outfile*) fun killChildren [] = () - | killChildren (childPid::children) = (killChild childPid; killChildren children) + | killChildren (child_handle::children) = (killChild child_handle; killChildren children) @@ -356,7 +438,7 @@ (*********************************) | checkChildren ((childProc::otherChildren), toParentStr) = let val (childInput,childOutput) = cmdstreamsOf childProc - val childPid = cmdchildPid childProc + val child_handle= cmdchildHandle childProc (* childCmd is the .dfg file that the problem is in *) val childCmd = fst(snd (cmdchildInfo childProc)) (* now get the number of the subgoal from the filename *) @@ -392,7 +474,7 @@ (**********************************************) (* Remove this child and go on to check others*) (**********************************************) - ( reap(childPid, childInput, childOutput); + ( Unix.reap child_handle; checkChildren(otherChildren, toParentStr)) else (**********************************************) @@ -418,35 +500,58 @@ (* takes list of (string, string, string list, string)list proclist *) (********************************************************************) - (*** add subgoal id num to this *) + + (*** add subgoal id num to this *) fun execCmds [] procList = procList | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = if (prover = "spass") then - let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@["-FullRed=0"]@settings@[file]), procList) + let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) + val (instr, outstr)=Unix.streamsOf childhandle + val newProcList = (((CMDPROC{ + prover = prover, + cmd = file, + thmstring = thmstring, + goalstring = goalstring, + proc_handle = childhandle, + instr = instr, + outstr = outstr })::procList)) + val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child"))); + val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file ) + val _ = TextIO.closeOut outfile in execCmds cmds newProcList end else - let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@settings@[file]), procList) + let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) + val (instr, outstr)=Unix.streamsOf childhandle + val newProcList = (((CMDPROC{ + prover = prover, + cmd = file, + thmstring = thmstring, + goalstring = goalstring, + proc_handle = childhandle, + instr = instr, + outstr = outstr })::procList)) in execCmds cmds newProcList end + (****************************************) (* call resolution processes remotely *) (* settings should be a list of strings *) (* e.g. ["-t 300", "-m 100000"] *) (****************************************) - fun execRemoteCmds [] procList = procList + (* fun execRemoteCmds [] procList = procList | execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList = let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList) in execRemoteCmds cmds newProcList end - +*) fun printList (outStr, []) = () | printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs)) @@ -463,9 +568,9 @@ let fun loop (procList) = ( let val cmdsFromIsa = pollParentInput () - fun killchildHandler (n:int) = (TextIO.output(toParentStr, "Killing child proof processes!\n"); + fun killchildHandler (n:int) = (TextIO.output(toParentStr, "Killing child proof processes!\n"); TextIO.flushOut toParentStr; - killChildren (map (cmdchildPid) procList); + killChildren (map (cmdchildHandle) procList); ()) in @@ -476,11 +581,12 @@ if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" ) then ( - let val childPids = map cmdchildPid procList + let val child_handles = map cmdchildHandle procList in - killChildren childPids; - (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) loop ([]) + killChildren child_handles; + (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) loop ([]) end + ) else ( @@ -496,11 +602,12 @@ loop (newProcList') end ) - else (************************) - (* Execute remotely *) - ( (************************) + else (*********************************) + (* Execute remotely *) + (* (actually not remote for now )*) + ( (*********************************) let - val newProcList = execRemoteCmds (valOf cmdsFromIsa) procList + val newProcList = execCmds (valOf cmdsFromIsa) procList val parentID = Posix.ProcEnv.getppid() val newProcList' =checkChildren (newProcList, toParentStr) in @@ -594,7 +701,19 @@ (**********************************************************) (* Start a watcher and set up signal handlers *) (**********************************************************) -fun killWatcher pid= killChild pid; + +fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill); + +fun reapWatcher(pid, instr, outstr) = + let + val u = TextIO.closeIn instr; + val u = TextIO.closeOut outstr; + + val (_, status) = + Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) + in + status + end fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr, num_of_clauses)) val streams =snd mychild @@ -636,7 +755,7 @@ val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) val _ = TextIO.closeOut outfile in - reap (childpid,childin, childout); () + reapWatcher (childpid,childin, childout); () end) else () @@ -655,7 +774,7 @@ val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) val _ = TextIO.closeOut outfile in - reap (childpid,childin, childout); () + reapWatcher (childpid,childin, childout); () end ) else () @@ -674,7 +793,7 @@ val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) val _ = TextIO.closeOut outfile in - reap (childpid,childin, childout); () + reapWatcher (childpid,childin, childout); () end ) else () diff -r b645ff0c697c -r dfe264950511 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Sun May 22 19:26:18 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Mon May 23 00:18:51 2005 +0200 @@ -185,14 +185,14 @@ (* without paramodulation *) (warning ("goalstring in call_res_tac is: "^goalstring)); (warning ("prob file in cal_res_tac is: "^probfile)); - Watcher.callResProvers(childout, - [("spass",thmstr,goalstring,spass_home, + (* Watcher.callResProvers(childout, + [("spass",thmstr,goalstring,(*spass_home*), "-DocProof", - clasimpfile, axfile, hypsfile, probfile)]); + clasimpfile, axfile, hypsfile, probfile)]);*) Watcher.callResProvers(childout, - [("spass",thmstr,goalstring,spass_home, - "-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", + [("spass",thmstr,goalstring(*,spass_home*),"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/spassshell", + "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", clasimpfile, axfile, hypsfile, probfile)]); (* with paramodulation *) @@ -302,6 +302,7 @@ val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) ) (* cq: add write out clasimps to file *) + (* cq:create watcher and pass to isar_atp_aux *) (* tracing *) (*val tenth_ax = fst( Array.sub(clause_arr, 1)) @@ -373,8 +374,8 @@ (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *) (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *) (*claset file and prob file*) -(* FIX*) -fun isar_local_thms (delta_cs, delta_ss_thms) = +(* FIX: update to work with clausify_axiom_pairs now in ResAxioms*) +(*fun isar_local_thms (delta_cs, delta_ss_thms) = let val thms_cs = get_thms_cs delta_cs val thms_ss = get_thms_ss delta_ss_thms val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss)) @@ -384,7 +385,7 @@ in (ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out) end; - +*) @@ -404,7 +405,7 @@ (warning ("initial thm in isar_atp: "^thmstring)); (warning ("subgoals in isar_atp: "^prems_string)); (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no))); - (isar_local_thms (d_cs,d_ss_thms); (warning("about to call isar_atp'")); + ((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'")); isar_atp' (prems, thm)) end; diff -r b645ff0c697c -r dfe264950511 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Sun May 22 19:26:18 2005 +0200 +++ b/src/HOL/Tools/res_axioms.ML Mon May 23 00:18:51 2005 +0200 @@ -11,19 +11,18 @@ val elimRule_tac : thm -> Tactical.tactic val elimR2Fol : thm -> term val transform_elim : thm -> thm - - val clausify_axiom : thm -> ResClause.clause list + val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list val cnf_axiom : (string * thm) -> thm list val meta_cnf_axiom : thm -> thm list val cnf_rule : thm -> thm list val cnf_classical_rules_thy : theory -> thm list list * thm list - val clausify_classical_rules_thy : theory -> ResClause.clause list list * thm list + val cnf_simpset_rules_thy : theory -> thm list list * thm list - val clausify_simpset_rules_thy : theory -> ResClause.clause list list * thm list + val rm_Eps : (term * term) list -> thm list -> term list val claset_rules_of_thy : theory -> (string * thm) list val simpset_rules_of_thy : theory -> (string * thm) list - val clausify_rules : thm list -> thm list -> ResClause.clause list list * thm list + val clausify_rules_pairs : (string * thm) list -> thm list -> (ResClause.clause * thm) list list * thm list val setup : (theory -> theory) list end; @@ -136,9 +135,13 @@ let val tm = elimR2Fol th val ctm = cterm_of (sign_of_thm th) tm in + prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th]) end - else th; + else th;; + + + (**** Transformation of Clasets and Simpsets into First-Order Axioms ****) @@ -355,20 +358,6 @@ in th' :: (rm_Eps epss' thms) end; -(* convert a theorem into CNF and then into Clause.clause format. *) -fun clausify_axiom th = - let val name = Thm.name_of_thm th - val isa_clauses = cnf_axiom (name, th) - (*"isa_clauses" are already in "standard" form. *) - val isa_clauses' = rm_Eps [] isa_clauses - val clauses_n = length isa_clauses - fun make_axiom_clauses _ [] = [] - | make_axiom_clauses i (cls::clss) = - (ResClause.make_axiom_clause cls (name,i)) :: make_axiom_clauses (i+1) clss - in - make_axiom_clauses 0 isa_clauses' - end; - (**** Extract and Clausify theorems from a theory's claset and simpset ****) @@ -408,21 +397,26 @@ (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****) -(* classical rules *) -fun clausify_rules [] err_list = ([],err_list) - | clausify_rules (th::thms) err_list = - let val (ts,es) = clausify_rules thms err_list +(* outputs a list of (thm,clause) pairs *) +fun clausify_axiom_pairs (thm_name,thm) = + let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *) + val isa_clauses' = rm_Eps [] isa_clauses + val clauses_n = length isa_clauses + fun make_axiom_clauses _ [] []= [] + | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss' in - ((clausify_axiom th)::ts,es) handle _ => (ts,(th::es)) + make_axiom_clauses 0 isa_clauses' isa_clauses end; -(* convert all classical rules from a given theory into Clause.clause format. *) -fun clausify_classical_rules_thy thy = - clausify_rules (map #2 (claset_rules_of_thy thy)) []; -(* convert all simplifier rules from a given theory into Clause.clause format. *) -fun clausify_simpset_rules_thy thy = - clausify_rules (map #2 (simpset_rules_of_thy thy)) []; +fun clausify_rules_pairs [] err_list = ([],err_list) + | clausify_rules_pairs ((name,thm)::thms) err_list = + let val (ts,es) = clausify_rules_pairs thms err_list + in + ((clausify_axiom_pairs (name,thm))::ts,es) handle _ => (ts,(thm::es)) + end; +(* classical rules *) + (*Setup function: takes a theory and installs ALL simprules and claset rules into the clause cache*) diff -r b645ff0c697c -r dfe264950511 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Sun May 22 19:26:18 2005 +0200 +++ b/src/HOL/Tools/res_clause.ML Mon May 23 00:18:51 2005 +0200 @@ -30,6 +30,7 @@ val tptp_arity_clause : arityClause -> string val tptp_classrelClause : classrelClause -> string val tptp_clause : clause -> string list + val clause_info : clause -> string * string val tptp_clauses2str : string list -> string val typed : unit -> unit val untyped : unit -> unit @@ -643,6 +644,14 @@ cls_str :: (typ_clss 0 tfree_lits) end; +fun clause_info cls = + let + val cls_id = string_of_clauseID cls + val ax_name = string_of_axiomName cls + in + ((ax_name^""), cls_id) + end; + fun clause2tptp cls = let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)