# HG changeset patch # User paulson # Date 1113564953 -7200 # Node ID 1bb0399a9517d55856fd97714c5dbe5d9668eea0 # Parent 953f188e16c6ad69dc405726b1c1668c46cdc40f more tidying up of the SPASS interface diff -r 953f188e16c6 -r 1bb0399a9517 src/HOL/Tools/ATP/recon_translate_proof.ML --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Apr 15 12:00:00 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Apr 15 13:35:53 2005 +0200 @@ -214,7 +214,6 @@ val rev_ssubst = rotate_prems 1 ssubst; -(* have changed from negate_nead to negate_head. God knows if this will actually work *) fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= let val th1 = Recon_Base.assoc clause1 thml @@ -403,14 +402,11 @@ fun not_newline ch = not (ch = "\n"); -fun concat_with_and [] str = str -| concat_with_and (x::[]) str = str^"("^x^")" -| concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & ")) (* fun follow clauses [] allvars thml recons = let (* val _ = reset show_sorts*) - val thmstring = concat_with_and (map string_of_thm (map snd thml)) "" + val thmstring = Meson.concat_with_and (map string_of_thm (map snd thml)) val thmproofstring = proofstring ( thmstring) val no_returns =List.filter not_newline ( thmproofstring) val thmstr = implode no_returns diff -r 953f188e16c6 -r 1bb0399a9517 src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Fri Apr 15 12:00:00 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Fri Apr 15 13:35:53 2005 +0200 @@ -62,20 +62,6 @@ |SOME cls => cls ; -fun retr_thms ([]:MetaSimplifier.rrule list) = [] - | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs); - -fun snds [] = [] - | snds ((x,y)::l) = y::(snds l); - -fun simpset_rules_of_thy thy = - let val simpset = simpset_of thy - val rules = #rules(fst (rep_ss simpset)) - val thms = retr_thms (snds(Net.dest rules)) - in thms end; - - - fun not_second c (a,b) = not_equal b c; @@ -124,7 +110,7 @@ val names_rules = zip good_names name_fol_cs; - val new_clasrls = (fst(ResAxioms.clausify_classical_rules name_fol_cs[])); + val new_clasrls = #1(ResAxioms.clausify_classical_rules name_fol_cs[]) val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls; @@ -161,25 +147,25 @@ (*********************) (* Get simpset rules *) (*********************) - val (simpset_name_rules) =simpset_rules_of_thy (the_context()); + val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context()); val named_simps = List.filter has_name_pair simpset_name_rules; - val simp_names = map fst named_simps; - val simp_rules = map snd named_simps; + val simp_names = map #1 named_simps; + val simp_rules = map #2 named_simps; val (simpset_cls,badthms) = ResAxioms.clausify_simpset_rules simp_rules []; (* 1137 clausif simps *) val clausifiable_simps = remove_all_simps badthms named_simps; val name_fol_simps = List.filter thm_is_fol clausifiable_simps ; - val simp_names = map fst name_fol_simps; - val simp_rules = map snd name_fol_simps; + val simp_names = map #1 name_fol_simps; + val simp_rules = map #2 name_fol_simps; (* 995 of these *) (* need to get names of claset_cluases so we can make sure we've*) (* got the same ones (ie. the named ones ) as the claset rules *) (* length 1374*) - val new_simps = fst(ResAxioms.clausify_simpset_rules simp_rules []); + val new_simps = #1(ResAxioms.clausify_simpset_rules simp_rules []); val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps; val stick_strs = map stick simpset_tptp_strs; diff -r 953f188e16c6 -r 1bb0399a9517 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Fri Apr 15 12:00:00 2005 +0200 +++ b/src/HOL/Tools/meson.ML Fri Apr 15 13:35:53 2005 +0200 @@ -84,12 +84,10 @@ | has _ = false in has end; -(* for tracing statements *) - -fun concat_with_and [] str = str -| concat_with_and (x::[]) str = str^" ("^x^")" -| concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & ")) - +(* for tracing: encloses each string element in brackets. *) +fun concat_with_and [] = "" + | concat_with_and [x] = "(" ^ x ^ ")" + | concat_with_and (x::xs) = "(" ^ x ^ ")" ^ " & " ^ concat_with_and xs; (**** Clause handling ****) @@ -326,7 +324,8 @@ (*Make clauses from a list of theorems, previously Skolemized and put into nnf. The resulting clauses are HOL disjunctions.*) fun make_clauses ths = - ( (warning("in make_clauses ths are:"^(concat_with_and (map string_of_thm ths) ""))); sort_clauses (map (generalize o nodups) (foldr cnf [] ths))); + (warning("in make_clauses ths = " ^ concat_with_and (map string_of_thm ths)); + sort_clauses (map (generalize o nodups) (foldr cnf [] ths))); (*Convert a list of clauses to (contrapositive) Horn clauses*) fun make_horns ths = diff -r 953f188e16c6 -r 1bb0399a9517 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri Apr 15 12:00:00 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Fri Apr 15 13:35:53 2005 +0200 @@ -64,12 +64,6 @@ val dummy_tac = PRIMITIVE(fn thm => thm ); -fun concat_with_and [] str = str -| concat_with_and (x::[]) str = str^" ("^x^")" -| concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & ")) - - - (**** for Isabelle/ML interface ****) fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ") @@ -147,7 +141,7 @@ (*********************************************************************) fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = let - val thmstring = concat_with_and (map string_of_thm thms) "" + val thmstring = Meson.concat_with_and (map string_of_thm thms) val thm_no = length thms val _ = warning ("number of thms is : "^(string_of_int thm_no)) val _ = warning ("thmstring in call_res is: "^thmstring) @@ -163,7 +157,7 @@ val clauses = make_clauses thms val _ =( warning ("called make_clauses "))*) (*val _ = tptp_inputs clauses prob_file*) - val thmstring = concat_with_and (map string_of_thm thms) "" + val thmstring = Meson.concat_with_and (map string_of_thm thms) val goalstr = Sign.string_of_term sign sg_term val goalproofstring = proofstring goalstr @@ -227,7 +221,8 @@ (* dummy tac vs. Doesn't call resolve_tac *) fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = - ( warning("ths for tptp: " ^ (concat_with_and (map string_of_thm thms) "")); + ( warning("ths for tptp: " ^ + Meson.concat_with_and (map string_of_thm thms)); warning("in call_atp_tac_tfrees"); tptp_inputs_tfrees (make_clauses thms) n tfrees; @@ -243,7 +238,7 @@ SELECT_GOAL (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, METAHYPS(fn negs => (warning("calling call_atp_tac_tfrees with negs" - ^ (concat_with_and (map string_of_thm negs) "")); + ^ Meson.concat_with_and (map string_of_thm negs)); call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st end; @@ -305,9 +300,9 @@ val _= (warning ("in isar_atp'")) val prems = prems_of thm val sign = sign_of_thm thm - val thms_string =concat_with_and (map string_of_thm thms) "" + val thms_string = Meson.concat_with_and (map string_of_thm thms) val thmstring = string_of_thm thm - val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) "" + val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) (* set up variables for writing out the clasimps to a tptp file *) val _ = write_out_clasimp (File.sysify_path axiom_file) (* cq: add write out clasimps to file *) @@ -397,9 +392,8 @@ val sg_prems = prems_of thm val sign = sign_of_thm thm val prem_no = length sg_prems - val prems_string = concat_with_and (map (Sign.string_of_term sign) sg_prems) "" + val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) in - (warning ("initial thm in isar_atp: "^thmstring)); (warning ("subgoals in isar_atp: "^prems_string)); (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no))); diff -r 953f188e16c6 -r 1bb0399a9517 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Fri Apr 15 12:00:00 2005 +0200 +++ b/src/HOL/Tools/res_axioms.ML Fri Apr 15 13:35:53 2005 +0200 @@ -229,7 +229,7 @@ val rm_Eps : (Term.term * Term.term) list -> Thm.thm list -> Term.term list val claset_rules_of_thy : Theory.theory -> Thm.thm list -val simpset_rules_of_thy : Theory.theory -> Thm.thm list +val simpset_rules_of_thy : Theory.theory -> (string * Thm.thm) list val clausify_simpset_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list val clausify_classical_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list @@ -391,17 +391,8 @@ (******** Extracting and CNF/Clausify theorems from a classical reasoner and simpset of a given theory ******) -local - fun retr_thms ([]:MetaSimplifier.rrule list) = [] - | retr_thms (r::rs) = (#thm r)::(retr_thms rs); - - -fun snds [] = [] - | snds ((x,y)::l) = y::(snds l); - -in - + | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs); fun claset_rules_of_thy thy = let val clsset = rep_cs (claset_of thy) @@ -416,13 +407,11 @@ fun simpset_rules_of_thy thy = let val simpset = simpset_of thy val rules = #rules(fst (rep_ss simpset)) - val thms = retr_thms (snds(Net.dest rules)) + val thms = retr_thms (map #2 (Net.dest rules)) in thms end; -end; - (**** Translate a set of classical rules or simplifier rules into CNF (still as type "thm") from a given theory ****) @@ -455,7 +444,7 @@ (* CNF all simplifier rules from a given theory's simpset *) fun cnf_simpset_rules_thy thy = - let val thms = simpset_rules_of_thy thy + let val thms = map #2 (simpset_rules_of_thy thy) in cnf_simpset_rules thms [] end; @@ -474,7 +463,7 @@ -(* convert all classical rules from a given theory's classical reasoner into Clause.clause format. *) +(* convert all classical rules from a given theory into Clause.clause format. *) fun clausify_classical_rules_thy thy = let val rules = claset_rules_of_thy thy in @@ -491,9 +480,9 @@ end; -(* convert all simplifier rules from a given theory's simplifier into Clause.clause format. *) +(* convert all simplifier rules from a given theory into Clause.clause format. *) fun clausify_simpset_rules_thy thy = - let val thms = simpset_rules_of_thy thy + let val thms = map #2 (simpset_rules_of_thy thy) in clausify_simpset_rules thms [] end;