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