214 in (thisLine, thmstring, goalstring) end |
214 in (thisLine, thmstring, goalstring) end |
215 else getVampInput instr |
215 else getVampInput instr |
216 end |
216 end |
217 |
217 |
218 |
218 |
219 (*FIXME!!: The following code is a mess. It mostly refers to SPASS-specific things*) |
|
220 |
|
221 (***********************************************************************) |
219 (***********************************************************************) |
222 (* Function used by the Isabelle process to read in an E proof *) |
220 (* Function used by the Isabelle process to read in an E proof *) |
223 (***********************************************************************) |
221 (***********************************************************************) |
224 |
222 |
225 fun getEInput instr = |
223 fun getEInput instr = |
226 let val thisLine = TextIO.inputLine instr |
224 let val thisLine = TextIO.inputLine instr |
227 val _ = File.write (File.tmp_path (Path.basic "eprover_line")) thisLine |
225 val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine |
228 in |
226 in (* reconstructed proof string *) |
229 if thisLine = "" then ("No output from reconstruction process.\n","","") |
227 if thisLine = "" then ("No output from reconstruction process.\n","","") |
230 else if String.sub (thisLine, 0) = #"[" |
228 else if String.isPrefix "# Problem is satisfiable" thisLine orelse |
231 then |
229 String.isPrefix "# Cannot determine problem status" thisLine orelse |
232 let val reconstr = thisLine |
230 String.isPrefix "# Failure:" thisLine |
233 val thmstring = TextIO.inputLine instr |
231 then |
234 val goalstring = TextIO.inputLine instr |
232 let val thmstring = TextIO.inputLine instr |
235 in |
233 val goalstring = TextIO.inputLine instr |
236 (reconstr, thmstring, goalstring) |
234 in (thisLine, thmstring, goalstring) end |
237 end |
235 else if thisLine = "Proof found but translation failed!" |
238 else if String.isPrefix "SPASS beiseite:" thisLine (*FIXME: wrong!!*) |
236 then |
239 then |
237 let val thmstring = TextIO.inputLine instr |
240 let val reconstr = thisLine |
|
241 val thmstring = TextIO.inputLine instr |
|
242 val goalstring = TextIO.inputLine instr |
238 val goalstring = TextIO.inputLine instr |
243 in |
239 val _ = debug "getEInput: translation of proof failed" |
244 (reconstr, thmstring, goalstring) |
240 in (thisLine, thmstring, goalstring) end |
245 end |
|
246 |
|
247 else if String.isPrefix "# No proof" thisLine |
|
248 then |
|
249 let val reconstr = thisLine |
|
250 val thmstring = TextIO.inputLine instr |
|
251 val goalstring = TextIO.inputLine instr |
|
252 in |
|
253 (reconstr, thmstring, goalstring) |
|
254 end |
|
255 |
|
256 else if String.isPrefix "# Failure" thisLine |
|
257 then |
|
258 let val reconstr = thisLine |
|
259 val thmstring = TextIO.inputLine instr |
|
260 val goalstring = TextIO.inputLine instr |
|
261 in |
|
262 (reconstr, thmstring, goalstring) |
|
263 end |
|
264 else if String.isPrefix "Rules from" thisLine |
|
265 then |
|
266 let val reconstr = thisLine |
|
267 val thmstring = TextIO.inputLine instr |
|
268 val goalstring = TextIO.inputLine instr |
|
269 in |
|
270 (reconstr, thmstring, goalstring) |
|
271 end |
|
272 else if substring (thisLine, 0,5) = "Proof" |
|
273 then |
|
274 let val reconstr = thisLine |
|
275 val thmstring = TextIO.inputLine instr |
|
276 val goalstring = TextIO.inputLine instr |
|
277 in |
|
278 File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine; |
|
279 (reconstr, thmstring, goalstring) |
|
280 end |
|
281 else if substring (thisLine, 0,1) = "%" |
|
282 then |
|
283 let val reconstr = thisLine |
|
284 val thmstring = TextIO.inputLine instr |
|
285 val goalstring = TextIO.inputLine instr |
|
286 in |
|
287 File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine; |
|
288 (reconstr, thmstring, goalstring) |
|
289 end |
|
290 else getEInput instr |
241 else getEInput instr |
291 end |
242 end |
292 |
243 |
293 end; |
244 end; |