src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 15782 a1863ea9052b
parent 15774 9df37a0e935d
child 15787 8fad4bd4e53c
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Apr 20 17:19:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Apr 20 18:01:50 2005 +0200
     1.3 @@ -151,17 +151,19 @@
     1.4  |   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
     1.5  
     1.6  
     1.7 - fun get_axioms_used proof_steps thmstring = let 
     1.8 -                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
     1.9 + fun get_axioms_used proof_steps thms = let 
    1.10 +                                             (*val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    1.11                                               val _ = TextIO.output (outfile, thmstring)
    1.12                                               
    1.13 -                                             val _ =  TextIO.closeOut outfile
    1.14 +                                             val _ =  TextIO.closeOut outfile*)
    1.15                                              (* not sure why this is necessary again, but seems to be *)
    1.16 +
    1.17                                              val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.18                                              val axioms = get_init_axioms proof_steps
    1.19                                              val step_nums = get_step_nums axioms []
    1.20 -                                            val thm = thm_of_string thmstring
    1.21 -                                            val clauses = make_clauses [thm]
    1.22 +                                      
    1.23 +                                           
    1.24 +                                            val clauses = make_clauses thms
    1.25                                              
    1.26                                              val vars = map thm_vars clauses
    1.27                                             
    1.28 @@ -298,14 +300,20 @@
    1.29  
    1.30  *)
    1.31  
    1.32 +val dummy_tac = PRIMITIVE(fn thm => thm );
    1.33  
    1.34 -fun spassString_to_reconString proofstr thmstring = 
    1.35 -                                              let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                                                                      val _= warning("proofstr is: "^proofstr);
    1.36 -                                                  val _ = warning ("thmstring is: "^thmstring);
    1.37 -                                                  val _ = TextIO.output (outfile, (thmstring))
    1.38 +fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms= 
    1.39 +                                              let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                        
    1.40 +                                                  (* val sign = sign_of_thm thm
    1.41 +                                                 val prems = prems_of thm
    1.42 +                                                 val prems_string =  concat_with_and (map (Sign.string_of_term sign) prems) "" 
    1.43 +                                                  val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*)
    1.44 +                                                  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr))
    1.45 +             (*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*)
    1.46                                                    val _ =  TextIO.closeOut outfile
    1.47 -                                                  val proofextract = extract_proof proofstr
    1.48 -                                                  val tokens = #1(lex proofextract)
    1.49 +
    1.50 +                                                  val tokens = #1(lex proofstr)
    1.51 +
    1.52                                                       
    1.53                                                (***********************************)
    1.54                                                (* parse spass proof into datatype *)
    1.55 @@ -324,7 +332,9 @@
    1.56                                                (************************************)
    1.57                                                  
    1.58                                                    (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
    1.59 -                                                  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thmstring
    1.60 +                                                  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
    1.61 +                                                  (* subgoal this is, and turn it into meta_clauses *)
    1.62 +                                                  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms
    1.63                                                    
    1.64                                                    (*val numcls_string = numclstr ( vars, numcls) ""*)
    1.65                                                    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
    1.66 @@ -357,15 +367,29 @@
    1.67  
    1.68                                                    val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
    1.69                                                    val _ =  TextIO.closeOut outfile
    1.70 +    						  val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
    1.71                                                in 
    1.72 -                                                   (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
    1.73 +                                                   TextIO.output (toParent, reconstr^"\n");
    1.74 +                                                   TextIO.flushOut toParent;
    1.75 +                                        	   TextIO.output (toParent, thmstring^"\n");
    1.76 +                                         	   TextIO.flushOut toParent;
    1.77 +                                         	   TextIO.output (toParent, goalstring^"\n");
    1.78 +                                         	   TextIO.flushOut toParent;
    1.79 +                                          
    1.80 +                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.81 +                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
    1.82 +                                         	   OS.Process.sleep(Time.fromSeconds 1) ; dummy_tac
    1.83                                                end
    1.84                                                handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
    1.85  
    1.86                                                    val _ = TextIO.output (outfile, ("In exception handler"));
    1.87                                                    val _ =  TextIO.closeOut outfile
    1.88                                                in 
    1.89 -                                                 "Proof found but translation failed!"
    1.90 +                                                  TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
    1.91 +                                                  TextIO.flushOut toParent;
    1.92 +            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.93 +                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
    1.94 +                                         	  OS.Process.sleep(Time.fromSeconds 1) ;dummy_tac
    1.95                                                end)
    1.96  
    1.97