src/HOL/Tools/res_hol_clause.ML
author mengj
Thu Oct 05 13:54:17 2006 +0200 (2006-10-05)
changeset 20865 2cfa020109c1
parent 20864 bb75b876b260
child 20953 1ea394dc2a0f
permissions -rw-r--r--
Changed and removed some functions related to combinators, since they are Isabelle constants now.
     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 
   356 fun const_type_of (c,t) =
   357     let val (tp,ts) = type_of t
   358 	val tvars = !const_typargs(c,t)
   359 	val tvars' = map simp_type_of tvars
   360     in
   361 	(tp,ts,tvars')
   362     end;
   363 
   364 
   365 fun is_bool_type (Type("bool",[])) = true
   366   | is_bool_type _ = false;
   367 
   368 
   369 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   370 fun combterm_of (Const(c,t)) =
   371     let val (tp,ts,tvar_list) = const_type_of (c,t)
   372 	val is_bool = is_bool_type t
   373 	val c' = CombConst(ResClause.make_fixed_const c,tp,tvar_list)
   374 	val c'' = if is_bool then Bool(c') else c'
   375     in
   376 	(c'',ts)
   377     end
   378   | combterm_of (Free(v,t)) =
   379     let val (tp,ts) = type_of t
   380 	val is_bool = is_bool_type t
   381 	val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp)
   382 		 else CombFree(ResClause.make_fixed_var v,tp)
   383 	val v'' = if is_bool then Bool(v') else v'
   384     in
   385 	(v'',ts)
   386     end
   387   | combterm_of (Var(v,t)) =
   388     let val (tp,ts) = type_of t
   389 	val is_bool = is_bool_type t
   390 	val v' = CombVar(ResClause.make_schematic_var v,tp)
   391 	val v'' = if is_bool then Bool(v') else v'
   392     in
   393 	(v'',ts)
   394     end
   395   | combterm_of (t as (P $ Q)) =
   396     let val (P',tsP) = combterm_of P
   397 	val (Q',tsQ) = combterm_of Q
   398 	val tp = Term.type_of t
   399 	val tp' = simp_type_of tp
   400 	val is_bool = is_bool_type tp
   401 	val t' = CombApp(P',Q',tp')
   402 	val t'' = if is_bool then Bool(t') else t'
   403     in
   404 	(t'',tsP union tsQ)
   405     end;
   406 
   407 fun predicate_of ((Const("Not",_) $ P), polarity) =
   408     predicate_of (P, not polarity)
   409   | predicate_of (term,polarity) = (combterm_of term,polarity);
   410 
   411 
   412 fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
   413   | literals_of_term1 args (Const("op |",_) $ P $ Q) = 
   414     let val args' = literals_of_term1 args P
   415     in
   416 	literals_of_term1 args' Q
   417     end
   418   | literals_of_term1 (lits,ts) P =
   419     let val ((pred,ts'),pol) = predicate_of (P,true)
   420 	val lits' = Literal(pol,pred)::lits
   421     in
   422 	(lits',ts union ts')
   423     end;
   424 
   425 
   426 fun literals_of_term P = literals_of_term1 ([],[]) P;
   427 
   428 fun occurs a (CombVar(b,_)) = a = b
   429   | occurs a (CombApp(t1,t2,_)) = (occurs a t1) orelse (occurs a t2)
   430   | occurs _ _ = false
   431 
   432 fun too_general_terms (CombVar(v,_), t) = not (occurs v t)
   433   | too_general_terms _ = false;
   434 
   435 fun too_general_lit (Literal(true,(Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))))) =
   436       too_general_terms (t1,t2) orelse too_general_terms (t2,t1)
   437   | too_general_lit _ = false;
   438 
   439 (* forbid a clause that contains hBOOL(V) *)
   440 fun too_general [] = false
   441   | too_general (lit::lits) = 
   442     case lit of Literal(_,Bool(CombVar(_,_))) => true
   443 	      | _ => too_general lits;
   444 
   445 (* making axiom and conjecture clauses *)
   446 exception MAKE_CLAUSE
   447 fun make_clause(clause_id,axiom_name,kind,thm,is_user) =
   448     let val term = prop_of thm
   449 	val term' = comb_of term is_user
   450 	val (lits,ctypes_sorts) = literals_of_term term'
   451 	val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts
   452     in
   453 	if forall isFalse lits
   454 	then error "Problem too trivial for resolution (empty clause)"
   455 	else if too_general lits 
   456 	then (Output.debug ("Omitting " ^ axiom_name ^ ": clause contains universal predicates"); 
   457 	     raise MAKE_CLAUSE)
   458 	else
   459 	    if (!typ_level <> T_FULL) andalso kind=Axiom andalso forall too_general_lit lits 
   460 	    then (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); 
   461 	          raise MAKE_CLAUSE) 
   462 	else
   463 	    Clause {clause_id = clause_id, axiom_name = axiom_name, th = thm, kind = kind,
   464 		    literals = lits, ctypes_sorts = ctypes_sorts, 
   465 		    ctvar_type_literals = ctvar_lits,
   466 		    ctfree_type_literals = ctfree_lits}
   467     end;
   468 
   469 
   470 fun make_axiom_clause thm (ax_name,cls_id,is_user) = 
   471       make_clause(cls_id,ax_name,Axiom,thm,is_user);
   472  
   473 fun make_axiom_clauses [] user_lemmas = []
   474   | make_axiom_clauses ((thm,(name,id))::thms) user_lemmas =
   475     let val is_user = name mem user_lemmas
   476 	val cls = SOME (make_axiom_clause thm (name,id,is_user)) 
   477 	          handle MAKE_CLAUSE => NONE
   478 	val clss = make_axiom_clauses thms user_lemmas
   479     in
   480 	case cls of NONE => clss
   481 		  | SOME(cls') => if isTaut cls' then clss 
   482 		                  else (name,cls')::clss
   483     end;
   484 
   485 
   486 fun make_conjecture_clauses_aux _ [] = []
   487   | make_conjecture_clauses_aux n (th::ths) =
   488       make_clause(n,"conjecture",Conjecture,th,true) ::
   489       make_conjecture_clauses_aux (n+1) ths;
   490 
   491 val make_conjecture_clauses = make_conjecture_clauses_aux 0;
   492 
   493 
   494 (**********************************************************************)
   495 (* convert clause into ATP specific formats:                          *)
   496 (* TPTP used by Vampire and E                                         *)
   497 (* DFG used by SPASS                                                  *)
   498 (**********************************************************************)
   499 
   500 val type_wrapper = "typeinfo";
   501 
   502 fun wrap_type (c,t) = 
   503     case !typ_level of T_FULL => type_wrapper ^ (ResClause.paren_pack [c,t])
   504 		     | _ => c;
   505     
   506 
   507 val bool_tp = ResClause.make_fixed_type_const "bool";
   508 
   509 val app_str = "hAPP";
   510 
   511 val bool_str = "hBOOL";
   512 
   513 exception STRING_OF_COMBTERM of int;
   514 
   515 (* convert literals of clauses into strings *)
   516 fun string_of_combterm1_aux _ (CombConst(c,tp,_)) = 
   517     let val tp' = string_of_ctyp tp
   518 	val c' = if c = "equal" then "c_fequal" else c
   519     in
   520 	(wrap_type (c',tp'),tp')
   521     end
   522   | string_of_combterm1_aux _ (CombFree(v,tp)) = 
   523     let val tp' = string_of_ctyp tp
   524     in
   525 	(wrap_type (v,tp'),tp')
   526     end
   527   | string_of_combterm1_aux _ (CombVar(v,tp)) = 
   528     let val tp' = string_of_ctyp tp
   529     in
   530 	(wrap_type (v,tp'),tp')
   531     end
   532   | string_of_combterm1_aux is_pred (CombApp(t1,t2,tp)) =
   533     let val (s1,tp1) = string_of_combterm1_aux is_pred t1
   534 	val (s2,tp2) = string_of_combterm1_aux is_pred t2
   535 	val tp' = ResClause.string_of_fol_type tp
   536 	val r =	case !typ_level of T_FULL => type_wrapper ^  (ResClause.paren_pack [(app_str ^ (ResClause.paren_pack [s1,s2])),tp'])
   537 				 | T_PARTIAL => app_str ^ (ResClause.paren_pack [s1,s2,tp1])
   538 				 | T_NONE => app_str ^ (ResClause.paren_pack [s1,s2])
   539 				 | T_CONST => raise STRING_OF_COMBTERM (1) (*should not happen, if happened may be a bug*)
   540     in	(r,tp')
   541 
   542     end
   543   | string_of_combterm1_aux is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) =
   544     if is_pred then 
   545 	let val (s1,_) = string_of_combterm1_aux false t1
   546 	    val (s2,_) = string_of_combterm1_aux false t2
   547 	in
   548 	    ("equal" ^ (ResClause.paren_pack [s1,s2]),bool_tp)
   549 	end
   550     else
   551 	let val (t,_) = string_of_combterm1_aux false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))
   552 	in
   553 	    (t,bool_tp)
   554 	end
   555   | string_of_combterm1_aux is_pred (Bool(t)) = 
   556     let val (t',_) = string_of_combterm1_aux false t
   557 	val r = if is_pred then bool_str ^ (ResClause.paren_pack [t'])
   558 		else t'
   559     in
   560 	(r,bool_tp)
   561     end;
   562 
   563 fun string_of_combterm1 is_pred term = fst (string_of_combterm1_aux is_pred term);
   564 
   565 fun string_of_combterm2 _ (CombConst(c,tp,tvars)) = 
   566     let val tvars' = map string_of_ctyp tvars
   567 	val c' = if c = "equal" then "c_fequal" else c
   568     in
   569 	c' ^ (ResClause.paren_pack tvars')
   570     end
   571   | string_of_combterm2 _ (CombFree(v,tp)) = v
   572   | string_of_combterm2 _ (CombVar(v,tp)) = v
   573   | string_of_combterm2 is_pred (CombApp(t1,t2,tp)) =
   574     let val s1 = string_of_combterm2 is_pred t1
   575 	val s2 = string_of_combterm2 is_pred t2
   576     in
   577 	app_str ^ (ResClause.paren_pack [s1,s2])
   578     end
   579   | string_of_combterm2 is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) =
   580     if is_pred then 
   581 	let val s1 = string_of_combterm2 false t1
   582 	    val s2 = string_of_combterm2 false t2
   583 	in
   584 	    ("equal" ^ (ResClause.paren_pack [s1,s2]))
   585 	end
   586     else
   587 	string_of_combterm2 false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))
   588  
   589   | string_of_combterm2 is_pred (Bool(t)) = 
   590     let val t' = string_of_combterm2 false t
   591     in
   592 	if is_pred then bool_str ^ (ResClause.paren_pack [t'])
   593 	else t'
   594     end;
   595 
   596 
   597 
   598 fun string_of_combterm is_pred term = 
   599     case !typ_level of T_CONST => string_of_combterm2 is_pred term
   600 		     | _ => string_of_combterm1 is_pred term;
   601 
   602 
   603 fun string_of_clausename (cls_id,ax_name) = 
   604     ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   605 
   606 fun string_of_type_clsname (cls_id,ax_name,idx) = 
   607     string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   608 
   609 
   610 (* tptp format *)
   611 
   612 fun tptp_literal (Literal(pol,pred)) =
   613     let val pred_string = string_of_combterm true pred
   614 	val pol_str = if pol then "++" else "--"
   615     in
   616 	pol_str ^ pred_string
   617     end;
   618 
   619  
   620 fun tptp_type_lits (Clause cls) = 
   621     let val lits = map tptp_literal (#literals cls)
   622 	val ctvar_lits_strs =
   623 	    case !typ_level of T_NONE => []
   624 	      | _ => map ResClause.tptp_of_typeLit (#ctvar_type_literals cls)
   625 	val ctfree_lits = 
   626 	    case !typ_level of T_NONE => []
   627 	      | _ => map ResClause.tptp_of_typeLit (#ctfree_type_literals cls)
   628     in
   629 	(ctvar_lits_strs @ lits, ctfree_lits)
   630     end; 
   631     
   632     
   633 fun clause2tptp cls =
   634     let val (lits,ctfree_lits) = tptp_type_lits cls
   635 	val cls_id = get_clause_id cls
   636 	val ax_name = get_axiomName cls
   637 	val knd = string_of_kind cls
   638 	val lits_str = ResClause.bracket_pack lits
   639 	val cls_str = ResClause.gen_tptp_cls(cls_id,ax_name,knd,lits_str)
   640     in
   641 	(cls_str,ctfree_lits)
   642     end;
   643 
   644 
   645 (* dfg format *)
   646 fun dfg_literal (Literal(pol,pred)) = ResClause.dfg_sign pol (string_of_combterm true pred);
   647 
   648 fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = 
   649   let val lits = map dfg_literal literals
   650       val (tvar_lits,tfree_lits) = ResClause.add_typs_aux ctypes_sorts
   651       val tvar_lits_strs = 
   652 	  case !typ_level of T_NONE => [] 
   653 	      | _ => map ResClause.dfg_of_typeLit tvar_lits
   654       val tfree_lits =
   655           case !typ_level of T_NONE => []
   656 	      | _ => map ResClause.dfg_of_typeLit tfree_lits 
   657   in
   658       (tvar_lits_strs @ lits, tfree_lits)
   659   end; 
   660 
   661 fun get_uvars (CombConst(_,_,_)) vars = vars
   662   | get_uvars (CombFree(_,_)) vars = vars
   663   | get_uvars (CombVar(v,tp)) vars = (v::vars)
   664   | get_uvars (CombApp(P,Q,tp)) vars = get_uvars P (get_uvars Q vars)
   665   | get_uvars (Bool(c)) vars = get_uvars c vars;
   666 
   667 
   668 fun get_uvars_l (Literal(_,c)) = get_uvars c [];
   669 
   670 fun dfg_vars (Clause {literals,...}) = ResClause.union_all (map get_uvars_l literals);
   671  
   672 fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   673     let val (lits,tfree_lits) = dfg_clause_aux cls 
   674         val vars = dfg_vars cls
   675         val tvars = ResClause.get_tvar_strs ctypes_sorts
   676 	val knd = name_of_kind kind
   677 	val lits_str = commas lits
   678 	val cls_str = ResClause.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) 
   679     in (cls_str, tfree_lits) end;
   680 
   681 
   682 fun init_funcs_tab funcs = 
   683     let val tp = !typ_level
   684 	val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs
   685 				      | _ => Symtab.update ("hAPP",2) funcs
   686 	val funcs2 = case tp of T_FULL => Symtab.update ("typeinfo",2) funcs1
   687 				      | _ => funcs1
   688     in
   689 	funcs2
   690     end;
   691 
   692 
   693 fun add_funcs (CombConst(c,_,tvars),funcs) =
   694     if c = "equal" then foldl ResClause.add_foltype_funcs funcs tvars
   695     else
   696 	(case !typ_level of T_CONST => foldl ResClause.add_foltype_funcs (Symtab.update(c,length tvars) funcs) tvars
   697 			  | _ => foldl ResClause.add_foltype_funcs (Symtab.update(c,0) funcs) tvars)
   698   | add_funcs (CombFree(v,ctp),funcs) = ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs) 
   699   | add_funcs (CombVar(_,ctp),funcs) = ResClause.add_foltype_funcs (ctp,funcs)
   700   | add_funcs (CombApp(P,Q,_),funcs) = add_funcs(P,add_funcs (Q,funcs))
   701   | add_funcs (Bool(t),funcs) = add_funcs (t,funcs);
   702 
   703 
   704 fun add_literal_funcs (Literal(_,c), funcs) = add_funcs (c,funcs);
   705 
   706 fun add_clause_funcs (Clause {literals, ...}, funcs) =
   707     foldl add_literal_funcs funcs literals
   708     handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
   709 
   710 fun funcs_of_clauses clauses arity_clauses =
   711     Symtab.dest (foldl ResClause.add_arityClause_funcs 
   712                        (foldl add_clause_funcs (init_funcs_tab Symtab.empty) clauses)
   713                        arity_clauses)
   714 
   715 fun preds_of clsrel_clauses arity_clauses = 
   716     Symtab.dest
   717 	(foldl ResClause.add_classrelClause_preds 
   718 	       (foldl ResClause.add_arityClause_preds
   719 		      (Symtab.update ("hBOOL",1) Symtab.empty)
   720 		      arity_clauses)
   721 	       clsrel_clauses)
   722 
   723 
   724 (**********************************************************************)
   725 (* write clauses to files                                             *)
   726 (**********************************************************************)
   727 
   728 local
   729 
   730 val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
   731 
   732 in
   733 
   734 fun get_helper_clauses () =
   735     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 []
   736 	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 []
   737 	val S = if !combS_count > 0 then (Output.debug "Include combinator S"; cnf_helper_thms [comb_S]) else []
   738 	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 []
   739 	val S' = if !combS'_count > 0 then (Output.debug "Include combinator S'"; cnf_helper_thms [comb_S']) else []
   740 	val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
   741     in
   742 	make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S') []
   743     end
   744 
   745 end
   746 
   747 (* tptp format *)
   748 						  
   749 (* write TPTP format to a single file *)
   750 (* when "get_helper_clauses" is called, "include_combS" and "include_min_comb" should have correct values already *)
   751 fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas=
   752     let val clss = make_conjecture_clauses thms
   753         val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses user_lemmas)
   754 	val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
   755 	val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   756 	val out = TextIO.openOut filename
   757 	val helper_clauses = (#2 o ListPair.unzip o get_helper_clauses) ()
   758     in
   759 	List.app (curry TextIO.output out o #1 o clause2tptp) axclauses';
   760 	ResClause.writeln_strs out tfree_clss;
   761 	ResClause.writeln_strs out tptp_clss;
   762 	List.app (curry TextIO.output out o ResClause.tptp_classrelClause) classrel_clauses;
   763 	List.app (curry TextIO.output out o ResClause.tptp_arity_clause) arity_clauses;
   764 	List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
   765 	TextIO.closeOut out;
   766 	clnames
   767     end;
   768 
   769 
   770 
   771 (* dfg format *)
   772 
   773 fun dfg_write_file  thms filename (axclauses,classrel_clauses,arity_clauses) user_lemmas =
   774     let val _ = Output.debug ("Preparing to write the DFG file " ^ filename) 
   775 	val conjectures = make_conjecture_clauses thms
   776         val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses user_lemmas)
   777 	val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   778 	and probname = Path.pack (Path.base (Path.unpack filename))
   779 	val (axstrs,_) =  ListPair.unzip (map clause2dfg axclauses')
   780 	val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss)
   781 	val out = TextIO.openOut filename
   782 	val helper_clauses = (#2 o ListPair.unzip o get_helper_clauses) ()
   783 	val helper_clauses_strs = (#1 o ListPair.unzip o (map clause2dfg)) helper_clauses
   784 	val funcs = funcs_of_clauses (helper_clauses @ conjectures @ axclauses') arity_clauses
   785 	and preds = preds_of classrel_clauses arity_clauses
   786     in
   787 	TextIO.output (out, ResClause.string_of_start probname); 
   788 	TextIO.output (out, ResClause.string_of_descrip probname); 
   789 	TextIO.output (out, ResClause.string_of_symbols (ResClause.string_of_funcs funcs) (ResClause.string_of_preds preds)); 
   790 	TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
   791 	ResClause.writeln_strs out axstrs;
   792 	List.app (curry TextIO.output out o ResClause.dfg_classrelClause) classrel_clauses;
   793 	List.app (curry TextIO.output out o ResClause.dfg_arity_clause) arity_clauses;
   794 	ResClause.writeln_strs out helper_clauses_strs;
   795 	TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   796 	ResClause.writeln_strs out tfree_clss;
   797 	ResClause.writeln_strs out dfg_clss;
   798 	TextIO.output (out, "end_of_list.\n\nend_problem.\n");
   799 	TextIO.closeOut out;
   800 	clnames
   801     end;
   802 
   803 end