# HG changeset patch # User paulson # Date 1183134085 -7200 # Node ID a4ffa756d8eb02c7ec0287d2ea1fb465ae2b249a # Parent 6407d832da037142b7b1548e52b5cc69914fcd1a bug fixes to proof reconstruction diff -r 6407d832da03 -r a4ffa756d8eb src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Fri Jun 29 16:05:00 2007 +0200 +++ b/src/HOL/ATP_Linkup.thy Fri Jun 29 18:21:25 2007 +0200 @@ -15,7 +15,7 @@ ("Tools/res_hol_clause.ML") ("Tools/res_axioms.ML") ("Tools/res_reconstruct.ML") - ("Tools/ATP/watcher.ML") + ("Tools/watcher.ML") ("Tools/res_atp.ML") ("Tools/res_atp_provers.ML") ("Tools/res_atp_methods.ML") @@ -88,7 +88,7 @@ use "Tools/res_axioms.ML" --{*requires the combinators declared above*} use "Tools/res_hol_clause.ML" --{*requires the combinators*} use "Tools/res_reconstruct.ML" -use "Tools/ATP/watcher.ML" +use "Tools/watcher.ML" use "Tools/res_atp.ML" setup ResAxioms.meson_method_setup diff -r 6407d832da03 -r a4ffa756d8eb src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Jun 29 16:05:00 2007 +0200 +++ b/src/HOL/IsaMakefile Fri Jun 29 18:21:25 2007 +0200 @@ -92,7 +92,7 @@ Predicate.thy Product_Type.thy ROOT.ML Recdef.thy \ Record.thy Refute.thy Relation.thy Relation_Power.thy \ Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy \ - Groebner_Basis.thy Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML \ + Groebner_Basis.thy Tools/ATP/reduce_axiomsN.ML Tools/watcher.ML \ Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML \ Tools/Groebner_Basis/normalizer.ML \ Tools/Groebner_Basis/normalizer_data.ML Tools/Qelim/cooper.ML \ diff -r 6407d832da03 -r a4ffa756d8eb src/HOL/MetisExamples/Abstraction.thy --- a/src/HOL/MetisExamples/Abstraction.thy Fri Jun 29 16:05:00 2007 +0200 +++ b/src/HOL/MetisExamples/Abstraction.thy Fri Jun 29 18:21:25 2007 +0200 @@ -75,19 +75,13 @@ assume 1: "\f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)" assume 2: "a \ A \ a \ f b" have 3: "a \ A" - by (metis SigmaD1 0) -have 4: "b \ llabs_subgoal_1 f a" - by (metis SigmaD2 0) -have 5: "\X1 X2. X2 -` {X1} = llabs_subgoal_1 X2 X1" - by (metis 1 vimage_Collect_eq singleton_conv2) -have 6: "\X1 X2 X3. X1 X2 = X3 \ X2 \ llabs_subgoal_1 X1 X3" - by (metis vimage_singleton_eq 5) -have 7: "f b \ a" - by (metis 2 3) -have 8: "f b = a" - by (metis 6 4) + by (metis member2_def SigmaD1 0) +have 4: "f b \ a" + by (metis 3 2) +have 5: "f b = a" + by (metis Domain_Id Compl_UNIV_eq singleton_conv2 vimage_Collect_eq 1 vimage_singleton_eq SigmaD2 member2_def 0) show "False" - by (metis 8 7) + by (metis 5 4) qed finish_clausify diff -r 6407d832da03 -r a4ffa756d8eb src/HOL/MetisExamples/BigO.thy --- a/src/HOL/MetisExamples/BigO.thy Fri Jun 29 16:05:00 2007 +0200 +++ b/src/HOL/MetisExamples/BigO.thy Fri Jun 29 18:21:25 2007 +0200 @@ -683,70 +683,30 @@ (*Version 2: single-step proof*) proof (neg_clausify) fix x -assume 0: "\mes_mb9\'a. - (f\'a \ 'b\ordered_idom) mes_mb9 - \ (c\'b\ordered_idom) * (g\'a \ 'b\ordered_idom) mes_mb9" -assume 1: "\mes_mb8\'b\ordered_idom. - \ (f\'a \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a) mes_mb8) - \ mes_mb8 * \(g\'a \ 'b\ordered_idom) (x mes_mb8)\" -have 2: "\X3\'a. - (c\'b\ordered_idom) * (g\'a \ 'b\ordered_idom) X3 = - (f\'a \ 'b\ordered_idom) X3 \ - \ c * g X3 \ f X3" - by (metis Lattices.min_max.less_eq_less_inf.antisym_intro 0) -have 3: "\X3\'b\ordered_idom. - \ (f\'a \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a) \X3\) - \ \X3 * (g\'a \ 'b\ordered_idom) (x \X3\)\" - by (metis 1 Ring_and_Field.abs_mult) -have 4: "\X3\'b\ordered_idom. (1\'b\ordered_idom) * X3 = X3" - by (metis Ring_and_Field.mult_cancel_left2 Finite_Set.AC_mult.f.commute) -have 5: "\X3\'b\ordered_idom. X3 * (1\'b\ordered_idom) = X3" - by (metis Ring_and_Field.mult_cancel_right2 Finite_Set.AC_mult.f.commute) -have 6: "\X3\'b\ordered_idom. \X3\ * \X3\ = X3 * X3" - by (metis Ring_and_Field.abs_mult_self Finite_Set.AC_mult.f.commute) -have 7: "\X3\'b\ordered_idom. (0\'b\ordered_idom) \ X3 * X3" - by (metis Ring_and_Field.zero_le_square Finite_Set.AC_mult.f.commute) -have 8: "(0\'b\ordered_idom) \ (1\'b\ordered_idom)" - by (metis 7 Ring_and_Field.mult_cancel_left2) -have 9: "\X3\'b\ordered_idom. X3 * X3 = \X3 * X3\" - by (metis Ring_and_Field.abs_mult 6) -have 10: "\1\'b\ordered_idom\ = (1\'b\ordered_idom)" - by (metis 9 4) -have 11: "\X3\'b\ordered_idom. \\X3\\ = \X3\ * \1\'b\ordered_idom\" - by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 5) -have 12: "\X3\'b\ordered_idom. \\X3\\ = \X3\" - by (metis 11 10 5) -have 13: "\(X1\'b\ordered_idom) X3\'b\ordered_idom. - X3 * (1\'b\ordered_idom) \ X1 \ - \ \X3\ \ X1 \ \ (0\'b\ordered_idom) \ (1\'b\ordered_idom)" - by (metis OrderedGroup.abs_le_D1 Ring_and_Field.abs_mult_pos 5) -have 14: "\(X1\'b\ordered_idom) X3\'b\ordered_idom. - X3 \ X1 \ \ \X3\ \ X1 \ \ (0\'b\ordered_idom) \ (1\'b\ordered_idom)" - by (metis 13 5) -have 15: "\(X1\'b\ordered_idom) X3\'b\ordered_idom. X3 \ X1 \ \ \X3\ \ X1" - by (metis 14 8) -have 16: "\(X1\'b\ordered_idom) X3\'b\ordered_idom. X3 \ X1 \ X1 \ \X3\" - by (metis 15 Orderings.linorder_class.less_eq_less.linear) -have 17: "\X3\'b\ordered_idom. - X3 * (g\'a \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a) \X3\) - \ (f\'a \ 'b\ordered_idom) (x \X3\)" - by (metis 3 16) -have 18: "(c\'b\ordered_idom) * -(g\'a \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a) \c\) = -(f\'a \ 'b\ordered_idom) (x \c\)" - by (metis 2 17) -have 19: "\(X1\'b\ordered_idom) X3\'b\ordered_idom. \X3 * X1\ \ \\X3\\ * \\X1\\" - by (metis 15 Ring_and_Field.abs_le_mult Ring_and_Field.abs_mult) -have 20: "\(X1\'b\ordered_idom) X3\'b\ordered_idom. \X3 * X1\ \ \X3\ * \X1\" - by (metis 19 12 12) -have 21: "\(X1\'b\ordered_idom) X3\'b\ordered_idom. X3 * X1 \ \X3\ * \X1\" - by (metis 15 20) -have 22: "(f\'a \ 'b\ordered_idom) - ((x\'b\ordered_idom \ 'a) \c\'b\ordered_idom\) -\ \c\ * \(g\'a \ 'b\ordered_idom) (x \c\)\" - by (metis 21 18) -show 23: "False" - by (metis 22 1) +assume 0: "\A\'a\type. + (f\'a\type \ 'b\ordered_idom) A + \ (c\'b\ordered_idom) * (g\'a\type \ 'b\ordered_idom) A" +assume 1: "\A\'b\ordered_idom. + \ (f\'a\type \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a\type) A) + \ A * \(g\'a\type \ 'b\ordered_idom) (x A)\" +have 2: "\X2\'a\type. + \ (c\'b\ordered_idom) * (g\'a\type \ 'b\ordered_idom) X2 + < (f\'a\type \ 'b\ordered_idom) X2" + by (metis 0 linorder_not_le) +have 3: "\X2\'b\ordered_idom. + \ (f\'a\type \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a\type) \X2\) + \ \X2 * (g\'a\type \ 'b\ordered_idom) (x \X2\)\" + by (metis abs_mult 1) +have 4: "\X2\'b\ordered_idom. + \X2 * (g\'a\type \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a\type) \X2\)\ + < (f\'a\type \ 'b\ordered_idom) (x \X2\)" + by (metis 3 linorder_not_less) +have 5: "\X2\'b\ordered_idom. + X2 * (g\'a\type \ 'b\ordered_idom) ((x\'b\ordered_idom \ 'a\type) \X2\) + < (f\'a\type \ 'b\ordered_idom) (x \X2\)" + by (metis abs_less_iff 4) +show "False" + by (metis 2 5) qed @@ -1131,16 +1091,16 @@ apply (simp add: bigo_def) proof (neg_clausify) assume 0: "(c\'a\ordered_field) \ (0\'a\ordered_field)" -assume 1: "\mes_md\'a\ordered_field. \ (1\'a\ordered_field) \ mes_md * \c\'a\ordered_field\" +assume 1: "\A\'a\ordered_field. \ (1\'a\ordered_field) \ A * \c\'a\ordered_field\" have 2: "(0\'a\ordered_field) = \c\'a\ordered_field\ \ \ (1\'a\ordered_field) \ (1\'a\ordered_field)" by (metis 1 field_inverse) have 3: "\c\'a\ordered_field\ = (0\'a\ordered_field)" - by (metis 2 order_refl) + by (metis linorder_neq_iff linorder_antisym_conv1 2) have 4: "(0\'a\ordered_field) = (c\'a\ordered_field)" - by (metis OrderedGroup.abs_eq_0 3) -show 5: "False" - by (metis 4 0) + by (metis 3 abs_eq_0) +show "False" + by (metis 0 4) qed lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)" diff -r 6407d832da03 -r a4ffa756d8eb src/HOL/MetisExamples/set.thy --- a/src/HOL/MetisExamples/set.thy Fri Jun 29 16:05:00 2007 +0200 +++ b/src/HOL/MetisExamples/set.thy Fri Jun 29 18:21:25 2007 +0200 @@ -11,10 +11,11 @@ lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) & (S(x,y) | ~S(y,z) | Q(Z,Z)) & - (Q(X,y) | ~Q(y,Z) | S(X,X))"; -by metis; + (Q(X,y) | ~Q(y,Z) | S(X,X))" +by metis +(*??But metis can't prove the single-step version...*) -(*??Single-step reconstruction fails due to "assume?"*) + lemma "P(n::nat) ==> ~P(0) ==> n ~= 0" by metis @@ -220,11 +221,11 @@ proof (neg_clausify) fix x xa assume 0: "f (g x) = x" -assume 1: "\mes_oip. mes_oip = x \ f (g mes_oip) \ mes_oip" -assume 2: "\mes_oio. g (f (xa mes_oio)) = xa mes_oio \ g (f mes_oio) \ mes_oio" -assume 3: "\mes_oio. g (f mes_oio) \ mes_oio \ xa mes_oio \ mes_oio" +assume 1: "\A. A = x \ f (g A) \ A" +assume 2: "\A. g (f (xa A)) = xa A \ g (f A) \ A" +assume 3: "\A. g (f A) \ A \ xa A \ A" have 4: "\X1. g (f X1) \ X1 \ g x \ X1" - by (metis 3 2 1 2) + by (metis 3 1 2) show "False" by (metis 4 0) qed diff -r 6407d832da03 -r a4ffa756d8eb src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Fri Jun 29 16:05:00 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,397 +0,0 @@ -(* Title: Watcher.ML - ID: $Id$ - Author: Claire Quigley - Copyright 2004 University of Cambridge - *) - -(* 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. *) - -signature WATCHER = -sig - -(* Send request to Watcher for multiple spasses to be called for filenames in arg *) -(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *) - -val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit - -(* Send message to watcher to kill resolution provers *) -val callSlayer : TextIO.outstream -> unit - -(* Start a watcher and set up signal handlers*) -val createWatcher : - Proof.context * thm * string Vector.vector list -> - TextIO.instream * TextIO.outstream * Posix.Process.pid -val killWatcher : Posix.Process.pid -> unit -val killChild : ('a, 'b) Unix.proc -> OS.Process.status -val command_sep : char -val setting_sep : char -val reapAll : unit -> unit -end - - - -structure Watcher: WATCHER = -struct - -(*Field separators, used to pack items onto a text line*) -val command_sep = #"\t" -and setting_sep = #"%"; - -val goals_being_watched = ref 0; - -val trace_path = Path.basic "watcher_trace"; - -fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s - else (); - -(*Representation of a watcher process*) -type proc = {pid : Posix.Process.pid, - instr : TextIO.instream, - outstr : TextIO.outstream}; - -(*Representation of a child (ATP) process*) -type cmdproc = { - prover: string, (* Name of the resolution prover used, e.g. "spass"*) - file: string, (* The file containing the goal for the ATP to prove *) - proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc, - instr : TextIO.instream, (*Output of the child process *) - outstr : TextIO.outstream}; (*Input to the child process *) - - -fun fdReader (name : string, fd : Posix.IO.file_desc) = - Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd }; - -fun fdWriter (name, fd) = - Posix.IO.mkTextWriter { - appendMode = false, - initBlkMode = true, - name = name, - chunkSize=4096, - fd = fd}; - -fun openOutFD (name, fd) = - TextIO.mkOutstream ( - TextIO.StreamIO.mkOutstream ( - fdWriter (name, fd), IO.BLOCK_BUF)); - -fun openInFD (name, fd) = - TextIO.mkInstream ( - TextIO.StreamIO.mkInstream ( - fdReader (name, fd), "")); - - -(* Send request to Watcher for a vampire to be called for filename in arg*) -fun callResProver (toWatcherStr, arg) = - (TextIO.output (toWatcherStr, arg^"\n"); - TextIO.flushOut toWatcherStr) - -(* Send request to Watcher for multiple provers to be called*) -fun callResProvers (toWatcherStr, []) = - (TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr) - | callResProvers (toWatcherStr, - (prover,proverCmd,settings,probfile) :: args) = - (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile])); - (*Uses a special character to separate items sent to watcher*) - TextIO.output (toWatcherStr, - space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]); - inc goals_being_watched; - TextIO.flushOut toWatcherStr; - callResProvers (toWatcherStr,args)) - - -(*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) = - let val thisLine = the_default "" (TextIO.inputLine fromParentStr) - 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); - TextIO.flushOut toParentStr; - [("","Kill children",[],"")]) - else - let val [prover,proverCmd,settingstr,probfile,_] = - 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 ^ - "\n problem file: " ^ probfile); - getCmds (toParentStr, fromParentStr, - (prover, proverCmd, settings, probfile)::cmdList) - end - handle Bind => - (trace "\ngetCmds: command parsing failed!"; - getCmds (toParentStr, fromParentStr, cmdList)) - end - - -(*Get Io-descriptor for polling of an input stream*) -fun getInIoDesc someInstr = - let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr) - val _ = TextIO.output (TextIO.stdOut, buf) - val ioDesc = - case rd - of TextPrimIO.RD{ioDesc = SOME iod, ...} => SOME iod - | _ => NONE - in (* since getting the reader will have terminated the stream, we need - * to build a new stream. *) - TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf)); - ioDesc - end - -fun pollChild fromStr = - case getInIoDesc fromStr of - SOME iod => - (case OS.IO.pollDesc iod of - SOME pd => - let val pd' = OS.IO.pollIn pd in - case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of - [] => false - | pd''::_ => OS.IO.isIn pd'' - end - | NONE => false) - | NONE => false - - -(*************************************) -(* Set up a Watcher Process *) -(*************************************) - -fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc); - -val killChildren = List.app (ignore o killChild o #proc_handle) : cmdproc list -> unit; - -fun killWatcher (toParentStr, procList) = - (trace "\nWatcher timeout: Killing proof processes"; - TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); - TextIO.flushOut toParentStr; - killChildren procList; - Posix.Process.exit 0w0); - -(* take an instream and poll its underlying reader for input *) -fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = - case OS.IO.pollDesc fromParentIOD of - SOME pd => - (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of - [] => NONE - | pd''::_ => if OS.IO.isIn pd'' - then SOME (getCmds (toParentStr, fromParentStr, [])) - else NONE) - | NONE => NONE; - -(*get the number of the subgoal from the filename: the last digit string*) -fun number_from_filename s = - let val numbers = "xxx" :: String.tokens (not o Char.isDigit) s - in valOf (Int.fromString (List.last numbers)) end - handle Option => (trace ("\nWatcher could not read subgoal nunber! " ^ s); - error ("Watcher could not read subgoal nunber! " ^ s)); - -(*Call ATP. Settings should be a list of strings ["-t 300", "-m 100000"], - which we convert below to ["-t", "300", "-m", "100000"] using String.tokens. - Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and - Vampire will reject the switches.*) -fun execCmds [] procList = procList - | execCmds ((prover,proverCmd,settings,file)::cmds) procList = - let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file) - val settings' = List.concat (map (String.tokens Char.isSpace) settings) - val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = - Unix.execute(proverCmd, settings' @ [file]) - val (instr, outstr) = Unix.streamsOf childhandle - val newProcList = {prover=prover, file=file, proc_handle=childhandle, - instr=instr, outstr=outstr} :: procList - val _ = trace ("\nFinished at " ^ - Date.toString(Date.fromTimeLocal(Time.now()))) - in execCmds cmds newProcList end - -fun checkChildren (ctxt, th, thm_names_list) toParentStr children = - let fun check [] = [] (* no children to check *) - | check (child::children) = - let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child - val _ = trace ("\nprobfile = " ^ file) - val sgno = number_from_filename file (*subgoal number*) - val thm_names = List.nth(thm_names_list, sgno-1); - val ppid = Posix.ProcEnv.getppid() - in - if pollChild childIn - then (* check here for prover label on child*) - let val _ = trace ("\nInput available from child: " ^ file) - val childDone = (case prover of - "vampire" => ResReconstruct.checkVampProofFound - (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names) - | "E" => ResReconstruct.checkEProofFound - (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names) - | "spass" => ResReconstruct.checkSpassProofFound - (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names) - | _ => (trace ("\nBad prover! " ^ prover); true) ) - in - if childDone (*ATP has reported back (with success OR failure)*) - then (Unix.reap proc_handle; - if !Output.debugging then () else OS.FileSys.remove file; - check children) - else child :: check children - end - else (trace "\nNo child output"; child :: check children) - end - in - trace ("\nIn checkChildren, length of queue: " ^ Int.toString(length children)); - check children - end; - - -fun setupWatcher (ctxt, th, thm_names_list) = - let - val checkc = checkChildren (ctxt, th, thm_names_list) - val p1 = Posix.IO.pipe() (*pipes for communication between parent and watcher*) - val p2 = Posix.IO.pipe() - (****** 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 - 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 pid = Posix.ProcEnv.getpid() - val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid} - (*set process group id: allows killing all children*) - val () = trace "\nsubgoals forked to startWatcher" - val limit = ref 200; (*don't let watcher run forever*) - (*Watcher Loop : Check running ATP processes for output*) - fun keepWatching procList = - (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^ - " length(procList) = " ^ Int.toString(length procList)); - OS.Process.sleep (Time.fromMilliseconds 100); limit := !limit - 1; - if !limit < 0 then killWatcher (toParentStr, procList) - else - case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of - SOME [(_,"Kill children",_,_)] => - (trace "\nReceived Kill command"; - killChildren procList; keepWatching []) - | SOME cmds => (* deal with commands from Isabelle process *) - if length procList < 40 then (* Execute locally *) - let val _ = trace("\nCommands from parent: " ^ - Int.toString(length cmds)) - val newProcList' = checkc toParentStr (execCmds cmds procList) - in trace "\nCommands executed"; keepWatching newProcList' end - else (* Execute remotely [FIXME: NOT REALLY] *) - let val newProcList' = checkc toParentStr (execCmds cmds procList) - in keepWatching newProcList' end - | NONE => (* No new input from Isabelle *) - (trace "\nNothing from parent..."; - keepWatching(checkc toParentStr procList))) - handle exn => (*FIXME: exn handler is too general!*) - (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn); - keepWatching procList); - 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; - keepWatching (procList) - end; - - val _ = TextIO.flushOut TextIO.stdOut - val pid = startWatcher [] - (* communication streams to watcher*) - val instr = openInFD ("_exec_in", #infd p2) - val outstr = openOutFD ("_exec_out", #outfd p1) - in - (* close the child-side fds*) - Posix.IO.close (#outfd p2); Posix.IO.close (#infd p1); - (* set the fds close on exec *) - Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); - Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); - {pid = pid, instr = instr, outstr = outstr} - end; - - - -(**********************************************************) -(* Start a watcher and set up signal handlers *) -(**********************************************************) - -(*Signal handler to tidy away zombie processes*) -fun reapAll() = - (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of - SOME _ => reapAll() | NONE => ()) - handle OS.SysErr _ => () - -(*FIXME: does the main process need something like this? - IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*) - -fun killWatcher pid = - (goals_being_watched := 0; - Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill); - reapAll()); - -fun reapWatcher(pid, instr, outstr) = ignore - (TextIO.closeIn instr; TextIO.closeOut outstr; - Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])) - handle OS.SysErr _ => () - -fun string_of_subgoal th i = - string_of_cterm (List.nth(cprems_of th, i-1)) - handle Subscript => "Subgoal number out of range!" - -fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th)) - -fun createWatcher (ctxt, th, thm_names_list) = - let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list) - fun decr_watched() = - (goals_being_watched := !goals_being_watched - 1; - if !goals_being_watched = 0 - then - (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid)); - killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) ) - else ()) - fun proofHandler _ = - let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid) - val outcome = ResReconstruct.restore_newlines (the_default "" (TextIO.inputLine childin)) - val probfile = the_default "" (TextIO.inputLine childin) - val sgno = number_from_filename probfile - val text = string_of_subgoal th sgno - fun report s = priority ("Subgoal " ^ Int.toString sgno ^ ": " ^ s); - in - Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^ - "\"\nprobfile = " ^ probfile ^ - "\nGoals being watched: "^ Int.toString (!goals_being_watched))); - if String.isPrefix "Invalid" outcome - then (report ("Subgoal is not provable:\n" ^ text); - decr_watched()) - else if String.isPrefix "Failure" outcome - then (report ("Proof attempt failed:\n" ^ text); - decr_watched()) - (* print out a list of rules used from clasimpset*) - else if String.isPrefix "Success" outcome - then (report (outcome ^ text); - decr_watched()) - (* if proof translation failed *) - else if String.isPrefix "Translation failed" outcome - then (report (outcome ^ text); - decr_watched()) - else (report "System error in proof handler"; - decr_watched()) - end - in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th)); - IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler); - (childin, childout, childpid) - end - -end (* structure Watcher *) diff -r 6407d832da03 -r a4ffa756d8eb src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Fri Jun 29 16:05:00 2007 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Fri Jun 29 18:21:25 2007 +0200 @@ -228,7 +228,7 @@ case strip_prefix ResClause.schematic_var_prefix a of SOME b => make_var (b,T) | NONE => make_var (a,T) (*Variable from the ATP, say X1*) - in list_comb (opr, List.map (term_of_stree [] thy) (args@ts)) end; + in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end; (*Type class literal applied to a type. Returns triple of polarity, class, type.*) fun constraint_of_stree pol (Br("c_Not",[t])) = constraint_of_stree (not pol) t @@ -279,21 +279,18 @@ (*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints. vt0 holds the initial sort constraints, from the conjecture clauses.*) -fun clause_of_strees_aux ctxt vt0 ts = +fun clause_of_strees ctxt vt0 ts = let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in singleton (ProofContext.infer_types ctxt) (TypeInfer.constrain (fix_sorts vt dt) HOLogic.boolT) end; -(*Quantification over a list of Vars. FUXNE: for term.ML??*) +(*Quantification over a list of Vars. FIXME: for term.ML??*) fun list_all_var ([], t: term) = t | list_all_var ((v as Var(ix,T)) :: vars, t) = (all T) $ Abs(string_of_indexname ix, T, abstract_over (v, list_all_var (vars,t))); fun gen_all_vars t = list_all_var (term_vars t, t); -fun clause_of_strees thy vt0 ts = - gen_all_vars (HOLogic.mk_Trueprop (clause_of_strees_aux thy vt0 ts)); - fun ints_of_stree_aux (Int n, ns) = n::ns | ints_of_stree_aux (Br(_,ts), ns) = foldl ints_of_stree_aux ns ts; @@ -334,22 +331,62 @@ fun dest_disj t = dest_disj_aux t []; -(*Remove types from a term, to eliminate the randomness of type inference*) -fun smash_types (Const(a,_)) = Const(a,dummyT) - | smash_types (Free(a,_)) = Free(a,dummyT) - | smash_types (Var(a,_)) = Var(a,dummyT) - | smash_types (f$t) = smash_types f $ smash_types t - | smash_types t = t; +(** Finding a matching assumption. The literals may be permuted, and variable names + may disagree. We have to try all combinations of literals (quadratic!) and + match up the variable names consistently. **) + +fun strip_alls_aux n (Const("all",_)$Abs(a,T,t)) = + strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t)) + | strip_alls_aux _ t = t; + +val strip_alls = strip_alls_aux 0; + +exception MATCH_LITERAL; -val sort_lits = sort Term.fast_term_ord o dest_disj o - smash_types o HOLogic.dest_Trueprop o strip_all_body; +(*Ignore types: they are not to be trusted...*) +fun match_literal (t1$u1) (t2$u2) env = + match_literal t1 t2 (match_literal u1 u2 env) + | match_literal (Abs (_,_,t1)) (Abs (_,_,t2)) env = + match_literal t1 t2 env + | match_literal (Bound i1) (Bound i2) env = + if i1=i2 then env else raise MATCH_LITERAL + | match_literal (Const(a1,_)) (Const(a2,_)) env = + if a1=a2 then env else raise MATCH_LITERAL + | match_literal (Free(a1,_)) (Free(a2,_)) env = + if a1=a2 then env else raise MATCH_LITERAL + | match_literal (Var(ix1,_)) (Var(ix2,_)) env = insert (op =) (ix1,ix2) env + | match_literal _ _ env = raise MATCH_LITERAL; + +(*Checking that all variable associations are unique. The list env contains no + repetitions, but does it contain say (x,y) and (y,y)? *) +fun good env = + let val (xs,ys) = ListPair.unzip env + in not (has_duplicates (op=) xs orelse has_duplicates (op=) ys) end; + +(*Match one list of literals against another, ignoring types and the order of + literals. Sorting is unreliable because we don't have types or variable names.*) +fun matches_aux _ [] [] = true + | matches_aux env (lit::lits) ts = + let fun match1 us [] = false + | match1 us (t::ts) = + let val env' = match_literal lit t env + in (good env' andalso matches_aux env' lits (us@ts)) orelse + match1 (t::us) ts + end + handle MATCH_LITERAL => match1 (t::us) ts + in match1 [] ts end; + +(*Is this length test useful?*) +fun matches (lits1,lits2) = + length lits1 = length lits2 andalso + matches_aux [] (map Envir.eta_contract lits1) (map Envir.eta_contract lits2); fun permuted_clause t = - let val lits = sort_lits t + let val lits = dest_disj t fun perm [] = NONE | perm (ctm::ctms) = - if forall (op aconv) (ListPair.zip (lits, sort_lits ctm)) then SOME ctm - else perm ctms + if matches (lits, dest_disj (HOLogic.dest_Trueprop (strip_alls ctm))) + then SOME ctm else perm ctms in perm end; fun have_or_show "show " lname = "show \"" @@ -364,7 +401,7 @@ SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n" | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n") (*no match!!*) | doline have (lname, t, deps) = - have_or_show have lname ^ string_of t ^ + have_or_show have lname ^ string_of (gen_all_vars (HOLogic.mk_Trueprop t)) ^ "\"\n by (metis " ^ space_implode " " deps ^ ")\n" fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)] | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines @@ -373,7 +410,7 @@ fun notequal t (_,t',_) = not (t aconv t'); (*No "real" literals means only type information*) -fun eq_types t = t aconv (HOLogic.mk_Trueprop HOLogic.true_const); +fun eq_types t = t aconv HOLogic.true_const; fun replace_dep (old:int, new) dep = if dep=old then new else [dep]; @@ -465,16 +502,18 @@ val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c); -(*The output to the watcher must be a SINGLE line...clearly \t must not be used.*) -val encode_newlines = String.translate (fn c => if c = #"\n" then "\t" else str c); -val restore_newlines = String.translate (fn c => if c = #"\t" then "\n" else str c); +val txt_path = Path.ext "txt" o Path.explode o nospaces; fun signal_success probfile toParent ppid msg = - (trace ("\nReporting Success for " ^ probfile ^ "\n" ^ msg); - TextIO.output (toParent, "Success. " ^ encode_newlines msg ^ "\n"); - TextIO.output (toParent, probfile ^ "\n"); - TextIO.flushOut toParent; - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)); + let val _ = trace ("\nReporting Success for " ^ probfile ^ "\n" ^ msg) + in + (*We write the proof to a file because sending very long lines may fail...*) + File.write (txt_path probfile) msg; + TextIO.output (toParent, "Success.\n"); + TextIO.output (toParent, probfile ^ "\n"); + TextIO.flushOut toParent; + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2) + end; fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names = let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract)) diff -r 6407d832da03 -r a4ffa756d8eb src/HOL/Tools/watcher.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/watcher.ML Fri Jun 29 18:21:25 2007 +0200 @@ -0,0 +1,402 @@ +(* Title: Watcher.ML + ID: $Id$ + Author: Claire Quigley + Copyright 2004 University of Cambridge + *) + +(* 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. *) + +signature WATCHER = +sig + +(* Send request to Watcher for multiple spasses to be called for filenames in arg *) +(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *) + +val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit + +(* Send message to watcher to kill resolution provers *) +val callSlayer : TextIO.outstream -> unit + +(* Start a watcher and set up signal handlers*) +val createWatcher : + Proof.context * thm * string Vector.vector list -> + TextIO.instream * TextIO.outstream * Posix.Process.pid +val killWatcher : Posix.Process.pid -> unit +val killChild : ('a, 'b) Unix.proc -> OS.Process.status +val command_sep : char +val setting_sep : char +val reapAll : unit -> unit +end + + + +structure Watcher: WATCHER = +struct + +(*Field separators, used to pack items onto a text line*) +val command_sep = #"\t" +and setting_sep = #"%"; + +val goals_being_watched = ref 0; + +val trace_path = Path.basic "watcher_trace"; + +fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s + else (); + +(*Representation of a watcher process*) +type proc = {pid : Posix.Process.pid, + instr : TextIO.instream, + outstr : TextIO.outstream}; + +(*Representation of a child (ATP) process*) +type cmdproc = { + prover: string, (* Name of the resolution prover used, e.g. "spass"*) + file: string, (* The file containing the goal for the ATP to prove *) + proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc, + instr : TextIO.instream, (*Output of the child process *) + outstr : TextIO.outstream}; (*Input to the child process *) + + +fun fdReader (name : string, fd : Posix.IO.file_desc) = + Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd }; + +fun fdWriter (name, fd) = + Posix.IO.mkTextWriter { + appendMode = false, + initBlkMode = true, + name = name, + chunkSize=4096, + fd = fd}; + +fun openOutFD (name, fd) = + TextIO.mkOutstream ( + TextIO.StreamIO.mkOutstream ( + fdWriter (name, fd), IO.BLOCK_BUF)); + +fun openInFD (name, fd) = + TextIO.mkInstream ( + TextIO.StreamIO.mkInstream ( + fdReader (name, fd), "")); + + +(* Send request to Watcher for a vampire to be called for filename in arg*) +fun callResProver (toWatcherStr, arg) = + (TextIO.output (toWatcherStr, arg^"\n"); + TextIO.flushOut toWatcherStr) + +(* Send request to Watcher for multiple provers to be called*) +fun callResProvers (toWatcherStr, []) = + (TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr) + | callResProvers (toWatcherStr, + (prover,proverCmd,settings,probfile) :: args) = + (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile])); + (*Uses a special character to separate items sent to watcher*) + TextIO.output (toWatcherStr, + space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]); + inc goals_being_watched; + TextIO.flushOut toWatcherStr; + callResProvers (toWatcherStr,args)) + + +(*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) = + let val thisLine = the_default "" (TextIO.inputLine fromParentStr) + 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); + TextIO.flushOut toParentStr; + [("","Kill children",[],"")]) + else + let val [prover,proverCmd,settingstr,probfile,_] = + 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 ^ + "\n problem file: " ^ probfile); + getCmds (toParentStr, fromParentStr, + (prover, proverCmd, settings, probfile)::cmdList) + end + handle Bind => + (trace "\ngetCmds: command parsing failed!"; + getCmds (toParentStr, fromParentStr, cmdList)) + end + + +(*Get Io-descriptor for polling of an input stream*) +fun getInIoDesc someInstr = + let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr) + val _ = TextIO.output (TextIO.stdOut, buf) + val ioDesc = + case rd + of TextPrimIO.RD{ioDesc = SOME iod, ...} => SOME iod + | _ => NONE + in (* since getting the reader will have terminated the stream, we need + * to build a new stream. *) + TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf)); + ioDesc + end + +fun pollChild fromStr = + case getInIoDesc fromStr of + SOME iod => + (case OS.IO.pollDesc iod of + SOME pd => + let val pd' = OS.IO.pollIn pd in + case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of + [] => false + | pd''::_ => OS.IO.isIn pd'' + end + | NONE => false) + | NONE => false + + +(*************************************) +(* Set up a Watcher Process *) +(*************************************) + +fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc); + +val killChildren = List.app (ignore o killChild o #proc_handle) : cmdproc list -> unit; + +fun killWatcher (toParentStr, procList) = + (trace "\nWatcher timeout: Killing proof processes"; + TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); + TextIO.flushOut toParentStr; + killChildren procList; + Posix.Process.exit 0w0); + +(* take an instream and poll its underlying reader for input *) +fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = + case OS.IO.pollDesc fromParentIOD of + SOME pd => + (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of + [] => NONE + | pd''::_ => if OS.IO.isIn pd'' + then SOME (getCmds (toParentStr, fromParentStr, [])) + else NONE) + | NONE => NONE; + +(*get the number of the subgoal from the filename: the last digit string*) +fun number_from_filename s = + let val numbers = "xxx" :: String.tokens (not o Char.isDigit) s + in valOf (Int.fromString (List.last numbers)) end + handle Option => (trace ("\nWatcher could not read subgoal nunber! " ^ s); + error ("Watcher could not read subgoal nunber! " ^ s)); + +(*Call ATP. Settings should be a list of strings ["-t 300", "-m 100000"], + which we convert below to ["-t", "300", "-m", "100000"] using String.tokens. + Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and + Vampire will reject the switches.*) +fun execCmds [] procList = procList + | execCmds ((prover,proverCmd,settings,file)::cmds) procList = + let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file) + val settings' = List.concat (map (String.tokens Char.isSpace) settings) + val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = + Unix.execute(proverCmd, settings' @ [file]) + val (instr, outstr) = Unix.streamsOf childhandle + val newProcList = {prover=prover, file=file, proc_handle=childhandle, + instr=instr, outstr=outstr} :: procList + val _ = trace ("\nFinished at " ^ + Date.toString(Date.fromTimeLocal(Time.now()))) + in execCmds cmds newProcList end + +fun checkChildren (ctxt, th, thm_names_list) toParentStr children = + let fun check [] = [] (* no children to check *) + | check (child::children) = + let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child + val _ = trace ("\nprobfile = " ^ file) + val sgno = number_from_filename file (*subgoal number*) + val thm_names = List.nth(thm_names_list, sgno-1); + val ppid = Posix.ProcEnv.getppid() + in + if pollChild childIn + then (* check here for prover label on child*) + let val _ = trace ("\nInput available from child: " ^ file) + val childDone = (case prover of + "vampire" => ResReconstruct.checkVampProofFound + (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names) + | "E" => ResReconstruct.checkEProofFound + (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names) + | "spass" => ResReconstruct.checkSpassProofFound + (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names) + | _ => (trace ("\nBad prover! " ^ prover); true) ) + in + if childDone (*ATP has reported back (with success OR failure)*) + then (Unix.reap proc_handle; + if !Output.debugging then () else OS.FileSys.remove file; + check children) + else child :: check children + end + else (trace "\nNo child output"; child :: check children) + end + in + trace ("\nIn checkChildren, length of queue: " ^ Int.toString(length children)); + check children + end; + + +fun setupWatcher (ctxt, th, thm_names_list) = + let + val checkc = checkChildren (ctxt, th, thm_names_list) + val p1 = Posix.IO.pipe() (*pipes for communication between parent and watcher*) + val p2 = Posix.IO.pipe() + (****** 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 + 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 pid = Posix.ProcEnv.getpid() + val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid} + (*set process group id: allows killing all children*) + val () = trace "\nsubgoals forked to startWatcher" + val limit = ref 200; (*don't let watcher run forever*) + (*Watcher Loop : Check running ATP processes for output*) + fun keepWatching procList = + (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^ + " length(procList) = " ^ Int.toString(length procList)); + OS.Process.sleep (Time.fromMilliseconds 100); limit := !limit - 1; + if !limit < 0 then killWatcher (toParentStr, procList) + else + case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of + SOME [(_,"Kill children",_,_)] => + (trace "\nReceived Kill command"; + killChildren procList; keepWatching []) + | SOME cmds => (* deal with commands from Isabelle process *) + let val _ = trace("\nCommands from parent: " ^ + Int.toString(length cmds)) + val newProcList' = checkc toParentStr (execCmds cmds procList) + in trace "\nCommands executed"; keepWatching newProcList' end + | NONE => (* No new input from Isabelle *) + (trace "\nNothing from parent..."; + keepWatching(checkc toParentStr procList))) + handle exn => (*FIXME: exn handler is too general!*) + (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn); + keepWatching procList); + 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; + keepWatching (procList) + end; + + val _ = TextIO.flushOut TextIO.stdOut + val pid = startWatcher [] + (* communication streams to watcher*) + val instr = openInFD ("_exec_in", #infd p2) + val outstr = openOutFD ("_exec_out", #outfd p1) + in + (* close the child-side fds*) + Posix.IO.close (#outfd p2); Posix.IO.close (#infd p1); + (* set the fds close on exec *) + Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); + Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); + {pid = pid, instr = instr, outstr = outstr} + end; + + + +(**********************************************************) +(* Start a watcher and set up signal handlers *) +(**********************************************************) + +(*Signal handler to tidy away zombie processes*) +fun reapAll() = + (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of + SOME _ => reapAll() | NONE => ()) + handle OS.SysErr _ => () + +(*FIXME: does the main process need something like this? + IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*) + +fun killWatcher pid = + (goals_being_watched := 0; + Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill); + reapAll()); + +fun reapWatcher(pid, instr, outstr) = ignore + (TextIO.closeIn instr; TextIO.closeOut outstr; + Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])) + handle OS.SysErr _ => () + +fun string_of_subgoal th i = + string_of_cterm (List.nth(cprems_of th, i-1)) + handle Subscript => "Subgoal number out of range!" + +fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th)) + +fun read_proof probfile = + let val p = ResReconstruct.txt_path probfile + val _ = trace("\nReading proof from file " ^ Path.implode p) + val msg = File.read p + val _ = trace("\nProof:\n" ^ msg) + in if !Output.debugging then () else File.rm p; msg end; + +fun createWatcher (ctxt, th, thm_names_list) = + let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list) + fun decr_watched() = + (goals_being_watched := !goals_being_watched - 1; + if !goals_being_watched = 0 + then + (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid)); + killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) ) + else ()) + fun proofHandler _ = + let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid) + val outcome = valOf (TextIO.inputLine childin) + handle Option => error "watcher: \"outcome\" line is missing" + val probfile = valOf (TextIO.inputLine childin) + handle Option => error "watcher: \"probfile\" line is missing" + val sgno = number_from_filename probfile + val text = string_of_subgoal th sgno + fun report s = priority ("Subgoal " ^ Int.toString sgno ^ ": " ^ s); + in + Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^ + "\"\nprobfile = " ^ probfile ^ + "\nGoals being watched: "^ Int.toString (!goals_being_watched))); + if String.isPrefix "Invalid" outcome + then (report ("Subgoal is not provable:\n" ^ text); + decr_watched()) + else if String.isPrefix "Failure" outcome + then (report ("Proof attempt failed:\n" ^ text); + decr_watched()) + (* print out a list of rules used from clasimpset*) + else if String.isPrefix "Success" outcome + then (report (read_proof probfile ^ "\n" ^ text); + decr_watched()) + (* if proof translation failed *) + else if String.isPrefix "Translation failed" outcome + then (report (outcome ^ text); + decr_watched()) + else (report "System error in proof handler"; + decr_watched()) + end + in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th)); + IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler); + (childin, childout, childpid) + end + +end (* structure Watcher *)