Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
Will now signal if ATP has run out of time and then kill the watcher.
--- a/src/HOL/Tools/ATP/SpassCommunication.ML Wed Jun 22 19:48:20 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Wed Jun 22 20:26:31 2005 +0200
@@ -143,7 +143,7 @@
in if ( thisLine = "SPASS beiseite: Proof found.\n" )
then
(
- let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
+ let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
@@ -155,7 +155,7 @@
then
(
- let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
+ let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
@@ -184,15 +184,27 @@
end)
else if ( thisLine = "SPASS beiseite: Ran out of time.\n" )
then
- (
- Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
- TextIO.output (toParent,childCmd^"\n" );
- TextIO.flushOut toParent;
- TextIO.output (toParent, thisLine);
- TextIO.flushOut toParent;
+ ( let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
+ val _ = TextIO.output (outfile, (thisLine))
+
+
+ in TextIO.output (toParent, thisLine^"\n");
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, thmstring^"\n");
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, goalstring^"\n");
+ TextIO.flushOut toParent;
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+ TextIO.output (outfile, ("signalled parent\n"));TextIO.closeOut outfile;
- true)
- else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" ) then
+ (* Attempt to prevent several signals from turning up simultaneously *)
+ Posix.Process.sleep(Time.fromSeconds 1);
+ true
+ end)
+
+
+
+ else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" ) then
(
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
TextIO.output (toParent,childCmd^"\n" );
@@ -236,7 +248,7 @@
in
(reconstr, thmstring, goalstring)
end
- else if (thisLine = "SPASS beiseite: Completion found.\n" )
+ else if (String.isPrefix "SPASS beiseite:" thisLine )
then
(
let val reconstr = thisLine
--- a/src/HOL/Tools/ATP/recon_parse.ML Wed Jun 22 19:48:20 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML Wed Jun 22 20:26:31 2005 +0200
@@ -259,6 +259,10 @@
val term_num =
(number ++ (a (Other ".")) ++ number) >> (fn (a, (_, c)) => (a, c))
+
+ val term_num_list = (term_num ++ many (a (Other ",") ++ term_num >> snd)
+ >> (fn (a, b) => (a::b)))
+
val axiom = (a (Word "Inp"))
>> (fn (_) => Axiom)
@@ -296,9 +300,8 @@
>> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
val rewrite = (a (Word "Rew")) ++ (a (Other ":"))
- ++ term_num ++ (a (Other ","))
- ++ term_num
- >> (fn (_, (_, (c, (_, e)))) => Rewrite (c, e))
+ ++ term_num_list
+ >> (fn (_, (_, (c))) => Rewrite (c))
val mrr = (a (Word "MRR")) ++ (a (Other ":"))
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Jun 22 19:48:20 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Jun 22 20:26:31 2005 +0200
@@ -79,8 +79,8 @@
"Para(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
| proofstep_to_string (MRR ((a,b), (c,d))) =
"MRR(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
-| proofstep_to_string (Rewrite((a,b),(c,d))) =
- "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
+(*| proofstep_to_string (Rewrite((a,b),(c,d))) =
+ "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"*)
fun list_to_string [] liststr = liststr
| list_to_string (x::[]) liststr = liststr^(string_of_int x)
@@ -667,16 +667,16 @@
>> (fn (_, (_, (c, (_, (e,(_,(f,_))))))) => Factor (c,e,f))
-val rewritestep = (a (Word "Rewrite")) ++ (a (Other "(")) ++ (a (Other "("))
+(*val rewritestep = (a (Word "Rewrite")) ++ (a (Other "(")) ++ (a (Other "("))
++ term_numstep ++ (a (Other ")")) ++ (a (Other ","))
++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
- >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e))
+ >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e))*)
val obviousstep = (a (Word "Obvious")) ++ (a (Other "("))
++ term_numstep ++ (a (Other ")"))
>> (fn (_, (_, (c,_))) => Obvious (c))
- val methodstep = extraaxiomstep || origaxiomstep || axiomstep ||binarystep || factorstep|| parastep || mrrstep || rewritestep || obviousstep
+ val methodstep = extraaxiomstep || origaxiomstep || axiomstep ||binarystep || factorstep|| parastep || mrrstep || (*rewritestep ||*) obviousstep
val number_list_step =
@@ -869,9 +869,9 @@
| by_isar_line ((Factor ((a,b,c)))) =
"by (rule cl"^(string_of_int a)^" [factor "^(string_of_int b)^" "^
(string_of_int c)^" ])\n"
-| by_isar_line ( (Rewrite ((a,b),(c,d)))) =
+(*| by_isar_line ( (Rewrite ((a,b),(c,d)))) =
"by (rule cl"^(string_of_int a)^" [demod "^(string_of_int b)^" "^
- (string_of_int c)^" "^(string_of_int d)^" ])\n"
+ (string_of_int c)^" "^(string_of_int d)^" ])\n"*)
| by_isar_line ( (Obvious ((a,b)))) =
"by (rule cl"^(string_of_int a)^" [obvious "^(string_of_int b)^" ])\n"
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Wed Jun 22 19:48:20 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Wed Jun 22 20:26:31 2005 +0200
@@ -38,7 +38,8 @@
| Para of (int * int) * (int * int)
| Super_l of (int * int) * (int * int)
| Super_r of (int * int) * (int * int)
- | Rewrite of (int * int) * (int * int)
+ (*| Rewrite of (int * int) * (int * int) *)
+ | Rewrite of (int * int) list
| SortSimp of (int * int) * (int * int)
| UnitConf of (int * int) * (int * int)
| Obvious of (int * int)
@@ -304,7 +305,7 @@
(* extra conditions from the equality turn up as 2nd to last literals of result. Need to delete them *)
(* changed negate_nead to negate_head here too*)
(* clause1, lit1 is thing to rewrite with *)
-fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs =
+(*fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs =
let val th1 = valOf (assoc (thml,clause1))
val th2 = valOf (assoc (thml,clause2))
val eq_lit_th = select_literal (lit1+1) th1
@@ -323,7 +324,7 @@
end
handle Option => reconstruction_failed "follow_rewrite"
-
+*)
(*****************************************)
(* Reconstruct an obvious reduction step *)
@@ -362,8 +363,8 @@
| follow_proof clauses allvars clausenum thml (Para (a, b)) clause_strs
= follow_standard_para (a, b) allvars thml clause_strs
- | follow_proof clauses allvars clausenum thml (Rewrite (a,b)) clause_strs
- = follow_rewrite (a,b) allvars thml clause_strs
+ (* | follow_proof clauses allvars clausenum thml (Rewrite (a,b)) clause_strs
+ = follow_rewrite (a,b) allvars thml clause_strs*)
| follow_proof clauses allvars clausenum thml (Obvious (a,b)) clause_strs
= follow_obvious (a,b) allvars thml clause_strs
--- a/src/HOL/Tools/ATP/watcher.ML Wed Jun 22 19:48:20 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Wed Jun 22 20:26:31 2005 +0200
@@ -810,7 +810,7 @@
fun spass_proofHandler (n) = (
- let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
+ let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
val _ = TextIO.output (outfile, ("In signal handler now\n"))
val _ = TextIO.closeOut outfile
val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
@@ -883,25 +883,40 @@
else if ((substring (reconstr, 0,5)) = "Proof")
then
(
- goals_being_watched := (!goals_being_watched) -1;
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
- Pretty.writeln(Pretty.str (oct_char "361"));
- if (!goals_being_watched = 0)
- then
+ goals_being_watched := (!goals_being_watched) -1;
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
(let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
val _ = TextIO.closeOut outfile
- in
+ in
killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
- end )
- else
- ( )
+ end )
+ else
+ ( )
)
else (* add something here ?*)
- ()
+ (
+ goals_being_watched := (!goals_being_watched) -1;
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str ("Ran out of options in handler"));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
+ val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
+ val _ = TextIO.closeOut outfile
+ in
+ killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
+ end )
+ else
+ ( )
+ )