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