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