src/HOL/Tools/res_clause.ML
author quigley
Fri Aug 26 19:36:07 2005 +0200 (2005-08-26)
changeset 17150 ce2a1aeb42aa
parent 16976 377962871f5d
child 17230 77e93bf303a5
permissions -rw-r--r--
DFG output now works for untyped rules (ML "ResClause.untyped();")
paulson@15347
     1
(*  Author: Jia Meng, Cambridge University Computer Laboratory
quigley@17150
     2
paulson@15347
     3
    ID: $Id$
paulson@15347
     4
    Copyright 2004 University of Cambridge
paulson@15347
     5
paulson@15347
     6
ML data structure for storing/printing FOL clauses and arity clauses.
paulson@15347
     7
Typed equality is treated differently.
paulson@15347
     8
*)
paulson@15347
     9
quigley@17150
    10
(* works for writeoutclasimp on typed *)
paulson@15347
    11
signature RES_CLAUSE =
paulson@15347
    12
  sig
paulson@15347
    13
    exception ARCLAUSE of string
paulson@15347
    14
    exception CLAUSE of string
paulson@15347
    15
    type arityClause 
paulson@15347
    16
    type classrelClause
paulson@16925
    17
    val classrelClauses_of : string * string list -> classrelClause list
paulson@15347
    18
    type clause
paulson@16925
    19
    val init : theory -> unit
paulson@15347
    20
    val keep_types : bool ref
paulson@15347
    21
    val make_axiom_arity_clause :
paulson@15347
    22
       string * (string * string list list) -> arityClause
paulson@15347
    23
    val make_axiom_classrelClause :
skalberg@15531
    24
       string * string option -> classrelClause
quigley@17150
    25
paulson@15347
    26
    val make_axiom_clause : Term.term -> string * int -> clause
quigley@17150
    27
paulson@15347
    28
    val make_conjecture_clause : Term.term -> clause
paulson@15347
    29
    val make_conjecture_clause_thm : Thm.thm -> clause
paulson@15347
    30
    val make_hypothesis_clause : Term.term -> clause
paulson@15347
    31
    val special_equal : bool ref
quigley@17150
    32
    val clause_info : clause ->  string * string
quigley@17150
    33
    val typed : unit -> unit
quigley@17150
    34
    val untyped : unit -> unit
quigley@17150
    35
quigley@17150
    36
    val dfg_clauses2str : string list -> string
quigley@17150
    37
    val clause2dfg : clause -> string * string list
quigley@17150
    38
    val clauses2dfg : clause list -> string -> clause list -> clause list ->
quigley@17150
    39
                      (string * int) list -> (string * int) list -> string list -> string
quigley@17150
    40
    val tfree_dfg_clause : string -> string
quigley@17150
    41
paulson@15347
    42
    val tptp_arity_clause : arityClause -> string
paulson@15347
    43
    val tptp_classrelClause : classrelClause -> string
paulson@15347
    44
    val tptp_clause : clause -> string list
paulson@15347
    45
    val tptp_clauses2str : string list -> string
paulson@15608
    46
    val clause2tptp : clause -> string * string list
paulson@15608
    47
    val tfree_clause : string -> string
paulson@16953
    48
    val schematic_var_prefix : string
paulson@16953
    49
    val fixed_var_prefix : string
paulson@16953
    50
    val tvar_prefix : string
paulson@16953
    51
    val tfree_prefix : string
paulson@16953
    52
    val clause_prefix : string 
paulson@16953
    53
    val arclause_prefix : string
paulson@16953
    54
    val const_prefix : string
paulson@16953
    55
    val tconst_prefix : string 
paulson@16953
    56
    val class_prefix : string 
paulson@15347
    57
  end;
paulson@15347
    58
quigley@17150
    59
structure ResClause: RES_CLAUSE =
paulson@15347
    60
struct
paulson@15347
    61
paulson@15347
    62
(* Added for typed equality *)
paulson@15347
    63
val special_equal = ref false; (* by default,equality does not carry type information *)
paulson@15347
    64
val eq_typ_wrapper = "typeinfo"; (* default string *)
paulson@15347
    65
paulson@15347
    66
paulson@15347
    67
val schematic_var_prefix = "V_";
paulson@15347
    68
val fixed_var_prefix = "v_";
paulson@15347
    69
quigley@17150
    70
quigley@17150
    71
val tvar_prefix = "Typ_";
quigley@17150
    72
val tfree_prefix = "typ_";
quigley@17150
    73
paulson@15347
    74
paulson@15347
    75
val clause_prefix = "cls_"; 
paulson@15347
    76
paulson@15347
    77
val arclause_prefix = "arcls_" 
paulson@15347
    78
quigley@17150
    79
val const_prefix = "const_";
quigley@17150
    80
val tconst_prefix = "tconst_"; 
paulson@15347
    81
paulson@16199
    82
val class_prefix = "class_"; 
paulson@15347
    83
paulson@15347
    84
quigley@17150
    85
paulson@15347
    86
(**** some useful functions ****)
paulson@15347
    87
 
paulson@15347
    88
val const_trans_table =
paulson@15347
    89
      Symtab.make [("op =", "equal"),
paulson@15347
    90
	  	   ("op <=", "lessequals"),
paulson@15347
    91
		   ("op <", "less"),
paulson@15347
    92
		   ("op &", "and"),
paulson@15347
    93
		   ("op |", "or"),
paulson@15347
    94
		   ("op -->", "implies"),
paulson@15347
    95
		   ("op :", "in"),
paulson@15347
    96
		   ("op Un", "union"),
paulson@15347
    97
		   ("op Int", "inter")];
paulson@15347
    98
quigley@17150
    99
paulson@15347
   100
paulson@15610
   101
(*Escaping of special characters.
paulson@15610
   102
  Alphanumeric characters are left unchanged.
paulson@15610
   103
  The character _ goes to __
paulson@15610
   104
  Characters in the range ASCII space to / go to _A to _P, respectively.
paulson@15610
   105
  Other printing characters go to _NNN where NNN is the decimal ASCII code.*)
paulson@15610
   106
local
paulson@15610
   107
paulson@15610
   108
val A_minus_space = Char.ord #"A" - Char.ord #" ";
paulson@15610
   109
paulson@15347
   110
fun ascii_of_c c =
paulson@15610
   111
  if Char.isAlphaNum c then String.str c
paulson@15610
   112
  else if c = #"_" then "__"
quigley@17150
   113
  else if c = #"'" then ""
paulson@15610
   114
  else if #" " <= c andalso c <= #"/" 
paulson@15610
   115
       then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
paulson@15610
   116
  else if Char.isPrint c then ("_" ^ Int.toString (Char.ord c))
paulson@15610
   117
  else ""
paulson@15347
   118
paulson@15610
   119
in
paulson@15610
   120
paulson@15610
   121
val ascii_of = String.translate ascii_of_c;
paulson@15610
   122
paulson@15610
   123
end;
paulson@15347
   124
quigley@17150
   125
paulson@16925
   126
