src/HOL/Tools/res_hol_clause.ML
changeset 22064 3d716cc9bd7a
parent 21858 05f57309170c
child 22078 5084f53cef39
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Fri Jan 12 15:37:21 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Sun Jan 14 09:57:29 2007 +0100
     1.3 @@ -25,9 +25,25 @@
     1.4    combinators appear to work best.*)
     1.5  val use_Turner = ref false;
     1.6  
     1.7 +(*If true, each function will be directly applied to as many arguments as possible, avoiding
     1.8 +  use of the "apply" operator. Use of hBOOL is also minimized.*)
     1.9 +val minimize_applies = ref false;
    1.10 +
    1.11  val const_typargs = ref (Library.K [] : (string*typ -> typ list));
    1.12  
    1.13 -fun init thy = (const_typargs := Sign.const_typargs thy);
    1.14 +val const_min_arity = ref (Symtab.empty : int Symtab.table);
    1.15 +
    1.16 +val const_needs_hBOOL = ref (Symtab.empty : bool Symtab.table);
    1.17 +
    1.18 +fun min_arity_of c = getOpt (Symtab.lookup(!const_min_arity) c, 0);
    1.19 +
    1.20 +fun needs_hBOOL c = not (!minimize_applies) orelse 
    1.21 +                    getOpt (Symtab.lookup(!const_needs_hBOOL) c, false);
    1.22 +
    1.23 +fun init thy = 
    1.24 +  (const_typargs := Sign.const_typargs thy; 
    1.25 +   const_min_arity := Symtab.empty; 
    1.26 +   const_needs_hBOOL := Symtab.empty);
    1.27  
    1.28  (**********************************************************************)
    1.29  (* convert a Term.term with lambdas into a Term.term with combinators *) 
    1.30 @@ -38,14 +54,11 @@
    1.31    | is_free (P $ Q) n = ((is_free P n) orelse (is_free Q n))
    1.32    | is_free _ _ = false;
    1.33  
    1.34 -
    1.35 -(*******************************************)
    1.36  fun mk_compact_comb (tm as (Const("ATP_Linkup.COMBB",_)$p) $ (Const("ATP_Linkup.COMBB",_)$q$r)) bnds =
    1.37        let val tp_p = Term.type_of1(bnds,p)
    1.38  	  val tp_q = Term.type_of1(bnds,q)
    1.39  	  val tp_r = Term.type_of1(bnds,r)
    1.40 -	  val typ = Term.type_of1(bnds,tm)
    1.41 -	  val typ_B' = [tp_p,tp_q,tp_r] ---> typ
    1.42 +	  val typ_B' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm)
    1.43        in
    1.44  	  Const("ATP_Linkup.COMBB'",typ_B') $ p $ q $ r
    1.45        end
    1.46 @@ -53,8 +66,7 @@
    1.47        let val tp_p = Term.type_of1(bnds,p)
    1.48  	  val tp_q = Term.type_of1(bnds,q)
    1.49  	  val tp_r = Term.type_of1(bnds,r)
    1.50 -	  val typ = Term.type_of1(bnds,tm)
    1.51 -	  val typ_C' = [tp_p,tp_q,tp_r] ---> typ
    1.52 +	  val typ_C' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm)
    1.53        in
    1.54  	  Const("ATP_Linkup.COMBC'",typ_C') $ p $ q $ r
    1.55        end
    1.56 @@ -62,8 +74,7 @@
    1.57        let val tp_p = Term.type_of1(bnds,p)
    1.58  	  val tp_q = Term.type_of1(bnds,q)
    1.59  	  val tp_r = Term.type_of1(bnds,r)
    1.60 -	  val typ = Term.type_of1(bnds,tm)
    1.61 -	  val typ_S' = [tp_p,tp_q,tp_r] ---> typ
    1.62 +	  val typ_S' = [tp_p,tp_q,tp_r] ---> Term.type_of1(bnds,tm)
    1.63        in
    1.64  	  Const("ATP_Linkup.COMBS'",typ_S') $ p $ q $ r
    1.65        end
    1.66 @@ -75,9 +86,7 @@
    1.67  fun lam2comb (Abs(x,tp,Bound 0)) _ = Const("ATP_Linkup.COMBI",tp-->tp) 
    1.68    | lam2comb (Abs(x,tp,Bound n)) bnds = 
    1.69        let val tb = List.nth(bnds,n-1)
    1.70 -      in
    1.71 -	  Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ Bound (n-1)
    1.72 -      end
    1.73 +      in  Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ Bound (n-1)  end
    1.74    | lam2comb (Abs(x,t1,Const(c,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Const(c,t2) 
    1.75    | lam2comb (Abs(x,t1,Free(v,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Free(v,t2)
    1.76    | lam2comb (Abs(x,t1,Var(ind,t2))) _ = Const("ATP_Linkup.COMBK", [t2,t1] ---> t2) $ Var(ind,t2)
    1.77 @@ -86,8 +95,7 @@
    1.78  	  let val tI = [t1] ---> t1
    1.79  	      val P' = lam2comb (Abs(x,t1,P)) bnds
    1.80  	      val tp' = Term.type_of1(bnds,P')
    1.81 -	      val tr = Term.type_of1(t1::bnds,P)
    1.82 -	      val tS = [tp',tI] ---> tr
    1.83 +	      val tS = [tp',tI] ---> Term.type_of1(t1::bnds,P)
    1.84  	  in
    1.85  	      compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ 
    1.86  	                     Const("ATP_Linkup.COMBI",tI)) bnds
    1.87 @@ -101,44 +109,32 @@
    1.88  	  if nfreeP andalso nfreeQ 
    1.89  	  then 
    1.90  	    let val tK = [tpq,t1] ---> tpq
    1.91 -		val PQ' = incr_boundvars ~1 (P $ Q)
    1.92 -	    in 
    1.93 -		Const("ATP_Linkup.COMBK",tK) $ PQ'
    1.94 -	    end
    1.95 +	    in  Const("ATP_Linkup.COMBK",tK) $ incr_boundvars ~1 (P $ Q)  end
    1.96  	  else if nfreeP then 
    1.97  	    let val Q' = lam2comb (Abs(x,t1,Q)) bnds
    1.98  		val P' = incr_boundvars ~1 P
    1.99  		val tp = Term.type_of1(bnds,P')
   1.100  		val tq' = Term.type_of1(bnds, Q')
   1.101  		val tB = [tp,tq',t1] ---> tpq
   1.102 -	    in
   1.103 -		compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') bnds 
   1.104 -	    end
   1.105 +	    in  compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') bnds  end
   1.106  	  else if nfreeQ then 
   1.107  	    let val P' = lam2comb (Abs(x,t1,P)) bnds
   1.108  		val Q' = incr_boundvars ~1 Q
   1.109  		val tq = Term.type_of1(bnds,Q')
   1.110  		val tp' = Term.type_of1(bnds, P')
   1.111  		val tC = [tp',tq,t1] ---> tpq
   1.112 -	    in
   1.113 -		compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') bnds
   1.114 -	    end
   1.115 +	    in  compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') bnds  end
   1.116            else
   1.117  	    let val P' = lam2comb (Abs(x,t1,P)) bnds
   1.118  		val Q' = lam2comb (Abs(x,t1,Q)) bnds 
   1.119  		val tp' = Term.type_of1(bnds,P')
   1.120  		val tq' = Term.type_of1(bnds,Q')
   1.121  		val tS = [tp',tq',t1] ---> tpq
   1.122 -	    in
   1.123 -		compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds
   1.124 -	    end
   1.125 +	    in  compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds  end
   1.126        end
   1.127    | lam2comb (t as (Abs(x,t1,_))) _ = raise ResClause.CLAUSE("HOL CLAUSE",t);
   1.128  
   1.129 -(*********************)
   1.130 -
   1.131 -fun to_comb (Abs(x,tp,b)) bnds =
   1.132 -      lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds 
   1.133 +fun to_comb (Abs(x,tp,b)) bnds = lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds 
   1.134    | to_comb (P $ Q) bnds = (to_comb P bnds) $ (to_comb Q bnds)
   1.135    | to_comb t _ = t;
   1.136  
   1.137 @@ -328,13 +324,17 @@
   1.138  
   1.139  val app_str = "hAPP";
   1.140  
   1.141 -val bool_str = "hBOOL";
   1.142 -
   1.143  fun type_of_combterm (CombConst(c,tp,_)) = tp
   1.144    | type_of_combterm (CombFree(v,tp)) = tp
   1.145    | type_of_combterm (CombVar(v,tp)) = tp
   1.146    | type_of_combterm (CombApp(t1,t2,tp)) = tp;
   1.147  
   1.148 +(*gets the head of a combinator application, along with the list of arguments*)
   1.149 +fun strip_comb u =
   1.150 +    let fun stripc (CombApp(t,u,_), ts) = stripc (t, u::ts)
   1.151 +        |   stripc  x =  x
   1.152 +    in  stripc(u,[])  end;
   1.153 +
   1.154  fun string_of_combterm1 (CombConst(c,tp,_)) = 
   1.155        let val c' = if c = "equal" then "c_fequal" else c
   1.156        in  wrap_type (c',tp)  end
   1.157 @@ -355,25 +355,48 @@
   1.158  	    | T_CONST => raise ERROR "string_of_combterm1"
   1.159        end;
   1.160  
   1.161 -fun string_of_combterm2 (CombConst(c,tp,tvars)) = 
   1.162 -      let val tvars' = map ResClause.string_of_fol_type tvars
   1.163 -	  val c' = if c = "equal" then "c_fequal" else c
   1.164 +fun rev_apply (v, []) = v
   1.165 +  | rev_apply (v, arg::args) = app_str ^ ResClause.paren_pack [rev_apply (v, args), arg];
   1.166 +
   1.167 +fun string_apply (v, args) = rev_apply (v, rev args);
   1.168 +
   1.169 +(*Apply an operator to the argument strings, using either the "apply" operator or
   1.170 +  direct function application.*)
   1.171 +fun string_of_applic (CombConst(c,tp,tvars), args) =
   1.172 +      let val c = if c = "equal" then "c_fequal" else c
   1.173 +          val nargs = min_arity_of c
   1.174 +          val args1 = List.take(args, nargs) @ (map ResClause.string_of_fol_type tvars)
   1.175 +            handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^
   1.176 +					     Int.toString nargs ^ " but is applied to " ^ 
   1.177 +					     space_implode ", " args) 
   1.178 +          val args2 = List.drop(args, nargs)
   1.179        in
   1.180 -	  c' ^ ResClause.paren_pack tvars'
   1.181 +	  string_apply (c ^ ResClause.paren_pack args1, args2)
   1.182        end
   1.183 -  | string_of_combterm2 (CombFree(v,tp)) = v
   1.184 -  | string_of_combterm2 (CombVar(v,tp)) = v
   1.185 -  | string_of_combterm2 (CombApp(t1,t2,_)) =
   1.186 -      app_str ^ ResClause.paren_pack [string_of_combterm2 t1, string_of_combterm2 t2];
   1.187 +  | string_of_applic (CombFree(v,tp), args) = string_apply (v, args)
   1.188 +  | string_of_applic (CombVar(v,tp), args) = string_apply (v, args)  
   1.189 +  | string_of_applic _ = raise ERROR "string_of_applic";
   1.190 +
   1.191 +fun string_of_combterm2 t = 
   1.192 +  let val (head, args) = strip_comb t
   1.193 +  in  string_of_applic (head, map string_of_combterm2 args)  end;
   1.194  
   1.195  fun string_of_combterm t = 
   1.196      case !typ_level of T_CONST => string_of_combterm2 t
   1.197  		           | _ => string_of_combterm1 t;
   1.198 -		           
   1.199 -fun string_of_predicate (CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_)) =
   1.200 -      ("equal" ^ ResClause.paren_pack [string_of_combterm t1, string_of_combterm t2])
   1.201 -  | string_of_predicate t = 
   1.202 -      bool_str ^ ResClause.paren_pack [string_of_combterm t]
   1.203 +
   1.204 +(*Boolean-valued terms are here converted to literals.*)
   1.205 +fun boolify t = "hBOOL" ^ ResClause.paren_pack [string_of_combterm t];
   1.206 +
   1.207 +fun string_of_predicate t = 
   1.208 +  case t of
   1.209 +      (CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_)) =>
   1.210 +	  (*DFG only: new TPTP prefers infix equality*)
   1.211 +	  ("equal" ^ ResClause.paren_pack [string_of_combterm t1, string_of_combterm t2])
   1.212 +    | _ => 
   1.213 +          case #1 (strip_comb t) of
   1.214 +              CombConst(c,_,_) => if needs_hBOOL c then boolify t else string_of_combterm t
   1.215 +            | _ => boolify t;
   1.216  
   1.217  fun string_of_clausename (cls_id,ax_name) = 
   1.218      ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   1.219 @@ -393,6 +416,8 @@
   1.220    | tptp_literal (Literal(pol,pred)) = 
   1.221        ResClause.tptp_sign pol (string_of_predicate pred);
   1.222   
   1.223 +(*Given a clause, returns its literals paired with a list of literals concerning TFrees;
   1.224 +  the latter should only occur in conjecture clauses.*)
   1.225  fun tptp_type_lits (Clause cls) = 
   1.226      let val lits = map tptp_literal (#literals cls)
   1.227  	val ctvar_lits_strs =
   1.228 @@ -405,7 +430,6 @@
   1.229  	(ctvar_lits_strs @ lits, ctfree_lits)
   1.230      end; 
   1.231      
   1.232 -    
   1.233  fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   1.234      let val (lits,ctfree_lits) = tptp_type_lits cls
   1.235  	val cls_str = ResClause.gen_tptp_cls(clause_id,axiom_name,kind,lits)
   1.236 @@ -449,35 +473,43 @@
   1.237  	val cls_str = ResClause.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) 
   1.238      in (cls_str, tfree_lits) end;
   1.239  
   1.240 +(** For DFG format: accumulate function and predicate declarations **)
   1.241  
   1.242 -fun init_funcs_tab funcs = 
   1.243 -    let val funcs1 = case !typ_level of T_PARTIAL => Symtab.update ("hAPP",3) funcs
   1.244 -				      | _ => Symtab.update ("hAPP",2) funcs
   1.245 -    in
   1.246 -	Symtab.update ("typeinfo",2) funcs1
   1.247 -    end;
   1.248 +fun addtypes tvars tab = foldl ResClause.add_foltype_funcs tab tvars;
   1.249  
   1.250 -
   1.251 -fun add_funcs (CombConst(c,_,tvars),funcs) =
   1.252 -      if c = "equal" then foldl ResClause.add_foltype_funcs funcs tvars
   1.253 +fun add_decls (CombConst(c,_,tvars), (funcs,preds)) =
   1.254 +      if c = "equal" then (addtypes tvars funcs, preds)
   1.255        else
   1.256  	(case !typ_level of
   1.257 -	     T_CONST => foldl ResClause.add_foltype_funcs (Symtab.update(c,length tvars) funcs) tvars
   1.258 -           | _ => foldl ResClause.add_foltype_funcs (Symtab.update(c,0) funcs) tvars)
   1.259 -  | add_funcs (CombFree(v,ctp),funcs) = ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs) 
   1.260 -  | add_funcs (CombVar(_,ctp),funcs) = ResClause.add_foltype_funcs (ctp,funcs)
   1.261 -  | add_funcs (CombApp(P,Q,_),funcs) = add_funcs(P,add_funcs (Q,funcs));
   1.262 +	     T_CONST => 
   1.263 +               let val arity = min_arity_of c + length tvars
   1.264 +                   val addit = Symtab.update(c,arity) 
   1.265 +               in
   1.266 +                   if needs_hBOOL c then (addtypes tvars (addit funcs), preds)
   1.267 +                   else (addtypes tvars funcs, addit preds)
   1.268 +               end
   1.269 +           | _ => (addtypes tvars (Symtab.update(c,0) funcs), preds))
   1.270 +  | add_decls (CombFree(v,ctp), (funcs,preds)) = 
   1.271 +      (ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs), preds)
   1.272 +  | add_decls (CombVar(_,ctp), (funcs,preds)) = 
   1.273 +      (ResClause.add_foltype_funcs (ctp,funcs), preds)
   1.274 +  | add_decls (CombApp(P,Q,_),decls) = add_decls(P,add_decls (Q,decls));
   1.275  
   1.276 -fun add_literal_funcs (Literal(_,c), funcs) = add_funcs (c,funcs);
   1.277 +fun add_literal_decls (Literal(_,c), decls) = add_decls (c,decls);
   1.278  
   1.279 -fun add_clause_funcs (Clause {literals, ...}, funcs) =
   1.280 -    foldl add_literal_funcs funcs literals
   1.281 +fun add_clause_decls (Clause {literals, ...}, decls) =
   1.282 +    foldl add_literal_decls decls literals
   1.283      handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
   1.284  
   1.285 -fun funcs_of_clauses clauses arity_clauses =
   1.286 -    Symtab.dest (foldl ResClause.add_arityClause_funcs 
   1.287 -                       (foldl add_clause_funcs (init_funcs_tab Symtab.empty) clauses)
   1.288 -                       arity_clauses)
   1.289 +fun decls_of_clauses clauses arity_clauses =
   1.290 +  let val happ_ar = case !typ_level of T_PARTIAL => 3 | _ => 2
   1.291 +      val init_functab = Symtab.update ("typeinfo",2) (Symtab.update ("hAPP",happ_ar) Symtab.empty)
   1.292 +      val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
   1.293 +      val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses)
   1.294 +  in
   1.295 +      (Symtab.dest (foldl ResClause.add_arityClause_funcs functab arity_clauses), 
   1.296 +       Symtab.dest predtab)
   1.297 +  end;
   1.298  
   1.299  fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
   1.300    foldl ResClause.add_type_sort_preds preds ctypes_sorts
   1.301 @@ -488,8 +520,7 @@
   1.302      Symtab.dest
   1.303  	(foldl ResClause.add_classrelClause_preds 
   1.304  	       (foldl ResClause.add_arityClause_preds
   1.305 -		      (Symtab.update ("hBOOL",1) 
   1.306 -		        (foldl add_clause_preds Symtab.empty clauses))
   1.307 +		      (foldl add_clause_preds Symtab.empty clauses) 
   1.308  		      arity_clauses)
   1.309  	       clsrel_clauses)
   1.310  
   1.311 @@ -523,8 +554,10 @@
   1.312  
   1.313  val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
   1.314  
   1.315 -fun get_helper_clauses ct =
   1.316 -    let fun needed c = valOf (Symtab.lookup ct c) > 0
   1.317 +fun get_helper_clauses (conjectures, axclauses, user_lemmas) =
   1.318 +    let val ct0 = foldl count_clause init_counters conjectures
   1.319 +        val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
   1.320 +        fun needed c = valOf (Symtab.lookup ct c) > 0
   1.321          val IK = if needed "c_COMBI" orelse needed "c_COMBK" 
   1.322                   then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) 
   1.323                   else []
   1.324 @@ -542,24 +575,57 @@
   1.325  	         else []
   1.326  	val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
   1.327      in
   1.328 -	make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S')
   1.329 +	map #2 (make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S'))
   1.330      end
   1.331  
   1.332 +(*Find the minimal arity of each function mentioned in the term. Also, note which uses
   1.333 +  are not at top level, to see if hBOOL is needed.*)
   1.334 +fun count_constants_term toplev t =
   1.335 +  let val (head, args) = strip_comb t
   1.336 +      val n = length args
   1.337 +      val _ = List.app (count_constants_term false) args
   1.338 +  in
   1.339 +      case head of
   1.340 +	  CombConst (a,_,_) => (*predicate or function version of "equal"?*)
   1.341 +	    let val a = if a="equal" andalso not toplev then "c_fequal" else a
   1.342 +	    in  
   1.343 +	      const_min_arity := Symtab.map_default (a,n) (curry Int.min n) (!const_min_arity);
   1.344 +	      if toplev then ()
   1.345 +	      else const_needs_hBOOL := Symtab.update (a,true) (!const_needs_hBOOL)
   1.346 +	    end
   1.347 +	| ts => ()
   1.348 +  end;
   1.349 +
   1.350 +(*A literal is a top-level term*)
   1.351 +fun count_constants_lit (Literal (_,t)) = count_constants_term true t;
   1.352 +
   1.353 +fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals;
   1.354 +
   1.355 +fun display_arity (c,n) =
   1.356 +  Output.debug ("Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ 
   1.357 +                (if needs_hBOOL c then " needs hBOOL" else ""));
   1.358 +
   1.359 +fun count_constants (conjectures, axclauses, helper_clauses) = 
   1.360 +  if !minimize_applies then
   1.361 +    (List.app count_constants_clause conjectures;
   1.362 +     List.app count_constants_clause axclauses;
   1.363 +     List.app count_constants_clause helper_clauses;
   1.364 +     List.app display_arity (Symtab.dest (!const_min_arity)))
   1.365 +  else ();
   1.366 +
   1.367  (* tptp format *)
   1.368  						  
   1.369  (* write TPTP format to a single file *)
   1.370 -fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas =
   1.371 +fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   1.372      let val conjectures = make_conjecture_clauses thms
   1.373 -        val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses)
   1.374 +        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   1.375 +	val helper_clauses = get_helper_clauses (conjectures, axclauses, user_lemmas)
   1.376 +	val _ = count_constants (conjectures, axclauses, helper_clauses);
   1.377  	val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
   1.378  	val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   1.379 -	val out = TextIO.openOut filename
   1.380 -	val ct = foldl (count_user_clause user_lemmas) 
   1.381 -	            (foldl count_clause init_counters conjectures)
   1.382 -	            axclauses'
   1.383 -	val helper_clauses = map #2 (get_helper_clauses ct)
   1.384 +        val out = TextIO.openOut filename
   1.385      in
   1.386 -	List.app (curry TextIO.output out o #1 o clause2tptp) axclauses';
   1.387 +	List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
   1.388  	ResClause.writeln_strs out tfree_clss;
   1.389  	ResClause.writeln_strs out tptp_clss;
   1.390  	List.app (curry TextIO.output out o ResClause.tptp_classrelClause) classrel_clauses;
   1.391 @@ -573,26 +639,25 @@
   1.392  
   1.393  (* dfg format *)
   1.394  
   1.395 -fun dfg_write_file  thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas =
   1.396 -    let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) 
   1.397 -	val conjectures = make_conjecture_clauses thms
   1.398 -        val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses)
   1.399 +fun dfg_write_file  thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   1.400 +    let val conjectures = make_conjecture_clauses thms
   1.401 +        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   1.402 +	val helper_clauses = get_helper_clauses (conjectures, axclauses, user_lemmas)
   1.403 +	val _ = count_constants (conjectures, axclauses, helper_clauses);
   1.404  	val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   1.405  	and probname = Path.implode (Path.base (Path.explode filename))
   1.406 -	val axstrs = map (#1 o clause2dfg) axclauses'
   1.407 +	val axstrs = map (#1 o clause2dfg) axclauses
   1.408  	val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss)
   1.409  	val out = TextIO.openOut filename
   1.410 -	val ct = foldl (count_user_clause user_lemmas) 
   1.411 -	            (foldl count_clause init_counters conjectures)
   1.412 -	            axclauses'
   1.413 -	val helper_clauses = map #2 (get_helper_clauses ct)
   1.414  	val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses
   1.415 -	val funcs = funcs_of_clauses (helper_clauses @ conjectures @ axclauses') arity_clauses
   1.416 -	and preds = preds_of_clauses axclauses' classrel_clauses arity_clauses
   1.417 +	val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses
   1.418 +	and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   1.419      in
   1.420  	TextIO.output (out, ResClause.string_of_start probname); 
   1.421  	TextIO.output (out, ResClause.string_of_descrip probname); 
   1.422 -	TextIO.output (out, ResClause.string_of_symbols (ResClause.string_of_funcs funcs) (ResClause.string_of_preds preds)); 
   1.423 +	TextIO.output (out, ResClause.string_of_symbols 
   1.424 +	                      (ResClause.string_of_funcs funcs) 
   1.425 +	                      (ResClause.string_of_preds (cl_preds @ ty_preds))); 
   1.426  	TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
   1.427  	ResClause.writeln_strs out axstrs;
   1.428  	List.app (curry TextIO.output out o ResClause.dfg_classrelClause) classrel_clauses;