src/HOL/Tools/ATP/watcher.ML
changeset 16675 96bdc59afc05
parent 16561 2bc33f0cfe9a
child 16767 2d4433759b8d
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Mon Jul 04 15:15:55 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Mon Jul 04 15:51:56 2005 +0200
     1.3 @@ -165,8 +165,8 @@
     1.4                               (prover^thmstring^goalstring^proverCmd^settings^
     1.5                                clasimpfile^hypsfile^probfile)
     1.6        in sendOutput (toWatcherStr,    
     1.7 -            (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^
     1.8 -             settings^"*"^clasimpfile^"*"^hypsfile^"*"^probfile^"\n"));
     1.9 +            (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^
    1.10 +             settings^"$"^clasimpfile^"$"^hypsfile^"$"^probfile^"\n"));
    1.11           goals_being_watched := (!goals_being_watched) + 1;
    1.12  	 TextIO.flushOut toWatcherStr;
    1.13  	 callResProvers (toWatcherStr,args)
    1.14 @@ -213,33 +213,33 @@
    1.15    let val  outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field")))                                                                         
    1.16        val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") )
    1.17        val _ =  TextIO.closeOut outfile
    1.18 -      val (prover, rest) = takeUntil "*" str []
    1.19 +      val (prover, rest) = takeUntil "$" str []
    1.20        val prover = implode prover
    1.21  
    1.22 -      val (thmstring, rest) =  takeUntil "*" rest []
    1.23 +      val (thmstring, rest) =  takeUntil "$" rest []
    1.24        val thmstring = implode thmstring
    1.25  
    1.26 -      val (goalstring, rest) =  takeUntil "*" rest []
    1.27 +      val (goalstring, rest) =  takeUntil "$" rest []
    1.28        val goalstring = implode goalstring
    1.29  
    1.30 -      val (proverCmd, rest ) =  takeUntil "*" rest []
    1.31 +      val (proverCmd, rest ) =  takeUntil "$" rest []
    1.32        val proverCmd = implode proverCmd
    1.33        
    1.34 -      val (settings, rest) =  takeUntil "*" rest []
    1.35 +      val (settings, rest) =  takeUntil "$" rest []
    1.36        val settings = getSettings settings []
    1.37  
    1.38 -      val (clasimpfile, rest ) =  takeUntil "*" rest []
    1.39 +      val (clasimpfile, rest ) =  takeUntil "$" rest []
    1.40        val clasimpfile = implode clasimpfile
    1.41        
    1.42 -      val (hypsfile, rest ) =  takeUntil "*" rest []
    1.43 +      val (hypsfile, rest ) =  takeUntil "$" rest []
    1.44        val hypsfile = implode hypsfile
    1.45  
    1.46 -      val (file, rest) =  takeUntil "*" rest []
    1.47 +      val (file, rest) =  takeUntil "$" rest []
    1.48        val file = implode file
    1.49  
    1.50        val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
    1.51                    ("Sep comms are: "^(implode str)^"**"^
    1.52 -                   prover^thmstring^goalstring^proverCmd^clasimpfile^hypsfile^file^"\n\n")
    1.53 +                   prover^" thmstring: "^thmstring^"\n goalstr:  "^goalstring^" \n provercmd: "^proverCmd^" \n  clasimp "^clasimpfile^" \n hyps "^hypsfile^"\n prob  "^file^"\n\n")
    1.54    in
    1.55       (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file)
    1.56    end
    1.57 @@ -289,6 +289,7 @@
    1.58      val newfile =   if !SpassComm.spass 
    1.59  		    then 
    1.60  			    dfg_path^"/ax_prob"^"_"^(probID)^".dfg" 
    1.61 +
    1.62  		    else
    1.63  			    (File.platform_path wholefile)
    1.64      val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
    1.65 @@ -813,6 +814,8 @@
    1.66                             VampComm.getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
    1.67                            
    1.68  
    1.69 +
    1.70 +
    1.71  fun spass_proofHandler (n) = (
    1.72                                   let  val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
    1.73                                        val _ = TextIO.output (outfile, ("In signal handler now\n"))
    1.74 @@ -844,9 +847,8 @@
    1.75                                                                   else
    1.76                                                                      ()
    1.77                                                              )
    1.78 -                                                    (* if there's no proof, but a message from Spass *)
    1.79 -                                                    else if ((substring (reconstr, 0,5))= "SPASS")
    1.80 -                                                         then
    1.81 +                                                    (* if there's no proof, but a some sort of  message from Spass *)
    1.82 +                                                    else 
    1.83                                                                   (
    1.84                                                                       goals_being_watched := (!goals_being_watched) -1;
    1.85                                                                       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.86 @@ -862,67 +864,7 @@
    1.87                                                                             end )
    1.88                                                                        else
    1.89                                                                           ()
    1.90 -                                                                ) 
    1.91 -						   (* print out a list of rules used from clasimpset*)
    1.92 -                                                    else if ((substring (reconstr, 0,5))= "Rules")
    1.93 -                                                         then
    1.94 -                                                                 (
    1.95 -                                                                     goals_being_watched := (!goals_being_watched) -1;
    1.96 -                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    1.97 -                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
    1.98 -                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
    1.99 -                                                                      if (!goals_being_watched = 0)
   1.100 -                                                                      then 
   1.101 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   1.102 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.103 -                                                                               val _ =  TextIO.closeOut outfile
   1.104 -                                                                           in
   1.105 -                                                                              killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   1.106 -                                                                           end )
   1.107 -                                                                      else
   1.108 -                                                                         ()
   1.109 -                                                                )
   1.110 -							
   1.111 -                                                          (* if proof translation failed *)
   1.112 -                                                          else if ((substring (reconstr, 0,5)) = "Proof")
   1.113 -                                                               then 
   1.114 -                                                                   (
   1.115 -                                                                      goals_being_watched := (!goals_being_watched) -1;
   1.116 -                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.117 -                                                                       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   1.118 -                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.119 -                                                                       if (!goals_being_watched = 0)
   1.120 -                                                                       then 
   1.121 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
   1.122 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.123 -                                                                               val _ =  TextIO.closeOut outfile
   1.124 -                                                                            in
   1.125 -                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   1.126 -                                                                            end )
   1.127 -                                                                       else
   1.128 -                                                                          ( )
   1.129 -                                                                      )
   1.130 -
   1.131 -
   1.132 -                                                                else  (* add something here ?*)
   1.133 -                                                                   (
   1.134 -                                                                      goals_being_watched := (!goals_being_watched) -1;
   1.135 -                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.136 -                                                                       Pretty.writeln(Pretty.str ("Ran out of options in handler"));
   1.137 -                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.138 -                                                                       if (!goals_being_watched = 0)
   1.139 -                                                                       then 
   1.140 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
   1.141 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.142 -                                                                               val _ =  TextIO.closeOut outfile
   1.143 -                                                                            in
   1.144 -                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   1.145 -                                                                            end )
   1.146 -                                                                       else
   1.147 -                                                                          ( )
   1.148 -                                                                      )
   1.149 -                                                                     
   1.150 -                                                                           
   1.151 +                                                                )						               
   1.152                                                              
   1.153                                         end)
   1.154