--- 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
--- 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 \
--- 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: "\<And>f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)"
assume 2: "a \<notin> A \<or> a \<noteq> f b"
have 3: "a \<in> A"
- by (metis SigmaD1 0)
-have 4: "b \<in> llabs_subgoal_1 f a"
- by (metis SigmaD2 0)
-have 5: "\<And>X1 X2. X2 -` {X1} = llabs_subgoal_1 X2 X1"
- by (metis 1 vimage_Collect_eq singleton_conv2)
-have 6: "\<And>X1 X2 X3. X1 X2 = X3 \<or> X2 \<notin> llabs_subgoal_1 X1 X3"
- by (metis vimage_singleton_eq 5)
-have 7: "f b \<noteq> a"
- by (metis 2 3)
-have 8: "f b = a"
- by (metis 6 4)
+ by (metis member2_def SigmaD1 0)
+have 4: "f b \<noteq> 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
--- 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: "\<And>mes_mb9\<Colon>'a.
- (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) mes_mb9
- \<le> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) mes_mb9"
-assume 1: "\<And>mes_mb8\<Colon>'b\<Colon>ordered_idom.
- \<not> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_mb8)
- \<le> mes_mb8 * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x mes_mb8)\<bar>"
-have 2: "\<And>X3\<Colon>'a.
- (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) X3 =
- (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) X3 \<or>
- \<not> c * g X3 \<le> f X3"
- by (metis Lattices.min_max.less_eq_less_inf.antisym_intro 0)
-have 3: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
- \<not> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>X3\<bar>)
- \<le> \<bar>X3 * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X3\<bar>)\<bar>"
- by (metis 1 Ring_and_Field.abs_mult)
-have 4: "\<And>X3\<Colon>'b\<Colon>ordered_idom. (1\<Colon>'b\<Colon>ordered_idom) * X3 = X3"
- by (metis Ring_and_Field.mult_cancel_left2 Finite_Set.AC_mult.f.commute)
-have 5: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 * (1\<Colon>'b\<Colon>ordered_idom) = X3"
- by (metis Ring_and_Field.mult_cancel_right2 Finite_Set.AC_mult.f.commute)
-have 6: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
- by (metis Ring_and_Field.abs_mult_self Finite_Set.AC_mult.f.commute)
-have 7: "\<And>X3\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> X3 * X3"
- by (metis Ring_and_Field.zero_le_square Finite_Set.AC_mult.f.commute)
-have 8: "(0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
- by (metis 7 Ring_and_Field.mult_cancel_left2)
-have 9: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 * X3 = \<bar>X3 * X3\<bar>"
- by (metis Ring_and_Field.abs_mult 6)
-have 10: "\<bar>1\<Colon>'b\<Colon>ordered_idom\<bar> = (1\<Colon>'b\<Colon>ordered_idom)"
- by (metis 9 4)
-have 11: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>1\<Colon>'b\<Colon>ordered_idom\<bar>"
- by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 5)
-have 12: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar>"
- by (metis 11 10 5)
-have 13: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom.
- X3 * (1\<Colon>'b\<Colon>ordered_idom) \<le> X1 \<or>
- \<not> \<bar>X3\<bar> \<le> X1 \<or> \<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
- by (metis OrderedGroup.abs_le_D1 Ring_and_Field.abs_mult_pos 5)
-have 14: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom.
- X3 \<le> X1 \<or> \<not> \<bar>X3\<bar> \<le> X1 \<or> \<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
- by (metis 13 5)
-have 15: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> \<not> \<bar>X3\<bar> \<le> X1"
- by (metis 14 8)
-have 16: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
- by (metis 15 Orderings.linorder_class.less_eq_less.linear)
-have 17: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
- X3 * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>X3\<bar>)
- \<le> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X3\<bar>)"
- by (metis 3 16)
-have 18: "(c\<Colon>'b\<Colon>ordered_idom) *
-(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>c\<bar>) =
-(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>c\<bar>)"
- by (metis 2 17)
-have 19: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3 * X1\<bar> \<le> \<bar>\<bar>X3\<bar>\<bar> * \<bar>\<bar>X1\<bar>\<bar>"
- by (metis 15 Ring_and_Field.abs_le_mult Ring_and_Field.abs_mult)
-have 20: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3 * X1\<bar> \<le> \<bar>X3\<bar> * \<bar>X1\<bar>"
- by (metis 19 12 12)
-have 21: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 * X1 \<le> \<bar>X3\<bar> * \<bar>X1\<bar>"
- by (metis 15 20)
-have 22: "(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom)
- ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>c\<Colon>'b\<Colon>ordered_idom\<bar>)
-\<le> \<bar>c\<bar> * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>c\<bar>)\<bar>"
- by (metis 21 18)
-show 23: "False"
- by (metis 22 1)
+assume 0: "\<And>A\<Colon>'a\<Colon>type.
+ (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) A
+ \<le> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) A"
+assume 1: "\<And>A\<Colon>'b\<Colon>ordered_idom.
+ \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) A)
+ \<le> A * \<bar>(g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x A)\<bar>"
+have 2: "\<And>X2\<Colon>'a\<Colon>type.
+ \<not> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) X2
+ < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) X2"
+ by (metis 0 linorder_not_le)
+have 3: "\<And>X2\<Colon>'b\<Colon>ordered_idom.
+ \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
+ \<le> \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X2\<bar>)\<bar>"
+ by (metis abs_mult 1)
+have 4: "\<And>X2\<Colon>'b\<Colon>ordered_idom.
+ \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)\<bar>
+ < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X2\<bar>)"
+ by (metis 3 linorder_not_less)
+have 5: "\<And>X2\<Colon>'b\<Colon>ordered_idom.
+ X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
+ < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X2\<bar>)"
+ 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\<Colon>'a\<Colon>ordered_field) \<noteq> (0\<Colon>'a\<Colon>ordered_field)"
-assume 1: "\<And>mes_md\<Colon>'a\<Colon>ordered_field. \<not> (1\<Colon>'a\<Colon>ordered_field) \<le> mes_md * \<bar>c\<Colon>'a\<Colon>ordered_field\<bar>"
+assume 1: "\<And>A\<Colon>'a\<Colon>ordered_field. \<not> (1\<Colon>'a\<Colon>ordered_field) \<le> A * \<bar>c\<Colon>'a\<Colon>ordered_field\<bar>"
have 2: "(0\<Colon>'a\<Colon>ordered_field) = \<bar>c\<Colon>'a\<Colon>ordered_field\<bar> \<or>
\<not> (1\<Colon>'a\<Colon>ordered_field) \<le> (1\<Colon>'a\<Colon>ordered_field)"
by (metis 1 field_inverse)
have 3: "\<bar>c\<Colon>'a\<Colon>ordered_field\<bar> = (0\<Colon>'a\<Colon>ordered_field)"
- by (metis 2 order_refl)
+ by (metis linorder_neq_iff linorder_antisym_conv1 2)
have 4: "(0\<Colon>'a\<Colon>ordered_field) = (c\<Colon>'a\<Colon>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)"
--- 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: "\<And>mes_oip. mes_oip = x \<or> f (g mes_oip) \<noteq> mes_oip"
-assume 2: "\<And>mes_oio. g (f (xa mes_oio)) = xa mes_oio \<or> g (f mes_oio) \<noteq> mes_oio"
-assume 3: "\<And>mes_oio. g (f mes_oio) \<noteq> mes_oio \<or> xa mes_oio \<noteq> mes_oio"
+assume 1: "\<And>A. A = x \<or> f (g A) \<noteq> A"
+assume 2: "\<And>A. g (f (xa A)) = xa A \<or> g (f A) \<noteq> A"
+assume 3: "\<And>A. g (f A) \<noteq> A \<or> xa A \<noteq> A"
have 4: "\<And>X1. g (f X1) \<noteq> X1 \<or> g x \<noteq> X1"
- by (metis 3 2 1 2)
+ by (metis 3 1 2)
show "False"
by (metis 4 0)
qed
--- 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 *)
--- 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))
--- /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 *)