src/HOL/Tools/res_hol_clause.ML
author mengj
Fri Oct 28 02:23:49 2005 +0200 (2005-10-28)
changeset 17998 0a869029ca58
child 18200 9d476d1054d7
permissions -rw-r--r--
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj@17998
     1
(* ID: $Id$ 
mengj@17998
     2
   Author: Jia Meng, NICTA
mengj@17998
     3
mengj@17998
     4
FOL clauses translated from HOL formulae.  Combinators are used to represent lambda terms.
mengj@17998
     5
mengj@17998
     6
*)
mengj@17998
     7
mengj@17998
     8
structure ResHolClause =
mengj@17998
     9
mengj@17998
    10
struct
mengj@17998
    11
mengj@17998
    12
mengj@17998
    13
mengj@17998
    14
mengj@17998
    15
(**********************************************************************)
mengj@17998
    16
(* convert a Term.term with lambdas into a Term.term with combinators *) 
mengj@17998
    17
(**********************************************************************)
mengj@17998
    18
mengj@17998
    19
fun is_free (Bound(a)) n = (a = n)
mengj@17998
    20
  | is_free (Abs(x,_,b)) n = (is_free b (n+1))
mengj@17998
    21
  | is_free (P $ Q) n = ((is_free P n) orelse (is_free Q n))
mengj@17998
    22
  | is_free _ _ = false;
mengj@17998
    23
mengj@17998
    24
mengj@17998
    25
exception LAM2COMB of term;
mengj@17998
    26
mengj@17998
    27
exception BND of term;
mengj@17998
    28
mengj@17998
    29
fun decre_bndVar (Bound n) = Bound (n-1)
mengj@17998
    30
  | decre_bndVar (P $ Q) = (decre_bndVar P) $ (decre_bndVar Q)
mengj@17998
    31
  | decre_bndVar t =
mengj@17998
    32
    case t of Const(_,_) => t
mengj@17998
    33
	    | Free(_,_) => t
mengj@17998
    34
	    | Var(_,_) => t
mengj@17998
    35
	    | Abs(_,_,_) => raise BND(t); (*should not occur*)
mengj@17998
    36
mengj@17998
    37
mengj@17998
    38
(*******************************************)
mengj@17998
    39
fun lam2comb (Abs(x,tp,Bound 0)) _ = 
mengj@17998
    40
    let val tpI = Type("fun",[tp,tp])
mengj@17998
    41
    in 
mengj@17998
    42
	Const("COMBI",tpI) 
mengj@17998
    43
    end
mengj@17998
    44
  | lam2comb (Abs(x,t1,Const(c,t2))) _ = 
mengj@17998
    45
    let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
mengj@17998
    46
    in 
mengj@17998
    47
	Const("COMBK",tK) $ Const(c,t2) 
mengj@17998
    48
    end
mengj@17998
    49
  | lam2comb (Abs(x,t1,Free(v,t2))) _ =
mengj@17998
    50
    let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
mengj@17998
    51
    in
mengj@17998
    52
	Const("COMBK",tK) $ Free(v,t2)
mengj@17998
    53
    end
mengj@17998
    54
  | lam2comb (Abs(x,t1,Var(ind,t2))) _=
mengj@17998
    55
    let val tK = Type("fun",[t2,Type("fun",[t1,t2])])
mengj@17998
    56
    in
mengj@17998
    57
	Const("COMBK",tK) $ Var(ind,t2)
mengj@17998
    58
    end
mengj@17998
    59
  | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) Bnds =
mengj@17998
    60
    let val nfreeP = not(is_free P 0)
mengj@17998
    61
	val tr = Term.type_of1(t1::Bnds,P)
mengj@17998
    62
    in
mengj@17998
    63
	if nfreeP then (decre_bndVar P)
mengj@17998
    64
	else (
mengj@17998
    65
	      let val tI = Type("fun",[t1,t1])
mengj@17998
    66
		  val P' = lam2comb (Abs(x,t1,P)) Bnds
mengj@17998
    67
		  val tp' = Term.type_of1(Bnds,P')
