author | paulson |
Wed, 05 Oct 2005 11:18:06 +0200 | |
changeset 17764 | fde495b9e24b |
parent 17746 | af59c748371d |
child 17772 | 818cec5f82a4 |
permissions | -rw-r--r-- |
15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset
|
1 |
(* Title: Watcher.ML |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset
|
2 |
ID: $Id$ |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset
|
3 |
Author: Claire Quigley |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset
|
4 |
Copyright 2004 University of Cambridge |
15642 | 5 |
*) |
6 |
||
17764 | 7 |
(* The watcher process starts a resolution process when it receives a *) |
15642 | 8 |
(* message from Isabelle *) |
9 |
(* Signals Isabelle, puts output of child into pipe to Isabelle, *) |
|
10 |
(* and removes dead processes. Also possible to kill all the resolution *) |
|
11 |
(* processes currently running. *) |
|
12 |
||
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
13 |
signature WATCHER = |
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
14 |
sig |
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
15 |
|
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
16 |
(* Send request to Watcher for multiple spasses to be called for filenames in arg *) |
17568 | 17 |
(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *) |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
18 |
|
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
19 |
val callResProvers : |
17422 | 20 |
TextIO.outstream * (string*string*string*string*string) list |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
21 |
-> unit |
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
22 |
|
17764 | 23 |
(* Send message to watcher to kill resolution provers *) |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
24 |
val callSlayer : TextIO.outstream -> unit |
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
25 |
|
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
26 |
(* Start a watcher and set up signal handlers *) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
27 |
val createWatcher : |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
28 |
thm * (ResClause.clause * thm) Array.array -> |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
29 |
TextIO.instream * TextIO.outstream * Posix.Process.pid |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
30 |
val killWatcher : Posix.Process.pid -> unit |
17764 | 31 |
val setting_sep : char |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
32 |
end |
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
33 |
|
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
34 |
|
15642 | 35 |
|
36 |
structure Watcher: WATCHER = |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
37 |
struct |
15642 | 38 |
|
17764 | 39 |
(*Field separators, used to pack items onto a text line*) |
40 |
val command_sep = #"\t" |
|
41 |
and setting_sep = #"%"; |
|
42 |
||
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
43 |
open Recon_Transfer |
16805 | 44 |
|
15642 | 45 |
val goals_being_watched = ref 0; |
46 |
||
17583
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17568
diff
changeset
|
47 |
val trace_path = Path.basic "watcher_trace"; |
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17568
diff
changeset
|
48 |
|
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
49 |
fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
50 |
else (); |
17583
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17568
diff
changeset
|
51 |
|
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
52 |
(* The result of calling createWatcher *) |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
53 |
datatype proc = PROC of { |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
54 |
pid : Posix.Process.pid, |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
55 |
instr : TextIO.instream, |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
56 |
outstr : TextIO.outstream |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
57 |
}; |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
58 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
59 |
(* The result of calling executeToList *) |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
60 |
datatype cmdproc = CMDPROC of { |
17568 | 61 |
prover: string, (* Name of the resolution prover used, e.g. Vampire*) |
62 |
cmd: string, (* The file containing the goal for res prover to prove *) |
|
63 |
goalstring: string, (* string representation of subgoal*) |
|
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
64 |
proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc, |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
65 |
instr : TextIO.instream, (* Input stream to child process *) |
17568 | 66 |
outstr : TextIO.outstream}; (* Output stream from child process *) |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
67 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
68 |
type signal = Posix.Signal.signal |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
69 |
datatype exit_status = datatype Posix.Process.exit_status |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
70 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
71 |
val fromStatus = Posix.Process.fromStatus |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
72 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
73 |
fun reap(pid, instr, outstr) = |
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
74 |
let val u = TextIO.closeIn instr; |
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
75 |
val u = TextIO.closeOut outstr; |
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
76 |
val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) |
17568 | 77 |
in status end |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
78 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
79 |
fun fdReader (name : string, fd : Posix.IO.file_desc) = |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
80 |
Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd }; |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
81 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
82 |
fun fdWriter (name, fd) = |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
83 |
Posix.IO.mkTextWriter { |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
84 |
appendMode = false, |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
85 |
initBlkMode = true, |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
86 |
name = name, |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
87 |
chunkSize=4096, |
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
88 |
fd = fd}; |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
89 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
90 |
fun openOutFD (name, fd) = |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
91 |
TextIO.mkOutstream ( |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
92 |
TextIO.StreamIO.mkOutstream ( |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
93 |
fdWriter (name, fd), IO.BLOCK_BUF)); |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
94 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
95 |
fun openInFD (name, fd) = |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
96 |
TextIO.mkInstream ( |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
97 |
TextIO.StreamIO.mkInstream ( |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
98 |
fdReader (name, fd), "")); |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
99 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
100 |
fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr)); |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
101 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
102 |
fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr); |
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
103 |
|
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
104 |
fun cmdInStream (CMDPROC{instr,outstr,...}) = instr; |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
105 |
|
17422 | 106 |
fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) = |
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
107 |
(prover,(cmd, (instr,outstr))); |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
108 |
|
17422 | 109 |
fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr}) = |
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
110 |
proc_handle; |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
111 |
|
17422 | 112 |
fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr}) = |
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
113 |
prover; |
15642 | 114 |
|
17422 | 115 |
fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr}) = |
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
116 |
goalstring; |
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
117 |
|
15642 | 118 |
|
119 |
(* gets individual args from instream and concatenates them into a list *) |
|
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
120 |
fun getArgs (fromParentStr, toParentStr, ys) = |
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
121 |
let val thisLine = TextIO.input fromParentStr |
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
122 |
in ys@[thisLine] end |
15642 | 123 |
|
124 |
||
125 |
(* Send request to Watcher for a vampire to be called for filename in arg *) |
|
17568 | 126 |
|
17231 | 127 |
fun callResProver (toWatcherStr, arg) = |
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
128 |
(TextIO.output (toWatcherStr, arg^"\n"); |
17231 | 129 |
TextIO.flushOut toWatcherStr) |
15642 | 130 |
|
131 |
(*****************************************************************************************) |
|
16357 | 132 |
(* Send request to Watcher for multiple provers to be called for filenames in arg *) |
133 |
(* need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*) |
|
15642 | 134 |
(*****************************************************************************************) |
135 |
||
16475 | 136 |
fun callResProvers (toWatcherStr, []) = |
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
137 |
(TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr) |
16475 | 138 |
| callResProvers (toWatcherStr, |
17422 | 139 |
(prover,goalstring, proverCmd,settings, |
140 |
probfile) :: args) = |
|
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
141 |
let val _ = trace (space_implode "\n" |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
142 |
(["\ncallResProvers:",prover,goalstring,proverCmd,settings, |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
143 |
probfile])) |
17764 | 144 |
in TextIO.output (toWatcherStr, |
145 |
(*Uses a special character to separate items sent to watcher*) |
|
146 |
space_implode (str command_sep) |
|
147 |
[prover, proverCmd, settings, probfile, |
|
148 |
String.toString goalstring ^ "\n"]); |
|
17746 | 149 |
(*goalstring is a single string literal, with all specials escaped.*) |
16475 | 150 |
goals_being_watched := (!goals_being_watched) + 1; |
151 |
TextIO.flushOut toWatcherStr; |
|
152 |
callResProvers (toWatcherStr,args) |
|
153 |
end |
|
16357 | 154 |
|
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset
|
155 |
|
15642 | 156 |
|
157 |
||
17764 | 158 |
(*Send message to watcher to kill currently running vampires. NOT USED and possibly |
159 |
buggy. Note that killWatcher kills the entire process group anyway.*) |
|
160 |
fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n"); |
|
15642 | 161 |
TextIO.flushOut toWatcherStr) |
162 |
||
17746 | 163 |
|
15642 | 164 |
(**************************************************************) |
165 |
(* Get commands from Isabelle *) |
|
166 |
(**************************************************************) |
|
17764 | 167 |
fun getCmds (toParentStr, fromParentStr, cmdList) = |
16475 | 168 |
let val thisLine = TextIO.inputLine fromParentStr |
169 |
in |
|
17764 | 170 |
trace("\nGot command from parent: " ^ thisLine); |
17568 | 171 |
if thisLine = "End of calls\n" orelse thisLine = "" then cmdList |
17422 | 172 |
else if thisLine = "Kill children\n" |
17764 | 173 |
then (TextIO.output (toParentStr,thisLine); |
17568 | 174 |
TextIO.flushOut toParentStr; |
17764 | 175 |
[("","","Kill children",[],"")]) |
17746 | 176 |
else |
17764 | 177 |
let val [prover,proverCmd,settingstr,probfile,goalstring] = |
178 |
String.tokens (fn c => c = command_sep) thisLine |
|
179 |
val settings = String.tokens (fn c => c = setting_sep) settingstr |
|
17746 | 180 |
in |
181 |
trace ("\nprover: " ^ prover ^ " prover path: " ^ proverCmd^ |
|
182 |
" problem file: " ^ probfile ^ |
|
183 |
"\ngoalstring: "^goalstring); |
|
184 |
getCmds (toParentStr, fromParentStr, |
|
185 |
(prover, goalstring, proverCmd, settings, probfile)::cmdList) |
|
186 |
end |
|
17764 | 187 |
handle Bind => |
188 |
(trace "getCmds: command parsing failed!"; |
|
189 |
getCmds (toParentStr, fromParentStr, cmdList)) |
|
16475 | 190 |
end |
191 |
||
16357 | 192 |
|
15642 | 193 |
(**************************************************************) |
194 |
(* Get Io-descriptor for polling of an input stream *) |
|
195 |
(**************************************************************) |
|
196 |
||
197 |
fun getInIoDesc someInstr = |
|
198 |
let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr) |
|
15702
2677db44c795
new signalling primmitives for sml/nj compatibility
paulson
parents:
15684
diff
changeset
|
199 |
val _ = TextIO.output (TextIO.stdOut, buf) |
15642 | 200 |
val ioDesc = |
201 |
case rd |
|
202 |
of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod |
|
203 |
| _ => NONE |
|
204 |
in (* since getting the reader will have terminated the stream, we need |
|
205 |
* to build a new stream. *) |
|
206 |
TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf)); |
|
207 |
ioDesc |
|
208 |
end |
|
209 |
||
210 |
||
211 |
(*************************************) |
|
212 |
(* Set up a Watcher Process *) |
|
213 |
(*************************************) |
|
214 |
||
17716 | 215 |
(* for tracing: encloses each string element in brackets. *) |
216 |
val concat_with_and = space_implode " & " o map (enclose "(" ")"); |
|
217 |
||
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
218 |
fun prems_string_of th = |
17716 | 219 |
concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th)) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
220 |
|
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17502
diff
changeset
|
221 |
fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc); |
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17502
diff
changeset
|
222 |
|
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17502
diff
changeset
|
223 |
fun killChildren procs = List.app (ignore o killChild) procs; |
17502 | 224 |
|
17568 | 225 |
(*************************************************************) |
226 |
(* take an instream and poll its underlying reader for input *) |
|
227 |
(*************************************************************) |
|
228 |
||
229 |
fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = |
|
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
230 |
case OS.IO.pollDesc fromParentIOD of |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
231 |
SOME pd => |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
232 |
(case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
233 |
[] => NONE |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
234 |
| pd''::_ => if OS.IO.isIn pd'' |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
235 |
then SOME (getCmds (toParentStr, fromParentStr, [])) |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
236 |
else NONE) |
17568 | 237 |
| NONE => NONE; |
238 |
||
17583
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17568
diff
changeset
|
239 |
(*get the number of the subgoal from the filename: the last digit string*) |
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17568
diff
changeset
|
240 |
fun number_from_filename s = |
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17568
diff
changeset
|
241 |
case String.tokens (not o Char.isDigit) s of |
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
242 |
[] => (trace "\nWatcher could not read subgoal nunber!!"; raise ERROR) |
17583
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17568
diff
changeset
|
243 |
| numbers => valOf (Int.fromString (List.last numbers)); |
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17568
diff
changeset
|
244 |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
245 |
fun setupWatcher (thm,clause_arr) = |
16061 | 246 |
let |
17764 | 247 |
val p1 = Posix.IO.pipe () (** pipes for communication between parent and watcher **) |
16061 | 248 |
val p2 = Posix.IO.pipe () |
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
249 |
fun closep () = |
17764 | 250 |
(Posix.IO.close (#outfd p1); Posix.IO.close (#infd p1); |
251 |
Posix.IO.close (#outfd p2); Posix.IO.close (#infd p2)) |
|
252 |
(****** fork a watcher process and get it set up and going ******) |
|
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
253 |
fun startWatcher procList = |
17764 | 254 |
(case Posix.Process.fork() |
255 |
of SOME pid => pid (* parent - i.e. main Isabelle process *) |
|
256 |
| NONE => let (* child - i.e. watcher *) |
|
257 |
val oldchildin = #infd p1 |
|
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
258 |
val fromParent = Posix.FileSys.wordToFD 0w0 |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
259 |
val oldchildout = #outfd p2 |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
260 |
val toParent = Posix.FileSys.wordToFD 0w1 |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
261 |
val fromParentIOD = Posix.FileSys.fdToIOD fromParent |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
262 |
val fromParentStr = openInFD ("_exec_in_parent", fromParent) |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
263 |
val toParentStr = openOutFD ("_exec_out_parent", toParent) |
17764 | 264 |
val pid = Posix.ProcEnv.getpid() |
265 |
val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid} |
|
266 |
(*set process group id: allows killing all children*) |
|
267 |
val () = debug ("subgoals forked to startWatcher: "^ prems_string_of thm); |
|
17568 | 268 |
|
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
269 |
fun pollChildInput fromStr = |
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
270 |
case getInIoDesc fromStr of |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
271 |
SOME iod => |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
272 |
(case OS.IO.pollDesc iod of |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
273 |
SOME pd => |
17764 | 274 |
let val pd' = OS.IO.pollIn pd in |
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
275 |
case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
276 |
[] => false |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
277 |
| pd''::_ => OS.IO.isIn pd'' |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
278 |
end |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
279 |
| NONE => false) |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
280 |
| NONE => false |
15642 | 281 |
|
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
282 |
(* Check all ATP processes currently running for output *) |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
283 |
fun checkChildren ([], toParentStr) = [] (* no children to check *) |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
284 |
| checkChildren (childProc::otherChildren, toParentStr) = |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
285 |
let val _ = trace ("\nIn check child, length of queue:"^ |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
286 |
Int.toString (length (childProc::otherChildren))) |
17568 | 287 |
val (childInput,childOutput) = cmdstreamsOf childProc |
288 |
val child_handle = cmdchildHandle childProc |
|
17764 | 289 |
val childCmd = #1(#2(cmdchildInfo childProc)) (*name of problem file*) |
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
290 |
val _ = trace ("\nchildCmd = " ^ childCmd) |
17583
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17568
diff
changeset
|
291 |
val sg_num = number_from_filename childCmd |
17234 | 292 |
val childIncoming = pollChildInput childInput |
293 |
val parentID = Posix.ProcEnv.getppid() |
|
294 |
val prover = cmdProver childProc |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
295 |
val prems_string = prems_string_of thm |
17234 | 296 |
val goalstring = cmdGoal childProc |
297 |
in |
|
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
298 |
trace("\nsubgoals forked to checkChildren: " ^ goalstring); |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
299 |
if childIncoming |
17764 | 300 |
then (* check here for prover label on child*) |
301 |
let val _ = trace ("\nInput available from child: " ^ childCmd ^ |
|
17746 | 302 |
"\ngoalstring is " ^ goalstring) |
17306 | 303 |
val childDone = (case prover of |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
304 |
"vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr) |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
305 |
| "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
306 |
|"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr) ) |
17306 | 307 |
in |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
308 |
if childDone |
17306 | 309 |
then (* child has found a proof and transferred it *) |
310 |
(* Remove this child and go on to check others*) |
|
311 |
(Unix.reap child_handle; |
|
17716 | 312 |
OS.FileSys.remove childCmd; |
17306 | 313 |
checkChildren(otherChildren, toParentStr)) |
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
314 |
else (* Keep this child and go on to check others *) |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
315 |
childProc :: checkChildren (otherChildren, toParentStr) |
17306 | 316 |
end |
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
317 |
else (trace "\nNo child output"; |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
318 |
childProc::(checkChildren (otherChildren, toParentStr))) |
17234 | 319 |
end |
15642 | 320 |
|
17234 | 321 |
|
17764 | 322 |
(* call resolution processes *) |
323 |
(* settings should be a list of strings ["-t 300", "-m 100000"] *) |
|
324 |
(* takes list of (string, string, string list, string)list proclist *) |
|
325 |
fun execCmds [] procList = procList |
|
326 |
| execCmds ((prover, goalstring,proverCmd,settings,file)::cmds) procList = |
|
327 |
let val _ = trace (space_implode "\n" |
|
328 |
(["\nAbout to execute command for goal:", |
|
329 |
goalstring, proverCmd] @ settings @ |
|
330 |
[file, Date.toString(Date.fromTimeLocal(Time.now()))])) |
|
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
331 |
val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = |
17764 | 332 |
Unix.execute(proverCmd, settings@[file]) |
17234 | 333 |
val (instr, outstr) = Unix.streamsOf childhandle |
17764 | 334 |
val newProcList = CMDPROC{prover = prover, |
335 |
cmd = file, |
|
336 |
goalstring = goalstring, |
|
337 |
proc_handle = childhandle, |
|
338 |
instr = instr, |
|
339 |
outstr = outstr} :: procList |
|
17234 | 340 |
|
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
341 |
val _ = trace ("\nFinished at " ^ |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
342 |
Date.toString(Date.fromTimeLocal(Time.now()))) |
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
343 |
in execCmds cmds newProcList end |
15642 | 344 |
|
17764 | 345 |
(******** Watcher Loop ********) |
346 |
val limit = ref 500; (*don't let it run forever*) |
|
16061 | 347 |
|
17568 | 348 |
fun keepWatching (procList) = |
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
349 |
let fun loop procList = |
17764 | 350 |
let val _ = trace ("\nCalling pollParentInput: " ^ Int.toString (!limit)); |
351 |
val cmdsFromIsa = pollParentInput |
|
352 |
(fromParentIOD, fromParentStr, toParentStr) |
|
353 |
in |
|
354 |
OS.Process.sleep (Time.fromMilliseconds 100); |
|
355 |
limit := !limit - 1; |
|
356 |
if !limit = 0 |
|
357 |
then |
|
358 |
(trace "\nTimeout: Killing proof processes"; |
|
359 |
TextIO.output(toParentStr, "Timeout: Killing proof processes!\n"); |
|
360 |
TextIO.flushOut toParentStr; |
|
361 |
killChildren (map cmdchildHandle procList); |
|
362 |
exit 0) |
|
363 |
else case cmdsFromIsa of |
|
364 |
SOME [(_,_,"Kill children",_,_)] => |
|
17234 | 365 |
let val child_handles = map cmdchildHandle procList |
17764 | 366 |
in killChildren child_handles; loop [] end |
367 |
| SOME cmds => (* deal with commands from Isabelle process *) |
|
368 |
if length procList < 40 |
|
17234 | 369 |
then (* Execute locally *) |
370 |
let |
|
17764 | 371 |
val newProcList = execCmds cmds procList |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
372 |
val newProcList' = checkChildren (newProcList, toParentStr) |
17234 | 373 |
in |
17764 | 374 |
trace "\nJust execed a child"; loop newProcList' |
17234 | 375 |
end |
17764 | 376 |
else (* Execute remotely [FIXME: NOT REALLY] *) |
17234 | 377 |
let |
17764 | 378 |
val newProcList = execCmds cmds procList |
379 |
val newProcList' = checkChildren (newProcList, toParentStr) |
|
380 |
in loop newProcList' end |
|
381 |
| NONE => (* No new input from Isabelle *) |
|
382 |
let val newProcList = checkChildren (procList, toParentStr) |
|
383 |
in |
|
384 |
trace "\nNo new input, still watching"; loop newProcList |
|
385 |
end |
|
386 |
end |
|
17234 | 387 |
in |
17306 | 388 |
loop procList |
17234 | 389 |
end |
390 |
||
15642 | 391 |
|
17764 | 392 |
in |
393 |
(*** Sort out pipes ********) |
|
394 |
Posix.IO.close (#outfd p1); |
|
395 |
Posix.IO.close (#infd p2); |
|
396 |
Posix.IO.dup2{old = oldchildin, new = fromParent}; |
|
397 |
Posix.IO.close oldchildin; |
|
398 |
Posix.IO.dup2{old = oldchildout, new = toParent}; |
|
399 |
Posix.IO.close oldchildout; |
|
15642 | 400 |
|
17764 | 401 |
(* start the watcher loop *) |
402 |
keepWatching (procList); |
|
403 |
(* fake return value - actually want the watcher to loop until killed *) |
|
404 |
Posix.Process.wordToPid 0w0 |
|
405 |
end); |
|
17234 | 406 |
(* end case *) |
15642 | 407 |
|
408 |
||
16061 | 409 |
val _ = TextIO.flushOut TextIO.stdOut |
15642 | 410 |
|
16061 | 411 |
(*******************************) |
412 |
(*** set watcher going ********) |
|
413 |
(*******************************) |
|
15642 | 414 |
|
16061 | 415 |
val procList = [] |
17317
3f12de2e2e6e
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset
|
416 |
val pid = startWatcher procList |
16061 | 417 |
(**************************************************) |
418 |
(* communication streams to watcher *) |
|
419 |
(**************************************************) |
|
15642 | 420 |
|
16061 | 421 |
val instr = openInFD ("_exec_in", #infd p2) |
422 |
val outstr = openOutFD ("_exec_out", #outfd p1) |
|
423 |
||
17568 | 424 |
in |
425 |
(*******************************) |
|
426 |
(* close the child-side fds *) |
|
427 |
(*******************************) |
|
428 |
Posix.IO.close (#outfd p2); |
|
429 |
Posix.IO.close (#infd p1); |
|
430 |
(* set the fds close on exec *) |
|
431 |
Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
|
432 |
Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
|
433 |
||
434 |
(*******************************) |
|
435 |
(* return value *) |
|
436 |
(*******************************) |
|
437 |
PROC{pid = pid, instr = instr, outstr = outstr} |
|
438 |
end; |
|
15642 | 439 |
|
440 |
||
441 |
||
442 |
(**********************************************************) |
|
443 |
(* Start a watcher and set up signal handlers *) |
|
444 |
(**********************************************************) |
|
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
445 |
|
17764 | 446 |
fun killWatcher pid = Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill); |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
447 |
|
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset
|
448 |
fun reapWatcher(pid, instr, outstr) = |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
449 |
(TextIO.closeIn instr; TextIO.closeOut outstr; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
450 |
Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ()) |
15642 | 451 |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
452 |
fun createWatcher (thm, clause_arr) = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
453 |
let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr)) |
17435 | 454 |
fun decr_watched() = |
17502 | 455 |
(goals_being_watched := !goals_being_watched - 1; |
17435 | 456 |
if !goals_being_watched = 0 |
457 |
then |
|
17716 | 458 |
(debug ("\nReaping a watcher, childpid = "^ |
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
459 |
LargeWord.toString (Posix.Process.pidToWord childpid)); |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
460 |
killWatcher childpid; reapWatcher (childpid,childin, childout)) |
17435 | 461 |
else ()) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
462 |
val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
463 |
fun proofHandler n = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
464 |
let val outcome = TextIO.inputLine childin |
17746 | 465 |
val goalstring = valOf (String.fromString (TextIO.inputLine childin)) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
466 |
val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
467 |
"\"\ngoalstring = " ^ goalstring ^ |
17568 | 468 |
"\ngoals_being_watched: "^ Int.toString (!goals_being_watched)) |
17502 | 469 |
in |
470 |
if String.isPrefix "[" outcome (*indicates a proof reconstruction*) |
|
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
471 |
then (priority (Recon_Transfer.apply_res_thm outcome goalstring); |
17435 | 472 |
decr_watched()) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
473 |
else if String.isPrefix "Invalid" outcome |
17746 | 474 |
then (priority ("Subgoal is not provable:\n" ^ goalstring); |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
475 |
decr_watched()) |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
476 |
else if String.isPrefix "Failure" outcome |
17746 | 477 |
then (priority ("Proof attempt failed:\n" ^ goalstring); |
17435 | 478 |
decr_watched()) |
17216 | 479 |
(* print out a list of rules used from clasimpset*) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
480 |
else if String.isPrefix "Success" outcome |
17746 | 481 |
then (priority (outcome ^ goalstring); |
17435 | 482 |
decr_watched()) |
17216 | 483 |
(* if proof translation failed *) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
484 |
else if String.isPrefix "Translation failed" outcome |
17746 | 485 |
then (priority (outcome ^ goalstring); |
17435 | 486 |
decr_watched()) |
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17583
diff
changeset
|
487 |
else (priority "System error in proof handler"; |
17435 | 488 |
decr_watched()) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
489 |
end |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset
|
490 |
in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler); |
17216 | 491 |
(childin, childout, childpid) |
492 |
end |
|
15642 | 493 |
|
494 |
end (* structure Watcher *) |