src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 15919 b30a35432f5a
parent 15817 f79b673da664
child 16039 dfe264950511
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 03 10:33:31 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 03 14:27:21 2005 +0200
     1.3 @@ -17,6 +17,39 @@
     1.4  
     1.5  
     1.6  
     1.7 +(*
     1.8 +fun fill_cls_array array n [] = ()
     1.9 +|   fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x)
    1.10 +                                     in
    1.11 +                                        fill_cls_array array (n+1) (xs)
    1.12 +                                     end;
    1.13 +
    1.14 +
    1.15 +
    1.16 +fun memo_add_clauses ((name:string, (cls:Thm.thm list)), symtable)=
    1.17 +                        symtable := Symtab.update((name , cls), !symtable);
    1.18 +      	       
    1.19 +
    1.20 +fun memo_add_all ([], symtable) = ()
    1.21 +|   memo_add_all ((x::xs),symtable) = let val _ = memo_add_clauses (x, symtable)
    1.22 +                           in
    1.23 +                               memo_add_all (xs, symtable)
    1.24 +                           end
    1.25 +
    1.26 +fun memo_find_clause (name, (symtable: Thm.thm list Symtab.table ref)) = case Symtab.lookup (!symtable,name) of
    1.27 +      	        NONE =>  []
    1.28 +                |SOME cls  => cls ;
    1.29 +      	        	
    1.30 +
    1.31 +fun retrieve_clause array symtable clausenum = let
    1.32 +                                                  val (name, clnum) = Array.sub(array, clausenum)
    1.33 +                                                  val clauses = memo_find_clause (name, symtable)
    1.34 +                                                  val clause = get_nth clnum clauses
    1.35 +                                               in
    1.36 +                                                  (name, clause)
    1.37 +                                               end
    1.38 + *)                                             
    1.39 +
    1.40  (* Versions that include type information *)
    1.41   
    1.42  fun string_of_thm thm = let val _ = set show_sorts
    1.43 @@ -146,8 +179,30 @@
    1.44  fun thmstrings [] str = str
    1.45  |   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
    1.46  
    1.47 +fun is_clasimp_ax clasimp_num n = n <=clasimp_num 
    1.48  
    1.49 - fun get_axioms_used proof_steps thms = let 
    1.50 +
    1.51 +
    1.52 +fun retrieve_axioms clause_arr  [] = []
    1.53 +|   retrieve_axioms clause_arr  (x::xs) =  [Array.sub(clause_arr, x)]@
    1.54 + 						     (retrieve_axioms clause_arr  xs)
    1.55 +
    1.56 +
    1.57 +(* retrieve the axioms that were obtained from the clasimpset *)
    1.58 +
    1.59 +fun get_clasimp_cls clause_arr clasimp_num step_nums = 
    1.60 +                                let val clasimp_nums = List.filter (is_clasimp_ax clasimp_num) step_nums
    1.61 +                                in
    1.62 +                                    retrieve_axioms clause_arr  clasimp_nums
    1.63 +                                end
    1.64 +
    1.65 +
    1.66 +
    1.67 +
    1.68 +(* add array and table here, so can retrieve clasimp axioms *)
    1.69 +
    1.70 + fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    1.71 +                                         let 
    1.72                                               (*val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    1.73                                               val _ = TextIO.output (outfile, thmstring)
    1.74                                               
    1.75 @@ -157,9 +212,21 @@
    1.76                                              val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.77                                              val axioms = get_init_axioms proof_steps
    1.78                                              val step_nums = get_step_nums axioms []
    1.79 -                                      
    1.80 -                                           
    1.81 -                                            val clauses = make_clauses thms
    1.82 +
    1.83 +                                           (***********************************************)
    1.84 +                                           (* here need to add the clauses from clause_arr*)
    1.85 +                                           (***********************************************)
    1.86 +
    1.87 +                                           (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
    1.88 +                                            val clasimp_names = map #1 clasimp_names_cls
    1.89 +                                            val clasimp_cls = map #2 clasimp_names_cls
    1.90 +                                            val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
    1.91 +                                             val _ = TextIO.output (outfile,clasimp_namestr)
    1.92 +                                             
    1.93 +                                             val _ =  TextIO.closeOut outfile
    1.94 +*)
    1.95 +
    1.96 +                                            val clauses =(*(clasimp_cls)@*)( make_clauses thms)
    1.97                                              
    1.98                                              val vars = map thm_vars clauses
    1.99                                             
   1.100 @@ -215,7 +282,7 @@
   1.101                                             val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
   1.102                                             
   1.103                                           in
   1.104 -                                            (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
   1.105 +                                            (distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
   1.106                                           end
   1.107                                          
   1.108  fun numclstr (vars, []) str = str
   1.109 @@ -293,9 +360,12 @@
   1.110  
   1.111  *)
   1.112  
   1.113 +
   1.114 +
   1.115 +
   1.116  val dummy_tac = PRIMITIVE(fn thm => thm );
   1.117  
   1.118 -fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms= 
   1.119 +fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.120                                                let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   1.121                                                    (* val sign = sign_of_thm thm
   1.122                                                   val prems = prems_of thm
   1.123 @@ -307,7 +377,8 @@
   1.124  
   1.125                                                    val tokens = #1(lex proofstr)
   1.126  
   1.127 -                                                     
   1.128 +                                                    
   1.129 +
   1.130                                                (***********************************)
   1.131                                                (* parse spass proof into datatype *)
   1.132                                                (***********************************)
   1.133 @@ -327,7 +398,9 @@
   1.134                                                    (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   1.135                                                    (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   1.136                                                    (* subgoal this is, and turn it into meta_clauses *)
   1.137 -                                                  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms
   1.138 +                                                  (* should prob add array and table here, so that we can get axioms*)
   1.139 +                                                  (* produced from the clasimpset rather than the problem *)
   1.140 +                                                  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   1.141                                                    
   1.142                                                    (*val numcls_string = numclstr ( vars, numcls) ""*)
   1.143                                                    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")