src/HOL/Tools/res_hol_clause.ML
author paulson
Thu Nov 16 17:06:24 2006 +0100 (2006-11-16)
changeset 21398 11996e938dfe
parent 21254 d53f76357f41
child 21470 7c1b59ddcd56
permissions -rw-r--r--
Includes type:sort constraints in its code to collect predicates in axiom clauses.
     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 
     8 structure ResHolClause =
     9 
    10 struct
    11 
    12 (* theorems for combinators and function extensionality *)
    13 val ext = thm "HOL.ext";
    14 val comb_I = thm "ATP_Linkup.COMBI_def";
    15 val comb_K = thm "ATP_Linkup.COMBK_def";
    16 val comb_B = thm "ATP_Linkup.COMBB_def";
    17 val comb_C = thm "ATP_Linkup.COMBC_def";
    18 val comb_S = thm "ATP_Linkup.COMBS_def";
    19 val comb_B' = thm "ATP_Linkup.COMBB'_def";
    20 val comb_C' = thm "ATP_Linkup.COMBC'_def";
    21 val comb_S' = thm "ATP_Linkup.COMBS'_def";
    22 val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
    23 val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
    24 
    25 (*A flag to set if we use the Turner optimizations. Currently FALSE, as the 5 standard
    26   combinators appear to work best.*)
    27 val use_Turner = ref false;
    28 
    29 (*FIXME: these refs should probaby replaced by code to count the combinators in the 
    30   translated form of the term.*)
    31 val combI_count = ref 0;
    32 val combK_count = ref 0;
    33 val combB_count = ref 0;
    34 val combC_count = ref 0;
    35 val combS_count = ref 0;
    36 
    37 val combB'_count = ref 0;
    38 val combC'_count = ref 0;
    39 val combS'_count = ref 0; 
    40 
    41 
    42 fun increI count_comb =  if count_comb then combI_count := !combI_count + 1 else ();
    43 fun increK count_comb =  if count_comb then combK_count := !combK_count + 1 else ();
    44 fun increB count_comb =  if count_comb then combB_count := !combB_count + 1 else ();
    45 fun increC count_comb =  if count_comb then combC_count := !combC_count + 1 else ();
    46 fun increS count_comb =  if count_comb then combS_count := !combS_count + 1 else (); 
    47 fun increB' count_comb =  if count_comb then combB'_count := !combB'_count + 1 else (); 
    48 fun increC' count_comb =  if count_comb then combC'_count := !combC'_count + 1 else ();
    49 fun increS' count_comb =  if count_comb then combS'_count := !combS'_count + 1 else (); 
    50 
    51 
    52 exception DECRE_COMB of string;
    53 fun decreB count_comb n = 
    54   if count_comb then 
    55     if !combB_count >= n then combB_count := !combB_count - n else raise DECRE_COMB "COMBB"
    56   else ();
    57 
    58 fun decreC count_comb n =
    59   if count_comb then 
    60     if !combC_count >= n then combC_count := !combC_count - n else raise DECRE_COMB "COMBC"
    61   else ();
    62 
    63 fun decreS count_comb n = 
    64   if count_comb then 
    65     if !combS_count >= n then combS_count := !combS_count - n else raise DECRE_COMB "COMBS"
    66   else ();
    67 
    68 val const_typargs = ref (Library.K [] : (string*typ -> typ list));
    69 
    70 fun init thy = (combI_count:=0; combK_count:=0;combB_count:=0;combC_count:=0;combS_count:=0;combB'_count:=0;combC'_count:=0;combS'_count:=0;
    71                 const_typargs := Sign.const_typargs thy);
    72 
    73 (**********************************************************************)
    74 (* convert a Term.term with lambdas into a Term.term with combinators *) 
    75 (**********************************************************************)
    76 
    77 fun is_free (Bound(a)) n = (a = n)
    78   | is_free (Abs(x,_,b)) n = (is_free b (n+1))
    79   | is_free (P $ Q) n = ((is_free P n) orelse (is_free Q n))
    80   | is_free _ _ = false;
    81 
    82 
    83 (*******************************************)
    84 fun mk_compact_comb (tm as (Const("ATP_Linkup.COMBB",_)$p) $ (Const("ATP_Linkup.COMBB",_)$q$r)) Bnds count_comb =
    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 = Term.type_of1(Bnds,tm)
    89 	val typ_B' = [tp_p,tp_q,tp_r] ---> typ
    90 	val _ = increB' count_comb
    91 	val _ = decreB count_comb 2
    92     in
    93 	Const("ATP_Linkup.COMBB'",typ_B') $ p $ q $ r
    94     end
    95   | mk_compact_comb (tm as (Const("ATP_Linkup.COMBC",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) Bnds count_comb =
    96     let val tp_p = Term.type_of1(Bnds,p)
    97 	val tp_q = Term.type_of1(Bnds,q)
    98 	val tp_r = Term.type_of1(Bnds,r)
    99 	val typ = Term.type_of1(Bnds,tm)
   100 	val typ_C' = [tp_p,tp_q,tp_r] ---> typ
   101 	val _ = increC' count_comb
   102 	val _ = decreC count_comb 1
   103 	val _ = decreB count_comb 1
   104     in
   105 	Const("ATP_Linkup.COMBC'",typ_C') $ p $ q $ r
   106     end
   107   | mk_compact_comb (tm as (Const("ATP_Linkup.COMBS",_) $ (Const("ATP_Linkup.COMBB",_)$p$q) $ r)) Bnds count_comb =
   108     let val tp_p = Term.type_of1(Bnds,p)
   109 	val tp_q = Term.type_of1(Bnds,q)
   110 	val tp_r = Term.type_of1(Bnds,r)
   111 	val typ = Term.type_of1(Bnds,tm)
   112 	val typ_S' = [tp_p,tp_q,tp_r] ---> typ
   113 	val _ = increS' count_comb
   114 	val _ = decreS count_comb 1
   115 	val _ = decreB count_comb 1
   116     in
   117 	Const("ATP_Linkup.COMBS'",typ_S') $ p $ q $ r
   118     end
   119   | mk_compact_comb tm _ _ = tm;
   120 
   121 fun compact_comb t Bnds count_comb = 
   122   if !use_Turner then mk_compact_comb t Bnds count_comb else t;
   123 
   124 fun lam2comb (Abs(x,tp,Bound 0)) _ count_comb = 
   125       let val _ = increI count_comb
   126       in 
   127 	  Const("ATP_Linkup.COMBI",tp-->tp) 
   128       end
   129   | lam2comb (Abs(x,tp,Bound n)) Bnds count_comb = 
   130       let val tb = List.nth(Bnds,n-1)
   131 	  val _ = increK count_comb 
   132       in
   133 	  Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ (Bound (n-1))
   134       end
   135   | lam2comb (Abs(x,t1,Const(c,t2))) _ count_comb = 
   136       let val _ = increK count_comb 
   137       in 
   138 	  Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Const(c,t2) 
   139       end
   140   | lam2comb (Abs(x,t1,Free(v,t2))) _ count_comb =
   141       let val _ = increK count_comb
   142       in
   143 	  Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Free(v,t2)
   144       end
   145   | lam2comb (Abs(x,t1,Var(ind,t2))) _ count_comb =
   146       let val _ = increK count_comb 
   147       in
   148 	  Const("ATP_Linkup.COMBK", [t2,t1] ---> t2) $ Var(ind,t2)
   149       end
   150   | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) Bnds count_comb =
   151       let val tr = Term.type_of1(t1::Bnds,P)
   152       in
   153 	  if not(is_free P 0) then (incr_boundvars ~1 P)
   154 	  else 
   155 	  let val tI = [t1] ---> t1
   156 	      val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   157 	      val tp' = Term.type_of1(Bnds,P')
   158 	      val tS = [tp',tI] ---> tr
   159 	      val _ = increI count_comb
   160 	      val _ = increS count_comb
   161 	  in
   162 	      compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ 
   163 	                     Const("ATP_Linkup.COMBI",tI)) Bnds count_comb
   164 	  end
   165       end	    
   166   | lam2comb (t as (Abs(x,t1,P$Q))) Bnds count_comb =
   167       let val nfreeP = not(is_free P 0)
   168 	  and nfreeQ = not(is_free Q 0)
   169 	  val tpq = Term.type_of1(t1::Bnds, P$Q) 
   170       in
   171 	  if nfreeP andalso nfreeQ 
   172 	  then 
   173 	    let val tK = [tpq,t1] ---> tpq
   174 		val PQ' = incr_boundvars ~1(P $ Q)
   175 		val _ = increK count_comb
   176 	    in 
   177 		Const("ATP_Linkup.COMBK",tK) $ PQ'
   178 	    end
   179 	  else if nfreeP then 
   180 	    let val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb
   181 		val P' = incr_boundvars ~1 P
   182 		val tp = Term.type_of1(Bnds,P')
   183 		val tq' = Term.type_of1(Bnds, Q')
   184 		val tB = [tp,tq',t1] ---> tpq
   185 		val _ = increB count_comb
   186 	    in
   187 		compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') Bnds count_comb 
   188 	    end
   189 	  else if nfreeQ then 
   190 	    let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   191 		val Q' = incr_boundvars ~1 Q
   192 		val tq = Term.type_of1(Bnds,Q')
   193 		val tp' = Term.type_of1(Bnds, P')
   194 		val tC = [tp',tq,t1] ---> tpq
   195 		val _ = increC count_comb
   196 	    in
   197 		compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') Bnds count_comb
   198 	    end
   199           else
   200 	    let val P' = lam2comb (Abs(x,t1,P)) Bnds count_comb
   201 		val Q' = lam2comb (Abs(x,t1,Q)) Bnds count_comb 
   202 		val tp' = Term.type_of1(Bnds,P')
   203 		val tq' = Term.type_of1(Bnds,Q')
   204 		val tS = [tp',tq',t1] ---> tpq
   205 		val _ = increS count_comb
   206 	    in
   207 		compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') Bnds count_comb
   208 	    end
   209       end
   210   | lam2comb (t as (Abs(x,t1,_))) _ _ = raise ResClause.CLAUSE("HOL CLAUSE",t);
   211 
   212 (*********************)
   213 
   214 fun to_comb (Abs(x,tp,b)) Bnds count_comb =
   215     let val b' = to_comb b (tp::Bnds) count_comb
   216     in lam2comb (Abs(x,tp,b')) Bnds count_comb end
   217   | to_comb (P $ Q) Bnds count_comb = ((to_comb P Bnds count_comb) $ (to_comb Q Bnds count_comb))
   218   | to_comb t _ _ = t;
   219  
   220    
   221 fun comb_of t count_comb = to_comb t [] count_comb;
   222  
   223 (* print a term containing combinators, used for debugging *)
   224 exception TERM_COMB of term;
   225 
   226 fun string_of_term (Const(c,t)) = c
   227   | string_of_term (Free(v,t)) = v
   228   | string_of_term (Var((x,n),t)) = x ^ "_" ^ (string_of_int n)
   229   | string_of_term (P $ Q) =
   230       "(" ^ string_of_term P ^ " " ^ string_of_term Q ^ ")" 
   231   | string_of_term t =  raise TERM_COMB (t);
   232 
   233 
   234 
   235 (******************************************************)
   236 (* data types for typed combinator expressions        *)
   237 (******************************************************)
   238 
   239 datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE;
   240 
   241 val typ_level = ref T_CONST;
   242 
   243 fun full_types () = (typ_level:=T_FULL);
   244 fun partial_types () = (typ_level:=T_PARTIAL);
   245 fun const_types_only () = (typ_level:=T_CONST);
   246 fun no_types () = (typ_level:=T_NONE);
   247 
   248 
   249 fun find_typ_level () = !typ_level;
   250 
   251 
   252 type axiom_name = string;
   253 datatype kind = Axiom | Conjecture;
   254 
   255 fun name_of_kind Axiom = "axiom"
   256   | name_of_kind Conjecture = "conjecture";
   257 
   258 type polarity = bool;
   259 type indexname = Term.indexname;
   260 type clause_id = int;
   261 type csort = Term.sort;
   262 type ctyp = ResClause.fol_type;
   263 
   264 val string_of_ctyp = ResClause.string_of_fol_type;
   265 
   266 type ctyp_var = ResClause.typ_var;
   267 
   268 type ctype_literal = ResClause.type_literal;
   269 
   270 
   271 datatype combterm = CombConst of string * ctyp * ctyp list
   272 		  | CombFree of string * ctyp
   273 		  | CombVar of string * ctyp
   274 		  | CombApp of combterm * combterm * ctyp
   275 		  | Bool of combterm;
   276 		  
   277 datatype literal = Literal of polarity * combterm;
   278 
   279 datatype clause = 
   280 	 Clause of {clause_id: clause_id,
   281 		    axiom_name: axiom_name,
   282 		    th: thm,
   283 		    kind: kind,
   284 		    literals: literal list,
   285 		    ctypes_sorts: (ctyp_var * csort) list, 
   286                     ctvar_type_literals: ctype_literal list, 
   287                     ctfree_type_literals: ctype_literal list};
   288 
   289 
   290 fun string_of_kind (Clause cls) = name_of_kind (#kind cls);
   291 fun get_axiomName (Clause cls) = #axiom_name cls;
   292 fun get_clause_id (Clause cls) = #clause_id cls;
   293 
   294 fun get_literals (c as Clause(cls)) = #literals cls;
   295 
   296 
   297 (*********************************************************************)
   298 (* convert a clause with type Term.term to a clause with type clause *)
   299 (*********************************************************************)
   300 
   301 fun isFalse (Literal(pol,Bool(CombConst(c,_,_)))) =
   302       (pol andalso c = "c_False") orelse
   303       (not pol andalso c = "c_True")
   304   | isFalse _ = false;
   305 
   306 
   307 fun isTrue (Literal (pol,Bool(CombConst(c,_,_)))) =
   308       (pol andalso c = "c_True") orelse
   309       (not pol andalso c = "c_False")
   310   | isTrue _ = false;
   311   
   312 fun isTaut (Clause {literals,...}) = exists isTrue literals;  
   313 
   314 fun type_of (Type (a, Ts)) =
   315     let val (folTypes,ts) = types_of Ts
   316 	val t = ResClause.make_fixed_type_const a
   317     in
   318 	(ResClause.mk_fol_type("Comp",t,folTypes),ts)
   319     end
   320   | type_of (tp as (TFree(a,s))) =
   321     let val t = ResClause.make_fixed_type_var a
   322     in
   323 	(ResClause.mk_fol_type("Fixed",t,[]),[ResClause.mk_typ_var_sort tp])
   324     end
   325   | type_of (tp as (TVar(v,s))) =
   326     let val t = ResClause.make_schematic_type_var v
   327     in
   328 	(ResClause.mk_fol_type("Var",t,[]),[ResClause.mk_typ_var_sort tp])
   329     end
   330 
   331 and types_of Ts =
   332     let val foltyps_ts = map type_of Ts
   333 	val (folTyps,ts) = ListPair.unzip foltyps_ts
   334     in
   335 	(folTyps,ResClause.union_all ts)
   336     end;
   337 
   338 (* same as above, but no gathering of sort information *)
   339 fun simp_type_of (Type (a, Ts)) = 
   340     let val typs = map simp_type_of Ts
   341 	val t = ResClause.make_fixed_type_const a
   342     in
   343 	ResClause.mk_fol_type("Comp",t,typs)
   344     end
   345   | simp_type_of (TFree (a,s)) = ResClause.mk_fol_type("Fixed",ResClause.make_fixed_type_var a,[])
   346   | simp_type_of (TVar (v,s)) = ResClause.mk_fol_type("Var",ResClause.make_schematic_type_var v,[]);
   347 
   348 
   349 fun const_type_of (c,t) =
   350     let val (tp,ts) = type_of t
   351 	val tvars = !const_typargs(c,t)
   352 	val tvars' = map simp_type_of tvars
   353     in
   354 	(tp,ts,tvars')
   355     end;
   356 
   357 
   358 fun is_bool_type (Type("bool",[])) = true
   359   | is_bool_type _ = false;
   360 
   361 
   362 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   363 fun combterm_of (Const(c,t)) =
   364     let val (tp,ts,tvar_list) = const_type_of (c,t)
   365 	val is_bool = is_bool_type t
   366 	val c' = CombConst(ResClause.make_fixed_const c,tp,tvar_list)
   367 	val c'' = if is_bool then Bool(c') else c'
   368     in
   369 	(c'',ts)
   370     end
   371   | combterm_of (Free(v,t)) =
   372     let val (tp,ts) = type_of t
   373 	val is_bool = is_bool_type t
   374 	val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp)
   375 		 else CombFree(ResClause.make_fixed_var v,tp)
   376 	val v'' = if is_bool then Bool(v') else v'
   377     in
   378 	(v'',ts)
   379     end
   380   | combterm_of (Var(v,t)) =
   381     let val (tp,ts) = type_of t
   382 	val is_bool = is_bool_type t
   383 	val v' = CombVar(ResClause.make_schematic_var v,tp)
   384 	val v'' = if is_bool then Bool(v') else v'
   385     in
   386 	(v'',ts)
   387     end
   388   | combterm_of (t as (P $ Q)) =
   389     let val (P',tsP) = combterm_of P
   390 	val (Q',tsQ) = combterm_of Q
   391 	val tp = Term.type_of t
   392 	val tp' = simp_type_of tp
   393 	val is_bool = is_bool_type tp
   394 	val t' = CombApp(P',Q',tp')
   395 	val t'' = if is_bool then Bool(t') else t'
   396     in
   397 	(t'',tsP union tsQ)
   398     end;
   399 
   400 fun predicate_of ((Const("Not",_) $ P), polarity) =
   401     predicate_of (P, not polarity)
   402   | predicate_of (term,polarity) = (combterm_of term,polarity);
   403 
   404 
   405 fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
   406   | literals_of_term1 args (Const("op |",_) $ P $ Q) = 
   407     let val args' = literals_of_term1 args P
   408     in
   409 	literals_of_term1 args' Q
   410     end
   411   | literals_of_term1 (lits,ts) P =
   412     let val ((pred,ts'),pol) = predicate_of (P,true)
   413 	val lits' = Literal(pol,pred)::lits
   414     in
   415 	(lits',ts union ts')
   416     end;
   417 
   418 
   419 fun literals_of_term P = literals_of_term1 ([],[]) P;
   420 
   421 fun occurs a (CombVar(b,_)) = a = b
   422   | occurs a (CombApp(t1,t2,_)) = (occurs a t1) orelse (occurs a t2)
   423   | occurs _ _ = false
   424 
   425 fun too_general_terms (CombVar(v,_), t) = not (occurs v t)
   426   | too_general_terms _ = false;
   427 
   428 fun too_general_equality (Literal(true,(Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))))) =
   429       too_general_terms (t1,t2) orelse too_general_terms (t2,t1)
   430   | too_general_equality _ = false;
   431 
   432 (* forbid the literal hBOOL(V) *)
   433 fun too_general_bool (Literal(_,Bool(CombVar _))) = true
   434   | too_general_bool _ = false;
   435 
   436 (* making axiom and conjecture clauses *)
   437 exception MAKE_CLAUSE
   438 fun make_clause(clause_id,axiom_name,kind,thm,is_user) =
   439     let val term = prop_of thm
   440 	val term' = comb_of term is_user
   441 	val (lits,ctypes_sorts) = literals_of_term term'
   442 	val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts
   443     in
   444 	if forall isFalse lits
   445 	then error "Problem too trivial for resolution (empty clause)"
   446 	else if (!typ_level <> T_FULL) andalso kind=Axiom andalso 
   447 	        (forall too_general_equality lits orelse exists too_general_bool lits)
   448 	    then (Output.debug ("Omitting " ^ axiom_name ^ ": clause is too prolific"); 
   449 	          raise MAKE_CLAUSE) 
   450 	else
   451 	    Clause {clause_id = clause_id, axiom_name = axiom_name, th = thm, kind = kind,
   452 		    literals = lits, ctypes_sorts = ctypes_sorts, 
   453 		    ctvar_type_literals = ctvar_lits,
   454 		    ctfree_type_literals = ctfree_lits}
   455     end;
   456 
   457 
   458 fun make_axiom_clause thm (ax_name,cls_id,is_user) = 
   459       make_clause(cls_id,ax_name,Axiom,thm,is_user);
   460  
   461 fun make_axiom_clauses [] user_lemmas = []
   462   | make_axiom_clauses ((thm,(name,id))::thms) user_lemmas =
   463     let val is_user = name mem user_lemmas
   464 	val cls = SOME (make_axiom_clause thm (name,id,is_user)) 
   465 	          handle MAKE_CLAUSE => NONE
   466 	val clss = make_axiom_clauses thms user_lemmas
   467     in
   468 	case cls of NONE => clss
   469 		  | SOME(cls') => if isTaut cls' then clss 
   470 		                  else (name,cls')::clss
   471     end;
   472 
   473 
   474 fun make_conjecture_clauses_aux _ [] = []
   475   | make_conjecture_clauses_aux n (th::ths) =
   476       make_clause(n,"conjecture",Conjecture,th,true) ::
   477       make_conjecture_clauses_aux (n+1) ths;
   478 
   479 val make_conjecture_clauses = make_conjecture_clauses_aux 0;
   480 
   481 
   482 (**********************************************************************)
   483 (* convert clause into ATP specific formats:                          *)
   484 (* TPTP used by Vampire and E                                         *)
   485 (* DFG used by SPASS                                                  *)
   486 (**********************************************************************)
   487 
   488 val type_wrapper = "typeinfo";
   489 
   490 fun wrap_type (c,t) = 
   491     case !typ_level of T_FULL => type_wrapper ^ ResClause.paren_pack [c,t]
   492 		     | _ => c;
   493     
   494 
   495 val bool_tp = ResClause.make_fixed_type_const "bool";
   496 
   497 val app_str = "hAPP";
   498 
   499 val bool_str = "hBOOL";
   500 
   501 exception STRING_OF_COMBTERM of int;
   502 
   503 (* convert literals of clauses into strings *)
   504 fun string_of_combterm1_aux _ (CombConst(c,tp,_)) = 
   505     let val tp' = string_of_ctyp tp
   506 	val c' = if c = "equal" then "c_fequal" else c
   507     in
   508 	(wrap_type (c',tp'),tp')
   509     end
   510   | string_of_combterm1_aux _ (CombFree(v,tp)) = 
   511     let val tp' = string_of_ctyp tp
   512     in
   513 	(wrap_type (v,tp'),tp')
   514     end
   515   | string_of_combterm1_aux _ (CombVar(v,tp)) = 
   516     let val tp' = string_of_ctyp tp
   517     in
   518 	(wrap_type (v,tp'),tp')
   519     end
   520   | string_of_combterm1_aux is_pred (CombApp(t1,t2,tp)) =
   521     let val (s1,tp1) = string_of_combterm1_aux is_pred t1
   522 	val (s2,tp2) = string_of_combterm1_aux is_pred t2
   523 	val tp' = ResClause.string_of_fol_type tp
   524 	val r =	case !typ_level of
   525 	            T_FULL => type_wrapper ^ ResClause.paren_pack [(app_str ^ ResClause.paren_pack [s1,s2]),tp']
   526 		  | T_PARTIAL => app_str ^ ResClause.paren_pack [s1,s2,tp1]
   527 		  | T_NONE => app_str ^ ResClause.paren_pack [s1,s2]
   528 		  | T_CONST => raise STRING_OF_COMBTERM 1 (*should not happen, if happened may be a bug*)
   529     in	(r,tp')   end
   530   | string_of_combterm1_aux is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) =
   531     if is_pred then 
   532 	let val (s1,_) = string_of_combterm1_aux false t1
   533 	    val (s2,_) = string_of_combterm1_aux false t2
   534 	in
   535 	    ("equal" ^ ResClause.paren_pack [s1,s2], bool_tp)
   536 	end
   537     else
   538 	let val (t,_) = string_of_combterm1_aux false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))
   539 	in
   540 	    (t,bool_tp)
   541 	end
   542   | string_of_combterm1_aux is_pred (Bool(t)) = 
   543     let val (t',_) = string_of_combterm1_aux false t
   544 	val r = if is_pred then bool_str ^ ResClause.paren_pack [t']
   545 		else t'
   546     in
   547 	(r,bool_tp)
   548     end;
   549 
   550 fun string_of_combterm1 is_pred term = fst (string_of_combterm1_aux is_pred term);
   551 
   552 fun string_of_combterm2 _ (CombConst(c,tp,tvars)) = 
   553     let val tvars' = map string_of_ctyp tvars
   554 	val c' = if c = "equal" then "c_fequal" else c
   555     in
   556 	c' ^ ResClause.paren_pack tvars'
   557     end
   558   | string_of_combterm2 _ (CombFree(v,tp)) = v
   559   | string_of_combterm2 _ (CombVar(v,tp)) = v
   560   | string_of_combterm2 is_pred (CombApp(t1,t2,tp)) =
   561     let val s1 = string_of_combterm2 is_pred t1
   562 	val s2 = string_of_combterm2 is_pred t2
   563     in
   564 	app_str ^ ResClause.paren_pack [s1,s2]
   565     end
   566   | string_of_combterm2 is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) =
   567     if is_pred then 
   568 	let val s1 = string_of_combterm2 false t1
   569 	    val s2 = string_of_combterm2 false t2
   570 	in
   571 	    ("equal" ^ ResClause.paren_pack [s1,s2])
   572 	end
   573     else
   574 	string_of_combterm2 false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))
   575  
   576   | string_of_combterm2 is_pred (Bool(t)) = 
   577     let val t' = string_of_combterm2 false t
   578     in
   579 	if is_pred then bool_str ^ ResClause.paren_pack [t']
   580 	else t'
   581     end;
   582 
   583 fun string_of_combterm is_pred term = 
   584     case !typ_level of T_CONST => string_of_combterm2 is_pred term
   585 		     | _ => string_of_combterm1 is_pred term;
   586 
   587 fun string_of_clausename (cls_id,ax_name) = 
   588     ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   589 
   590 fun string_of_type_clsname (cls_id,ax_name,idx) = 
   591     string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   592 
   593 
   594 (* tptp format *)
   595 
   596 fun tptp_literal (Literal(pol,pred)) =
   597     let val pred_string = string_of_combterm true pred
   598 	val pol_str = if pol then "++" else "--"
   599     in
   600 	pol_str ^ pred_string
   601     end;
   602 
   603  
   604 fun tptp_type_lits (Clause cls) = 
   605     let val lits = map tptp_literal (#literals cls)
   606 	val ctvar_lits_strs =
   607 	    case !typ_level of T_NONE => []
   608 	      | _ => map ResClause.tptp_of_typeLit (#ctvar_type_literals cls)
   609 	val ctfree_lits = 
   610 	    case !typ_level of T_NONE => []
   611 	      | _ => map ResClause.tptp_of_typeLit (#ctfree_type_literals cls)
   612     in
   613 	(ctvar_lits_strs @ lits, ctfree_lits)
   614     end; 
   615     
   616     
   617 fun clause2tptp cls =
   618     let val (lits,ctfree_lits) = tptp_type_lits cls
   619 	val cls_id = get_clause_id cls
   620 	val ax_name = get_axiomName cls
   621 	val knd = string_of_kind cls
   622 	val lits_str = ResClause.bracket_pack lits
   623 	val cls_str = ResClause.gen_tptp_cls(cls_id,ax_name,knd,lits_str)
   624     in
   625 	(cls_str,ctfree_lits)
   626     end;
   627 
   628 
   629 (* dfg format *)
   630 fun dfg_literal (Literal(pol,pred)) = ResClause.dfg_sign pol (string_of_combterm true pred);
   631 
   632 fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = 
   633   let val lits = map dfg_literal literals
   634       val (tvar_lits,tfree_lits) = ResClause.add_typs_aux ctypes_sorts
   635       val tvar_lits_strs = 
   636 	  case !typ_level of T_NONE => [] 
   637 	      | _ => map ResClause.dfg_of_typeLit tvar_lits
   638       val tfree_lits =
   639           case !typ_level of T_NONE => []
   640 	      | _ => map ResClause.dfg_of_typeLit tfree_lits 
   641   in
   642       (tvar_lits_strs @ lits, tfree_lits)
   643   end; 
   644 
   645 fun get_uvars (CombConst(_,_,_)) vars = vars
   646   | get_uvars (CombFree(_,_)) vars = vars
   647   | get_uvars (CombVar(v,tp)) vars = (v::vars)
   648   | get_uvars (CombApp(P,Q,tp)) vars = get_uvars P (get_uvars Q vars)
   649   | get_uvars (Bool(c)) vars = get_uvars c vars;
   650 
   651 
   652 fun get_uvars_l (Literal(_,c)) = get_uvars c [];
   653 
   654 fun dfg_vars (Clause {literals,...}) = ResClause.union_all (map get_uvars_l literals);
   655  
   656 fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   657     let val (lits,tfree_lits) = dfg_clause_aux cls 
   658         val vars = dfg_vars cls
   659         val tvars = ResClause.get_tvar_strs ctypes_sorts
   660 	val knd = name_of_kind kind
   661 	val lits_str = commas lits
   662 	val cls_str = ResClause.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) 
   663     in (cls_str, tfree_lits) end;
   664 
   665 
   666 fun init_funcs_tab funcs = 
   667     let val tp = !typ_level
   668 	val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs
   669 				      | _ => Symtab.update ("hAPP",2) funcs
   670 	val funcs2 = case tp of T_FULL => Symtab.update ("typeinfo",2) funcs1
   671 				      | _ => funcs1
   672     in
   673 	funcs2
   674     end;
   675 
   676 
   677 fun add_funcs (CombConst(c,_,tvars),funcs) =
   678     if c = "equal" then foldl ResClause.add_foltype_funcs funcs tvars
   679     else
   680 	(case !typ_level of T_CONST => foldl ResClause.add_foltype_funcs (Symtab.update(c,length tvars) funcs) tvars
   681 			  | _ => foldl ResClause.add_foltype_funcs (Symtab.update(c,0) funcs) tvars)
   682   | add_funcs (CombFree(v,ctp),funcs) = ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs) 
   683   | add_funcs (CombVar(_,ctp),funcs) = ResClause.add_foltype_funcs (ctp,funcs)
   684   | add_funcs (CombApp(P,Q,_),funcs) = add_funcs(P,add_funcs (Q,funcs))
   685   | add_funcs (Bool(t),funcs) = add_funcs (t,funcs);
   686 
   687 
   688 fun add_literal_funcs (Literal(_,c), funcs) = add_funcs (c,funcs);
   689 
   690 fun add_clause_funcs (Clause {literals, ...}, funcs) =
   691     foldl add_literal_funcs funcs literals
   692     handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
   693 
   694 fun funcs_of_clauses clauses arity_clauses =
   695     Symtab.dest (foldl ResClause.add_arityClause_funcs 
   696                        (foldl add_clause_funcs (init_funcs_tab Symtab.empty) clauses)
   697                        arity_clauses)
   698 
   699 fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
   700   foldl ResClause.add_type_sort_preds preds ctypes_sorts
   701   handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
   702 
   703 (*Higher-order clauses have only the predicates hBOOL and type classes.*)
   704 fun preds_of_clauses clauses clsrel_clauses arity_clauses = 
   705     Symtab.dest
   706 	(foldl ResClause.add_classrelClause_preds 
   707 	       (foldl ResClause.add_arityClause_preds
   708 		      (Symtab.update ("hBOOL",1) 
   709 		        (foldl add_clause_preds Symtab.empty clauses))
   710 		      arity_clauses)
   711 	       clsrel_clauses)
   712 
   713 
   714 
   715 (**********************************************************************)
   716 (* write clauses to files                                             *)
   717 (**********************************************************************)
   718 
   719 val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
   720 
   721 (*Simulate the result of conversion to CNF*)
   722 fun pretend_cnf s = (thm s, (s,0));
   723 
   724 (*These theorems allow the proof of P=Q from P-->Q and Q-->P, so they are necessary for
   725   completeness. Unfortunately, they are very prolific, causing greatly increased runtimes.
   726   They also lead to many unsound proofs. Thus it is well that the "exists too_general_bool"
   727   test deletes them except with the full-typed translation.*)
   728 val iff_thms = [pretend_cnf "ATP_Linkup.iff_positive", 
   729                 pretend_cnf "ATP_Linkup.iff_negative"];
   730 
   731 fun get_helper_clauses () =
   732     let val IK = if !combI_count > 0 orelse !combK_count > 0 
   733                  then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) 
   734                  else []
   735 	val BC = if !combB_count > 0 orelse !combC_count > 0 
   736 	         then (Output.debug "Include combinator B C"; cnf_helper_thms [comb_B,comb_C]) 
   737 	         else []
   738 	val S = if !combS_count > 0 
   739 	        then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S]) 
   740 	        else []
   741 	val B'C' = if !combB'_count > 0 orelse !combC'_count > 0 
   742 	           then (Output.debug "Include combinator B' C'"; cnf_helper_thms [comb_B', comb_C']) 
   743 	           else []
   744 	val S' = if !combS'_count > 0 
   745 	         then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S']) 
   746 	         else []
   747 	val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
   748     in
   749 	make_axiom_clauses (iff_thms @ other @ IK @ BC @ S @ B'C' @ S') []
   750     end
   751 
   752 
   753 (* tptp format *)
   754 						  
   755 (* write TPTP format to a single file *)
   756 (* when "get_helper_clauses" is called, "include_combS" and "include_min_comb" should have correct values already *)
   757 fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas=
   758     let val clss = make_conjecture_clauses thms
   759         val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses user_lemmas)
   760 	val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
   761 	val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   762 	val out = TextIO.openOut filename
   763 	val helper_clauses = (#2 o ListPair.unzip o get_helper_clauses) ()
   764     in
   765 	List.app (curry TextIO.output out o #1 o clause2tptp) axclauses';
   766 	ResClause.writeln_strs out tfree_clss;
   767 	ResClause.writeln_strs out tptp_clss;
   768 	List.app (curry TextIO.output out o ResClause.tptp_classrelClause) classrel_clauses;
   769 	List.app (curry TextIO.output out o ResClause.tptp_arity_clause) arity_clauses;
   770 	List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
   771 	TextIO.closeOut out;
   772 	clnames
   773     end;
   774 
   775 
   776 
   777 (* dfg format *)
   778 
   779 fun dfg_write_file  thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas =
   780     let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) 
   781 	val conjectures = make_conjecture_clauses thms
   782         val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses user_lemmas)
   783 	val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   784 	and probname = Path.pack (Path.base (Path.unpack filename))
   785 	val (axstrs,_) =  ListPair.unzip (map clause2dfg axclauses')
   786 	val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss)
   787 	val out = TextIO.openOut filename
   788 	val helper_clauses = (#2 o ListPair.unzip o get_helper_clauses) ()
   789 	val helper_clauses_strs = (#1 o ListPair.unzip o (map clause2dfg)) helper_clauses
   790 	val funcs = funcs_of_clauses (helper_clauses @ conjectures @ axclauses') arity_clauses
   791 	and preds = preds_of_clauses axclauses' classrel_clauses arity_clauses
   792     in
   793 	TextIO.output (out, ResClause.string_of_start probname); 
   794 	TextIO.output (out, ResClause.string_of_descrip probname); 
   795 	TextIO.output (out, ResClause.string_of_symbols (ResClause.string_of_funcs funcs) (ResClause.string_of_preds preds)); 
   796 	TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
   797 	ResClause.writeln_strs out axstrs;
   798 	List.app (curry TextIO.output out o ResClause.dfg_classrelClause) classrel_clauses;
   799 	List.app (curry TextIO.output out o ResClause.dfg_arity_clause) arity_clauses;
   800 	ResClause.writeln_strs out helper_clauses_strs;
   801 	TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   802 	ResClause.writeln_strs out tfree_clss;
   803 	ResClause.writeln_strs out dfg_clss;
   804 	TextIO.output (out, "end_of_list.\n\n");
   805 	(*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   806 	TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
   807 	TextIO.output (out, "end_problem.\n");
   808 	TextIO.closeOut out;
   809 	clnames
   810     end;
   811 
   812 end