# HG changeset patch # User quigley # Date 1119464791 -7200 # Node ID aa36ae6b955eb055b6ea8a07e4aaefe36b5fce15 # Parent 09f7a953d2d67797fa7cff1398129403e30c547c 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. diff -r 09f7a953d2d6 -r aa36ae6b955e src/HOL/Tools/ATP/SpassCommunication.ML --- 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 diff -r 09f7a953d2d6 -r aa36ae6b955e src/HOL/Tools/ATP/recon_parse.ML --- 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 ":")) diff -r 09f7a953d2d6 -r aa36ae6b955e src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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" diff -r 09f7a953d2d6 -r aa36ae6b955e src/HOL/Tools/ATP/recon_translate_proof.ML --- 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 diff -r 09f7a953d2d6 -r aa36ae6b955e src/HOL/Tools/ATP/watcher.ML --- 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 + ( ) + )