minor tidying and sml/nj compatibility
authorpaulson
Tue May 31 17:52:10 2005 +0200 (2005-05-31)
changeset 161571764cc98bafd
parent 16156 2f6fc19aba1e
child 16158 2c3565b74b7a
minor tidying and sml/nj compatibility
src/HOL/Tools/ATP/recon_order_clauses.ML
src/HOL/Tools/ATP/recon_prelim.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue May 31 12:42:36 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue May 31 17:52:10 2005 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4                                  else
     1.5                                       takeUntil ch xs (res@[x]);
     1.6  
     1.7 -fun contains_eq str = inlist "=" str 
     1.8 +fun contains_eq str = "=" mem str 
     1.9  
    1.10  fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str [])
    1.11                       in (last uptoeq) <> "~" end
     2.1 --- a/src/HOL/Tools/ATP/recon_prelim.ML	Tue May 31 12:42:36 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_prelim.ML	Tue May 31 17:52:10 2005 +0200
     2.3 @@ -131,31 +131,6 @@
     2.4                       Free (istr,tv)
     2.5                   end;
     2.6  
     2.7 -fun  inlist v [] = false
     2.8 -    | inlist v (first::rest) = if first = v then
     2.9 -				true
    2.10 -			     else inlist v rest;
    2.11 -
    2.12 -(*fun in_vars v [] = false
    2.13 -    | in_vars v ((a,b)::rest) = if v = a then
    2.14 -				  true
    2.15 -			       else if v = b then
    2.16 -				  true
    2.17 -			       else in_vars v rest;*)
    2.18 -
    2.19 -fun in_vars v [] = false
    2.20 -    | in_vars v (a::rest) = if (fst v) = a then
    2.21 -				  true
    2.22 -			      
    2.23 -			       else in_vars v rest;
    2.24 -
    2.25 -fun equalpair (a,b) (c,d) = if (a,b)= (c,d) then
    2.26 -					true
    2.27 -			    else if (a,b) = (d,c) then
    2.28 -					true
    2.29 -			    else false;
    2.30 -
    2.31 -
    2.32  fun is_empty_seq thisseq =  case Seq.chop (1, thisseq) of
    2.33                               ([],_)   => true
    2.34                             |      _   => false
     3.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 31 12:42:36 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 31 17:52:10 2005 +0200
     3.3 @@ -53,13 +53,14 @@
     3.4  
     3.5  (* Versions that include type information *)
     3.6   
     3.7 -fun string_of_thm thm = let val _ = set show_sorts
     3.8 -                                val str = Display.string_of_thm thm
     3.9 -                                val no_returns =List.filter not_newline (explode str)
    3.10 -                                val _ = reset show_sorts
    3.11 -                            in 
    3.12 -                                implode no_returns
    3.13 -                            end
    3.14 +fun string_of_thm thm =
    3.15 +  let val _ = set show_sorts
    3.16 +      val str = Display.string_of_thm thm
    3.17 +      val no_returns =List.filter not_newline (explode str)
    3.18 +      val _ = reset show_sorts
    3.19 +  in 
    3.20 +      implode no_returns
    3.21 +  end
    3.22  
    3.23  
    3.24  (* check separate args in the watcher program for separating strings with a * or ; or something *)
    3.25 @@ -67,8 +68,6 @@
    3.26  fun clause_strs_to_string [] str = str
    3.27  |   clause_strs_to_string (x::xs) str = clause_strs_to_string xs (str^x^"%")
    3.28  
    3.29 -
    3.30 -
    3.31  fun thmvars_to_string [] str = str
    3.32  |   thmvars_to_string (x::xs) str = thmvars_to_string xs (str^x^"%")
    3.33  
    3.34 @@ -174,11 +173,8 @@
    3.35  fun get_assoc_snds [] xs assocs= assocs
    3.36  |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))])
    3.37  
    3.38 -
    3.39 -
    3.40 -
    3.41  fun add_if_not_inlist [] xs newlist = newlist
    3.42 -|   add_if_not_inlist (y::ys) xs newlist = if (not (inlist y xs)) then 
    3.43 +|   add_if_not_inlist (y::ys) xs newlist = if (not (y mem xs)) then 
    3.44                                        add_if_not_inlist ys xs (y::newlist)
    3.45                                          else add_if_not_inlist ys xs (newlist)
    3.46  
    3.47 @@ -205,57 +201,47 @@
    3.48  (* retrieve the axioms that were obtained from the clasimpset *)
    3.49  
    3.50  fun get_clasimp_cls clause_arr clasimp_num step_nums = 
    3.51 -                                let 
    3.52 -                                    val realnums = map subone step_nums
    3.53 -                                   
    3.54 - 				    
    3.55 -                                    val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
    3.56 -                                   val axnums = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "axnums")))     
    3.57 -                                   val _ = TextIO.output(axnums,(numstr clasimp_nums))
    3.58 -                                   val _ = TextIO.closeOut(axnums)
    3.59 -                                in
    3.60 -                                    retrieve_axioms clause_arr  clasimp_nums
    3.61 -                                end
    3.62 +    let val realnums = map subone step_nums	
    3.63 +	val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
    3.64 +	val axnums = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "axnums")))     
    3.65 +	val _ = TextIO.output(axnums,(numstr clasimp_nums))
    3.66 +	val _ = TextIO.closeOut(axnums)
    3.67 +    in
    3.68 +	retrieve_axioms clause_arr  clasimp_nums
    3.69 +    end
    3.70  
    3.71 -fun get_cls []  = []
    3.72 -|   get_cls (x::xs) = ((#1 x)::(get_cls xs))
    3.73  
    3.74  (* add array and table here, so can retrieve clasimp axioms *)
    3.75  
    3.76 - fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * Thm.thm) Array.array) num_of_clauses  =
    3.77 -                                         let 
    3.78 -                                           (* not sure why this is necessary again, but seems to be *)
    3.79 -					    val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    3.80 -                                            val axioms = get_init_axioms proof_steps
    3.81 -                                            val step_nums = get_step_nums axioms []
    3.82 -
    3.83 -                                           (***********************************************)
    3.84 -                                           (* here need to add the clauses from clause_arr*)
    3.85 -                                           (***********************************************)
    3.86 -
    3.87 -                                            val (clasimp_names_cls) = get_clasimp_cls clause_arr   num_of_clauses step_nums 
    3.88 -                                            val clauses=(get_cls clasimp_names_cls) 
    3.89 -                                            val (names_clsnums) = map ResClause.clause_info clauses
    3.90 -                                            val clasimp_names = map fst names_clsnums
    3.91 -
    3.92 -                                            val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "clasimp_names")))                                                                   val clasimp_namestr = concat clasimp_names                            
    3.93 -                                            val _ = TextIO.output (outfile,clasimp_namestr)
    3.94 -                                            val _ =  TextIO.closeOut outfile
    3.95 -					    val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    3.96 -                                           
    3.97 -                                         in
    3.98 -                                            (clasimp_names)
    3.99 -                                         end
   3.100 + fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
   3.101 +   let 
   3.102 +     (* not sure why this is necessary again, but seems to be *)
   3.103 +      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   3.104 +      val axioms = get_init_axioms proof_steps
   3.105 +      val step_nums = get_step_nums axioms []
   3.106 +  
   3.107 +     (***********************************************)
   3.108 +     (* here need to add the clauses from clause_arr*)
   3.109 +     (***********************************************)
   3.110 +  
   3.111 +      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
   3.112 +      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
   3.113 +  
   3.114 +      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
   3.115 +                         (concat clasimp_names)
   3.116 +      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
   3.117 +   in
   3.118 +      clasimp_names
   3.119 +   end
   3.120      
   3.121  fun numclstr (vars, []) str = str
   3.122 -|   numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
   3.123 -in
   3.124 -numclstr  (vars,rest) newstr
   3.125 -end
   3.126 +|   numclstr ( vars, ((num, thm)::rest)) str =
   3.127 +      let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
   3.128 +      in
   3.129 +        numclstr  (vars,rest) newstr
   3.130 +      end
   3.131  
   3.132 -
   3.133 -fun addvars  c (a,b)  = (a,b,c)
   3.134 -
   3.135 +fun addvars c (a,b)  = (a,b,c)
   3.136  
   3.137   fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
   3.138       let 
     4.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue May 31 12:42:36 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue May 31 17:52:10 2005 +0200
     4.3 @@ -10,10 +10,8 @@
     4.4                               else
     4.5                                    (y::(add_in_order x ys))
     4.6  fun add_once x [] = [x]
     4.7 -|   add_once x (y::ys) = if (inlist x (y::ys)) then 
     4.8 -                            (y::ys)
     4.9 -                        else
    4.10 -                            add_in_order x (y::ys)
    4.11 +|   add_once x (y::ys) = if x mem (y::ys) then (y::ys)
    4.12 +                         else add_in_order x (y::ys)
    4.13       
    4.14  fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);
    4.15