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--
```     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
```