src/HOL/Tools/res_hol_clause.ML
author paulson
Fri Dec 01 12:23:53 2006 +0100 (2006-12-01)
changeset 21617 4664489469fc
parent 21573 8a7a68c0096c
child 21858 05f57309170c
permissions -rw-r--r--
Deleted dead code
     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 val const_typargs = ref (Library.K [] : (string*typ -> typ list));
    29 
    30 fun init thy = (const_typargs := Sign.const_typargs thy);
    31 
    32 (**********************************************************************)
    33 (* convert a Term.term with lambdas into a Term.term with combinators *) 
    34 (**********************************************************************)
    35 
    36 fun is_free (Bound(a)) n = (a = n)
    37   | is_free (Abs(x,_,b)) n = (is_free b (n+1))
    38   | is_free (P $ Q) n = ((is_free P n) orelse (is_free Q n))
    39   | is_free _ _ = false;
    40 
    41 
    42 (*******************************************)
    43 fun mk_compact_comb (tm as (Const("ATP_Linkup.COMBB",_)$p) $ (Const("ATP_Linkup.COMBB",_)$q$r)) bnds =
    44       let val tp_p = Term.type_of1(bnds,p)
    45 	  val tp_q = Term.type_of1(bnds,q)
    46 	  val tp_r = Term.type_of1(bnds,r)
    47 	  val typ = Term.type_of1(bnds,tm)
    48 	  val typ_B' = [tp_p,tp_q,tp_r] ---> typ
    49       in
    50 	  Const("ATP_Linkup.COMBB'",typ_B') $ p $ q $ r
    51       end
    52   | mk_compact_comb (tm as (Const("ATP_Linkup.COMBC",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) bnds =
    53       let val tp_p = Term.type_of1(bnds,p)
    54 	  val tp_q = Term.type_of1(bnds,q)
    55 	  val tp_r = Term.type_of1(bnds,r)
    56 	  val typ = Term.type_of1(bnds,tm)
    57 	  val typ_C' = [tp_p,tp_q,tp_r] ---> typ
    58       in
    59 	  Const("ATP_Linkup.COMBC'",typ_C') $ p $ q $ r
    60       end
    61   | mk_compact_comb (tm as (Const("ATP_Linkup.COMBS",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) bnds =
    62       let val tp_p = Term.type_of1(bnds,p)
    63 	  val tp_q = Term.type_of1(bnds,q)
    64 	  val tp_r = Term.type_of1(bnds,r)
    65 	  val typ = Term.type_of1(bnds,tm)
    66 	  val typ_S' = [tp_p,tp_q,tp_r] ---> typ
    67       in
    68 	  Const("ATP_Linkup.COMBS'",typ_S') $ p $ q $ r
    69       end
    70   | mk_compact_comb tm _ = tm;
    71 
    72 fun compact_comb t bnds = 
    73   if !use_Turner then mk_compact_comb t bnds else t;
    74 
    75 fun lam2comb (Abs(x,tp,Bound 0)) _ = Const("ATP_Linkup.COMBI",tp-->tp) 
    76   | lam2comb (Abs(x,tp,Bound n)) bnds = 
    77       let val tb = List.nth(bnds,n-1)
    78       in
    79 	  Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ Bound (n-1)
    80       end
    81   | lam2comb (Abs(x,t1,Const(c,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Const(c,t2) 
    82   | lam2comb (Abs(x,t1,Free(v,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Free(v,t2)
    83   | lam2comb (Abs(x,t1,Var(ind,t2))) _ = Const("ATP_Linkup.COMBK", [t2,t1] ---> t2) $ Var(ind,t2)
    84   | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) bnds =
    85       if is_free P 0 then 
    86 	  let val tI = [t1] ---> t1
    87 	      val P' = lam2comb (Abs(x,t1,P)) bnds
    88 	      val tp' = Term.type_of1(bnds,P')
    89 	      val tr = Term.type_of1(t1::bnds,P)
    90 	      val tS = [tp',tI] ---> tr
    91 	  in
    92 	      compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ 
    93 	                     Const("ATP_Linkup.COMBI",tI)) bnds
    94 	  end
    95       else incr_boundvars ~1 P
    96   | lam2comb (t as (Abs(x,t1,P$Q))) bnds =
    97       let val nfreeP = not(is_free P 0)
    98 	  and nfreeQ = not(is_free Q 0)
    99 	  val tpq = Term.type_of1(t1::bnds, P$Q) 
   100       in
   101 	  if nfreeP andalso nfreeQ 
   102 	  then 
   103 	    let val tK = [tpq,t1] ---> tpq
   104 		val PQ' = incr_boundvars ~1 (P $ Q)
   105 	    in 
   106 		Const("ATP_Linkup.COMBK",tK) $ PQ'
   107 	    end
   108 	  else if nfreeP then 
   109 	    let val Q' = lam2comb (Abs(x,t1,Q)) bnds
   110 		val P' = incr_boundvars ~1 P
   111 		val tp = Term.type_of1(bnds,P')
   112 		val tq' = Term.type_of1(bnds, Q')
   113 		val tB = [tp,tq',t1] ---> tpq
   114 	    in
   115 		compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') bnds 
   116 	    end
   117 	  else if nfreeQ then 
   118 	    let val P' = lam2comb (Abs(x,t1,P)) bnds
   119 		val Q' = incr_boundvars ~1 Q
   120 		val tq = Term.type_of1(bnds,Q')
   121 		val tp' = Term.type_of1(bnds, P')
   122 		val tC = [tp',tq,t1] ---> tpq
   123 	    in
   124 		compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') bnds
   125 	    end
   126           else
   127 	    let val P' = lam2comb (Abs(x,t1,P)) bnds
   128 		val Q' = lam2comb (Abs(x,t1,Q)) bnds 
   129 		val tp' = Term.type_of1(bnds,P')
   130 		val tq' = Term.type_of1(bnds,Q')
   131 		val tS = [tp',tq',t1] ---> tpq
   132 	    in
   133 		compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds
   134 	    end
   135       end
   136   | lam2comb (t as (Abs(x,t1,_))) _ = raise ResClause.CLAUSE("HOL CLAUSE",t);
   137 
   138 (*********************)
   139 
   140 fun to_comb (Abs(x,tp,b)) bnds =
   141       lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds 
   142   | to_comb (P $ Q) bnds = (to_comb P bnds) $ (to_comb Q bnds)
   143   | to_comb t _ = t;
   144 
   145 
   146 (******************************************************)
   147 (* data types for typed combinator expressions        *)
   148 (******************************************************)
   149 
   150 datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE;
   151 
   152 val typ_level = ref T_CONST;
   153 
   154 fun full_types () = (typ_level:=T_FULL);
   155 fun partial_types () = (typ_level:=T_PARTIAL);
   156 fun const_types_only () = (typ_level:=T_CONST);
   157 fun no_types () = (typ_level:=T_NONE);
   158 
   159 fun find_typ_level () = !typ_level;
   160 
   161 type axiom_name = string;
   162 type polarity = bool;
   163 type clause_id = int;
   164 
   165 datatype combterm = CombConst of string * ResClause.fol_type * ResClause.fol_type list
   166 		  | CombFree of string * ResClause.fol_type
   167 		  | CombVar of string * ResClause.fol_type
   168 		  | CombApp of combterm * combterm * ResClause.fol_type
   169 		  
   170 datatype literal = Literal of polarity * combterm;
   171 
   172 datatype clause = 
   173 	 Clause of {clause_id: clause_id,
   174 		    axiom_name: axiom_name,
   175 		    th: thm,
   176 		    kind: ResClause.kind,
   177 		    literals: literal list,
   178 		    ctypes_sorts: (ResClause.typ_var * Term.sort) list, 
   179                     ctvar_type_literals: ResClause.type_literal list, 
   180                     ctfree_type_literals: ResClause.type_literal list};
   181 
   182 
   183 (*********************************************************************)
   184 (* convert a clause with type Term.term to a clause with type clause *)
   185 (*********************************************************************)
   186 
   187 fun isFalse (Literal(pol, CombConst(c,_,_))) =
   188       (pol andalso c = "c_False") orelse
   189       (not pol andalso c = "c_True")
   190   | isFalse _ = false;
   191 
   192 fun isTrue (Literal (pol, CombConst(c,_,_))) =
   193       (pol andalso c = "c_True") orelse
   194       (not pol andalso c = "c_False")
   195   | isTrue _ = false;
   196   
   197 fun isTaut (Clause {literals,...}) = exists isTrue literals;  
   198 
   199 fun type_of (Type (a, Ts)) =
   200       let val (folTypes,ts) = types_of Ts
   201 	  val t = ResClause.make_fixed_type_const a
   202       in
   203 	  (ResClause.mk_fol_type("Comp",t,folTypes), ts)
   204       end
   205   | type_of (tp as (TFree(a,s))) =
   206       let val t = ResClause.make_fixed_type_var a
   207       in
   208 	  (ResClause.mk_fol_type("Fixed",t,[]), [ResClause.mk_typ_var_sort tp])
   209       end
   210   | type_of (tp as (TVar(v,s))) =
   211       let val t = ResClause.make_schematic_type_var v
   212       in
   213 	  (ResClause.mk_fol_type("Var",t,[]), [ResClause.mk_typ_var_sort tp])
   214       end
   215 and types_of Ts =
   216       let val foltyps_ts = map type_of Ts
   217 	  val (folTyps,ts) = ListPair.unzip foltyps_ts
   218       in
   219 	  (folTyps, ResClause.union_all ts)
   220       end;
   221 
   222 (* same as above, but no gathering of sort information *)
   223 fun simp_type_of (Type (a, Ts)) = 
   224       let val typs = map simp_type_of Ts
   225 	  val t = ResClause.make_fixed_type_const a
   226       in
   227 	  ResClause.mk_fol_type("Comp",t,typs)
   228       end
   229   | simp_type_of (TFree (a,s)) = ResClause.mk_fol_type("Fixed",ResClause.make_fixed_type_var a,[])
   230   | simp_type_of (TVar (v,s)) = ResClause.mk_fol_type("Var",ResClause.make_schematic_type_var v,[]);
   231 
   232 
   233 fun const_type_of (c,t) =
   234     let val (tp,ts) = type_of t
   235 	val tvars = !const_typargs(c,t)
   236     in
   237 	(tp, ts, map simp_type_of tvars)
   238     end;
   239 
   240 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   241 fun combterm_of (Const(c,t)) =
   242       let val (tp,ts,tvar_list) = const_type_of (c,t)
   243 	  val c' = CombConst(ResClause.make_fixed_const c,tp,tvar_list)
   244       in
   245 	  (c',ts)
   246       end
   247   | combterm_of (Free(v,t)) =
   248       let val (tp,ts) = type_of t
   249 	  val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp)
   250 		   else CombFree(ResClause.make_fixed_var v,tp)
   251       in
   252 	  (v',ts)
   253       end
   254   | combterm_of (Var(v,t)) =
   255       let val (tp,ts) = type_of t
   256 	  val v' = CombVar(ResClause.make_schematic_var v,tp)
   257       in
   258 	  (v',ts)
   259       end
   260   | combterm_of (t as (P $ Q)) =
   261       let val (P',tsP) = combterm_of P
   262 	  val (Q',tsQ) = combterm_of Q
   263 	  val tp = Term.type_of t
   264 	  val t' = CombApp(P',Q', simp_type_of tp)
   265       in
   266 	  (t',tsP union tsQ)
   267       end;
   268 
   269 fun predicate_of ((Const("Not",_) $ P), polarity) = predicate_of (P, not polarity)
   270   | predicate_of (t,polarity) = (combterm_of t, polarity);
   271 
   272 fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
   273   | literals_of_term1 args (Const("op |",_) $ P $ Q) = 
   274       literals_of_term1 (literals_of_term1 args P) Q
   275   | literals_of_term1 (lits,ts) P =
   276       let val ((pred,ts'),pol) = predicate_of (P,true)
   277       in
   278 	  (Literal(pol,pred)::lits, ts union ts')
   279       end;
   280 
   281 fun literals_of_term P = literals_of_term1 ([],[]) P;
   282 
   283 (* making axiom and conjecture clauses *)
   284 fun make_clause(clause_id,axiom_name,kind,th) =
   285     let val (lits,ctypes_sorts) = literals_of_term (to_comb (prop_of th) [])
   286 	val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts
   287     in
   288 	if forall isFalse lits
   289 	then error "Problem too trivial for resolution (empty clause)"
   290 	else
   291 	    Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
   292 		    literals = lits, ctypes_sorts = ctypes_sorts, 
   293 		    ctvar_type_literals = ctvar_lits,
   294 		    ctfree_type_literals = ctfree_lits}
   295     end;
   296 
   297 
   298 fun add_axiom_clause ((th,(name,id)), pairs) =
   299   let val cls = make_clause(id, name, ResClause.Axiom, th)
   300   in
   301       if isTaut cls then pairs else (name,cls)::pairs
   302   end;
   303 
   304 val make_axiom_clauses = foldl add_axiom_clause [];
   305 
   306 fun make_conjecture_clauses_aux _ [] = []
   307   | make_conjecture_clauses_aux n (th::ths) =
   308       make_clause(n,"conjecture", ResClause.Conjecture, th) ::
   309       make_conjecture_clauses_aux (n+1) ths;
   310 
   311 val make_conjecture_clauses = make_conjecture_clauses_aux 0;
   312 
   313 
   314 (**********************************************************************)
   315 (* convert clause into ATP specific formats:                          *)
   316 (* TPTP used by Vampire and E                                         *)
   317 (* DFG used by SPASS                                                  *)
   318 (**********************************************************************)
   319 
   320 val type_wrapper = "typeinfo";
   321 
   322 fun wrap_type (c,tp) = case !typ_level of
   323 	T_FULL => type_wrapper ^ ResClause.paren_pack [c, ResClause.string_of_fol_type tp]
   324       | _ => c;
   325     
   326 
   327 val bool_tp = ResClause.make_fixed_type_const "bool";
   328 
   329 val app_str = "hAPP";
   330 
   331 val bool_str = "hBOOL";
   332 
   333 fun type_of_combterm (CombConst(c,tp,_)) = tp
   334   | type_of_combterm (CombFree(v,tp)) = tp
   335   | type_of_combterm (CombVar(v,tp)) = tp
   336   | type_of_combterm (CombApp(t1,t2,tp)) = tp;
   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 string_of_combterm2 (CombConst(c,tp,tvars)) = 
   359       let val tvars' = map ResClause.string_of_fol_type tvars
   360 	  val c' = if c = "equal" then "c_fequal" else c
   361       in
   362 	  c' ^ ResClause.paren_pack tvars'
   363       end
   364   | string_of_combterm2 (CombFree(v,tp)) = v
   365   | string_of_combterm2 (CombVar(v,tp)) = v
   366   | string_of_combterm2 (CombApp(t1,t2,_)) =
   367       app_str ^ ResClause.paren_pack [string_of_combterm2 t1, string_of_combterm2 t2];
   368 
   369 fun string_of_combterm t = 
   370     case !typ_level of T_CONST => string_of_combterm2 t
   371 		           | _ => string_of_combterm1 t;
   372 		           
   373 fun string_of_predicate (CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_)) =
   374       ("equal" ^ ResClause.paren_pack [string_of_combterm t1, string_of_combterm t2])
   375   | string_of_predicate t = 
   376       bool_str ^ ResClause.paren_pack [string_of_combterm t]
   377 
   378 fun string_of_clausename (cls_id,ax_name) = 
   379     ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   380 
   381 fun string_of_type_clsname (cls_id,ax_name,idx) = 
   382     string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   383 
   384 
   385 (*** tptp format ***)
   386 
   387 fun tptp_of_equality pol (t1,t2) =
   388   let val eqop = if pol then " = " else " != "
   389   in  string_of_combterm t1 ^ eqop ^ string_of_combterm t2  end;
   390 
   391 fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_))) = 
   392       tptp_of_equality pol (t1,t2)
   393   | tptp_literal (Literal(pol,pred)) = 
   394       ResClause.tptp_sign pol (string_of_predicate pred);
   395  
   396 fun tptp_type_lits (Clause cls) = 
   397     let val lits = map tptp_literal (#literals cls)
   398 	val ctvar_lits_strs =
   399 	    case !typ_level of T_NONE => []
   400 	      | _ => map ResClause.tptp_of_typeLit (#ctvar_type_literals cls)
   401 	val ctfree_lits = 
   402 	    case !typ_level of T_NONE => []
   403 	      | _ => map ResClause.tptp_of_typeLit (#ctfree_type_literals cls)
   404     in
   405 	(ctvar_lits_strs @ lits, ctfree_lits)
   406     end; 
   407     
   408     
   409 fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   410     let val (lits,ctfree_lits) = tptp_type_lits cls
   411 	val cls_str = ResClause.gen_tptp_cls(clause_id,axiom_name,kind,lits)
   412     in
   413 	(cls_str,ctfree_lits)
   414     end;
   415 
   416 
   417 (*** dfg format ***)
   418 
   419 fun dfg_literal (Literal(pol,pred)) = ResClause.dfg_sign pol (string_of_predicate pred);
   420 
   421 fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = 
   422   let val lits = map dfg_literal literals
   423       val (tvar_lits,tfree_lits) = ResClause.add_typs_aux ctypes_sorts
   424       val tvar_lits_strs = 
   425 	  case !typ_level of T_NONE => [] 
   426 	      | _ => map ResClause.dfg_of_typeLit tvar_lits
   427       val tfree_lits =
   428           case !typ_level of T_NONE => []
   429 	      | _ => map ResClause.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,tp)) vars = (v::vars)
   437   | get_uvars (CombApp(P,Q,tp)) 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,...}) = ResClause.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 = ResClause.get_tvar_strs ctypes_sorts
   447 	val knd = ResClause.name_of_kind kind
   448 	val lits_str = commas lits
   449 	val cls_str = ResClause.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) 
   450     in (cls_str, tfree_lits) end;
   451 
   452 
   453 fun init_funcs_tab funcs = 
   454     let val funcs1 = case !typ_level of T_PARTIAL => Symtab.update ("hAPP",3) funcs
   455 				      | _ => Symtab.update ("hAPP",2) funcs
   456     in
   457 	Symtab.update ("typeinfo",2) funcs1
   458     end;
   459 
   460 
   461 fun add_funcs (CombConst(c,_,tvars),funcs) =
   462       if c = "equal" then foldl ResClause.add_foltype_funcs funcs tvars
   463       else
   464 	(case !typ_level of
   465 	     T_CONST => foldl ResClause.add_foltype_funcs (Symtab.update(c,length tvars) funcs) tvars
   466            | _ => foldl ResClause.add_foltype_funcs (Symtab.update(c,0) funcs) tvars)
   467   | add_funcs (CombFree(v,ctp),funcs) = ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs) 
   468   | add_funcs (CombVar(_,ctp),funcs) = ResClause.add_foltype_funcs (ctp,funcs)
   469   | add_funcs (CombApp(P,Q,_),funcs) = add_funcs(P,add_funcs (Q,funcs));
   470 
   471 fun add_literal_funcs (Literal(_,c), funcs) = add_funcs (c,funcs);
   472 
   473 fun add_clause_funcs (Clause {literals, ...}, funcs) =
   474     foldl add_literal_funcs funcs literals
   475     handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
   476 
   477 fun funcs_of_clauses clauses arity_clauses =
   478     Symtab.dest (foldl ResClause.add_arityClause_funcs 
   479                        (foldl add_clause_funcs (init_funcs_tab Symtab.empty) clauses)
   480                        arity_clauses)
   481 
   482 fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
   483   foldl ResClause.add_type_sort_preds preds ctypes_sorts
   484   handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
   485 
   486 (*Higher-order clauses have only the predicates hBOOL and type classes.*)
   487 fun preds_of_clauses clauses clsrel_clauses arity_clauses = 
   488     Symtab.dest
   489 	(foldl ResClause.add_classrelClause_preds 
   490 	       (foldl ResClause.add_arityClause_preds
   491 		      (Symtab.update ("hBOOL",1) 
   492 		        (foldl add_clause_preds Symtab.empty clauses))
   493 		      arity_clauses)
   494 	       clsrel_clauses)
   495 
   496 
   497 
   498 (**********************************************************************)
   499 (* write clauses to files                                             *)
   500 (**********************************************************************)
   501 
   502 
   503 val init_counters =
   504     Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
   505 		 ("c_COMBB", 0), ("c_COMBC", 0),
   506 		 ("c_COMBS", 0), ("c_COMBB_e", 0),
   507 		 ("c_COMBC_e", 0), ("c_COMBS_e", 0)];
   508                 
   509 fun count_combterm (CombConst(c,tp,_), ct) = 
   510      (case Symtab.lookup ct c of NONE => ct  (*no counter*)
   511                                | SOME n => Symtab.update (c,n+1) ct)
   512   | count_combterm (CombFree(v,tp), ct) = ct
   513   | count_combterm (CombVar(v,tp), ct) = ct
   514   | count_combterm (CombApp(t1,t2,tp), ct) = count_combterm(t1, count_combterm(t2, ct));
   515 
   516 fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
   517 
   518 fun count_clause (Clause{literals,...}, ct) = foldl count_literal ct literals;
   519 
   520 fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) = 
   521   if axiom_name mem_string user_lemmas then foldl count_literal ct literals
   522   else ct;
   523 
   524 val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
   525 
   526 fun get_helper_clauses ct =
   527     let fun needed c = valOf (Symtab.lookup ct c) > 0
   528         val IK = if needed "c_COMBI" orelse needed "c_COMBK" 
   529                  then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) 
   530                  else []
   531 	val BC = if needed "c_COMBB" orelse needed "c_COMBC" 
   532 	         then (Output.debug "Include combinator B C"; cnf_helper_thms [comb_B,comb_C]) 
   533 	         else []
   534 	val S = if needed "c_COMBS" 
   535 	        then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S]) 
   536 	        else []
   537 	val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e" 
   538 	           then (Output.debug "Include combinator B' C'"; cnf_helper_thms [comb_B', comb_C']) 
   539 	           else []
   540 	val S' = if needed "c_COMBS_e" 
   541 	         then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S']) 
   542 	         else []
   543 	val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
   544     in
   545 	make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S')
   546     end
   547 
   548 (* tptp format *)
   549 						  
   550 (* write TPTP format to a single file *)
   551 fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas =
   552     let val conjectures = make_conjecture_clauses thms
   553         val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses)
   554 	val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
   555 	val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   556 	val out = TextIO.openOut filename
   557 	val ct = foldl (count_user_clause user_lemmas) 
   558 	            (foldl count_clause init_counters conjectures)
   559 	            axclauses'
   560 	val helper_clauses = map #2 (get_helper_clauses ct)
   561     in
   562 	List.app (curry TextIO.output out o #1 o clause2tptp) axclauses';
   563 	ResClause.writeln_strs out tfree_clss;
   564 	ResClause.writeln_strs out tptp_clss;
   565 	List.app (curry TextIO.output out o ResClause.tptp_classrelClause) classrel_clauses;
   566 	List.app (curry TextIO.output out o ResClause.tptp_arity_clause) arity_clauses;
   567 	List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
   568 	TextIO.closeOut out;
   569 	clnames
   570     end;
   571 
   572 
   573 
   574 (* dfg format *)
   575 
   576 fun dfg_write_file  thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas =
   577     let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) 
   578 	val conjectures = make_conjecture_clauses thms
   579         val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses)
   580 	val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   581 	and probname = Path.pack (Path.base (Path.unpack filename))
   582 	val axstrs = map (#1 o clause2dfg) axclauses'
   583 	val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss)
   584 	val out = TextIO.openOut filename
   585 	val ct = foldl (count_user_clause user_lemmas) 
   586 	            (foldl count_clause init_counters conjectures)
   587 	            axclauses'
   588 	val helper_clauses = map #2 (get_helper_clauses ct)
   589 	val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses
   590 	val funcs = funcs_of_clauses (helper_clauses @ conjectures @ axclauses') arity_clauses
   591 	and preds = preds_of_clauses axclauses' classrel_clauses arity_clauses
   592     in
   593 	TextIO.output (out, ResClause.string_of_start probname); 
   594 	TextIO.output (out, ResClause.string_of_descrip probname); 
   595 	TextIO.output (out, ResClause.string_of_symbols (ResClause.string_of_funcs funcs) (ResClause.string_of_preds preds)); 
   596 	TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
   597 	ResClause.writeln_strs out axstrs;
   598 	List.app (curry TextIO.output out o ResClause.dfg_classrelClause) classrel_clauses;
   599 	List.app (curry TextIO.output out o ResClause.dfg_arity_clause) arity_clauses;
   600 	ResClause.writeln_strs out helper_clauses_strs;
   601 	TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   602 	ResClause.writeln_strs out tfree_clss;
   603 	ResClause.writeln_strs out dfg_clss;
   604 	TextIO.output (out, "end_of_list.\n\n");
   605 	(*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   606 	TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
   607 	TextIO.output (out, "end_problem.\n");
   608 	TextIO.closeOut out;
   609 	clnames
   610     end;
   611 
   612 end