improved process handling. tidied
1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML Wed Oct 05 10:56:06 2005 +0200
1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Wed Oct 05 11:18:06 2005 +0200
1.3 @@ -68,7 +68,7 @@
1.4 let val consts = consts_in_goal goal
1.5 fun relevant_axioms_aux1 cs k =
1.6 let val thms1 = axioms_having_consts cs thmTab
1.7 - val cs1 = ResLib.flat_noDup (map consts_of_thm thms1)
1.8 + val cs1 = foldl (op union_string) [] (map consts_of_thm thms1)
1.9 in
1.10 if ((cs1 subset cs) orelse n <= k) then (k,thms1)
1.11 else (relevant_axioms_aux1 (cs1 union cs) (k+1))
2.1 --- a/src/HOL/Tools/ATP/watcher.ML Wed Oct 05 10:56:06 2005 +0200
2.2 +++ b/src/HOL/Tools/ATP/watcher.ML Wed Oct 05 11:18:06 2005 +0200
2.3 @@ -4,14 +4,11 @@
2.4 Copyright 2004 University of Cambridge
2.5 *)
2.6
2.7 - (***************************************************************************)
2.8 - (* The watcher process starts a resolution process when it receives a *)
2.9 +(* The watcher process starts a resolution process when it receives a *)
2.10 (* message from Isabelle *)
2.11 (* Signals Isabelle, puts output of child into pipe to Isabelle, *)
2.12 (* and removes dead processes. Also possible to kill all the resolution *)
2.13 (* processes currently running. *)
2.14 -(* Hardwired version of where to pick up the tptp files for the moment *)
2.15 -(***************************************************************************)
2.16
2.17 signature WATCHER =
2.18 sig
2.19 @@ -23,17 +20,15 @@
2.20 TextIO.outstream * (string*string*string*string*string) list
2.21 -> unit
2.22
2.23 -(* Send message to watcher to kill currently running resolution provers *)
2.24 +(* Send message to watcher to kill resolution provers *)
2.25 val callSlayer : TextIO.outstream -> unit
2.26
2.27 (* Start a watcher and set up signal handlers *)
2.28 val createWatcher :
2.29 thm * (ResClause.clause * thm) Array.array ->
2.30 TextIO.instream * TextIO.outstream * Posix.Process.pid
2.31 -
2.32 -(* Kill watcher process *)
2.33 val killWatcher : Posix.Process.pid -> unit
2.34 -val killWatcher' : int -> unit
2.35 +val setting_sep : char
2.36 end
2.37
2.38
2.39 @@ -41,6 +36,10 @@
2.40 structure Watcher: WATCHER =
2.41 struct
2.42
2.43 +(*Field separators, used to pack items onto a text line*)
2.44 +val command_sep = #"\t"
2.45 +and setting_sep = #"%";
2.46 +
2.47 open Recon_Transfer
2.48
2.49 val goals_being_watched = ref 0;
2.50 @@ -134,8 +133,6 @@
2.51 (* need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
2.52 (*****************************************************************************************)
2.53
2.54 -
2.55 -(*Uses the $-character to separate items sent to watcher*)
2.56 fun callResProvers (toWatcherStr, []) =
2.57 (TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr)
2.58 | callResProvers (toWatcherStr,
2.59 @@ -144,9 +141,11 @@
2.60 let val _ = trace (space_implode "\n"
2.61 (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
2.62 probfile]))
2.63 - in TextIO.output (toWatcherStr,
2.64 - prover^"$"^proverCmd^"$"^ settings^"$"^probfile^"$\n");
2.65 - TextIO.output (toWatcherStr, String.toString goalstring^"\n");
2.66 + in TextIO.output (toWatcherStr,
2.67 + (*Uses a special character to separate items sent to watcher*)
2.68 + space_implode (str command_sep)
2.69 + [prover, proverCmd, settings, probfile,
2.70 + String.toString goalstring ^ "\n"]);
2.71 (*goalstring is a single string literal, with all specials escaped.*)
2.72 goals_being_watched := (!goals_being_watched) + 1;
2.73 TextIO.flushOut toWatcherStr;
2.74 @@ -155,31 +154,29 @@
2.75
2.76
2.77
2.78 -(**************************************************************)
2.79 -(* Send message to watcher to kill currently running vampires *)
2.80 -(**************************************************************)
2.81
2.82 -fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n");
2.83 +(*Send message to watcher to kill currently running vampires. NOT USED and possibly
2.84 + buggy. Note that killWatcher kills the entire process group anyway.*)
2.85 +fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
2.86 TextIO.flushOut toWatcherStr)
2.87
2.88
2.89 (**************************************************************)
2.90 (* Get commands from Isabelle *)
2.91 (**************************************************************)
2.92 -fun getCmds (toParentStr,fromParentStr, cmdList) =
2.93 +fun getCmds (toParentStr, fromParentStr, cmdList) =
2.94 let val thisLine = TextIO.inputLine fromParentStr
2.95 - val _ = trace("\nGot command from parent: " ^ thisLine)
2.96 in
2.97 + trace("\nGot command from parent: " ^ thisLine);
2.98 if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
2.99 else if thisLine = "Kill children\n"
2.100 - then (TextIO.output (toParentStr,thisLine );
2.101 + then (TextIO.output (toParentStr,thisLine);
2.102 TextIO.flushOut toParentStr;
2.103 - (("","","Kill children",[],"")::cmdList) )
2.104 + [("","","Kill children",[],"")])
2.105 else
2.106 - let val [prover,proverCmd,settingstr,probfile,_] =
2.107 - String.tokens (fn c => c = #"$") thisLine
2.108 - val settings = String.tokens (fn c => c = #"%") settingstr
2.109 - val goalstring = TextIO.inputLine fromParentStr
2.110 + let val [prover,proverCmd,settingstr,probfile,goalstring] =
2.111 + String.tokens (fn c => c = command_sep) thisLine
2.112 + val settings = String.tokens (fn c => c = setting_sep) settingstr
2.113 in
2.114 trace ("\nprover: " ^ prover ^ " prover path: " ^ proverCmd^
2.115 " problem file: " ^ probfile ^
2.116 @@ -187,6 +184,9 @@
2.117 getCmds (toParentStr, fromParentStr,
2.118 (prover, goalstring, proverCmd, settings, probfile)::cmdList)
2.119 end
2.120 + handle Bind =>
2.121 + (trace "getCmds: command parsing failed!";
2.122 + getCmds (toParentStr, fromParentStr, cmdList))
2.123 end
2.124
2.125
2.126 @@ -212,8 +212,6 @@
2.127 (* Set up a Watcher Process *)
2.128 (*************************************)
2.129
2.130 -fun getProofCmd (a,c,d,e,f) = d
2.131 -
2.132 (* for tracing: encloses each string element in brackets. *)
2.133 val concat_with_and = space_implode " & " o map (enclose "(" ")");
2.134
2.135 @@ -246,40 +244,34 @@
2.136
2.137 fun setupWatcher (thm,clause_arr) =
2.138 let
2.139 - (** pipes for communication between parent and watcher **)
2.140 - val p1 = Posix.IO.pipe ()
2.141 + val p1 = Posix.IO.pipe () (** pipes for communication between parent and watcher **)
2.142 val p2 = Posix.IO.pipe ()
2.143 fun closep () =
2.144 - (Posix.IO.close (#outfd p1);
2.145 - Posix.IO.close (#infd p1);
2.146 - Posix.IO.close (#outfd p2);
2.147 - Posix.IO.close (#infd p2))
2.148 - (***********************************************************)
2.149 - (****** fork a watcher process and get it set up and going *)
2.150 - (***********************************************************)
2.151 + (Posix.IO.close (#outfd p1); Posix.IO.close (#infd p1);
2.152 + Posix.IO.close (#outfd p2); Posix.IO.close (#infd p2))
2.153 + (****** fork a watcher process and get it set up and going ******)
2.154 fun startWatcher procList =
2.155 - (case Posix.Process.fork() (***************************************)
2.156 - of SOME pid => pid (* parent - i.e. main Isabelle process *)
2.157 - (***************************************)
2.158 -
2.159 - (*************************)
2.160 - | NONE => let (* child - i.e. watcher *)
2.161 - val oldchildin = #infd p1 (*************************)
2.162 + (case Posix.Process.fork()
2.163 + of SOME pid => pid (* parent - i.e. main Isabelle process *)
2.164 + | NONE => let (* child - i.e. watcher *)
2.165 + val oldchildin = #infd p1
2.166 val fromParent = Posix.FileSys.wordToFD 0w0
2.167 val oldchildout = #outfd p2
2.168 val toParent = Posix.FileSys.wordToFD 0w1
2.169 val fromParentIOD = Posix.FileSys.fdToIOD fromParent
2.170 val fromParentStr = openInFD ("_exec_in_parent", fromParent)
2.171 val toParentStr = openOutFD ("_exec_out_parent", toParent)
2.172 - val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
2.173 + val pid = Posix.ProcEnv.getpid()
2.174 + val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
2.175 + (*set process group id: allows killing all children*)
2.176 + val () = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
2.177
2.178 fun pollChildInput fromStr =
2.179 case getInIoDesc fromStr of
2.180 SOME iod =>
2.181 (case OS.IO.pollDesc iod of
2.182 SOME pd =>
2.183 - let val pd' = OS.IO.pollIn pd
2.184 - in
2.185 + let val pd' = OS.IO.pollIn pd in
2.186 case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
2.187 [] => false
2.188 | pd''::_ => OS.IO.isIn pd''
2.189 @@ -287,7 +279,6 @@
2.190 | NONE => false)
2.191 | NONE => false
2.192
2.193 -
2.194 (* Check all ATP processes currently running for output *)
2.195 fun checkChildren ([], toParentStr) = [] (* no children to check *)
2.196 | checkChildren (childProc::otherChildren, toParentStr) =
2.197 @@ -295,8 +286,7 @@
2.198 Int.toString (length (childProc::otherChildren)))
2.199 val (childInput,childOutput) = cmdstreamsOf childProc
2.200 val child_handle = cmdchildHandle childProc
2.201 - (* childCmd is the file that the problem is in *)
2.202 - val childCmd = fst(snd (cmdchildInfo childProc))
2.203 + val childCmd = #1(#2(cmdchildInfo childProc)) (*name of problem file*)
2.204 val _ = trace ("\nchildCmd = " ^ childCmd)
2.205 val sg_num = number_from_filename childCmd
2.206 val childIncoming = pollChildInput childInput
2.207 @@ -307,10 +297,8 @@
2.208 in
2.209 trace("\nsubgoals forked to checkChildren: " ^ goalstring);
2.210 if childIncoming
2.211 - then
2.212 - (* check here for prover label on child*)
2.213 - let val _ = trace ("\nInput available from child: " ^
2.214 - childCmd ^
2.215 + then (* check here for prover label on child*)
2.216 + let val _ = trace ("\nInput available from child: " ^ childCmd ^
2.217 "\ngoalstring is " ^ goalstring)
2.218 val childDone = (case prover of
2.219 "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)
2.220 @@ -331,138 +319,90 @@
2.221 end
2.222
2.223
2.224 - (********************************************************************)
2.225 - (* call resolution processes *)
2.226 - (* settings should be a list of strings *)
2.227 - (* e.g. ["-t 300", "-m 100000"] (TextIO.input instr)^ *)
2.228 - (* takes list of (string, string, string list, string)list proclist *)
2.229 - (********************************************************************)
2.230 -
2.231 -
2.232 -(*** add subgoal id num to this *)
2.233 - fun execCmds [] procList = procList
2.234 - | execCmds ((prover, goalstring,proverCmd,settings,file)::cmds) procList =
2.235 - let val _ = trace
2.236 - (space_implode "\n"
2.237 - (["\nAbout to execute command for goal:",
2.238 - goalstring, proverCmd] @ settings @
2.239 - [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
2.240 + (* call resolution processes *)
2.241 + (* settings should be a list of strings ["-t 300", "-m 100000"] *)
2.242 + (* takes list of (string, string, string list, string)list proclist *)
2.243 + fun execCmds [] procList = procList
2.244 + | execCmds ((prover, goalstring,proverCmd,settings,file)::cmds) procList =
2.245 + let val _ = trace (space_implode "\n"
2.246 + (["\nAbout to execute command for goal:",
2.247 + goalstring, proverCmd] @ settings @
2.248 + [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
2.249 val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc =
2.250 - (Unix.execute(proverCmd, (settings@[file])))
2.251 + Unix.execute(proverCmd, settings@[file])
2.252 val (instr, outstr) = Unix.streamsOf childhandle
2.253 - val newProcList = (CMDPROC{
2.254 - prover = prover,
2.255 - cmd = file,
2.256 - goalstring = goalstring,
2.257 - proc_handle = childhandle,
2.258 - instr = instr,
2.259 - outstr = outstr }) :: procList
2.260 + val newProcList = CMDPROC{prover = prover,
2.261 + cmd = file,
2.262 + goalstring = goalstring,
2.263 + proc_handle = childhandle,
2.264 + instr = instr,
2.265 + outstr = outstr} :: procList
2.266
2.267 val _ = trace ("\nFinished at " ^
2.268 Date.toString(Date.fromTimeLocal(Time.now())))
2.269 in execCmds cmds newProcList end
2.270
2.271 -
2.272 - (****************************************)
2.273 - (* call resolution processes remotely *)
2.274 - (* settings should be a list of strings *)
2.275 - (* e.g. ["-t300", "-m100000"] *)
2.276 - (****************************************)
2.277 -
2.278 - (* fun execRemoteCmds [] procList = procList
2.279 - | execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList =
2.280 - let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
2.281 - in
2.282 - execRemoteCmds cmds newProcList
2.283 - end
2.284 -*)
2.285 -
2.286 - (**********************************************)
2.287 - (* Watcher Loop *)
2.288 - (**********************************************)
2.289 - val iterations_left = ref 500; (*don't let it run forever*)
2.290 + (******** Watcher Loop ********)
2.291 + val limit = ref 500; (*don't let it run forever*)
2.292
2.293 fun keepWatching (procList) =
2.294 let fun loop procList =
2.295 - let val _ = trace ("\nCalling pollParentInput: " ^
2.296 - Int.toString (!iterations_left));
2.297 - val cmdsFromIsa = pollParentInput
2.298 - (fromParentIOD, fromParentStr, toParentStr)
2.299 - in
2.300 - OS.Process.sleep (Time.fromMilliseconds 100);
2.301 - iterations_left := !iterations_left - 1;
2.302 - if !iterations_left <= 0
2.303 - then
2.304 - (trace "\nTimeout: Killing proof processes";
2.305 - TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
2.306 - TextIO.flushOut toParentStr;
2.307 - killChildren (map cmdchildHandle procList);
2.308 - exit 0)
2.309 - else if isSome cmdsFromIsa
2.310 - then (* deal with input from Isabelle *)
2.311 - if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children"
2.312 - then
2.313 + let val _ = trace ("\nCalling pollParentInput: " ^ Int.toString (!limit));
2.314 + val cmdsFromIsa = pollParentInput
2.315 + (fromParentIOD, fromParentStr, toParentStr)
2.316 + in
2.317 + OS.Process.sleep (Time.fromMilliseconds 100);
2.318 + limit := !limit - 1;
2.319 + if !limit = 0
2.320 + then
2.321 + (trace "\nTimeout: Killing proof processes";
2.322 + TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
2.323 + TextIO.flushOut toParentStr;
2.324 + killChildren (map cmdchildHandle procList);
2.325 + exit 0)
2.326 + else case cmdsFromIsa of
2.327 + SOME [(_,_,"Kill children",_,_)] =>
2.328 let val child_handles = map cmdchildHandle procList
2.329 - in
2.330 - killChildren child_handles;
2.331 - loop []
2.332 - end
2.333 - else
2.334 - if length procList < 5 (********************)
2.335 + in killChildren child_handles; loop [] end
2.336 + | SOME cmds => (* deal with commands from Isabelle process *)
2.337 + if length procList < 40
2.338 then (* Execute locally *)
2.339 let
2.340 - val newProcList = execCmds (valOf cmdsFromIsa) procList
2.341 - val _ = Posix.ProcEnv.getppid()
2.342 - val _ = trace "\nJust execed a child"
2.343 + val newProcList = execCmds cmds procList
2.344 val newProcList' = checkChildren (newProcList, toParentStr)
2.345 in
2.346 - trace ("\nOff to keep watching: " ^
2.347 - Int.toString (!iterations_left));
2.348 - loop newProcList'
2.349 + trace "\nJust execed a child"; loop newProcList'
2.350 end
2.351 - else (* Execute remotely *)
2.352 - (* (actually not remote for now )*)
2.353 + else (* Execute remotely [FIXME: NOT REALLY] *)
2.354 let
2.355 - val newProcList = execCmds (valOf cmdsFromIsa) procList
2.356 - val _ = Posix.ProcEnv.getppid()
2.357 - val newProcList' =checkChildren (newProcList, toParentStr)
2.358 - in
2.359 - loop newProcList'
2.360 - end
2.361 - else (* No new input from Isabelle *)
2.362 - let val newProcList = checkChildren (procList, toParentStr)
2.363 - in
2.364 - trace ("\nNo new input, still watching: " ^
2.365 - Int.toString (!iterations_left));
2.366 - loop newProcList
2.367 - end
2.368 - end
2.369 + val newProcList = execCmds cmds procList
2.370 + val newProcList' = checkChildren (newProcList, toParentStr)
2.371 + in loop newProcList' end
2.372 + | NONE => (* No new input from Isabelle *)
2.373 + let val newProcList = checkChildren (procList, toParentStr)
2.374 + in
2.375 + trace "\nNo new input, still watching"; loop newProcList
2.376 + end
2.377 + end
2.378 in
2.379 loop procList
2.380 end
2.381
2.382
2.383 - in
2.384 - (***************************)
2.385 - (*** Sort out pipes ********)
2.386 - (***************************)
2.387 + in
2.388 + (*** Sort out pipes ********)
2.389 + Posix.IO.close (#outfd p1);
2.390 + Posix.IO.close (#infd p2);
2.391 + Posix.IO.dup2{old = oldchildin, new = fromParent};
2.392 + Posix.IO.close oldchildin;
2.393 + Posix.IO.dup2{old = oldchildout, new = toParent};
2.394 + Posix.IO.close oldchildout;
2.395
2.396 - Posix.IO.close (#outfd p1);
2.397 - Posix.IO.close (#infd p2);
2.398 - Posix.IO.dup2{old = oldchildin, new = fromParent};
2.399 - Posix.IO.close oldchildin;
2.400 - Posix.IO.dup2{old = oldchildout, new = toParent};
2.401 - Posix.IO.close oldchildout;
2.402 -
2.403 - (***************************)
2.404 - (* start the watcher loop *)
2.405 - (***************************)
2.406 - keepWatching (procList);
2.407 - (****************************************************************************)
2.408 -(* fake return value - actually want the watcher to loop until killed *)
2.409 - (****************************************************************************)
2.410 - Posix.Process.wordToPid 0w0
2.411 - end);
2.412 + (* start the watcher loop *)
2.413 + keepWatching (procList);
2.414 + (* fake return value - actually want the watcher to loop until killed *)
2.415 + Posix.Process.wordToPid 0w0
2.416 + end);
2.417 (* end case *)
2.418
2.419
2.420 @@ -503,9 +443,7 @@
2.421 (* Start a watcher and set up signal handlers *)
2.422 (**********************************************************)
2.423
2.424 -fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
2.425 -
2.426 -val killWatcher' = killWatcher o ResLib.pidOfInt;
2.427 +fun killWatcher pid = Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
2.428
2.429 fun reapWatcher(pid, instr, outstr) =
2.430 (TextIO.closeIn instr; TextIO.closeOut outstr;
3.1 --- a/src/HOL/Tools/res_atp.ML Wed Oct 05 10:56:06 2005 +0200
3.2 +++ b/src/HOL/Tools/res_atp.ML Wed Oct 05 11:18:06 2005 +0200
3.3 @@ -50,6 +50,8 @@
3.4 (* a special version of repeat_RS *)
3.5 fun repeat_someI_ex th = repeat_RS th someI_ex;
3.6
3.7 +fun writeln_strs _ [] = ()
3.8 + | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
3.9
3.10 (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
3.11 fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
3.12 @@ -61,8 +63,8 @@
3.13 val arity_cls = map ResClause.tptp_arity_clause arity_clauses
3.14 val out = TextIO.openOut(pf n)
3.15 in
3.16 - ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
3.17 - ResLib.writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
3.18 + writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
3.19 + writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
3.20 TextIO.closeOut out
3.21 end;
3.22
3.23 @@ -74,7 +76,7 @@
3.24 axclauses [] [] []
3.25 val out = TextIO.openOut(pf n)
3.26 in
3.27 - ResLib.writeln_strs out [probN]; TextIO.closeOut out
3.28 + writeln_strs out [probN]; TextIO.closeOut out
3.29 end;
3.30
3.31
3.32 @@ -82,19 +84,20 @@
3.33 (* call prover with settings and problem file for the current subgoal *)
3.34 (*********************************************************************)
3.35 (* now passing in list of skolemized thms and list of sgterms to go with them *)
3.36 -fun watcher_call_provers sign sg_terms (childin, childout,pid) =
3.37 +fun watcher_call_provers sign sg_terms (childin, childout, pid) =
3.38 let
3.39 fun make_atp_list [] n = []
3.40 | make_atp_list (sg_term::xs) n =
3.41 let
3.42 val goalstring = Sign.string_of_term sign sg_term
3.43 - val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
3.44 val probfile = prob_pathname n
3.45 val time = Int.toString (!time_limit)
3.46 - val _ = debug ("problem file in watcher_call_provers is " ^ probfile)
3.47 in
3.48 + debug ("goalstring in make_atp_lists is\n" ^ goalstring);
3.49 + debug ("problem file in watcher_call_provers is " ^ probfile);
3.50 (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
3.51 versions of Unix.execute treat them differently!*)
3.52 + (*options are separated by Watcher.setting_sep, currently #"%"*)
3.53 if !prover = "spass"
3.54 then
3.55 let val optionline =
3.56 @@ -165,7 +168,8 @@
3.57 ())
3.58 in writenext (length prems); clause_arr end;
3.59
3.60 -val last_watcher_pid = ref (NONE : Posix.Process.pid option);
3.61 +val last_watcher_pid =
3.62 + ref (NONE : (TextIO.instream * TextIO.outstream * Posix.Process.pid) option);
3.63
3.64
3.65 (*writes out the current clasimpset to a tptp file;
3.66 @@ -175,8 +179,13 @@
3.67 if Thm.no_prems th then ()
3.68 else
3.69 let
3.70 + val _ = (*Set up signal handler to tidy away dead processes*)
3.71 + IsaSignal.signal (IsaSignal.chld,
3.72 + IsaSignal.SIG_HANDLE (fn _ =>
3.73 + (Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []);
3.74 + debug "Child signal received\n")));
3.75 val _ = (case !last_watcher_pid of NONE => ()
3.76 - | SOME pid => (*FIXME: should kill ATP processes too; at least they time out*)
3.77 + | SOME (_, childout, pid) =>
3.78 (debug ("Killing old watcher, pid = " ^
3.79 Int.toString (ResLib.intOfPid pid));
3.80 Watcher.killWatcher pid))
3.81 @@ -184,7 +193,7 @@
3.82 val clause_arr = write_problem_files prob_pathname (ctxt,th)
3.83 val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr)
3.84 in
3.85 - last_watcher_pid := SOME pid;
3.86 + last_watcher_pid := SOME (childin, childout, pid);
3.87 debug ("proof state: " ^ string_of_thm th);
3.88 debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
3.89 watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
3.90 @@ -208,9 +217,9 @@
3.91 handle Proof.STATE _ => error "No goal present";
3.92 val thy = ProofContext.theory_of ctxt;
3.93 in
3.94 - debug ("initial thm in isar_atp: " ^
3.95 + debug ("initial thm in isar_atp:\n" ^
3.96 Pretty.string_of (ProofContext.pretty_thm ctxt goal));
3.97 - debug ("subgoals in isar_atp: " ^
3.98 + debug ("subgoals in isar_atp:\n" ^
3.99 Pretty.string_of (ProofContext.pretty_term ctxt
3.100 (Logic.mk_conjunction_list (Thm.prems_of goal))));
3.101 debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal));
4.1 --- a/src/HOL/Tools/res_clause.ML Wed Oct 05 10:56:06 2005 +0200
4.2 +++ b/src/HOL/Tools/res_clause.ML Wed Oct 05 11:18:06 2005 +0200
4.3 @@ -32,7 +32,6 @@
4.4 val isTaut : clause -> bool
4.5 val num_of_clauses : clause -> int
4.6
4.7 - val dfg_clauses2str : string list -> string
4.8 val clause2dfg : clause -> string * string list
4.9 val clauses2dfg : clause list -> string -> clause list -> clause list ->
4.10 (string * int) list -> (string * int) list -> string
4.11 @@ -41,7 +40,6 @@
4.12 val tptp_arity_clause : arityClause -> string
4.13 val tptp_classrelClause : classrelClause -> string
4.14 val tptp_clause : clause -> string list
4.15 - val tptp_clauses2str : string list -> string
4.16 val clause2tptp : clause -> string * string list
4.17 val tfree_clause : string -> string
4.18 val schematic_var_prefix : string
4.19 @@ -293,11 +291,11 @@
4.20 val funcs' = ResLib.flat_noDup funcslist
4.21 val t = make_fixed_type_const a
4.22 in
4.23 - ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs') )
4.24 + ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs'))
4.25 end
4.26 | type_of (TFree (a, s)) =
4.27 let val t = make_fixed_type_var a
4.28 - in (t, ([((FOLTFree a),s)],[(t,0)]) ) end
4.29 + in (t, ([((FOLTFree a),s)],[(t,0)])) end
4.30 | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], []))
4.31
4.32
4.33 @@ -617,7 +615,7 @@
4.34 val conclLit = make_TConsLit(true,(res,tcons,tvars))
4.35 val tvars_srts = ListPair.zip (tvars,args)
4.36 val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts)
4.37 - val false_tvars_srts' = ResLib.pair_ins false tvars_srts'
4.38 + val false_tvars_srts' = map (pair false) tvars_srts'
4.39 val premLits = map make_TVarLit false_tvars_srts'
4.40 in
4.41 make_arity_clause (cls_id,Axiom,conclLit,premLits)
4.42 @@ -773,7 +771,7 @@
4.43 | uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT));
4.44
4.45 fun mergelist [] = []
4.46 -| mergelist (x::xs ) = x @ mergelist xs
4.47 +| mergelist (x::xs) = x @ mergelist xs
4.48
4.49 fun dfg_vars (Clause cls) =
4.50 let val lits = #literals cls
4.51 @@ -861,9 +859,6 @@
4.52
4.53 fun string_of_end () = "end_problem.\n%------------------------------------------------------------------------------";
4.54
4.55 -val delim = "\n";
4.56 -val dfg_clauses2str = ResLib.list2str_sep delim;
4.57 -
4.58
4.59 fun clause2dfg cls =
4.60 let val (lits,tfree_lits) = dfg_clause_aux cls
4.61 @@ -890,16 +885,16 @@
4.62 fun gen_dfg_file probname axioms conjectures funcs preds =
4.63 let val axstrs_tfrees = (map clause2dfg axioms)
4.64 val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
4.65 - val axstr = ResLib.list2str_sep delim axstrs
4.66 + val axstr = (space_implode "\n" axstrs) ^ "\n\n"
4.67 val conjstrs_tfrees = (map clause2dfg conjectures)
4.68 val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
4.69 val tfree_clss = map tfree_dfg_clause (ResLib.flat_noDup atfrees)
4.70 - val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs)
4.71 + val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n"
4.72 val funcstr = string_of_funcs funcs
4.73 val predstr = string_of_preds preds
4.74 in
4.75 (string_of_start probname) ^ (string_of_descrip ()) ^
4.76 - (string_of_symbols funcstr predstr ) ^
4.77 + (string_of_symbols funcstr predstr) ^
4.78 (string_of_axioms axstr) ^
4.79 (string_of_conjectures conjstr) ^ (string_of_end ())
4.80 end;
4.81 @@ -1042,9 +1037,6 @@
4.82 fun tfree_clause tfree_lit =
4.83 "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).";
4.84
4.85 -val delim = "\n";
4.86 -val tptp_clauses2str = ResLib.list2str_sep delim;
4.87 -
4.88
4.89 fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
4.90 let val pol = if b then "++" else "--"
5.1 --- a/src/HOL/Tools/res_lib.ML Wed Oct 05 10:56:06 2005 +0200
5.2 +++ b/src/HOL/Tools/res_lib.ML Wed Oct 05 11:18:06 2005 +0200
5.3 @@ -10,12 +10,8 @@
5.4 sig
5.5 val flat_noDup : ''a list list -> ''a list
5.6 val helper_path : string -> string -> string
5.7 -val list2str_sep : string -> string list -> string
5.8 val no_rep_add : ''a -> ''a list -> ''a list
5.9 val no_rep_app : ''a list -> ''a list -> ''a list
5.10 -val pair_ins : 'a -> 'b list -> ('a * 'b) list
5.11 -val write_strs : TextIO.outstream -> TextIO.vector list -> unit
5.12 -val writeln_strs : TextIO.outstream -> TextIO.vector list -> unit
5.13 val intOfPid : Posix.Process.pid -> Int.int
5.14 val pidOfInt : Int.int -> Posix.Process.pid
5.15 end;
5.16 @@ -33,19 +29,7 @@
5.17 fun flat_noDup [] = []
5.18 | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
5.19
5.20 -fun list2str_sep delim [] = delim
5.21 - | list2str_sep delim (s::ss) = (s ^ delim) ^ (list2str_sep delim ss);
5.22 -
5.23 -fun write_strs _ [] = ()
5.24 - | write_strs out (s::ss) = (TextIO.output (out, s); write_strs out ss);
5.25 -
5.26 -fun writeln_strs _ [] = ()
5.27 - | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
5.28 -
5.29 -(* pair the first argument with each element in the second input list *)
5.30 -fun pair_ins x [] = []
5.31 - | pair_ins x (y::ys) = (x, y) :: (pair_ins x ys);
5.32 -
5.33 +
5.34 (*Return the path to a "helper" like SPASS or tptp2X, first checking that
5.35 it exists. --lcp *)
5.36 fun helper_path evar base =