--- a/src/HOL/Tools/ATP/AtpCommunication.ML Tue Oct 04 09:58:38 2005 +0200
+++ b/src/HOL/Tools/ATP/AtpCommunication.ML Tue Oct 04 09:59:01 2005 +0200
@@ -89,7 +89,7 @@
fun signal_parent (toParent, ppid, msg, goalstring) =
(TextIO.output (toParent, msg);
- TextIO.output (toParent, goalstring^"\n");
+ TextIO.output (toParent, goalstring);
TextIO.flushOut toParent;
trace ("\nSignalled parent: " ^ msg);
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Oct 04 09:58:38 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Oct 04 09:59:01 2005 +0200
@@ -279,24 +279,19 @@
fun rules_to_string [] = "NONE"
| rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
-fun subst_for a b = String.translate (fn c => str (if c=a then b else c));
-
-val remove_linebreaks = subst_for #"\n" #"\t";
-val restore_linebreaks = subst_for #"\t" #"\n";
-
fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr =
let val _ = trace
("\nGetting lemma names. proofstr is " ^ proofstr ^
- "\ngoalstr is " ^ goalstring ^
- "\nnum of clauses is " ^ string_of_int (Array.length clause_arr))
+ "\ngoalstring is " ^ goalstring ^
+ "num 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
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.output (toParent, goalstring);
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
end
@@ -304,8 +299,8 @@
(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");
+ String.toString proofstr ^ "\n");
+ TextIO.output (toParent, goalstring);
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
@@ -367,7 +362,7 @@
val _ = trace ("\nReconstruction:\n" ^ reconstr)
in
TextIO.output (toParent, reconstr^"\n");
- TextIO.output (toParent, goalstring^"\n");
+ TextIO.output (toParent, goalstring);
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
all_tac
@@ -375,8 +370,8 @@
handle exn => (*FIXME: exn handler is too general!*)
(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");
+ String.toString proofstr ^"\n");
+ TextIO.output (toParent, goalstring);
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac)
@@ -677,7 +672,8 @@
fun apply_res_thm str goalstring =
let val tokens = #1 (lex str);
- val _ = trace ("\napply_res_thm. str is: "^str^" goalstr is: "^goalstring^"\n")
+ val _ = trace ("\napply_res_thm. str is: "^str^
+ "\ngoalstring is: \n"^goalstring^"\n")
val (frees,recon_steps) = parse_step tokens
in
to_isar_proof (frees, recon_steps, goalstring)
--- a/src/HOL/Tools/ATP/watcher.ML Tue Oct 04 09:58:38 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Tue Oct 04 09:59:01 2005 +0200
@@ -145,8 +145,9 @@
(["\ncallResProvers:",prover,goalstring,proverCmd,settings,
probfile]))
in TextIO.output (toWatcherStr,
- (prover^"$"^goalstring^"$"^proverCmd^"$"^
- settings^"$"^probfile^"\n"));
+ prover^"$"^proverCmd^"$"^ settings^"$"^probfile^"$\n");
+ TextIO.output (toWatcherStr, String.toString goalstring^"\n");
+ (*goalstring is a single string literal, with all specials escaped.*)
goals_being_watched := (!goals_being_watched) + 1;
TextIO.flushOut toWatcherStr;
callResProvers (toWatcherStr,args)
@@ -161,24 +162,7 @@
fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n");
TextIO.flushOut toWatcherStr)
-
-(**************************************************************)
-(* Remove \n token from a vampire goal filename and extract *)
-(* prover, proverCmd, settings and file from input string *)
-(**************************************************************)
-
-val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
-
-fun getCmd cmdStr =
- let val [prover,goalstring,proverCmd,settingstr,probfile] =
- String.tokens (fn c => c = #"$") (remove_newlines cmdStr)
- val settings = String.tokens (fn c => c = #"%") settingstr
- val _ = trace ("getCmd: " ^ cmdStr ^
- "\nprover" ^ prover ^ " goalstr: "^goalstring^
- "\nprovercmd: " ^ proverCmd^
- "\nprob " ^ probfile ^ "\n\n")
- in (prover,goalstring, proverCmd, settings, probfile) end
-
+
(**************************************************************)
(* Get commands from Isabelle *)
(**************************************************************)
@@ -191,8 +175,18 @@
then (TextIO.output (toParentStr,thisLine );
TextIO.flushOut toParentStr;
(("","","Kill children",[],"")::cmdList) )
- else let val thisCmd = getCmd thisLine
- in getCmds (toParentStr, fromParentStr, thisCmd::cmdList) end
+ else
+ let val [prover,proverCmd,settingstr,probfile,_] =
+ String.tokens (fn c => c = #"$") thisLine
+ val settings = String.tokens (fn c => c = #"%") settingstr
+ val goalstring = TextIO.inputLine fromParentStr
+ in
+ trace ("\nprover: " ^ prover ^ " prover path: " ^ proverCmd^
+ " problem file: " ^ probfile ^
+ "\ngoalstring: "^goalstring);
+ getCmds (toParentStr, fromParentStr,
+ (prover, goalstring, proverCmd, settings, probfile)::cmdList)
+ end
end
@@ -317,7 +311,7 @@
(* check here for prover label on child*)
let val _ = trace ("\nInput available from child: " ^
childCmd ^
- "\ngoalstring is " ^ goalstring ^ "\n\n")
+ "\ngoalstring is " ^ goalstring)
val childDone = (case prover of
"vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)
| "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)
@@ -530,7 +524,7 @@
val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
fun proofHandler n =
let val outcome = TextIO.inputLine childin
- val goalstring = TextIO.inputLine childin
+ val goalstring = valOf (String.fromString (TextIO.inputLine childin))
val _ = debug ("In signal handler. outcome = \"" ^ outcome ^
"\"\ngoalstring = " ^ goalstring ^
"\ngoals_being_watched: "^ Int.toString (!goals_being_watched))
@@ -539,18 +533,18 @@
then (priority (Recon_Transfer.apply_res_thm outcome goalstring);
decr_watched())
else if String.isPrefix "Invalid" outcome
- then (priority (goalstring ^ "is not provable");
+ then (priority ("Subgoal is not provable:\n" ^ goalstring);
decr_watched())
else if String.isPrefix "Failure" outcome
- then (priority (goalstring ^ "proof attempt failed");
+ then (priority ("Proof attempt failed:\n" ^ goalstring);
decr_watched())
(* print out a list of rules used from clasimpset*)
else if String.isPrefix "Success" outcome
- then (priority (goalstring^outcome);
+ then (priority (outcome ^ goalstring);
decr_watched())
(* if proof translation failed *)
else if String.isPrefix "Translation failed" outcome
- then (priority (goalstring ^ outcome);
+ then (priority (outcome ^ goalstring);
decr_watched())
else (priority "System error in proof handler";
decr_watched())
--- a/src/HOL/Tools/res_atp.ML Tue Oct 04 09:58:38 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue Oct 04 09:59:01 2005 +0200
@@ -38,18 +38,6 @@
fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
-(**** for Isabelle/ML interface ****)
-
-(*Remove unwanted characters such as ? and newline from the textural
- representation of a theorem (surely they don't need to be produced in
- the first place?) *)
-
-fun is_proof_char ch = (#" " <= ch andalso ch <= #"~" andalso ch <> #"?");
-
-val proofstring =
- String.translate (fn c => if is_proof_char c then str c else "");
-
-
(**** For running in Isar ****)
(* same function as that in res_axioms.ML *)
@@ -99,7 +87,7 @@
fun make_atp_list [] n = []
| make_atp_list (sg_term::xs) n =
let
- val goalstring = proofstring (Sign.string_of_term sign sg_term)
+ val goalstring = Sign.string_of_term sign sg_term
val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
val probfile = prob_pathname n
val time = Int.toString (!time_limit)
@@ -235,7 +223,7 @@
end);
val call_atpP =
- OuterSyntax.improper_command
+ OuterSyntax.command
"ProofGeneral.call_atp"
"call automatic theorem provers"
OuterKeyword.diag