src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 16157 1764cc98bafd
parent 16156 2f6fc19aba1e
child 16259 aed1a8ae4b23
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 31 12:42:36 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 31 17:52:10 2005 +0200
     1.3 @@ -53,13 +53,14 @@
     1.4  
     1.5  (* Versions that include type information *)
     1.6   
     1.7 -fun string_of_thm thm = let val _ = set show_sorts
     1.8 -                                val str = Display.string_of_thm thm
     1.9 -                                val no_returns =List.filter not_newline (explode str)
    1.10 -                                val _ = reset show_sorts
    1.11 -                            in 
    1.12 -                                implode no_returns
    1.13 -                            end
    1.14 +fun string_of_thm thm =
    1.15 +  let val _ = set show_sorts
    1.16 +      val str = Display.string_of_thm thm
    1.17 +      val no_returns =List.filter not_newline (explode str)
    1.18 +      val _ = reset show_sorts
    1.19 +  in 
    1.20 +      implode no_returns
    1.21 +  end
    1.22  
    1.23  
    1.24  (* check separate args in the watcher program for separating strings with a * or ; or something *)
    1.25 @@ -67,8 +68,6 @@
    1.26  fun clause_strs_to_string [] str = str
    1.27  |   clause_strs_to_string (x::xs) str = clause_strs_to_string xs (str^x^"%")
    1.28  
    1.29 -
    1.30 -
    1.31  fun thmvars_to_string [] str = str
    1.32  |   thmvars_to_string (x::xs) str = thmvars_to_string xs (str^x^"%")
    1.33  
    1.34 @@ -174,11 +173,8 @@
    1.35  fun get_assoc_snds [] xs assocs= assocs
    1.36  |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))])
    1.37  
    1.38 -
    1.39 -
    1.40 -
    1.41  fun add_if_not_inlist [] xs newlist = newlist
    1.42 -|   add_if_not_inlist (y::ys) xs newlist = if (not (inlist y xs)) then 
    1.43 +|   add_if_not_inlist (y::ys) xs newlist = if (not (y mem xs)) then 
    1.44                                        add_if_not_inlist ys xs (y::newlist)
    1.45                                          else add_if_not_inlist ys xs (newlist)
    1.46  
    1.47 @@ -205,57 +201,47 @@
    1.48  (* retrieve the axioms that were obtained from the clasimpset *)
    1.49  
    1.50  fun get_clasimp_cls clause_arr clasimp_num step_nums = 
    1.51 -                                let 
    1.52 -                                    val realnums = map subone step_nums
    1.53 -                                   
    1.54 - 				    
    1.55 -                                    val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
    1.56 -                                   val axnums = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "axnums")))     
    1.57 -                                   val _ = TextIO.output(axnums,(numstr clasimp_nums))
    1.58 -                                   val _ = TextIO.closeOut(axnums)
    1.59 -                                in
    1.60 -                                    retrieve_axioms clause_arr  clasimp_nums
    1.61 -                                end
    1.62 +    let val realnums = map subone step_nums	
    1.63 +	val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
    1.64 +	val axnums = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "axnums")))     
    1.65 +	val _ = TextIO.output(axnums,(numstr clasimp_nums))
    1.66 +	val _ = TextIO.closeOut(axnums)
    1.67 +    in
    1.68 +	retrieve_axioms clause_arr  clasimp_nums
    1.69 +    end
    1.70  
    1.71 -fun get_cls []  = []
    1.72 -|   get_cls (x::xs) = ((#1 x)::(get_cls xs))
    1.73  
    1.74  (* add array and table here, so can retrieve clasimp axioms *)
    1.75  
    1.76 - fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * Thm.thm) Array.array) num_of_clauses  =
    1.77 -                                         let 
    1.78 -                                           (* not sure why this is necessary again, but seems to be *)
    1.79 -					    val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.80 -                                            val axioms = get_init_axioms proof_steps
    1.81 -                                            val step_nums = get_step_nums axioms []
    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 clauses=(get_cls clasimp_names_cls) 
    1.89 -                                            val (names_clsnums) = map ResClause.clause_info clauses
    1.90 -                                            val clasimp_names = map fst names_clsnums
    1.91 -
    1.92 -                                            val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "clasimp_names")))                                                                   val clasimp_namestr = concat clasimp_names                            
    1.93 -                                            val _ = TextIO.output (outfile,clasimp_namestr)
    1.94 -                                            val _ =  TextIO.closeOut outfile
    1.95 -					    val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    1.96 -                                           
    1.97 -                                         in
    1.98 -                                            (clasimp_names)
    1.99 -                                         end
   1.100 + fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
   1.101 +   let 
   1.102 +     (* not sure why this is necessary again, but seems to be *)
   1.103 +      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   1.104 +      val axioms = get_init_axioms proof_steps
   1.105 +      val step_nums = get_step_nums axioms []
   1.106 +  
   1.107 +     (***********************************************)
   1.108 +     (* here need to add the clauses from clause_arr*)
   1.109 +     (***********************************************)
   1.110 +  
   1.111 +      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
   1.112 +      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
   1.113 +  
   1.114 +      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
   1.115 +                         (concat clasimp_names)
   1.116 +      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
   1.117 +   in
   1.118 +      clasimp_names
   1.119 +   end
   1.120      
   1.121  fun numclstr (vars, []) str = str
   1.122 -|   numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
   1.123 -in
   1.124 -numclstr  (vars,rest) newstr
   1.125 -end
   1.126 +|   numclstr ( vars, ((num, thm)::rest)) str =
   1.127 +      let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
   1.128 +      in
   1.129 +        numclstr  (vars,rest) newstr
   1.130 +      end
   1.131  
   1.132 -
   1.133 -fun addvars  c (a,b)  = (a,b,c)
   1.134 -
   1.135 +fun addvars c (a,b)  = (a,b,c)
   1.136  
   1.137   fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
   1.138       let