# HG changeset patch # User blanchet # Date 1279739687 -7200 # Node ID 1188e6bff48dabc1248eb905f3fc157fb5134f1f # Parent 17f36ad210d64b90a4b98904c841cb28f52d8625 rename "classrel" to "class_rel" diff -r 17f36ad210d6 -r 1188e6bff48d src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 21 21:14:26 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 21 21:14:47 2010 +0200 @@ -233,10 +233,11 @@ val helper_clauses = get_helper_clauses thy is_FO full_types conjectures extra_cls val (supers', arity_clauses) = make_arity_clauses thy tycons supers - val classrel_clauses = make_classrel_clauses thy subs supers' + val class_rel_clauses = make_class_rel_clauses thy subs supers' in (Vector.fromList clnames, - (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses)) + (conjectures, axiom_clauses, extra_clauses, helper_clauses, + class_rel_clauses, arity_clauses)) end diff -r 17f36ad210d6 -r 1188e6bff48d src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Wed Jul 21 21:14:26 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Wed Jul 21 21:14:47 2010 +0200 @@ -18,7 +18,7 @@ TVarLit of name * name datatype arity_clause = ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list} - datatype classrel_clause = ClassrelClause of + datatype class_rel_clause = ClassRelClause of {axiom_name: string, subclass: name, superclass: name} datatype combtyp = CombTVar of name | @@ -59,7 +59,7 @@ val is_skolem_const_name: string -> bool val num_type_args: theory -> string -> int val type_literals_for_types : typ list -> type_literal list - val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list + val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list val type_of_combterm : combterm -> combtyp val strip_combterm_comb : combterm -> combterm * combterm list @@ -85,7 +85,7 @@ val tvar_prefix = "T_"; val tfree_prefix = "t_"; -val classrel_clause_prefix = "clsrel_"; +val class_rel_clause_prefix = "clsrel_"; val const_prefix = "c_"; val type_const_prefix = "tc_"; @@ -288,8 +288,8 @@ (**** Isabelle class relations ****) -datatype classrel_clause = - ClassrelClause of {axiom_name: string, subclass: name, superclass: name} +datatype class_rel_clause = + ClassRelClause of {axiom_name: string, subclass: name, superclass: name} (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) fun class_pairs _ [] _ = [] @@ -300,14 +300,14 @@ fun add_supers sub = fold (add_super sub) supers in fold add_supers subs [] end -fun make_classrel_clause (sub,super) = - ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^ +fun make_class_rel_clause (sub,super) = + ClassRelClause {axiom_name = class_rel_clause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super, subclass = `make_type_class sub, superclass = `make_type_class super}; -fun make_classrel_clauses thy subs supers = - map make_classrel_clause (class_pairs thy subs supers); +fun make_class_rel_clauses thy subs supers = + map make_class_rel_clause (class_pairs thy subs supers); (** Isabelle arities **) diff -r 17f36ad210d6 -r 1188e6bff48d src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Jul 21 21:14:26 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Jul 21 21:14:47 2010 +0200 @@ -170,11 +170,11 @@ (* CLASSREL CLAUSE *) -fun m_classrel_cls (subclass, _) (superclass, _) = +fun m_class_rel_cls (subclass, _) (superclass, _) = [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]]; -fun classrel_cls (ClassrelClause {subclass, superclass, ...}) = - (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass))); +fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) = + (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_class_rel_cls subclass superclass))); (* ------------------------------------------------------------------------- *) (* FOL to HOL (Metis to Isabelle) *) @@ -606,8 +606,8 @@ val supers = tvar_classes_of_terms tms and tycons = type_consts_of_terms thy tms val (supers', arity_clauses) = make_arity_clauses thy tycons supers - val classrel_clauses = make_classrel_clauses thy subs supers' - in map classrel_cls classrel_clauses @ map arity_cls arity_clauses + val class_rel_clauses = make_class_rel_clauses thy subs supers' + in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end; (* ------------------------------------------------------------------------- *) diff -r 17f36ad210d6 -r 1188e6bff48d src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Wed Jul 21 21:14:26 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Wed Jul 21 21:14:47 2010 +0200 @@ -7,7 +7,7 @@ signature SLEDGEHAMMER_TPTP_FORMAT = sig - type classrel_clause = Metis_Clauses.classrel_clause + type class_rel_clause = Metis_Clauses.class_rel_clause type arity_clause = Metis_Clauses.arity_clause type fol_clause = Metis_Clauses.fol_clause type name_pool = string Symtab.table * string Symtab.table @@ -15,7 +15,7 @@ val write_tptp_file : theory -> bool -> bool -> bool -> Path.T -> fol_clause list * fol_clause list * fol_clause list * fol_clause list - * classrel_clause list * arity_clause list + * class_rel_clause list * arity_clause list -> name_pool option * int end; @@ -164,8 +164,8 @@ Cnf (hol_ident axiom_name clause_id, kind, atp_literals_for_axiom full_types clause) -fun problem_line_for_classrel - (ClassrelClause {axiom_name, subclass, superclass, ...}) = +fun problem_line_for_class_rel + (ClassRelClause {axiom_name, subclass, superclass, ...}) = let val ty_arg = ATerm (("T", "T"), []) in Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])), (true, ATerm (superclass, [ty_arg]))]) @@ -303,17 +303,17 @@ fun write_tptp_file thy readable_names full_types explicit_apply file (conjectures, axiom_clauses, extra_clauses, helper_clauses, - classrel_clauses, arity_clauses) = + class_rel_clauses, arity_clauses) = let val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses - val classrel_lines = map problem_line_for_classrel classrel_clauses + val class_rel_lines = map problem_line_for_class_rel class_rel_clauses val arity_lines = map problem_line_for_arity arity_clauses val helper_lines = map (problem_line_for_axiom full_types) helper_clauses val conjecture_lines = map (problem_line_for_conjecture full_types) conjectures val tfree_lines = problem_lines_for_free_types conjectures val problem = [("Relevant facts", axiom_lines), - ("Class relationships", classrel_lines), + ("Class relationships", class_rel_lines), ("Arity declarations", arity_lines), ("Helper facts", helper_lines), ("Conjectures", conjecture_lines), @@ -321,7 +321,7 @@ |> repair_problem thy full_types explicit_apply val (problem, pool) = nice_problem problem (empty_name_pool readable_names) val conjecture_offset = - length axiom_lines + length classrel_lines + length arity_lines + length axiom_lines + length class_rel_lines + length arity_lines + length helper_lines val _ = File.write_list file (strings_for_problem problem) in (pool, conjecture_offset) end