# HG changeset patch # User paulson # Date 1125676524 -7200 # Node ID 12a9393c5d77c543391e66904710b228ff7fa18f # Parent 41eee2e7b465972f51de92eea8337590cc074838 further tidying up of Isabelle-ATP link diff -r 41eee2e7b465 -r 12a9393c5d77 src/HOL/Tools/ATP/res_clasimpset.ML --- 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) diff -r 41eee2e7b465 -r 12a9393c5d77 src/HOL/Tools/ATP/watcher.ML --- 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 diff -r 41eee2e7b465 -r 12a9393c5d77 src/HOL/Tools/res_atp.ML --- 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 ) diff -r 41eee2e7b465 -r 12a9393c5d77 src/HOL/Tools/res_clause.ML --- 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