src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 16478 d0a1f6231e2f
parent 16357 f1275d2a1dee
child 16520 7a9cda53bfa2
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Jun 20 16:41:47 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Jun 20 18:39:24 2005 +0200
     1.3 @@ -201,9 +201,9 @@
     1.4  fun get_clasimp_cls clause_arr clasimp_num step_nums = 
     1.5      let val realnums = map subone step_nums	
     1.6  	val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
     1.7 -	val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))     
     1.8 +(*	val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))     
     1.9  	val _ = TextIO.output(axnums,(numstr clasimp_nums))
    1.10 -	val _ = TextIO.closeOut(axnums)
    1.11 +	val _ = TextIO.closeOut(axnums)*)
    1.12      in
    1.13  	retrieve_axioms clause_arr  clasimp_nums
    1.14      end
    1.15 @@ -235,12 +235,11 @@
    1.16        clasimp_names
    1.17     end
    1.18      
    1.19 - fun get_axiom_names_vamp proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    1.20 + fun get_axiom_names_vamp proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    1.21     let 
    1.22       (* not sure why this is necessary again, but seems to be *)
    1.23        val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.24 -      val axioms = get_init_axioms proof_steps
    1.25 -      val step_nums = get_step_nums axioms []
    1.26 +      val step_nums =get_linenums proofstr
    1.27    
    1.28       (***********************************************)
    1.29       (* here need to add the clauses from clause_arr*)
    1.30 @@ -455,7 +454,49 @@
    1.31                                                    val _ = TextIO.output (outfile, ("In exception handler"));
    1.32                                                    val _ =  TextIO.closeOut outfile
    1.33                                                in 
    1.34 -                                                 TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr) ^"\n");
    1.35 +                                                 TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" );
    1.36 +                                                  TextIO.flushOut toParent;
    1.37 +						   TextIO.output (toParent, (remove_linebreaks thmstring)^"\n");
    1.38 +                                         	   TextIO.flushOut toParent;
    1.39 +                                         	   TextIO.output (toParent, ( (remove_linebreaks goalstring)^"\n"));
    1.40 +                                         	   TextIO.flushOut toParent;
    1.41 +            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.42 +                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
    1.43 +                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
    1.44 +                                              end)
    1.45 +
    1.46 +
    1.47 +fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    1.48 +           let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));     						       val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses)))
    1.49 +                                               val _ =  TextIO.closeOut outfile
    1.50 +
    1.51 +                                              (***********************************)
    1.52 +                                              (* get vampire axiom names         *)
    1.53 +                                              (***********************************)
    1.54 +         
    1.55 +                                               val (axiom_names) = get_axiom_names_vamp proofstr  thms clause_arr  num_of_clauses
    1.56 +                                               val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
    1.57 +                                               val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile")));                                                    val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
    1.58 +                                               val _ =  TextIO.closeOut outfile
    1.59 +                                                   
    1.60 +                                              in 
    1.61 +                                                   TextIO.output (toParent, ax_str^"\n");
    1.62 +                                                   TextIO.flushOut toParent;
    1.63 +                                        	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
    1.64 +                                         	   TextIO.flushOut toParent;
    1.65 +                                         	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
    1.66 +                                         	   TextIO.flushOut toParent;
    1.67 +                                          
    1.68 +                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.69 +                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
    1.70 +                                         	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
    1.71 +                                              end
    1.72 +                                              handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
    1.73 +
    1.74 +                                                  val _ = TextIO.output (outfile, ("In exception handler"));
    1.75 +                                                  val _ =  TextIO.closeOut outfile
    1.76 +                                              in 
    1.77 +                                                  TextIO.output (toParent,"Proof found but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
    1.78                                                    TextIO.flushOut toParent;
    1.79  						   TextIO.output (toParent, thmstring^"\n");
    1.80                                           	   TextIO.flushOut toParent;
    1.81 @@ -467,66 +508,6 @@
    1.82                                                end)
    1.83  
    1.84  
    1.85 -(*fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    1.86 -           let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));     						  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses)))
    1.87 -                                                  val _ =  TextIO.closeOut outfile
    1.88 -
    1.89 -                                              (***********************************)
    1.90 -                                              (* parse spass proof into datatype *)
    1.91 -                                              (***********************************)
    1.92 -         
    1.93 -                                                  val tokens = #1(lex proofstr)
    1.94 -                                                  val proof_steps = VampParse.parse tokens
    1.95 -                                                  (*val proof_steps = just_change_space proof_steps1*)
    1.96 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                     val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
    1.97 -                                                  val _ =  TextIO.closeOut outfile
    1.98 -                                                
    1.99 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                        val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   1.100 -                                                  val _ =  TextIO.closeOut outfile
   1.101 -                                              (************************************)
   1.102 -                                              (* recreate original subgoal as thm *)
   1.103 -                                              (************************************)
   1.104 -                                                
   1.105 -                                                  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   1.106 -                                                  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   1.107 -                                                  (* subgoal this is, and turn it into meta_clauses *)
   1.108 -                                                  (* should prob add array and table here, so that we can get axioms*)
   1.109 -                                                  (* produced from the clasimpset rather than the problem *)
   1.110 -
   1.111 -                                                  val (axiom_names) = get_axiom_names_vamp proof_steps  thms clause_arr  num_of_clauses
   1.112 -                                                  val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
   1.113 -                                                  val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "reconstrfile")));                                                     val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   1.114 -                                                  val _ =  TextIO.closeOut outfile
   1.115 -                                                   
   1.116 -                                              in 
   1.117 -                                                   TextIO.output (toParent, ax_str^"\n");
   1.118 -                                                   TextIO.flushOut toParent;
   1.119 -                                        	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.120 -                                         	   TextIO.flushOut toParent;fdsa
   1.121 -                                         	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.122 -                                         	   TextIO.flushOut toParent;
   1.123 -                                          
   1.124 -                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.125 -                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.126 -                                         	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.127 -                                              end
   1.128 -                                              handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   1.129 -
   1.130 -                                                  val _ = TextIO.output (outfile, ("In exception handler"));
   1.131 -                                                  val _ =  TextIO.closeOut outfile
   1.132 -                                              in 
   1.133 -                                                  TextIO.output (toParent,"Proof found but translation failed for resolution proof: \n"^(remove_linebreaks proofstr) ^"\n");
   1.134 -                                                  TextIO.flushOut toParent;
   1.135 -						   TextIO.output (toParent, thmstring^"\n");
   1.136 -                                         	   TextIO.flushOut toParent;
   1.137 -                                         	   TextIO.output (toParent, goalstring^"\n");
   1.138 -                                         	   TextIO.flushOut toParent;
   1.139 -            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.140 -                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.141 -                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.142 -                                              end)
   1.143 -*)
   1.144 -
   1.145  
   1.146  
   1.147  (* val proofstr = "1582[0:Inp] || -> v_P*.\
   1.148 @@ -619,7 +600,7 @@
   1.149  	  val _ = TextIO.output (outfile, ("In exception handler"));
   1.150  	  val _ =  TextIO.closeOut outfile
   1.151        in 
   1.152 -	   TextIO.output (toParent,"Proof found but translation failed for resolution proof: \n"^proofstr ^"\n");
   1.153 +	   TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^(remove_linebreaks proofstr) ^"\n");
   1.154  	  TextIO.flushOut toParent;
   1.155  	TextIO.output (toParent, thmstring^"\n");
   1.156  	   TextIO.flushOut toParent;