src/HOL/Tools/ATP/watcher.ML
changeset 16767 2d4433759b8d
parent 16675 96bdc59afc05
child 16805 fadf80952202
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Mon Jul 11 14:52:55 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Mon Jul 11 16:42:42 2005 +0200
     1.3 @@ -266,6 +266,7 @@
     1.4      
     1.5      val tptp2X = ResLib.helper_path "TPTP2X_HOME" "tptp2X"  		
     1.6  
     1.7 +
     1.8      (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
     1.9      val probID = List.last(explode probfile)
    1.10      val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    1.11 @@ -814,8 +815,6 @@
    1.12                             VampComm.getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
    1.13                            
    1.14  
    1.15 -
    1.16 -
    1.17  fun spass_proofHandler (n) = (
    1.18                                   let  val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
    1.19                                        val _ = TextIO.output (outfile, ("In signal handler now\n"))
    1.20 @@ -847,8 +846,9 @@
    1.21                                                                   else
    1.22                                                                      ()
    1.23                                                              )
    1.24 -                                                    (* if there's no proof, but a some sort of  message from Spass *)
    1.25 -                                                    else 
    1.26 +                                                    (* if there's no proof, but a message from Spass *)
    1.27 +                                                    else if ((substring (reconstr, 0,5))= "SPASS")
    1.28 +                                                         then
    1.29                                                                   (
    1.30                                                                       goals_being_watched := (!goals_being_watched) -1;
    1.31                                                                       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.32 @@ -864,7 +864,86 @@
    1.33                                                                             end )
    1.34                                                                        else
    1.35                                                                           ()
    1.36 -                                                                )						               
    1.37 +                                                                ) 
    1.38 +						   (* print out a list of rules used from clasimpset*)
    1.39 +                                                    else if ((substring (reconstr, 0,5))= "Rules")
    1.40 +                                                         then
    1.41 +                                                                 (
    1.42 +                                                                     goals_being_watched := (!goals_being_watched) -1;
    1.43 +                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.44 +                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
    1.45 +                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
    1.46 +                                                                      if (!goals_being_watched = 0)
    1.47 +                                                                      then 
    1.48 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
    1.49 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
    1.50 +                                                                               val _ =  TextIO.closeOut outfile
    1.51 +                                                                           in
    1.52 +                                                                              killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
    1.53 +                                                                           end )
    1.54 +                                                                      else
    1.55 +                                                                         ()
    1.56 +                                                                )
    1.57 +							
    1.58 +                                                          (* if proof translation failed *)
    1.59 +                                                          else if ((substring (reconstr, 0,5)) = "Proof")
    1.60 +                                                               then 
    1.61 +                                                                   (
    1.62 +                                                                      goals_being_watched := (!goals_being_watched) -1;
    1.63 +                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.64 +                                                                       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
    1.65 +                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
    1.66 +                                                                       if (!goals_being_watched = 0)
    1.67 +                                                                       then 
    1.68 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
    1.69 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
    1.70 +                                                                               val _ =  TextIO.closeOut outfile
    1.71 +                                                                            in
    1.72 +                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
    1.73 +                                                                            end )
    1.74 +                                                                       else
    1.75 +                                                                          ( )
    1.76 +                                                                      )
    1.77 +
    1.78 +							        else if ((substring (reconstr, 0,1)) = "%")
    1.79 +                                                               then 
    1.80 +                                                                   (
    1.81 +                                                                      goals_being_watched := (!goals_being_watched) -1;
    1.82 +                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.83 +                                                                       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
    1.84 +                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
    1.85 +                                                                       if (!goals_being_watched = 0)
    1.86 +                                                                       then 
    1.87 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
    1.88 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
    1.89 +                                                                               val _ =  TextIO.closeOut outfile
    1.90 +                                                                            in
    1.91 +                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
    1.92 +                                                                            end )
    1.93 +                                                                       else
    1.94 +                                                                          ( )
    1.95 +                                                                      )
    1.96 +
    1.97 +
    1.98 +                                                                else  (* add something here ?*)
    1.99 +                                                                   (
   1.100 +                                                                      goals_being_watched := (!goals_being_watched) -1;
   1.101 +                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.102 +                                                                       Pretty.writeln(Pretty.str ("Ran out of options in handler"));
   1.103 +                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.104 +                                                                       if (!goals_being_watched = 0)
   1.105 +                                                                       then 
   1.106 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
   1.107 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.108 +                                                                               val _ =  TextIO.closeOut outfile
   1.109 +                                                                            in
   1.110 +                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   1.111 +                                                                            end )
   1.112 +                                                                       else
   1.113 +                                                                          ( )
   1.114 +                                                                      )
   1.115 +                                                                     
   1.116 +                                                                           
   1.117                                                              
   1.118                                         end)
   1.119