# HG changeset patch # User paulson # Date 1113581765 -7200 # Node ID bb2acfed8212bcf9f2c581eb62bc47e41b06c572 # Parent 1c1d40ff875a3d7abb65cb04c79aa70b69d62690 yet more tidying up: removal of some references to Main diff -r 1c1d40ff875a -r bb2acfed8212 src/HOL/Tools/ATP/recon_order_clauses.ML --- a/src/HOL/Tools/ATP/recon_order_clauses.ML Fri Apr 15 17:03:35 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Fri Apr 15 18:16:05 2005 +0200 @@ -228,28 +228,27 @@ fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") -fun lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t +fun lit_string sg t = + let val termstr = Sign.string_of_term sg t val exp_term = explode termstr in implode(List.filter is_alpha_space_or_neg_or_eq exp_term) end -fun get_meta_lits thm = map lit_string (prems_of thm) - +fun get_meta_lits thm = map (lit_string (sign_of_thm thm)) (prems_of thm) +fun is_alpha_space_or_neg_or_eq_or_bracket ch = is_alpha_space_or_neg_or_eq ch orelse (ch= "(") orelse (ch = ")") -fun is_alpha_space_or_neg_or_eq_or_bracket ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") orelse (ch= "(") orelse (ch = ")") - -fun lit_string_bracket t = let val termstr = (Sign.string_of_term Mainsign ) t +fun lit_string_bracket sg t = + let val termstr = Sign.string_of_term sg t val exp_term = explode termstr in implode(List.filter is_alpha_space_or_neg_or_eq_or_bracket exp_term) end -fun get_meta_lits_bracket thm = map lit_string_bracket (prems_of thm) - - +fun get_meta_lits_bracket thm = + map (lit_string_bracket (sign_of_thm thm)) (prems_of thm) fun apply_rule rule [] thm = thm diff -r 1c1d40ff875a -r bb2acfed8212 src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Apr 15 17:03:35 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Apr 15 18:16:05 2005 +0200 @@ -108,9 +108,6 @@ - - - fun is_axiom ( num:int,Axiom, str) = true | is_axiom (num, _,_) = false @@ -128,8 +125,7 @@ | get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))]) *) (*FIX - should this have vars in it? *) -fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[])) - +fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[])) in true end @@ -155,9 +151,6 @@ fun thmstrings [] str = str | thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x)) -fun onelist [] newlist = newlist -| onelist (x::xs) newlist = onelist xs (newlist@x) - fun get_axioms_used proof_steps thmstring = let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr"))) @@ -175,7 +168,7 @@ val distvars = distinct (fold append vars []) val clause_terms = map prop_of clauses - val clause_frees = onelist (map term_frees clause_terms) [] + val clause_frees = List.concat (map term_frees clause_terms) val frees = map lit_string_with_nums clause_frees; @@ -313,7 +306,7 @@ val _ = TextIO.output (outfile, (thmstring)) val _ = TextIO.closeOut outfile val proofextract = extract_proof proofstr - val tokens = fst(lex proofextract) + val tokens = #1(lex proofextract) (***********************************) (* parse spass proof into datatype *) @@ -352,8 +345,8 @@ (* turn the proof into a string *) val reconProofStr = proofs_to_string proof "" (* do the bit for the Isabelle ordered axioms at the top *) - val ax_nums = map fst numcls - val ax_strs = map get_meta_lits_bracket (map snd numcls) + val ax_nums = map #1 numcls + val ax_strs = map get_meta_lits_bracket (map #2 numcls) val numcls_strs = zip ax_nums ax_strs val num_cls_vars = map (addvars vars) numcls_strs; val reconIsaAxStr = origAxs_to_string (zip ax_nums ax_with_vars) "" @@ -449,7 +442,7 @@ val number_list_step = - ( number ++ many ((a (Other ",") ++ number)>> snd)) + ( number ++ many ((a (Other ",") ++ number)>> #2)) >> (fn (a,b) => (a::b)) val numberlist_step = a (Other "[") ++ a (Other "]") @@ -510,9 +503,9 @@ val lines_step = many linestep - val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> fst + val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> #1 - val parse_step = fst o alllines_step + val parse_step = #1 o alllines_step (* @@ -702,7 +695,7 @@ 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)))"; *) -fun apply_res_thm str goalstring = let val tokens = fst (lex str); +fun apply_res_thm str goalstring = let val tokens = #1 (lex str); val (frees,recon_steps) = parse_step tokens val isar_str = to_isar_proof (frees, recon_steps, goalstring) diff -r 1c1d40ff875a -r bb2acfed8212 src/HOL/Tools/ATP/recon_translate_proof.ML --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Apr 15 17:03:35 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Apr 15 18:16:05 2005 +0200 @@ -141,6 +141,7 @@ (* Reconstruct a factoring step *) (*************************************) +(*FIXME: share code with that in Tools/reconstruction.ML*) fun follow_factor clause lit1 lit2 allvars thml clause_strs= let val th = Recon_Base.assoc clause thml @@ -148,7 +149,7 @@ val sign = sign_of_thm th val fac1 = get_nth (lit1+1) prems val fac2 = get_nth (lit2+1) prems - val unif_env = Unify.unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)]) + val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)]) val newenv = getnewenv unif_env val envlist = Envir.alist_of newenv