improved process handling. tidied
--- a/src/HOL/Tools/ATP/res_clasimpset.ML Wed Oct 05 10:56:06 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Wed Oct 05 11:18:06 2005 +0200
@@ -68,7 +68,7 @@
let val consts = consts_in_goal goal
fun relevant_axioms_aux1 cs k =
let val thms1 = axioms_having_consts cs thmTab
- val cs1 = ResLib.flat_noDup (map consts_of_thm thms1)
+ val cs1 = foldl (op union_string) [] (map consts_of_thm thms1)
in
if ((cs1 subset cs) orelse n <= k) then (k,thms1)
else (relevant_axioms_aux1 (cs1 union cs) (k+1))
--- a/src/HOL/Tools/ATP/watcher.ML Wed Oct 05 10:56:06 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Wed Oct 05 11:18:06 2005 +0200
@@ -4,14 +4,11 @@
Copyright 2004 University of Cambridge
*)
- (***************************************************************************)
- (* The watcher process starts a resolution process when it receives a *)
+(* The watcher process starts a resolution process when it receives a *)
(* message from Isabelle *)
(* Signals Isabelle, puts output of child into pipe to Isabelle, *)
(* and removes dead processes. Also possible to kill all the resolution *)
(* processes currently running. *)
-(* Hardwired version of where to pick up the tptp files for the moment *)
-(***************************************************************************)
signature WATCHER =
sig
@@ -23,17 +20,15 @@
TextIO.outstream * (string*string*string*string*string) list
-> unit
-(* Send message to watcher to kill currently running resolution provers *)
+(* Send message to watcher to kill resolution provers *)
val callSlayer : TextIO.outstream -> unit
(* Start a watcher and set up signal handlers *)
val createWatcher :
thm * (ResClause.clause * thm) Array.array ->
TextIO.instream * TextIO.outstream * Posix.Process.pid
-
-(* Kill watcher process *)
val killWatcher : Posix.Process.pid -> unit
-val killWatcher' : int -> unit
+val setting_sep : char
end
@@ -41,6 +36,10 @@
structure Watcher: WATCHER =
struct
+(*Field separators, used to pack items onto a text line*)
+val command_sep = #"\t"
+and setting_sep = #"%";
+
open Recon_Transfer
val goals_being_watched = ref 0;
@@ -134,8 +133,6 @@
(* need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
(*****************************************************************************************)
-
-(*Uses the $-character to separate items sent to watcher*)
fun callResProvers (toWatcherStr, []) =
(TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr)
| callResProvers (toWatcherStr,
@@ -144,9 +141,11 @@
let val _ = trace (space_implode "\n"
(["\ncallResProvers:",prover,goalstring,proverCmd,settings,
probfile]))
- in TextIO.output (toWatcherStr,
- prover^"$"^proverCmd^"$"^ settings^"$"^probfile^"$\n");
- TextIO.output (toWatcherStr, String.toString goalstring^"\n");
+ in TextIO.output (toWatcherStr,
+ (*Uses a special character to separate items sent to watcher*)
+ space_implode (str command_sep)
+ [prover, proverCmd, settings, probfile,
+ String.toString goalstring ^ "\n"]);
(*goalstring is a single string literal, with all specials escaped.*)
goals_being_watched := (!goals_being_watched) + 1;
TextIO.flushOut toWatcherStr;
@@ -155,31 +154,29 @@
-(**************************************************************)
-(* Send message to watcher to kill currently running vampires *)
-(**************************************************************)
-fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n");
+(*Send message to watcher to kill currently running vampires. NOT USED and possibly
+ buggy. Note that killWatcher kills the entire process group anyway.*)
+fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
TextIO.flushOut toWatcherStr)
(**************************************************************)
(* Get commands from Isabelle *)
(**************************************************************)
-fun getCmds (toParentStr,fromParentStr, cmdList) =
+fun getCmds (toParentStr, fromParentStr, cmdList) =
let val thisLine = TextIO.inputLine fromParentStr
- val _ = trace("\nGot command from parent: " ^ thisLine)
in
+ trace("\nGot command from parent: " ^ thisLine);
if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
else if thisLine = "Kill children\n"
- then (TextIO.output (toParentStr,thisLine );
+ then (TextIO.output (toParentStr,thisLine);
TextIO.flushOut toParentStr;
- (("","","Kill children",[],"")::cmdList) )
+ [("","","Kill children",[],"")])
else
- let val [prover,proverCmd,settingstr,probfile,_] =
- String.tokens (fn c => c = #"$") thisLine
- val settings = String.tokens (fn c => c = #"%") settingstr
- val goalstring = TextIO.inputLine fromParentStr
+ let val [prover,proverCmd,settingstr,probfile,goalstring] =
+ String.tokens (fn c => c = command_sep) thisLine
+ val settings = String.tokens (fn c => c = setting_sep) settingstr
in
trace ("\nprover: " ^ prover ^ " prover path: " ^ proverCmd^
" problem file: " ^ probfile ^
@@ -187,6 +184,9 @@
getCmds (toParentStr, fromParentStr,
(prover, goalstring, proverCmd, settings, probfile)::cmdList)
end
+ handle Bind =>
+ (trace "getCmds: command parsing failed!";
+ getCmds (toParentStr, fromParentStr, cmdList))
end
@@ -212,8 +212,6 @@
(* Set up a Watcher Process *)
(*************************************)
-fun getProofCmd (a,c,d,e,f) = d
-
(* for tracing: encloses each string element in brackets. *)
val concat_with_and = space_implode " & " o map (enclose "(" ")");
@@ -246,40 +244,34 @@
fun setupWatcher (thm,clause_arr) =
let
- (** pipes for communication between parent and watcher **)
- val p1 = Posix.IO.pipe ()
+ val p1 = Posix.IO.pipe () (** pipes for communication between parent and watcher **)
val p2 = Posix.IO.pipe ()
fun closep () =
- (Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p1);
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p2))
- (***********************************************************)
- (****** fork a watcher process and get it set up and going *)
- (***********************************************************)
+ (Posix.IO.close (#outfd p1); Posix.IO.close (#infd p1);
+ Posix.IO.close (#outfd p2); Posix.IO.close (#infd p2))
+ (****** 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 *)
- (***************************************)
-
- (*************************)
- | NONE => let (* child - i.e. watcher *)
- val oldchildin = #infd p1 (*************************)
+ (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 _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
+ val pid = Posix.ProcEnv.getpid()
+ val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
+ (*set process group id: allows killing all children*)
+ val () = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
fun pollChildInput fromStr =
case getInIoDesc fromStr of
SOME iod =>
(case OS.IO.pollDesc iod of
SOME pd =>
- let val pd' = OS.IO.pollIn pd
- in
+ let val pd' = OS.IO.pollIn pd in
case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
[] => false
| pd''::_ => OS.IO.isIn pd''
@@ -287,7 +279,6 @@
| NONE => false)
| NONE => false
-
(* Check all ATP processes currently running for output *)
fun checkChildren ([], toParentStr) = [] (* no children to check *)
| checkChildren (childProc::otherChildren, toParentStr) =
@@ -295,8 +286,7 @@
Int.toString (length (childProc::otherChildren)))
val (childInput,childOutput) = cmdstreamsOf childProc
val child_handle = cmdchildHandle childProc
- (* childCmd is the file that the problem is in *)
- val childCmd = fst(snd (cmdchildInfo childProc))
+ val childCmd = #1(#2(cmdchildInfo childProc)) (*name of problem file*)
val _ = trace ("\nchildCmd = " ^ childCmd)
val sg_num = number_from_filename childCmd
val childIncoming = pollChildInput childInput
@@ -307,10 +297,8 @@
in
trace("\nsubgoals forked to checkChildren: " ^ goalstring);
if childIncoming
- then
- (* check here for prover label on child*)
- let val _ = trace ("\nInput available from child: " ^
- childCmd ^
+ then (* check here for prover label on child*)
+ let val _ = trace ("\nInput available from child: " ^ childCmd ^
"\ngoalstring is " ^ goalstring)
val childDone = (case prover of
"vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)
@@ -331,138 +319,90 @@
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 *)
- (********************************************************************)
-
-
-(*** add subgoal id num to this *)
- fun execCmds [] procList = procList
- | execCmds ((prover, goalstring,proverCmd,settings,file)::cmds) procList =
- let val _ = trace
- (space_implode "\n"
- (["\nAbout to execute command for goal:",
- goalstring, proverCmd] @ settings @
- [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
+ (* call resolution processes *)
+ (* settings should be a list of strings ["-t 300", "-m 100000"] *)
+ (* takes list of (string, string, string list, string)list proclist *)
+ fun execCmds [] procList = procList
+ | execCmds ((prover, goalstring,proverCmd,settings,file)::cmds) procList =
+ let val _ = trace (space_implode "\n"
+ (["\nAbout to execute command for goal:",
+ goalstring, proverCmd] @ settings @
+ [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc =
- (Unix.execute(proverCmd, (settings@[file])))
+ Unix.execute(proverCmd, settings@[file])
val (instr, outstr) = Unix.streamsOf childhandle
- val newProcList = (CMDPROC{
- prover = prover,
- cmd = file,
- goalstring = goalstring,
- proc_handle = childhandle,
- instr = instr,
- outstr = outstr }) :: procList
+ val newProcList = CMDPROC{prover = prover,
+ cmd = file,
+ goalstring = goalstring,
+ proc_handle = childhandle,
+ instr = instr,
+ outstr = outstr} :: procList
val _ = trace ("\nFinished at " ^
Date.toString(Date.fromTimeLocal(Time.now())))
in execCmds cmds newProcList end
-
- (****************************************)
- (* call resolution processes remotely *)
- (* settings should be a list of strings *)
- (* e.g. ["-t300", "-m100000"] *)
- (****************************************)
-
- (* fun execRemoteCmds [] procList = procList
- | execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList =
- let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
- in
- execRemoteCmds cmds newProcList
- end
-*)
-
- (**********************************************)
- (* Watcher Loop *)
- (**********************************************)
- val iterations_left = ref 500; (*don't let it run forever*)
+ (******** Watcher Loop ********)
+ val limit = ref 500; (*don't let it run forever*)
fun keepWatching (procList) =
let fun loop procList =
- let val _ = trace ("\nCalling pollParentInput: " ^
- Int.toString (!iterations_left));
- val cmdsFromIsa = pollParentInput
- (fromParentIOD, fromParentStr, toParentStr)
- in
- OS.Process.sleep (Time.fromMilliseconds 100);
- iterations_left := !iterations_left - 1;
- if !iterations_left <= 0
- then
- (trace "\nTimeout: Killing proof processes";
- TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
- TextIO.flushOut toParentStr;
- killChildren (map cmdchildHandle procList);
- exit 0)
- else if isSome cmdsFromIsa
- then (* deal with input from Isabelle *)
- if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children"
- then
+ let val _ = trace ("\nCalling pollParentInput: " ^ Int.toString (!limit));
+ val cmdsFromIsa = pollParentInput
+ (fromParentIOD, fromParentStr, toParentStr)
+ in
+ OS.Process.sleep (Time.fromMilliseconds 100);
+ limit := !limit - 1;
+ if !limit = 0
+ then
+ (trace "\nTimeout: Killing proof processes";
+ TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
+ TextIO.flushOut toParentStr;
+ killChildren (map cmdchildHandle procList);
+ exit 0)
+ else case cmdsFromIsa of
+ SOME [(_,_,"Kill children",_,_)] =>
let val child_handles = map cmdchildHandle procList
- in
- killChildren child_handles;
- loop []
- end
- else
- if length procList < 5 (********************)
+ in killChildren child_handles; loop [] end
+ | SOME cmds => (* deal with commands from Isabelle process *)
+ if length procList < 40
then (* Execute locally *)
let
- val newProcList = execCmds (valOf cmdsFromIsa) procList
- val _ = Posix.ProcEnv.getppid()
- val _ = trace "\nJust execed a child"
+ val newProcList = execCmds cmds procList
val newProcList' = checkChildren (newProcList, toParentStr)
in
- trace ("\nOff to keep watching: " ^
- Int.toString (!iterations_left));
- loop newProcList'
+ trace "\nJust execed a child"; loop newProcList'
end
- else (* Execute remotely *)
- (* (actually not remote for now )*)
+ else (* Execute remotely [FIXME: NOT REALLY] *)
let
- val newProcList = execCmds (valOf cmdsFromIsa) procList
- val _ = 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
- trace ("\nNo new input, still watching: " ^
- Int.toString (!iterations_left));
- loop newProcList
- end
- end
+ val newProcList = execCmds cmds procList
+ val newProcList' = checkChildren (newProcList, toParentStr)
+ in loop newProcList' end
+ | NONE => (* No new input from Isabelle *)
+ let val newProcList = checkChildren (procList, toParentStr)
+ in
+ trace "\nNo new input, still watching"; loop newProcList
+ end
+ end
in
loop procList
end
- in
- (***************************)
- (*** Sort out pipes ********)
- (***************************)
+ in
+ (*** Sort out pipes ********)
+ 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;
- 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 (procList);
- (****************************************************************************)
-(* fake return value - actually want the watcher to loop until killed *)
- (****************************************************************************)
- Posix.Process.wordToPid 0w0
- end);
+ (* start the watcher loop *)
+ keepWatching (procList);
+ (* fake return value - actually want the watcher to loop until killed *)
+ Posix.Process.wordToPid 0w0
+ end);
(* end case *)
@@ -503,9 +443,7 @@
(* Start a watcher and set up signal handlers *)
(**********************************************************)
-fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
-
-val killWatcher' = killWatcher o ResLib.pidOfInt;
+fun killWatcher pid = Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
fun reapWatcher(pid, instr, outstr) =
(TextIO.closeIn instr; TextIO.closeOut outstr;
--- a/src/HOL/Tools/res_atp.ML Wed Oct 05 10:56:06 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Wed Oct 05 11:18:06 2005 +0200
@@ -50,6 +50,8 @@
(* a special version of repeat_RS *)
fun repeat_someI_ex th = repeat_RS th someI_ex;
+fun writeln_strs _ [] = ()
+ | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
(* write out a subgoal as tptp clauses to the file "xxxx_N"*)
fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
@@ -61,8 +63,8 @@
val arity_cls = map ResClause.tptp_arity_clause arity_clauses
val out = TextIO.openOut(pf n)
in
- ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
- ResLib.writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
+ writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
+ writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
TextIO.closeOut out
end;
@@ -74,7 +76,7 @@
axclauses [] [] []
val out = TextIO.openOut(pf n)
in
- ResLib.writeln_strs out [probN]; TextIO.closeOut out
+ writeln_strs out [probN]; TextIO.closeOut out
end;
@@ -82,19 +84,20 @@
(* call prover with settings and problem file for the current subgoal *)
(*********************************************************************)
(* now passing in list of skolemized thms and list of sgterms to go with them *)
-fun watcher_call_provers sign sg_terms (childin, childout,pid) =
+fun watcher_call_provers sign sg_terms (childin, childout, pid) =
let
fun make_atp_list [] n = []
| make_atp_list (sg_term::xs) n =
let
val goalstring = Sign.string_of_term sign sg_term
- val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
val probfile = prob_pathname n
val time = Int.toString (!time_limit)
- val _ = debug ("problem file in watcher_call_provers is " ^ probfile)
in
+ debug ("goalstring in make_atp_lists is\n" ^ goalstring);
+ debug ("problem file in watcher_call_provers is " ^ probfile);
(*Avoid command arguments containing spaces: Poly/ML and SML/NJ
versions of Unix.execute treat them differently!*)
+ (*options are separated by Watcher.setting_sep, currently #"%"*)
if !prover = "spass"
then
let val optionline =
@@ -165,7 +168,8 @@
())
in writenext (length prems); clause_arr end;
-val last_watcher_pid = ref (NONE : Posix.Process.pid option);
+val last_watcher_pid =
+ ref (NONE : (TextIO.instream * TextIO.outstream * Posix.Process.pid) option);
(*writes out the current clasimpset to a tptp file;
@@ -175,8 +179,13 @@
if Thm.no_prems th then ()
else
let
+ val _ = (*Set up signal handler to tidy away dead processes*)
+ IsaSignal.signal (IsaSignal.chld,
+ IsaSignal.SIG_HANDLE (fn _ =>
+ (Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []);
+ debug "Child signal received\n")));
val _ = (case !last_watcher_pid of NONE => ()
- | SOME pid => (*FIXME: should kill ATP processes too; at least they time out*)
+ | SOME (_, childout, pid) =>
(debug ("Killing old watcher, pid = " ^
Int.toString (ResLib.intOfPid pid));
Watcher.killWatcher pid))
@@ -184,7 +193,7 @@
val clause_arr = write_problem_files prob_pathname (ctxt,th)
val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr)
in
- last_watcher_pid := SOME pid;
+ last_watcher_pid := SOME (childin, childout, pid);
debug ("proof state: " ^ string_of_thm th);
debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
@@ -208,9 +217,9 @@
handle Proof.STATE _ => error "No goal present";
val thy = ProofContext.theory_of ctxt;
in
- debug ("initial thm in isar_atp: " ^
+ debug ("initial thm in isar_atp:\n" ^
Pretty.string_of (ProofContext.pretty_thm ctxt goal));
- debug ("subgoals in isar_atp: " ^
+ debug ("subgoals in isar_atp:\n" ^
Pretty.string_of (ProofContext.pretty_term ctxt
(Logic.mk_conjunction_list (Thm.prems_of goal))));
debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal));
--- a/src/HOL/Tools/res_clause.ML Wed Oct 05 10:56:06 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML Wed Oct 05 11:18:06 2005 +0200
@@ -32,7 +32,6 @@
val isTaut : clause -> bool
val num_of_clauses : clause -> int
- val dfg_clauses2str : string list -> string
val clause2dfg : clause -> string * string list
val clauses2dfg : clause list -> string -> clause list -> clause list ->
(string * int) list -> (string * int) list -> string
@@ -41,7 +40,6 @@
val tptp_arity_clause : arityClause -> string
val tptp_classrelClause : classrelClause -> string
val tptp_clause : clause -> string list
- val tptp_clauses2str : string list -> string
val clause2tptp : clause -> string * string list
val tfree_clause : string -> string
val schematic_var_prefix : string
@@ -293,11 +291,11 @@
val funcs' = ResLib.flat_noDup funcslist
val t = make_fixed_type_const a
in
- ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs') )
+ ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs'))
end
| type_of (TFree (a, s)) =
let val t = make_fixed_type_var a
- in (t, ([((FOLTFree a),s)],[(t,0)]) ) end
+ in (t, ([((FOLTFree a),s)],[(t,0)])) end
| type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], []))
@@ -617,7 +615,7 @@
val conclLit = make_TConsLit(true,(res,tcons,tvars))
val tvars_srts = ListPair.zip (tvars,args)
val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts)
- val false_tvars_srts' = ResLib.pair_ins false tvars_srts'
+ val false_tvars_srts' = map (pair false) tvars_srts'
val premLits = map make_TVarLit false_tvars_srts'
in
make_arity_clause (cls_id,Axiom,conclLit,premLits)
@@ -773,7 +771,7 @@
| uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT));
fun mergelist [] = []
-| mergelist (x::xs ) = x @ mergelist xs
+| mergelist (x::xs) = x @ mergelist xs
fun dfg_vars (Clause cls) =
let val lits = #literals cls
@@ -861,9 +859,6 @@
fun string_of_end () = "end_problem.\n%------------------------------------------------------------------------------";
-val delim = "\n";
-val dfg_clauses2str = ResLib.list2str_sep delim;
-
fun clause2dfg cls =
let val (lits,tfree_lits) = dfg_clause_aux cls
@@ -890,16 +885,16 @@
fun gen_dfg_file probname axioms conjectures funcs preds =
let val axstrs_tfrees = (map clause2dfg axioms)
val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
- val axstr = ResLib.list2str_sep delim axstrs
+ val axstr = (space_implode "\n" axstrs) ^ "\n\n"
val conjstrs_tfrees = (map clause2dfg conjectures)
val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
val tfree_clss = map tfree_dfg_clause (ResLib.flat_noDup atfrees)
- val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs)
+ val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n"
val funcstr = string_of_funcs funcs
val predstr = string_of_preds preds
in
(string_of_start probname) ^ (string_of_descrip ()) ^
- (string_of_symbols funcstr predstr ) ^
+ (string_of_symbols funcstr predstr) ^
(string_of_axioms axstr) ^
(string_of_conjectures conjstr) ^ (string_of_end ())
end;
@@ -1042,9 +1037,6 @@
fun tfree_clause tfree_lit =
"input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).";
-val delim = "\n";
-val tptp_clauses2str = ResLib.list2str_sep delim;
-
fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
let val pol = if b then "++" else "--"
--- a/src/HOL/Tools/res_lib.ML Wed Oct 05 10:56:06 2005 +0200
+++ b/src/HOL/Tools/res_lib.ML Wed Oct 05 11:18:06 2005 +0200
@@ -10,12 +10,8 @@
sig
val flat_noDup : ''a list list -> ''a list
val helper_path : string -> string -> string
-val list2str_sep : string -> string list -> string
val no_rep_add : ''a -> ''a list -> ''a list
val no_rep_app : ''a list -> ''a list -> ''a list
-val pair_ins : 'a -> 'b list -> ('a * 'b) list
-val write_strs : TextIO.outstream -> TextIO.vector list -> unit
-val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
val intOfPid : Posix.Process.pid -> Int.int
val pidOfInt : Int.int -> Posix.Process.pid
end;
@@ -33,19 +29,7 @@
fun flat_noDup [] = []
| flat_noDup (x::y) = no_rep_app x (flat_noDup y);
-fun list2str_sep delim [] = delim
- | list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss);
-
-fun write_strs _ [] = ()
- | write_strs out (s::ss) = (TextIO.output (out, s); write_strs out ss);
-
-fun writeln_strs _ [] = ()
- | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
-
-(* pair the first argument with each element in the second input list *)
-fun pair_ins x [] = []
- | pair_ins x (y::ys) = (x, y) :: (pair_ins x ys);
-
+
(*Return the path to a "helper" like SPASS or tptp2X, first checking that
it exists. --lcp *)
fun helper_path evar base =