--- a/src/HOL/Tools/ATP/AtpCommunication.ML Thu Sep 29 12:45:04 2005 +0200
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML Thu Sep 29 12:45:16 2005 +0200
@@ -27,6 +27,11 @@
(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
val reconstruct = ref false;
+val trace_path = Path.basic "atp_trace";
+
+fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s
+ else ();
+
exception EOF;
val start_E = "# Proof object starts here."
@@ -64,18 +69,17 @@
let val thisLine = TextIO.inputLine fromChild
in
if thisLine = "" (*end of file?*)
- then (File.write (File.tmp_path (Path.basic"extraction_failed"))
- ("end bracket: " ^ endS ^
- "\naccumulated text: " ^ currentString);
+ then (trace ("\n extraction_failed. End bracket: " ^ endS ^
+ "\naccumulated text: " ^ currentString);
raise EOF)
else if String.isPrefix endS thisLine
then let val proofextract = extract_proof (currentString^thisLine)
+ val lemma_list = if endS = end_V8
+ then Recon_Transfer.vamp_lemma_list
+ else Recon_Transfer.e_lemma_list
in
- File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract;
- (if endS = end_V8 (*vampire?*)
- then Recon_Transfer.vamp_lemma_list
- else Recon_Transfer.e_lemma_list)
- proofextract goalstring toParent ppid clause_arr
+ trace ("\nExtracted_prf\n" ^ proofextract);
+ lemma_list proofextract goalstring toParent ppid clause_arr
end
else transferInput (currentString^thisLine)
end
@@ -87,17 +91,16 @@
(TextIO.output (toParent, msg);
TextIO.output (toParent, goalstring^"\n");
TextIO.flushOut toParent;
+ trace ("\nSignalled parent: " ^ msg);
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
let val thisLine = TextIO.inputLine fromChild
in
- File.append (File.tmp_path (Path.basic "proof")) thisLine;
+ trace thisLine;
if thisLine = ""
- then (File.append (File.tmp_path (Path.basic "proof"))
- "No proof output seen \n";
- false)
+ then (trace "No proof output seen\n"; false)
else if String.isPrefix start_V8 thisLine
then
startTransfer (end_V8, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
@@ -114,11 +117,9 @@
fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, clause_arr) =
let val thisLine = TextIO.inputLine fromChild
in
- File.append (File.tmp_path (Path.basic "proof")) thisLine;
+ trace thisLine;
if thisLine = ""
- then (File.append (File.tmp_path (Path.basic "proof"))
- "No proof output seen \n";
- false)
+ then (trace "No proof output seen\n"; false)
else if String.isPrefix start_E thisLine
then
startTransfer (end_E, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
@@ -152,13 +153,13 @@
let val thisLine = TextIO.inputLine fromChild
in
if thisLine = "" (*end of file?*)
- then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString;
+ then (trace ("\nspass_extraction_failed: " ^ currentString);
raise EOF)
else if String.isPrefix "--------------------------SPASS-STOP" thisLine
then
let val proofextract = extract_proof (currentString^thisLine)
in
- File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract;
+ trace ("\nextracted spass proof: " ^ proofextract);
if !reconstruct
then (spass_reconstruct_tac proofextract goalstring toParent ppid sg_num
clause_arr thm; ())
@@ -182,8 +183,7 @@
in
if thisLine = "" then false
else if String.isPrefix "Here is a proof" thisLine then
- (File.append (File.tmp_path (Path.basic "spass_transfer"))
- ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n");
+ (trace ("\nabout to transfer proof, thm is " ^ string_of_thm thm);
transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine,
thm, sg_num,clause_arr);
true) handle EOF => false
@@ -192,40 +192,26 @@
end
-(*Called from watcher. Returns true if the E process has returned a verdict.*)
+(*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd,
thm, sg_num, clause_arr) =
- let val spass_proof_file = TextIO.openAppend
- (File.platform_path(File.tmp_path (Path.basic "spass_proof")))
- val thisLine = TextIO.inputLine fromChild
+ let val thisLine = TextIO.inputLine fromChild
in
- File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
- if thisLine = ""
- then (TextIO.output (spass_proof_file, ("No proof output seen \n"));
- TextIO.closeOut spass_proof_file;
- false)
+ trace thisLine;
+ if thisLine = "" then (trace "No proof output seen\n"; false)
else if thisLine = "SPASS beiseite: Proof found.\n"
then
startSpassTransfer (fromChild, toParent, ppid, goalstring,
childCmd, thm, sg_num, clause_arr)
else if thisLine = "SPASS beiseite: Completion found.\n"
- then
- (TextIO.output (spass_proof_file, thisLine);
- TextIO.closeOut spass_proof_file;
- signal_parent (toParent, ppid, "Invalid\n", goalstring);
- true)
+ then (signal_parent (toParent, ppid, "Invalid\n", goalstring);
+ true)
else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
- then
- (signal_parent (toParent, ppid, "Failure\n", goalstring);
- TextIO.output (spass_proof_file, "signalled parent\n");
- TextIO.closeOut spass_proof_file;
- true)
- else
- (TextIO.output (spass_proof_file, thisLine);
- TextIO.flushOut spass_proof_file;
- checkSpassProofFound (fromChild, toParent, ppid, goalstring,
- childCmd, thm, sg_num, clause_arr))
+ then (signal_parent (toParent, ppid, "Failure\n", goalstring);
+ true)
+ else checkSpassProofFound (fromChild, toParent, ppid, goalstring,
+ childCmd, thm, sg_num, clause_arr)
end
end;
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Sep 29 12:45:04 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Sep 29 12:45:16 2005 +0200
@@ -10,6 +10,11 @@
infixr 8 ++; infixr 7 >>; infixr 6 ||;
+val trace_path = Path.basic "transfer_trace";
+
+fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s
+ else ();
+
(* Versions that include type information *)
@@ -175,11 +180,9 @@
fun get_axiom_names_spass proofstr clause_arr =
let (* parse spass proof into datatype *)
- val _ = File.write (File.tmp_path (Path.basic "parsing_progress"))
- ("Started parsing:\n" ^ proofstr)
- val tokens = #1(lex proofstr)
- val proof_steps = parse tokens
- val _ = File.append (File.tmp_path (Path.basic "parsing_progress")) "\nFinished!"
+ val _ = trace ("\nStarted parsing:\n" ^ proofstr)
+ val proof_steps = parse (#1(lex proofstr))
+ val _ = trace "\nParsing finished!"
(* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
in
get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr
@@ -248,8 +251,8 @@
val meta_strs = map ReconOrderClauses.get_meta_lits metas
val metas_and_strs = ListPair.zip (metas,meta_strs)
- val _ = File.write(File.tmp_path (Path.basic "foo_clauses")) (onestr ax_strs)
- val _ = File.write(File.tmp_path (Path.basic "foo_metastrs")) (onestr meta_strs)
+ val _ = trace ("\nAxioms: " ^ onestr ax_strs)
+ val _ = trace ("\nMeta_strs: " ^ onestr meta_strs)
(* get list of axioms as thms with their variables *)
@@ -283,25 +286,23 @@
fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr =
- let val _ = File.append(File.tmp_path (Path.basic "prover_lemmastring"))
- ("proofstr is " ^ proofstr ^
+ let val _ = trace
+ ("\nGetting lemma names. proofstr is " ^ proofstr ^
"\ngoalstr is " ^ goalstring ^
"\nnum of clauses is " ^ string_of_int (Array.length clause_arr))
val axiom_names = getax proofstr clause_arr
val ax_str = rules_to_string axiom_names
in
- File.append(File.tmp_path (Path.basic "prover_lemmastring"))
- ("\nlemma list is: " ^ ax_str);
+ trace ("\nDone. Lemma list is " ^ ax_str);
TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
ax_str ^ "\n");
TextIO.output (toParent, "goalstring: "^goalstring^"\n");
TextIO.flushOut toParent;
-
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
end
handle exn => (*FIXME: exn handler is too general!*)
- (File.write(File.tmp_path (Path.basic "proverString_handler"))
- ("In exception handler: " ^ Toplevel.exn_message exn);
+ (trace ("\nprover_lemma_list_aux: In exception handler: " ^
+ Toplevel.exn_message exn);
TextIO.output (toParent, "Translation failed for the proof: " ^
remove_linebreaks proofstr ^ "\n");
TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
@@ -318,17 +319,13 @@
(**** Full proof reconstruction for SPASS (not really working) ****)
fun spass_reconstruct proofstr goalstring toParent ppid thms clause_arr =
- let val _ = File.write(File.tmp_path (Path.basic "prover_reconstruction"))
- ("proofstr is: "^proofstr)
+ let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr)
val tokens = #1(lex proofstr)
- (***********************************)
(* parse spass proof into datatype *)
(***********************************)
val proof_steps = parse tokens
-
- val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))
- ("Did parsing on "^proofstr)
+ val _ = trace "\nParsing finished"
(************************************)
(* recreate original subgoal as thm *)
@@ -341,17 +338,15 @@
val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr
(*val numcls_string = numclstr ( vars, numcls) ""*)
- val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) "got axioms"
+ val _ = trace "\ngot axioms"
(************************************)
(* translate proof *)
(************************************)
- val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))
- ("about to translate proof, steps: "
- ^(init_proofsteps_to_string proof_steps ""))
+ val _ = trace ("\nabout to translate proof, steps: "
+ ^ (init_proofsteps_to_string proof_steps ""))
val (newthm,proof) = translate_proof numcls proof_steps vars
- val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))
- ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
+ val _ = trace ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
(***************************************************)
(* transfer necessary steps as strings to Isabelle *)
(***************************************************)
@@ -368,9 +363,8 @@
else []
val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
val frees_str = "["^(thmvars_to_string frees "")^"]"
- val _ = File.write (File.tmp_path (Path.basic "reconstringfile"))
- (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
+ val _ = trace ("\nReconstruction:\n" ^ reconstr)
in
TextIO.output (toParent, reconstr^"\n");
TextIO.output (toParent, goalstring^"\n");
@@ -379,8 +373,7 @@
all_tac
end
handle exn => (*FIXME: exn handler is too general!*)
- (File.append(File.tmp_path (Path.basic "prover_reconstruction"))
- ("In exception handler: " ^ Toplevel.exn_message exn);
+ (trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn);
TextIO.output (toParent,"Translation failed for the proof:"^
(remove_linebreaks proofstr) ^"\n");
TextIO.output (toParent, goalstring^"\n");
@@ -667,7 +660,7 @@
(isar_lines firststeps "")^
(last_isar_line laststep)^
("qed")
- val _ = File.write (File.tmp_path (Path.basic "isar_proof_file")) isar_proof
+ val _ = trace ("\nto_isar_proof returns " ^ isar_proof)
in
isar_proof
end;
@@ -684,8 +677,7 @@
fun apply_res_thm str goalstring =
let val tokens = #1 (lex str);
- val _ = File.append (File.tmp_path (Path.basic "apply_res_1"))
- ("str is: "^str^" goalstr is: "^goalstring^"\n")
+ val _ = trace ("\napply_res_thm. str is: "^str^" goalstr is: "^goalstring^"\n")
val (frees,recon_steps) = parse_step tokens
in
to_isar_proof (frees, recon_steps, goalstring)