mengj@17998
    68
		  val tS = Type("fun",[tp',Type("fun",[tI,tr])])
mengj@17998
    69
	      in
mengj@17998
    70
		  Const("COMBS",tS) $ P' $ Const("COMBI",tI)
mengj@17998
    71
	      end)
mengj@17998
    72
    end
mengj@17998
    73
	    
mengj@17998
    74
  | lam2comb (t as (Abs(x,t1,P$Q))) Bnds =
mengj@17998
    75
    let val (nfreeP,nfreeQ) = (not(is_free P 0),not(is_free Q 0))
mengj@17998
    76
	val tpq = Term.type_of1(t1::Bnds, P$Q) 
mengj@17998
    77
    in
mengj@17998
    78
	if(nfreeP andalso nfreeQ) then (
mengj@17998
    79
	    let val tK = Type("fun",[tpq,Type("fun",[t1,tpq])])
mengj@17998
    80
		val PQ' = decre_bndVar(P $ Q)
mengj@17998
    81
	    in 
mengj@17998
    82
		Const("COMBK",tK) $ PQ'
mengj@17998
    83
	    end)
mengj@17998
    84
	else (
mengj@17998
    85
	      if nfreeP then (
mengj@17998
    86
			       let val Q' = lam2comb (Abs(x,t1,Q)) Bnds
mengj@17998
    87
				   val P' = decre_bndVar P
mengj@17998
    88
				   val tp = Term.type_of1(Bnds,P')
mengj@17998
    89
				   val tq' = Term.type_of1(Bnds, Q')
mengj@17998
    90
				   val tB = Type("fun",[tp,Type("fun",[tq',Type("fun",[t1,tpq])])])
mengj@17998
    91
			       in
mengj@17998
    92
				   Const("COMBB",tB) $ P' $ Q' 
mengj@17998
    93
			       end)
mengj@17998
    94
	      else (
mengj@17998
    95
		    if nfreeQ then (
mengj@17998
    96
				    let val P' = lam2comb (Abs(x,t1,P)) Bnds
mengj@17998
    97
					val Q' = decre_bndVar Q
mengj@17998
    98
					val tq = Term.type_of1(Bnds,Q')
mengj@17998
    99
					val tp' = Term.type_of1(Bnds, P')
mengj@17998
   100
					val tC = Type("fun",[tp',Type("fun",[tq,Type("fun",[t1,tpq])])])
mengj@17998
   101
				    in
mengj@17998
   102
					Const("COMBC",tC) $ P' $ Q'
mengj@17998
   103
				    end)
mengj@17998
   104
		    else(
mengj@17998
   105
			 let val P' = lam2comb (Abs(x,t1,P)) Bnds
mengj@17998
   106
			     val Q' = lam2comb (Abs(x,t1,Q)) Bnds
mengj@17998
   107
			     val tp' = Term.type_of1(Bnds,P')
mengj@17998
   108
			     val tq' = Term.type_of1(Bnds,Q')
mengj@17998
   109
			     val tS = Type("fun",[tp',Type("fun",[tq',Type("fun",[t1,tpq])])])
mengj@17998
   110
			 in
mengj@17998
   111
			     Const("COMBS",tS) $ P' $ Q'
mengj@17998
   112
			 end)))
mengj@17998
   113
    end
mengj@17998
   114
  | lam2comb (t as (Abs(x,t1,_))) _ = raise LAM2COMB (t);
mengj@17998
   115
mengj@17998
   116
	     
mengj@17998
   117
mengj@17998
   118
(*********************)
mengj@17998
   119
mengj@17998
   120
fun to_comb (Abs(x,tp,b)) Bnds =
mengj@17998
   121
    let val b' = to_comb b (tp::Bnds)
mengj@17998
   122
    in lam2comb (Abs(x,tp,b')) Bnds end
mengj@17998
   123
  | to_comb (P $ Q) Bnds = ((to_comb P Bnds) $ (to_comb Q Bnds))
mengj@17998
   124
  | to_comb t _ = t;
mengj@17998
   125
 
mengj@17998
   126
    
mengj@17998
   127
fun comb_of t = to_comb t [];
mengj@17998
   128
mengj@17998
   129
mengj@17998
   130
(* print a term containing combinators, used for debugging *)
mengj@17998
   131
exception TERM_COMB of term;
mengj@17998
   132
mengj@17998
   133
fun string_of_term (Const(c,t)) = c
mengj@17998
   134
  | string_of_term (Free(v,t)) = v
mengj@17998
   135
  | string_of_term (Var((x,n),t)) =
mengj@17998
   136
    let val xn = x ^ "_" ^ (string_of_int n)
mengj@17998
   137
    in xn end
mengj@17998
   138
  | string_of_term (P $ Q) =
mengj@17998
   139
    let val P' = string_of_term P
mengj@17998
   140
	val Q' = string_of_term Q
mengj@17998
   141
    in
mengj@17998
   142
	"(" ^ P' ^ " " ^ Q' ^ ")" end
mengj@17998
   143
  | string_of_term t =  raise TERM_COMB (t);
mengj@17998
   144
mengj@17998
   145
mengj@17998
   146
mengj@17998
   147
(******************************************************)
mengj@17998
   148
(* data types for typed combinator expressions        *)
mengj@17998
   149
(******************************************************)
mengj@17998
   150
mengj@17998
   151
type axiom_name = string;
mengj@17998
   152
datatype kind = Axiom | Conjecture;
mengj@17998
   153
fun name_of_kind Axiom = "axiom"
mengj@17998
   154
  | name_of_kind Conjecture = "conjecture";
mengj@17998
   155
mengj@17998
   156
type polarity = bool;
mengj@17998
   157
type indexname = Term.indexname;
mengj@17998
   158
type clause_id = int;
mengj@17998
   159
type csort = Term.sort;
mengj@17998
   160
type ctyp = string;
mengj@17998
   161
mengj@17998
   162
type ctyp_var = ResClause.typ_var;
mengj@17998
   163
mengj@17998
   164
type ctype_literal = ResClause.type_literal;
mengj@17998
   165
mengj@17998
   166
mengj@17998
   167
datatype combterm = CombConst of string * ctyp
mengj@17998
   168
		  | CombFree of string * ctyp
mengj@17998
   169
		  | CombVar of string * ctyp
mengj@17998
   170
		  | CombApp of combterm * combterm * ctyp
mengj@17998
   171
		  | Bool of combterm
mengj@17998
   172
		  | Equal of combterm * combterm;
mengj@17998
   173
datatype literal = Literal of polarity * combterm;
mengj@17998
   174
mengj@17998
   175
mengj@17998
   176
mengj@17998
   177
datatype clause = 
mengj@17998
   178
	 Clause of {clause_id: clause_id,
mengj@17998
   179
		    axiom_name: axiom_name,
mengj@17998
   180
		    kind: kind,
mengj@17998
   181
		    literals: literal list,
mengj@17998
   182
		    ctypes_sorts: (ctyp_var * csort) list, 
mengj@17998
   183
                    ctvar_type_literals: ctype_literal list, 
mengj@17998
   184
                    ctfree_type_literals: ctype_literal list};
mengj@17998
   185
mengj@17998
   186
mengj@17998
   187
mengj@17998
   188
fun string_of_kind (Clause cls) = name_of_kind (#kind cls);
mengj@17998
   189
fun get_axiomName (Clause cls) = #axiom_name cls;
mengj@17998
   190
fun get_clause_id (Clause cls) = #clause_id cls;
mengj@17998
   191
mengj@17998
   192
mengj@17998
   193
mengj@17998
   194
mengj@17998
   195
(*********************************************************************)
mengj@17998
   196
(* convert a clause with type Term.term to a clause with type clause *)
mengj@17998
   197
(*********************************************************************)
mengj@17998
   198
mengj@17998
   199
mengj@17998
   200
fun isFalse (Literal(pol,Bool(CombConst(c,_)))) =
mengj@17998
   201
    (pol andalso c = "c_False") orelse
mengj@17998
   202
    (not pol andalso c = "c_True")
mengj@17998
   203
  | isFalse _ = false;
mengj@17998
   204
mengj@17998
   205
mengj@17998
   206
fun isTrue (Literal (pol,Bool(CombConst(c,_)))) =
mengj@17998
   207
      (pol andalso c = "c_True") orelse
mengj@17998
   208
      (not pol andalso c = "c_False")
mengj@17998
   209
  | isTrue _ = false;
mengj@17998
   210
  
mengj@17998
   211
fun isTaut (Clause {literals,...}) = exists isTrue literals;  
mengj@17998
   212
mengj@17998
   213
mengj@17998
   214
mengj@17998
   215
fun make_clause(clause_id,axiom_name,kind,literals,ctypes_sorts,ctvar_type_literals,ctfree_type_literals) =
mengj@17998
   216
    if forall isFalse literals
mengj@17998
   217
    then error "Problem too trivial for resolution (empty clause)"
mengj@17998
   218
    else
mengj@17998
   219
	Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind,
mengj@17998
   220
		literals = literals, ctypes_sorts = ctypes_sorts, 
mengj@17998
   221
		ctvar_type_literals = ctvar_type_literals,
mengj@17998
   222
		ctfree_type_literals = ctfree_type_literals};
mengj@17998
   223
mengj@17998
   224
mengj@17998
   225
(* convert a Term.type to a string; gather sort information of type variables; also check if the type is a bool type *)
mengj@17998
   226
mengj@17998
   227
fun type_of (Type (a, [])) = ((ResClause.make_fixed_type_const a,[]),a ="bool")
mengj@17998
   228
  | type_of (Type (a, Ts)) = 
mengj@17998
   229
    let val typbs = map type_of Ts
mengj@17998
   230
	val (types,_) = ListPair.unzip typbs
mengj@17998
   231
	val (ctyps,tvarSorts) = ListPair.unzip types
mengj@17998
   232
	val ts = ResClause.union_all tvarSorts
mengj@17998
   233
	val t = ResClause.make_fixed_type_const a
mengj@17998
   234
    in
mengj@17998
   235
	(((t ^ ResClause.paren_pack ctyps),ts),false)
mengj@17998
   236
    end
mengj@17998
   237
  | type_of (tp as (TFree (a,s))) = ((ResClause.make_fixed_type_var a,[ResClause.mk_typ_var_sort tp]),false)
mengj@17998
   238
  | type_of (tp as (TVar (v,s))) = ((ResClause.make_schematic_type_var v,[ResClause.mk_typ_var_sort tp]),false);
mengj@17998
   239
mengj@17998
   240
mengj@17998
   241
(* same as above, but no gathering of sort information *)
mengj@17998
   242
fun simp_type_of (Type (a, [])) = (ResClause.make_fixed_type_const a,a ="bool")
mengj@17998
   243
  | simp_type_of (Type (a, Ts)) = 
mengj@17998
   244
    let val typbs = map simp_type_of Ts
mengj@17998
   245
	val (types,_) = ListPair.unzip typbs
mengj@17998
   246
	val t = ResClause.make_fixed_type_const a
mengj@17998
   247
    in
mengj@17998
   248
	((t ^ ResClause.paren_pack types),false)
mengj@17998
   249
    end
mengj@17998
   250
  | simp_type_of (TFree (a,s)) = (ResClause.make_fixed_type_var a,false)
mengj@17998
   251
  | simp_type_of (TVar (v,s)) = (ResClause.make_schematic_type_var v,false);
mengj@17998
   252
mengj@17998
   253
mengj@17998
   254
mengj@17998
   255
mengj@17998
   256
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
mengj@17998
   257
fun combterm_of (Const(c,t)) =
mengj@17998
   258
    let val ((tp,ts),is_bool) = type_of t
mengj@17998
   259
	val c' = CombConst(ResClause.make_fixed_const c,tp)
mengj@17998
   260
	val c'' = if is_bool then Bool(c') else c'
mengj@17998
   261
    in
mengj@17998
   262
	(c'',ts)
mengj@17998
   263
    end
mengj@17998
   264
  | combterm_of (Free(v,t)) =
mengj@17998
   265
    let val ((tp,ts),is_bool) = type_of t
mengj@17998
   266
	val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp)
mengj@17998
   267
		 else CombFree(ResClause.make_fixed_var v,tp)
mengj@17998
   268
	val v'' = if is_bool then Bool(v') else v'
mengj@17998
   269
    in
mengj@17998
   270
	(v'',ts)
mengj@17998
   271
    end
mengj@17998
   272
  | combterm_of (Var(v,t)) =
mengj@17998
   273
    let val ((tp,ts),is_bool) = type_of t
mengj@17998
   274
	val v' = CombVar(ResClause.make_schematic_var v,tp)
mengj@17998
   275
	val v'' = if is_bool then Bool(v') else v'
mengj@17998
   276
    in
mengj@17998
   277
	(v'',ts)
mengj@17998
   278
    end
mengj@17998
   279
  | combterm_of (Const("op =",T) $ P $ Q) = (*FIXME: allow equal between bools?*)
mengj@17998
   280
    let val (P',tsP) = combterm_of P        
mengj@17998
   281
	val (Q',tsQ) = combterm_of Q
mengj@17998
   282
    in
mengj@17998
   283
	(Equal(P',Q'),tsP union tsQ)
mengj@17998
   284
    end
mengj@17998
   285
  | combterm_of (t as (P $ Q)) =
mengj@17998
   286
    let val (P',tsP) = combterm_of P
mengj@17998
   287
	val (Q',tsQ) = combterm_of Q
mengj@17998
   288
	val tp = Term.type_of t
mengj@17998
   289
	val (tp',is_bool) = simp_type_of tp
mengj@17998
   290
	val t' = CombApp(P',Q',tp')
mengj@17998
   291
	val t'' = if is_bool then Bool(t') else t'
mengj@17998
   292
    in
mengj@17998
   293
	(t'',tsP union tsQ)
mengj@17998
   294
    end;
mengj@17998
   295
mengj@17998
   296
fun predicate_of ((Const("Not",_) $ P), polarity) =
mengj@17998
   297
    predicate_of (P, not polarity)
mengj@17998
   298
  | predicate_of (term,polarity) = (combterm_of term,polarity);
mengj@17998
   299
mengj@17998
   300
mengj@17998
   301
fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
mengj@17998
   302
  | literals_of_term1 args (Const("op |",_) $ P $ Q) = 
mengj@17998
   303
    let val args' = literals_of_term1 args P
mengj@17998
   304
    in
mengj@17998
   305
	literals_of_term1 args' Q
mengj@17998
   306
    end
mengj@17998
   307
  | literals_of_term1 (lits,ts) P =
mengj@17998
   308
    let val ((pred,ts'),pol) = predicate_of (P,true)
mengj@17998
   309
	val lits' = Literal(pol,pred)::lits
mengj@17998
   310
    in
mengj@17998
   311
	(lits',ts union ts')
mengj@17998
   312
    end;
mengj@17998
   313
mengj@17998
   314
mengj@17998
   315
fun literals_of_term P = literals_of_term1 ([],[]) P;
mengj@17998
   316
mengj@17998
   317
mengj@17998
   318
(* making axiom and conjecture clauses *)
mengj@17998
   319
fun make_axiom_clause term (ax_name,cls_id) =
mengj@17998
   320
    let val term' = comb_of term
mengj@17998
   321
	val (lits,ctypes_sorts) = literals_of_term term'
mengj@17998
   322
	val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux2 ctypes_sorts
mengj@17998
   323
    in
mengj@17998
   324
	make_clause(cls_id,ax_name,Axiom,
mengj@17998
   325
		    lits,ctypes_sorts,ctvar_lits,ctfree_lits)
mengj@17998
   326
    end;
mengj@17998
   327
mengj@17998
   328
mengj@17998
   329
fun make_conjecture_clause n t =
mengj@17998
   330
    let val t' = comb_of t
mengj@17998
   331
	val (lits,ctypes_sorts) = literals_of_term t'
mengj@17998
   332
	val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux2 ctypes_sorts
mengj@17998
   333
    in
mengj@17998
   334
	make_clause(n,"conjecture",Conjecture,lits,ctypes_sorts,ctvar_lits,ctfree_lits)
mengj@17998
   335
    end;
mengj@17998
   336
mengj@17998
   337
mengj@17998
   338
mengj@17998
   339
fun make_conjecture_clauses_aux _ [] = []
mengj@17998
   340
  | make_conjecture_clauses_aux n (t::ts) =
mengj@17998
   341
    make_conjecture_clause n t :: make_conjecture_clauses_aux (n+1) ts;
mengj@17998
   342
mengj@17998
   343
val make_conjecture_clauses = make_conjecture_clauses_aux 0;
mengj@17998
   344
mengj@17998
   345
mengj@17998
   346
(**********************************************************************)
mengj@17998
   347
(* convert clause into ATP specific formats:                          *)
mengj@17998
   348
(* TPTP used by Vampire and E                                         *)
mengj@17998
   349
(**********************************************************************)
mengj@17998
   350
mengj@17998
   351
val keep_types = ref true;
mengj@17998
   352
mengj@17998
   353
val type_wrapper = "typeinfo";
mengj@17998
   354
mengj@17998
   355
fun put_type (c,t) = 
mengj@17998
   356
    if !keep_types then type_wrapper ^ (ResClause.paren_pack [c,t])
mengj@17998
   357
    else c;
mengj@17998
   358
mengj@17998
   359
mengj@17998
   360
val bool_tp = ResClause.make_fixed_type_const "bool";
mengj@17998
   361
mengj@17998
   362
val app_str = "hAPP";
mengj@17998
   363
mengj@17998
   364
val bool_str = "hBOOL";
mengj@17998
   365
mengj@17998
   366
mengj@17998
   367
(* convert literals of clauses into strings *)
mengj@17998
   368
fun string_of_combterm (CombConst(c,tp)) = 
mengj@17998
   369
    if tp = bool_tp then c else put_type(c,tp)
mengj@17998
   370
  | string_of_combterm (CombFree(v,tp)) = 
mengj@17998
   371
    if tp = bool_tp then v else put_type(v,tp)
mengj@17998
   372
  | string_of_combterm (CombVar(v,tp)) = 
mengj@17998
   373
    if tp = bool_tp then v else put_type(v,tp)
mengj@17998
   374
  | string_of_combterm (CombApp(t1,t2,tp)) = 
mengj@17998
   375
    let val s1 = string_of_combterm t1
mengj@17998
   376
	val s2 = string_of_combterm t2
mengj@17998
   377
	val app = app_str ^ (ResClause.paren_pack [s1,s2])
mengj@17998
   378
    in
mengj@17998
   379
	if tp = bool_tp then app else put_type(app,tp)
mengj@17998
   380
    end
mengj@17998
   381
  | string_of_combterm (Bool(t)) = 
mengj@17998
   382
    let val t' = string_of_combterm t
mengj@17998
   383
    in
mengj@17998
   384
	bool_str ^ (ResClause.paren_pack [t'])
mengj@17998
   385
    end
mengj@17998
   386
  | string_of_combterm (Equal(t1,t2)) =
mengj@17998
   387
    let val s1 = string_of_combterm t1
mengj@17998
   388
	val s2 = string_of_combterm t2
mengj@17998
   389
    in
mengj@17998
   390
	"equal" ^ (ResClause.paren_pack [s1,s2]) 
mengj@17998
   391
    end;
mengj@17998
   392
mengj@17998
   393
fun string_of_clausename (cls_id,ax_name) = 
mengj@17998
   394
    ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
mengj@17998
   395
mengj@17998
   396
fun string_of_type_clsname (cls_id,ax_name,idx) = 
mengj@17998
   397
    string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
mengj@17998
   398
mengj@17998
   399
mengj@17998
   400
fun tptp_literal (Literal(pol,pred)) =
mengj@17998
   401
    let val pred_string = string_of_combterm pred
mengj@17998
   402
	val pol_str = if pol then "++" else "--"
mengj@17998
   403
    in
mengj@17998
   404
	pol_str ^ pred_string
mengj@17998
   405
    end;
mengj@17998
   406
mengj@17998
   407
 
mengj@17998
   408
fun tptp_type_lits (Clause cls) = 
mengj@17998
   409
    let val lits = map tptp_literal (#literals cls)
mengj@17998
   410
	val ctvar_lits_strs =
mengj@17998
   411
	      if !keep_types 
mengj@17998
   412
	      then (map ResClause.tptp_of_typeLit (#ctvar_type_literals cls)) 
mengj@17998
   413
	      else []
mengj@17998
   414
	val ctfree_lits = 
mengj@17998
   415
	      if !keep_types
mengj@17998
   416
	      then (map ResClause.tptp_of_typeLit (#ctfree_type_literals cls)) 
mengj@17998
   417
	      else []
mengj@17998
   418
    in
mengj@17998
   419
	(ctvar_lits_strs @ lits, ctfree_lits)
mengj@17998
   420
    end; 
mengj@17998
   421
mengj@17998
   422
mengj@17998
   423
fun clause2tptp cls =
mengj@17998
   424
    let val (lits,ctfree_lits) = tptp_type_lits cls
mengj@17998
   425
	val cls_id = get_clause_id cls
mengj@17998
   426
	val ax_name = get_axiomName cls
mengj@17998
   427
	val knd = string_of_kind cls
mengj@17998
   428
	val lits_str = ResClause.bracket_pack lits
mengj@17998
   429
	val cls_str = ResClause.gen_tptp_cls(cls_id,ax_name,knd,lits_str)
mengj@17998
   430
    in
mengj@17998
   431
	(cls_str,ctfree_lits)
mengj@17998
   432
    end;
mengj@17998
   433
mengj@17998
   434
mengj@17998
   435
end