src/HOL/Tools/res_hol_clause.ML

-(* ID: $Id$
+(*
    Author: Jia Meng, NICTA
 
 FOL clauses translated from HOL formulae.
 *)
 

   val comb_K: thm
   val comb_B: thm
   val comb_C: thm
   val comb_S: thm
   datatype type_level = T_FULL | T_CONST
-  val typ_level: type_level ref
-  val minimize_applies: bool ref
+  val typ_level: type_level
+  val minimize_applies: bool
   type axiom_name = string
   type polarity = bool
   type clause_id = int
   datatype combterm =
       CombConst of string * ResClause.fol_type * ResClause.fol_type list (*Const and Free*)

 
 
 (*The different translations of types*)
 datatype type_level = T_FULL | T_CONST;
 
-val typ_level = ref T_CONST;
+val typ_level = T_CONST;
 
 (*If true, each function will be directly applied to as many arguments as possible, avoiding
   use of the "apply" operator. Use of hBOOL is also minimized.*)
-val minimize_applies = ref true;
-
-val const_min_arity = ref (Symtab.empty : int Symtab.table);
-
-val const_needs_hBOOL = ref (Symtab.empty : bool Symtab.table);
-
-fun min_arity_of c = getOpt (Symtab.lookup(!const_min_arity) c, 0);
+val minimize_applies = true;
+
+fun min_arity_of const_min_arity c = getOpt (Symtab.lookup const_min_arity c, 0);
 
 (*True if the constant ever appears outside of the top-level position in literals.
   If false, the constant always receives all of its arguments and is used as a predicate.*)
-fun needs_hBOOL c = not (!minimize_applies) orelse
-                    getOpt (Symtab.lookup(!const_needs_hBOOL) c, false);
+fun needs_hBOOL const_needs_hBOOL c = not minimize_applies orelse
+                    getOpt (Symtab.lookup const_needs_hBOOL c, false);
 
 
 (******************************************************)
 (* data types for typed combinator expressions        *)
 (******************************************************)

       (not pol andalso c = "c_False")
   | isTrue _ = false;
 
 fun isTaut (Clause {literals,...}) = exists isTrue literals;
 
-fun type_of (Type (a, Ts)) =
-      let val (folTypes,ts) = types_of Ts
-      in  (RC.Comp(RC.make_fixed_type_const a, folTypes), ts)  end
-  | type_of (tp as (TFree(a,s))) =
+fun type_of dfg (Type (a, Ts)) =
+      let val (folTypes,ts) = types_of dfg Ts
+      in  (RC.Comp(RC.make_fixed_type_const dfg a, folTypes), ts)  end
+  | type_of dfg (tp as (TFree(a,s))) =
       (RC.AtomF (RC.make_fixed_type_var a), [tp])
-  | type_of (tp as (TVar(v,s))) =
+  | type_of dfg (tp as (TVar(v,s))) =
       (RC.AtomV (RC.make_schematic_type_var v), [tp])
-and types_of Ts =
-      let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
+and types_of dfg Ts =
+      let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
       in  (folTyps, RC.union_all ts)  end;
 
 (* same as above, but no gathering of sort information *)
-fun simp_type_of (Type (a, Ts)) =
-      RC.Comp(RC.make_fixed_type_const a, map simp_type_of Ts)
-  | simp_type_of (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a)
-  | simp_type_of (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v);
-
-
-fun const_type_of thy (c,t) =
-      let val (tp,ts) = type_of t
-      in  (tp, ts, map simp_type_of (Sign.const_typargs thy (c,t))) end;
+fun simp_type_of dfg (Type (a, Ts)) =
+      RC.Comp(RC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
+  | simp_type_of dfg (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a)
+  | simp_type_of dfg (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v);
+
+
+fun const_type_of dfg thy (c,t) =
+      let val (tp,ts) = type_of dfg t
+      in  (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end;
 
 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
-fun combterm_of thy (Const(c,t)) =
-      let val (tp,ts,tvar_list) = const_type_of thy (c,t)
-          val c' = CombConst(RC.make_fixed_const c, tp, tvar_list)
+fun combterm_of dfg thy (Const(c,t)) =
+      let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
+          val c' = CombConst(RC.make_fixed_const dfg c, tp, tvar_list)
       in  (c',ts)  end
-  | combterm_of thy (Free(v,t)) =
-      let val (tp,ts) = type_of t
+  | combterm_of dfg thy (Free(v,t)) =
+      let val (tp,ts) = type_of dfg t
           val v' = CombConst(RC.make_fixed_var v, tp, [])
       in  (v',ts)  end
-  | combterm_of thy (Var(v,t)) =
-      let val (tp,ts) = type_of t
+  | combterm_of dfg thy (Var(v,t)) =
+      let val (tp,ts) = type_of dfg t
           val v' = CombVar(RC.make_schematic_var v,tp)
       in  (v',ts)  end
-  | combterm_of thy (P $ Q) =
-      let val (P',tsP) = combterm_of thy P
-          val (Q',tsQ) = combterm_of thy Q
+  | combterm_of dfg thy (P $ Q) =
+      let val (P',tsP) = combterm_of dfg thy P
+          val (Q',tsQ) = combterm_of dfg thy Q
       in  (CombApp(P',Q'), tsP union tsQ)  end
-  | combterm_of thy (t as Abs _) = raise RC.CLAUSE("HOL CLAUSE",t);
-
-fun predicate_of thy ((Const("Not",_) $ P), polarity) = predicate_of thy (P, not polarity)
-  | predicate_of thy (t,polarity) = (combterm_of thy (Envir.eta_contract t), polarity);
-
-fun literals_of_term1 thy args (Const("Trueprop",_) $ P) = literals_of_term1 thy args P
-  | literals_of_term1 thy args (Const("op |",_) $ P $ Q) =
-      literals_of_term1 thy (literals_of_term1 thy args P) Q
-  | literals_of_term1 thy (lits,ts) P =
-      let val ((pred,ts'),pol) = predicate_of thy (P,true)
+  | combterm_of _ thy (t as Abs _) = raise RC.CLAUSE("HOL CLAUSE",t);
+
+fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
+  | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
+
+fun literals_of_term1 dfg thy args (Const("Trueprop",_) $ P) = literals_of_term1 dfg thy args P
+  | literals_of_term1 dfg thy args (Const("op |",_) $ P $ Q) =
+      literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
+  | literals_of_term1 dfg thy (lits,ts) P =
+      let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
       in
           (Literal(pol,pred)::lits, ts union ts')
       end;
 
-fun literals_of_term thy P = literals_of_term1 thy ([],[]) P;
+fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
+val literals_of_term = literals_of_term_dfg false;
 
 (* Problem too trivial for resolution (empty clause) *)
 exception TOO_TRIVIAL;
 
 (* making axiom and conjecture clauses *)
-fun make_clause thy (clause_id,axiom_name,kind,th) =
-    let val (lits,ctypes_sorts) = literals_of_term thy (prop_of th)
+fun make_clause dfg thy (clause_id,axiom_name,kind,th) =
+    let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
     in
         if forall isFalse lits
         then raise TOO_TRIVIAL
         else
             Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
                     literals = lits, ctypes_sorts = ctypes_sorts}
     end;
 
 
-fun add_axiom_clause thy ((th,(name,id)), pairs) =
-  let val cls = make_clause thy (id, name, RC.Axiom, th)
+fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
+  let val cls = make_clause dfg thy (id, name, RC.Axiom, th)
   in
       if isTaut cls then pairs else (name,cls)::pairs
   end;
 
-fun make_axiom_clauses thy = foldl (add_axiom_clause thy) [];
-
-fun make_conjecture_clauses_aux _ _ [] = []
-  | make_conjecture_clauses_aux thy n (th::ths) =
-      make_clause thy (n,"conjecture", RC.Conjecture, th) ::
-      make_conjecture_clauses_aux thy (n+1) ths;
-
-fun make_conjecture_clauses thy = make_conjecture_clauses_aux thy 0;
+fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) [];
+
+fun make_conjecture_clauses_aux dfg _ _ [] = []
+  | make_conjecture_clauses_aux dfg thy n (th::ths) =
+      make_clause dfg thy (n,"conjecture", RC.Conjecture, th) ::
+      make_conjecture_clauses_aux dfg thy (n+1) ths;
+
+fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
 
 
 (**********************************************************************)
 (* convert clause into ATP specific formats:                          *)
 (* TPTP used by Vampire and E                                         *)

         |   stripc  x =  x
     in  stripc(u,[])  end;
 
 val type_wrapper = "ti";
 
-fun head_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL c
-  | head_needs_hBOOL _ = true;
+fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
+  | head_needs_hBOOL const_needs_hBOOL _ = true;
 
 fun wrap_type (s, tp) =
-  if !typ_level=T_FULL then
+  if typ_level=T_FULL then
       type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp]
   else s;
 
 fun apply ss = "hAPP" ^ RC.paren_pack ss;
 

 
 fun string_apply (v, args) = rev_apply (v, rev args);
 
 (*Apply an operator to the argument strings, using either the "apply" operator or
   direct function application.*)
-fun string_of_applic (CombConst(c,tp,tvars), args) =
+fun string_of_applic cma (CombConst(c,tp,tvars), args) =
       let val c = if c = "equal" then "c_fequal" else c
-          val nargs = min_arity_of c
+          val nargs = min_arity_of cma c
           val args1 = List.take(args, nargs)
             handle Subscript => error ("string_of_applic: " ^ c ^ " has arity " ^
                                          Int.toString nargs ^ " but is applied to " ^
                                          space_implode ", " args)
           val args2 = List.drop(args, nargs)
-          val targs = if !typ_level = T_CONST then map RC.string_of_fol_type tvars
+          val targs = if typ_level = T_CONST then map RC.string_of_fol_type tvars
                       else []
       in
           string_apply (c ^ RC.paren_pack (args1@targs), args2)
       end
-  | string_of_applic (CombVar(v,tp), args) = string_apply (v, args)
-  | string_of_applic _ = error "string_of_applic";
-
-fun wrap_type_if (head, s, tp) = if head_needs_hBOOL head then wrap_type (s, tp) else s;
-
-fun string_of_combterm t =
+  | string_of_applic cma (CombVar(v,tp), args) = string_apply (v, args)
+  | string_of_applic _ _ = error "string_of_applic";
+
+fun wrap_type_if cnh (head, s, tp) = if head_needs_hBOOL cnh head then wrap_type (s, tp) else s;
+
+fun string_of_combterm cma cnh t =
   let val (head, args) = strip_comb t
-  in  wrap_type_if (head,
-                    string_of_applic (head, map string_of_combterm args),
+  in  wrap_type_if cnh (head,
+                    string_of_applic cma (head, map (string_of_combterm cma cnh) args),
                     type_of_combterm t)
   end;
 
 (*Boolean-valued terms are here converted to literals.*)
-fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t];
-
-fun string_of_predicate t =
+fun boolify cma cnh t = "hBOOL" ^ RC.paren_pack [string_of_combterm cma cnh t];
+
+fun string_of_predicate cma cnh t =
   case t of
       (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
           (*DFG only: new TPTP prefers infix equality*)
-          ("equal" ^ RC.paren_pack [string_of_combterm t1, string_of_combterm t2])
+          ("equal" ^ RC.paren_pack [string_of_combterm cma cnh t1, string_of_combterm cma cnh t2])
     | _ =>
           case #1 (strip_comb t) of
-              CombConst(c,_,_) => if needs_hBOOL c then boolify t else string_of_combterm t
-            | _ => boolify t;
+              CombConst(c,_,_) => if needs_hBOOL cnh c then boolify cma cnh t else string_of_combterm cma cnh t
+            | _ => boolify cma cnh t;
 
 fun string_of_clausename (cls_id,ax_name) =
     RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
 
 fun string_of_type_clsname (cls_id,ax_name,idx) =
     string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
 
 
 (*** tptp format ***)
 
-fun tptp_of_equality pol (t1,t2) =
+fun tptp_of_equality cma cnh pol (t1,t2) =
   let val eqop = if pol then " = " else " != "
-  in  string_of_combterm t1 ^ eqop ^ string_of_combterm t2  end;
-
-fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
-      tptp_of_equality pol (t1,t2)
-  | tptp_literal (Literal(pol,pred)) =
-      RC.tptp_sign pol (string_of_predicate pred);
+  in  string_of_combterm cma cnh t1 ^ eqop ^ string_of_combterm cma cnh t2  end;
+
+fun tptp_literal cma cnh (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
+      tptp_of_equality cma cnh pol (t1,t2)
+  | tptp_literal cma cnh (Literal(pol,pred)) =
+      RC.tptp_sign pol (string_of_predicate cma cnh pred);
 
 (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
   the latter should only occur in conjecture clauses.*)
-fun tptp_type_lits pos (Clause{literals, ctypes_sorts, ...}) =
-      (map tptp_literal literals, 
+fun tptp_type_lits cma cnh pos (Clause{literals, ctypes_sorts, ...}) =
+      (map (tptp_literal cma cnh) literals, 
        map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
 
-fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
-  let val (lits,tylits) = tptp_type_lits (kind = RC.Conjecture) cls
+fun clause2tptp cma cnh (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
+  let val (lits,tylits) = tptp_type_lits cma cnh (kind = RC.Conjecture) cls
   in
       (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
   end;
 
 
 (*** dfg format ***)
 
-fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred);
-
-fun dfg_type_lits pos (Clause{literals, ctypes_sorts, ...}) =
-      (map dfg_literal literals, 
+fun dfg_literal cma cnh (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate cma cnh pred);
+
+fun dfg_type_lits cma cnh pos (Clause{literals, ctypes_sorts, ...}) =
+      (map (dfg_literal cma cnh) literals, 
        map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts));
 
 fun get_uvars (CombConst _) vars = vars
   | get_uvars (CombVar(v,_)) vars = (v::vars)
   | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars);
 
 fun get_uvars_l (Literal(_,c)) = get_uvars c [];
 
 fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
 
-fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
-  let val (lits,tylits) = dfg_type_lits (kind = RC.Conjecture) cls
+fun clause2dfg cma cnh (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
+  let val (lits,tylits) = dfg_type_lits cma cnh (kind = RC.Conjecture) cls
       val vars = dfg_vars cls
       val tvars = RC.get_tvar_strs ctypes_sorts
   in
       (RC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
   end;
 
 
 (** For DFG format: accumulate function and predicate declarations **)
 
-fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars;
-
-fun add_decls (CombConst(c,tp,tvars), (funcs,preds)) =
+fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars;
+
+fun add_decls cma cnh (CombConst(c,tp,tvars), (funcs,preds)) =
       if c = "equal" then (addtypes tvars funcs, preds)
       else
-	let val arity = min_arity_of c
-	    val ntys = if !typ_level = T_CONST then length tvars else 0
+	let val arity = min_arity_of cma c
+	    val ntys = if typ_level = T_CONST then length tvars else 0
 	    val addit = Symtab.update(c, arity+ntys)
 	in
-	    if needs_hBOOL c then (addtypes tvars (addit funcs), preds)
+	    if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
 	    else (addtypes tvars funcs, addit preds)
 	end
-  | add_decls (CombVar(_,ctp), (funcs,preds)) =
+  | add_decls _ _ (CombVar(_,ctp), (funcs,preds)) =
       (RC.add_foltype_funcs (ctp,funcs), preds)
-  | add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls));
-
-fun add_literal_decls (Literal(_,c), decls) = add_decls (c,decls);
-
-fun add_clause_decls (Clause {literals, ...}, decls) =
-    foldl add_literal_decls decls literals
+  | add_decls cma cnh (CombApp(P,Q),decls) = add_decls cma cnh (P,add_decls cma cnh (Q,decls));
+
+fun add_literal_decls cma cnh (Literal(_,c), decls) = add_decls cma cnh (c,decls);
+
+fun add_clause_decls cma cnh (Clause {literals, ...}, decls) =
+    List.foldl (add_literal_decls cma cnh) decls literals
     handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
 
-fun decls_of_clauses clauses arity_clauses =
+fun decls_of_clauses cma cnh clauses arity_clauses =
   let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
       val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
-      val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses)
+      val (functab,predtab) = (List.foldl (add_clause_decls cma cnh) (init_functab, init_predtab) clauses)
   in
-      (Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses),
+      (Symtab.dest (List.foldl RC.add_arityClause_funcs functab arity_clauses),
        Symtab.dest predtab)
   end;
 
 fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
-  foldl RC.add_type_sort_preds preds ctypes_sorts
+  List.foldl RC.add_type_sort_preds preds ctypes_sorts
   handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
 
 (*Higher-order clauses have only the predicates hBOOL and type classes.*)
 fun preds_of_clauses clauses clsrel_clauses arity_clauses =
     Symtab.dest
-        (foldl RC.add_classrelClause_preds
-               (foldl RC.add_arityClause_preds
-                      (foldl add_clause_preds Symtab.empty clauses)
+        (List.foldl RC.add_classrelClause_preds
+               (List.foldl RC.add_arityClause_preds
+                      (List.foldl add_clause_preds Symtab.empty clauses)
                       arity_clauses)
                clsrel_clauses)
 
 
 (**********************************************************************)

   | count_combterm (CombVar(v,tp), ct) = ct
   | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
 
 fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
 
-fun count_clause (Clause{literals,...}, ct) = foldl count_literal ct literals;
+fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals;
 
 fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
-  if axiom_name mem_string user_lemmas then foldl count_literal ct literals
+  if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
   else ct;
 
 fun cnf_helper_thms thy =
   ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
 
-fun get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) =
+fun get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas) =
   if isFO then []  (*first-order*)
   else
-    let val ct0 = foldl count_clause init_counters conjectures
-        val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
+    let val ct0 = List.foldl count_clause init_counters conjectures
+        val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
         fun needed c = valOf (Symtab.lookup ct c) > 0
         val IK = if needed "c_COMBI" orelse needed "c_COMBK"
                  then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K])
                  else []
         val BC = if needed "c_COMBB" orelse needed "c_COMBC"

         val S = if needed "c_COMBS"
                 then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
                 else []
         val other = cnf_helper_thms thy [ext,fequal_imp_equal,equal_imp_fequal]
     in
-        map #2 (make_axiom_clauses thy (other @ IK @ BC @ S))
+        map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
     end;
 
 (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   are not at top level, to see if hBOOL is needed.*)
-fun count_constants_term toplev t =
+fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
   let val (head, args) = strip_comb t
       val n = length args
-      val _ = List.app (count_constants_term false) args
+      val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
   in
       case head of
           CombConst (a,_,_) => (*predicate or function version of "equal"?*)
             let val a = if a="equal" andalso not toplev then "c_fequal" else a
+            val const_min_arity = Symtab.map_default (a,n) (curry Int.min n) const_min_arity
             in
-              const_min_arity := Symtab.map_default (a,n) (curry Int.min n) (!const_min_arity);
-              if toplev then ()
-              else const_needs_hBOOL := Symtab.update (a,true) (!const_needs_hBOOL)
+              if toplev then (const_min_arity, const_needs_hBOOL)
+              else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL))
             end
-        | ts => ()
+        | ts => (const_min_arity, const_needs_hBOOL)
   end;
 
 (*A literal is a top-level term*)
-fun count_constants_lit (Literal (_,t)) = count_constants_term true t;
-
-fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals;
-
-fun display_arity (c,n) =
+fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
+  count_constants_term true t (const_min_arity, const_needs_hBOOL);
+
+fun count_constants_clause (Clause{literals,...}) (const_min_arity, const_needs_hBOOL) =
+  fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
+
+fun display_arity const_needs_hBOOL (c,n) =
   Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
-                (if needs_hBOOL c then " needs hBOOL" else ""));
+                (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
 
 fun count_constants (conjectures, axclauses, helper_clauses) =
-  if !minimize_applies then
-    (const_min_arity := Symtab.empty;
-     const_needs_hBOOL := Symtab.empty;
-     List.app count_constants_clause conjectures;
-     List.app count_constants_clause axclauses;
-     List.app count_constants_clause helper_clauses;
-     List.app display_arity (Symtab.dest (!const_min_arity)))
-  else ();
+  if minimize_applies then
+     let val (const_min_arity, const_needs_hBOOL) =
+          fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
+       |> fold count_constants_clause axclauses
+       |> fold count_constants_clause helper_clauses
+     val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
+     in (const_min_arity, const_needs_hBOOL) end
+  else (Symtab.empty, Symtab.empty);
 
 (* tptp format *)
 
 (* write TPTP format to a single file *)
 fun tptp_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
     let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
-        val _ = RC.dfg_format := false
-        val conjectures = make_conjecture_clauses thy thms
-        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses thy ax_tuples)
-        val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas)
-        val _ = count_constants (conjectures, axclauses, helper_clauses);
-        val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
-        val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
+        val conjectures = make_conjecture_clauses false thy thms
+        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses false thy ax_tuples)
+        val helper_clauses = get_helper_clauses false thy isFO (conjectures, axclauses, user_lemmas)
+        val (const_min_arity, const_needs_hBOOL) = count_constants (conjectures, axclauses, helper_clauses);
+        val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_min_arity const_needs_hBOOL) conjectures)
+        val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
         val out = TextIO.openOut filename
     in
-        List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
+        List.app (curry TextIO.output out o #1 o (clause2tptp const_min_arity const_needs_hBOOL)) axclauses;
         RC.writeln_strs out tfree_clss;
         RC.writeln_strs out tptp_clss;
         List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
         List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
-        List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
+        List.app (curry TextIO.output out o #1 o (clause2tptp const_min_arity const_needs_hBOOL)) helper_clauses;
         TextIO.closeOut out;
         clnames
     end;
 
 
 (* dfg format *)
 
 fun dfg_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
     let val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
-        val _ = RC.dfg_format := true
-        val conjectures = make_conjecture_clauses thy thms
-        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses thy ax_tuples)
-        val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas)
-        val _ = count_constants (conjectures, axclauses, helper_clauses);
-        val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
+        val conjectures = make_conjecture_clauses true thy thms
+        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses true thy ax_tuples)
+        val helper_clauses = get_helper_clauses true thy isFO (conjectures, axclauses, user_lemmas)
+        val (const_min_arity, const_needs_hBOOL) = count_constants (conjectures, axclauses, helper_clauses);
+        val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_min_arity const_needs_hBOOL) conjectures)
         and probname = Path.implode (Path.base (Path.explode filename))
-        val axstrs = map (#1 o clause2dfg) axclauses
+        val axstrs = map (#1 o (clause2dfg const_min_arity const_needs_hBOOL)) axclauses
         val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
         val out = TextIO.openOut filename
-        val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses
-        val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses
+        val helper_clauses_strs = map (#1 o (clause2dfg const_min_arity const_needs_hBOOL)) helper_clauses
+        val (funcs,cl_preds) = decls_of_clauses const_min_arity const_needs_hBOOL (helper_clauses @ conjectures @ axclauses) arity_clauses
         and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
     in
         TextIO.output (out, RC.string_of_start probname);
         TextIO.output (out, RC.string_of_descrip probname);
         TextIO.output (out, RC.string_of_symbols