|
1 (* Title: SpassCommunication.ml |
|
2 Author: Claire Quigley |
|
3 Copyright 2004 University of Cambridge |
|
4 *) |
|
5 |
|
6 (***************************************************************************) |
|
7 (* Code to deal with the transfer of proofs from a Spass process *) |
|
8 (***************************************************************************) |
|
9 |
|
10 (***********************************) |
|
11 (* Write Spass output to a file *) |
|
12 (***********************************) |
|
13 |
|
14 fun logSpassInput (instr, fd) = let val thisLine = TextIO.inputLine instr |
|
15 in if thisLine = "--------------------------SPASS-STOP------------------------------\n" |
|
16 then TextIO.output (fd, thisLine) |
|
17 else ( |
|
18 TextIO.output (fd, thisLine); logSpassInput (instr,fd)) |
|
19 end; |
|
20 |
|
21 |
|
22 (**********************************************************************) |
|
23 (* Reconstruct the Spass proof w.r.t. thmstring (string version of *) |
|
24 (* Isabelle goal to be proved), then transfer the reconstruction *) |
|
25 (* steps as a string to the input pipe of the main Isabelle process *) |
|
26 (**********************************************************************) |
|
27 |
|
28 |
|
29 |
|
30 fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString) = let |
|
31 val thisLine = TextIO.inputLine fromChild |
|
32 in |
|
33 if (thisLine = "--------------------------SPASS-STOP------------------------------\n" ) |
|
34 then ( |
|
35 let val proofextract = extract_proof (currentString^thisLine) |
|
36 val reconstr = spassString_to_reconString (currentString^thisLine) thmstring |
|
37 val foo = TextIO.openOut "foobar2"; |
|
38 in |
|
39 TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo; |
|
40 |
|
41 TextIO.output (toParent, reconstr^"\n"); |
|
42 TextIO.flushOut toParent; |
|
43 TextIO.output (toParent, thmstring^"\n"); |
|
44 TextIO.flushOut toParent; |
|
45 TextIO.output (toParent, goalstring^"\n"); |
|
46 TextIO.flushOut toParent; |
|
47 |
|
48 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
|
49 (* Attempt to prevent several signals from turning up simultaneously *) |
|
50 OS.Process.sleep(Time.fromSeconds 1) |
|
51 |
|
52 end |
|
53 |
|
54 ) |
|
55 else ( |
|
56 |
|
57 transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine)) |
|
58 ) |
|
59 end; |
|
60 |
|
61 |
|
62 |
|
63 (*********************************************************************************) |
|
64 (* Inspect the output of a Spass process to see if it has found a proof, *) |
|
65 (* and if so, transfer output to the input pipe of the main Isabelle process *) |
|
66 (*********************************************************************************) |
|
67 |
|
68 |
|
69 fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd) = |
|
70 (*let val _ = Posix.Process.wait () |
|
71 in*) |
|
72 if (isSome (TextIO.canInput(fromChild, 5))) |
|
73 then |
|
74 ( |
|
75 let val thisLine = TextIO.inputLine fromChild |
|
76 in |
|
77 if (String.isPrefix "Here is a proof" thisLine ) |
|
78 then |
|
79 ( |
|
80 |
|
81 |
|
82 transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine); |
|
83 true) |
|
84 |
|
85 else |
|
86 ( |
|
87 startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd) |
|
88 ) |
|
89 end |
|
90 ) |
|
91 else (false) |
|
92 (* end*) |
|
93 |
|
94 fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd) = |
|
95 let val spass_proof_file = TextIO.openAppend("spass_proof") |
|
96 val outfile = TextIO.openOut("foo_checkspass"); |
|
97 val _ = TextIO.output (outfile, "checking proof found") |
|
98 |
|
99 val _ = TextIO.closeOut outfile |
|
100 in |
|
101 if (isSome (TextIO.canInput(fromChild, 5))) |
|
102 then |
|
103 ( |
|
104 let val thisLine = TextIO.inputLine fromChild |
|
105 in if ( thisLine = "SPASS beiseite: Proof found.\n" ) |
|
106 then |
|
107 ( |
|
108 let val outfile = TextIO.openOut("foo_proof"); (*val _ = OS.Process.sleep(Time.fromSeconds 3 );*) |
|
109 val _ = TextIO.output (outfile, (thisLine)) |
|
110 |
|
111 val _ = TextIO.closeOut outfile |
|
112 in |
|
113 startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd) |
|
114 end |
|
115 ) |
|
116 else if (thisLine= "SPASS beiseite: Completion found.\n" ) |
|
117 then |
|
118 |
|
119 ( |
|
120 let val outfile = TextIO.openOut("foo_proof"); (* val _ = OS.Process.sleep(Time.fromSeconds 3 );*) |
|
121 val _ = TextIO.output (outfile, (thisLine)) |
|
122 |
|
123 val _ = TextIO.closeOut outfile |
|
124 in |
|
125 |
|
126 (*TextIO.output (toParent,childCmd^"\n" ); |
|
127 TextIO.flushOut toParent;*) |
|
128 TextIO.output (spass_proof_file, (thisLine)); |
|
129 TextIO.flushOut spass_proof_file; |
|
130 TextIO.closeOut spass_proof_file; |
|
131 (*TextIO.output (toParent, thisLine); |
|
132 TextIO.flushOut toParent; |
|
133 TextIO.output (toParent, "bar\n"); |
|
134 TextIO.flushOut toParent;*) |
|
135 |
|
136 TextIO.output (toParent, thisLine^"\n"); |
|
137 TextIO.flushOut toParent; |
|
138 TextIO.output (toParent, thmstring^"\n"); |
|
139 TextIO.flushOut toParent; |
|
140 TextIO.output (toParent, goalstring^"\n"); |
|
141 TextIO.flushOut toParent; |
|
142 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
|
143 (* Attempt to prevent several signals from turning up simultaneously *) |
|
144 OS.Process.sleep(Time.fromSeconds 1); |
|
145 true |
|
146 end) |
|
147 else if ( thisLine = "SPASS beiseite: Ran out of time.\n" ) |
|
148 then |
|
149 ( |
|
150 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
|
151 TextIO.output (toParent,childCmd^"\n" ); |
|
152 TextIO.flushOut toParent; |
|
153 TextIO.output (toParent, thisLine); |
|
154 TextIO.flushOut toParent; |
|
155 |
|
156 true) |
|
157 else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" ) then |
|
158 ( |
|
159 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
|
160 TextIO.output (toParent,childCmd^"\n" ); |
|
161 TextIO.flushOut toParent; |
|
162 TextIO.output (toParent, thisLine); |
|
163 TextIO.flushOut toParent; |
|
164 |
|
165 true) |
|
166 else |
|
167 (TextIO.output (spass_proof_file, (thisLine)); |
|
168 TextIO.flushOut spass_proof_file; |
|
169 checkSpassProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd)) |
|
170 |
|
171 end |
|
172 ) |
|
173 else |
|
174 (TextIO.output (spass_proof_file, ("No proof output seen \n"));TextIO.closeOut spass_proof_file;false) |
|
175 end |
|
176 |
|
177 |
|
178 (***********************************************************************) |
|
179 (* Function used by the Isabelle process to read in a spass proof *) |
|
180 (***********************************************************************) |
|
181 |
|
182 |
|
183 (***********************************************************************) |
|
184 (* Function used by the Isabelle process to read in a vampire proof *) |
|
185 (***********************************************************************) |
|
186 |
|
187 (*fun getVampInput instr = let val thisLine = TextIO.inputLine instr |
|
188 in |
|
189 if (thisLine = "%============== End of proof. ==================\n" ) |
|
190 then |
|
191 ( |
|
192 (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));() |
|
193 ) |
|
194 else if (thisLine = "% Unprovable.\n" ) |
|
195 then |
|
196 ( |
|
197 (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));() |
|
198 ) |
|
199 else if (thisLine = "% Proof not found.\n") |
|
200 then |
|
201 ( |
|
202 Pretty.writeln(Pretty.str (concat["vampire", thisLine]));() |
|
203 ) |
|
204 |
|
205 |
|
206 else |
|
207 ( |
|
208 Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr |
|
209 ) |
|
210 end; |
|
211 |
|
212 *) |
|
213 |
|
214 fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2))) |
|
215 then |
|
216 let val thisLine = TextIO.inputLine instr |
|
217 val outfile = TextIO.openOut("foo_thisLine"); val _ = TextIO.output (outfile, (thisLine)) |
|
218 |
|
219 val _ = TextIO.closeOut outfile |
|
220 in |
|
221 if ( (substring (thisLine, 0,1))= "[") |
|
222 then |
|
223 (*Pretty.writeln(Pretty.str (thisLine))*) |
|
224 let val reconstr = thisLine |
|
225 val thmstring = TextIO.inputLine instr |
|
226 val goalstring = TextIO.inputLine instr |
|
227 in |
|
228 (reconstr, thmstring, goalstring) |
|
229 end |
|
230 else if (thisLine = "SPASS beiseite: Completion found.\n" ) |
|
231 then |
|
232 ( |
|
233 let val reconstr = thisLine |
|
234 val thmstring = TextIO.inputLine instr |
|
235 val goalstring = TextIO.inputLine instr |
|
236 in |
|
237 (reconstr, thmstring, goalstring) |
|
238 end |
|
239 ) |
|
240 else if (thisLine = "Proof found but translation failed!") |
|
241 then |
|
242 ( |
|
243 let val reconstr = thisLine |
|
244 val thmstring = TextIO.inputLine instr |
|
245 val goalstring = TextIO.inputLine instr |
|
246 val outfile = TextIO.openOut("foo_getSpass"); |
|
247 val _ = TextIO.output (outfile, (thisLine)) |
|
248 val _ = TextIO.closeOut outfile |
|
249 in |
|
250 (reconstr, thmstring, goalstring) |
|
251 end |
|
252 ) |
|
253 else |
|
254 getSpassInput instr |
|
255 |
|
256 end |
|
257 else |
|
258 ("No output from Spass.\n","","") |
|
259 |
|
260 |