bug fixes to proof reconstruction
authorpaulson
Fri Jun 29 18:21:25 2007 +0200 (2007-06-29)
changeset 23519a4ffa756d8eb
parent 23518 6407d832da03
child 23520 483fe92f00c1
bug fixes to proof reconstruction
src/HOL/ATP_Linkup.thy
src/HOL/IsaMakefile
src/HOL/MetisExamples/Abstraction.thy
src/HOL/MetisExamples/BigO.thy
src/HOL/MetisExamples/set.thy
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/watcher.ML
     1.1 --- a/src/HOL/ATP_Linkup.thy	Fri Jun 29 16:05:00 2007 +0200
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Fri Jun 29 18:21:25 2007 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    ("Tools/res_hol_clause.ML")
     1.5    ("Tools/res_axioms.ML")
     1.6    ("Tools/res_reconstruct.ML")
     1.7 -  ("Tools/ATP/watcher.ML")
     1.8 +  ("Tools/watcher.ML")
     1.9    ("Tools/res_atp.ML")
    1.10    ("Tools/res_atp_provers.ML")
    1.11    ("Tools/res_atp_methods.ML")
    1.12 @@ -88,7 +88,7 @@
    1.13  use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
    1.14  use "Tools/res_hol_clause.ML"  --{*requires the combinators*}
    1.15  use "Tools/res_reconstruct.ML"
    1.16 -use "Tools/ATP/watcher.ML"
    1.17 +use "Tools/watcher.ML"
    1.18  use "Tools/res_atp.ML"
    1.19  
    1.20  setup ResAxioms.meson_method_setup
     2.1 --- a/src/HOL/IsaMakefile	Fri Jun 29 16:05:00 2007 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Jun 29 18:21:25 2007 +0200
     2.3 @@ -92,7 +92,7 @@
     2.4    Predicate.thy Product_Type.thy ROOT.ML Recdef.thy			\
     2.5    Record.thy Refute.thy Relation.thy Relation_Power.thy			\
     2.6    Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy	\
     2.7 -  Groebner_Basis.thy Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML	\
     2.8 +  Groebner_Basis.thy Tools/ATP/reduce_axiomsN.ML Tools/watcher.ML	\
     2.9    Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML		\
    2.10    Tools/Groebner_Basis/normalizer.ML					\
    2.11    Tools/Groebner_Basis/normalizer_data.ML Tools/Qelim/cooper.ML		\
     3.1 --- a/src/HOL/MetisExamples/Abstraction.thy	Fri Jun 29 16:05:00 2007 +0200
     3.2 +++ b/src/HOL/MetisExamples/Abstraction.thy	Fri Jun 29 18:21:25 2007 +0200
     3.3 @@ -75,19 +75,13 @@
     3.4  assume 1: "\<And>f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)"
     3.5  assume 2: "a \<notin> A \<or> a \<noteq> f b"
     3.6  have 3: "a \<in> A"
     3.7 -  by (metis SigmaD1 0)
     3.8 -have 4: "b \<in> llabs_subgoal_1 f a"
     3.9 -  by (metis SigmaD2 0)
    3.10 -have 5: "\<And>X1 X2. X2 -` {X1} = llabs_subgoal_1 X2 X1"
    3.11 -  by (metis 1 vimage_Collect_eq singleton_conv2)
    3.12 -have 6: "\<And>X1 X2 X3. X1 X2 = X3 \<or> X2 \<notin> llabs_subgoal_1 X1 X3"
    3.13 -  by (metis vimage_singleton_eq 5)
    3.14 -have 7: "f b \<noteq> a"
    3.15 -  by (metis 2 3)
    3.16 -have 8: "f b = a"
    3.17 -  by (metis 6 4)
    3.18 +  by (metis member2_def SigmaD1 0)
    3.19 +have 4: "f b \<noteq> a"
    3.20 +  by (metis 3 2)
    3.21 +have 5: "f b = a"
    3.22 +  by (metis Domain_Id Compl_UNIV_eq singleton_conv2 vimage_Collect_eq 1 vimage_singleton_eq SigmaD2 member2_def 0)
    3.23  show "False"
    3.24 -  by (metis 8 7)
    3.25 +  by (metis 5 4)
    3.26  qed finish_clausify
    3.27  
    3.28  
     4.1 --- a/src/HOL/MetisExamples/BigO.thy	Fri Jun 29 16:05:00 2007 +0200
     4.2 +++ b/src/HOL/MetisExamples/BigO.thy	Fri Jun 29 18:21:25 2007 +0200
     4.3 @@ -683,70 +683,30 @@
     4.4  (*Version 2: single-step proof*)
     4.5  proof (neg_clausify)
     4.6  fix x
     4.7 -assume 0: "\<And>mes_mb9\<Colon>'a.
     4.8 -   (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) mes_mb9
     4.9 -   \<le> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) mes_mb9"
    4.10 -assume 1: "\<And>mes_mb8\<Colon>'b\<Colon>ordered_idom.
    4.11 -   \<not> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) mes_mb8)
    4.12 -     \<le> mes_mb8 * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x mes_mb8)\<bar>"
    4.13 -have 2: "\<And>X3\<Colon>'a.
    4.14 -   (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) X3 =
    4.15 -   (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) X3 \<or>
    4.16 -   \<not> c * g X3 \<le> f X3"
    4.17 -  by (metis Lattices.min_max.less_eq_less_inf.antisym_intro 0)
    4.18 -have 3: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
    4.19 -   \<not> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>X3\<bar>)
    4.20 -     \<le> \<bar>X3 * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X3\<bar>)\<bar>"
    4.21 -  by (metis 1 Ring_and_Field.abs_mult)
    4.22 -have 4: "\<And>X3\<Colon>'b\<Colon>ordered_idom. (1\<Colon>'b\<Colon>ordered_idom) * X3 = X3"
    4.23 -  by (metis Ring_and_Field.mult_cancel_left2 Finite_Set.AC_mult.f.commute)
    4.24 -have 5: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 * (1\<Colon>'b\<Colon>ordered_idom) = X3"
    4.25 -  by (metis Ring_and_Field.mult_cancel_right2 Finite_Set.AC_mult.f.commute)
    4.26 -have 6: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
    4.27 -  by (metis Ring_and_Field.abs_mult_self Finite_Set.AC_mult.f.commute)
    4.28 -have 7: "\<And>X3\<Colon>'b\<Colon>ordered_idom. (0\<Colon>'b\<Colon>ordered_idom) \<le> X3 * X3"
    4.29 -  by (metis Ring_and_Field.zero_le_square Finite_Set.AC_mult.f.commute)
    4.30 -have 8: "(0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
    4.31 -  by (metis 7 Ring_and_Field.mult_cancel_left2)
    4.32 -have 9: "\<And>X3\<Colon>'b\<Colon>ordered_idom. X3 * X3 = \<bar>X3 * X3\<bar>"
    4.33 -  by (metis Ring_and_Field.abs_mult 6)
    4.34 -have 10: "\<bar>1\<Colon>'b\<Colon>ordered_idom\<bar> = (1\<Colon>'b\<Colon>ordered_idom)"
    4.35 -  by (metis 9 4)
    4.36 -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>"
    4.37 -  by (metis Ring_and_Field.abs_mult OrderedGroup.abs_idempotent 5)
    4.38 -have 12: "\<And>X3\<Colon>'b\<Colon>ordered_idom. \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar>"
    4.39 -  by (metis 11 10 5)
    4.40 -have 13: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom.
    4.41 -   X3 * (1\<Colon>'b\<Colon>ordered_idom) \<le> X1 \<or>
    4.42 -   \<not> \<bar>X3\<bar> \<le> X1 \<or> \<not> (0\<Colon>'b\<Colon>ordered_idom) \<le> (1\<Colon>'b\<Colon>ordered_idom)"
    4.43 -  by (metis OrderedGroup.abs_le_D1 Ring_and_Field.abs_mult_pos 5)
    4.44 -have 14: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom.
    4.45 -   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)"
    4.46 -  by (metis 13 5)
    4.47 -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"
    4.48 -  by (metis 14 8)
    4.49 -have 16: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
    4.50 -  by (metis 15 Orderings.linorder_class.less_eq_less.linear)
    4.51 -have 17: "\<And>X3\<Colon>'b\<Colon>ordered_idom.
    4.52 -   X3 * (g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>X3\<bar>)
    4.53 -   \<le> (f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X3\<bar>)"
    4.54 -  by (metis 3 16)
    4.55 -have 18: "(c\<Colon>'b\<Colon>ordered_idom) *
    4.56 -(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>c\<bar>) =
    4.57 -(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>c\<bar>)"
    4.58 -  by (metis 2 17)
    4.59 -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>"
    4.60 -  by (metis 15 Ring_and_Field.abs_le_mult Ring_and_Field.abs_mult)
    4.61 -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>"
    4.62 -  by (metis 19 12 12)
    4.63 -have 21: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X3\<Colon>'b\<Colon>ordered_idom. X3 * X1 \<le> \<bar>X3\<bar> * \<bar>X1\<bar>"
    4.64 -  by (metis 15 20)
    4.65 -have 22: "(f\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom)
    4.66 - ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a) \<bar>c\<Colon>'b\<Colon>ordered_idom\<bar>)
    4.67 -\<le> \<bar>c\<bar> * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>c\<bar>)\<bar>"
    4.68 -  by (metis 21 18)
    4.69 -show 23: "False"
    4.70 -  by (metis 22 1)
    4.71 +assume 0: "\<And>A\<Colon>'a\<Colon>type.
    4.72 +   (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) A
    4.73 +   \<le> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) A"
    4.74 +assume 1: "\<And>A\<Colon>'b\<Colon>ordered_idom.
    4.75 +   \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) A)
    4.76 +     \<le> A * \<bar>(g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x A)\<bar>"
    4.77 +have 2: "\<And>X2\<Colon>'a\<Colon>type.
    4.78 +   \<not> (c\<Colon>'b\<Colon>ordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) X2
    4.79 +     < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) X2"
    4.80 +  by (metis 0 linorder_not_le)
    4.81 +have 3: "\<And>X2\<Colon>'b\<Colon>ordered_idom.
    4.82 +   \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
    4.83 +     \<le> \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X2\<bar>)\<bar>"
    4.84 +  by (metis abs_mult 1)
    4.85 +have 4: "\<And>X2\<Colon>'b\<Colon>ordered_idom.
    4.86 +   \<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>
    4.87 +   < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X2\<bar>)"
    4.88 +  by (metis 3 linorder_not_less)
    4.89 +have 5: "\<And>X2\<Colon>'b\<Colon>ordered_idom.
    4.90 +   X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) ((x\<Colon>'b\<Colon>ordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
    4.91 +   < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>ordered_idom) (x \<bar>X2\<bar>)"
    4.92 +  by (metis abs_less_iff 4)
    4.93 +show "False"
    4.94 +  by (metis 2 5)
    4.95  qed
    4.96  
    4.97  
    4.98 @@ -1131,16 +1091,16 @@
    4.99  apply (simp add: bigo_def)
   4.100  proof (neg_clausify)
   4.101  assume 0: "(c\<Colon>'a\<Colon>ordered_field) \<noteq> (0\<Colon>'a\<Colon>ordered_field)"
   4.102 -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>"
   4.103 +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>"
   4.104  have 2: "(0\<Colon>'a\<Colon>ordered_field) = \<bar>c\<Colon>'a\<Colon>ordered_field\<bar> \<or>
   4.105  \<not> (1\<Colon>'a\<Colon>ordered_field) \<le> (1\<Colon>'a\<Colon>ordered_field)"
   4.106    by (metis 1 field_inverse)
   4.107  have 3: "\<bar>c\<Colon>'a\<Colon>ordered_field\<bar> = (0\<Colon>'a\<Colon>ordered_field)"
   4.108 -  by (metis 2 order_refl)
   4.109 +  by (metis linorder_neq_iff linorder_antisym_conv1 2)
   4.110  have 4: "(0\<Colon>'a\<Colon>ordered_field) = (c\<Colon>'a\<Colon>ordered_field)"
   4.111 -  by (metis OrderedGroup.abs_eq_0 3)
   4.112 -show 5: "False"
   4.113 -  by (metis 4 0)
   4.114 +  by (metis 3 abs_eq_0)
   4.115 +show "False"
   4.116 +  by (metis 0 4)
   4.117  qed
   4.118  
   4.119  lemma bigo_const4: "(c::'a::ordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
     5.1 --- a/src/HOL/MetisExamples/set.thy	Fri Jun 29 16:05:00 2007 +0200
     5.2 +++ b/src/HOL/MetisExamples/set.thy	Fri Jun 29 18:21:25 2007 +0200
     5.3 @@ -11,10 +11,11 @@
     5.4  
     5.5  lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
     5.6                 (S(x,y) | ~S(y,z) | Q(Z,Z))  &
     5.7 -               (Q(X,y) | ~Q(y,Z) | S(X,X))";
     5.8 -by metis;
     5.9 +               (Q(X,y) | ~Q(y,Z) | S(X,X))"
    5.10 +by metis
    5.11 +(*??But metis can't prove the single-step version...*)
    5.12  
    5.13 -(*??Single-step reconstruction fails due to "assume?"*)
    5.14 +
    5.15  
    5.16  lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
    5.17  by metis
    5.18 @@ -220,11 +221,11 @@
    5.19  proof (neg_clausify)
    5.20  fix x xa
    5.21  assume 0: "f (g x) = x"
    5.22 -assume 1: "\<And>mes_oip. mes_oip = x \<or> f (g mes_oip) \<noteq> mes_oip"
    5.23 -assume 2: "\<And>mes_oio. g (f (xa mes_oio)) = xa mes_oio \<or> g (f mes_oio) \<noteq> mes_oio"
    5.24 -assume 3: "\<And>mes_oio. g (f mes_oio) \<noteq> mes_oio \<or> xa mes_oio \<noteq> mes_oio"
    5.25 +assume 1: "\<And>A. A = x \<or> f (g A) \<noteq> A"
    5.26 +assume 2: "\<And>A. g (f (xa A)) = xa A \<or> g (f A) \<noteq> A"
    5.27 +assume 3: "\<And>A. g (f A) \<noteq> A \<or> xa A \<noteq> A"
    5.28  have 4: "\<And>X1. g (f X1) \<noteq> X1 \<or> g x \<noteq> X1"
    5.29 -  by (metis 3 2 1 2)
    5.30 +  by (metis 3 1 2)
    5.31  show "False"
    5.32    by (metis 4 0)
    5.33  qed
     6.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Jun 29 16:05:00 2007 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,397 +0,0 @@
     6.4 -(*  Title:      Watcher.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Claire Quigley
     6.7 -    Copyright   2004  University of Cambridge
     6.8 - *)
     6.9 -
    6.10 -(*  The watcher process starts a resolution process when it receives a     *)
    6.11 -(*  message from Isabelle                                                  *)
    6.12 -(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    6.13 -(*  and removes dead processes.  Also possible to kill all the resolution  *)
    6.14 -(*  processes currently running.                                           *)
    6.15 -
    6.16 -signature WATCHER =
    6.17 -sig
    6.18 -
    6.19 -(*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
    6.20 -(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
    6.21 -
    6.22 -val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit
    6.23 -
    6.24 -(* Send message to watcher to kill resolution provers *)
    6.25 -val callSlayer : TextIO.outstream -> unit
    6.26 -
    6.27 -(* Start a watcher and set up signal handlers*)
    6.28 -val createWatcher : 
    6.29 -	Proof.context * thm * string Vector.vector list ->
    6.30 -	TextIO.instream * TextIO.outstream * Posix.Process.pid
    6.31 -val killWatcher : Posix.Process.pid -> unit
    6.32 -val killChild  : ('a, 'b) Unix.proc -> OS.Process.status
    6.33 -val command_sep : char
    6.34 -val setting_sep : char
    6.35 -val reapAll : unit -> unit
    6.36 -end
    6.37 -
    6.38 -
    6.39 -
    6.40 -structure Watcher: WATCHER =
    6.41 -struct
    6.42 -
    6.43 -(*Field separators, used to pack items onto a text line*)
    6.44 -val command_sep = #"\t"
    6.45 -and setting_sep = #"%";
    6.46 -
    6.47 -val goals_being_watched = ref 0;
    6.48 -
    6.49 -val trace_path = Path.basic "watcher_trace";
    6.50 -
    6.51 -fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
    6.52 -              else ();
    6.53 -
    6.54 -(*Representation of a watcher process*)
    6.55 -type proc = {pid : Posix.Process.pid,
    6.56 -             instr : TextIO.instream,
    6.57 -             outstr : TextIO.outstream};
    6.58 -
    6.59 -(*Representation of a child (ATP) process*)
    6.60 -type cmdproc = {
    6.61 -        prover: string,       (* Name of the resolution prover used, e.g. "spass"*)
    6.62 -        file:  string,        (* The file containing the goal for the ATP to prove *)
    6.63 -        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    6.64 -        instr : TextIO.instream,     (*Output of the child process *)
    6.65 -        outstr : TextIO.outstream};  (*Input to the child process *)
    6.66 -
    6.67 -
    6.68 -fun fdReader (name : string, fd : Posix.IO.file_desc) =
    6.69 -	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    6.70 -
    6.71 -fun fdWriter (name, fd) =
    6.72 -          Posix.IO.mkTextWriter {
    6.73 -	      appendMode = false,
    6.74 -              initBlkMode = true,
    6.75 -              name = name,
    6.76 -              chunkSize=4096,
    6.77 -              fd = fd};
    6.78 -
    6.79 -fun openOutFD (name, fd) =
    6.80 -	  TextIO.mkOutstream (
    6.81 -	    TextIO.StreamIO.mkOutstream (
    6.82 -	      fdWriter (name, fd), IO.BLOCK_BUF));
    6.83 -
    6.84 -fun openInFD (name, fd) =
    6.85 -	  TextIO.mkInstream (
    6.86 -	    TextIO.StreamIO.mkInstream (
    6.87 -	      fdReader (name, fd), ""));
    6.88 -
    6.89 -
    6.90 -(*  Send request to Watcher for a vampire to be called for filename in arg*)
    6.91 -fun callResProver (toWatcherStr,  arg) =
    6.92 -      (TextIO.output (toWatcherStr, arg^"\n");
    6.93 -       TextIO.flushOut toWatcherStr)
    6.94 -
    6.95 -(*  Send request to Watcher for multiple provers to be called*)
    6.96 -fun callResProvers (toWatcherStr,  []) =
    6.97 -      (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
    6.98 -  | callResProvers (toWatcherStr,
    6.99 -                    (prover,proverCmd,settings,probfile)  ::  args) =
   6.100 -      (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile]));
   6.101 -       (*Uses a special character to separate items sent to watcher*)
   6.102 -       TextIO.output (toWatcherStr,
   6.103 -          space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
   6.104 -       inc goals_being_watched;
   6.105 -       TextIO.flushOut toWatcherStr;
   6.106 -       callResProvers (toWatcherStr,args))
   6.107 -
   6.108 -
   6.109 -(*Send message to watcher to kill currently running vampires. NOT USED and possibly
   6.110 -  buggy. Note that killWatcher kills the entire process group anyway.*)
   6.111 -fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
   6.112 -                            TextIO.flushOut toWatcherStr)
   6.113 -
   6.114 -
   6.115 -(* Get commands from Isabelle*)
   6.116 -fun getCmds (toParentStr, fromParentStr, cmdList) =
   6.117 -  let val thisLine = the_default "" (TextIO.inputLine fromParentStr)
   6.118 -  in
   6.119 -     trace("\nGot command from parent: " ^ thisLine);
   6.120 -     if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
   6.121 -     else if thisLine = "Kill children\n"
   6.122 -     then (TextIO.output (toParentStr,thisLine);
   6.123 -	   TextIO.flushOut toParentStr;
   6.124 -	   [("","Kill children",[],"")])
   6.125 -     else
   6.126 -       let val [prover,proverCmd,settingstr,probfile,_] =
   6.127 -                   String.tokens (fn c => c = command_sep) thisLine
   6.128 -           val settings = String.tokens (fn c => c = setting_sep) settingstr
   6.129 -       in
   6.130 -           trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd ^
   6.131 -                  "\n  problem file: " ^ probfile);
   6.132 -           getCmds (toParentStr, fromParentStr,
   6.133 -                    (prover, proverCmd, settings, probfile)::cmdList)
   6.134 -       end
   6.135 -       handle Bind =>
   6.136 -          (trace "\ngetCmds: command parsing failed!";
   6.137 -           getCmds (toParentStr, fromParentStr, cmdList))
   6.138 -  end
   6.139 -	
   6.140 -
   6.141 -(*Get Io-descriptor for polling of an input stream*)
   6.142 -fun getInIoDesc someInstr =
   6.143 -    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   6.144 -        val _ = TextIO.output (TextIO.stdOut, buf)
   6.145 -        val ioDesc =
   6.146 -	    case rd
   6.147 -	      of TextPrimIO.RD{ioDesc = SOME iod, ...} => SOME iod
   6.148 -	       | _ => NONE
   6.149 -     in (* since getting the reader will have terminated the stream, we need
   6.150 -	 * to build a new stream. *)
   6.151 -	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
   6.152 -	ioDesc
   6.153 -    end
   6.154 -
   6.155 -fun pollChild fromStr =
   6.156 -   case getInIoDesc fromStr of
   6.157 -     SOME iod =>
   6.158 -       (case OS.IO.pollDesc iod of
   6.159 -	  SOME pd =>
   6.160 -	      let val pd' = OS.IO.pollIn pd in
   6.161 -		case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
   6.162 -		    [] => false
   6.163 -		  | pd''::_ => OS.IO.isIn pd''
   6.164 -	      end
   6.165 -	 | NONE => false)
   6.166 -   | NONE => false
   6.167 -
   6.168 -
   6.169 -(*************************************)
   6.170 -(*  Set up a Watcher Process         *)
   6.171 -(*************************************)
   6.172 -
   6.173 -fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
   6.174 -
   6.175 -val killChildren = List.app (ignore o killChild o #proc_handle) : cmdproc list -> unit;
   6.176 -
   6.177 -fun killWatcher (toParentStr, procList) =
   6.178 -      (trace "\nWatcher timeout: Killing proof processes";
   6.179 -       TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   6.180 -       TextIO.flushOut toParentStr;
   6.181 -       killChildren procList;
   6.182 -       Posix.Process.exit 0w0);
   6.183 -
   6.184 -(* take an instream and poll its underlying reader for input *)
   6.185 -fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) =
   6.186 -  case OS.IO.pollDesc fromParentIOD of
   6.187 -     SOME pd =>
   6.188 -	(case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
   6.189 -	     [] => NONE
   6.190 -	   | pd''::_ => if OS.IO.isIn pd''
   6.191 -			then SOME (getCmds (toParentStr, fromParentStr, []))
   6.192 -			else NONE)
   6.193 -  | NONE => NONE;
   6.194 -
   6.195 -(*get the number of the subgoal from the filename: the last digit string*)
   6.196 -fun number_from_filename s =
   6.197 -  let val numbers = "xxx" :: String.tokens (not o Char.isDigit) s 
   6.198 -  in  valOf (Int.fromString (List.last numbers))  end
   6.199 -  handle Option => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
   6.200 -                    error ("Watcher could not read subgoal nunber! " ^ s));
   6.201 -
   6.202 -(*Call ATP.  Settings should be a list of strings  ["-t 300", "-m 100000"],
   6.203 -  which we convert below to ["-t", "300", "-m", "100000"] using String.tokens.
   6.204 -  Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and
   6.205 -  Vampire will reject the switches.*)
   6.206 -fun execCmds [] procList = procList
   6.207 -  | execCmds ((prover,proverCmd,settings,file)::cmds) procList  =
   6.208 -      let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
   6.209 -          val settings' = List.concat (map (String.tokens Char.isSpace) settings)
   6.210 -	  val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  =
   6.211 -	       Unix.execute(proverCmd, settings' @ [file])
   6.212 -	  val (instr, outstr) = Unix.streamsOf childhandle
   6.213 -	  val newProcList = {prover=prover, file=file, proc_handle=childhandle,
   6.214 -			     instr=instr, outstr=outstr} :: procList
   6.215 -	  val _ = trace ("\nFinished at " ^
   6.216 -			 Date.toString(Date.fromTimeLocal(Time.now())))
   6.217 -      in execCmds cmds newProcList end
   6.218 -
   6.219 -fun checkChildren (ctxt, th, thm_names_list) toParentStr children =
   6.220 -  let fun check [] = []  (* no children to check *)
   6.221 -	| check (child::children) =
   6.222 -	   let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
   6.223 -	       val _ = trace ("\nprobfile = " ^ file)
   6.224 -	       val sgno = number_from_filename file  (*subgoal number*)
   6.225 -	       val thm_names = List.nth(thm_names_list, sgno-1);
   6.226 -	       val ppid = Posix.ProcEnv.getppid()
   6.227 -	   in
   6.228 -	     if pollChild childIn
   6.229 -	     then (* check here for prover label on child*)
   6.230 -	       let val _ = trace ("\nInput available from child: " ^ file)
   6.231 -		   val childDone = (case prover of
   6.232 -		       "vampire" => ResReconstruct.checkVampProofFound
   6.233 -			    (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
   6.234 -		     | "E" => ResReconstruct.checkEProofFound
   6.235 -			    (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
   6.236 -		     | "spass" => ResReconstruct.checkSpassProofFound
   6.237 -			    (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
   6.238 -		     | _ => (trace ("\nBad prover! " ^ prover); true) )
   6.239 -		in
   6.240 -		 if childDone (*ATP has reported back (with success OR failure)*)
   6.241 -		 then (Unix.reap proc_handle;
   6.242 -		       if !Output.debugging then () else OS.FileSys.remove file;
   6.243 -		       check children)
   6.244 -		 else child :: check children
   6.245 -	      end
   6.246 -	    else (trace "\nNo child output";  child :: check children)
   6.247 -	   end
   6.248 -  in
   6.249 -    trace ("\nIn checkChildren, length of queue: " ^  Int.toString(length children));
   6.250 -    check children
   6.251 -  end;
   6.252 -
   6.253 -
   6.254 -fun setupWatcher (ctxt, th, thm_names_list) =
   6.255 -  let
   6.256 -    val checkc = checkChildren (ctxt, th, thm_names_list)
   6.257 -    val p1 = Posix.IO.pipe()   (*pipes for communication between parent and watcher*)
   6.258 -    val p2 = Posix.IO.pipe()
   6.259 -    (****** fork a watcher process and get it set up and going ******)
   6.260 -    fun startWatcher procList =
   6.261 -      case  Posix.Process.fork() of
   6.262 -         SOME pid => pid (* parent - i.e. main Isabelle process *)
   6.263 -       | NONE =>
   6.264 -          let            (* child - i.e. watcher  *)
   6.265 -	    val oldchildin = #infd p1
   6.266 -	    val fromParent = Posix.FileSys.wordToFD 0w0
   6.267 -	    val oldchildout = #outfd p2
   6.268 -	    val toParent = Posix.FileSys.wordToFD 0w1
   6.269 -	    val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   6.270 -	    val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   6.271 -	    val toParentStr = openOutFD ("_exec_out_parent", toParent)
   6.272 -	    val pid = Posix.ProcEnv.getpid()
   6.273 -	    val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
   6.274 -		     (*set process group id: allows killing all children*)
   6.275 -	    val () = trace "\nsubgoals forked to startWatcher"
   6.276 -	    val limit = ref 200;  (*don't let watcher run forever*)
   6.277 -	    (*Watcher Loop : Check running ATP processes for output*)
   6.278 -	    fun keepWatching procList =
   6.279 -	      (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^
   6.280 -				"  length(procList) = " ^ Int.toString(length procList));
   6.281 -	       OS.Process.sleep (Time.fromMilliseconds 100);  limit := !limit - 1;
   6.282 -	       if !limit < 0 then killWatcher (toParentStr, procList)
   6.283 -	       else
   6.284 -	       case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of
   6.285 -		  SOME [(_,"Kill children",_,_)] =>
   6.286 -		    (trace "\nReceived Kill command";
   6.287 -		     killChildren procList; keepWatching [])
   6.288 -		| SOME cmds => (*  deal with commands from Isabelle process *)
   6.289 -		    if length procList < 40 then    (* Execute locally  *)
   6.290 -		      let val _ = trace("\nCommands from parent: " ^
   6.291 -					Int.toString(length cmds))
   6.292 -			  val newProcList' = checkc toParentStr (execCmds cmds procList)
   6.293 -		      in trace "\nCommands executed"; keepWatching newProcList' end
   6.294 -		    else  (* Execute remotely [FIXME: NOT REALLY]  *)
   6.295 -		      let val newProcList' = checkc toParentStr (execCmds cmds procList)
   6.296 -		      in keepWatching newProcList' end
   6.297 -		| NONE => (* No new input from Isabelle *)
   6.298 -		    (trace "\nNothing from parent...";
   6.299 -		     keepWatching(checkc toParentStr procList)))
   6.300 -	     handle exn => (*FIXME: exn handler is too general!*)
   6.301 -	       (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
   6.302 -		keepWatching procList);
   6.303 -	  in
   6.304 -	    (*** Sort out pipes ********)
   6.305 -	    Posix.IO.close (#outfd p1);  Posix.IO.close (#infd p2);
   6.306 -	    Posix.IO.dup2{old = oldchildin, new = fromParent};
   6.307 -	    Posix.IO.close oldchildin;
   6.308 -	    Posix.IO.dup2{old = oldchildout, new = toParent};
   6.309 -	    Posix.IO.close oldchildout;
   6.310 -	    keepWatching (procList)
   6.311 -	  end;
   6.312 -
   6.313 -    val _ = TextIO.flushOut TextIO.stdOut
   6.314 -    val pid = startWatcher []
   6.315 -    (* communication streams to watcher*)
   6.316 -    val instr = openInFD ("_exec_in", #infd p2)
   6.317 -    val outstr = openOutFD ("_exec_out", #outfd p1)
   6.318 -  in
   6.319 -   (* close the child-side fds*)
   6.320 -    Posix.IO.close (#outfd p2);  Posix.IO.close (#infd p1);
   6.321 -    (* set the fds close on exec *)
   6.322 -    Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   6.323 -    Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   6.324 -    {pid = pid, instr = instr, outstr = outstr}
   6.325 -  end;
   6.326 -
   6.327 -
   6.328 -
   6.329 -(**********************************************************)
   6.330 -(* Start a watcher and set up signal handlers             *)
   6.331 -(**********************************************************)
   6.332 -
   6.333 -(*Signal handler to tidy away zombie processes*)
   6.334 -fun reapAll() =
   6.335 -     (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
   6.336 -	  SOME _ => reapAll() | NONE => ())
   6.337 -     handle OS.SysErr _ => ()
   6.338 -
   6.339 -(*FIXME: does the main process need something like this?
   6.340 -    IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*)
   6.341 -
   6.342 -fun killWatcher pid =
   6.343 -  (goals_being_watched := 0;
   6.344 -   Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
   6.345 -   reapAll());
   6.346 -
   6.347 -fun reapWatcher(pid, instr, outstr) = ignore
   6.348 -  (TextIO.closeIn instr; TextIO.closeOut outstr;
   6.349 -   Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
   6.350 -  handle OS.SysErr _ => ()
   6.351 -
   6.352 -fun string_of_subgoal th i =
   6.353 -    string_of_cterm (List.nth(cprems_of th, i-1))
   6.354 -    handle Subscript => "Subgoal number out of range!"
   6.355 -
   6.356 -fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
   6.357 -
   6.358 -fun createWatcher (ctxt, th, thm_names_list) =
   6.359 - let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
   6.360 -     fun decr_watched() =
   6.361 -	  (goals_being_watched := !goals_being_watched - 1;
   6.362 -	   if !goals_being_watched = 0
   6.363 -	   then
   6.364 -	     (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid));
   6.365 -	      killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
   6.366 -	    else ())
   6.367 -     fun proofHandler _ =
   6.368 -       let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid)
   6.369 -           val outcome = ResReconstruct.restore_newlines (the_default "" (TextIO.inputLine childin))
   6.370 -	   val probfile = the_default "" (TextIO.inputLine childin)
   6.371 -	   val sgno = number_from_filename probfile
   6.372 -	   val text = string_of_subgoal th sgno
   6.373 -	   fun report s = priority ("Subgoal " ^ Int.toString sgno ^ ": " ^ s);
   6.374 -       in
   6.375 -	 Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
   6.376 -		       "\"\nprobfile = " ^ probfile ^
   6.377 -		       "\nGoals being watched: "^  Int.toString (!goals_being_watched)));
   6.378 -	 if String.isPrefix "Invalid" outcome
   6.379 -	 then (report ("Subgoal is not provable:\n" ^ text);
   6.380 -	       decr_watched())
   6.381 -	 else if String.isPrefix "Failure" outcome
   6.382 -	 then (report ("Proof attempt failed:\n" ^ text);
   6.383 -	       decr_watched())
   6.384 -	(* print out a list of rules used from clasimpset*)
   6.385 -	 else if String.isPrefix "Success" outcome
   6.386 -	 then (report (outcome ^ text);
   6.387 -	       decr_watched())
   6.388 -	  (* if proof translation failed *)
   6.389 -	 else if String.isPrefix "Translation failed" outcome
   6.390 -	 then (report (outcome ^ text);
   6.391 -	       decr_watched())
   6.392 -	 else (report "System error in proof handler";
   6.393 -	       decr_watched())
   6.394 -       end
   6.395 - in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));
   6.396 -    IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
   6.397 -    (childin, childout, childpid)
   6.398 -  end
   6.399 -
   6.400 -end (* structure Watcher *)
     7.1 --- a/src/HOL/Tools/res_reconstruct.ML	Fri Jun 29 16:05:00 2007 +0200
     7.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Fri Jun 29 18:21:25 2007 +0200
     7.3 @@ -228,7 +228,7 @@
     7.4                      case strip_prefix ResClause.schematic_var_prefix a of
     7.5                          SOME b => make_var (b,T)
     7.6                        | NONE => make_var (a,T)    (*Variable from the ATP, say X1*)
     7.7 -              in  list_comb (opr, List.map (term_of_stree [] thy) (args@ts))  end;
     7.8 +              in  list_comb (opr, List.map (term_of_stree [] thy) (ts@args))  end;
     7.9  
    7.10  (*Type class literal applied to a type. Returns triple of polarity, class, type.*)
    7.11  fun constraint_of_stree pol (Br("c_Not",[t])) = constraint_of_stree (not pol) t
    7.12 @@ -279,21 +279,18 @@
    7.13  
    7.14  (*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints.
    7.15    vt0 holds the initial sort constraints, from the conjecture clauses.*)
    7.16 -fun clause_of_strees_aux ctxt vt0 ts =
    7.17 +fun clause_of_strees ctxt vt0 ts =
    7.18    let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in
    7.19      singleton (ProofContext.infer_types ctxt) (TypeInfer.constrain (fix_sorts vt dt) HOLogic.boolT)
    7.20    end;
    7.21  
    7.22 -(*Quantification over a list of Vars. FUXNE: for term.ML??*)
    7.23 +(*Quantification over a list of Vars. FIXME: for term.ML??*)
    7.24  fun list_all_var ([], t: term) = t
    7.25    | list_all_var ((v as Var(ix,T)) :: vars, t) =
    7.26        (all T) $ Abs(string_of_indexname ix, T, abstract_over (v, list_all_var (vars,t)));
    7.27  
    7.28  fun gen_all_vars t = list_all_var (term_vars t, t);
    7.29  
    7.30 -fun clause_of_strees thy vt0 ts =
    7.31 -  gen_all_vars (HOLogic.mk_Trueprop (clause_of_strees_aux thy vt0 ts));
    7.32 -
    7.33  fun ints_of_stree_aux (Int n, ns) = n::ns
    7.34    | ints_of_stree_aux (Br(_,ts), ns) = foldl ints_of_stree_aux ns ts;
    7.35  
    7.36 @@ -334,22 +331,62 @@
    7.37  
    7.38  fun dest_disj t = dest_disj_aux t [];
    7.39  
    7.40 -(*Remove types from a term, to eliminate the randomness of type inference*)
    7.41 -fun smash_types (Const(a,_)) = Const(a,dummyT)
    7.42 -  | smash_types (Free(a,_)) = Free(a,dummyT)
    7.43 -  | smash_types (Var(a,_)) = Var(a,dummyT)
    7.44 -  | smash_types (f$t) = smash_types f $ smash_types t
    7.45 -  | smash_types t = t;
    7.46 +(** Finding a matching assumption. The literals may be permuted, and variable names
    7.47 +    may disagree. We have to try all combinations of literals (quadratic!) and 
    7.48 +    match up the variable names consistently. **)
    7.49 +
    7.50 +fun strip_alls_aux n (Const("all",_)$Abs(a,T,t))  =  
    7.51 +      strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t))
    7.52 +  | strip_alls_aux _ t  =  t;
    7.53 +
    7.54 +val strip_alls = strip_alls_aux 0;
    7.55 +
    7.56 +exception MATCH_LITERAL;
    7.57  
    7.58 -val sort_lits = sort Term.fast_term_ord o dest_disj o
    7.59 -                smash_types o HOLogic.dest_Trueprop o strip_all_body;
    7.60 +(*Ignore types: they are not to be trusted...*)
    7.61 +fun match_literal (t1$u1) (t2$u2) env =
    7.62 +      match_literal t1 t2 (match_literal u1 u2 env)
    7.63 +  | match_literal (Abs (_,_,t1)) (Abs (_,_,t2)) env = 
    7.64 +      match_literal t1 t2 env
    7.65 +  | match_literal (Bound i1) (Bound i2) env = 
    7.66 +      if i1=i2 then env else raise MATCH_LITERAL
    7.67 +  | match_literal (Const(a1,_)) (Const(a2,_)) env = 
    7.68 +      if a1=a2 then env else raise MATCH_LITERAL
    7.69 +  | match_literal (Free(a1,_)) (Free(a2,_)) env = 
    7.70 +      if a1=a2 then env else raise MATCH_LITERAL
    7.71 +  | match_literal (Var(ix1,_)) (Var(ix2,_)) env = insert (op =) (ix1,ix2) env
    7.72 +  | match_literal _ _ env = raise MATCH_LITERAL;
    7.73 +
    7.74 +(*Checking that all variable associations are unique. The list env contains no
    7.75 +  repetitions, but does it contain say (x,y) and (y,y)? *)
    7.76 +fun good env = 
    7.77 +  let val (xs,ys) = ListPair.unzip env
    7.78 +  in  not (has_duplicates (op=) xs orelse has_duplicates (op=) ys)  end;
    7.79 +
    7.80 +(*Match one list of literals against another, ignoring types and the order of
    7.81 +  literals. Sorting is unreliable because we don't have types or variable names.*)
    7.82 +fun matches_aux _ [] [] = true
    7.83 +  | matches_aux env (lit::lits) ts =
    7.84 +      let fun match1 us [] = false
    7.85 +            | match1 us (t::ts) =
    7.86 +                let val env' = match_literal lit t env
    7.87 +                in  (good env' andalso matches_aux env' lits (us@ts)) orelse 
    7.88 +                    match1 (t::us) ts  
    7.89 +                end
    7.90 +                handle MATCH_LITERAL => match1 (t::us) ts
    7.91 +      in  match1 [] ts  end; 
    7.92 +
    7.93 +(*Is this length test useful?*)
    7.94 +fun matches (lits1,lits2) = 
    7.95 +  length lits1 = length lits2  andalso  
    7.96 +  matches_aux [] (map Envir.eta_contract lits1) (map Envir.eta_contract lits2);
    7.97  
    7.98  fun permuted_clause t =
    7.99 -  let val lits = sort_lits t
   7.100 +  let val lits = dest_disj t
   7.101        fun perm [] = NONE
   7.102          | perm (ctm::ctms) =
   7.103 -            if forall (op aconv) (ListPair.zip (lits, sort_lits ctm)) then SOME ctm
   7.104 -            else perm ctms
   7.105 +            if matches (lits, dest_disj (HOLogic.dest_Trueprop (strip_alls ctm)))
   7.106 +            then SOME ctm else perm ctms
   7.107    in perm end;
   7.108  
   7.109  fun have_or_show "show " lname = "show \""
   7.110 @@ -364,7 +401,7 @@
   7.111                  SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
   7.112                | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n")  (*no match!!*)
   7.113          | doline have (lname, t, deps) =
   7.114 -            have_or_show have lname ^ string_of t ^
   7.115 +            have_or_show have lname ^ string_of (gen_all_vars (HOLogic.mk_Trueprop t)) ^
   7.116              "\"\n  by (metis " ^ space_implode " " deps ^ ")\n"
   7.117        fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
   7.118          | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
   7.119 @@ -373,7 +410,7 @@
   7.120  fun notequal t (_,t',_) = not (t aconv t');
   7.121  
   7.122  (*No "real" literals means only type information*)
   7.123 -fun eq_types t = t aconv (HOLogic.mk_Trueprop HOLogic.true_const);
   7.124 +fun eq_types t = t aconv HOLogic.true_const;
   7.125  
   7.126  fun replace_dep (old:int, new) dep = if dep=old then new else [dep];
   7.127  
   7.128 @@ -465,16 +502,18 @@
   7.129  
   7.130  val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c);
   7.131  
   7.132 -(*The output to the watcher must be a SINGLE line...clearly \t must not be used.*)
   7.133 -val encode_newlines = String.translate (fn c => if c = #"\n" then "\t" else str c);
   7.134 -val restore_newlines = String.translate (fn c => if c = #"\t" then "\n" else str c);
   7.135 +val txt_path = Path.ext "txt" o Path.explode o nospaces;
   7.136  
   7.137  fun signal_success probfile toParent ppid msg =
   7.138 -  (trace ("\nReporting Success for " ^ probfile ^ "\n" ^ msg);
   7.139 -   TextIO.output (toParent, "Success. " ^ encode_newlines msg ^ "\n");
   7.140 -   TextIO.output (toParent, probfile ^ "\n");
   7.141 -   TextIO.flushOut toParent;
   7.142 -   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
   7.143 +  let val _ = trace ("\nReporting Success for " ^ probfile ^ "\n" ^ msg)
   7.144 +  in
   7.145 +    (*We write the proof to a file because sending very long lines may fail...*)
   7.146 +    File.write (txt_path probfile) msg;
   7.147 +    TextIO.output (toParent, "Success.\n");
   7.148 +    TextIO.output (toParent, probfile ^ "\n");
   7.149 +    TextIO.flushOut toParent;
   7.150 +    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
   7.151 +  end;
   7.152  
   7.153  fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names =
   7.154    let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/watcher.ML	Fri Jun 29 18:21:25 2007 +0200
     8.3 @@ -0,0 +1,402 @@
     8.4 +(*  Title:      Watcher.ML
     8.5 +    ID:         $Id$
     8.6 +    Author:     Claire Quigley
     8.7 +    Copyright   2004  University of Cambridge
     8.8 + *)
     8.9 +
    8.10 +(*  The watcher process starts a resolution process when it receives a     *)
    8.11 +(*  message from Isabelle                                                  *)
    8.12 +(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    8.13 +(*  and removes dead processes.  Also possible to kill all the resolution  *)
    8.14 +(*  processes currently running.                                           *)
    8.15 +
    8.16 +signature WATCHER =
    8.17 +sig
    8.18 +
    8.19 +(*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
    8.20 +(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
    8.21 +
    8.22 +val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit
    8.23 +
    8.24 +(* Send message to watcher to kill resolution provers *)
    8.25 +val callSlayer : TextIO.outstream -> unit
    8.26 +
    8.27 +(* Start a watcher and set up signal handlers*)
    8.28 +val createWatcher : 
    8.29 +	Proof.context * thm * string Vector.vector list ->
    8.30 +	TextIO.instream * TextIO.outstream * Posix.Process.pid
    8.31 +val killWatcher : Posix.Process.pid -> unit
    8.32 +val killChild  : ('a, 'b) Unix.proc -> OS.Process.status
    8.33 +val command_sep : char
    8.34 +val setting_sep : char
    8.35 +val reapAll : unit -> unit
    8.36 +end
    8.37 +
    8.38 +
    8.39 +
    8.40 +structure Watcher: WATCHER =
    8.41 +struct
    8.42 +
    8.43 +(*Field separators, used to pack items onto a text line*)
    8.44 +val command_sep = #"\t"
    8.45 +and setting_sep = #"%";
    8.46 +
    8.47 +val goals_being_watched = ref 0;
    8.48 +
    8.49 +val trace_path = Path.basic "watcher_trace";
    8.50 +
    8.51 +fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
    8.52 +              else ();
    8.53 +
    8.54 +(*Representation of a watcher process*)
    8.55 +type proc = {pid : Posix.Process.pid,
    8.56 +             instr : TextIO.instream,
    8.57 +             outstr : TextIO.outstream};
    8.58 +
    8.59 +(*Representation of a child (ATP) process*)
    8.60 +type cmdproc = {
    8.61 +        prover: string,       (* Name of the resolution prover used, e.g. "spass"*)
    8.62 +        file:  string,        (* The file containing the goal for the ATP to prove *)
    8.63 +        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    8.64 +        instr : TextIO.instream,     (*Output of the child process *)
    8.65 +        outstr : TextIO.outstream};  (*Input to the child process *)
    8.66 +
    8.67 +
    8.68 +fun fdReader (name : string, fd : Posix.IO.file_desc) =
    8.69 +	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    8.70 +
    8.71 +fun fdWriter (name, fd) =
    8.72 +          Posix.IO.mkTextWriter {
    8.73 +	      appendMode = false,
    8.74 +              initBlkMode = true,
    8.75 +              name = name,
    8.76 +              chunkSize=4096,
    8.77 +              fd = fd};
    8.78 +
    8.79 +fun openOutFD (name, fd) =
    8.80 +	  TextIO.mkOutstream (
    8.81 +	    TextIO.StreamIO.mkOutstream (
    8.82 +	      fdWriter (name, fd), IO.BLOCK_BUF));
    8.83 +
    8.84 +fun openInFD (name, fd) =
    8.85 +	  TextIO.mkInstream (
    8.86 +	    TextIO.StreamIO.mkInstream (
    8.87 +	      fdReader (name, fd), ""));
    8.88 +
    8.89 +
    8.90 +(*  Send request to Watcher for a vampire to be called for filename in arg*)
    8.91 +fun callResProver (toWatcherStr,  arg) =
    8.92 +      (TextIO.output (toWatcherStr, arg^"\n");
    8.93 +       TextIO.flushOut toWatcherStr)
    8.94 +
    8.95 +(*  Send request to Watcher for multiple provers to be called*)
    8.96 +fun callResProvers (toWatcherStr,  []) =
    8.97 +      (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
    8.98 +  | callResProvers (toWatcherStr,
    8.99 +                    (prover,proverCmd,settings,probfile)  ::  args) =
   8.100 +      (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile]));
   8.101 +       (*Uses a special character to separate items sent to watcher*)
   8.102 +       TextIO.output (toWatcherStr,
   8.103 +          space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
   8.104 +       inc goals_being_watched;
   8.105 +       TextIO.flushOut toWatcherStr;
   8.106 +       callResProvers (toWatcherStr,args))
   8.107 +
   8.108 +
   8.109 +(*Send message to watcher to kill currently running vampires. NOT USED and possibly
   8.110 +  buggy. Note that killWatcher kills the entire process group anyway.*)
   8.111 +fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
   8.112 +                            TextIO.flushOut toWatcherStr)
   8.113 +
   8.114 +
   8.115 +(* Get commands from Isabelle*)
   8.116 +fun getCmds (toParentStr, fromParentStr, cmdList) =
   8.117 +  let val thisLine = the_default "" (TextIO.inputLine fromParentStr)
   8.118 +  in
   8.119 +     trace("\nGot command from parent: " ^ thisLine);
   8.120 +     if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
   8.121 +     else if thisLine = "Kill children\n"
   8.122 +     then (TextIO.output (toParentStr,thisLine);
   8.123 +	   TextIO.flushOut toParentStr;
   8.124 +	   [("","Kill children",[],"")])
   8.125 +     else
   8.126 +       let val [prover,proverCmd,settingstr,probfile,_] =
   8.127 +                   String.tokens (fn c => c = command_sep) thisLine
   8.128 +           val settings = String.tokens (fn c => c = setting_sep) settingstr
   8.129 +       in
   8.130 +           trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd ^
   8.131 +                  "\n  problem file: " ^ probfile);
   8.132 +           getCmds (toParentStr, fromParentStr,
   8.133 +                    (prover, proverCmd, settings, probfile)::cmdList)
   8.134 +       end
   8.135 +       handle Bind =>
   8.136 +          (trace "\ngetCmds: command parsing failed!";
   8.137 +           getCmds (toParentStr, fromParentStr, cmdList))
   8.138 +  end
   8.139 +	
   8.140 +
   8.141 +(*Get Io-descriptor for polling of an input stream*)
   8.142 +fun getInIoDesc someInstr =
   8.143 +    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   8.144 +        val _ = TextIO.output (TextIO.stdOut, buf)
   8.145 +        val ioDesc =
   8.146 +	    case rd
   8.147 +	      of TextPrimIO.RD{ioDesc = SOME iod, ...} => SOME iod
   8.148 +	       | _ => NONE
   8.149 +     in (* since getting the reader will have terminated the stream, we need
   8.150 +	 * to build a new stream. *)
   8.151 +	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
   8.152 +	ioDesc
   8.153 +    end
   8.154 +
   8.155 +fun pollChild fromStr =
   8.156 +   case getInIoDesc fromStr of
   8.157 +     SOME iod =>
   8.158 +       (case OS.IO.pollDesc iod of
   8.159 +	  SOME pd =>
   8.160 +	      let val pd' = OS.IO.pollIn pd in
   8.161 +		case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
   8.162 +		    [] => false
   8.163 +		  | pd''::_ => OS.IO.isIn pd''
   8.164 +	      end
   8.165 +	 | NONE => false)
   8.166 +   | NONE => false
   8.167 +
   8.168 +
   8.169 +(*************************************)
   8.170 +(*  Set up a Watcher Process         *)
   8.171 +(*************************************)
   8.172 +
   8.173 +fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
   8.174 +
   8.175 +val killChildren = List.app (ignore o killChild o #proc_handle) : cmdproc list -> unit;
   8.176 +
   8.177 +fun killWatcher (toParentStr, procList) =
   8.178 +      (trace "\nWatcher timeout: Killing proof processes";
   8.179 +       TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   8.180 +       TextIO.flushOut toParentStr;
   8.181 +       killChildren procList;
   8.182 +       Posix.Process.exit 0w0);
   8.183 +
   8.184 +(* take an instream and poll its underlying reader for input *)
   8.185 +fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) =
   8.186 +  case OS.IO.pollDesc fromParentIOD of
   8.187 +     SOME pd =>
   8.188 +	(case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
   8.189 +	     [] => NONE
   8.190 +	   | pd''::_ => if OS.IO.isIn pd''
   8.191 +			then SOME (getCmds (toParentStr, fromParentStr, []))
   8.192 +			else NONE)
   8.193 +  | NONE => NONE;
   8.194 +
   8.195 +(*get the number of the subgoal from the filename: the last digit string*)
   8.196 +fun number_from_filename s =
   8.197 +  let val numbers = "xxx" :: String.tokens (not o Char.isDigit) s 
   8.198 +  in  valOf (Int.fromString (List.last numbers))  end
   8.199 +  handle Option => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
   8.200 +                    error ("Watcher could not read subgoal nunber! " ^ s));
   8.201 +
   8.202 +(*Call ATP.  Settings should be a list of strings  ["-t 300", "-m 100000"],
   8.203 +  which we convert below to ["-t", "300", "-m", "100000"] using String.tokens.
   8.204 +  Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and
   8.205 +  Vampire will reject the switches.*)
   8.206 +fun execCmds [] procList = procList
   8.207 +  | execCmds ((prover,proverCmd,settings,file)::cmds) procList  =
   8.208 +      let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
   8.209 +          val settings' = List.concat (map (String.tokens Char.isSpace) settings)
   8.210 +	  val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  =
   8.211 +	       Unix.execute(proverCmd, settings' @ [file])
   8.212 +	  val (instr, outstr) = Unix.streamsOf childhandle
   8.213 +	  val newProcList = {prover=prover, file=file, proc_handle=childhandle,
   8.214 +			     instr=instr, outstr=outstr} :: procList
   8.215 +	  val _ = trace ("\nFinished at " ^
   8.216 +			 Date.toString(Date.fromTimeLocal(Time.now())))
   8.217 +      in execCmds cmds newProcList end
   8.218 +
   8.219 +fun checkChildren (ctxt, th, thm_names_list) toParentStr children =
   8.220 +  let fun check [] = []  (* no children to check *)
   8.221 +	| check (child::children) =
   8.222 +	   let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
   8.223 +	       val _ = trace ("\nprobfile = " ^ file)
   8.224 +	       val sgno = number_from_filename file  (*subgoal number*)
   8.225 +	       val thm_names = List.nth(thm_names_list, sgno-1);
   8.226 +	       val ppid = Posix.ProcEnv.getppid()
   8.227 +	   in
   8.228 +	     if pollChild childIn
   8.229 +	     then (* check here for prover label on child*)
   8.230 +	       let val _ = trace ("\nInput available from child: " ^ file)
   8.231 +		   val childDone = (case prover of
   8.232 +		       "vampire" => ResReconstruct.checkVampProofFound
   8.233 +			    (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
   8.234 +		     | "E" => ResReconstruct.checkEProofFound
   8.235 +			    (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
   8.236 +		     | "spass" => ResReconstruct.checkSpassProofFound
   8.237 +			    (childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
   8.238 +		     | _ => (trace ("\nBad prover! " ^ prover); true) )
   8.239 +		in
   8.240 +		 if childDone (*ATP has reported back (with success OR failure)*)
   8.241 +		 then (Unix.reap proc_handle;
   8.242 +		       if !Output.debugging then () else OS.FileSys.remove file;
   8.243 +		       check children)
   8.244 +		 else child :: check children
   8.245 +	      end
   8.246 +	    else (trace "\nNo child output";  child :: check children)
   8.247 +	   end
   8.248 +  in
   8.249 +    trace ("\nIn checkChildren, length of queue: " ^  Int.toString(length children));
   8.250 +    check children
   8.251 +  end;
   8.252 +
   8.253 +
   8.254 +fun setupWatcher (ctxt, th, thm_names_list) =
   8.255 +  let
   8.256 +    val checkc = checkChildren (ctxt, th, thm_names_list)
   8.257 +    val p1 = Posix.IO.pipe()   (*pipes for communication between parent and watcher*)
   8.258 +    val p2 = Posix.IO.pipe()
   8.259 +    (****** fork a watcher process and get it set up and going ******)
   8.260 +    fun startWatcher procList =
   8.261 +      case  Posix.Process.fork() of
   8.262 +         SOME pid => pid (* parent - i.e. main Isabelle process *)
   8.263 +       | NONE =>
   8.264 +          let            (* child - i.e. watcher  *)
   8.265 +	    val oldchildin = #infd p1
   8.266 +	    val fromParent = Posix.FileSys.wordToFD 0w0
   8.267 +	    val oldchildout = #outfd p2
   8.268 +	    val toParent = Posix.FileSys.wordToFD 0w1
   8.269 +	    val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   8.270 +	    val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   8.271 +	    val toParentStr = openOutFD ("_exec_out_parent", toParent)
   8.272 +	    val pid = Posix.ProcEnv.getpid()
   8.273 +	    val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
   8.274 +		     (*set process group id: allows killing all children*)
   8.275 +	    val () = trace "\nsubgoals forked to startWatcher"
   8.276 +	    val limit = ref 200;  (*don't let watcher run forever*)
   8.277 +	    (*Watcher Loop : Check running ATP processes for output*)
   8.278 +	    fun keepWatching procList =
   8.279 +	      (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^
   8.280 +				"  length(procList) = " ^ Int.toString(length procList));
   8.281 +	       OS.Process.sleep (Time.fromMilliseconds 100);  limit := !limit - 1;
   8.282 +	       if !limit < 0 then killWatcher (toParentStr, procList)
   8.283 +	       else
   8.284 +	       case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of
   8.285 +		  SOME [(_,"Kill children",_,_)] =>
   8.286 +		    (trace "\nReceived Kill command";
   8.287 +		     killChildren procList; keepWatching [])
   8.288 +		| SOME cmds => (*  deal with commands from Isabelle process *)
   8.289 +		      let val _ = trace("\nCommands from parent: " ^
   8.290 +					Int.toString(length cmds))
   8.291 +			  val newProcList' = checkc toParentStr (execCmds cmds procList)
   8.292 +		      in trace "\nCommands executed"; keepWatching newProcList' end
   8.293 +		| NONE => (* No new input from Isabelle *)
   8.294 +		    (trace "\nNothing from parent...";
   8.295 +		     keepWatching(checkc toParentStr procList)))
   8.296 +	     handle exn => (*FIXME: exn handler is too general!*)
   8.297 +	       (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
   8.298 +		keepWatching procList);
   8.299 +	  in
   8.300 +	    (*** Sort out pipes ********)
   8.301 +	    Posix.IO.close (#outfd p1);  Posix.IO.close (#infd p2);
   8.302 +	    Posix.IO.dup2{old = oldchildin, new = fromParent};
   8.303 +	    Posix.IO.close oldchildin;
   8.304 +	    Posix.IO.dup2{old = oldchildout, new = toParent};
   8.305 +	    Posix.IO.close oldchildout;
   8.306 +	    keepWatching (procList)
   8.307 +	  end;
   8.308 +
   8.309 +    val _ = TextIO.flushOut TextIO.stdOut
   8.310 +    val pid = startWatcher []
   8.311 +    (* communication streams to watcher*)
   8.312 +    val instr = openInFD ("_exec_in", #infd p2)
   8.313 +    val outstr = openOutFD ("_exec_out", #outfd p1)
   8.314 +  in
   8.315 +   (* close the child-side fds*)
   8.316 +    Posix.IO.close (#outfd p2);  Posix.IO.close (#infd p1);
   8.317 +    (* set the fds close on exec *)
   8.318 +    Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   8.319 +    Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   8.320 +    {pid = pid, instr = instr, outstr = outstr}
   8.321 +  end;
   8.322 +
   8.323 +
   8.324 +
   8.325 +(**********************************************************)
   8.326 +(* Start a watcher and set up signal handlers             *)
   8.327 +(**********************************************************)
   8.328 +
   8.329 +(*Signal handler to tidy away zombie processes*)
   8.330 +fun reapAll() =
   8.331 +     (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
   8.332 +	  SOME _ => reapAll() | NONE => ())
   8.333 +     handle OS.SysErr _ => ()
   8.334 +
   8.335 +(*FIXME: does the main process need something like this?
   8.336 +    IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*)
   8.337 +
   8.338 +fun killWatcher pid =
   8.339 +  (goals_being_watched := 0;
   8.340 +   Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
   8.341 +   reapAll());
   8.342 +
   8.343 +fun reapWatcher(pid, instr, outstr) = ignore
   8.344 +  (TextIO.closeIn instr; TextIO.closeOut outstr;
   8.345 +   Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
   8.346 +  handle OS.SysErr _ => ()
   8.347 +
   8.348 +fun string_of_subgoal th i =
   8.349 +    string_of_cterm (List.nth(cprems_of th, i-1))
   8.350 +    handle Subscript => "Subgoal number out of range!"
   8.351 +
   8.352 +fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
   8.353 +
   8.354 +fun read_proof probfile =
   8.355 +  let val p = ResReconstruct.txt_path probfile
   8.356 +      val _ = trace("\nReading proof from file " ^ Path.implode p)
   8.357 +      val msg = File.read p 
   8.358 +      val _ = trace("\nProof:\n" ^ msg)
   8.359 +  in  if !Output.debugging then () else File.rm p;  msg  end;
   8.360 +
   8.361 +fun createWatcher (ctxt, th, thm_names_list) =
   8.362 + let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
   8.363 +     fun decr_watched() =
   8.364 +	  (goals_being_watched := !goals_being_watched - 1;
   8.365 +	   if !goals_being_watched = 0
   8.366 +	   then
   8.367 +	     (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid));
   8.368 +	      killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
   8.369 +	    else ())
   8.370 +     fun proofHandler _ =
   8.371 +       let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid)
   8.372 +           val outcome  = valOf (TextIO.inputLine childin)
   8.373 +                          handle Option => error "watcher: \"outcome\" line is missing"
   8.374 +	   val probfile = valOf (TextIO.inputLine childin)
   8.375 +                          handle Option => error "watcher: \"probfile\" line is missing"
   8.376 +	   val sgno = number_from_filename probfile
   8.377 +	   val text = string_of_subgoal th sgno
   8.378 +	   fun report s = priority ("Subgoal " ^ Int.toString sgno ^ ": " ^ s);
   8.379 +       in
   8.380 +	 Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
   8.381 +		       "\"\nprobfile = " ^ probfile ^
   8.382 +		       "\nGoals being watched: "^  Int.toString (!goals_being_watched)));
   8.383 +	 if String.isPrefix "Invalid" outcome
   8.384 +	 then (report ("Subgoal is not provable:\n" ^ text);
   8.385 +	       decr_watched())
   8.386 +	 else if String.isPrefix "Failure" outcome
   8.387 +	 then (report ("Proof attempt failed:\n" ^ text);
   8.388 +	       decr_watched())
   8.389 +	(* print out a list of rules used from clasimpset*)
   8.390 +	 else if String.isPrefix "Success" outcome
   8.391 +	 then (report (read_proof probfile ^ "\n" ^ text);
   8.392 +	       decr_watched())
   8.393 +	  (* if proof translation failed *)
   8.394 +	 else if String.isPrefix "Translation failed" outcome
   8.395 +	 then (report (outcome ^ text);
   8.396 +	       decr_watched())
   8.397 +	 else (report "System error in proof handler";
   8.398 +	       decr_watched())
   8.399 +       end
   8.400 + in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));
   8.401 +    IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
   8.402 +    (childin, childout, childpid)
   8.403 +  end
   8.404 +
   8.405 +end (* structure Watcher *)