improved formatting;
authorwenzelm
Mon Jun 20 21:34:31 2005 +0200 (2005-06-20)
changeset 16480abf475cf11f2
parent 16479 cf872f3e16d9
child 16481 fe61cdf5af51
improved formatting;
src/HOL/Tools/ATP/VampCommunication.ML
src/HOL/Tools/ATP/VampireCommunication.ML
     1.1 --- a/src/HOL/Tools/ATP/VampCommunication.ML	Mon Jun 20 21:33:27 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/VampCommunication.ML	Mon Jun 20 21:34:31 2005 +0200
     1.3 @@ -11,9 +11,9 @@
     1.4    sig
     1.5      val reconstruct : bool ref
     1.6      val getVampInput : TextIO.instream -> string * string * string
     1.7 -    val checkVampProofFound:  TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
     1.8 +    val checkVampProofFound:  TextIO.instream * TextIO.outstream * Posix.Process.pid * string *
     1.9                                 string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array  * int -> bool
    1.10 -    
    1.11 +
    1.12    end;
    1.13  
    1.14  structure VampComm :VAMP_COMM =
    1.15 @@ -26,12 +26,13 @@
    1.16  (*  Write Vamp   output to a file *)
    1.17  (***********************************)
    1.18  
    1.19 -fun logVampInput (instr, fd) = let val thisLine = TextIO.inputLine instr 
    1.20 -			 in if (thisLine = "%==============  End of proof. ==================\n" )
    1.21 -			    then TextIO.output (fd, thisLine)
    1.22 -      			  else (
    1.23 -				TextIO.output (fd, thisLine); logVampInput (instr,fd))
    1.24 - 			 end;
    1.25 +fun logVampInput (instr, fd) =
    1.26 +    let val thisLine = TextIO.inputLine instr
    1.27 +    in if (thisLine = "%==============  End of proof. ==================\n" )
    1.28 +       then TextIO.output (fd, thisLine)
    1.29 +       else (
    1.30 +             TextIO.output (fd, thisLine); logVampInput (instr,fd))
    1.31 +    end;
    1.32  
    1.33  (**********************************************************************)
    1.34  (*  Reconstruct the Vamp proof w.r.t. thmstring (string version of   *)
    1.35 @@ -43,49 +44,51 @@
    1.36  val atomize_tac =
    1.37      SUBGOAL
    1.38       (fn (prop,_) =>
    1.39 -	 let val ts = Logic.strip_assums_hyp prop
    1.40 -	 in EVERY1 
    1.41 -		[METAHYPS
    1.42 -		     (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
    1.43 -	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    1.44 +         let val ts = Logic.strip_assums_hyp prop
    1.45 +         in EVERY1
    1.46 +                [METAHYPS
    1.47 +                     (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
    1.48 +          REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    1.49       end);
    1.50  
    1.51  
    1.52 -fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr  (num_of_clauses:int ) = 
    1.53 - let val foo =   TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3")));
    1.54 - in
    1.55 -SELECT_GOAL
    1.56 -  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    1.57 -  METAHYPS(fn negs => ((*if !reconstruct 
    1.58 -		       then 
    1.59 -			   Recon_Transfer.vampString_to_reconString proofextract thmstring goalstring 
    1.60 -								     toParent ppid negs clause_arr  num_of_clauses 
    1.61 -		       else*)
    1.62 -			   Recon_Transfer.vampString_to_lemmaString proofextract thmstring goalstring 
    1.63 -								     toParent ppid negs clause_arr  num_of_clauses ))]) sg_num	
    1.64 - end ;
    1.65 +fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr  (num_of_clauses:int ) =
    1.66 +  let val foo =   TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3")));
    1.67 +  in
    1.68 +    SELECT_GOAL
    1.69 +      (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
    1.70 +               METAHYPS(fn negs =>
    1.71 +                           ((*if !reconstruct
    1.72 +                              then
    1.73 +                                Recon_Transfer.vampString_to_reconString proofextract thmstring goalstring
    1.74 +                                                                         toParent ppid negs clause_arr  num_of_clauses
    1.75 +                              else*)
    1.76 +                            Recon_Transfer.vampString_to_lemmaString proofextract thmstring goalstring
    1.77 +                                                                     toParent ppid negs clause_arr  num_of_clauses ))]) sg_num
    1.78 +  end ;
    1.79  
    1.80  
    1.81 -fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr,  num_of_clauses) = let 
    1.82 -                         val thisLine = TextIO.inputLine fromChild 
    1.83 -			 in 
    1.84 -                            if (thisLine = "%==============  End of proof. ==================\n" )
    1.85 -			    then ( 
    1.86 -                                    let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    1.87 -                                        val foo =   TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar2")));
    1.88 -                                
    1.89 -			            in 
    1.90 +fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr,  num_of_clauses) =
    1.91 +  let
    1.92 +    val thisLine = TextIO.inputLine fromChild
    1.93 +  in
    1.94 +    if (thisLine = "%==============  End of proof. ==================\n" )
    1.95 +    then (
    1.96 +          let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    1.97 +              val foo =   TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar2")));
    1.98 +
    1.99 +          in
   1.100  
   1.101 -                                        TextIO.output(foo,(proofextract));TextIO.closeOut foo;
   1.102 -                                        reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  clause_arr  num_of_clauses thm
   1.103 -                                               
   1.104 -                                    end
   1.105 -                                  )
   1.106 -      			    else (
   1.107 -				
   1.108 -                                transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num, clause_arr,  num_of_clauses)
   1.109 -                                )
   1.110 - 			 end;
   1.111 +            TextIO.output(foo,(proofextract));TextIO.closeOut foo;
   1.112 +            reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  clause_arr  num_of_clauses thm
   1.113 +
   1.114 +          end
   1.115 +            )
   1.116 +    else (
   1.117 +
   1.118 +          transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num, clause_arr,  num_of_clauses)
   1.119 +          )
   1.120 +  end;
   1.121  
   1.122  
   1.123  
   1.124 @@ -95,187 +98,184 @@
   1.125  (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   1.126  (*********************************************************************************)
   1.127  
   1.128 - 
   1.129 -fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = 
   1.130 -                                      (*let val _ = Posix.Process.wait ()
   1.131 -                                      in*)
   1.132 -                                       
   1.133 -                                       if (isSome (TextIO.canInput(fromChild, 5)))
   1.134 -                                       then
   1.135 -                                       (
   1.136 -                                       let val thisLine = TextIO.inputLine fromChild  
   1.137 -                                           in                 
   1.138 -                                              if (thisLine = "%================== Proof: ======================\n")
   1.139 -                                             then     
   1.140 -                                              ( 
   1.141 -                                                 let 
   1.142 -                                               val outfile =  TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_transfer")));
   1.143 -                                               val _=  TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm));
   1.144 -                                               val _ =  TextIO.closeOut outfile;
   1.145 -                                               in
   1.146 -                                                transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num,clause_arr,  num_of_clauses);
   1.147 -                                                true
   1.148 -                                               end)
   1.149 -                                             
   1.150 -                                             else 
   1.151 -                                                (
   1.152 -                                                 startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses)
   1.153 -                                                )
   1.154 -                                            end
   1.155 -                                           )
   1.156 -                                         else (false)
   1.157 -                                     (*  end*)
   1.158 +
   1.159 +fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) =
   1.160 +    (*let val _ = Posix.Process.wait ()
   1.161 +      in*)
   1.162 +
   1.163 +    if (isSome (TextIO.canInput(fromChild, 5)))
   1.164 +    then
   1.165 +      (
   1.166 +       let val thisLine = TextIO.inputLine fromChild
   1.167 +       in
   1.168 +         if (thisLine = "%================== Proof: ======================\n")
   1.169 +         then
   1.170 +           (
   1.171 +            let
   1.172 +              val outfile =  TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_transfer")));
   1.173 +                  val _=  TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm));
   1.174 +                      val _ =  TextIO.closeOut outfile;
   1.175 +            in
   1.176 +              transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num,clause_arr,  num_of_clauses);
   1.177 +              true
   1.178 +            end)
   1.179 +
   1.180 +         else
   1.181 +           (
   1.182 +            startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses)
   1.183 +            )
   1.184 +       end
   1.185 +         )
   1.186 +    else (false)
   1.187 +(*  end*)
   1.188  
   1.189  
   1.190  
   1.191 -fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr,  (num_of_clauses:int )) = 
   1.192 -                                       let val vamp_proof_file =  TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "vamp_proof")))
   1.193 -                                            val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_checkvamp")));                                                                            
   1.194 -                                            val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm))
   1.195 -                                             
   1.196 -                                            val _ =  TextIO.closeOut outfile
   1.197 -                                       in 
   1.198 -                                       if (isSome (TextIO.canInput(fromChild, 5)))
   1.199 -                                       then
   1.200 -                                       (
   1.201 -                                       let val thisLine = TextIO.inputLine fromChild  
   1.202 -                                           in if (thisLine = "% Proof found. Thanks to Tanya!\n" )
   1.203 -                                              then      
   1.204 -                                              (  
   1.205 -                                                 let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   1.206 -                                                     val _ = TextIO.output (outfile, (thisLine))
   1.207 -                                             
   1.208 -                                                     val _ =  TextIO.closeOut outfile
   1.209 -                                                 in 
   1.210 -                                                    startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses) 
   1.211 -                                                 end
   1.212 -                                               )   
   1.213 -                                               else if (thisLine = "% Unprovable.\n" ) 
   1.214 -                                                   then  
   1.215 +fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr,  (num_of_clauses:int )) =
   1.216 +    let val vamp_proof_file =  TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "vamp_proof")))
   1.217 +        val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_checkvamp")));
   1.218 +             val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm))
   1.219 +
   1.220 +             val _ =  TextIO.closeOut outfile
   1.221 +    in
   1.222 +      if (isSome (TextIO.canInput(fromChild, 5)))
   1.223 +      then
   1.224 +        (
   1.225 +         let val thisLine = TextIO.inputLine fromChild
   1.226 +         in if (thisLine = "% Proof found. Thanks to Tanya!\n" )
   1.227 +            then
   1.228 +              (
   1.229 +               let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   1.230 +                        val _ = TextIO.output (outfile, (thisLine))
   1.231 +
   1.232 +                        val _ =  TextIO.closeOut outfile
   1.233 +               in
   1.234 +                 startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses)
   1.235 +               end
   1.236 +                 )
   1.237 +            else if (thisLine = "% Unprovable.\n" )
   1.238 +            then
   1.239 +
   1.240 +              (
   1.241 +               let    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   1.242 +                           val _ = TextIO.output (outfile, (thisLine))
   1.243 +
   1.244 +                           val _ =  TextIO.closeOut outfile
   1.245 +               in
   1.246  
   1.247 -                                                 (
   1.248 -                                                      let    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   1.249 -                                                             val _ = TextIO.output (outfile, (thisLine))
   1.250 -                                             
   1.251 -                                                             val _ =  TextIO.closeOut outfile
   1.252 -                                                      in
   1.253 -                                                       
   1.254 -                                                        TextIO.output (toParent,childCmd^"\n" );
   1.255 -                                                        TextIO.flushOut toParent;
   1.256 -                                                        TextIO.output (vamp_proof_file, (thisLine));
   1.257 -                                                        TextIO.flushOut vamp_proof_file;
   1.258 -                                                        TextIO.closeOut vamp_proof_file;
   1.259 -                                                        (*TextIO.output (toParent, thisLine);
   1.260 -                                                        TextIO.flushOut toParent;
   1.261 -                                                        TextIO.output (toParent, "bar\n");
   1.262 -                                                        TextIO.flushOut toParent;*)
   1.263 +                 TextIO.output (toParent,childCmd^"\n" );
   1.264 +                 TextIO.flushOut toParent;
   1.265 +                 TextIO.output (vamp_proof_file, (thisLine));
   1.266 +                 TextIO.flushOut vamp_proof_file;
   1.267 +                 TextIO.closeOut vamp_proof_file;
   1.268 +                 (*TextIO.output (toParent, thisLine);
   1.269 +                  TextIO.flushOut toParent;
   1.270 +                  TextIO.output (toParent, "bar\n");
   1.271 +                  TextIO.flushOut toParent;*)
   1.272  
   1.273 -                                                       TextIO.output (toParent, thisLine^"\n");
   1.274 -                                                       TextIO.flushOut toParent;
   1.275 -                                                       TextIO.output (toParent, thmstring^"\n");
   1.276 -                                                       TextIO.flushOut toParent;
   1.277 -                                                       TextIO.output (toParent, goalstring^"\n");
   1.278 -                                                       TextIO.flushOut toParent;
   1.279 -                                                       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.280 -                                                       (* Attempt to prevent several signals from turning up simultaneously *)
   1.281 -                                                       Posix.Process.sleep(Time.fromSeconds 1);
   1.282 -                                                        true  
   1.283 -                                                      end) 
   1.284 -                                                     else if (thisLine = "% Proof not found.\n")
   1.285 -                                                          then  
   1.286 -                                                (
   1.287 -                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.288 -                                                        TextIO.output (toParent,childCmd^"\n" );
   1.289 -                                                        TextIO.flushOut toParent;
   1.290 -                                                        TextIO.output (toParent, thisLine);
   1.291 -                                                        TextIO.flushOut toParent;
   1.292 +                 TextIO.output (toParent, thisLine^"\n");
   1.293 +                 TextIO.flushOut toParent;
   1.294 +                 TextIO.output (toParent, thmstring^"\n");
   1.295 +                 TextIO.flushOut toParent;
   1.296 +                 TextIO.output (toParent, goalstring^"\n");
   1.297 +                 TextIO.flushOut toParent;
   1.298 +                 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.299 +                 (* Attempt to prevent several signals from turning up simultaneously *)
   1.300 +                 Posix.Process.sleep(Time.fromSeconds 1);
   1.301 +                 true
   1.302 +               end)
   1.303 +            else if (thisLine = "% Proof not found.\n")
   1.304 +            then
   1.305 +              (
   1.306 +               Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.307 +               TextIO.output (toParent,childCmd^"\n" );
   1.308 +               TextIO.flushOut toParent;
   1.309 +               TextIO.output (toParent, thisLine);
   1.310 +               TextIO.flushOut toParent;
   1.311  
   1.312 -                                                        true) 
   1.313 -                                                          
   1.314 -                                                    else
   1.315 -                                                       (TextIO.output (vamp_proof_file, (thisLine));
   1.316 -                                                       TextIO.flushOut vamp_proof_file;
   1.317 -                                                       checkVampProofFound  (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses))
   1.318 +               true)
   1.319 +
   1.320 +            else
   1.321 +              (TextIO.output (vamp_proof_file, (thisLine));
   1.322 +               TextIO.flushOut vamp_proof_file;
   1.323 +               checkVampProofFound  (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses))
   1.324  
   1.325 -                                              end
   1.326 -                                          )
   1.327 -                                         else 
   1.328 -                                             (TextIO.output (vamp_proof_file, ("No proof output seen \n"));TextIO.closeOut vamp_proof_file;false)
   1.329 -                                      end
   1.330 +         end
   1.331 +           )
   1.332 +      else
   1.333 +        (TextIO.output (vamp_proof_file, ("No proof output seen \n"));TextIO.closeOut vamp_proof_file;false)
   1.334 +    end
   1.335  
   1.336 -  
   1.337 +
   1.338  (***********************************************************************)
   1.339  (*  Function used by the Isabelle process to read in a vamp proof   *)
   1.340  (***********************************************************************)
   1.341  
   1.342 -
   1.343 +fun getVampInput instr =
   1.344 +    if (isSome (TextIO.canInput(instr, 2)))
   1.345 +    then
   1.346 +      let val thisLine = TextIO.inputLine instr
   1.347 +          val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
   1.348  
   1.349 -fun getVampInput instr = if (isSome (TextIO.canInput(instr, 2)))
   1.350 -                          then
   1.351 -                               let val thisLine = TextIO.inputLine instr 
   1.352 -                                   val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
   1.353 -                                             
   1.354 -                                   val _ =  TextIO.closeOut outfile
   1.355 -			       in    (* reconstructed proof string *)
   1.356 -                                     if ( (substring (thisLine, 0,1))= "[")
   1.357 -                                     then 
   1.358 -			                 (*Pretty.writeln(Pretty.str (thisLine))*)
   1.359 -                                             let val reconstr = thisLine
   1.360 -                                                 val thmstring = TextIO.inputLine instr 
   1.361 -                                                 val goalstring = TextIO.inputLine instr   
   1.362 -                                             in
   1.363 -                                                 (reconstr, thmstring, goalstring)
   1.364 -                                             end
   1.365 -                                     else if (thisLine = "% Unprovable.\n" ) 
   1.366 -                                          then 
   1.367 -                                          (
   1.368 -                                             let val reconstr = thisLine
   1.369 -                                                 val thmstring = TextIO.inputLine instr
   1.370 -                                                 val goalstring = TextIO.inputLine instr
   1.371 -                                             in
   1.372 -                                                 (reconstr, thmstring, goalstring)
   1.373 -                                             end
   1.374 -                                          )
   1.375 -					else  if (thisLine = "% Proof not found.\n")
   1.376 -                                          then 
   1.377 -                                          (
   1.378 -                                             let val reconstr = thisLine
   1.379 -                                                 val thmstring = TextIO.inputLine instr
   1.380 -                                                 val goalstring = TextIO.inputLine instr
   1.381 -                                             in
   1.382 -                                                 (reconstr, thmstring, goalstring)
   1.383 -                                             end
   1.384 -                                          )
   1.385 -					else if (String.isPrefix   "Rules from"  thisLine)
   1.386 -                                        then 
   1.387 -                                          (
   1.388 -                                             let val reconstr = thisLine
   1.389 -                                                 val thmstring = TextIO.inputLine instr
   1.390 -                                                 val goalstring = TextIO.inputLine instr
   1.391 -                                             in
   1.392 -                                                 (reconstr, thmstring, goalstring)
   1.393 -                                             end
   1.394 -                                          )
   1.395 +                                                                                                                                                                            val _ =  TextIO.closeOut outfile
   1.396 +      in    (* reconstructed proof string *)
   1.397 +        if ( (substring (thisLine, 0,1))= "[")
   1.398 +        then
   1.399 +          (*Pretty.writeln(Pretty.str (thisLine))*)
   1.400 +          let val reconstr = thisLine
   1.401 +              val thmstring = TextIO.inputLine instr
   1.402 +              val goalstring = TextIO.inputLine instr
   1.403 +          in
   1.404 +            (reconstr, thmstring, goalstring)
   1.405 +          end
   1.406 +        else if (thisLine = "% Unprovable.\n" )
   1.407 +        then
   1.408 +          (
   1.409 +           let val reconstr = thisLine
   1.410 +               val thmstring = TextIO.inputLine instr
   1.411 +               val goalstring = TextIO.inputLine instr
   1.412 +           in
   1.413 +             (reconstr, thmstring, goalstring)
   1.414 +           end
   1.415 +             )
   1.416 +        else  if (thisLine = "% Proof not found.\n")
   1.417 +        then
   1.418 +          (
   1.419 +           let val reconstr = thisLine
   1.420 +               val thmstring = TextIO.inputLine instr
   1.421 +               val goalstring = TextIO.inputLine instr
   1.422 +           in
   1.423 +             (reconstr, thmstring, goalstring)
   1.424 +           end
   1.425 +             )
   1.426 +        else if (String.isPrefix   "Rules from"  thisLine)
   1.427 +        then
   1.428 +          (
   1.429 +           let val reconstr = thisLine
   1.430 +               val thmstring = TextIO.inputLine instr
   1.431 +               val goalstring = TextIO.inputLine instr
   1.432 +           in
   1.433 +             (reconstr, thmstring, goalstring)
   1.434 +           end
   1.435 +             )
   1.436  
   1.437 -                                         else if (thisLine = "Proof found but translation failed!")
   1.438 -                                              then
   1.439 -  						(
   1.440 -						   let val reconstr = thisLine
   1.441 -                                                       val thmstring = TextIO.inputLine instr
   1.442 -                                                       val goalstring = TextIO.inputLine instr
   1.443 -						      val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_getVamp")));
   1.444 -                                    		val _ = TextIO.output (outfile, (thisLine))
   1.445 -                                     			 val _ =  TextIO.closeOut outfile
   1.446 -                                                   in
   1.447 -                                                      (reconstr, thmstring, goalstring)
   1.448 -                                                   end
   1.449 -						)
   1.450 -                                        	 else
   1.451 -                                                     getVampInput instr
   1.452 -                                            
   1.453 - 			        end
   1.454 -                          else 
   1.455 -                              ("No output from reconstruction process.\n","","")
   1.456 +        else if (thisLine = "Proof found but translation failed!")
   1.457 +        then
   1.458 +          (
   1.459 +           let val reconstr = thisLine
   1.460 +               val thmstring = TextIO.inputLine instr
   1.461 +               val goalstring = TextIO.inputLine instr
   1.462 +               val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_getVamp")));
   1.463 +                    val _ = TextIO.output (outfile, (thisLine))
   1.464 +                    val _ =  TextIO.closeOut outfile
   1.465 +           in
   1.466 +             (reconstr, thmstring, goalstring)
   1.467 +           end
   1.468 +             )
   1.469 +        else
   1.470 +          getVampInput instr
   1.471  
   1.472 -
   1.473 +      end
   1.474 +    else
   1.475 +      ("No output from reconstruction process.\n","","")
   1.476  end;
     2.1 --- a/src/HOL/Tools/ATP/VampireCommunication.ML	Mon Jun 20 21:33:27 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/VampireCommunication.ML	Mon Jun 20 21:34:31 2005 +0200
     2.3 @@ -4,6 +4,8 @@
     2.4      Copyright   2004  University of Cambridge
     2.5  *)
     2.6  
     2.7 +(* FIXME proper structure definition *)
     2.8 +
     2.9  (***************************************************************************)
    2.10  (*  Code to deal with the transfer of proofs from a Vampire process        *)
    2.11  (***************************************************************************)
    2.12 @@ -12,32 +14,34 @@
    2.13  (*  Write vampire output to a file *)
    2.14  (***********************************)
    2.15  
    2.16 -fun logVampInput (instr, fd) = let val thisLine = TextIO.inputLine instr 
    2.17 -			 in if thisLine = "%==============  End of proof. ==================\n" 
    2.18 -			    then TextIO.output (fd, thisLine)
    2.19 -      			  else (
    2.20 -				TextIO.output (fd, thisLine); logVampInput (instr,fd))
    2.21 - 			 end;
    2.22 +fun logVampInput (instr, fd) =
    2.23 +    let val thisLine = TextIO.inputLine instr
    2.24 +    in if thisLine = "%==============  End of proof. ==================\n"
    2.25 +       then TextIO.output (fd, thisLine)
    2.26 +       else (
    2.27 +             TextIO.output (fd, thisLine); logVampInput (instr,fd))
    2.28 +    end;
    2.29  
    2.30  (**********************************************************************)
    2.31  (*  Transfer the vampire output from the watcher to the input pipe of *)
    2.32  (*  the main Isabelle process                                         *)
    2.33  (**********************************************************************)
    2.34  
    2.35 -fun transferVampInput (fromChild, toParent, ppid) = let 
    2.36 -                         val thisLine = TextIO.inputLine fromChild 
    2.37 -			 in 
    2.38 -                            if (thisLine = "%==============  End of proof. ==================\n" )
    2.39 -			    then ( 
    2.40 -                                   TextIO.output (toParent, thisLine);
    2.41 -                                   TextIO.flushOut toParent
    2.42 -                                  )
    2.43 -      			    else (
    2.44 -				TextIO.output (toParent, thisLine); 
    2.45 -                                TextIO.flushOut toParent;
    2.46 -                                transferVampInput (fromChild, toParent, ppid)
    2.47 -                                )
    2.48 - 			 end;
    2.49 +fun transferVampInput (fromChild, toParent, ppid) =
    2.50 +    let
    2.51 +      val thisLine = TextIO.inputLine fromChild
    2.52 +    in
    2.53 +      if (thisLine = "%==============  End of proof. ==================\n" )
    2.54 +      then (
    2.55 +            TextIO.output (toParent, thisLine);
    2.56 +            TextIO.flushOut toParent
    2.57 +            )
    2.58 +      else (
    2.59 +            TextIO.output (toParent, thisLine);
    2.60 +            TextIO.flushOut toParent;
    2.61 +            transferVampInput (fromChild, toParent, ppid)
    2.62 +            )
    2.63 +    end;
    2.64  
    2.65  
    2.66  (*********************************************************************************)
    2.67 @@ -45,74 +49,63 @@
    2.68  (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    2.69  (*********************************************************************************)
    2.70  
    2.71 -fun startVampireTransfer (fromChild, toParent, ppid, childCmd) = 
    2.72 -                                       if (isSome (TextIO.canInput(fromChild, 5)))
    2.73 -                                       then
    2.74 -                                       (
    2.75 -                                       let val thisLine = TextIO.inputLine fromChild  
    2.76 -                                           in                 
    2.77 -                                             if (thisLine = "% Proof found. Thanks to Tanya!\n" )
    2.78 -                                             then      
    2.79 -                                              ( 
    2.80 -                                                Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
    2.81 -                                                TextIO.output (toParent,childCmd^"\n" );
    2.82 -                                                TextIO.flushOut toParent;
    2.83 -                                                TextIO.output (toParent, thisLine);
    2.84 -                                                TextIO.flushOut toParent;
    2.85 +fun startVampireTransfer (fromChild, toParent, ppid, childCmd) =
    2.86 +    if (isSome (TextIO.canInput(fromChild, 5)))
    2.87 +    then
    2.88 +      (
    2.89 +       let val thisLine = TextIO.inputLine fromChild
    2.90 +       in
    2.91 +         if (thisLine = "% Proof found. Thanks to Tanya!\n" )
    2.92 +         then
    2.93 +           (
    2.94 +            Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
    2.95 +            TextIO.output (toParent,childCmd^"\n" );
    2.96 +            TextIO.flushOut toParent;
    2.97 +            TextIO.output (toParent, thisLine);
    2.98 +            TextIO.flushOut toParent;
    2.99  
   2.100 -                                                transferVampInput (fromChild, toParent, ppid);
   2.101 -                                                true)
   2.102 -                                              else if (thisLine = "% Unprovable.\n" ) 
   2.103 -                                                   then 
   2.104 -                                                       (
   2.105 -                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
   2.106 -                                                        TextIO.output (toParent,childCmd^"\n" );
   2.107 -                                                        TextIO.flushOut toParent;
   2.108 -                                                        TextIO.output (toParent, thisLine);
   2.109 -                                                        TextIO.flushOut toParent;
   2.110 +            transferVampInput (fromChild, toParent, ppid);
   2.111 +            true)
   2.112 +         else if (thisLine = "% Unprovable.\n" )
   2.113 +         then
   2.114 +           (
   2.115 +            Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
   2.116 +            TextIO.output (toParent,childCmd^"\n" );
   2.117 +            TextIO.flushOut toParent;
   2.118 +            TextIO.output (toParent, thisLine);
   2.119 +            TextIO.flushOut toParent;
   2.120  
   2.121 -                                                        true)
   2.122 -                                                   else if (thisLine = "% Proof not found.\n")
   2.123 -                                                        then 
   2.124 -                                                            (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);                                                            TextIO.output (toParent,childCmd^"\n" );
   2.125 -                                                             TextIO.flushOut toParent;
   2.126 -                                                             TextIO.output (toParent, thisLine);
   2.127 -                                                             TextIO.flushOut toParent;
   2.128 -                                                             true)
   2.129 -                                                        else 
   2.130 -                                                           (
   2.131 -                                                             startVampireTransfer (fromChild, toParent, ppid, childCmd)
   2.132 -                                                            )
   2.133 -                                            end
   2.134 -                                           )
   2.135 -                                         else (false)
   2.136 +            true)
   2.137 +         else if (thisLine = "% Proof not found.\n")
   2.138 +         then
   2.139 +           (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
   2.140 +            TextIO.output (toParent,childCmd^"\n" );
   2.141 +            TextIO.flushOut toParent;
   2.142 +            TextIO.output (toParent, thisLine);
   2.143 +            TextIO.flushOut toParent;
   2.144 +            true)
   2.145 +         else
   2.146 +           (
   2.147 +            startVampireTransfer (fromChild, toParent, ppid, childCmd)
   2.148 +            )
   2.149 +       end
   2.150 +         )
   2.151 +    else (false)
   2.152  
   2.153  
   2.154  (***********************************************************************)
   2.155  (*  Function used by the Isabelle process to read in a vampire proof   *)
   2.156  (***********************************************************************)
   2.157  
   2.158 -fun getVampInput instr = let val thisLine = TextIO.inputLine instr 
   2.159 -			 in 
   2.160 -                           if (thisLine = "%==============  End of proof. ==================\n" )
   2.161 -			    then
   2.162 -                               (
   2.163 -                                (Pretty.writeln(Pretty.str  (concat["vampire",thisLine])));()
   2.164 -                               )
   2.165 -                             else if (thisLine = "% Unprovable.\n" ) 
   2.166 -                                  then 
   2.167 -                                     (
   2.168 -                                      (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
   2.169 -                                      )
   2.170 -                                   else if (thisLine = "% Proof not found.\n")
   2.171 -                                        then 
   2.172 -                                            (
   2.173 -                                             Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
   2.174 -                                             )
   2.175 -
   2.176 -
   2.177 -                                         else 
   2.178 -                                            (
   2.179 -				              Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
   2.180 -                                             )
   2.181 - 			 end;
   2.182 +fun getVampInput instr =
   2.183 +  let val thisLine = TextIO.inputLine instr
   2.184 +  in
   2.185 +    if thisLine = "%==============  End of proof. ==================\n" then
   2.186 +      Pretty.writeln (Pretty.str (concat ["vampire", thisLine]))
   2.187 +    else if thisLine = "% Unprovable.\n" then
   2.188 +      Pretty.writeln (Pretty.str (concat ["vampire", thisLine]))
   2.189 +    else if thisLine = "% Proof not found.\n" then
   2.190 +      Pretty.writeln (Pretty.str (concat ["vampire", thisLine]))
   2.191 +    else
   2.192 +      (Pretty.writeln (Pretty.str (concat ["vampire", thisLine])); getVampInput instr)
   2.193 +  end;