(*Remove the initial ' character from a type variable, if it is present*)
paulson@16925
   127
fun trim_type_var s =
paulson@16925
   128
  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
paulson@16925
   129
  else error ("trim_type: Malformed type variable encountered: " ^ s);
paulson@16925
   130
paulson@16903
   131
fun ascii_of_indexname (v,0) = ascii_of v
paulson@16903
   132
  | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i;
paulson@15347
   133
quigley@17150
   134
(* another version of above functions that remove chars that may not be allowed by Vampire *)
quigley@17150
   135
fun make_schematic_var v = schematic_var_prefix ^ (ascii_of v);
paulson@15347
   136
fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
paulson@15347
   137
quigley@17150
   138
paulson@16903
   139
(*Type variables contain _H because the character ' translates to that.*)
paulson@16925
   140
fun make_schematic_type_var (x,i) = 
paulson@16925
   141
      tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
paulson@16925
   142
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
paulson@15347
   143
quigley@17150
   144
fun make_fixed_const c = const_prefix ^ (ascii_of c);
quigley@17150
   145
fun make_fixed_type_const c = tconst_prefix ^ (ascii_of c);
quigley@17150
   146
quigley@17150
   147
fun make_type_class clas = class_prefix ^ (ascii_of clas);
quigley@17150
   148
quigley@17150
   149
quigley@17150
   150
quigley@17150
   151
fun lookup_const c =
paulson@16903
   152
    case Symtab.lookup (const_trans_table,c) of
paulson@16903
   153
        SOME c' => c'
quigley@17150
   154
      | NONE =>  make_fixed_const c;
paulson@15347
   155
paulson@15347
   156
paulson@15347
   157
paulson@15347
   158
(***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****)
paulson@15347
   159
paulson@15347
   160
val keep_types = ref true; (* default is true *)
paulson@15347
   161
fun untyped () = (keep_types := false);
paulson@15347
   162
fun typed () = (keep_types := true);
paulson@15347
   163
paulson@15347
   164
paulson@15347
   165
datatype kind = Axiom | Hypothesis | Conjecture;
paulson@15347
   166
fun name_of_kind Axiom = "axiom"
paulson@15347
   167
  | name_of_kind Hypothesis = "hypothesis"
paulson@15347
   168
  | name_of_kind Conjecture = "conjecture";
paulson@15347
   169
paulson@15347
   170
type clause_id = int;
paulson@15347
   171
type axiom_name = string;
paulson@15347
   172
paulson@15347
   173
paulson@15347
   174
type polarity = bool;
paulson@15347
   175
paulson@15347
   176
type indexname = Term.indexname;
paulson@15347
   177
paulson@15347
   178
paulson@15347
   179
(* "tag" is used for vampire specific syntax  *)
paulson@15347
   180
type tag = bool; 
paulson@15347
   181
paulson@15347
   182
quigley@17150
   183
quigley@17150
   184
fun string_of_indexname (name,index) = name ^ "_" ^ (string_of_int index);
quigley@17150
   185
quigley@17150
   186
paulson@16903
   187
val id_ref = ref 0;
paulson@15347
   188
fun generate_id () = 
quigley@17150
   189
     let val id = !id_ref
quigley@17150
   190
     in
quigley@17150
   191
	 (id_ref:=id + 1; id)
quigley@17150
   192
     end;
paulson@15347
   193
paulson@15347
   194
paulson@15347
   195
paulson@15347
   196
(**** Isabelle FOL clauses ****)
paulson@15347
   197
paulson@15347
   198
(* by default it is false *)
paulson@15347
   199
val tagged = ref false;
paulson@15347
   200
paulson@15347
   201
type pred_name = string;
paulson@15347
   202
type sort = Term.sort;
paulson@15347
   203
type fol_type = string;
paulson@15347
   204
paulson@15347
   205
paulson@15347
   206
datatype type_literal = LTVar of string | LTFree of string;
paulson@15347
   207
paulson@15347
   208
paulson@15347
   209
datatype folTerm = UVar of string * fol_type| Fun of string * fol_type * folTerm list;
paulson@15347
   210
datatype predicate = Predicate of pred_name * fol_type * folTerm list;
paulson@15347
   211
paulson@15347
   212
paulson@15347
   213
datatype literal = Literal of polarity * predicate * tag;
paulson@15347
   214
paulson@15347
   215
paulson@15347
   216
datatype typ_var = FOLTVar of indexname | FOLTFree of string;
paulson@15347
   217
paulson@15347
   218
paulson@15347
   219
(* ML datatype used to repsent one single clause: disjunction of literals. *)
paulson@15347
   220
datatype clause = 
paulson@15347
   221
	 Clause of {clause_id: clause_id,
paulson@15347
   222
		    axiom_name: axiom_name,
paulson@15347
   223
		    kind: kind,
paulson@15347
   224
		    literals: literal list,
paulson@15347
   225
		    types_sorts: (typ_var * sort) list, 
paulson@15347
   226
                    tvar_type_literals: type_literal list, 
quigley@17150
   227
                    tfree_type_literals: type_literal list ,
quigley@17150
   228
                    tvars: string list,
quigley@17150
   229
                    predicates: (string*int) list,
quigley@17150
   230
                    functions: (string*int) list};
quigley@17150
   231
paulson@15347
   232
paulson@15347
   233
paulson@15347
   234
exception CLAUSE of string;
paulson@15347
   235
paulson@15347
   236
paulson@15347
   237
paulson@15347
   238
(*** make clauses ***)
paulson@15347
   239
paulson@15347
   240
quigley@17150
   241
fun make_clause (clause_id,axiom_name,kind,literals,types_sorts,tvar_type_literals,tfree_type_literals,tvars, predicates, functions) =
quigley@17150
   242
     Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, literals = literals, types_sorts = types_sorts,tvar_type_literals = tvar_type_literals,tfree_type_literals = tfree_type_literals,tvars = tvars, predicates = predicates, functions = functions};
quigley@17150
   243
quigley@17150
   244
paulson@15347
   245
quigley@17150
   246
fun type_of (Type (a, [])) = let val t = make_fixed_type_const a
quigley@17150
   247
                                    in
quigley@17150
   248
					(t,([],[(t,0)]))
quigley@17150
   249
  				    end
paulson@16925
   250
paulson@16925
   251
(*Definitions of the current theory--to allow suppressing types.*)
paulson@16925
   252
val curr_defs = ref Defs.empty;
paulson@16925
   253
paulson@16925
   254
(*Initialize the type suppression mechanism with the current theory before
paulson@16925
   255
    producing any clauses!*)
paulson@16925
   256
fun init thy = (curr_defs := Theory.defs_of thy);
quigley@17150
   257
(*<<<<<<< res_clause.ML
quigley@17150
   258
*)
quigley@17150
   259
quigley@17150
   260
(*Types aren't needed if the constant has at most one definition and is monomorphic*)
quigley@17150
   261
(*fun no_types_needed s =
quigley@17150
   262
  (case Defs.fast_overloading_info (!curr_defs) s of
quigley@17150
   263
      NONE => true
quigley@17150
   264
    | SOME (T,len,_) => len <= 1 andalso null (typ_tvars T))
quigley@17150
   265
=======*)
wenzelm@16976
   266
fun no_types_needed s = Defs.monomorphic (!curr_defs) s;
quigley@17150
   267
(*>>>>>>> 1.18*)
paulson@16925
   268
    
quigley@17150
   269
paulson@16925
   270
(*Flatten a type to a string while accumulating sort constraints on the TFress and
paulson@16925
   271
  TVars it contains.*)    
quigley@17150
   272
fun type_of (Type (a, [])) = let val t = make_fixed_type_const a
quigley@17150
   273
                                    in
quigley@17150
   274
					(t,([],[(t,0)]))
quigley@17150
   275
  				    end
paulson@15347
   276
  | type_of (Type (a, Ts)) = 
quigley@17150
   277
    let val foltyps_ts = map type_of Ts 
quigley@17150
   278
        val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts
quigley@17150
   279
        val (ts, funcslist) = ListPair.unzip ts_funcs
quigley@17150
   280
        val ts' = ResLib.flat_noDup ts
quigley@17150
   281
        val funcs' = (ResLib.flat_noDup funcslist)
quigley@17150
   282
        val t = (make_fixed_type_const a)
quigley@17150
   283
    in    
quigley@17150
   284
        ((t ^ (ResLib.list_to_string folTyps)),(ts', ((t,(length Ts))::funcs')) )
quigley@17150
   285
    end
quigley@17150
   286
  | type_of (TFree (a, s))  = let val t = make_fixed_type_const a
quigley@17150
   287
                              in
quigley@17150
   288
				(t, ([((FOLTFree a),s)],[(t,0)]) )
quigley@17150
   289
			      end
quigley@17150
   290
quigley@17150
   291
  | type_of (TVar (v, s))   = let val t =make_schematic_type_var ( v)
quigley@17150
   292
                              in
quigley@17150
   293
				(t, ([((FOLTVar v),s)], [(*(t,0)*)]))
quigley@17150
   294
                              end
quigley@17150
   295
quigley@17150
   296
(* added: checkMeta: string -> bool *)
quigley@17150
   297
(* Any meta vars like ?x should be treated as universal vars,although it is represented as "Free(...)" by Isabelle *)
quigley@17150
   298
fun checkMeta s =
quigley@17150
   299
    let val chars = explode s
quigley@17150
   300
    in
quigley@17150
   301
	["M", "E", "T", "A", "H", "Y", "P", "1"] prefix chars
quigley@17150
   302
    end;
paulson@15390
   303
paulson@16925
   304
fun maybe_type_of c T =
quigley@17150
   305
 if no_types_needed c then ("",([],[])) else type_of T;
paulson@16925
   306
paulson@16903
   307
(* Any variables created via the METAHYPS tactical should be treated as
paulson@16903
   308
   universal vars, although it is represented as "Free(...)" by Isabelle *)
paulson@16903
   309
val isMeta = String.isPrefix "METAHYP1_"
quigley@17150
   310
quigley@17150
   311
fun pred_name_type (Const(c,T)) = (let val t = make_fixed_const c
quigley@17150
   312
                                      val (typof,(folTyps,funcs)) = type_of T
quigley@17150
   313
                                     
quigley@17150
   314
                                  in
quigley@17150
   315
					(t, (typof,folTyps), (funcs))
quigley@17150
   316
      				  end) 
paulson@15390
   317
  | pred_name_type (Free(x,T))  = 
quigley@17150
   318
    let val is_meta = checkMeta x
quigley@17150
   319
    in
quigley@17150
   320
	if is_meta then (raise CLAUSE("Predicate Not First Order")) else
quigley@17150
   321
	(let val t = (make_fixed_var x)
quigley@17150
   322
                                      val (typof,(folTyps, funcs)) = type_of T
quigley@17150
   323
                                  in
quigley@17150
   324
					(t, (typof,folTyps),funcs)
quigley@17150
   325
      				  end)
quigley@17150
   326
quigley@17150
   327
    end
paulson@15347
   328
  | pred_name_type (Var(_,_))   = raise CLAUSE("Predicate Not First Order")
paulson@15347
   329
  | pred_name_type _          = raise CLAUSE("Predicate input unexpected");
paulson@15347
   330
paulson@15615
   331
paulson@15615
   332
(* For type equality *)
paulson@15615
   333
(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *)
paulson@15615
   334
(* Find type of equality arg *)
paulson@15615
   335
fun eq_arg_type (Type("fun",[T,_])) = 
paulson@15615
   336
    let val (folT,_) = type_of T;
paulson@15615
   337
    in
paulson@15615
   338
	folT
paulson@15615
   339
    end;
quigley@17150
   340
  
paulson@15615
   341
paulson@15347
   342
quigley@17150
   343
(* FIX: retest with lcp's changes *)
quigley@17150
   344
fun fun_name_type (Const(c,T)) args = (let val t = make_fixed_const c
quigley@17150
   345
                                      val (typof,(folTyps,funcs)) = maybe_type_of c T
quigley@17150
   346
                                      val arity = if (!keep_types) then
quigley@17150
   347
                                       (length args)(*+ 1*) (*(length folTyps) *)
quigley@17150
   348
					  else
quigley@17150
   349
					  (length args)(* -1*)
quigley@17150
   350
                                  in
quigley@17150
   351
					(t, (typof,folTyps), ((t,arity)::funcs))
quigley@17150
   352
      				  end)
quigley@17150
   353
                                     
quigley@17150
   354
  | fun_name_type (Free(x,T)) args  = (let val t = (make_fixed_var x)
quigley@17150
   355
                                      val (typof,(folTyps,funcs)) = type_of T
quigley@17150
   356
                                      val arity = if (!keep_types) then
quigley@17150
   357
                                       (length args) (*+ 1*) (*(length folTyps)*)
quigley@17150
   358
					  else
quigley@17150
   359
					  (length args) (*-1*)(*(length args) + 1*)(*(length folTyps)*)
quigley@17150
   360
                                  in
quigley@17150
   361
					(t, (typof,folTyps), ((t,0)::funcs))
quigley@17150
   362
      				  end)
quigley@17150
   363
quigley@17150
   364
  | fun_name_type _  args = raise CLAUSE("Function Not First Order");
quigley@17150
   365
paulson@15615
   366
paulson@15347
   367
fun term_of (Var(ind_nm,T)) = 
quigley@17150
   368
    let val (folType,(ts,funcs)) = type_of T
quigley@17150
   369
    in
quigley@17150
   370
	(UVar(make_schematic_var(string_of_indexname ind_nm),folType),(ts, (funcs)))
quigley@17150
   371
    end
paulson@15347
   372
  | term_of (Free(x,T)) = 
quigley@17150
   373
    let val is_meta = checkMeta x
quigley@17150
   374
	val (folType,(ts, funcs)) = type_of T
quigley@17150
   375
    in
quigley@17150
   376
	if is_meta then (UVar(make_schematic_var x,folType),(ts, (((make_schematic_var x),0)::funcs)))
quigley@17150
   377
	else
quigley@17150
   378
            (Fun(make_fixed_var x,folType,[]),(ts, (((make_fixed_var x),0)::funcs)))
quigley@17150
   379
    end
quigley@17150
   380
  |  term_of (Const(c,T)) =  (* impossible to be equality *)
quigley@17150
   381
    let val (folType,(ts,funcs)) = type_of T
quigley@17150
   382
     in
quigley@17150
   383
        (Fun(lookup_const c,folType,[]),(ts, (((lookup_const c),0)::funcs)))
quigley@17150
   384
    end    
quigley@17150
   385
  |  term_of (app as (t $ a)) = 
quigley@17150
   386
    let val (f,args) = strip_comb app
quigley@17150
   387
        fun term_of_aux () = 
quigley@17150
   388
            let val (funName,(funType,ts1),funcs) = fun_name_type f args
quigley@17150
   389
	        val (args',ts_funcs) = ListPair.unzip (map term_of args)
quigley@17150
   390
      	        val (ts2,funcs') = ListPair.unzip ( ts_funcs)
quigley@17150
   391
                val ts3 = ResLib.flat_noDup (ts1::ts2)
quigley@17150
   392
                val funcs'' = ResLib.flat_noDup((funcs::funcs'))
quigley@17150
   393
            in
quigley@17150
   394
		(Fun(funName,funType,args'),(ts3,funcs''))
quigley@17150
   395
            end
quigley@17150
   396
	fun term_of_eq ((Const ("op =", typ)),args) =
quigley@17150
   397
	    let val arg_typ = eq_arg_type typ
quigley@17150
   398
		val (args',ts_funcs) = ListPair.unzip (map term_of args)
quigley@17150
   399
      	        val (ts,funcs) = ListPair.unzip ( ts_funcs)
quigley@17150
   400
		val equal_name = lookup_const ("op =")
quigley@17150
   401
	    in
quigley@17150
   402
		(Fun(equal_name,arg_typ,args'),(ResLib.flat_noDup ts, (((make_fixed_var equal_name),2):: ResLib.flat_noDup (funcs))))
quigley@17150
   403
	    end
quigley@17150
   404
    in
quigley@17150
   405
        case f of Const ("op =", typ) => term_of_eq (f,args)
quigley@17150
   406
	        | Const(_,_) => term_of_aux ()
quigley@17150
   407
                | Free(s,_)  => if (checkMeta s) then (raise CLAUSE("Function Not First Order")) else term_of_aux ()
quigley@17150
   408
                | _          => raise CLAUSE("Function Not First Order")
quigley@17150
   409
    end
paulson@15390
   410
  | term_of _ = raise CLAUSE("Function Not First Order"); 
paulson@15390
   411
paulson@15347
   412
quigley@17150
   413
quigley@17150
   414
paulson@15347
   415
fun pred_of_eq ((Const ("op =", typ)),args) =
paulson@15347
   416
    let val arg_typ = eq_arg_type typ 
quigley@17150
   417
	val (args',ts_funcs) = ListPair.unzip (map term_of args)
quigley@17150
   418
        val (ts,funcs) = ListPair.unzip ( ts_funcs)
quigley@17150
   419
	val equal_name = lookup_const "op ="
paulson@15347
   420
    in
quigley@17150
   421
	(Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts,([((make_fixed_var equal_name),2)]:(string*int)list), (ResLib.flat_noDup (funcs)))
paulson@15347
   422
    end;
paulson@15347
   423
quigley@17150
   424
(* CHECK arity for predicate is set to (2*args) to account for type info.  Is this right? *)
paulson@15347
   425
(* changed for non-equality predicate *)
paulson@15347
   426
(* The input "pred" cannot be an equality *)
paulson@15347
   427
fun pred_of_nonEq (pred,args) = 
quigley@17150
   428
    let val (predName,(predType,ts1), pfuncs) = pred_name_type pred
quigley@17150
   429
	val (args',ts_funcs) = ListPair.unzip (map term_of args)
quigley@17150
   430
        val (ts2,ffuncs) = ListPair.unzip ( ts_funcs)
paulson@15347
   431
	val ts3 = ResLib.flat_noDup (ts1::ts2)
quigley@17150
   432
        val ffuncs' = (ResLib.flat_noDup (ffuncs))
quigley@17150
   433
        val newfuncs = distinct (pfuncs@ffuncs')
quigley@17150
   434
        val pred_arity = (*if ((length ts3) <> 0) 
quigley@17150
   435
			 then 
quigley@17150
   436
			    ((length args) +(length ts3))
quigley@17150
   437
			 else*)
quigley@17150
   438
                           (* just doing length args if untyped seems to work*)
quigley@17150
   439
			    (if !keep_types then (length args)+1 else (length args))
paulson@15347
   440
    in
quigley@17150
   441
	(Predicate(predName,predType,args'),ts3, [(predName, pred_arity)], newfuncs)
paulson@15347
   442
    end;
paulson@15347
   443
paulson@15347
   444
paulson@15347
   445
(* Changed for typed equality *)
paulson@15347
   446
(* First check if the predicate is an equality or not, then call different functions for equality and non-equalities *)
paulson@15347
   447
fun predicate_of term =
paulson@15347
   448
    let val (pred,args) = strip_comb term
paulson@15347
   449
    in
paulson@15347
   450
	case pred of (Const ("op =", _)) => pred_of_eq (pred,args)
paulson@15347
   451
		   | _ => pred_of_nonEq (pred,args)
paulson@15347
   452
    end;
paulson@15347
   453
paulson@15347
   454
 
quigley@17150
   455
quigley@17150
   456
fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) = literals_of_term(P,lits_ts, preds, funcs)
quigley@17150
   457
  | literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts), preds,funcs) = 
quigley@17150
   458
    let val (lits',ts', preds', funcs') = literals_of_term(P,(lits,ts), preds,funcs)
quigley@17150
   459
    in
quigley@17150
   460
        literals_of_term(Q,(lits',ts'), distinct(preds'@preds), distinct(funcs'@funcs))
quigley@17150
   461
    end
quigley@17150
   462
  | literals_of_term ((Const("Not",_) $ P),(lits,ts), preds, funcs) = 
quigley@17150
   463
    let val (pred,ts', preds', funcs') = predicate_of P
quigley@17150
   464
        val lits' = Literal(false,pred,false) :: lits
quigley@17150
   465
        val ts'' = ResLib.no_rep_app ts ts'
quigley@17150
   466
    in
quigley@17150
   467
        (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
quigley@17150
   468
    end
quigley@17150
   469
  | literals_of_term (P,(lits,ts), preds, funcs) = 
quigley@17150
   470
    let val (pred,ts', preds', funcs') = predicate_of P
quigley@17150
   471
        val lits' = Literal(true,pred,false) :: lits
quigley@17150
   472
        val ts'' = ResLib.no_rep_app ts ts' 
quigley@17150
   473
    in
quigley@17150
   474
        (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
quigley@17150
   475
    end;
quigley@17150
   476
quigley@17150
   477
quigley@17150
   478
fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]), [], []);
quigley@17150
   479
quigley@17150
   480
quigley@17150
   481
(* FIX: not sure what to do with these funcs *)
quigley@17150
   482
paulson@16199
   483
(*Make literals for sorted type variables*) 
quigley@17150
   484
fun sorts_on_typs (_, [])   = ([]) 
paulson@16199
   485
  | sorts_on_typs (v, "HOL.type" :: s) =
paulson@16199
   486
      sorts_on_typs (v,s)   (*Ignore sort "type"*)
paulson@16199
   487
  | sorts_on_typs ((FOLTVar(indx)), (s::ss)) =
quigley@17150
   488
      (LTVar((make_type_class s) ^ 
quigley@17150
   489
        "(" ^ (make_schematic_type_var( indx)) ^ ")") :: 
quigley@17150
   490
      (sorts_on_typs ((FOLTVar(indx)), ss)))
paulson@16199
   491
  | sorts_on_typs ((FOLTFree(x)), (s::ss)) =
paulson@16199
   492
      LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var(x)) ^ ")") :: 
paulson@16199
   493
      (sorts_on_typs ((FOLTFree(x)), ss));
paulson@15347
   494
quigley@17150
   495
quigley@17150
   496
fun takeUntil ch [] res  = (res, [])
quigley@17150
   497
 |   takeUntil ch (x::xs) res = if   x = ch 
quigley@17150
   498
                                then
quigley@17150
   499
                                     (res, xs)
quigley@17150
   500
                                else
quigley@17150
   501
                                     takeUntil ch xs (res@[x])
quigley@17150
   502
quigley@17150
   503
fun remove_type str = let val exp = explode str
quigley@17150
   504
		 	  val (first,rest) =  (takeUntil "(" exp [])
quigley@17150
   505
                      in
quigley@17150
   506
                        implode first
quigley@17150
   507
		      end
quigley@17150
   508
quigley@17150
   509
fun pred_of_sort (LTVar x) = ((remove_type x),1)
quigley@17150
   510
|   pred_of_sort (LTFree x) = ((remove_type x),1)
quigley@17150
   511
quigley@17150
   512
quigley@17150
   513
quigley@17150
   514
paulson@16199
   515
(*Given a list of sorted type variables, return two separate lists.
paulson@16199
   516
  The first is for TVars, the second for TFrees.*)
quigley@17150
   517
fun add_typs_aux [] preds  = ([],[], preds)
quigley@17150
   518
  | add_typs_aux ((FOLTVar(indx),s)::tss) preds = 
quigley@17150
   519
      let val (vs) = sorts_on_typs (FOLTVar(indx), s)
quigley@17150
   520
          val preds' = (map pred_of_sort vs)@preds
quigley@17150
   521
	  val (vss,fss, preds'') = add_typs_aux tss preds'
quigley@17150
   522
      in
quigley@17150
   523
	  (ResLib.no_rep_app vs vss, fss, preds'')
quigley@17150
   524
      end
quigley@17150
   525
  | add_typs_aux ((FOLTFree(x),s)::tss) preds  =
quigley@17150
   526
      let val (fs) = sorts_on_typs (FOLTFree(x), s)
quigley@17150
   527
          val preds' = (map pred_of_sort fs)@preds
quigley@17150
   528
	  val (vss,fss, preds'') = add_typs_aux tss preds'
quigley@17150
   529
      in
quigley@17150
   530
	  (vss, ResLib.no_rep_app fs fss,preds'')
quigley@17150
   531
      end;
quigley@17150
   532
quigley@17150
   533
quigley@17150
   534
(*fun add_typs_aux [] = ([],[])
paulson@15347
   535
  | add_typs_aux ((FOLTVar(indx),s)::tss) = 
paulson@16199
   536
      let val vs = sorts_on_typs (FOLTVar(indx), s)
paulson@16199
   537
	  val (vss,fss) = add_typs_aux tss
paulson@16199
   538
      in
paulson@16199
   539
	  (ResLib.no_rep_app vs vss, fss)
paulson@16199
   540
      end
paulson@15347
   541
  | add_typs_aux ((FOLTFree(x),s)::tss) =
paulson@16199
   542
      let val fs = sorts_on_typs (FOLTFree(x), s)
paulson@16199
   543
	  val (vss,fss) = add_typs_aux tss
paulson@16199
   544
      in
paulson@16199
   545
	  (vss, ResLib.no_rep_app fs fss)
quigley@17150
   546
      end;*)
paulson@15347
   547
quigley@17150
   548
quigley@17150
   549
fun add_typs (Clause cls) preds  = add_typs_aux (#types_sorts cls) preds 
paulson@15347
   550
paulson@15347
   551
paulson@15347
   552
(** make axiom clauses, hypothesis clauses and conjecture clauses. **)
quigley@17150
   553
quigley@17150
   554
local 
quigley@17150
   555
    fun replace_dot "." = "_"
quigley@17150
   556
      | replace_dot "'" = ""
quigley@17150
   557
      | replace_dot c = c;
quigley@17150
   558
quigley@17150
   559
in
quigley@17150
   560
quigley@17150
   561
fun proper_ax_name ax_name = 
quigley@17150
   562
    let val chars = explode ax_name
quigley@17150
   563
    in
quigley@17150
   564
	implode (map replace_dot chars)
quigley@17150
   565
    end;
quigley@17150
   566
end;
paulson@15347
   567
quigley@17150
   568
fun get_tvar_strs [] = []
quigley@17150
   569
  | get_tvar_strs ((FOLTVar(indx),s)::tss) = 
quigley@17150
   570
      let val vstr =(make_schematic_type_var( indx));
quigley@17150
   571
          val (vstrs) = get_tvar_strs tss
quigley@17150
   572
      in
quigley@17150
   573
	  (distinct( vstr:: vstrs))
quigley@17150
   574
      end
quigley@17150
   575
  | get_tvar_strs((FOLTFree(x),s)::tss) =
quigley@17150
   576
      let val (vstrs) = get_tvar_strs tss
quigley@17150
   577
      in
quigley@17150
   578
	  (distinct( vstrs))
quigley@17150
   579
      end;
quigley@17150
   580
quigley@17150
   581
(* FIX add preds and funcs to add typs aux here *)
quigley@17150
   582
quigley@17150
   583
fun make_axiom_clause_thm thm (name,number)=
quigley@17150
   584
    let val (lits,types_sorts, preds, funcs) = literals_of_thm thm
quigley@17150
   585
	val cls_id = number
quigley@17150
   586
	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
quigley@17150
   587
        val tvars = get_tvar_strs types_sorts
quigley@17150
   588
	val ax_name = proper_ax_name name
quigley@17150
   589
    in 
quigley@17150
   590
	make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs)
paulson@15347
   591
    end;
paulson@15347
   592
paulson@15347
   593
quigley@17150
   594
quigley@17150
   595
fun make_conjecture_clause_thm thm =
quigley@17150
   596
    let val (lits,types_sorts, preds, funcs) = literals_of_thm thm
quigley@17150
   597
	val cls_id = generate_id()
quigley@17150
   598
	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
quigley@17150
   599
        val tvars = get_tvar_strs types_sorts
quigley@17150
   600
    in
quigley@17150
   601
	make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs)
quigley@17150
   602
    end;
quigley@17150
   603
quigley@17150
   604
quigley@17150
   605
fun make_axiom_clause term (name,number)=
quigley@17150
   606
    let val (lits,types_sorts, preds,funcs) = literals_of_term (term,([],[]), [],[])
quigley@17150
   607
	val cls_id = number
quigley@17150
   608
	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts  preds 
quigley@17150
   609
        val tvars = get_tvar_strs types_sorts	
quigley@17150
   610
	val ax_name = proper_ax_name name
paulson@15347
   611
    in 
quigley@17150
   612
	make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs)
paulson@15347
   613
    end;
paulson@15347
   614
paulson@15347
   615
paulson@15347
   616
fun make_hypothesis_clause term =
quigley@17150
   617
    let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[])
paulson@15347
   618
	val cls_id = generate_id()
quigley@17150
   619
	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts  preds 
quigley@17150
   620
        val tvars = get_tvar_strs types_sorts
paulson@15347
   621
    in
quigley@17150
   622
	make_clause(cls_id,"",Hypothesis,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs)
paulson@15347
   623
    end;
paulson@15347
   624
    
paulson@15347
   625
 
paulson@15347
   626
fun make_conjecture_clause term =
quigley@17150
   627
    let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[])
paulson@15347
   628
	val cls_id = generate_id()
quigley@17150
   629
	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts  preds 
quigley@17150
   630
        val tvars = get_tvar_strs types_sorts	
paulson@15347
   631
    in
quigley@17150
   632
	make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs)
paulson@15347
   633
    end;
paulson@15347
   634
 
paulson@15347
   635
paulson@15347
   636
 
paulson@15347
   637
(**** Isabelle arities ****)
paulson@15347
   638
paulson@15347
   639
exception ARCLAUSE of string;
paulson@15347
   640
 
paulson@15347
   641
paulson@15347
   642
type class = string; 
paulson@15347
   643
type tcons = string; 
paulson@15347
   644
paulson@15347
   645
paulson@15347
   646
datatype arLit = TConsLit of bool * (class * tcons * string list) | TVarLit of bool * (class * string);
paulson@15347
   647
 
paulson@15347
   648
datatype arityClause =  
paulson@15347
   649
	 ArityClause of {clause_id: clause_id,
paulson@15347
   650
			 kind: kind,
paulson@15347
   651
			 conclLit: arLit,
paulson@15347
   652
			 premLits: arLit list};
paulson@15347
   653
paulson@15347
   654
paulson@15347
   655
fun get_TVars 0 = []
paulson@15347
   656
  | get_TVars n = ("T_" ^ (string_of_int n)) :: get_TVars (n-1);
paulson@15347
   657
paulson@15347
   658
paulson@15347
   659
paulson@15347
   660
fun pack_sort(_,[])  = raise ARCLAUSE("Empty Sort Found") 
paulson@15347
   661
  | pack_sort(tvar, [cls]) = [(make_type_class cls, tvar)] 
paulson@15347
   662
  | pack_sort(tvar, cls::srt) =  (make_type_class cls,tvar) :: (pack_sort(tvar, srt));
paulson@15347
   663
    
paulson@15347
   664
    
paulson@15347
   665
fun make_TVarLit (b,(cls,str)) = TVarLit(b,(cls,str));
paulson@15347
   666
fun make_TConsLit (b,(cls,tcons,tvars)) = TConsLit(b,(make_type_class cls,make_fixed_type_const tcons,tvars));
paulson@15347
   667
paulson@15347
   668
paulson@15347
   669
fun make_arity_clause (clause_id,kind,conclLit,premLits) =
paulson@15347
   670
    ArityClause {clause_id = clause_id, kind = kind, conclLit = conclLit, premLits = premLits};
paulson@15347
   671
paulson@15347
   672
paulson@15347
   673
fun make_axiom_arity_clause (tcons,(res,args)) =
paulson@15347
   674
     let val cls_id = generate_id()
paulson@15347
   675
	 val nargs = length args
paulson@15347
   676
	 val tvars = get_TVars nargs
paulson@15347
   677
	 val conclLit = make_TConsLit(true,(res,tcons,tvars))
paulson@15774
   678
         val tvars_srts = ListPair.zip (tvars,args)
paulson@15347
   679
	 val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts)
paulson@15347
   680
         val false_tvars_srts' = ResLib.pair_ins false tvars_srts'
paulson@15347
   681
	 val premLits = map make_TVarLit false_tvars_srts'
paulson@15347
   682
     in
paulson@15347
   683
	 make_arity_clause (cls_id,Axiom,conclLit,premLits)
paulson@15347
   684
     end;
paulson@15347
   685
    
paulson@15347
   686
paulson@15347
   687
paulson@15347
   688
(**** Isabelle class relations ****)
paulson@15347
   689
paulson@15347
   690
paulson@15347
   691
datatype classrelClause = 
paulson@15347
   692
	 ClassrelClause of {clause_id: clause_id,
paulson@15347
   693
			    subclass: class,
skalberg@15531
   694
			    superclass: class option};
paulson@15347
   695
paulson@15347
   696
fun make_classrelClause (clause_id,subclass,superclass) =
paulson@15347
   697
    ClassrelClause {clause_id = clause_id,subclass = subclass, superclass = superclass};
paulson@15347
   698
paulson@15347
   699
paulson@15347
   700
fun make_axiom_classrelClause (subclass,superclass) =
paulson@15347
   701
    let val cls_id = generate_id()
paulson@15347
   702
	val sub = make_type_class subclass
skalberg@15531
   703
	val sup = case superclass of NONE => NONE 
skalberg@15531
   704
				   | SOME s => SOME (make_type_class s)
paulson@15347
   705
    in
paulson@15347
   706
	make_classrelClause(cls_id,sub,sup)
paulson@15347
   707
    end;
paulson@15347
   708
paulson@15347
   709
paulson@15347
   710
paulson@15347
   711
fun classrelClauses_of_aux (sub,[]) = []
skalberg@15531
   712
  | classrelClauses_of_aux (sub,(sup::sups)) = make_axiom_classrelClause(sub,SOME sup) :: (classrelClauses_of_aux (sub,sups));
paulson@15347
   713
paulson@15347
   714
paulson@15347
   715
fun classrelClauses_of (sub,sups) = 
skalberg@15531
   716
    case sups of [] => [make_axiom_classrelClause (sub,NONE)]
paulson@15347
   717
	       | _ => classrelClauses_of_aux (sub, sups);
paulson@15347
   718
paulson@15347
   719
paulson@15347
   720
quigley@17150
   721
(***** convert clauses to DFG format *****)
paulson@15347
   722
paulson@15347
   723
quigley@17150
   724
fun string_of_clauseID (Clause cls) = clause_prefix ^ (string_of_int (#clause_id cls));
quigley@17150
   725
paulson@15347
   726
paulson@15347
   727
fun string_of_kind (Clause cls) = name_of_kind (#kind cls);
paulson@15347
   728
paulson@15347
   729
fun string_of_axiomName (Clause cls) = #axiom_name cls;
paulson@15347
   730
paulson@15347
   731
(****!!!! Changed for typed equality !!!!****)
paulson@15347
   732
fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")";
paulson@15347
   733
paulson@15347
   734
paulson@15347
   735
(****!!!! Changed for typed equality !!!!****)
paulson@15347
   736
(* Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed && if we specifically ask for types to be included.   *)
paulson@15347
   737
fun string_of_equality (typ,terms) =
paulson@15347
   738
    let val [tstr1,tstr2] = map string_of_term terms
paulson@15347
   739
    in
paulson@15347
   740
	if ((!keep_types) andalso (!special_equal)) then 
paulson@15347
   741
	    "equal(" ^ (wrap_eq_type typ tstr1) ^ "," ^ (wrap_eq_type typ tstr2) ^ ")"
paulson@15347
   742
	else
paulson@15347
   743
	    "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")"
paulson@15615
   744
    end
paulson@15615
   745
quigley@17150
   746
paulson@15615
   747
and
paulson@15615
   748
    string_of_term (UVar(x,_)) = x
paulson@15615
   749
  | string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms)
paulson@15615
   750
  | string_of_term (Fun (name,typ,[])) = name
paulson@15615
   751
  | string_of_term (Fun (name,typ,terms)) = 
paulson@15615
   752
    let val terms' = map string_of_term terms
paulson@15615
   753
    in
paulson@16925
   754
        if !keep_types andalso typ<>"" then name ^ (ResLib.list_to_string (terms' @ [typ]))
paulson@15615
   755
        else name ^ (ResLib.list_to_string terms')
paulson@15347
   756
    end;
paulson@15347
   757
paulson@15347
   758
paulson@15347
   759
paulson@15347
   760
(* Changed for typed equality *)
paulson@15347
   761
(* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
quigley@17150
   762
fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms)
quigley@17150
   763
  | string_of_predicate (Predicate(name,_,[])) = name 
quigley@17150
   764
  | string_of_predicate (Predicate(name,typ,terms)) = 
quigley@17150
   765
    let val terms_as_strings = map string_of_term terms
quigley@17150
   766
    in
quigley@17150
   767
        if (!keep_types) then name ^ (ResLib.list_to_string  (typ :: terms_as_strings))
quigley@17150
   768
        else name ^ (ResLib.list_to_string terms_as_strings) 
quigley@17150
   769
    end;
quigley@17150
   770
quigley@17150
   771
    
quigley@17150
   772
quigley@17150
   773
(********************************)
quigley@17150
   774
(* Code for producing DFG files *)
quigley@17150
   775
(********************************)
quigley@17150
   776
quigley@17150
   777
fun dfg_literal (Literal(pol,pred,tag)) =
quigley@17150
   778
    let val pred_string = string_of_predicate pred
quigley@17150
   779
	val tagged_pol =if pol then pred_string else "not(" ^pred_string ^ ")"
quigley@17150
   780
     in
quigley@17150
   781
	tagged_pol  
quigley@17150
   782
    end;
quigley@17150
   783
quigley@17150
   784
quigley@17150
   785
(* FIX: what does this mean? *)
quigley@17150
   786
(*fun dfg_of_typeLit (LTVar x) = "not(" ^ x ^ ")"
quigley@17150
   787
  | dfg_of_typeLit (LTFree x) = "(" ^ x ^ ")";*)
quigley@17150
   788
quigley@17150
   789
fun dfg_of_typeLit (LTVar x) =  x 
quigley@17150
   790
  | dfg_of_typeLit (LTFree x) = x ;
quigley@17150
   791
 
quigley@17150
   792
quigley@17150
   793
fun strlist [] = ""
quigley@17150
   794
|   strlist (x::[]) = x 
quigley@17150
   795
|   strlist (x::xs) = x ^ "," ^ (strlist xs)
quigley@17150
   796
quigley@17150
   797
quigley@17150
   798
fun gen_dfg_cls (cls_id,ax_name,knd,lits, tvars,vars) = 
quigley@17150
   799
    let val ax_str = (if ax_name = "" then "" else ("_" ^ ax_name))
quigley@17150
   800
        val forall_str = if (vars = []) andalso (tvars = []) 
quigley@17150
   801
			 then 
quigley@17150
   802
				""
quigley@17150
   803
			 else 
quigley@17150
   804
			 	"forall([" ^ (strlist (vars@tvars))^ "]"
quigley@17150
   805
    in
quigley@17150
   806
	if forall_str = "" 
quigley@17150
   807
	then 
quigley@17150
   808
		"clause( %(" ^ knd ^ ")\n" ^ "or(" ^ lits ^ ") ,\n" ^  cls_id ^ ax_str ^  ")."
quigley@17150
   809
        else	
quigley@17150
   810
		"clause( %(" ^ knd ^ ")\n" ^ forall_str ^ ",\n" ^ "or(" ^ lits ^ ")),\n" ^  cls_id ^ ax_str ^  ")."
quigley@17150
   811
    end;
quigley@17150
   812
quigley@17150
   813
quigley@17150
   814
quigley@17150
   815
fun gen_dfg_type_cls (cls_id,knd,tfree_lit,idx,tvars,  vars) = 
quigley@17150
   816
    let  val forall_str = if (vars = []) andalso (tvars = []) 
quigley@17150
   817
			 then 
quigley@17150
   818
				""
quigley@17150
   819
			 else 
quigley@17150
   820
			 	"forall([" ^ (strlist (vars@tvars))^"]"
quigley@17150
   821
    in
quigley@17150
   822
	if forall_str = "" 
quigley@17150
   823
	then 
quigley@17150
   824
		"clause( %(" ^ knd ^ ")\n" ^ "or( " ^ tfree_lit ^ ") ,\n" ^  cls_id ^ "_tcs" ^ (string_of_int idx) ^  ")."
quigley@17150
   825
        else	
quigley@17150
   826
		"clause( %(" ^ knd ^ ")\n" ^ forall_str ^ ",\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^  cls_id ^ "_tcs" ^ (string_of_int idx) ^  ")."
quigley@17150
   827
    end;
quigley@17150
   828
quigley@17150
   829
quigley@17150
   830
quigley@17150
   831
fun dfg_clause_aux (Clause cls) = 
quigley@17150
   832
    let val lits = map dfg_literal (#literals cls)
quigley@17150
   833
	val tvar_lits_strs = if (!keep_types) then (map dfg_of_typeLit (#tvar_type_literals cls)) else []
quigley@17150
   834
	val tfree_lits = if (!keep_types) then (map dfg_of_typeLit (#tfree_type_literals cls)) else []
quigley@17150
   835
    in
quigley@17150
   836
	(tvar_lits_strs @ lits,tfree_lits)
quigley@17150
   837
    end; 
quigley@17150
   838
quigley@17150
   839
quigley@17150
   840
fun dfg_folterms (Literal(pol,pred,tag)) = 
quigley@17150
   841
    let val  Predicate (predname, foltype, folterms) = pred
quigley@17150
   842
    in
quigley@17150
   843
	folterms
quigley@17150
   844
    end
quigley@17150
   845
quigley@17150
   846
 
quigley@17150
   847
fun get_uvars (UVar(str,typ)) =(*if (substring (str, 0,2))= "V_" then  *)[str] (*else []*)
quigley@17150
   848
|   get_uvars (Fun (str,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist)
quigley@17150
   849
quigley@17150
   850
quigley@17150
   851
fun is_uvar  (UVar(str,typ)) = true
quigley@17150
   852
|   is_uvar  (Fun (str,typ,tlist)) = false;
quigley@17150
   853
quigley@17150
   854
fun uvar_name  (UVar(str,typ)) = str
quigley@17150
   855
|   uvar_name  _ = (raise CLAUSE("Not a variable"));
quigley@17150
   856
quigley@17150
   857
quigley@17150
   858
fun mergelist [] = []
quigley@17150
   859
|   mergelist (x::xs ) = x@(mergelist xs)
quigley@17150
   860
quigley@17150
   861
quigley@17150
   862
fun dfg_vars (Clause cls) =
quigley@17150
   863
    let val  lits =  (#literals cls)
quigley@17150
   864
        val  folterms = mergelist(map dfg_folterms lits)
quigley@17150
   865
        val vars =  ResLib.flat_noDup(map get_uvars folterms)	
quigley@17150
   866
    in 
quigley@17150
   867
        vars
quigley@17150
   868
    end
quigley@17150
   869
quigley@17150
   870
quigley@17150
   871
fun dfg_tvars (Clause cls) =(#tvars cls)
quigley@17150
   872
quigley@17150
   873
quigley@17150
   874
	
quigley@17150
   875
(* make this return funcs and preds too? *)
quigley@17150
   876
fun string_of_predname (Predicate("equal",typ,terms)) = "EQUALITY"
quigley@17150
   877
  | string_of_predname (Predicate(name,_,[])) = name 
quigley@17150
   878
  | string_of_predname (Predicate(name,typ,terms)) = name
quigley@17150
   879
    
quigley@17150
   880
	
quigley@17150
   881
(* make this return funcs and preds too? *)
quigley@17150
   882
quigley@17150
   883
    fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms)
paulson@15347
   884
  | string_of_predicate (Predicate(name,_,[])) = name 
paulson@15347
   885
  | string_of_predicate (Predicate(name,typ,terms)) = 
paulson@16903
   886
      let val terms_as_strings = map string_of_term terms
paulson@16903
   887
      in
paulson@16925
   888
	  if !keep_types andalso typ<>""
paulson@16903
   889
	  then name ^ (ResLib.list_to_string  (terms_as_strings @ [typ]))
paulson@16903
   890
	  else name ^ (ResLib.list_to_string terms_as_strings) 
paulson@16903
   891
      end;
paulson@15347
   892
quigley@17150
   893
quigley@17150
   894
quigley@17150
   895
quigley@17150
   896
fun concat_with sep []  = ""
quigley@17150
   897
  | concat_with sep [x] = "(" ^ x ^ ")"
quigley@17150
   898
  | concat_with sep (x::xs) = "(" ^ x ^ ")" ^  sep ^ (concat_with sep xs);
quigley@17150
   899
quigley@17150
   900
fun concat_with_comma []  = ""
quigley@17150
   901
  | concat_with_comma [x] =  x 
quigley@17150
   902
  | concat_with_comma (x::xs) =  x  ^ ", " ^ (concat_with_comma xs);
quigley@17150
   903
quigley@17150
   904
quigley@17150
   905
fun dfg_pred (Literal(pol,pred,tag)) ax_name = (string_of_predname pred)^" "^ax_name
quigley@17150
   906
quigley@17150
   907
fun dfg_clause cls =
quigley@17150
   908
    let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)
quigley@17150
   909
        val vars = dfg_vars cls
quigley@17150
   910
        val tvars = dfg_tvars cls
quigley@17150
   911
	val cls_id = string_of_clauseID cls
quigley@17150
   912
	val ax_name = string_of_axiomName cls
quigley@17150
   913
	val knd = string_of_kind cls
quigley@17150
   914
	val lits_str = concat_with_comma lits
quigley@17150
   915
	val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars, vars) 			
quigley@17150
   916
        fun typ_clss k [] = []
quigley@17150
   917
          | typ_clss k (tfree :: tfrees) = 
quigley@17150
   918
            (gen_dfg_type_cls(cls_id,knd,tfree,k, tvars,vars)) ::  (typ_clss (k+1) tfrees)
quigley@17150
   919
    in 
quigley@17150
   920
	cls_str :: (typ_clss 0 tfree_lits)
quigley@17150
   921
    end;
quigley@17150
   922
quigley@17150
   923
fun clause_info cls =
quigley@17150
   924
    let 
quigley@17150
   925
	val cls_id = string_of_clauseID cls
quigley@17150
   926
	val ax_name = string_of_axiomName cls
quigley@17150
   927
    in 
quigley@17150
   928
	((ax_name^""), cls_id)
quigley@17150
   929
    end;
quigley@17150
   930
quigley@17150
   931
quigley@17150
   932
quigley@17150
   933
fun zip_concat name  [] = []
quigley@17150
   934
|   zip_concat  name ((str, num)::xs) = (((str^name), num)::(zip_concat name xs))
quigley@17150
   935
quigley@17150
   936
quigley@17150
   937
(*fun funcs_of_cls (Clause cls) = let val funcs = #functions cls
quigley@17150
   938
 				    val name = #axiom_name cls
quigley@17150
   939
				in
quigley@17150
   940
				    zip_concat name funcs 
quigley@17150
   941
				end;
quigley@17150
   942
quigley@17150
   943
quigley@17150
   944
fun preds_of_cls (Clause cls) = let val preds = #predicates cls
quigley@17150
   945
;                                   val name = ("foo"^(#axiom_name cls))
quigley@17150
   946
				in
quigley@17150
   947
				    zip_concat name preds
quigley@17150
   948
				end
quigley@17150
   949
*)
quigley@17150
   950
quigley@17150
   951
fun funcs_of_cls (Clause cls) = #functions cls;
quigley@17150
   952
quigley@17150
   953
quigley@17150
   954
fun preds_of_cls (Clause cls) = #predicates cls;
quigley@17150
   955
quigley@17150
   956
quigley@17150
   957
quigley@17150
   958
quigley@17150
   959
fun string_of_arity (name, num) =  name ^"," ^ (string_of_int num) 
quigley@17150
   960
quigley@17150
   961
quigley@17150
   962
fun string_of_preds preds =  "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n";
quigley@17150
   963
quigley@17150
   964
fun string_of_funcs funcs ="functions[" ^ (concat_with ", " (map string_of_arity funcs)) ^ "].\n" ;
quigley@17150
   965
quigley@17150
   966
quigley@17150
   967
fun string_of_symbols predstr funcstr = "list_of_symbols.\n" ^ predstr  ^ funcstr  ^ "end_of_list.\n\n";
quigley@17150
   968
quigley@17150
   969
quigley@17150
   970
fun string_of_axioms axstr = "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n";
quigley@17150
   971
quigley@17150
   972
quigley@17150
   973
fun string_of_conjectures conjstr = "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n";
quigley@17150
   974
quigley@17150
   975
fun string_of_descrip () = "list_of_descriptions.\nname({*[ File     : ],[ Names    :]*}).\nauthor({*[ Source   :]*}).\nstatus(unknown).\ndescription({*[ Refs     :]*}).\nend_of_list.\n\n"
quigley@17150
   976
quigley@17150
   977
quigley@17150
   978
fun string_of_start name = "%------------------------------------------------------------------------------\nbegin_problem(" ^ name ^ ").\n\n";
quigley@17150
   979
quigley@17150
   980
quigley@17150
   981
fun string_of_end () = "end_problem.\n%------------------------------------------------------------------------------";
quigley@17150
   982
quigley@17150
   983
val delim = "\n";
quigley@17150
   984
val dfg_clauses2str = ResLib.list2str_sep delim; 
quigley@17150
   985
     
quigley@17150
   986
quigley@17150
   987
fun clause2dfg cls =
quigley@17150
   988
    let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)
quigley@17150
   989
	val cls_id = string_of_clauseID cls
quigley@17150
   990
	val ax_name = string_of_axiomName cls
quigley@17150
   991
        val vars = dfg_vars cls
quigley@17150
   992
        val tvars = dfg_tvars cls
quigley@17150
   993
        val funcs = funcs_of_cls cls
quigley@17150
   994
        val preds = preds_of_cls cls
quigley@17150
   995
	val knd = string_of_kind cls
quigley@17150
   996
	val lits_str = concat_with_comma lits
quigley@17150
   997
	val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars,vars) 
quigley@17150
   998
    in
quigley@17150
   999
	(cls_str,tfree_lits) 
quigley@17150
  1000
    end;
quigley@17150
  1001
quigley@17150
  1002
quigley@17150
  1003
quigley@17150
  1004
fun tfree_dfg_clause tfree_lit = "clause( %(conjecture)\n" ^  "or( " ^ tfree_lit ^ ")),\n" ^ "tfree_tcs" ^  ")."
quigley@17150
  1005
quigley@17150
  1006
quigley@17150
  1007
fun gen_dfg_file fname axioms conjectures funcs preds tfrees= 
quigley@17150
  1008
    let val (axstrs_tfrees) = (map clause2dfg axioms)
quigley@17150
  1009
	val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
quigley@17150
  1010
        val axstr = ResLib.list2str_sep delim axstrs
quigley@17150
  1011
        val (conjstrs_tfrees) = (map clause2dfg conjectures)
quigley@17150
  1012
	val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
quigley@17150
  1013
        val tfree_clss = map tfree_dfg_clause ((ResLib.flat_noDup atfrees) \\ tfrees) 
quigley@17150
  1014
        val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs)
quigley@17150
  1015
        val funcstr = string_of_funcs funcs
quigley@17150
  1016
        val predstr = string_of_preds preds
quigley@17150
  1017
    in
quigley@17150
  1018
  (string_of_start fname) ^ (string_of_descrip ()) ^ (string_of_symbols funcstr predstr ) ^  
quigley@17150
  1019
         (string_of_axioms axstr)^
quigley@17150
  1020
        (string_of_conjectures conjstr) ^ (string_of_end ())
quigley@17150
  1021
    end;
quigley@17150
  1022
   
quigley@17150
  1023
							    
quigley@17150
  1024
quigley@17150
  1025
fun clauses2dfg [] filename axioms conjectures funcs preds tfrees= 
quigley@17150
  1026
   let val funcs' = ((ResLib.flat_noDup(map funcs_of_cls axioms))@funcs)
quigley@17150
  1027
       val preds' = ((ResLib.flat_noDup(map preds_of_cls axioms))@preds)
quigley@17150
  1028
       
quigley@17150
  1029
   
quigley@17150
  1030
   in
quigley@17150
  1031
	gen_dfg_file filename axioms conjectures funcs' preds' tfrees 
quigley@17150
  1032
       (*(filename, axioms, conjectures, funcs, preds)*)
quigley@17150
  1033
   end
quigley@17150
  1034
|clauses2dfg (cls::clss) filename  axioms conjectures funcs preds tfrees = 
quigley@17150
  1035
    let val (lits,tfree_lits) = dfg_clause_aux (cls) (*"lits" includes the typing assumptions (TVars)*)
quigley@17150
  1036
	val cls_id = string_of_clauseID cls
quigley@17150
  1037
	val ax_name = string_of_axiomName cls
quigley@17150
  1038
        val vars = dfg_vars cls
quigley@17150
  1039
        val tvars = dfg_tvars cls
quigley@17150
  1040
        val funcs' = distinct((funcs_of_cls cls)@funcs)
quigley@17150
  1041
        val preds' = distinct((preds_of_cls cls)@preds)
quigley@17150
  1042
	val knd = string_of_kind cls
quigley@17150
  1043
	val lits_str = concat_with ", " lits
quigley@17150
  1044
	val axioms' = if knd = "axiom" then (cls::axioms) else axioms
quigley@17150
  1045
	val conjectures' = if knd = "conjecture" then (cls::conjectures) else conjectures
quigley@17150
  1046
    in
quigley@17150
  1047
	clauses2dfg clss filename axioms' conjectures' funcs' preds' tfrees 
quigley@17150
  1048
    end;
quigley@17150
  1049
quigley@17150
  1050
quigley@17150
  1051
fun fileout f str = let val out = TextIO.openOut(f)
quigley@17150
  1052
    in
quigley@17150
  1053
	ResLib.writeln_strs out (str); TextIO.closeOut out
quigley@17150
  1054
    end;
quigley@17150
  1055
quigley@17150
  1056
(*val filestr = clauses2dfg newcls "flump" [] [] [] [];
quigley@17150
  1057
*)
quigley@17150
  1058
(* fileout "flump.dfg" [filestr];*)
quigley@17150
  1059
quigley@17150
  1060
quigley@17150
  1061
(*FIX: ask Jia what this is for *)
quigley@17150
  1062
quigley@17150
  1063
quigley@17150
  1064
fun string_of_arClauseID (ArityClause arcls) = arclause_prefix ^ string_of_int(#clause_id arcls);
quigley@17150
  1065
quigley@17150
  1066
quigley@17150
  1067
fun string_of_arLit (TConsLit(b,(c,t,args))) =
quigley@17150
  1068
    let val pol = if b then "++" else "--"
quigley@17150
  1069
	val  arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args)
quigley@17150
  1070
    in 
quigley@17150
  1071
	pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
quigley@17150
  1072
    end
quigley@17150
  1073
  | string_of_arLit (TVarLit(b,(c,str))) =
quigley@17150
  1074
    let val pol = if b then "++" else "--"
quigley@17150
  1075
    in
quigley@17150
  1076
	pol ^ c ^ "(" ^ str ^ ")"
quigley@17150
  1077
    end;
paulson@15347
  1078
    
paulson@15347
  1079
quigley@17150
  1080
fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls);
quigley@17150
  1081
     
quigley@17150
  1082
quigley@17150
  1083
fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls);
quigley@17150
  1084
		
quigley@17150
  1085
quigley@17150
  1086
fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
quigley@17150
  1087
quigley@17150
  1088
(*FIX: would this have variables in a forall? *)
quigley@17150
  1089
quigley@17150
  1090
fun dfg_arity_clause arcls = 
quigley@17150
  1091
    let val arcls_id = string_of_arClauseID arcls
quigley@17150
  1092
	val concl_lit = string_of_conclLit arcls
quigley@17150
  1093
	val prems_lits = strings_of_premLits arcls
quigley@17150
  1094
	val knd = string_of_arKind arcls
quigley@17150
  1095
	val all_lits = concl_lit :: prems_lits
quigley@17150
  1096
    in
quigley@17150
  1097
quigley@17150
  1098
	"clause( %(" ^ knd ^ ")\n" ^  "or( " ^ (ResLib.list_to_string' all_lits) ^ ")),\n" ^ arcls_id ^  ")."
quigley@17150
  1099
    end;
quigley@17150
  1100
quigley@17150
  1101
quigley@17150
  1102
val clrelclause_prefix = "relcls_";
quigley@17150
  1103
quigley@17150
  1104
(* FIX later.  Doesn't seem to be used in clasimp *)
quigley@17150
  1105
quigley@17150
  1106
(*fun tptp_classrelLits sub sup = 
quigley@17150
  1107
    let val tvar = "(T)"
quigley@17150
  1108
    in 
quigley@17150
  1109
	case sup of NONE => "[++" ^ sub ^ tvar ^ "]"
quigley@17150
  1110
		  | (SOME supcls) =>  "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]"
quigley@17150
  1111
    end;
quigley@17150
  1112
quigley@17150
  1113
quigley@17150
  1114
fun tptp_classrelClause (ClassrelClause cls) =
quigley@17150
  1115
    let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls)
quigley@17150
  1116
	val sub = #subclass cls
quigley@17150
  1117
	val sup = #superclass cls
quigley@17150
  1118
	val lits = tptp_classrelLits sub sup
quigley@17150
  1119
    in
quigley@17150
  1120
	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")."
quigley@17150
  1121
    end; 
quigley@17150
  1122
    *)
quigley@17150
  1123
quigley@17150
  1124
(********************************)
quigley@17150
  1125
(* code to produce TPTP files   *)
quigley@17150
  1126
(********************************)
quigley@17150
  1127
quigley@17150
  1128
paulson@15347
  1129
paulson@15347
  1130
fun tptp_literal (Literal(pol,pred,tag)) =
paulson@15347
  1131
    let val pred_string = string_of_predicate pred
quigley@17150
  1132
	val tagged_pol = if (tag andalso !tagged) then (if pol then "+++" else "---")
quigley@17150
  1133
                         else (if pol then "++" else "--")
paulson@15347
  1134
     in
paulson@15347
  1135
	tagged_pol ^ pred_string
paulson@15347
  1136
    end;
paulson@15347
  1137
paulson@15347
  1138
paulson@15347
  1139
paulson@15347
  1140
fun tptp_of_typeLit (LTVar x) = "--" ^ x
paulson@15347
  1141
  | tptp_of_typeLit (LTFree x) = "++" ^ x;
paulson@15347
  1142
 
paulson@15347
  1143
paulson@15347
  1144
fun gen_tptp_cls (cls_id,ax_name,knd,lits) = 
quigley@17150
  1145
    let val ax_str = (if ax_name = "" then "" else ("_" ^ ax_name))
paulson@15347
  1146
    in
paulson@15347
  1147
	"input_clause(" ^ cls_id ^ ax_str ^ "," ^ knd ^ "," ^ lits ^ ")."
paulson@15347
  1148
    end;
paulson@15347
  1149
quigley@17150
  1150
quigley@17150
  1151
fun gen_tptp_type_cls (cls_id,knd,tfree_lit,idx) = "input_clause(" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ "," ^ knd ^ ",[" ^ tfree_lit ^ "]).";
paulson@15347
  1152
paulson@15347
  1153
paulson@15347
  1154
fun tptp_clause_aux (Clause cls) = 
paulson@15347
  1155
    let val lits = map tptp_literal (#literals cls)
quigley@17150
  1156
	val tvar_lits_strs = if (!keep_types) then (map tptp_of_typeLit (#tvar_type_literals cls)) else []
quigley@17150
  1157
	val tfree_lits = if (!keep_types) then (map tptp_of_typeLit (#tfree_type_literals cls)) else []
paulson@15347
  1158
    in
paulson@15347
  1159
	(tvar_lits_strs @ lits,tfree_lits)
paulson@15347
  1160
    end; 
paulson@15347
  1161
paulson@15608
  1162
paulson@15347
  1163
fun tptp_clause cls =
paulson@15347
  1164
    let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)
paulson@15347
  1165
	val cls_id = string_of_clauseID cls
paulson@15347
  1166
	val ax_name = string_of_axiomName cls
paulson@15347
  1167
	val knd = string_of_kind cls
paulson@15347
  1168
	val lits_str = ResLib.list_to_string' lits
paulson@15347
  1169
	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 			fun typ_clss k [] = []
paulson@15347
  1170
          | typ_clss k (tfree :: tfrees) = 
paulson@15347
  1171
            (gen_tptp_type_cls(cls_id,knd,tfree,k)) ::  (typ_clss (k+1) tfrees)
paulson@15347
  1172
    in 
paulson@15347
  1173
	cls_str :: (typ_clss 0 tfree_lits)
paulson@15347
  1174
    end;
paulson@15347
  1175
quigley@17150
  1176
fun clause_info cls =
quigley@17150
  1177
    let 
quigley@17150
  1178
	val cls_id = string_of_clauseID cls
quigley@17150
  1179
	val ax_name = string_of_axiomName cls
quigley@17150
  1180
    in 
quigley@17150
  1181
	((ax_name^""), cls_id)
quigley@17150
  1182
    end;
quigley@16039
  1183
paulson@15347
  1184
paulson@15608
  1185
fun clause2tptp cls =
paulson@15608
  1186
    let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)
paulson@15608
  1187
	val cls_id = string_of_clauseID cls
paulson@15608
  1188
	val ax_name = string_of_axiomName cls
paulson@15608
  1189
	val knd = string_of_kind cls
paulson@15608
  1190
	val lits_str = ResLib.list_to_string' lits
paulson@15608
  1191
	val cls_str = gen_tptp_cls(cls_id,ax_name,knd,lits_str) 
paulson@15608
  1192
    in
paulson@15608
  1193
	(cls_str,tfree_lits) 
paulson@15608
  1194
    end;
paulson@15608
  1195
paulson@15608
  1196
quigley@17150
  1197
fun tfree_clause tfree_lit = "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).";
paulson@15608
  1198
paulson@15347
  1199
val delim = "\n";
paulson@15347
  1200
val tptp_clauses2str = ResLib.list2str_sep delim; 
paulson@15347
  1201
     
paulson@15347
  1202
paulson@15347
  1203
fun string_of_arClauseID (ArityClause arcls) = arclause_prefix ^ string_of_int(#clause_id arcls);
paulson@15347
  1204
paulson@15347
  1205
paulson@15347
  1206
fun string_of_arLit (TConsLit(b,(c,t,args))) =
paulson@15347
  1207
    let val pol = if b then "++" else "--"
paulson@15347
  1208
	val  arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args)
paulson@15347
  1209
    in 
paulson@15347
  1210
	pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
paulson@15347
  1211
    end
paulson@15347
  1212
  | string_of_arLit (TVarLit(b,(c,str))) =
paulson@15347
  1213
    let val pol = if b then "++" else "--"
paulson@15347
  1214
    in
paulson@15347
  1215
	pol ^ c ^ "(" ^ str ^ ")"
paulson@15347
  1216
    end;
paulson@15347
  1217
    
paulson@15347
  1218
paulson@15347
  1219
fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls);
paulson@15347
  1220
     
paulson@15347
  1221
paulson@15347
  1222
fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls);
paulson@15347
  1223
		
paulson@15347
  1224
paulson@15347
  1225
fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
paulson@15347
  1226
paulson@15347
  1227
fun tptp_arity_clause arcls = 
paulson@15347
  1228
    let val arcls_id = string_of_arClauseID arcls
paulson@15347
  1229
	val concl_lit = string_of_conclLit arcls
paulson@15347
  1230
	val prems_lits = strings_of_premLits arcls
paulson@15347
  1231
	val knd = string_of_arKind arcls
paulson@15347
  1232
	val all_lits = concl_lit :: prems_lits
paulson@15347
  1233
    in
paulson@15452
  1234
	"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ (ResLib.list_to_string' all_lits) ^ ")."
paulson@15347
  1235
	
paulson@15347
  1236
    end;
paulson@15347
  1237
paulson@15347
  1238
paulson@15347
  1239
val clrelclause_prefix = "relcls_";
paulson@15347
  1240
paulson@15347
  1241
paulson@15347
  1242
fun tptp_classrelLits sub sup = 
paulson@15347
  1243
    let val tvar = "(T)"
paulson@15347
  1244
    in 
skalberg@15531
  1245
	case sup of NONE => "[++" ^ sub ^ tvar ^ "]"
skalberg@15531
  1246
		  | (SOME supcls) =>  "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]"
paulson@15347
  1247
    end;
paulson@15347
  1248
paulson@15347
  1249
paulson@15347
  1250
fun tptp_classrelClause (ClassrelClause cls) =
paulson@15347
  1251
    let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls)
paulson@15347
  1252
	val sub = #subclass cls
paulson@15347
  1253
	val sup = #superclass cls
paulson@15347
  1254
	val lits = tptp_classrelLits sub sup
paulson@15347
  1255
    in
paulson@15347
  1256
	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")."
paulson@15347
  1257
    end; 
quigley@17150
  1258
paulson@15347
  1259
end;