# HG changeset patch # User paulson # Date 1163188728 -3600 # Node ID 33b6bb5d6ab80f9838520a6cc1048caac9587c94 # Parent 920b7b893d9c06e4d0e7e19ca07e3fa75efbe1db Improvement to classrel clauses: now outputs the minimum needed. Theorem names: trying to minimize the number of multiple theorem names presented diff -r 920b7b893d9c -r 33b6bb5d6ab8 src/HOL/Tools/res_atp.ML --- 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 diff -r 920b7b893d9c -r 33b6bb5d6ab8 src/HOL/Tools/res_axioms.ML --- 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) ****) diff -r 920b7b893d9c -r 33b6bb5d6ab8 src/HOL/Tools/res_clause.ML --- 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 **)