277 (*********************************************************************) |
277 (*********************************************************************) |
278 |
278 |
279 fun rules_to_string [] = "NONE" |
279 fun rules_to_string [] = "NONE" |
280 | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]" |
280 | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]" |
281 |
281 |
282 fun subst_for a b = String.translate (fn c => str (if c=a then b else c)); |
|
283 |
|
284 val remove_linebreaks = subst_for #"\n" #"\t"; |
|
285 val restore_linebreaks = subst_for #"\t" #"\n"; |
|
286 |
|
287 |
282 |
288 fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr = |
283 fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr = |
289 let val _ = trace |
284 let val _ = trace |
290 ("\nGetting lemma names. proofstr is " ^ proofstr ^ |
285 ("\nGetting lemma names. proofstr is " ^ proofstr ^ |
291 "\ngoalstr is " ^ goalstring ^ |
286 "\ngoalstring is " ^ goalstring ^ |
292 "\nnum of clauses is " ^ string_of_int (Array.length clause_arr)) |
287 "num of clauses is " ^ string_of_int (Array.length clause_arr)) |
293 val axiom_names = getax proofstr clause_arr |
288 val axiom_names = getax proofstr clause_arr |
294 val ax_str = rules_to_string axiom_names |
289 val ax_str = rules_to_string axiom_names |
295 in |
290 in |
296 trace ("\nDone. Lemma list is " ^ ax_str); |
291 trace ("\nDone. Lemma list is " ^ ax_str); |
297 TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^ |
292 TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^ |
298 ax_str ^ "\n"); |
293 ax_str ^ "\n"); |
299 TextIO.output (toParent, "goalstring: "^goalstring^"\n"); |
294 TextIO.output (toParent, goalstring); |
300 TextIO.flushOut toParent; |
295 TextIO.flushOut toParent; |
301 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2) |
296 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2) |
302 end |
297 end |
303 handle exn => (*FIXME: exn handler is too general!*) |
298 handle exn => (*FIXME: exn handler is too general!*) |
304 (trace ("\nprover_lemma_list_aux: In exception handler: " ^ |
299 (trace ("\nprover_lemma_list_aux: In exception handler: " ^ |
305 Toplevel.exn_message exn); |
300 Toplevel.exn_message exn); |
306 TextIO.output (toParent, "Translation failed for the proof: " ^ |
301 TextIO.output (toParent, "Translation failed for the proof: " ^ |
307 remove_linebreaks proofstr ^ "\n"); |
302 String.toString proofstr ^ "\n"); |
308 TextIO.output (toParent, remove_linebreaks goalstring ^ "\n"); |
303 TextIO.output (toParent, goalstring); |
309 TextIO.flushOut toParent; |
304 TextIO.flushOut toParent; |
310 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)); |
305 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)); |
311 |
306 |
312 val e_lemma_list = prover_lemma_list_aux get_axiom_names_e; |
307 val e_lemma_list = prover_lemma_list_aux get_axiom_names_e; |
313 |
308 |
365 val frees_str = "["^(thmvars_to_string frees "")^"]" |
360 val frees_str = "["^(thmvars_to_string frees "")^"]" |
366 val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr) |
361 val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr) |
367 val _ = trace ("\nReconstruction:\n" ^ reconstr) |
362 val _ = trace ("\nReconstruction:\n" ^ reconstr) |
368 in |
363 in |
369 TextIO.output (toParent, reconstr^"\n"); |
364 TextIO.output (toParent, reconstr^"\n"); |
370 TextIO.output (toParent, goalstring^"\n"); |
365 TextIO.output (toParent, goalstring); |
371 TextIO.flushOut toParent; |
366 TextIO.flushOut toParent; |
372 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
367 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); |
373 all_tac |
368 all_tac |
374 end |
369 end |
375 handle exn => (*FIXME: exn handler is too general!*) |
370 handle exn => (*FIXME: exn handler is too general!*) |
376 (trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn); |
371 (trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn); |
377 TextIO.output (toParent,"Translation failed for the proof:"^ |
372 TextIO.output (toParent,"Translation failed for the proof:"^ |
378 (remove_linebreaks proofstr) ^"\n"); |
373 String.toString proofstr ^"\n"); |
379 TextIO.output (toParent, goalstring^"\n"); |
374 TextIO.output (toParent, goalstring); |
380 TextIO.flushOut toParent; |
375 TextIO.flushOut toParent; |
381 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac) |
376 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac) |
382 |
377 |
383 (**********************************************************************************) |
378 (**********************************************************************************) |
384 (* At other end, want to turn back into datatype so can apply reconstruct_proof. *) |
379 (* At other end, want to turn back into datatype so can apply reconstruct_proof. *) |
675 (* be passed over to the watcher, e.g. numcls25 *) |
670 (* be passed over to the watcher, e.g. numcls25 *) |
676 (*******************************************************) |
671 (*******************************************************) |
677 |
672 |
678 fun apply_res_thm str goalstring = |
673 fun apply_res_thm str goalstring = |
679 let val tokens = #1 (lex str); |
674 let val tokens = #1 (lex str); |
680 val _ = trace ("\napply_res_thm. str is: "^str^" goalstr is: "^goalstring^"\n") |
675 val _ = trace ("\napply_res_thm. str is: "^str^ |
|
676 "\ngoalstring is: \n"^goalstring^"\n") |
681 val (frees,recon_steps) = parse_step tokens |
677 val (frees,recon_steps) = parse_step tokens |
682 in |
678 in |
683 to_isar_proof (frees, recon_steps, goalstring) |
679 to_isar_proof (frees, recon_steps, goalstring) |
684 end |
680 end |
685 |
681 |