Improvement to classrel clauses: now outputs the minimum needed.
Theorem names: trying to minimize the number of multiple theorem names presented
--- a/src/HOL/Tools/res_atp.ML Fri Nov 10 19:04:18 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML Fri Nov 10 20:58:48 2006 +0100
@@ -72,7 +72,7 @@
fun set_prover atp =
case String.map Char.toLower atp of
"e" =>
- (ReduceAxiomsN.max_new := 80;
+ (ReduceAxiomsN.max_new := 100;
ReduceAxiomsN.theory_const := false;
prover := "E")
| "spass" =>
@@ -585,11 +585,16 @@
fun multi_name a (th, (n,pairs)) =
(n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
-fun multi_names ((a, []), pairs) = pairs
- | multi_names ((a, [th]), pairs) = (a,th)::pairs
- | multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
+fun add_multi_names ((a, []), pairs) = pairs
+ | add_multi_names ((a, [th]), pairs) = (a,th)::pairs
+ | add_multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
-fun name_thm_pairs ctxt = foldl multi_names [] (all_valid_thms ctxt);
+fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
+
+(*The single theorems go BEFORE the multiple ones*)
+fun name_thm_pairs ctxt =
+ let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
+ in foldl add_multi_names (foldl add_multi_names [] mults) singles end;
fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
| check_named (_,th) = true;
@@ -633,6 +638,24 @@
in okthms end
else thms;
+(***************************************************************)
+(* Type Classes Present in the Axiom or Conjecture Clauses *)
+(***************************************************************)
+
+fun setinsert (x,s) = Symtab.update (x,()) s;
+
+fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts);
+
+(*Remove this trivial type class*)
+fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
+
+fun tvar_classes_of_terms ts =
+ let val sorts_list = map (map #2 o term_tvars) ts
+ in Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list)) end;
+
+fun tfree_classes_of_terms ts =
+ let val sorts_list = map (map #2 o term_tfrees) ts
+ in Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list)) end;
(***************************************************************)
(* ATP invocation methods setup *)
@@ -681,7 +704,12 @@
val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
user_cls (map prop_of goal_cls) |> make_unique
val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
- val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
+ val subs = tfree_classes_of_terms (map prop_of goal_cls)
+ and supers = tvar_classes_of_terms (map (prop_of o #1) axclauses)
+ (*TFrees in conjecture clauses; TVars in axiom clauses*)
+ val classrel_clauses =
+ if keep_types then ResClause.make_classrel_clauses thy subs supers
+ else []
val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
val writer = if dfg then dfg_writer else tptp_writer
and file = atp_input_file()
@@ -800,10 +828,6 @@
axcls_list
val keep_types = if is_fol_logic logic then !ResClause.keep_types
else is_typed_hol ()
- val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
- else []
- val _ = Output.debug ("classrel clauses = " ^
- Int.toString (length classrel_clauses))
val arity_clauses = if keep_types then ResClause.arity_clause_thy thy
else []
val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
@@ -813,6 +837,13 @@
let val fname = probfile k
val axcls = make_unique axcls
val ccls = subtract_cls ccls axcls
+ val subs = tfree_classes_of_terms (map prop_of ccls)
+ and supers = tvar_classes_of_terms (map (prop_of o #1) axcls)
+ (*TFrees in conjecture clauses; TVars in axiom clauses*)
+ val classrel_clauses =
+ if keep_types then ResClause.make_classrel_clauses thy subs supers
+ else []
+ val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
val thm_names = Array.fromList clnames
val _ = if !Output.show_debug_msgs
--- a/src/HOL/Tools/res_axioms.ML Fri Nov 10 19:04:18 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML Fri Nov 10 20:58:48 2006 +0100
@@ -647,7 +647,8 @@
handle THM _ => pairs | ResClause.CLAUSE _ => pairs
in cnf_rules_pairs_aux pairs' ths end;
-val cnf_rules_pairs = cnf_rules_pairs_aux [];
+(*The combination of rev and tail recursion preserves the original order*)
+fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l);
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
--- a/src/HOL/Tools/res_clause.ML Fri Nov 10 19:04:18 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML Fri Nov 10 20:58:48 2006 +0100
@@ -23,7 +23,7 @@
val arity_clause_thy: theory -> arityClause list
val ascii_of : string -> string
val bracket_pack : string list -> string
- val classrel_clauses_thy: theory -> classrelClause list
+ val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
val clause_prefix : string
val clause2tptp : clause -> string * string list
val const_prefix : string
@@ -529,23 +529,22 @@
ClassrelClause of {axiom_name: axiom_name,
subclass: class,
superclass: class};
-
-fun make_axiom_classrelClause n subclass superclass =
- ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of subclass ^
- "_" ^ Int.toString n,
- subclass = make_type_class subclass,
- superclass = make_type_class superclass};
+
+(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
+fun class_pairs thy subs supers =
+ let val class_less = Sorts.class_less(Sign.classes_of thy)
+ fun add_super sub (super,pairs) =
+ if class_less (sub,super) then (sub,super)::pairs else pairs
+ fun add_supers (sub,pairs) = foldl (add_super sub) pairs supers
+ in foldl add_supers [] subs end;
-fun classrelClauses_of_aux n sub [] = []
- | classrelClauses_of_aux n sub ("HOL.type"::sups) = (*Should be ignored*)
- classrelClauses_of_aux n sub sups
- | classrelClauses_of_aux n sub (sup::sups) =
- make_axiom_classrelClause n sub sup :: classrelClauses_of_aux (n+1) sub sups;
+fun make_classrelClause (sub,super) =
+ ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
+ subclass = make_type_class sub,
+ superclass = make_type_class super};
-fun classrelClauses_of (sub,sups) = classrelClauses_of_aux 0 sub sups;
-
-val classrel_clauses_thy =
- maps classrelClauses_of o Graph.dest o #classes o Sorts.rep_algebra o Sign.classes_of;
+fun make_classrel_clauses thy subs supers =
+ map make_classrelClause (class_pairs thy subs supers);
(** Isabelle arities **)