src/HOL/Tools/res_hol_clause.ML
author paulson
Mon Apr 30 13:22:35 2007 +0200 (2007-04-30)
changeset 22825 bd774e01d6d5
parent 22130 0906fd95e0b5
child 22851 7b7d6e1c70b6
permissions -rw-r--r--
Fixing bugs in the partial-typed and fully-typed translations
     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_CONST 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 val type_wrapper = "ti";
   296 
   297 fun wrap_type (c,tp) = case !typ_level of
   298 	T_FULL => type_wrapper ^ RC.paren_pack [c, RC.string_of_fol_type tp]
   299       | _ => c;
   300     
   301 
   302 val bool_tp = RC.make_fixed_type_const "bool";
   303 
   304 val app_str = "hAPP";
   305 
   306 (*Result of a function type; no need to check that the argument type matches.*)
   307 fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
   308   | result_type _ = raise ERROR "result_type"
   309 
   310 fun type_of_combterm (CombConst(c,tp,_)) = tp
   311   | type_of_combterm (CombFree(v,tp)) = tp
   312   | type_of_combterm (CombVar(v,tp)) = tp
   313   | type_of_combterm (CombApp(t1,t2)) = result_type (type_of_combterm t1);
   314 
   315 (*gets the head of a combinator application, along with the list of arguments*)
   316 fun strip_comb u =
   317     let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   318         |   stripc  x =  x
   319     in  stripc(u,[])  end;
   320 
   321 (*Full and partial-typed transations*)
   322 fun string_of_combterm1 (CombConst(c,tp,_)) = 
   323       let val c' = if c = "equal" then "c_fequal" else c
   324       in  wrap_type (c',tp)  end
   325   | string_of_combterm1 (CombFree(v,tp)) = wrap_type (v,tp)
   326   | string_of_combterm1 (CombVar(v,tp)) = wrap_type (v,tp)
   327   | string_of_combterm1 (CombApp(t1,t2)) =
   328       let val s1 = string_of_combterm1 t1
   329 	  and s2 = string_of_combterm1 t2
   330       in
   331 	  case !typ_level of
   332 	      T_FULL => type_wrapper ^ 
   333 	                RC.paren_pack 
   334 	                  [app_str ^ RC.paren_pack [s1,s2], 
   335 	                   RC.string_of_fol_type (result_type (type_of_combterm t1))]
   336 	    | T_PARTIAL => app_str ^ RC.paren_pack 
   337 	                     [s1,s2, RC.string_of_fol_type (type_of_combterm t1)]
   338 	    | T_CONST => raise ERROR "string_of_combterm1"
   339       end;
   340 
   341 fun rev_apply (v, []) = v
   342   | rev_apply (v, arg::args) = app_str ^ RC.paren_pack [rev_apply (v, args), arg];
   343 
   344 fun string_apply (v, args) = rev_apply (v, rev args);
   345 
   346 (*Apply an operator to the argument strings, using either the "apply" operator or
   347   direct function application.*)
   348 fun string_of_applic (CombConst(c,_,tvars), args) =
   349       let val c = if c = "equal" then "c_fequal" else c
   350           val nargs = min_arity_of c
   351           val args1 = List.take(args, nargs) @ (map RC.string_of_fol_type tvars)
   352             handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^
   353 					     Int.toString nargs ^ " but is applied to " ^ 
   354 					     space_implode ", " args) 
   355           val args2 = List.drop(args, nargs)
   356       in
   357 	  string_apply (c ^ RC.paren_pack args1, args2)
   358       end
   359   | string_of_applic (CombFree(v,_), args) = string_apply (v, args)
   360   | string_of_applic (CombVar(v,_), args) = string_apply (v, args)  
   361   | string_of_applic _ = raise ERROR "string_of_applic";
   362 
   363 (*Constant-typed transation*)
   364 fun string_of_combterm2 t = 
   365   let val (head, args) = strip_comb t
   366   in  string_of_applic (head, map string_of_combterm2 args)  end;
   367 
   368 fun string_of_combterm t = 
   369     case !typ_level of T_CONST => string_of_combterm2 t
   370 		           | _ => string_of_combterm1 t;
   371 
   372 (*Boolean-valued terms are here converted to literals.*)
   373 fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t];
   374 
   375 fun string_of_predicate t = 
   376   case t of
   377       (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
   378 	  (*DFG only: new TPTP prefers infix equality*)
   379 	  ("equal" ^ RC.paren_pack [string_of_combterm t1, string_of_combterm t2])
   380     | _ => 
   381           case #1 (strip_comb t) of
   382               CombConst(c,_,_) => if needs_hBOOL c then boolify t else string_of_combterm t
   383             | _ => boolify t;
   384 
   385 fun string_of_clausename (cls_id,ax_name) = 
   386     RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   387 
   388 fun string_of_type_clsname (cls_id,ax_name,idx) = 
   389     string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   390 
   391 
   392 (*** tptp format ***)
   393 
   394 fun tptp_of_equality pol (t1,t2) =
   395   let val eqop = if pol then " = " else " != "
   396   in  string_of_combterm t1 ^ eqop ^ string_of_combterm t2  end;
   397 
   398 fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) = 
   399       tptp_of_equality pol (t1,t2)
   400   | tptp_literal (Literal(pol,pred)) = 
   401       RC.tptp_sign pol (string_of_predicate pred);
   402  
   403 (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
   404   the latter should only occur in conjecture clauses.*)
   405 fun tptp_type_lits (Clause cls) = 
   406     let val lits = map tptp_literal (#literals cls)
   407 	val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls)
   408 	val ctfree_lits = map RC.tptp_of_typeLit (#ctfree_type_literals cls)
   409     in
   410 	(ctvar_lits_strs @ lits, ctfree_lits)
   411     end; 
   412     
   413 fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   414     let val (lits,ctfree_lits) = tptp_type_lits cls
   415 	val cls_str = RC.gen_tptp_cls(clause_id,axiom_name,kind,lits)
   416     in
   417 	(cls_str,ctfree_lits)
   418     end;
   419 
   420 
   421 (*** dfg format ***)
   422 
   423 fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred);
   424 
   425 fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = 
   426   let val lits = map dfg_literal literals
   427       val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts
   428       val tvar_lits_strs = map RC.dfg_of_typeLit tvar_lits
   429       val tfree_lits = map RC.dfg_of_typeLit tfree_lits 
   430   in
   431       (tvar_lits_strs @ lits, tfree_lits)
   432   end; 
   433 
   434 fun get_uvars (CombConst _) vars = vars
   435   | get_uvars (CombFree _) vars = vars
   436   | get_uvars (CombVar(v,_)) vars = (v::vars)
   437   | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars);
   438 
   439 fun get_uvars_l (Literal(_,c)) = get_uvars c [];
   440 
   441 fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
   442  
   443 fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   444     let val (lits,tfree_lits) = dfg_clause_aux cls 
   445         val vars = dfg_vars cls
   446         val tvars = RC.get_tvar_strs ctypes_sorts
   447 	val knd = RC.name_of_kind kind
   448 	val lits_str = commas lits
   449 	val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) 
   450     in (cls_str, tfree_lits) end;
   451 
   452 (** For DFG format: accumulate function and predicate declarations **)
   453 
   454 fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars;
   455 
   456 fun add_decls (CombConst(c,tp,tvars), (funcs,preds)) =
   457       if c = "equal" then (addtypes tvars funcs, preds)
   458       else
   459 	(case !typ_level of
   460 	     T_CONST => 
   461                let val arity = min_arity_of c + length tvars
   462                    val addit = Symtab.update(c,arity) 
   463                in
   464                    if needs_hBOOL c then (addtypes tvars (addit funcs), preds)
   465                    else (addtypes tvars funcs, addit preds)
   466                end
   467            | _ => (RC.add_foltype_funcs (tp, Symtab.update(c,0) funcs), preds))
   468   | add_decls (CombFree(v,ctp), (funcs,preds)) = 
   469       (RC.add_foltype_funcs (ctp,Symtab.update (v,0) funcs), preds)
   470   | add_decls (CombVar(_,ctp), (funcs,preds)) = 
   471       (RC.add_foltype_funcs (ctp,funcs), preds)
   472   | add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls));
   473 
   474 fun add_literal_decls (Literal(_,c), decls) = add_decls (c,decls);
   475 
   476 fun add_clause_decls (Clause {literals, ...}, decls) =
   477     foldl add_literal_decls decls literals
   478     handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
   479 
   480 fun decls_of_clauses clauses arity_clauses =
   481   let val happ_ar = case !typ_level of T_PARTIAL => 3 | _ => 2
   482       val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",happ_ar) Symtab.empty)
   483       val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
   484       val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses)
   485   in
   486       (Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses), 
   487        Symtab.dest predtab)
   488   end;
   489 
   490 fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
   491   foldl RC.add_type_sort_preds preds ctypes_sorts
   492   handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
   493 
   494 (*Higher-order clauses have only the predicates hBOOL and type classes.*)
   495 fun preds_of_clauses clauses clsrel_clauses arity_clauses = 
   496     Symtab.dest
   497 	(foldl RC.add_classrelClause_preds 
   498 	       (foldl RC.add_arityClause_preds
   499 		      (foldl add_clause_preds Symtab.empty clauses) 
   500 		      arity_clauses)
   501 	       clsrel_clauses)
   502 
   503 
   504 
   505 (**********************************************************************)
   506 (* write clauses to files                                             *)
   507 (**********************************************************************)
   508 
   509 
   510 val init_counters =
   511     Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
   512 		 ("c_COMBB", 0), ("c_COMBC", 0),
   513 		 ("c_COMBS", 0), ("c_COMBB_e", 0),
   514 		 ("c_COMBC_e", 0), ("c_COMBS_e", 0)];
   515                 
   516 fun count_combterm (CombConst(c,tp,_), ct) = 
   517      (case Symtab.lookup ct c of NONE => ct  (*no counter*)
   518                                | SOME n => Symtab.update (c,n+1) ct)
   519   | count_combterm (CombFree(v,tp), ct) = ct
   520   | count_combterm (CombVar(v,tp), ct) = ct
   521   | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
   522 
   523 fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
   524 
   525 fun count_clause (Clause{literals,...}, ct) = foldl count_literal ct literals;
   526 
   527 fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) = 
   528   if axiom_name mem_string user_lemmas then foldl count_literal ct literals
   529   else ct;
   530 
   531 val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
   532 
   533 fun get_helper_clauses (conjectures, axclauses, user_lemmas) =
   534     let val ct0 = foldl count_clause init_counters conjectures
   535         val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
   536         fun needed c = valOf (Symtab.lookup ct c) > 0
   537         val IK = if needed "c_COMBI" orelse needed "c_COMBK" 
   538                  then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K]) 
   539                  else []
   540 	val BC = if needed "c_COMBB" orelse needed "c_COMBC" 
   541 	         then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C]) 
   542 	         else []
   543 	val S = if needed "c_COMBS" 
   544 	        then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S]) 
   545 	        else []
   546 	val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e" 
   547 	           then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C']) 
   548 	           else []
   549 	val S' = if needed "c_COMBS_e" 
   550 	         then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S']) 
   551 	         else []
   552 	val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
   553     in
   554 	map #2 (make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S'))
   555     end
   556 
   557 (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   558   are not at top level, to see if hBOOL is needed.*)
   559 fun count_constants_term toplev t =
   560   let val (head, args) = strip_comb t
   561       val n = length args
   562       val _ = List.app (count_constants_term false) args
   563   in
   564       case head of
   565 	  CombConst (a,_,_) => (*predicate or function version of "equal"?*)
   566 	    let val a = if a="equal" andalso not toplev then "c_fequal" else a
   567 	    in  
   568 	      const_min_arity := Symtab.map_default (a,n) (curry Int.min n) (!const_min_arity);
   569 	      if toplev then ()
   570 	      else const_needs_hBOOL := Symtab.update (a,true) (!const_needs_hBOOL)
   571 	    end
   572 	| ts => ()
   573   end;
   574 
   575 (*A literal is a top-level term*)
   576 fun count_constants_lit (Literal (_,t)) = count_constants_term true t;
   577 
   578 fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals;
   579 
   580 fun display_arity (c,n) =
   581   Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ 
   582                 (if needs_hBOOL c then " needs hBOOL" else ""));
   583 
   584 fun count_constants (conjectures, axclauses, helper_clauses) = 
   585   if !minimize_applies andalso !typ_level=T_CONST then
   586     (List.app count_constants_clause conjectures;
   587      List.app count_constants_clause axclauses;
   588      List.app count_constants_clause helper_clauses;
   589      List.app display_arity (Symtab.dest (!const_min_arity)))
   590   else ();
   591 
   592 (* tptp format *)
   593 						  
   594 (* write TPTP format to a single file *)
   595 fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   596     let val conjectures = make_conjecture_clauses thms
   597         val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   598 	val helper_clauses = get_helper_clauses (conjectures, axclauses, user_lemmas)
   599 	val _ = count_constants (conjectures, axclauses, helper_clauses);
   600 	val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
   601 	val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   602         val out = TextIO.openOut filename
   603     in
   604 	List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
   605 	RC.writeln_strs out tfree_clss;
   606 	RC.writeln_strs out tptp_clss;
   607 	List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
   608 	List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
   609 	List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
   610 	TextIO.closeOut out;
   611 	clnames
   612     end;
   613 
   614 
   615 
   616 (* dfg format *)
   617 
   618 fun dfg_write_file  thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   619     let val conjectures = make_conjecture_clauses thms
   620         val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   621 	val helper_clauses = get_helper_clauses (conjectures, axclauses, user_lemmas)
   622 	val _ = count_constants (conjectures, axclauses, helper_clauses);
   623 	val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   624 	and probname = Path.implode (Path.base (Path.explode filename))
   625 	val axstrs = map (#1 o clause2dfg) axclauses
   626 	val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
   627 	val out = TextIO.openOut filename
   628 	val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses
   629 	val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses
   630 	and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   631     in
   632 	TextIO.output (out, RC.string_of_start probname); 
   633 	TextIO.output (out, RC.string_of_descrip probname); 
   634 	TextIO.output (out, RC.string_of_symbols 
   635 	                      (RC.string_of_funcs funcs) 
   636 	                      (RC.string_of_preds (cl_preds @ ty_preds))); 
   637 	TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
   638 	RC.writeln_strs out axstrs;
   639 	List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
   640 	List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
   641 	RC.writeln_strs out helper_clauses_strs;
   642 	TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   643 	RC.writeln_strs out tfree_clss;
   644 	RC.writeln_strs out dfg_clss;
   645 	TextIO.output (out, "end_of_list.\n\n");
   646 	(*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   647 	TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
   648 	TextIO.output (out, "end_problem.\n");
   649 	TextIO.closeOut out;
   650 	clnames
   651     end;
   652 
   653 end