--- 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
--- 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