src/HOL/Tools/res_clause.ML
changeset 21790 9d2761d09d91
parent 21564 519ee3129ee1
child 21813 06a06f6d3166
     1.1 --- a/src/HOL/Tools/res_clause.ML	Tue Dec 12 12:03:46 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Dec 12 16:20:57 2006 +0100
     1.3 @@ -38,7 +38,6 @@
     1.4    val init : theory -> unit
     1.5    val isMeta : string -> bool
     1.6    val isTaut : clause -> bool
     1.7 -  val keep_types : bool ref
     1.8    val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order
     1.9    val make_axiom_clause : thm -> string * int -> clause option
    1.10    val make_conjecture_clauses : thm list -> clause list
    1.11 @@ -201,8 +200,6 @@
    1.12  
    1.13  (***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****)
    1.14  
    1.15 -val keep_types = ref true;
    1.16 -
    1.17  datatype kind = Axiom | Conjecture;
    1.18  fun name_of_kind Axiom = "axiom"
    1.19    | name_of_kind Conjecture = "negated_conjecture";
    1.20 @@ -274,7 +271,7 @@
    1.21  (*Declarations of the current theory--to allow suppressing types.*)
    1.22  val const_typargs = ref (Library.K [] : (string*typ -> typ list));
    1.23  
    1.24 -fun num_typargs(s,T) = if !keep_types then length (!const_typargs (s,T)) else 0;
    1.25 +fun num_typargs(s,T) = length (!const_typargs (s,T));
    1.26  
    1.27  (*Initialize the type suppression mechanism with the current theory before
    1.28      producing any clauses!*)
    1.29 @@ -633,10 +630,8 @@
    1.30  (**** String-oriented operations ****)
    1.31  
    1.32  fun string_of_term (UVar(x,_)) = x
    1.33 -  | string_of_term (Fun (name,typs,[])) = name ^ (paren_pack (map string_of_fol_type typs))
    1.34    | string_of_term (Fun (name,typs,terms)) = 
    1.35 -      let val typs' = if !keep_types then map string_of_fol_type typs else []
    1.36 -      in  name ^ (paren_pack (map string_of_term terms @ typs'))  end;
    1.37 +      name ^ (paren_pack (map string_of_term terms @ map string_of_fol_type typs));
    1.38  
    1.39  fun string_of_pair [t1,t2] = (string_of_term t1, string_of_term t2)
    1.40    | string_of_pair _ = raise ERROR ("equality predicate requires two arguments");
    1.41 @@ -648,8 +643,7 @@
    1.42  (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
    1.43  fun string_of_predicate (Predicate("equal",_,ts)) = string_of_equality ts
    1.44    | string_of_predicate (Predicate(name,typs,ts)) = 
    1.45 -      let val typs' = if !keep_types then map string_of_fol_type typs else []
    1.46 -      in  name ^ (paren_pack (map string_of_term ts @ typs'))  end;
    1.47 +      name ^ (paren_pack (map string_of_term ts @ map string_of_fol_type typs));
    1.48  
    1.49  fun string_of_clausename (cls_id,ax_name) = 
    1.50      clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
    1.51 @@ -685,14 +679,9 @@
    1.52      string_of_clausename (cls_id,ax_name) ^  ").\n\n";
    1.53  
    1.54  fun dfg_clause_aux (Clause{literals, types_sorts, ...}) = 
    1.55 -  let val lits = map dfg_literal literals
    1.56 -      val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
    1.57 -      val tvar_lits_strs = 
    1.58 -	  if !keep_types then map dfg_of_typeLit tvar_lits else []
    1.59 -      val tfree_lits =
    1.60 -          if !keep_types then map dfg_of_typeLit tfree_lits else []
    1.61 -  in
    1.62 -      (tvar_lits_strs @ lits, tfree_lits)
    1.63 +  let val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
    1.64 +  in  (map dfg_of_typeLit tvar_lits @ map dfg_literal literals, 
    1.65 +       map dfg_of_typeLit tfree_lits)
    1.66    end; 
    1.67  
    1.68  fun dfg_folterms (Literal(pol,pred)) = 
    1.69 @@ -809,15 +798,11 @@
    1.70      name_of_kind knd ^ "," ^ tptp_pack lits ^ ").\n";
    1.71  
    1.72  fun tptp_type_lits (Clause {literals, types_sorts, ...}) = 
    1.73 -    let val lits = map tptp_literal literals
    1.74 -	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
    1.75 -        val tvar_lits_strs =
    1.76 -            if !keep_types then map tptp_of_typeLit tvar_lits else []
    1.77 -	val tfree_lits =
    1.78 -	    if !keep_types then map tptp_of_typeLit tfree_lits else []
    1.79 -    in
    1.80 -	(tvar_lits_strs @ lits, tfree_lits)
    1.81 -    end; 
    1.82 +  let val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
    1.83 +  in
    1.84 +      (map tptp_of_typeLit tvar_lits @ map tptp_literal literals,
    1.85 +       map tptp_of_typeLit tfree_lits)
    1.86 +  end; 
    1.87  
    1.88  fun clause2tptp (cls as Clause {clause_id, axiom_name, kind, ...}) =
    1.89      let val (lits,tfree_lits) = tptp_type_lits cls