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