# HG changeset patch # User paulson # Date 1120753502 -7200 # Node ID 7a6c17b826c0caa95d192dd40a400fb81c5da511 # Parent a5ae2757dd09c694db0acff6d88ab3ca9bde0dbb inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL diff -r a5ae2757dd09 -r 7a6c17b826c0 src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Thu Jul 07 18:24:20 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Thu Jul 07 18:25:02 2005 +0200 @@ -5,9 +5,124 @@ Copyright 2004 University of Cambridge *) + +structure ReduceAxiomsN = +(* Author: Jia Meng, Cambridge University Computer Laboratory + Remove irrelevant axioms used for a proof of a goal, with with iteration control*) + +struct + +fun add_term_consts_rm ncs (Const(c, _)) cs = + if (c mem ncs) then cs else (c ins_string cs) + | add_term_consts_rm ncs (t $ u) cs = add_term_consts_rm ncs t (add_term_consts_rm ncs u cs) + | add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs + | add_term_consts_rm ncs _ cs = cs; + + +fun term_consts_rm ncs t = add_term_consts_rm ncs t []; + + +fun thm_consts_rm ncs thm = term_consts_rm ncs (prop_of thm); + + +fun consts_of_thm (n,thm) = thm_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] thm; + + + + +fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term; + +fun make_pairs [] _ = [] + | make_pairs (x::xs) y = (x,y)::(make_pairs xs y); + + + +fun const_thm_list_aux [] cthms = cthms + | const_thm_list_aux (thm::thms) cthms = + let val consts = consts_of_thm thm + val cthms' = make_pairs consts thm + in + const_thm_list_aux thms (cthms' @ cthms) + end; + + +fun const_thm_list thms = const_thm_list_aux thms []; + +fun make_thm_table thms = + let val consts_thms = const_thm_list thms + in + Symtab.make_multi consts_thms + end; + + +fun consts_in_goal goal = consts_of_term goal; + +fun axioms_having_consts_aux [] tab thms = thms + | axioms_having_consts_aux (c::cs) tab thms = + let val thms1 = Symtab.lookup(tab,c) + val thms2 = + case thms1 of (SOME x) => x + | NONE => [] + in + axioms_having_consts_aux cs tab (thms2 union thms) + end; + + +fun axioms_having_consts cs tab = axioms_having_consts_aux cs tab []; + + +fun relevant_axioms goal thmTab n = + let val consts = consts_in_goal goal + fun relevant_axioms_aux1 cs k = + let val thms1 = axioms_having_consts cs thmTab + val cs1 = ResLib.flat_noDup (map consts_of_thm thms1) + in + if ((cs1 subset cs) orelse (n <= k)) then (k,thms1) + else (relevant_axioms_aux1 (cs1 union cs) (k+1)) + end + + fun relevant_axioms_aux2 cs k = + let val thms1 = axioms_having_consts cs thmTab + val cs1 = ResLib.flat_noDup (map consts_of_thm thms1) + in + if (cs1 subset cs) then (k,thms1) + else (relevant_axioms_aux2 (cs1 union cs) (k+1)) + end + + in + if n <= 0 then (relevant_axioms_aux2 consts 1) else (relevant_axioms_aux1 consts 1) + end; + + + +fun relevant_filter n goal thms = #2 (relevant_axioms goal (make_thm_table thms) n); + + +(* find the thms from thy that contain relevant constants, n is the iteration number *) +fun find_axioms_n thy goal n = + let val clasetR = ResAxioms.claset_rules_of_thy thy + val simpsetR = ResAxioms.simpset_rules_of_thy thy + val table = make_thm_table (clasetR @ simpsetR) + in + relevant_axioms goal table n + end; + + +fun find_axioms_n_c thy goal n = + let val current_thms = PureThy.thms_of thy + val table = make_thm_table current_thms + in + relevant_axioms goal table n + + end; + +end; + + signature RES_CLASIMP = sig - val write_out_clasimp :string -> theory -> (ResClause.clause * thm) Array.array * int + val write_out_clasimp : string -> theory -> term -> + (ResClause.clause * thm) Array.array * int val write_out_clasimp_small :string -> theory -> (ResClause.clause * thm) Array.array * int end; @@ -72,14 +187,17 @@ (multi_name) end; -(*Write out the claset and simpset rules of the supplied theory.*) -fun write_out_clasimp filename thy = - let val claset_rules = ResAxioms.claset_rules_of_thy thy; +(*Write out the claset and simpset rules of the supplied theory. + FIXME: argument "goal" is a hack to allow relevance filtering.*) +fun write_out_clasimp filename thy goal = + let val claset_rules = ReduceAxiomsN.relevant_filter 1 goal + (ResAxioms.claset_rules_of_thy thy); val named_claset = List.filter has_name_pair claset_rules; val claset_names = map remove_spaces_pair (named_claset) val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []); - val simpset_rules = ResAxioms.simpset_rules_of_thy thy; + val simpset_rules = ReduceAxiomsN.relevant_filter 1 goal + (ResAxioms.simpset_rules_of_thy thy); val named_simpset = map remove_spaces_pair (List.filter has_name_pair simpset_rules) val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []); diff -r a5ae2757dd09 -r 7a6c17b826c0 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Jul 07 18:24:20 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Jul 07 18:25:02 2005 +0200 @@ -287,10 +287,13 @@ (******************************************************************) (*FIX changed to clasimp_file *) fun isar_atp' (ctxt,thms, thm) = + if null (prems_of thm) then () + else let - val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) + val _= (print_mode := (Library.gen_rems (op =) + (! print_mode, ["xsymbols", "symbols"]))) val _= (warning ("in isar_atp'")) - val prems = prems_of thm + val prems = prems_of thm val sign = sign_of_thm thm val thms_string = Meson.concat_with_and (map string_of_thm thms) val thmstring = string_of_thm thm @@ -298,22 +301,21 @@ (* set up variables for writing out the clasimps to a tptp file *) val (clause_arr, num_of_clauses) = - ResClasimp.write_out_clasimp(*_small*) (File.platform_path clasimp_file) + ResClasimp.write_out_clasimp (File.platform_path clasimp_file) (ProofContext.theory_of ctxt) - val _ = (warning ("clasimp_file is this: "^(File.platform_path clasimp_file)) ) - - + (hd prems) (*FIXME: hack!! need to do all prems*) + val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file) val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses) - val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid ))) + val pidstring = string_of_int(Word.toInt + (Word.fromLargeWord ( Posix.Process.pidToWord pid ))) in - case prems of [] => () - | _ => ((warning ("initial thms: "^thms_string)); - (warning ("initial thm: "^thmstring)); - (warning ("subgoals: "^prems_string)); - (warning ("pid: "^ pidstring))); - isar_atp_aux thms thm (length prems) (childin, childout, pid) ; - (warning("turning xsymbol back on!")); - print_mode := (["xsymbols", "symbols"] @ ! print_mode) + warning ("initial thms: "^thms_string); + warning ("initial thm: "^thmstring); + warning ("subgoals: "^prems_string); + warning ("pid: "^ pidstring); + isar_atp_aux thms thm (length prems) (childin, childout, pid); + warning("turning xsymbol back on!"); + print_mode := (["xsymbols", "symbols"] @ ! print_mode) end; diff -r a5ae2757dd09 -r 7a6c17b826c0 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Thu Jul 07 18:24:20 2005 +0200 +++ b/src/HOL/Tools/res_clause.ML Thu Jul 07 18:25:02 2005 +0200 @@ -577,7 +577,7 @@ | string_of_term (Fun (name,typ,terms)) = let val terms' = map string_of_term terms in - if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms')) + if (!keep_types) then name ^ (ResLib.list_to_string (terms' @ [typ])) else name ^ (ResLib.list_to_string terms') end; @@ -590,7 +590,8 @@ | string_of_predicate (Predicate(name,typ,terms)) = let val terms_as_strings = map string_of_term terms in - if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms_as_strings)) + if (!keep_types) + then name ^ (ResLib.list_to_string (terms_as_strings @ [typ])) else name ^ (ResLib.list_to_string terms_as_strings) end;