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