# HG changeset patch # User paulson # Date 1128503886 -7200 # Node ID fde495b9e24bfaf963f13399bcc71b0f85e61cb9 # Parent 6f933b702f44a4d4b5b6bca0e40817625b968f51 improved process handling. tidied diff -r 6f933b702f44 -r fde495b9e24b src/HOL/Tools/ATP/res_clasimpset.ML --- 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)) diff -r 6f933b702f44 -r fde495b9e24b src/HOL/Tools/ATP/watcher.ML --- 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; diff -r 6f933b702f44 -r fde495b9e24b src/HOL/Tools/res_atp.ML --- 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)); diff -r 6f933b702f44 -r fde495b9e24b src/HOL/Tools/res_clause.ML --- 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 "--" diff -r 6f933b702f44 -r fde495b9e24b src/HOL/Tools/res_lib.ML --- 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 =