--- a/src/HOL/Tools/ATP/res_clasimpset.ML Fri Sep 02 17:23:59 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Fri Sep 02 17:55:24 2005 +0200
@@ -6,7 +6,9 @@
structure ReduceAxiomsN =
(* Author: Jia Meng, Cambridge University Computer Laboratory
- Remove irrelevant axioms used for a proof of a goal, with with iteration control*)
+ Remove irrelevant axioms used for a proof of a goal, with with iteration control
+
+ Initial version. Needs elaboration. *)
struct
@@ -143,31 +145,6 @@
(* outputs a list of (thm,clause) pairs *)
-(* 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;
-
-(*FIXME: this logic (especially concat_with_stop) needs to be replaced by code
-to invert the function ascii_of.*)
-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) = (remove_symb str, thm);
-
-fun remove_spaces_pair (str, thm) = (remove_spaces str, thm);
-
-
(*Insert th into the result provided the name is not "".*)
fun add_nonempty ((name,th), ths) = if name="" then ths else th::ths;
@@ -187,16 +164,10 @@
fun clause_numbering ((clause, theorem), cls) =
let val num_of_cls = length cls
val numbers = 0 upto (num_of_cls -1)
- val multi_name = multi (clause, theorem) num_of_cls []
in
- (multi_name)
+ multi (clause, theorem) num_of_cls []
end;
-
-
-fun concat_with sep [] = ""
- | concat_with sep [x] = "(" ^ x ^ ")"
- | concat_with sep (x::xs) = "(" ^ x ^ ")" ^ sep ^ (concat_with sep xs);
-
+
(*Write out the claset and simpset rules of the supplied theory.
FIXME: argument "goal" is a hack to allow relevance filtering.
@@ -211,17 +182,12 @@
val simpset_rules =
ReduceAxiomsN.relevant_filter (!relevant) goal
(ResAxioms.simpset_rules_of_thy thy);
- val named_simpset =
- map remove_spaces_pair (map put_name_pair simpset_rules)
- val justnames = map #1 named_simpset
- val namestring = concat_with "\n" justnames
- val _ = File.append (File.tmp_path (Path.basic "clasimp_names"))
- (namestring)
+ val named_simpset = map put_name_pair simpset_rules
val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
- val cls_thms = if !use_simpset then (claset_cls_thms@simpset_cls_thms) else claset_cls_thms;
+ val cls_thms = if !use_simpset then (claset_cls_thms@simpset_cls_thms)
+ else claset_cls_thms;
val cls_thms_list = List.concat cls_thms;
- (* length 1429 *)
(*************************************************)
(* Write out clauses as tptp strings to filename *)
(*************************************************)
@@ -239,10 +205,8 @@
(* list of lists of tptp string clauses *)
val stick_clasrls = List.concat cls_tptp_strs;
- (* length 1581*)
val out = TextIO.openOut filename;
val _= ResLib.writeln_strs out stick_clasrls;
- val _= TextIO.flushOut out;
val _= TextIO.closeOut out
in
(clause_arr, num_of_clauses, clauses)
--- a/src/HOL/Tools/ATP/watcher.ML Fri Sep 02 17:23:59 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Fri Sep 02 17:55:24 2005 +0200
@@ -236,7 +236,9 @@
val _ = File.append (File.tmp_path (Path.basic "sep_comms"))
("Sep comms are: "^(implode str)^"**"^
- prover^" thmstring: "^thmstring^"\n goalstr: "^goalstring^" \n provercmd: "^proverCmd^" \n clasimp "^clasimpfile^" \n hyps "^hypsfile^"\n prob "^file^"\n\n")
+ prover^" thmstring: "^thmstring^"\n goalstr: "^goalstring^
+ " \n provercmd: "^proverCmd^" \n clasimp "^clasimpfile^
+ " \n hyps "^hypsfile^"\n prob "^file^"\n\n")
in
(prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file)
end
@@ -255,20 +257,9 @@
(*** 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, ">",
+ [clasimpfile,probfile, ">",
File.platform_path wholefile])
- val dfg_dir = File.tmp_path (Path.basic "dfg");
- val dfg_path = File.platform_path dfg_dir;
-
- (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
- val probID = List.last(explode probfile)
- 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.platform_path wholefile)])
-
(* if using spass prob_n already contains whole DFG file, otherwise need to mash axioms*)
(* from clasimpset onto problem file *)
val newfile = if !SpassComm.spass
@@ -276,7 +267,8 @@
else (File.platform_path wholefile)
val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
- (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")
+ (thmstring^"\n goals_watched"^
+ (string_of_int(!goals_being_watched))^newfile^"\n")
in
(prover,thmstring,goalstring, proverCmd, settings,newfile)
end;
@@ -378,317 +370,317 @@
(****** fork a watcher process and get it set up and going *)
(***********************************************************)
fun startWatcher (procList) =
- (case Posix.Process.fork() (***************************************)
- of SOME pid => pid (* parent - i.e. main Isabelle process *)
- (***************************************)
+ (case Posix.Process.fork() (***************************************)
+ of SOME pid => pid (* parent - i.e. main Isabelle process *)
+ (***************************************)
- (*************************)
- | NONE => let (* child - i.e. watcher *)
- val oldchildin = #infd p1 (*************************)
- val fromParent = Posix.FileSys.wordToFD 0w0
- val oldchildout = #outfd p2
- val toParent = Posix.FileSys.wordToFD 0w1
- val fromParentIOD = Posix.FileSys.fdToIOD fromParent
- val fromParentStr = openInFD ("_exec_in_parent", fromParent)
- val toParentStr = openOutFD ("_exec_out_parent", toParent)
- val sign = sign_of_thm thm
- val prems = prems_of thm
- val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
- val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
- (* tracing *)
- (*val tenth_ax = fst( Array.sub(clause_arr, 1))
- val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
- val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
- val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))
- val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))
- val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )
- *)
- (*val goalstr = string_of_thm (the_goal)
- val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher")));
- val _ = TextIO.output (outfile,goalstr )
- val _ = TextIO.closeOut outfile*)
- fun killChildren [] = ()
- | killChildren (child_handle::children) = (killChild child_handle; killChildren children)
+ (*************************)
+ | NONE => let (* child - i.e. watcher *)
+ val oldchildin = #infd p1 (*************************)
+ val fromParent = Posix.FileSys.wordToFD 0w0
+ val oldchildout = #outfd p2
+ val toParent = Posix.FileSys.wordToFD 0w1
+ val fromParentIOD = Posix.FileSys.fdToIOD fromParent
+ val fromParentStr = openInFD ("_exec_in_parent", fromParent)
+ val toParentStr = openOutFD ("_exec_out_parent", toParent)
+ val sign = sign_of_thm thm
+ val prems = prems_of thm
+ val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
+ val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
+ (* tracing *)
+ (*val tenth_ax = fst( Array.sub(clause_arr, 1))
+ val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
+ val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
+ val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))
+ val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))
+ val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )
+ *)
+ (*val goalstr = string_of_thm (the_goal)
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher")));
+ val _ = TextIO.output (outfile,goalstr )
+ val _ = TextIO.closeOut outfile*)
+ fun killChildren [] = ()
+ | killChildren (child_handle::children) = (killChild child_handle; killChildren children)
- (*************************************************************)
- (* take an instream and poll its underlying reader for input *)
- (*************************************************************)
+ (*************************************************************)
+ (* take an instream and poll its underlying reader for input *)
+ (*************************************************************)
- fun pollParentInput () =
- let val pd = OS.IO.pollDesc (fromParentIOD)
- in
- if (isSome pd ) then
- let val pd' = OS.IO.pollIn (valOf pd)
- val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000))
- val _ = File.append (File.tmp_path (Path.basic "parent_poll"))
- ("In parent_poll\n")
- in
- if null pdl
- then
- NONE
- else if (OS.IO.isIn (hd pdl))
- then SOME (getCmds (toParentStr, fromParentStr, []))
- else NONE
- end
- else NONE
- end
-
- fun pollChildInput (fromStr) =
- let val _ = File.append (File.tmp_path (Path.basic "child_poll"))
- ("In child_poll\n")
- val iod = getInIoDesc fromStr
- in
- if isSome iod
- then
- let val pd = OS.IO.pollDesc (valOf iod)
- in
- if (isSome pd ) then
- let val pd' = OS.IO.pollIn (valOf pd)
- val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000))
- in
- if null pdl
+ fun pollParentInput () =
+ let val pd = OS.IO.pollDesc (fromParentIOD)
+ in
+ if (isSome pd ) then
+ let val pd' = OS.IO.pollIn (valOf pd)
+ val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000))
+ val _ = File.append (File.tmp_path (Path.basic "parent_poll"))
+ ("In parent_poll\n")
+ in
+ if null pdl
+ then
+ NONE
+ else if (OS.IO.isIn (hd pdl))
+ then SOME (getCmds (toParentStr, fromParentStr, []))
+ else NONE
+ end
+ else NONE
+ end
+
+ fun pollChildInput (fromStr) =
+ let val _ = File.append (File.tmp_path (Path.basic "child_poll"))
+ ("In child_poll\n")
+ val iod = getInIoDesc fromStr
+ in
+ if isSome iod
+ then
+ let val pd = OS.IO.pollDesc (valOf iod)
+ in
+ if (isSome pd ) then
+ let val pd' = OS.IO.pollIn (valOf pd)
+ val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000))
+ in
+ if null pdl
+ then
+ ( File.append (File.tmp_path (Path.basic "child_poll_res"))
+ ("Null pdl \n");NONE)
+ else if (OS.IO.isIn (hd pdl))
then
- ( File.append (File.tmp_path (Path.basic "child_poll_res"))
- ("Null pdl \n");NONE)
- else if (OS.IO.isIn (hd pdl))
- then
- (let val inval = (TextIO.inputLine fromStr)
- val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
- in
- SOME inval
- end)
- else
- ( File.append (File.tmp_path (Path.basic "child_poll_res"))
- ("Null pdl \n");NONE)
- end
- else NONE
- end
- else NONE
- end
+ (let val inval = (TextIO.inputLine fromStr)
+ val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
+ in
+ SOME inval
+ end)
+ else
+ ( File.append (File.tmp_path (Path.basic "child_poll_res"))
+ ("Null pdl \n");NONE)
+ end
+ else NONE
+ end
+ else NONE
+ end
- (****************************************************************************)
- (* Check all vampire processes currently running for output *)
- (****************************************************************************)
- (*********************************)
- fun checkChildren ([], toParentStr) = [] (*** no children to check ********)
- (*********************************)
- | checkChildren ((childProc::otherChildren), toParentStr) =
- let val _ = File.append (File.tmp_path (Path.basic "child_check"))
- ("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n")
- val (childInput,childOutput) = cmdstreamsOf childProc
- val child_handle= cmdchildHandle childProc
- (* childCmd is the .dfg file that the problem is in *)
- val childCmd = fst(snd (cmdchildInfo childProc))
- val _ = File.append (File.tmp_path (Path.basic "child_command"))
- (childCmd^"\n")
- (* now get the number of the subgoal from the filename *)
- val sg_num = (*if (!SpassComm.spass )
- then
- int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
- else*)
- int_of_string(hd (rev(explode childCmd)))
+ (****************************************************************************)
+ (* Check all vampire processes currently running for output *)
+ (****************************************************************************)
+ (*********************************)
+ fun checkChildren ([], toParentStr) = [] (*** no children to check ********)
+ (*********************************)
+ | checkChildren ((childProc::otherChildren), toParentStr) =
+ let val _ = File.append (File.tmp_path (Path.basic "child_check"))
+ ("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n")
+ val (childInput,childOutput) = cmdstreamsOf childProc
+ val child_handle= cmdchildHandle childProc
+ (* childCmd is the .dfg file that the problem is in *)
+ val childCmd = fst(snd (cmdchildInfo childProc))
+ val _ = File.append (File.tmp_path (Path.basic "child_command"))
+ (childCmd^"\n")
+ (* now get the number of the subgoal from the filename *)
+ val sg_num = (*if (!SpassComm.spass )
+ then
+ int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
+ else*)
+ int_of_string(hd (rev(explode childCmd)))
- val childIncoming = pollChildInput childInput
- val _ = File.append (File.tmp_path (Path.basic "child_check_polled"))
- ("finished polling child \n")
- val parentID = Posix.ProcEnv.getppid()
- val prover = cmdProver childProc
- val thmstring = cmdThm childProc
- val sign = sign_of_thm thm
- val prems = prems_of thm
- val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
- val _ = warning("subgoals forked to checkChildren: "^prems_string)
- val goalstring = cmdGoal childProc
- val _ = File.append (File.tmp_path (Path.basic "child_comms"))
- (prover^thmstring^goalstring^childCmd^"\n")
- in
- if (isSome childIncoming)
- then
- (* check here for prover label on child*)
- let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))
- ("subgoals forked to checkChildren:"^
- prems_string^prover^thmstring^goalstring^childCmd)
- val childDone = (case prover of
- "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )
- |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) )
- in
- if childDone (**********************************************)
- then (* child has found a proof and transferred it *)
- (* Remove this child and go on to check others*)
- (**********************************************)
- (Unix.reap child_handle;
- checkChildren(otherChildren, toParentStr))
- else
- (**********************************************)
- (* Keep this child and go on to check others *)
- (**********************************************)
- (childProc::(checkChildren (otherChildren, toParentStr)))
- end
- else
- (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
- childProc::(checkChildren (otherChildren, toParentStr)))
+ val childIncoming = pollChildInput childInput
+ val _ = File.append (File.tmp_path (Path.basic "child_check_polled"))
+ ("finished polling child \n")
+ val parentID = Posix.ProcEnv.getppid()
+ val prover = cmdProver childProc
+ val thmstring = cmdThm childProc
+ val sign = sign_of_thm thm
+ val prems = prems_of thm
+ val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
+ val _ = warning("subgoals forked to checkChildren: "^prems_string)
+ val goalstring = cmdGoal childProc
+ val _ = File.append (File.tmp_path (Path.basic "child_comms"))
+ (prover^thmstring^goalstring^childCmd^"\n")
+ in
+ if (isSome childIncoming)
+ then
+ (* check here for prover label on child*)
+ let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))
+ ("subgoals forked to checkChildren:"^
+ prems_string^prover^thmstring^goalstring^childCmd)
+ val childDone = (case prover of
+ "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )
+ |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) )
+ in
+ if childDone (**********************************************)
+ then (* child has found a proof and transferred it *)
+ (* Remove this child and go on to check others*)
+ (**********************************************)
+ (Unix.reap child_handle;
+ checkChildren(otherChildren, toParentStr))
+ else
+ (**********************************************)
+ (* Keep this child and go on to check others *)
+ (**********************************************)
+ (childProc::(checkChildren (otherChildren, toParentStr)))
end
+ else
+ (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
+ childProc::(checkChildren (otherChildren, toParentStr)))
+ end
-
- (********************************************************************)
- (* call resolution processes *)
- (* settings should be a list of strings *)
- (* e.g. ["-t 300", "-m 100000"] (TextIO.input instr)^ *)
- (* takes list of (string, string, string list, string)list proclist *)
- (********************************************************************)
+
+ (********************************************************************)
+ (* call resolution processes *)
+ (* settings should be a list of strings *)
+ (* e.g. ["-t 300", "-m 100000"] (TextIO.input instr)^ *)
+ (* takes list of (string, string, string list, string)list proclist *)
+ (********************************************************************)
(*** add subgoal id num to this *)
- fun execCmds [] procList = procList
- | 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()))))
- in
- if (prover = "spass")
- then
- 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 _ = File.append (File.tmp_path (Path.basic "exec_child"))
- ("\nexecuting command for goal:\n"^
- goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
- in
- Posix.Process.sleep (Time.fromSeconds 1);execCmds cmds newProcList
- end
- else
- let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc =
- (Unix.execute(proverCmd, (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 _ = File.append (File.tmp_path (Path.basic "exec_child"))
- ("executing command for goal:\n"^
- goalstring^proverCmd^(concat settings)^file^
- " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
- in
- Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList
- end
- end
+ fun execCmds [] procList = procList
+ | 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()))))
+ in
+ if (prover = "spass")
+ then
+ 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 _ = File.append (File.tmp_path (Path.basic "exec_child"))
+ ("\nexecuting command for goal:\n"^
+ goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
+ in
+ Posix.Process.sleep (Time.fromSeconds 1);
+ execCmds cmds newProcList
+ end
+ else
+ let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc =
+ (Unix.execute(proverCmd, (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 _ = File.append (File.tmp_path (Path.basic "exec_child"))
+ ("executing command for goal:\n"^
+ goalstring^proverCmd^(concat settings)^file^
+ " at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
+ in
+ Posix.Process.sleep (Time.fromSeconds 1);
+ execCmds cmds newProcList
+ end
+ end
- (****************************************)
- (* call resolution processes remotely *)
- (* settings should be a list of strings *)
- (* e.g. ["-t 300", "-m 100000"] *)
- (****************************************)
+ (****************************************)
+ (* call resolution processes remotely *)
+ (* settings should be a list of strings *)
+ (* e.g. ["-t 300", "-m 100000"] *)
+ (****************************************)
- (* 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 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))
+ fun printList (outStr, []) = ()
+ | printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))
- (**********************************************)
- (* Watcher Loop *)
- (**********************************************)
+ (**********************************************)
+ (* Watcher Loop *)
+ (**********************************************)
- fun keepWatching (toParentStr, fromParentStr,procList) =
- let fun loop (procList) =
- let val cmdsFromIsa = pollParentInput ()
- fun killchildHandler (n:int) =
- (TextIO.output(toParentStr, "Killing child proof processes!\n");
- TextIO.flushOut toParentStr;
- killChildren (map (cmdchildHandle) procList);
- ())
- in
- (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
- (**********************************)
- if (isSome cmdsFromIsa)
- then (* deal with input from Isabelle *)
- if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
- then
- let val child_handles = map cmdchildHandle procList
- in
- killChildren child_handles;
- (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)
- loop ([])
- end
- else
- if ((length procList)<10) (********************)
- then (* Execute locally *)
- let
- val newProcList = execCmds (valOf cmdsFromIsa) procList
- val parentID = Posix.ProcEnv.getppid()
- val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
- val newProcList' =checkChildren (newProcList, toParentStr)
+ fun keepWatching (toParentStr, fromParentStr,procList) =
+ let fun loop (procList) =
+ let val _ = Posix.Process.sleep (Time.fromMilliseconds 200)
+ val cmdsFromIsa = pollParentInput ()
+ fun killchildHandler (n:int) =
+ (TextIO.output(toParentStr, "Killing child proof processes!\n");
+ TextIO.flushOut toParentStr;
+ killChildren (map (cmdchildHandle) procList);
+ ())
+ in
+ (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
+ (**********************************)
+ if (isSome cmdsFromIsa)
+ then (* deal with input from Isabelle *)
+ if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
+ then
+ let val child_handles = map cmdchildHandle procList
+ in
+ killChildren child_handles;
+ (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)
+ loop ([])
+ end
+ else
+ if ((length procList)<10) (********************)
+ then (* Execute locally *)
+ let
+ val newProcList = execCmds (valOf cmdsFromIsa) procList
+ val parentID = Posix.ProcEnv.getppid()
+ val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
+ val newProcList' =checkChildren (newProcList, toParentStr)
- val _ = warning("off to keep watching...")
- val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
- in
- (*Posix.Process.sleep (Time.fromSeconds 1);*)
- loop (newProcList')
- end
- else (* Execute remotely *)
- (* (actually not remote for now )*)
- let
- val newProcList = execCmds (valOf cmdsFromIsa) procList
- val parentID = Posix.ProcEnv.getppid()
- val newProcList' =checkChildren (newProcList, toParentStr)
- in
- (*Posix.Process.sleep (Time.fromSeconds 1);*)
- loop (newProcList')
- end
- else (* No new input from Isabelle *)
- let val newProcList = checkChildren ((procList), toParentStr)
- in
- (*Posix.Process.sleep (Time.fromSeconds 1);*)
- (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
- loop (newProcList)
- end
- end
- in
- loop (procList)
- end
-
-
- in
- (***************************)
- (*** Sort out pipes ********)
- (***************************)
+ val _ = warning("off to keep watching...")
+ val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
+ in
+ loop (newProcList')
+ end
+ else (* Execute remotely *)
+ (* (actually not remote for now )*)
+ let
+ val newProcList = execCmds (valOf cmdsFromIsa) procList
+ val parentID = Posix.ProcEnv.getppid()
+ val newProcList' =checkChildren (newProcList, toParentStr)
+ in
+ loop (newProcList')
+ end
+ else (* No new input from Isabelle *)
+ let val newProcList = checkChildren ((procList), toParentStr)
+ in
+ (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
+ loop (newProcList)
+ end
+ end
+ in
+ loop (procList)
+ end
+
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p2);
- Posix.IO.dup2{old = oldchildin, new = fromParent};
- Posix.IO.close oldchildin;
- Posix.IO.dup2{old = oldchildout, new = toParent};
- Posix.IO.close oldchildout;
+ in
+ (***************************)
+ (*** Sort out pipes ********)
+ (***************************)
- (***************************)
- (* start the watcher loop *)
- (***************************)
- keepWatching (toParentStr, fromParentStr, procList);
- (****************************************************************************)
- (* fake return value - actually want the watcher to loop until killed *)
- (****************************************************************************)
- Posix.Process.wordToPid 0w0
- end);
- (* end case *)
+ Posix.IO.close (#outfd p1);
+ Posix.IO.close (#infd p2);
+ Posix.IO.dup2{old = oldchildin, new = fromParent};
+ Posix.IO.close oldchildin;
+ Posix.IO.dup2{old = oldchildout, new = toParent};
+ Posix.IO.close oldchildout;
+
+ (***************************)
+ (* start the watcher loop *)
+ (***************************)
+ keepWatching (toParentStr, fromParentStr, procList);
+ (****************************************************************************)
+(* fake return value - actually want the watcher to loop until killed *)
+ (****************************************************************************)
+ Posix.Process.wordToPid 0w0
+ end);
+ (* end case *)
val _ = TextIO.flushOut TextIO.stdOut
--- a/src/HOL/Tools/res_atp.ML Fri Sep 02 17:23:59 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Fri Sep 02 17:55:24 2005 +0200
@@ -8,8 +8,6 @@
signature RES_ATP =
sig
val axiom_file : Path.T
- val hyps_file : Path.T
- val prob_file : Path.T;
(*val atp_ax_tac : thm list -> int -> Tactical.tactic*)
(*val atp_tac : int -> Tactical.tactic*)
val full_spass: bool ref
@@ -53,16 +51,10 @@
REPEAT_DETERM_N (length ts) o (etac thin_rl)]
end);
-(* temporarily use these files, which will be loaded by Vampire *)
-val file_id_num = ref 0;
-fun new_prob_file () = "prob" ^ string_of_int (inc file_id_num);
-
val axiom_file = File.tmp_path (Path.basic "axioms");
val clasimp_file = File.tmp_path (Path.basic "clasimp");
val hyps_file = File.tmp_path (Path.basic "hyps");
val prob_file = File.tmp_path (Path.basic "prob");
-val dummy_tac = all_tac;
-val _ =debug (File.platform_path prob_file);
(**** for Isabelle/ML interface ****)
@@ -149,11 +141,11 @@
val _ = debug ("about to write out dfg prob file " ^ probfile)
(*val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
val tfree_clss = map ResClause.tfree_dfg_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) *)
- val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n))
+ val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n))
axclauses [] [] [] tfrees
val out = TextIO.openOut(probfile)
in
- (ResLib.writeln_strs out [filestr]; TextIO.closeOut out; debug probfile )
+ (ResLib.writeln_strs out [probN]; TextIO.closeOut out; debug probfile )
(* (ResLib.writeln_strs out (tfree_clss @ dfg_clss); *)
end;
@@ -210,12 +202,12 @@
in
Watcher.callResProvers(childout,atp_list);
debug "Sent commands to watcher!";
- dummy_tac
+ all_tac
end
(**********************************************************)
(* write out the current subgoal as a tptp file, probN, *)
-(* then call dummy_tac - should be call_res_tac *)
+(* then call all_tac - should be call_res_tac *)
(**********************************************************)
@@ -223,7 +215,7 @@
if n=0 then
(call_resolve_tac (rev sko_thms)
sign sg_terms (childin, childout, pid) (List.length sg_terms);
- dummy_tac thm)
+ all_tac thm)
else
( SELECT_GOAL
@@ -234,7 +226,7 @@
else tptp_inputs_tfrees (make_clauses negs) n tfrees;
get_sko_thms tfrees sign sg_terms (childin, childout, pid)
thm (n -1) (negs::sko_thms) axclauses;
- dummy_tac))]) n thm )
+ all_tac))]) n thm )
--- a/src/HOL/Tools/res_clause.ML Fri Sep 02 17:23:59 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML Fri Sep 02 17:55:24 2005 +0200
@@ -226,8 +226,12 @@
(*** make clauses ***)
-fun make_clause (clause_id,axiom_name,kind,literals,types_sorts,tvar_type_literals,
+fun make_clause (clause_id,axiom_name,kind,literals,
+ types_sorts,tvar_type_literals,
tfree_type_literals,tvars, predicates, functions) =
+ if null literals
+ then error "Problem too trivial for resolution (empty clause)"
+ else
Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind,
literals = literals, types_sorts = types_sorts,
tvar_type_literals = tvar_type_literals,
@@ -400,28 +404,29 @@
| _ => pred_of_nonEq (pred,args)
end;
-
-
-fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) = literals_of_term(P,lits_ts, preds, funcs)
+fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) =
+ literals_of_term(P,lits_ts, preds, funcs)
| literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts), preds,funcs) =
- let val (lits',ts', preds', funcs') = literals_of_term(P,(lits,ts), preds,funcs)
- in
- literals_of_term(Q,(lits',ts'), distinct(preds'@preds), distinct(funcs'@funcs))
- end
+ let val (lits',ts', preds', funcs') =
+ literals_of_term(P,(lits,ts), preds,funcs)
+ in
+ literals_of_term(Q, (lits',ts'), distinct(preds'@preds),
+ distinct(funcs'@funcs))
+ end
| literals_of_term ((Const("Not",_) $ P),(lits,ts), preds, funcs) =
- let val (pred,ts', preds', funcs') = predicate_of P
- val lits' = Literal(false,pred,false) :: lits
- val ts'' = ResLib.no_rep_app ts ts'
- in
- (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
- end
+ let val (pred,ts', preds', funcs') = predicate_of P
+ val lits' = Literal(false,pred,false) :: lits
+ val ts'' = ResLib.no_rep_app ts ts'
+ in
+ (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
+ end
| literals_of_term (P,(lits,ts), preds, funcs) =
- let val (pred,ts', preds', funcs') = predicate_of P
- val lits' = Literal(true,pred,false) :: lits
- val ts'' = ResLib.no_rep_app ts ts'
- in
- (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
- end;
+ let val (pred,ts', preds', funcs') = predicate_of P
+ val lits' = Literal(true,pred,false) :: lits
+ val ts'' = ResLib.no_rep_app ts ts'
+ in
+ (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
+ end;
fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]), [], []);
@@ -690,7 +695,8 @@
end;
(* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
-fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms)
+fun string_of_predicate (Predicate("equal",typ,terms)) =
+ string_of_equality(typ,terms)
| string_of_predicate (Predicate(name,_,[])) = name
| string_of_predicate (Predicate(name,typ,terms)) =
let val terms_as_strings = map string_of_term terms
@@ -708,9 +714,8 @@
fun dfg_literal (Literal(pol,pred,tag)) =
let val pred_string = string_of_predicate pred
- val tagged_pol =if pol then pred_string else "not(" ^pred_string ^ ")"
- in
- tagged_pol
+ in
+ if pol then pred_string else "not(" ^pred_string ^ ")"
end;
@@ -755,7 +760,7 @@
if !keep_types then map dfg_of_typeLit (#tfree_type_literals cls)
else []
in
- (tvar_lits_strs @ lits,tfree_lits)
+ (tvar_lits_strs @ lits, tfree_lits)
end;
@@ -766,7 +771,7 @@
end
-fun get_uvars (UVar(str,typ)) =(*if (substring (str, 0,2))= "V_" then *)[str] (*else []*)
+fun get_uvars (UVar(str,typ)) = [str]
| get_uvars (Fun (str,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist)
@@ -819,12 +824,8 @@
| concat_with sep [x] = "(" ^ x ^ ")"
| concat_with sep (x::xs) = "(" ^ x ^ ")" ^ sep ^ (concat_with sep xs);
-fun concat_with_comma [] = ""
- | concat_with_comma [x] = x
- | concat_with_comma (x::xs) = x ^ ", " ^ (concat_with_comma xs);
-
-
-fun dfg_pred (Literal(pol,pred,tag)) ax_name = (string_of_predname pred)^" "^ax_name
+fun dfg_pred (Literal(pol,pred,tag)) ax_name =
+ (string_of_predname pred) ^ " " ^ ax_name
fun dfg_clause cls =
let val (lits,tfree_lits) = dfg_clause_aux cls
@@ -834,11 +835,12 @@
val cls_id = string_of_clauseID cls
val ax_name = string_of_axiomName cls
val knd = string_of_kind cls
- val lits_str = concat_with_comma lits
+ val lits_str = commas lits
val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars, vars)
fun typ_clss k [] = []
| typ_clss k (tfree :: tfrees) =
- (gen_dfg_type_cls(cls_id,knd,tfree,k, tvars,vars)) :: (typ_clss (k+1) tfrees)
+ (gen_dfg_type_cls(cls_id,knd,tfree,k, tvars,vars)) ::
+ (typ_clss (k+1) tfrees)
in
cls_str :: (typ_clss 0 tfree_lits)
end;
@@ -851,21 +853,26 @@
fun string_of_arity (name, num) = name ^"," ^ (string_of_int num)
+fun string_of_preds preds =
+ "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n";
-fun string_of_preds preds = "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n";
-
-fun string_of_funcs funcs ="functions[" ^ (concat_with ", " (map string_of_arity funcs)) ^ "].\n" ;
+fun string_of_funcs funcs =
+ "functions[" ^ (concat_with ", " (map string_of_arity funcs)) ^ "].\n" ;
-fun string_of_symbols predstr funcstr = "list_of_symbols.\n" ^ predstr ^ funcstr ^ "end_of_list.\n\n";
+fun string_of_symbols predstr funcstr =
+ "list_of_symbols.\n" ^ predstr ^ funcstr ^ "end_of_list.\n\n";
-fun string_of_axioms axstr = "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n";
+fun string_of_axioms axstr =
+ "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n";
-fun string_of_conjectures conjstr = "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n";
+fun string_of_conjectures conjstr =
+ "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n";
-fun string_of_descrip () = "list_of_descriptions.\nname({*[ File : ],[ Names :]*}).\nauthor({*[ Source :]*}).\nstatus(unknown).\ndescription({*[ Refs :]*}).\nend_of_list.\n\n"
+fun string_of_descrip () =
+ "list_of_descriptions.\nname({*[ File : ],[ Names :]*}).\nauthor({*[ Source :]*}).\nstatus(unknown).\ndescription({*[ Refs :]*}).\nend_of_list.\n\n"
fun string_of_start name = "%------------------------------------------------------------------------------\nbegin_problem(" ^ name ^ ").\n\n";
@@ -878,7 +885,8 @@
fun clause2dfg cls =
- let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)
+ let val (lits,tfree_lits) = dfg_clause_aux cls
+ (*"lits" includes the typing assumptions (TVars)*)
val cls_id = string_of_clauseID cls
val ax_name = string_of_axiomName cls
val vars = dfg_vars cls
@@ -886,7 +894,7 @@
val funcs = funcs_of_cls cls
val preds = preds_of_cls cls
val knd = string_of_kind cls
- val lits_str = concat_with_comma lits
+ val lits_str = commas lits
val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars,vars)
in
(cls_str,tfree_lits)
@@ -894,7 +902,8 @@
-fun tfree_dfg_clause tfree_lit = "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^ "tfree_tcs" ^ ")."
+fun tfree_dfg_clause tfree_lit =
+ "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^ "tfree_tcs" ^ ")."
fun gen_dfg_file probname axioms conjectures funcs preds tfrees=
@@ -1113,8 +1122,8 @@
fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls);
-
-fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls);
+fun strings_of_premLits (ArityClause arcls) =
+ map string_of_arLit (#premLits arcls);
fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
@@ -1127,13 +1136,11 @@
val all_lits = concl_lit :: prems_lits
in
"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ (ResLib.list_to_string' all_lits) ^ ")."
-
end;
val clrelclause_prefix = "relcls_";
-
fun tptp_classrelLits sub sup =
let val tvar = "(T)"
in