# HG changeset patch # User paulson # Date 1165936857 -3600 # Node ID 9d2761d09d91a10273aa4e80706de60a96267cf3 # Parent c4f6bb3920308f91d97f019c7af53820290ed772 Removal of the "keep_types" flag: we always keep types! diff -r c4f6bb392030 -r 9d2761d09d91 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Tue Dec 12 12:03:46 2006 +0100 +++ b/src/HOL/Tools/res_atp.ML Tue Dec 12 16:20:57 2006 +0100 @@ -31,7 +31,6 @@ val atp_method: (Proof.context -> thm list -> int -> tactic) -> Method.src -> Proof.context -> Proof.method val cond_rm_tmp: string -> unit - val fol_keep_types: bool ref val hol_full_types: unit -> unit val hol_partial_types: unit -> unit val hol_const_types_only: unit -> unit @@ -135,7 +134,6 @@ fun eproverLimit () = !eprover_time; fun spassLimit () = !spass_time; -val fol_keep_types = ResClause.keep_types; val hol_full_types = ResHolClause.full_types; val hol_partial_types = ResHolClause.partial_types; val hol_const_types_only = ResHolClause.const_types_only; @@ -741,16 +739,13 @@ val user_cls = ResAxioms.cnf_rules_pairs user_rules val thy = ProofContext.theory_of ctxt val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms) - val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol () val subs = tfree_classes_of_terms goal_tms and axtms = map (prop_of o #1) axclauses val supers = tvar_classes_of_terms axtms and tycons = type_consts_of_terms thy (goal_tms@axtms) (*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 tycons supers else [] + val classrel_clauses = ResClause.make_classrel_clauses thy subs supers + val arity_clauses = ResClause.arity_clause_thy thy tycons supers val writer = if dfg then dfg_writer else tptp_writer and file = atp_input_file() and user_lemmas_names = map #1 user_rules @@ -861,8 +856,6 @@ val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls))) axcls_list - val keep_types = if is_fol_logic logic then !ResClause.keep_types - else is_typed_hol () val writer = if !prover = "spass" then dfg_writer else tptp_writer fun write_all [] [] _ = [] | write_all (ccls::ccls_list) (axcls::axcls_list) k = @@ -875,12 +868,9 @@ and supers = tvar_classes_of_terms axtms and tycons = type_consts_of_terms thy (ccltms@axtms) (*TFrees in conjecture clauses; TVars in axiom clauses*) - val classrel_clauses = - if keep_types then ResClause.make_classrel_clauses thy subs supers - else [] + val classrel_clauses = ResClause.make_classrel_clauses thy subs supers val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses)) - val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers - else [] + val arity_clauses = ResClause.arity_clause_thy thy tycons supers val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses)) val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) [] val thm_names = Array.fromList clnames diff -r c4f6bb392030 -r 9d2761d09d91 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Tue Dec 12 12:03:46 2006 +0100 +++ b/src/HOL/Tools/res_clause.ML Tue Dec 12 16:20:57 2006 +0100 @@ -38,7 +38,6 @@ val init : theory -> unit val isMeta : string -> bool val isTaut : clause -> bool - val keep_types : bool ref val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order val make_axiom_clause : thm -> string * int -> clause option val make_conjecture_clauses : thm list -> clause list @@ -201,8 +200,6 @@ (***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****) -val keep_types = ref true; - datatype kind = Axiom | Conjecture; fun name_of_kind Axiom = "axiom" | name_of_kind Conjecture = "negated_conjecture"; @@ -274,7 +271,7 @@ (*Declarations of the current theory--to allow suppressing types.*) val const_typargs = ref (Library.K [] : (string*typ -> typ list)); -fun num_typargs(s,T) = if !keep_types then length (!const_typargs (s,T)) else 0; +fun num_typargs(s,T) = length (!const_typargs (s,T)); (*Initialize the type suppression mechanism with the current theory before producing any clauses!*) @@ -633,10 +630,8 @@ (**** String-oriented operations ****) fun string_of_term (UVar(x,_)) = x - | string_of_term (Fun (name,typs,[])) = name ^ (paren_pack (map string_of_fol_type typs)) | string_of_term (Fun (name,typs,terms)) = - let val typs' = if !keep_types then map string_of_fol_type typs else [] - in name ^ (paren_pack (map string_of_term terms @ typs')) end; + name ^ (paren_pack (map string_of_term terms @ map string_of_fol_type typs)); fun string_of_pair [t1,t2] = (string_of_term t1, string_of_term t2) | string_of_pair _ = raise ERROR ("equality predicate requires two arguments"); @@ -648,8 +643,7 @@ (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) fun string_of_predicate (Predicate("equal",_,ts)) = string_of_equality ts | string_of_predicate (Predicate(name,typs,ts)) = - let val typs' = if !keep_types then map string_of_fol_type typs else [] - in name ^ (paren_pack (map string_of_term ts @ typs')) end; + name ^ (paren_pack (map string_of_term ts @ map string_of_fol_type typs)); fun string_of_clausename (cls_id,ax_name) = clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id; @@ -685,14 +679,9 @@ string_of_clausename (cls_id,ax_name) ^ ").\n\n"; fun dfg_clause_aux (Clause{literals, types_sorts, ...}) = - let val lits = map dfg_literal literals - val (tvar_lits,tfree_lits) = add_typs_aux types_sorts - val tvar_lits_strs = - if !keep_types then map dfg_of_typeLit tvar_lits else [] - val tfree_lits = - if !keep_types then map dfg_of_typeLit tfree_lits else [] - in - (tvar_lits_strs @ lits, tfree_lits) + let val (tvar_lits,tfree_lits) = add_typs_aux types_sorts + in (map dfg_of_typeLit tvar_lits @ map dfg_literal literals, + map dfg_of_typeLit tfree_lits) end; fun dfg_folterms (Literal(pol,pred)) = @@ -809,15 +798,11 @@ name_of_kind knd ^ "," ^ tptp_pack lits ^ ").\n"; fun tptp_type_lits (Clause {literals, types_sorts, ...}) = - let val lits = map tptp_literal literals - val (tvar_lits,tfree_lits) = add_typs_aux types_sorts - val tvar_lits_strs = - if !keep_types then map tptp_of_typeLit tvar_lits else [] - val tfree_lits = - if !keep_types then map tptp_of_typeLit tfree_lits else [] - in - (tvar_lits_strs @ lits, tfree_lits) - end; + let val (tvar_lits,tfree_lits) = add_typs_aux types_sorts + in + (map tptp_of_typeLit tvar_lits @ map tptp_literal literals, + map tptp_of_typeLit tfree_lits) + end; fun clause2tptp (cls as Clause {clause_id, axiom_name, kind, ...}) = let val (lits,tfree_lits) = tptp_type_lits cls