--- 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 []);
--- 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;
--- 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;