Removal of the "keep_types" flag: we always keep types!
authorpaulson
Tue Dec 12 16:20:57 2006 +0100 (2006-12-12)
changeset 217909d2761d09d91
parent 21789 c4f6bb392030
child 21791 367477e8458b
Removal of the "keep_types" flag: we always keep types!
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Dec 12 12:03:46 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Dec 12 16:20:57 2006 +0100
     1.3 @@ -31,7 +31,6 @@
     1.4    val atp_method: (Proof.context -> thm list -> int -> tactic) ->
     1.5      Method.src -> Proof.context -> Proof.method
     1.6    val cond_rm_tmp: string -> unit
     1.7 -  val fol_keep_types: bool ref
     1.8    val hol_full_types: unit -> unit
     1.9    val hol_partial_types: unit -> unit
    1.10    val hol_const_types_only: unit -> unit
    1.11 @@ -135,7 +134,6 @@
    1.12  fun eproverLimit () = !eprover_time;
    1.13  fun spassLimit () = !spass_time;
    1.14  
    1.15 -val fol_keep_types = ResClause.keep_types;
    1.16  val hol_full_types = ResHolClause.full_types;
    1.17  val hol_partial_types = ResHolClause.partial_types;
    1.18  val hol_const_types_only = ResHolClause.const_types_only;
    1.19 @@ -741,16 +739,13 @@
    1.20          val user_cls = ResAxioms.cnf_rules_pairs user_rules
    1.21          val thy = ProofContext.theory_of ctxt
    1.22          val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
    1.23 -        val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
    1.24          val subs = tfree_classes_of_terms goal_tms
    1.25          and axtms = map (prop_of o #1) axclauses
    1.26          val supers = tvar_classes_of_terms axtms
    1.27          and tycons = type_consts_of_terms thy (goal_tms@axtms)
    1.28          (*TFrees in conjecture clauses; TVars in axiom clauses*)
    1.29 -        val classrel_clauses =
    1.30 -              if keep_types then ResClause.make_classrel_clauses thy subs supers
    1.31 -              else []
    1.32 -        val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers else []
    1.33 +        val classrel_clauses = ResClause.make_classrel_clauses thy subs supers
    1.34 +        val arity_clauses = ResClause.arity_clause_thy thy tycons supers
    1.35          val writer = if dfg then dfg_writer else tptp_writer
    1.36          and file = atp_input_file()
    1.37          and user_lemmas_names = map #1 user_rules
    1.38 @@ -861,8 +856,6 @@
    1.39        val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls
    1.40        val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
    1.41                    axcls_list
    1.42 -      val keep_types = if is_fol_logic logic then !ResClause.keep_types
    1.43 -                       else is_typed_hol ()
    1.44        val writer = if !prover = "spass" then dfg_writer else tptp_writer
    1.45        fun write_all [] [] _ = []
    1.46          | write_all (ccls::ccls_list) (axcls::axcls_list) k =
    1.47 @@ -875,12 +868,9 @@
    1.48                  and supers = tvar_classes_of_terms axtms
    1.49                  and tycons = type_consts_of_terms thy (ccltms@axtms)
    1.50                  (*TFrees in conjecture clauses; TVars in axiom clauses*)
    1.51 -                val classrel_clauses =
    1.52 -                      if keep_types then ResClause.make_classrel_clauses thy subs supers
    1.53 -                      else []
    1.54 +                val classrel_clauses = ResClause.make_classrel_clauses thy subs supers
    1.55                  val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.56 -                val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers
    1.57 -                                    else []
    1.58 +                val arity_clauses = ResClause.arity_clause_thy thy tycons supers
    1.59                  val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.60                  val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
    1.61                  val thm_names = Array.fromList clnames
     2.1 --- a/src/HOL/Tools/res_clause.ML	Tue Dec 12 12:03:46 2006 +0100
     2.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Dec 12 16:20:57 2006 +0100
     2.3 @@ -38,7 +38,6 @@
     2.4    val init : theory -> unit
     2.5    val isMeta : string -> bool
     2.6    val isTaut : clause -> bool
     2.7 -  val keep_types : bool ref
     2.8    val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order
     2.9    val make_axiom_clause : thm -> string * int -> clause option
    2.10    val make_conjecture_clauses : thm list -> clause list
    2.11 @@ -201,8 +200,6 @@
    2.12  
    2.13  (***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****)
    2.14  
    2.15 -val keep_types = ref true;
    2.16 -
    2.17  datatype kind = Axiom | Conjecture;
    2.18  fun name_of_kind Axiom = "axiom"
    2.19    | name_of_kind Conjecture = "negated_conjecture";
    2.20 @@ -274,7 +271,7 @@
    2.21  (*Declarations of the current theory--to allow suppressing types.*)
    2.22  val const_typargs = ref (Library.K [] : (string*typ -> typ list));
    2.23  
    2.24 -fun num_typargs(s,T) = if !keep_types then length (!const_typargs (s,T)) else 0;
    2.25 +fun num_typargs(s,T) = length (!const_typargs (s,T));
    2.26  
    2.27  (*Initialize the type suppression mechanism with the current theory before
    2.28      producing any clauses!*)
    2.29 @@ -633,10 +630,8 @@
    2.30  (**** String-oriented operations ****)
    2.31  
    2.32  fun string_of_term (UVar(x,_)) = x
    2.33 -  | string_of_term (Fun (name,typs,[])) = name ^ (paren_pack (map string_of_fol_type typs))
    2.34    | string_of_term (Fun (name,typs,terms)) = 
    2.35 -      let val typs' = if !keep_types then map string_of_fol_type typs else []
    2.36 -      in  name ^ (paren_pack (map string_of_term terms @ typs'))  end;
    2.37 +      name ^ (paren_pack (map string_of_term terms @ map string_of_fol_type typs));
    2.38  
    2.39  fun string_of_pair [t1,t2] = (string_of_term t1, string_of_term t2)
    2.40    | string_of_pair _ = raise ERROR ("equality predicate requires two arguments");
    2.41 @@ -648,8 +643,7 @@
    2.42  (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
    2.43  fun string_of_predicate (Predicate("equal",_,ts)) = string_of_equality ts
    2.44    | string_of_predicate (Predicate(name,typs,ts)) = 
    2.45 -      let val typs' = if !keep_types then map string_of_fol_type typs else []
    2.46 -      in  name ^ (paren_pack (map string_of_term ts @ typs'))  end;
    2.47 +      name ^ (paren_pack (map string_of_term ts @ map string_of_fol_type typs));
    2.48  
    2.49  fun string_of_clausename (cls_id,ax_name) = 
    2.50      clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
    2.51 @@ -685,14 +679,9 @@
    2.52      string_of_clausename (cls_id,ax_name) ^  ").\n\n";
    2.53  
    2.54  fun dfg_clause_aux (Clause{literals, types_sorts, ...}) = 
    2.55 -  let val lits = map dfg_literal literals
    2.56 -      val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
    2.57 -      val tvar_lits_strs = 
    2.58 -	  if !keep_types then map dfg_of_typeLit tvar_lits else []
    2.59 -      val tfree_lits =
    2.60 -          if !keep_types then map dfg_of_typeLit tfree_lits else []
    2.61 -  in
    2.62 -      (tvar_lits_strs @ lits, tfree_lits)
    2.63 +  let val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
    2.64 +  in  (map dfg_of_typeLit tvar_lits @ map dfg_literal literals, 
    2.65 +       map dfg_of_typeLit tfree_lits)
    2.66    end; 
    2.67  
    2.68  fun dfg_folterms (Literal(pol,pred)) = 
    2.69 @@ -809,15 +798,11 @@
    2.70      name_of_kind knd ^ "," ^ tptp_pack lits ^ ").\n";
    2.71  
    2.72  fun tptp_type_lits (Clause {literals, types_sorts, ...}) = 
    2.73 -    let val lits = map tptp_literal literals
    2.74 -	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
    2.75 -        val tvar_lits_strs =
    2.76 -            if !keep_types then map tptp_of_typeLit tvar_lits else []
    2.77 -	val tfree_lits =
    2.78 -	    if !keep_types then map tptp_of_typeLit tfree_lits else []
    2.79 -    in
    2.80 -	(tvar_lits_strs @ lits, tfree_lits)
    2.81 -    end; 
    2.82 +  let val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
    2.83 +  in
    2.84 +      (map tptp_of_typeLit tvar_lits @ map tptp_literal literals,
    2.85 +       map tptp_of_typeLit tfree_lits)
    2.86 +  end; 
    2.87  
    2.88  fun clause2tptp (cls as Clause {clause_id, axiom_name, kind, ...}) =
    2.89      let val (lits,tfree_lits) = tptp_type_lits cls