src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 16357 f1275d2a1dee
parent 16259 aed1a8ae4b23
child 16478 d0a1f6231e2f
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Jun 09 23:33:28 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Jun 10 16:15:36 2005 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  
     1.5  structure Recon_Transfer =
     1.6  struct
     1.7 -
     1.8  open Recon_Parse
     1.9  infixr 8 ++; infixr 7 >>; infixr 6 ||;
    1.10  
    1.11 @@ -210,7 +209,10 @@
    1.12      end
    1.13  
    1.14  
    1.15 -(* add array and table here, so can retrieve clasimp axioms *)
    1.16 +
    1.17 +(*****************************************************)
    1.18 +(* get names of clasimp axioms used                  *)
    1.19 +(*****************************************************)
    1.20  
    1.21   fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    1.22     let 
    1.23 @@ -233,6 +235,33 @@
    1.24        clasimp_names
    1.25     end
    1.26      
    1.27 + fun get_axiom_names_vamp proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    1.28 +   let 
    1.29 +     (* not sure why this is necessary again, but seems to be *)
    1.30 +      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.31 +      val axioms = get_init_axioms proof_steps
    1.32 +      val step_nums = get_step_nums axioms []
    1.33 +  
    1.34 +     (***********************************************)
    1.35 +     (* here need to add the clauses from clause_arr*)
    1.36 +     (***********************************************)
    1.37 +  
    1.38 +      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
    1.39 +      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
    1.40 +  
    1.41 +      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    1.42 +                         (concat clasimp_names)
    1.43 +      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    1.44 +   in
    1.45 +      clasimp_names
    1.46 +   end
    1.47 +    
    1.48 +
    1.49 +
    1.50 +
    1.51 +(***********************************************)
    1.52 +(* get axioms for reconstruction               *)
    1.53 +(***********************************************)
    1.54  fun numclstr (vars, []) str = str
    1.55  |   numclstr ( vars, ((num, thm)::rest)) str =
    1.56        let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
    1.57 @@ -343,18 +372,53 @@
    1.58  val dummy_tac = PRIMITIVE(fn thm => thm );
    1.59  
    1.60  
    1.61 -fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    1.62 -           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.63 -                                                  val _ =  TextIO.closeOut outfile
    1.64 +(*val  proofstr = "1242[0:Inp] ||  -> equal(const_List_Orev(tconst_fun(tconst_List_Olist(U),tconst_List_Olist(U)),const_List_Olist_ONil),const_List_Olist_ONil)**.\
    1.65 +\1279[0:Inp] ||  -> equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(U),tconst_nat),const_List_Olist_ONil),const_0)**.\
    1.66 +\1430[0:Inp] || equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Orev(tconst_fun(tconst_List_Olist(typ__Ha),tconst_List_Olist(typ__Ha)),const_List_Olist_ONil)),const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Olist_ONil))** -> .\
    1.67 +\1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\
    1.68 +\1454[0:Obv:1453.0] ||  -> .";*)
    1.69 +
    1.70 +fun remove_linebreaks str = let val strlist = explode str
    1.71 +	                        val nonewlines = filter (not_equal "\n") strlist
    1.72 +	                    in
    1.73 +				implode nonewlines
    1.74 +			    end
    1.75 +
    1.76 +
    1.77 +fun subst_for a b [] = ""
    1.78 +|   subst_for a b (x::xs) = if (x = a)
    1.79 +				   then 
    1.80 +					(b^(subst_for a b  xs))
    1.81 +				   else
    1.82 +					x^(subst_for a b xs)
    1.83 +
    1.84  
    1.85 -                                              (***********************************)
    1.86 -                                              (* parse spass proof into datatype *)
    1.87 -                                              (***********************************)
    1.88 +fun remove_linebreaks str = let val strlist = explode str
    1.89 +			    in
    1.90 +				subst_for "\n" "\t" strlist
    1.91 +			    end
    1.92 +
    1.93 +fun restore_linebreaks str = let val strlist = explode str
    1.94 +			     in
    1.95 +				subst_for "\t" "\n" strlist
    1.96 +			     end
    1.97 +
    1.98 +
    1.99 +
   1.100 +fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.101 +           let 	val  outfile = TextIO.openAppend( File.platform_path(File.tmp_path (Path.basic"thmstringfile")));          
   1.102 +		val _ = TextIO.output (outfile, ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n  num of clauses is: "^(string_of_int num_of_clauses)))
   1.103 +
   1.104 +              	val _ =  TextIO.closeOut outfile
   1.105 +
   1.106 +                 (***********************************)
   1.107 +                 (* parse spass proof into datatype *)
   1.108 +                 (***********************************)
   1.109           
   1.110 -                                                  val tokens = #1(lex proofstr)
   1.111 -                                                  val proof_steps1 = parse tokens
   1.112 -                                                  val proof_steps = just_change_space proof_steps1
   1.113 -                                                  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));                                                     val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   1.114 +                  val tokens = #1(lex proofstr)
   1.115 +                  val proof_steps1 = parse tokens
   1.116 +                  val proof_steps = just_change_space proof_steps1
   1.117 +                  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));        val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   1.118                                                    val _ =  TextIO.closeOut outfile
   1.119                                                  
   1.120                                                    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                        val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   1.121 @@ -391,7 +455,7 @@
   1.122                                                    val _ = TextIO.output (outfile, ("In exception handler"));
   1.123                                                    val _ =  TextIO.closeOut outfile
   1.124                                                in 
   1.125 -                                                  TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
   1.126 +                                                 TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr) ^"\n");
   1.127                                                    TextIO.flushOut toParent;
   1.128  						   TextIO.output (toParent, thmstring^"\n");
   1.129                                           	   TextIO.flushOut toParent;
   1.130 @@ -403,6 +467,71 @@
   1.131                                                end)
   1.132  
   1.133  
   1.134 +(*fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.135 +           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.136 +                                                  val _ =  TextIO.closeOut outfile
   1.137 +
   1.138 +                                              (***********************************)
   1.139 +                                              (* parse spass proof into datatype *)
   1.140 +                                              (***********************************)
   1.141 +         
   1.142 +                                                  val tokens = #1(lex proofstr)
   1.143 +                                                  val proof_steps = VampParse.parse tokens
   1.144 +                                                  (*val proof_steps = just_change_space proof_steps1*)
   1.145 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                     val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   1.146 +                                                  val _ =  TextIO.closeOut outfile
   1.147 +                                                
   1.148 +                                                  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.149 +                                                  val _ =  TextIO.closeOut outfile
   1.150 +                                              (************************************)
   1.151 +                                              (* recreate original subgoal as thm *)
   1.152 +                                              (************************************)
   1.153 +                                                
   1.154 +                                                  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   1.155 +                                                  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   1.156 +                                                  (* subgoal this is, and turn it into meta_clauses *)
   1.157 +                                                  (* should prob add array and table here, so that we can get axioms*)
   1.158 +                                                  (* produced from the clasimpset rather than the problem *)
   1.159 +
   1.160 +                                                  val (axiom_names) = get_axiom_names_vamp proof_steps  thms clause_arr  num_of_clauses
   1.161 +                                                  val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
   1.162 +                                                  val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "reconstrfile")));                                                     val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   1.163 +                                                  val _ =  TextIO.closeOut outfile
   1.164 +                                                   
   1.165 +                                              in 
   1.166 +                                                   TextIO.output (toParent, ax_str^"\n");
   1.167 +                                                   TextIO.flushOut toParent;
   1.168 +                                        	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.169 +                                         	   TextIO.flushOut toParent;fdsa
   1.170 +                                         	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.171 +                                         	   TextIO.flushOut toParent;
   1.172 +                                          
   1.173 +                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.174 +                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.175 +                                         	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.176 +                                              end
   1.177 +                                              handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   1.178 +
   1.179 +                                                  val _ = TextIO.output (outfile, ("In exception handler"));
   1.180 +                                                  val _ =  TextIO.closeOut outfile
   1.181 +                                              in 
   1.182 +                                                  TextIO.output (toParent,"Proof found but translation failed for resolution proof: \n"^(remove_linebreaks proofstr) ^"\n");
   1.183 +                                                  TextIO.flushOut toParent;
   1.184 +						   TextIO.output (toParent, thmstring^"\n");
   1.185 +                                         	   TextIO.flushOut toParent;
   1.186 +                                         	   TextIO.output (toParent, goalstring^"\n");
   1.187 +                                         	   TextIO.flushOut toParent;
   1.188 +            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.189 +                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.190 +                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.191 +                                              end)
   1.192 +*)
   1.193 +
   1.194 +
   1.195 +
   1.196 +(* val proofstr = "1582[0:Inp] || -> v_P*.\
   1.197 +                 \1583[0:Inp] || v_P* -> .\
   1.198 +		 \1584[0:MRR:1583.0,1582.0] || -> ."; *)
   1.199  
   1.200  fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.201        let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   1.202 @@ -490,7 +619,7 @@
   1.203  	  val _ = TextIO.output (outfile, ("In exception handler"));
   1.204  	  val _ =  TextIO.closeOut outfile
   1.205        in 
   1.206 -	  TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
   1.207 +	   TextIO.output (toParent,"Proof found but translation failed for resolution proof: \n"^proofstr ^"\n");
   1.208  	  TextIO.flushOut toParent;
   1.209  	TextIO.output (toParent, thmstring^"\n");
   1.210  	   TextIO.flushOut toParent;
   1.211 @@ -742,12 +871,16 @@
   1.212  
   1.213  
   1.214  fun have_isar_line (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
   1.215 -
   1.216 +(*FIX: ask Larry to add and mrr attribute *)
   1.217  
   1.218  fun by_isar_line ((Binary ((a,b), (c,d)))) = 
   1.219      "by(rule cl"^
   1.220  		(string_of_int a)^" [binary "^(string_of_int b)^" cl"^
   1.221  		(string_of_int c)^" "^(string_of_int d)^"])\n"
   1.222 +|by_isar_line ((MRR ((a,b), (c,d)))) = 
   1.223 +    "by(rule cl"^
   1.224 +		(string_of_int a)^" [binary "^(string_of_int b)^" cl"^
   1.225 +		(string_of_int c)^" "^(string_of_int d)^"])\n"
   1.226  |   by_isar_line ( (Para ((a,b), (c,d)))) =
   1.227      "by (rule cl"^
   1.228  		(string_of_int a)^" [paramod "^(string_of_int b)^" cl"^
   1.229 @@ -826,7 +959,8 @@
   1.230  *)
   1.231  
   1.232  fun apply_res_thm str goalstring  = let val tokens = #1 (lex str);
   1.233 -
   1.234 +				val _ = File.append (File.tmp_path (Path.basic "applyres")) 
   1.235 +			           ("str is: "^str^" goalstr is: "^goalstring^"\n")	
   1.236                                     val (frees,recon_steps) = parse_step tokens 
   1.237                                     val isar_str = to_isar_proof (frees, recon_steps, goalstring)
   1.238                                     val foo =   TextIO.openOut (File.platform_path(File.tmp_path (Path.basic "foobar")));
   1.239 @@ -835,6 +969,6 @@
   1.240                                 end 
   1.241  
   1.242  
   1.243 -
   1.244 -
   1.245 +(* val reconstr = reconstr^"[P%]51Axiom()[~P%]52Axiom[P%][]53MRR((52,0),(51,0))[][]";
   1.246 +*)
   1.247  end;