yet more tidying up: removal of some references to Main
authorpaulson
Fri Apr 15 18:16:05 2005 +0200 (2005-04-15)
changeset 15739bb2acfed8212
parent 15738 1c1d40ff875a
child 15740 d63e7a65b2d0
yet more tidying up: removal of some references to Main
src/HOL/Tools/ATP/recon_order_clauses.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	Fri Apr 15 17:03:35 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Fri Apr 15 18:16:05 2005 +0200
     1.3 @@ -228,28 +228,27 @@
     1.4  
     1.5  fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
     1.6  
     1.7 -fun lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t
     1.8 +fun lit_string sg t = 
     1.9 +                   let val termstr = Sign.string_of_term sg t
    1.10                         val exp_term = explode termstr
    1.11                     in
    1.12                         implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
    1.13                     end
    1.14  
    1.15 -fun get_meta_lits thm = map lit_string (prems_of thm)
    1.16 -
    1.17 +fun get_meta_lits thm = map (lit_string (sign_of_thm thm)) (prems_of thm)
    1.18  
    1.19  
    1.20 +fun is_alpha_space_or_neg_or_eq_or_bracket ch = is_alpha_space_or_neg_or_eq ch orelse (ch= "(") orelse (ch = ")")
    1.21  
    1.22 -fun is_alpha_space_or_neg_or_eq_or_bracket ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") orelse (ch= "(") orelse (ch = ")")
    1.23 -
    1.24 -fun lit_string_bracket  t = let val termstr = (Sign.string_of_term Mainsign ) t
    1.25 +fun lit_string_bracket sg t = 
    1.26 +                   let val termstr = Sign.string_of_term sg t
    1.27                         val exp_term = explode termstr
    1.28                     in
    1.29                         implode(List.filter  is_alpha_space_or_neg_or_eq_or_bracket exp_term)
    1.30                     end
    1.31  
    1.32 -fun get_meta_lits_bracket thm = map lit_string_bracket (prems_of thm)
    1.33 -
    1.34 -
    1.35 +fun get_meta_lits_bracket thm = 
    1.36 +    map (lit_string_bracket (sign_of_thm thm)) (prems_of thm)
    1.37  
    1.38        
    1.39  fun apply_rule rule [] thm = thm
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Apr 15 17:03:35 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Apr 15 18:16:05 2005 +0200
     2.3 @@ -108,9 +108,6 @@
     2.4  
     2.5  
     2.6  
     2.7 -
     2.8 -
     2.9 -
    2.10  fun is_axiom ( num:int,Axiom, str) = true
    2.11  |   is_axiom (num, _,_) = false
    2.12  
    2.13 @@ -128,8 +125,7 @@
    2.14  |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
    2.15  *)
    2.16  (*FIX - should this have vars in it? *)
    2.17 -fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[])) 
    2.18 -                                   
    2.19 +fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[]))                        
    2.20                                 in 
    2.21                                     true
    2.22                                end
    2.23 @@ -155,9 +151,6 @@
    2.24  fun thmstrings [] str = str
    2.25  |   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
    2.26  
    2.27 -fun onelist [] newlist = newlist
    2.28 -|   onelist (x::xs) newlist = onelist xs (newlist@x)
    2.29 -
    2.30  
    2.31   fun get_axioms_used proof_steps thmstring = let 
    2.32                                               val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    2.33 @@ -175,7 +168,7 @@
    2.34                                             
    2.35                                              val distvars = distinct (fold append vars [])
    2.36                                              val clause_terms = map prop_of clauses  
    2.37 -                                            val clause_frees = onelist (map term_frees clause_terms) []
    2.38 +                                            val clause_frees = List.concat (map term_frees clause_terms)
    2.39  
    2.40                                              val frees = map lit_string_with_nums clause_frees;
    2.41  
    2.42 @@ -313,7 +306,7 @@
    2.43                                                    val _ = TextIO.output (outfile, (thmstring))
    2.44                                                    val _ =  TextIO.closeOut outfile
    2.45                                                    val proofextract = extract_proof proofstr
    2.46 -                                                  val tokens = fst(lex proofextract)
    2.47 +                                                  val tokens = #1(lex proofextract)
    2.48                                                       
    2.49                                                (***********************************)
    2.50                                                (* parse spass proof into datatype *)
    2.51 @@ -352,8 +345,8 @@
    2.52                                                    (* turn the proof into a string *)
    2.53                                                    val reconProofStr = proofs_to_string proof ""
    2.54                                                    (* do the bit for the Isabelle ordered axioms at the top *)
    2.55 -                                                  val ax_nums = map fst numcls
    2.56 -                                                  val ax_strs = map get_meta_lits_bracket (map snd numcls)
    2.57 +                                                  val ax_nums = map #1 numcls
    2.58 +                                                  val ax_strs = map get_meta_lits_bracket (map #2 numcls)
    2.59                                                    val numcls_strs = zip ax_nums ax_strs
    2.60                                                    val num_cls_vars =  map (addvars vars) numcls_strs;
    2.61                                                    val reconIsaAxStr = origAxs_to_string (zip ax_nums ax_with_vars) ""
    2.62 @@ -449,7 +442,7 @@
    2.63  
    2.64  
    2.65   val number_list_step =
    2.66 -        ( number ++ many ((a (Other ",") ++ number)>> snd))
    2.67 +        ( number ++ many ((a (Other ",") ++ number)>> #2))
    2.68          >> (fn (a,b) => (a::b))
    2.69          
    2.70   val numberlist_step = a (Other "[")  ++ a (Other "]")
    2.71 @@ -510,9 +503,9 @@
    2.72      
    2.73   val lines_step = many linestep
    2.74  
    2.75 - val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> fst
    2.76 + val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> #1
    2.77      
    2.78 - val parse_step = fst o alllines_step
    2.79 + val parse_step = #1 o alllines_step
    2.80  
    2.81  
    2.82   (*
    2.83 @@ -702,7 +695,7 @@
    2.84  val thmstring = " (ALL xa::'a::type.   (~ (P::'a::type => bool) (x::'a::type) | P xa) & (~ P xa | P x)) & (((P::'a::type => bool) (xa::'a::type) | (ALL x::'a::type. P x)) &((ALL x::'a::type. ~ P x) | ~ P (xb::'a::type)))";
    2.85  *)
    2.86  
    2.87 -fun apply_res_thm str goalstring  = let val tokens = fst (lex str);
    2.88 +fun apply_res_thm str goalstring  = let val tokens = #1 (lex str);
    2.89  
    2.90                                     val (frees,recon_steps) = parse_step tokens 
    2.91                                     val isar_str = to_isar_proof (frees, recon_steps, goalstring)
     3.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Apr 15 17:03:35 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Apr 15 18:16:05 2005 +0200
     3.3 @@ -141,6 +141,7 @@
     3.4  (* Reconstruct a factoring step      *)
     3.5  (*************************************)
     3.6  
     3.7 +(*FIXME: share code with that in Tools/reconstruction.ML*)
     3.8  fun follow_factor clause lit1 lit2 allvars thml clause_strs= 
     3.9                            let 
    3.10                              val th =  Recon_Base.assoc clause thml
    3.11 @@ -148,7 +149,7 @@
    3.12                              val sign = sign_of_thm th
    3.13                              val fac1 = get_nth (lit1+1) prems
    3.14                              val fac2 = get_nth (lit2+1) prems
    3.15 -                            val unif_env = Unify.unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)])
    3.16 +                            val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)])
    3.17                              val newenv = getnewenv unif_env
    3.18                              val envlist = Envir.alist_of newenv
    3.19