Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
authorquigley
Wed Jun 22 20:26:31 2005 +0200 (2005-06-22)
changeset 16548aa36ae6b955e
parent 16547 09f7a953d2d6
child 16549 32523b65a388
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.
src/HOL/Tools/ATP/SpassCommunication.ML
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/ATP/watcher.ML
     1.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Wed Jun 22 19:48:20 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Wed Jun 22 20:26:31 2005 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4                                             in if ( thisLine = "SPASS beiseite: Proof found.\n" )
     1.5                                                then      
     1.6                                                (  
     1.7 -                                                 let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
     1.8 +                                                 let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
     1.9                                                       val _ = TextIO.output (outfile, (thisLine))
    1.10                                               
    1.11                                                       val _ =  TextIO.closeOut outfile
    1.12 @@ -155,7 +155,7 @@
    1.13                                                     then  
    1.14  
    1.15                                                   (
    1.16 -                                                      let    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
    1.17 +                                                      let    val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
    1.18                                                               val _ = TextIO.output (outfile, (thisLine))
    1.19                                               
    1.20                                                               val _ =  TextIO.closeOut outfile
    1.21 @@ -184,15 +184,27 @@
    1.22                                                        end) 
    1.23                                                       else if ( thisLine = "SPASS beiseite: Ran out of time.\n" ) 
    1.24                                                            then  
    1.25 -                                                (
    1.26 -                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.27 -                                                        TextIO.output (toParent,childCmd^"\n" );
    1.28 -                                                        TextIO.flushOut toParent;
    1.29 -                                                        TextIO.output (toParent, thisLine);
    1.30 -                                                        TextIO.flushOut toParent;
    1.31 +                                                		( let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                          	(*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
    1.32 +                                                     		val _ = TextIO.output (outfile, (thisLine))
    1.33 +                                             	
    1.34 +                                                    
    1.35 +                                                     		in TextIO.output (toParent, thisLine^"\n");
    1.36 +                                                     		  TextIO.flushOut toParent;
    1.37 +                                                     		  TextIO.output (toParent, thmstring^"\n");
    1.38 +                                                     		  TextIO.flushOut toParent;
    1.39 +                                                     		  TextIO.output (toParent, goalstring^"\n");
    1.40 +                                                     		  TextIO.flushOut toParent;
    1.41 +                                                     		  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.42 +                                                    		  TextIO.output (outfile, ("signalled parent\n"));TextIO.closeOut outfile;
    1.43  
    1.44 -                                                        true) 
    1.45 -                                                          else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" )                                                             then
    1.46 +                                                	       (* Attempt to prevent several signals from turning up simultaneously *)
    1.47 +                                                       		Posix.Process.sleep(Time.fromSeconds 1);
    1.48 +                                                       		 true 
    1.49 +                                                       		end)
    1.50 +
    1.51 +
    1.52 + 
    1.53 +                                                    else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" )                                                           		    then
    1.54                                                   (
    1.55                                                          Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.56                                                          TextIO.output (toParent,childCmd^"\n" );
    1.57 @@ -236,7 +248,7 @@
    1.58                                               in
    1.59                                                   (reconstr, thmstring, goalstring)
    1.60                                               end
    1.61 -                                     else if (thisLine = "SPASS beiseite: Completion found.\n" ) 
    1.62 +                                     else if (String.isPrefix "SPASS beiseite:" thisLine ) 
    1.63                                            then 
    1.64                                            (
    1.65                                               let val reconstr = thisLine
     2.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Wed Jun 22 19:48:20 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Wed Jun 22 20:26:31 2005 +0200
     2.3 @@ -259,6 +259,10 @@
     2.4        val term_num =
     2.5          (number ++ (a (Other ".")) ++ number) >> (fn (a, (_, c)) => (a, c))
     2.6  
     2.7 +
     2.8 +      val term_num_list = (term_num ++ many (a (Other ",") ++ term_num >> snd)
     2.9 +			   >> (fn (a, b) => (a::b)))
    2.10 +
    2.11        val axiom = (a (Word "Inp"))
    2.12              >> (fn (_) => Axiom)
    2.13        
    2.14 @@ -296,9 +300,8 @@
    2.15                   >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
    2.16  
    2.17        val rewrite = (a (Word "Rew")) ++ (a (Other ":")) 
    2.18 -                    ++ term_num ++ (a (Other ",")) 
    2.19 -                    ++ term_num
    2.20 -            >> (fn (_, (_, (c, (_, e)))) =>  Rewrite (c, e))
    2.21 +                    ++ term_num_list
    2.22 +            >> (fn (_, (_, (c))) =>  Rewrite (c))
    2.23  
    2.24  
    2.25        val mrr = (a (Word "MRR")) ++ (a (Other ":"))
     3.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Jun 22 19:48:20 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Jun 22 20:26:31 2005 +0200
     3.3 @@ -79,8 +79,8 @@
     3.4        "Para(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
     3.5  |   proofstep_to_string  (MRR ((a,b), (c,d))) =
     3.6        "MRR(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
     3.7 -|   proofstep_to_string (Rewrite((a,b),(c,d))) =
     3.8 -      "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
     3.9 +(*|   proofstep_to_string (Rewrite((a,b),(c,d))) =
    3.10 +      "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"*)
    3.11  
    3.12  fun list_to_string [] liststr = liststr
    3.13  |   list_to_string (x::[]) liststr = liststr^(string_of_int x)
    3.14 @@ -667,16 +667,16 @@
    3.15              >> (fn (_, (_, (c, (_, (e,(_,(f,_))))))) =>  Factor (c,e,f))
    3.16  
    3.17  
    3.18 -val rewritestep = (a (Word "Rewrite"))  ++ (a (Other "(")) ++ (a (Other "(")) 
    3.19 +(*val rewritestep = (a (Word "Rewrite"))  ++ (a (Other "(")) ++ (a (Other "(")) 
    3.20                     ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
    3.21                     ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
    3.22 -            >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e))
    3.23 +            >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e))*)
    3.24  
    3.25  val obviousstep = (a (Word "Obvious")) ++ (a (Other "(")) 
    3.26                     ++ term_numstep  ++ (a (Other ")")) 
    3.27              >> (fn (_, (_, (c,_))) => Obvious (c))
    3.28  
    3.29 - val methodstep = extraaxiomstep || origaxiomstep || axiomstep ||binarystep || factorstep|| parastep || mrrstep || rewritestep || obviousstep
    3.30 + val methodstep = extraaxiomstep || origaxiomstep || axiomstep ||binarystep || factorstep|| parastep || mrrstep || (*rewritestep ||*) obviousstep
    3.31  
    3.32  
    3.33   val number_list_step =
    3.34 @@ -869,9 +869,9 @@
    3.35  |   by_isar_line ((Factor ((a,b,c)))) = 
    3.36      "by (rule cl"^(string_of_int a)^" [factor "^(string_of_int b)^" "^
    3.37  		(string_of_int c)^" ])\n"
    3.38 -|   by_isar_line ( (Rewrite ((a,b),(c,d)))) =
    3.39 +(*|   by_isar_line ( (Rewrite ((a,b),(c,d)))) =
    3.40      "by (rule cl"^(string_of_int a)^" [demod "^(string_of_int b)^" "^
    3.41 -		(string_of_int c)^" "^(string_of_int d)^" ])\n"
    3.42 +		(string_of_int c)^" "^(string_of_int d)^" ])\n"*)
    3.43  |   by_isar_line ( (Obvious ((a,b)))) =
    3.44      "by (rule cl"^(string_of_int a)^" [obvious "^(string_of_int b)^" ])\n"
    3.45  
     4.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Wed Jun 22 19:48:20 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Wed Jun 22 20:26:31 2005 +0200
     4.3 @@ -38,7 +38,8 @@
     4.4                       | Para of (int * int) * (int * int) 
     4.5  		     | Super_l of (int * int) * (int * int)
     4.6  		     | Super_r of (int * int) * (int * int)
     4.7 -                     | Rewrite of (int * int) * (int * int)  
     4.8 +                     (*| Rewrite of (int * int) * (int * int)  *)
     4.9 +                     | Rewrite of (int * int) list
    4.10  		     | SortSimp of (int * int) * (int * int)  
    4.11  		     | UnitConf of (int * int) * (int * int)  
    4.12                       | Obvious of (int * int)
    4.13 @@ -304,7 +305,7 @@
    4.14  (* extra conditions from the equality turn up as 2nd to last literals of result.  Need to delete them *)
    4.15  (* changed negate_nead to negate_head here too*)
    4.16                      (* clause1, lit1 is thing to rewrite with *)
    4.17 -fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs = 
    4.18 +(*fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs = 
    4.19        let val th1 =  valOf (assoc (thml,clause1))
    4.20  	  val th2 = valOf (assoc (thml,clause2))
    4.21  	  val eq_lit_th = select_literal (lit1+1) th1
    4.22 @@ -323,7 +324,7 @@
    4.23         end
    4.24         handle Option => reconstruction_failed "follow_rewrite"
    4.25  
    4.26 -
    4.27 +*)
    4.28  
    4.29  (*****************************************)
    4.30  (* Reconstruct an obvious reduction step *)
    4.31 @@ -362,8 +363,8 @@
    4.32        | follow_proof clauses  allvars clausenum  thml (Para (a, b)) clause_strs
    4.33          = follow_standard_para (a, b) allvars  thml clause_strs
    4.34  
    4.35 -      | follow_proof clauses  allvars clausenum thml (Rewrite (a,b)) clause_strs
    4.36 -        = follow_rewrite (a,b)  allvars thml clause_strs
    4.37 +    (*  | follow_proof clauses  allvars clausenum thml (Rewrite (a,b)) clause_strs
    4.38 +        = follow_rewrite (a,b)  allvars thml clause_strs*)
    4.39  
    4.40        | follow_proof clauses  allvars clausenum thml (Obvious (a,b)) clause_strs
    4.41          = follow_obvious (a,b)  allvars thml clause_strs
     5.1 --- a/src/HOL/Tools/ATP/watcher.ML	Wed Jun 22 19:48:20 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Jun 22 20:26:31 2005 +0200
     5.3 @@ -810,7 +810,7 @@
     5.4                            
     5.5  
     5.6  fun spass_proofHandler (n) = (
     5.7 -                                 let  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
     5.8 +                                 let  val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
     5.9                                        val _ = TextIO.output (outfile, ("In signal handler now\n"))
    5.10                                        val _ =  TextIO.closeOut outfile
    5.11                                        val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
    5.12 @@ -883,25 +883,40 @@
    5.13                                                            else if ((substring (reconstr, 0,5)) = "Proof")
    5.14                                                                 then 
    5.15                                                                     (
    5.16 -                                                                     goals_being_watched := (!goals_being_watched) -1;
    5.17 -                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    5.18 -                                                                      Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
    5.19 -                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
    5.20 -                                                                      if (!goals_being_watched = 0)
    5.21 -                                                                      then 
    5.22 +                                                                      goals_being_watched := (!goals_being_watched) -1;
    5.23 +                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    5.24 +                                                                       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
    5.25 +                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
    5.26 +                                                                       if (!goals_being_watched = 0)
    5.27 +                                                                       then 
    5.28                                                                            (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
    5.29                                                                                 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
    5.30                                                                                 val _ =  TextIO.closeOut outfile
    5.31 -                                                                           in
    5.32 +                                                                            in
    5.33                                                                                killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
    5.34 -                                                                           end )
    5.35 -                                                                      else
    5.36 -                                                                         ( )
    5.37 +                                                                            end )
    5.38 +                                                                       else
    5.39 +                                                                          ( )
    5.40                                                                        )
    5.41  
    5.42  
    5.43                                                                  else  (* add something here ?*)
    5.44 -                                                                   ()
    5.45 +                                                                   (
    5.46 +                                                                      goals_being_watched := (!goals_being_watched) -1;
    5.47 +                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    5.48 +                                                                       Pretty.writeln(Pretty.str ("Ran out of options in handler"));
    5.49 +                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
    5.50 +                                                                       if (!goals_being_watched = 0)
    5.51 +                                                                       then 
    5.52 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
    5.53 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
    5.54 +                                                                               val _ =  TextIO.closeOut outfile
    5.55 +                                                                            in
    5.56 +                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
    5.57 +                                                                            end )
    5.58 +                                                                       else
    5.59 +                                                                          ( )
    5.60 +                                                                      )
    5.61                                                                       
    5.62                                                                             
    5.63