src/HOL/Tools/res_hol_clause.ML
author wenzelm
Fri Aug 17 23:10:42 2007 +0200 (2007-08-17)
changeset 24311 d6864b34eecd
parent 24215 5458fbf18276
child 24323 9aa7b5708eac
permissions -rw-r--r--
proper signature;
     1 (* ID: $Id$
     2    Author: Jia Meng, NICTA
     3 
     4 FOL clauses translated from HOL formulae.
     5 
     6 The combinator code needs to be deleted after the translation paper has been published.
     7 It cannot be used with proof reconstruction because combinators are not introduced by proof.
     8 The Turner combinators (B', C', S') yield no improvement and should be deleted.
     9 *)
    10 
    11 signature RES_HOL_CLAUSE =
    12 sig
    13   val ext: thm
    14   val comb_I: thm
    15   val comb_K: thm
    16   val comb_B: thm
    17   val comb_C: thm
    18   val comb_S: thm
    19   datatype type_level = T_FULL | T_PARTIAL | T_CONST
    20   val typ_level: type_level ref
    21   val minimize_applies: bool ref
    22   val init: theory -> unit
    23   type axiom_name = string
    24   type polarity = bool
    25   type clause_id = int
    26   datatype combterm =
    27       CombConst of string * ResClause.fol_type * ResClause.fol_type list (*Const and Free*)
    28     | CombVar of string * ResClause.fol_type
    29     | CombApp of combterm * combterm
    30   datatype literal = Literal of polarity * combterm
    31   val strip_comb: combterm -> combterm * combterm list
    32   val literals_of_term: term -> literal list * (ResClause.typ_var * sort) list
    33   val tptp_write_file: bool -> thm list -> string ->
    34     (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
    35       ResClause.arityClause list -> string list -> axiom_name list
    36   val dfg_write_file: bool -> thm list -> string ->
    37     (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
    38       ResClause.arityClause list -> string list -> axiom_name list
    39 end
    40 
    41 structure ResHolClause: RES_HOL_CLAUSE =
    42 struct
    43 
    44 structure RC = ResClause;
    45 
    46 (* theorems for combinators and function extensionality *)
    47 val ext = thm "HOL.ext";
    48 val comb_I = thm "ATP_Linkup.COMBI_def";
    49 val comb_K = thm "ATP_Linkup.COMBK_def";
    50 val comb_B = thm "ATP_Linkup.COMBB_def";
    51 val comb_C = thm "ATP_Linkup.COMBC_def";
    52 val comb_S = thm "ATP_Linkup.COMBS_def";
    53 val comb_B' = thm "ATP_Linkup.COMBB'_def";
    54 val comb_C' = thm "ATP_Linkup.COMBC'_def";
    55 val comb_S' = thm "ATP_Linkup.COMBS'_def";
    56 val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
    57 val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
    58 
    59 
    60 (*The different translations of types*)
    61 datatype type_level = T_FULL | T_PARTIAL | T_CONST;
    62 
    63 val typ_level = ref T_CONST;
    64 
    65 fun full_types () = (typ_level:=T_FULL);
    66 fun partial_types () = (typ_level:=T_PARTIAL);
    67 fun const_types_only () = (typ_level:=T_CONST);
    68 
    69 (*If true, each function will be directly applied to as many arguments as possible, avoiding
    70   use of the "apply" operator. Use of hBOOL is also minimized. It only works for the
    71   constant-typed translation, though it could be tried for the partially-typed one.*)
    72 val minimize_applies = ref true;
    73 
    74 val const_typargs = ref (Library.K [] : (string*typ -> typ list));
    75 
    76 val const_min_arity = ref (Symtab.empty : int Symtab.table);
    77 
    78 val const_needs_hBOOL = ref (Symtab.empty : bool Symtab.table);
    79 
    80 fun min_arity_of c = getOpt (Symtab.lookup(!const_min_arity) c, 0);
    81 
    82 (*True if the constant ever appears outside of the top-level position in literals.
    83   If false, the constant always receives all of its arguments and is used as a predicate.*)
    84 fun needs_hBOOL c = not (!minimize_applies) orelse !typ_level=T_PARTIAL orelse
    85                     getOpt (Symtab.lookup(!const_needs_hBOOL) c, false);
    86 
    87 fun init thy = (const_typargs := Sign.const_typargs thy);
    88 
    89 (**********************************************************************)
    90 (* convert a Term.term with lambdas into a Term.term with combinators *)
    91 (**********************************************************************)
    92 
    93 fun is_free (Bound(a)) n = (a = n)
    94   | is_free (Abs(x,_,b)) n = (is_free b (n+1))
    95   | is_free (P $ Q) n = ((is_free P n) orelse (is_free Q n))
    96   | is_free _ _ = false;
    97 
    98 fun compact_comb t bnds = t;
    99 
   100 fun lam2comb (Abs(x,tp,Bound 0)) _ = Const("ATP_Linkup.COMBI",tp-->tp)
   101   | lam2comb (Abs(x,tp,Bound n)) bnds =
   102       let val tb = List.nth(bnds,n-1)
   103       in  Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ Bound (n-1)  end
   104   | lam2comb (Abs(x,t1,Const(c,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Const(c,t2)
   105   | lam2comb (Abs(x,t1,Free(v,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Free(v,t2)
   106   | lam2comb (Abs(x,t1,Var(ind,t2))) _ = Const("ATP_Linkup.COMBK", [t2,t1] ---> t2) $ Var(ind,t2)
   107   | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) bnds =
   108       if is_free P 0 then
   109           let val tI = [t1] ---> t1
   110               val P' = lam2comb (Abs(x,t1,P)) bnds
   111               val tp' = Term.type_of1(bnds,P')
   112               val tS = [tp',tI] ---> Term.type_of1(t1::bnds,P)
   113           in
   114               compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $
   115                              Const("ATP_Linkup.COMBI",tI)) bnds
   116           end
   117       else incr_boundvars ~1 P
   118   | lam2comb (t as (Abs(x,t1,P$Q))) bnds =
   119       let val nfreeP = not(is_free P 0)
   120           and nfreeQ = not(is_free Q 0)
   121           val tpq = Term.type_of1(t1::bnds, P$Q)
   122       in
   123           if nfreeP andalso nfreeQ
   124           then
   125             let val tK = [tpq,t1] ---> tpq
   126             in  Const("ATP_Linkup.COMBK",tK) $ incr_boundvars ~1 (P $ Q)  end
   127           else if nfreeP then
   128             let val Q' = lam2comb (Abs(x,t1,Q)) bnds
   129                 val P' = incr_boundvars ~1 P
   130                 val tp = Term.type_of1(bnds,P')
   131                 val tq' = Term.type_of1(bnds, Q')
   132                 val tB = [tp,tq',t1] ---> tpq
   133             in  compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') bnds  end
   134           else if nfreeQ then
   135             let val P' = lam2comb (Abs(x,t1,P)) bnds
   136                 val Q' = incr_boundvars ~1 Q
   137                 val tq = Term.type_of1(bnds,Q')
   138                 val tp' = Term.type_of1(bnds, P')
   139                 val tC = [tp',tq,t1] ---> tpq
   140             in  compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') bnds  end
   141           else
   142             let val P' = lam2comb (Abs(x,t1,P)) bnds
   143                 val Q' = lam2comb (Abs(x,t1,Q)) bnds
   144                 val tp' = Term.type_of1(bnds,P')
   145                 val tq' = Term.type_of1(bnds,Q')
   146                 val tS = [tp',tq',t1] ---> tpq
   147             in  compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds  end
   148       end
   149   | lam2comb (t as (Abs(x,t1,_))) _ = raise RC.CLAUSE("HOL CLAUSE",t);
   150 
   151 fun to_comb (Abs(x,tp,b)) bnds = lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds
   152   | to_comb (P $ Q) bnds = (to_comb P bnds) $ (to_comb Q bnds)
   153   | to_comb t _ = t;
   154 
   155 
   156 (******************************************************)
   157 (* data types for typed combinator expressions        *)
   158 (******************************************************)
   159 
   160 type axiom_name = string;
   161 type polarity = bool;
   162 type clause_id = int;
   163 
   164 datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list (*Const and Free*)
   165                   | CombVar of string * RC.fol_type
   166                   | CombApp of combterm * combterm
   167 
   168 datatype literal = Literal of polarity * combterm;
   169 
   170 datatype clause =
   171          Clause of {clause_id: clause_id,
   172                     axiom_name: axiom_name,
   173                     th: thm,
   174                     kind: RC.kind,
   175                     literals: literal list,
   176                     ctypes_sorts: (RC.typ_var * Term.sort) list,
   177                     ctvar_type_literals: RC.type_literal list,
   178                     ctfree_type_literals: RC.type_literal list};
   179 
   180 
   181 (*********************************************************************)
   182 (* convert a clause with type Term.term to a clause with type clause *)
   183 (*********************************************************************)
   184 
   185 fun isFalse (Literal(pol, CombConst(c,_,_))) =
   186       (pol andalso c = "c_False") orelse
   187       (not pol andalso c = "c_True")
   188   | isFalse _ = false;
   189 
   190 fun isTrue (Literal (pol, CombConst(c,_,_))) =
   191       (pol andalso c = "c_True") orelse
   192       (not pol andalso c = "c_False")
   193   | isTrue _ = false;
   194 
   195 fun isTaut (Clause {literals,...}) = exists isTrue literals;
   196 
   197 fun type_of (Type (a, Ts)) =
   198       let val (folTypes,ts) = types_of Ts
   199       in  (RC.Comp(RC.make_fixed_type_const a, folTypes), ts)  end
   200   | type_of (tp as (TFree(a,s))) =
   201       (RC.AtomF (RC.make_fixed_type_var a), [RC.mk_typ_var_sort tp])
   202   | type_of (tp as (TVar(v,s))) =
   203       (RC.AtomV (RC.make_schematic_type_var v), [RC.mk_typ_var_sort tp])
   204 and types_of Ts =
   205       let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
   206       in  (folTyps, RC.union_all ts)  end;
   207 
   208 (* same as above, but no gathering of sort information *)
   209 fun simp_type_of (Type (a, Ts)) =
   210       RC.Comp(RC.make_fixed_type_const a, map simp_type_of Ts)
   211   | simp_type_of (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a)
   212   | simp_type_of (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v);
   213 
   214 
   215 fun const_type_of (c,t) =
   216       let val (tp,ts) = type_of t
   217       in  (tp, ts, map simp_type_of (!const_typargs(c,t))) end;
   218 
   219 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   220 fun combterm_of (Const(c,t)) =
   221       let val (tp,ts,tvar_list) = const_type_of (c,t)
   222           val c' = CombConst(RC.make_fixed_const c, tp, tvar_list)
   223       in  (c',ts)  end
   224   | combterm_of (Free(v,t)) =
   225       let val (tp,ts) = type_of t
   226           val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp)
   227                    else CombConst(RC.make_fixed_var v, tp, [])
   228       in  (v',ts)  end
   229   | combterm_of (Var(v,t)) =
   230       let val (tp,ts) = type_of t
   231           val v' = CombVar(RC.make_schematic_var v,tp)
   232       in  (v',ts)  end
   233   | combterm_of (t as (P $ Q)) =
   234       let val (P',tsP) = combterm_of P
   235           val (Q',tsQ) = combterm_of Q
   236       in  (CombApp(P',Q'), tsP union tsQ)  end;
   237 
   238 fun predicate_of ((Const("Not",_) $ P), polarity) = predicate_of (P, not polarity)
   239   | predicate_of (t,polarity) = (combterm_of t, polarity);
   240 
   241 fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
   242   | literals_of_term1 args (Const("op |",_) $ P $ Q) =
   243       literals_of_term1 (literals_of_term1 args P) Q
   244   | literals_of_term1 (lits,ts) P =
   245       let val ((pred,ts'),pol) = predicate_of (P,true)
   246       in
   247           (Literal(pol,pred)::lits, ts union ts')
   248       end;
   249 
   250 fun literals_of_term P = literals_of_term1 ([],[]) P;
   251 
   252 (* making axiom and conjecture clauses *)
   253 fun make_clause(clause_id,axiom_name,kind,th) =
   254     let val (lits,ctypes_sorts) = literals_of_term (to_comb (prop_of th) [])
   255         val (ctvar_lits,ctfree_lits) = RC.add_typs_aux ctypes_sorts
   256     in
   257         if forall isFalse lits
   258         then error "Problem too trivial for resolution (empty clause)"
   259         else
   260             Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
   261                     literals = lits, ctypes_sorts = ctypes_sorts,
   262                     ctvar_type_literals = ctvar_lits,
   263                     ctfree_type_literals = ctfree_lits}
   264     end;
   265 
   266 
   267 fun add_axiom_clause ((th,(name,id)), pairs) =
   268   let val cls = make_clause(id, name, RC.Axiom, th)
   269   in
   270       if isTaut cls then pairs else (name,cls)::pairs
   271   end;
   272 
   273 val make_axiom_clauses = foldl add_axiom_clause [];
   274 
   275 fun make_conjecture_clauses_aux _ [] = []
   276   | make_conjecture_clauses_aux n (th::ths) =
   277       make_clause(n,"conjecture", RC.Conjecture, th) ::
   278       make_conjecture_clauses_aux (n+1) ths;
   279 
   280 val make_conjecture_clauses = make_conjecture_clauses_aux 0;
   281 
   282 
   283 (**********************************************************************)
   284 (* convert clause into ATP specific formats:                          *)
   285 (* TPTP used by Vampire and E                                         *)
   286 (* DFG used by SPASS                                                  *)
   287 (**********************************************************************)
   288 
   289 (*Result of a function type; no need to check that the argument type matches.*)
   290 fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
   291   | result_type _ = raise ERROR "result_type"
   292 
   293 fun type_of_combterm (CombConst(c,tp,_)) = tp
   294   | type_of_combterm (CombVar(v,tp)) = tp
   295   | type_of_combterm (CombApp(t1,t2)) = result_type (type_of_combterm t1);
   296 
   297 (*gets the head of a combinator application, along with the list of arguments*)
   298 fun strip_comb u =
   299     let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   300         |   stripc  x =  x
   301     in  stripc(u,[])  end;
   302 
   303 val type_wrapper = "ti";
   304 
   305 fun head_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL c
   306   | head_needs_hBOOL _ = true;
   307 
   308 fun wrap_type (s, tp) =
   309   if !typ_level=T_FULL then
   310       type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp]
   311   else s;
   312 
   313 fun apply ss = "hAPP" ^ RC.paren_pack ss;
   314 
   315 (*Full (non-optimized) and partial-typed transations*)
   316 fun string_of_combterm1 (CombConst(c,tp,_)) =
   317       let val c' = if c = "equal" then "c_fequal" else c
   318       in  wrap_type (c',tp)  end
   319   | string_of_combterm1 (CombVar(v,tp)) = wrap_type (v,tp)
   320   | string_of_combterm1 (CombApp(t1,t2)) =
   321       let val s1 = string_of_combterm1 t1
   322           and s2 = string_of_combterm1 t2
   323       in
   324           case !typ_level of
   325               T_FULL => wrap_type (apply [s1,s2], result_type (type_of_combterm t1))
   326             | T_PARTIAL => apply [s1,s2, RC.string_of_fol_type (type_of_combterm t1)]
   327             | T_CONST => raise ERROR "string_of_combterm1"
   328       end;
   329 
   330 fun rev_apply (v, []) = v
   331   | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
   332 
   333 fun string_apply (v, args) = rev_apply (v, rev args);
   334 
   335 (*Apply an operator to the argument strings, using either the "apply" operator or
   336   direct function application.*)
   337 fun string_of_applic (CombConst(c,tp,tvars), args) =
   338       let val c = if c = "equal" then "c_fequal" else c
   339           val nargs = min_arity_of c
   340           val args1 = List.take(args, nargs)
   341             handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^
   342                                              Int.toString nargs ^ " but is applied to " ^
   343                                              space_implode ", " args)
   344           val args2 = List.drop(args, nargs)
   345           val targs = if !typ_level = T_CONST then map RC.string_of_fol_type tvars
   346                       else []
   347       in
   348           string_apply (c ^ RC.paren_pack (args1@targs), args2)
   349       end
   350   | string_of_applic (CombVar(v,tp), args) = string_apply (v, args)
   351   | string_of_applic _ = raise ERROR "string_of_applic";
   352 
   353 fun wrap_type_if (head, s, tp) = if head_needs_hBOOL head then wrap_type (s, tp) else s;
   354 
   355 (*Full (if optimized) and constant-typed transations*)
   356 fun string_of_combterm2 t =
   357   let val (head, args) = strip_comb t
   358   in  wrap_type_if (head,
   359                     string_of_applic (head, map string_of_combterm2 args),
   360                     type_of_combterm t)
   361   end;
   362 
   363 fun string_of_combterm t =
   364     case (!typ_level,!minimize_applies) of
   365          (T_PARTIAL, _) => string_of_combterm1 t
   366        | (T_FULL, false) => string_of_combterm1 t
   367        | _ => string_of_combterm2 t;
   368 
   369 (*Boolean-valued terms are here converted to literals.*)
   370 fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t];
   371 
   372 fun string_of_predicate t =
   373   case t of
   374       (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
   375           (*DFG only: new TPTP prefers infix equality*)
   376           ("equal" ^ RC.paren_pack [string_of_combterm t1, string_of_combterm t2])
   377     | _ =>
   378           case #1 (strip_comb t) of
   379               CombConst(c,_,_) => if needs_hBOOL c then boolify t else string_of_combterm t
   380             | _ => boolify t;
   381 
   382 fun string_of_clausename (cls_id,ax_name) =
   383     RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   384 
   385 fun string_of_type_clsname (cls_id,ax_name,idx) =
   386     string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   387 
   388 
   389 (*** tptp format ***)
   390 
   391 fun tptp_of_equality pol (t1,t2) =
   392   let val eqop = if pol then " = " else " != "
   393   in  string_of_combterm t1 ^ eqop ^ string_of_combterm t2  end;
   394 
   395 fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
   396       tptp_of_equality pol (t1,t2)
   397   | tptp_literal (Literal(pol,pred)) =
   398       RC.tptp_sign pol (string_of_predicate pred);
   399 
   400 (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
   401   the latter should only occur in conjecture clauses.*)
   402 fun tptp_type_lits (Clause cls) =
   403     let val lits = map tptp_literal (#literals cls)
   404         val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls)
   405         val ctfree_lits = map RC.tptp_of_typeLit (#ctfree_type_literals cls)
   406     in
   407         (ctvar_lits_strs @ lits, ctfree_lits)
   408     end;
   409 
   410 fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   411     let val (lits,ctfree_lits) = tptp_type_lits cls
   412         val cls_str = RC.gen_tptp_cls(clause_id,axiom_name,kind,lits)
   413     in
   414         (cls_str,ctfree_lits)
   415     end;
   416 
   417 
   418 (*** dfg format ***)
   419 
   420 fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred);
   421 
   422 fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) =
   423   let val lits = map dfg_literal literals
   424       val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts
   425       val tvar_lits_strs = map RC.dfg_of_typeLit tvar_lits
   426       val tfree_lits = map RC.dfg_of_typeLit tfree_lits
   427   in
   428       (tvar_lits_strs @ lits, tfree_lits)
   429   end;
   430 
   431 fun get_uvars (CombConst _) vars = vars
   432   | get_uvars (CombVar(v,_)) vars = (v::vars)
   433   | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars);
   434 
   435 fun get_uvars_l (Literal(_,c)) = get_uvars c [];
   436 
   437 fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
   438 
   439 fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   440     let val (lits,tfree_lits) = dfg_clause_aux cls
   441         val vars = dfg_vars cls
   442         val tvars = RC.get_tvar_strs ctypes_sorts
   443         val knd = RC.name_of_kind kind
   444         val lits_str = commas lits
   445         val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars)
   446     in (cls_str, tfree_lits) end;
   447 
   448 (** For DFG format: accumulate function and predicate declarations **)
   449 
   450 fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars;
   451 
   452 fun add_decls (CombConst(c,tp,tvars), (funcs,preds)) =
   453       if c = "equal" then (addtypes tvars funcs, preds)
   454       else
   455         (case !typ_level of
   456             T_PARTIAL => (RC.add_foltype_funcs (tp, Symtab.update(c,0) funcs), preds)
   457           | _ =>
   458                let val arity = min_arity_of c
   459                    val ntys = if !typ_level = T_CONST then length tvars else 0
   460                    val addit = Symtab.update(c, arity+ntys)
   461                in
   462                    if needs_hBOOL c then (addtypes tvars (addit funcs), preds)
   463                    else (addtypes tvars funcs, addit preds)
   464                end)
   465   | add_decls (CombVar(_,ctp), (funcs,preds)) =
   466       (RC.add_foltype_funcs (ctp,funcs), preds)
   467   | add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls));
   468 
   469 fun add_literal_decls (Literal(_,c), decls) = add_decls (c,decls);
   470 
   471 fun add_clause_decls (Clause {literals, ...}, decls) =
   472     foldl add_literal_decls decls literals
   473     handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
   474 
   475 fun decls_of_clauses clauses arity_clauses =
   476   let val happ_ar = case !typ_level of T_PARTIAL => 3 | _ => 2
   477       val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",happ_ar) RC.init_functab)
   478       val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
   479       val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses)
   480   in
   481       (Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses),
   482        Symtab.dest predtab)
   483   end;
   484 
   485 fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
   486   foldl RC.add_type_sort_preds preds ctypes_sorts
   487   handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
   488 
   489 (*Higher-order clauses have only the predicates hBOOL and type classes.*)
   490 fun preds_of_clauses clauses clsrel_clauses arity_clauses =
   491     Symtab.dest
   492         (foldl RC.add_classrelClause_preds
   493                (foldl RC.add_arityClause_preds
   494                       (foldl add_clause_preds Symtab.empty clauses)
   495                       arity_clauses)
   496                clsrel_clauses)
   497 
   498 
   499 
   500 (**********************************************************************)
   501 (* write clauses to files                                             *)
   502 (**********************************************************************)
   503 
   504 
   505 val init_counters =
   506     Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
   507                  ("c_COMBB", 0), ("c_COMBC", 0),
   508                  ("c_COMBS", 0), ("c_COMBB_e", 0),
   509                  ("c_COMBC_e", 0), ("c_COMBS_e", 0)];
   510 
   511 fun count_combterm (CombConst(c,tp,_), ct) =
   512      (case Symtab.lookup ct c of NONE => ct  (*no counter*)
   513                                | SOME n => Symtab.update (c,n+1) ct)
   514   | count_combterm (CombVar(v,tp), ct) = ct
   515   | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
   516 
   517 fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
   518 
   519 fun count_clause (Clause{literals,...}, ct) = foldl count_literal ct literals;
   520 
   521 fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
   522   if axiom_name mem_string user_lemmas then foldl count_literal ct literals
   523   else ct;
   524 
   525 val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
   526 
   527 fun get_helper_clauses isFO (conjectures, axclauses, user_lemmas) =
   528   if isFO then []  (*first-order*)
   529   else
   530     let val ct0 = foldl count_clause init_counters conjectures
   531         val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
   532         fun needed c = valOf (Symtab.lookup ct c) > 0
   533         val IK = if needed "c_COMBI" orelse needed "c_COMBK"
   534                  then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K])
   535                  else []
   536         val BC = if needed "c_COMBB" orelse needed "c_COMBC"
   537                  then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C])
   538                  else []
   539         val S = if needed "c_COMBS"
   540                 then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S])
   541                 else []
   542         val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e"
   543                    then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C'])
   544                    else []
   545         val S' = if needed "c_COMBS_e"
   546                  then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S'])
   547                  else []
   548         val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
   549     in
   550         map #2 (make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S'))
   551     end;
   552 
   553 (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   554   are not at top level, to see if hBOOL is needed.*)
   555 fun count_constants_term toplev t =
   556   let val (head, args) = strip_comb t
   557       val n = length args
   558       val _ = List.app (count_constants_term false) args
   559   in
   560       case head of
   561           CombConst (a,_,_) => (*predicate or function version of "equal"?*)
   562             let val a = if a="equal" andalso not toplev then "c_fequal" else a
   563             in
   564               const_min_arity := Symtab.map_default (a,n) (curry Int.min n) (!const_min_arity);
   565               if toplev then ()
   566               else const_needs_hBOOL := Symtab.update (a,true) (!const_needs_hBOOL)
   567             end
   568         | ts => ()
   569   end;
   570 
   571 (*A literal is a top-level term*)
   572 fun count_constants_lit (Literal (_,t)) = count_constants_term true t;
   573 
   574 fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals;
   575 
   576 fun display_arity (c,n) =
   577   Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
   578                 (if needs_hBOOL c then " needs hBOOL" else ""));
   579 
   580 fun count_constants (conjectures, axclauses, helper_clauses) =
   581   if !minimize_applies andalso !typ_level<>T_PARTIAL then
   582     (const_min_arity := Symtab.empty;
   583      const_needs_hBOOL := Symtab.empty;
   584      List.app count_constants_clause conjectures;
   585      List.app count_constants_clause axclauses;
   586      List.app count_constants_clause helper_clauses;
   587      List.app display_arity (Symtab.dest (!const_min_arity)))
   588   else ();
   589 
   590 (* tptp format *)
   591 
   592 (* write TPTP format to a single file *)
   593 fun tptp_write_file isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   594     let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
   595         val _ = RC.dfg_format := false
   596         val conjectures = make_conjecture_clauses thms
   597         val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   598         val helper_clauses = get_helper_clauses isFO (conjectures, axclauses, user_lemmas)
   599         val _ = count_constants (conjectures, axclauses, helper_clauses);
   600         val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
   601         val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   602         val out = TextIO.openOut filename
   603     in
   604         List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
   605         RC.writeln_strs out tfree_clss;
   606         RC.writeln_strs out tptp_clss;
   607         List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
   608         List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
   609         List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
   610         TextIO.closeOut out;
   611         clnames
   612     end;
   613 
   614 
   615 
   616 (* dfg format *)
   617 
   618 fun dfg_write_file isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   619     let val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
   620         val _ = RC.dfg_format := true
   621         val conjectures = make_conjecture_clauses thms
   622         val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   623         val helper_clauses = get_helper_clauses isFO (conjectures, axclauses, user_lemmas)
   624         val _ = count_constants (conjectures, axclauses, helper_clauses);
   625         val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   626         and probname = Path.implode (Path.base (Path.explode filename))
   627         val axstrs = map (#1 o clause2dfg) axclauses
   628         val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
   629         val out = TextIO.openOut filename
   630         val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses
   631         val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses
   632         and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   633     in
   634         TextIO.output (out, RC.string_of_start probname);
   635         TextIO.output (out, RC.string_of_descrip probname);
   636         TextIO.output (out, RC.string_of_symbols
   637                               (RC.string_of_funcs funcs)
   638                               (RC.string_of_preds (cl_preds @ ty_preds)));
   639         TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
   640         RC.writeln_strs out axstrs;
   641         List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
   642         List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
   643         RC.writeln_strs out helper_clauses_strs;
   644         TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   645         RC.writeln_strs out tfree_clss;
   646         RC.writeln_strs out dfg_clss;
   647         TextIO.output (out, "end_of_list.\n\n");
   648         (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   649         TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
   650         TextIO.output (out, "end_problem.\n");
   651         TextIO.closeOut out;
   652         clnames
   653     end;
   654 
   655 end