tidying up SPASS output
authorpaulson
Fri Jan 27 18:29:33 2006 +0100 (2006-01-27 ago)
changeset 18798ca02a2077955
parent 18797 8559cc115673
child 18799 f137c5e971f5
tidying up SPASS output
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Jan 27 18:29:11 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Jan 27 18:29:33 2006 +0100
     1.3 @@ -74,8 +74,8 @@
     1.4  fun dfg_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) = 
     1.5      let val clss = ResClause.make_conjecture_clauses (map prop_of ths)
     1.6          (*FIXME: classrel_clauses and arity_clauses*)
     1.7 -        val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n)
     1.8 -                        axclauses [] [] []    
     1.9 +        val probN = ResClause.clauses2dfg (!problem_name ^ "_" ^ Int.toString n)
    1.10 +                        axclauses clss 
    1.11  	val out = TextIO.openOut(pf n)
    1.12      in
    1.13  	writeln_strs out [probN]; TextIO.closeOut out
    1.14 @@ -106,14 +106,14 @@
    1.15                    val spass = helper_path "SPASS_HOME" "SPASS"
    1.16              in 
    1.17                  ([("spass", spass, infopts ^ baseopts, probfile)] @ 
    1.18 -                  (make_atp_list xs (n+1)))
    1.19 +                  make_atp_list xs (n+1))
    1.20                end
    1.21              else if !prover = "vampire"
    1.22  	    then 
    1.23                let val vampire = helper_path "VAMPIRE_HOME" "vampire"
    1.24                in
    1.25                  ([("vampire", vampire, "-m 100000%-t " ^ time, probfile)] @
    1.26 -                 (make_atp_list xs (n+1)))       (*BEWARE! spaces in options!*)
    1.27 +                 make_atp_list xs (n+1))       (*BEWARE! spaces in options!*)
    1.28                end
    1.29        	     else if !prover = "E"
    1.30        	     then
    1.31 @@ -122,7 +122,7 @@
    1.32  		  ([("E", Eprover, 
    1.33  		     "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time,
    1.34  		     probfile)] @
    1.35 -		   (make_atp_list xs (n+1)))
    1.36 +		   make_atp_list xs (n+1))
    1.37  	       end
    1.38  	     else error ("Invalid prover name: " ^ !prover)
    1.39            end
     2.1 --- a/src/HOL/Tools/res_clause.ML	Fri Jan 27 18:29:11 2006 +0100
     2.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Jan 27 18:29:33 2006 +0100
     2.3 @@ -26,8 +26,7 @@
     2.4    val num_of_clauses : clause -> int
     2.5  
     2.6    val clause2dfg : clause -> string * string list
     2.7 -  val clauses2dfg : clause list -> string -> clause list -> clause list ->
     2.8 -	   (string * int) list -> (string * int) list -> string
     2.9 +  val clauses2dfg : string -> clause list -> clause list -> string
    2.10    val tfree_dfg_clause : string -> string
    2.11  
    2.12    val arity_clause_thy: theory -> arityClause list 
    2.13 @@ -103,13 +102,10 @@
    2.14  
    2.15  val const_prefix = "c_";
    2.16  val tconst_prefix = "tc_"; 
    2.17 -
    2.18  val class_prefix = "class_"; 
    2.19  
    2.20 -
    2.21  fun union_all xss = foldl (op union) [] xss;
    2.22  
    2.23 - 
    2.24  (*Provide readable names for the more common symbolic functions*)
    2.25  val const_trans_table =
    2.26        Symtab.make [("op =", "equal"),
    2.27 @@ -197,8 +193,7 @@
    2.28  fun make_type_class clas = class_prefix ^ ascii_of clas;
    2.29  
    2.30  
    2.31 -
    2.32 -(***** definitions and functions for FOL clauses, prepared for conversion into TPTP format or SPASS format. *****)
    2.33 +(***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****)
    2.34  
    2.35  val keep_types = ref true;
    2.36  
    2.37 @@ -213,9 +208,6 @@
    2.38  
    2.39  type polarity = bool;
    2.40  
    2.41 -type indexname = Term.indexname;
    2.42 -
    2.43 -
    2.44  (* "tag" is used for vampire specific syntax  *)
    2.45  type tag = bool; 
    2.46  
    2.47 @@ -225,12 +217,10 @@
    2.48  val tagged = ref false;
    2.49  
    2.50  type pred_name = string;
    2.51 -type sort = Term.sort;
    2.52 -
    2.53 -
    2.54  
    2.55  datatype typ_var = FOLTVar of indexname | FOLTFree of string;
    2.56  
    2.57 +(*FIXME: give the constructors more sensible names*)
    2.58  datatype fol_type = AtomV of string
    2.59  		  | AtomF of string
    2.60  		  | Comp of string * fol_type list;
    2.61 @@ -248,8 +238,8 @@
    2.62    | mk_fol_type ("Comp",con,args) = Comp(con,args)
    2.63  
    2.64  
    2.65 -
    2.66 -datatype type_literal = LTVar of string | LTFree of string;
    2.67 +(*First string is the type class; the second is a TVar or TFfree*)
    2.68 +datatype type_literal = LTVar of string * string | LTFree of string * string;
    2.69  
    2.70  datatype folTerm = UVar of string * fol_type
    2.71                   | Fun of string * fol_type list * folTerm list;
    2.72 @@ -270,18 +260,12 @@
    2.73  		    literals: literal list,
    2.74  		    types_sorts: (typ_var * sort) list, 
    2.75                      tvar_type_literals: type_literal list, 
    2.76 -                    tfree_type_literals: type_literal list ,
    2.77 -                    tvars: string list,
    2.78 -                    predicates: (string*int) list,
    2.79 -                    functions: (string*int) list};
    2.80 +                    tfree_type_literals: type_literal list,
    2.81 +                    predicates: (string*int) list};
    2.82  
    2.83  
    2.84  exception CLAUSE of string * term;
    2.85  
    2.86 -fun get_literals (c as Clause(cls)) = #literals cls;
    2.87 -
    2.88 -fun components_of_literal (Literal (pol,pred,tag)) = ((pol,pred),tag);
    2.89 -
    2.90  fun predicate_name (Predicate(predname,_,_)) = predname;
    2.91  
    2.92  
    2.93 @@ -301,7 +285,7 @@
    2.94  
    2.95  fun make_clause (clause_id,axiom_name,kind,literals,
    2.96                   types_sorts,tvar_type_literals,
    2.97 -                 tfree_type_literals,tvars, predicates, functions) =
    2.98 +                 tfree_type_literals,predicates) =
    2.99    if forall isFalse literals 
   2.100    then error "Problem too trivial for resolution (empty clause)"
   2.101    else
   2.102 @@ -309,8 +293,7 @@
   2.103               literals = literals, types_sorts = types_sorts,
   2.104               tvar_type_literals = tvar_type_literals,
   2.105               tfree_type_literals = tfree_type_literals,
   2.106 -             tvars = tvars, predicates = predicates, 
   2.107 -             functions = functions};
   2.108 +             predicates = predicates};
   2.109  
   2.110  
   2.111  (** Some Clause destructor functions **)
   2.112 @@ -321,8 +304,6 @@
   2.113  
   2.114  fun get_clause_id (Clause cls) = #clause_id cls;
   2.115  
   2.116 -fun funcs_of_cls (Clause cls) = #functions cls;
   2.117 -
   2.118  fun preds_of_cls (Clause cls) = #predicates cls;
   2.119  
   2.120  
   2.121 @@ -339,23 +320,14 @@
   2.122  (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
   2.123    TVars it contains.*)    
   2.124  fun type_of (Type (a, Ts)) = 
   2.125 -      let val (folTyps, (ts, funcs)) = types_of Ts 
   2.126 +      let val (folTyps, ts) = types_of Ts 
   2.127  	  val t = make_fixed_type_const a
   2.128 -      in    
   2.129 -	  (Comp(t,folTyps), (ts, (t, length Ts)::funcs))
   2.130 -      end
   2.131 -  | type_of (TFree (a,s)) = 
   2.132 -      let val t = make_fixed_type_var a
   2.133 -      in (AtomF(t), ([((FOLTFree a),s)], [(t,0)])) end
   2.134 -  | type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), ([((FOLTVar v),s)], []))
   2.135 +      in (Comp(t,folTyps), ts) end
   2.136 +  | type_of (TFree (a,s)) = (AtomF(make_fixed_type_var a), [(FOLTFree a, s)]) 
   2.137 +  | type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), [(FOLTVar v, s)])
   2.138  and types_of Ts =
   2.139 -      let val foltyps_ts = map type_of Ts 
   2.140 -	  val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts
   2.141 -	  val (ts, funcslist) = ListPair.unzip ts_funcs
   2.142 -      in    
   2.143 -	  (folTyps, (union_all ts, union_all funcslist))
   2.144 -      end;
   2.145 -
   2.146 +      let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
   2.147 +      in (folTyps, union_all ts) end;
   2.148  
   2.149  
   2.150  fun const_types_of (c,T) = types_of (!const_typargs (c,T));
   2.151 @@ -364,12 +336,10 @@
   2.152     universal vars, although it is represented as "Free(...)" by Isabelle *)
   2.153  val isMeta = String.isPrefix "METAHYP1_"
   2.154  
   2.155 -fun pred_name_type (Const(c,T)) = 
   2.156 -      let val (contys,(folTyps,funcs)) = const_types_of (c,T)
   2.157 -      in (make_fixed_const c, (contys,folTyps), funcs) end
   2.158 +fun pred_name_type (Const(c,T)) = (make_fixed_const c, const_types_of (c,T))
   2.159    | pred_name_type (Free(x,T))  = 
   2.160        if isMeta x then raise CLAUSE("Predicate Not First Order 1", Free(x,T)) 
   2.161 -      else (make_fixed_var x, ([],[]), [])
   2.162 +      else (make_fixed_var x, ([],[]))
   2.163    | pred_name_type (v as Var _) = raise CLAUSE("Predicate Not First Order 2", v)
   2.164    | pred_name_type t        = raise CLAUSE("Predicate input unexpected", t);
   2.165  
   2.166 @@ -381,87 +351,51 @@
   2.167      let val (folT,_) = type_of T;
   2.168      in  folT  end;
   2.169  
   2.170 -fun fun_name_type (Const("op =",T)) args =   (*FIXME: Is this special treatment of = needed??*)
   2.171 -      let val t = make_fixed_const "op ="
   2.172 -      in (t, ([eq_arg_type T], []), [(t,2)]) end
   2.173 -  | fun_name_type (Const(c,T)) args = 
   2.174 -      let val t = make_fixed_const c
   2.175 -	  val (contys, (folTyps,funcs)) = const_types_of (c,T)
   2.176 -	  val arity = num_typargs(c,T) + length args
   2.177 -      in
   2.178 -	  (t, (contys,folTyps), ((t,arity)::funcs))
   2.179 -      end
   2.180 - | fun_name_type (Free(x,T)) args  = 
   2.181 -      let val t = make_fixed_var x
   2.182 -      in  (t, ([],[]), [(t, length args)]) end
   2.183 +fun fun_name_type (Const(c,T)) args = (make_fixed_const c, const_types_of (c,T))
   2.184 +  | fun_name_type (Free(x,T)) args  = 
   2.185 +       if isMeta x then raise CLAUSE("Function Not First Order", Free(x,T))
   2.186 +       else (make_fixed_var x, ([],[]))
   2.187    | fun_name_type f args = raise CLAUSE("Function Not First Order 1", f);
   2.188  
   2.189 -
   2.190  fun term_of (Var(ind_nm,T)) = 
   2.191 -      let val (folType,(ts,funcs)) = type_of T
   2.192 -      in
   2.193 -	  (UVar(make_schematic_var ind_nm, folType), (ts, funcs))
   2.194 -      end
   2.195 +      let val (folType,ts) = type_of T
   2.196 +      in (UVar(make_schematic_var ind_nm, folType), ts) end
   2.197    | term_of (Free(x,T)) = 
   2.198 -      let val (folType, (ts,funcs)) = type_of T
   2.199 +      let val (folType, ts) = type_of T
   2.200        in
   2.201 -	  if isMeta x then (UVar(make_schematic_var(x,0),folType),
   2.202 -			    (ts, ((make_schematic_var(x,0)),0)::funcs))
   2.203 -	  else
   2.204 -	      (Fun(make_fixed_var x, [folType], []), 
   2.205 -	       (ts, ((make_fixed_var x),0)::funcs))
   2.206 +	  if isMeta x then (UVar(make_schematic_var(x,0),folType), ts)
   2.207 +	  else (Fun(make_fixed_var x, [folType], []), ts)
   2.208        end
   2.209 -  | term_of (Const(c,T)) =  (* impossible to be equality *)
   2.210 -      let val (contys, (folTyps,funcs)) = const_types_of (c,T)
   2.211 -      in
   2.212 -	  (Fun(make_fixed_const c, contys, []),
   2.213 -	   (folTyps, ((make_fixed_const c),0)::funcs))
   2.214 -      end    
   2.215    | term_of app = 
   2.216        let val (f,args) = strip_comb app
   2.217 -          val _ = case f of Const(_,_) => ()
   2.218 -			  | Free(s,_)  => 
   2.219 -			      if isMeta s 
   2.220 -			      then raise CLAUSE("Function Not First Order 2", f)
   2.221 -			      else ()
   2.222 -			  | _ => raise CLAUSE("Function Not First Order 3", f);
   2.223 -	  val (funName,(contys,ts1),funcs) = fun_name_type f args
   2.224 -	  val (args',(ts2,funcs')) = terms_of args
   2.225 +	  val (funName,(contys,ts1)) = fun_name_type f args
   2.226 +	  val (args',ts2) = terms_of args
   2.227        in
   2.228  	  (Fun(funName,contys,args'), 
   2.229 -	   (union_all (ts1::ts2), 
   2.230 -	    union_all(funcs::funcs')))
   2.231 +	   (union_all (ts1::ts2)))
   2.232        end
   2.233 -and terms_of ts =  
   2.234 -      let val (args, ts_funcs) = ListPair.unzip (map term_of ts)
   2.235 -      in
   2.236 -	  (args, ListPair.unzip ts_funcs)
   2.237 -      end
   2.238 +and terms_of ts = ListPair.unzip (map term_of ts)
   2.239  
   2.240  
   2.241  fun pred_of (Const("op =", typ), args) =
   2.242        let val arg_typ = eq_arg_type typ 
   2.243 -	  val (args',(ts,funcs)) = terms_of args
   2.244 +	  val (args',ts) = terms_of args
   2.245  	  val equal_name = make_fixed_const "op ="
   2.246        in
   2.247  	  (Predicate(equal_name,[arg_typ],args'),
   2.248  	   union_all ts, 
   2.249 -	   [((make_fixed_var equal_name), 2)], 
   2.250 -	   union_all funcs)
   2.251 +	   [((make_fixed_var equal_name), 2)])
   2.252        end
   2.253    | pred_of (pred,args) = 
   2.254 -      let val (predName,(predType,ts1), pfuncs) = pred_name_type pred
   2.255 -	  val (args',(ts2,ffuncs)) = terms_of args
   2.256 +      let val (predName, (predType,ts1)) = pred_name_type pred
   2.257 +	  val (args',ts2) = terms_of args
   2.258  	  val ts3 = union_all (ts1::ts2)
   2.259 -	  val ffuncs' = union_all ffuncs
   2.260 -	  val newfuncs = pfuncs union ffuncs'
   2.261  	  val arity = 
   2.262  	    case pred of
   2.263  		Const (c,T) => num_typargs(c,T) + length args
   2.264  	      | _ => length args
   2.265        in
   2.266 -	  (Predicate(predName,predType,args'), ts3, 
   2.267 -	   [(predName, arity)], newfuncs)
   2.268 +	  (Predicate(predName,predType,args'), ts3, [(predName, arity)])
   2.269        end;
   2.270  
   2.271  
   2.272 @@ -474,20 +408,20 @@
   2.273          (pred_of (strip_comb term), polarity, tag);
   2.274  
   2.275  fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
   2.276 -  | literals_of_term1 (args as (lits, ts, preds, funcs)) (Const("op |",_) $ P $ Q) = 
   2.277 -      let val (lits', ts', preds', funcs') = literals_of_term1 args P
   2.278 +  | literals_of_term1 (args as (lits, ts, preds)) (Const("op |",_) $ P $ Q) = 
   2.279 +      let val (lits', ts', preds') = literals_of_term1 args P
   2.280        in
   2.281 -	  literals_of_term1 (lits', ts', preds' union preds, funcs' union funcs) Q
   2.282 +	  literals_of_term1 (lits', ts', preds' union preds) Q
   2.283        end
   2.284 -  | literals_of_term1 (lits, ts, preds, funcs) P =
   2.285 -      let val ((pred, ts', preds', funcs'), pol, tag) = predicate_of (P,true,false)
   2.286 +  | literals_of_term1 (lits, ts, preds) P =
   2.287 +      let val ((pred, ts', preds'), pol, tag) = predicate_of (P,true,false)
   2.288  	  val lits' = Literal(pol,pred,tag) :: lits
   2.289        in
   2.290 -	  (lits', ts union ts', preds' union preds, funcs' union funcs)
   2.291 +	  (lits', ts union ts', preds' union preds)
   2.292        end;
   2.293  
   2.294  
   2.295 -val literals_of_term = literals_of_term1 ([],[],[],[]);
   2.296 +val literals_of_term = literals_of_term1 ([],[],[]);
   2.297  
   2.298  
   2.299  
   2.300 @@ -649,12 +583,8 @@
   2.301  
   2.302  
   2.303  (*Equality of two clauses up to variable renaming*)
   2.304 -fun clause_eq (cls1,cls2) =
   2.305 -    let val lits1 = get_literals cls1
   2.306 -	val lits2 = get_literals cls2
   2.307 -    in
   2.308 -	length lits1 = length lits2 andalso #1 (lits_eq (lits1,lits2) ([],[]))
   2.309 -    end;
   2.310 +fun clause_eq (Clause{literals=lits1,...}, Clause{literals=lits2,...}) =
   2.311 +  length lits1 = length lits2 andalso #1 (lits_eq (lits1,lits2) ([],[]));
   2.312  
   2.313  
   2.314  (*** Hash function for clauses ***)
   2.315 @@ -671,32 +601,24 @@
   2.316  fun hash1_literal (Literal(true,pred,_)) = hashw_pred (pred, 0w0)
   2.317    | hash1_literal (Literal(false,pred,_)) = Word.notb (hashw_pred (pred, 0w0));
   2.318    
   2.319 -fun hash_clause clause = Word.toIntX (xor_words (map hash1_literal (get_literals clause)));
   2.320 +fun hash_clause (Clause{literals,...}) =
   2.321 +  Word.toIntX (xor_words (map hash1_literal literals));
   2.322  
   2.323  
   2.324 -(* FIX: not sure what to do with these funcs *)
   2.325 -
   2.326 -(*Make literals for sorted type variables*) 
   2.327 +(*Make literals for sorted type variables.  FIXME: can it use map?*) 
   2.328  fun sorts_on_typs (_, [])   = ([]) 
   2.329    | sorts_on_typs (v, "HOL.type" :: s) =
   2.330        sorts_on_typs (v,s)                (*IGNORE sort "type"*)
   2.331 -  | sorts_on_typs ((FOLTVar indx), (s::ss)) =
   2.332 -      LTVar((make_type_class s) ^ 
   2.333 -        "(" ^ (make_schematic_type_var indx) ^ ")") :: 
   2.334 -      (sorts_on_typs ((FOLTVar indx), ss))
   2.335 -  | sorts_on_typs ((FOLTFree x), (s::ss)) =
   2.336 -      LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var x) ^ ")") :: 
   2.337 -      (sorts_on_typs ((FOLTFree x), ss));
   2.338 +  | sorts_on_typs ((FOLTVar indx), s::ss) =
   2.339 +      LTVar(make_type_class s, make_schematic_type_var indx) :: 
   2.340 +      sorts_on_typs ((FOLTVar indx), ss)
   2.341 +  | sorts_on_typs ((FOLTFree x), s::ss) =
   2.342 +      LTFree(make_type_class s, make_fixed_type_var x) :: 
   2.343 +      sorts_on_typs ((FOLTFree x), ss);
   2.344  
   2.345  
   2.346 -(*UGLY: seems to be parsing the "show sorts" output, removing anything that
   2.347 -  starts with a left parenthesis.*)
   2.348 -fun remove_type str = hd (String.fields (fn c => c = #"(") str);
   2.349 -
   2.350 -fun pred_of_sort (LTVar x) = ((remove_type x),1)
   2.351 -|   pred_of_sort (LTFree x) = ((remove_type x),1)
   2.352 -
   2.353 -
   2.354 +fun pred_of_sort (LTVar (s,ty)) = (s,1)
   2.355 +|   pred_of_sort (LTFree (s,ty)) = (s,1)
   2.356  
   2.357  (*Given a list of sorted type variables, return two separate lists.
   2.358    The first is for TVars, the second for TFrees.*)
   2.359 @@ -744,17 +666,13 @@
   2.360        end
   2.361    | get_tvar_strs((FOLTFree x,s)::tss) = distinct (get_tvar_strs tss)
   2.362  
   2.363 -(* FIX add preds and funcs to add typs aux here *)
   2.364 -
   2.365  fun make_axiom_clause_thm thm (ax_name,cls_id) =
   2.366 -    let val (lits,types_sorts, preds, funcs) = literals_of_term (prop_of thm)
   2.367 +    let val (lits,types_sorts, preds) = literals_of_term (prop_of thm)
   2.368  	val lits' = sort_lits lits
   2.369  	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
   2.370 -        val tvars = get_tvar_strs types_sorts
   2.371      in 
   2.372  	make_clause(cls_id,ax_name,Axiom,
   2.373 -	            lits',types_sorts,tvar_lits,tfree_lits,
   2.374 -	            tvars, preds, funcs)
   2.375 +	            lits',types_sorts,tvar_lits,tfree_lits,preds)
   2.376      end;
   2.377  
   2.378  
   2.379 @@ -762,13 +680,11 @@
   2.380  fun make_conjecture_clause n t =
   2.381      let val _ = check_is_fol_term t
   2.382  	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t)
   2.383 -	val (lits,types_sorts, preds, funcs) = literals_of_term t
   2.384 +	val (lits,types_sorts, preds) = literals_of_term t
   2.385  	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
   2.386 -        val tvars = get_tvar_strs types_sorts
   2.387      in
   2.388  	make_clause(n,"conjecture",Conjecture,
   2.389 -	            lits,types_sorts,tvar_lits,tfree_lits,
   2.390 -	            tvars, preds, funcs)
   2.391 +	            lits,types_sorts,tvar_lits,tfree_lits,preds)
   2.392      end;
   2.393      
   2.394  fun make_conjecture_clauses_aux _ [] = []
   2.395 @@ -782,14 +698,12 @@
   2.396  fun make_axiom_clause term (ax_name,cls_id) =
   2.397      let val _ = check_is_fol_term term 
   2.398  	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
   2.399 -	val (lits,types_sorts, preds,funcs) = literals_of_term term
   2.400 +	val (lits,types_sorts, preds) = literals_of_term term
   2.401  	val lits' = sort_lits lits
   2.402  	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds
   2.403 -        val tvars = get_tvar_strs types_sorts	
   2.404      in 
   2.405  	make_clause(cls_id,ax_name,Axiom,
   2.406 -	            lits',types_sorts,tvar_lits,tfree_lits,
   2.407 -	            tvars, preds,funcs)
   2.408 +	            lits',types_sorts,tvar_lits,tfree_lits,preds)
   2.409      end;
   2.410  
   2.411  
   2.412 @@ -799,11 +713,9 @@
   2.413  
   2.414  exception ARCLAUSE of string;
   2.415   
   2.416 -
   2.417  type class = string; 
   2.418  type tcons = string; 
   2.419  
   2.420 -
   2.421  datatype arLit = TConsLit of bool * (class * tcons * string list) | TVarLit of bool * (class * string);
   2.422   
   2.423  datatype arityClause =  
   2.424 @@ -814,8 +726,8 @@
   2.425  			 premLits: arLit list};
   2.426  
   2.427  
   2.428 -fun get_TVars 0 = []
   2.429 -  | get_TVars n = ("T_" ^ (Int.toString n)) :: get_TVars (n-1);
   2.430 +fun gen_TVars 0 = []
   2.431 +  | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
   2.432  
   2.433  fun pack_sort(_,[])  = []
   2.434    | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt)   (*IGNORE sort "type"*)
   2.435 @@ -827,7 +739,7 @@
   2.436  (*Arity of type constructor tcon :: (arg1,...,argN)res*)
   2.437  fun make_axiom_arity_clause (tcons, n, (res,args)) =
   2.438     let val nargs = length args
   2.439 -       val tvars = get_TVars nargs
   2.440 +       val tvars = gen_TVars nargs
   2.441         val tvars_srts = ListPair.zip (tvars,args)
   2.442         val tvars_srts' = union_all(map pack_sort tvars_srts)
   2.443         val false_tvars_srts' = map (pair false) tvars_srts'
   2.444 @@ -891,13 +803,13 @@
   2.445  type classrelClauses = classrelClause list Symtab.table;
   2.446  
   2.447  val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of;
   2.448 -fun classrel_clauses_classrel (C: Sorts.classes) = map classrelClauses_of (Graph.dest C);
   2.449 +
   2.450 +fun classrel_clauses_classrel (C: Sorts.classes) =
   2.451 +  map classrelClauses_of (Graph.dest C);
   2.452 +
   2.453  val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of;
   2.454  
   2.455  
   2.456 -
   2.457 -(****!!!! Changed for typed equality !!!!****)
   2.458 -
   2.459  fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")";
   2.460  
   2.461  (*Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed 
   2.462 @@ -943,13 +855,8 @@
   2.463  	if pol then pred_string else "not(" ^pred_string ^ ")"  
   2.464      end;
   2.465  
   2.466 -
   2.467 -(* FIX: what does this mean? *)
   2.468 -(*fun dfg_of_typeLit (LTVar x) = "not(" ^ x ^ ")"
   2.469 -  | dfg_of_typeLit (LTFree x) = "(" ^ x ^ ")";*)
   2.470 -
   2.471 -fun dfg_of_typeLit (LTVar x) =  x 
   2.472 -  | dfg_of_typeLit (LTFree x) = x ;
   2.473 +fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))"
   2.474 +  | dfg_of_typeLit (LTFree (s,ty)) = "(" ^ s ^ "(" ^ ty ^ "))";
   2.475   
   2.476  (*Make the string of universal quantifiers for a clause*)
   2.477  fun forall_open ([],[]) = ""
   2.478 @@ -985,11 +892,9 @@
   2.479    let val Predicate (predname, _, folterms) = pred
   2.480    in  folterms  end
   2.481  
   2.482 - 
   2.483  fun get_uvars (UVar(a,typ)) = [a] 
   2.484  |   get_uvars (Fun (_,typ,tlist)) = union_all(map get_uvars tlist)
   2.485  
   2.486 -
   2.487  fun is_uvar (UVar _) = true
   2.488  |   is_uvar (Fun _) = false;
   2.489  
   2.490 @@ -1003,94 +908,47 @@
   2.491          union_all(map get_uvars folterms)
   2.492      end
   2.493  
   2.494 -
   2.495 -fun dfg_tvars (Clause cls) =(#tvars cls)
   2.496 -
   2.497 -
   2.498 -	
   2.499 -(* make this return funcs and preds too? *)
   2.500  fun string_of_predname (Predicate("equal",_,terms)) = "EQUALITY"
   2.501    | string_of_predname (Predicate(name,_,terms)) = name
   2.502 -    
   2.503 -	
   2.504 -
   2.505 -fun concat_with sep []  = ""
   2.506 -  | concat_with sep [x] = "(" ^ x ^ ")"
   2.507 -  | concat_with sep (x::xs) = "(" ^ x ^ ")" ^  sep ^ (concat_with sep xs);
   2.508  
   2.509  fun dfg_pred (Literal(pol,pred,tag)) ax_name = 
   2.510      (string_of_predname pred) ^ " " ^ ax_name
   2.511  
   2.512 -fun dfg_clause cls =
   2.513 +fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,types_sorts,...}) =
   2.514      let val (lits,tfree_lits) = dfg_clause_aux cls 
   2.515 -             (*"lits" includes the typing assumptions (TVars)*)
   2.516 +            (*"lits" includes the typing assumptions (TVars)*)
   2.517          val vars = dfg_vars cls
   2.518 -        val tvars = dfg_tvars cls
   2.519 -	val knd = string_of_kind cls
   2.520 +        val tvars = get_tvar_strs types_sorts
   2.521 +        val preds = preds_of_cls cls
   2.522 +	val knd = name_of_kind kind
   2.523  	val lits_str = commas lits
   2.524 -	val cls_id = get_clause_id cls
   2.525 -	val axname = get_axiomName cls
   2.526 -	val cls_str = gen_dfg_cls(cls_id,axname,knd,lits_str,tvars, vars) 			
   2.527 -        fun typ_clss k [] = []
   2.528 -          | typ_clss k (tfree :: tfrees) = 
   2.529 -              (gen_dfg_type_cls(cls_id,axname,knd,tfree,k, tvars,vars)) :: 
   2.530 -              (typ_clss (k+1) tfrees)
   2.531 -    in 
   2.532 -	cls_str :: (typ_clss 0 tfree_lits)
   2.533 -    end;
   2.534 +	val cls_str = gen_dfg_cls(clause_id,axiom_name,knd,lits_str,tvars,vars) 
   2.535 +    in (cls_str, tfree_lits) end;
   2.536  
   2.537 -fun string_of_arity (name, num) =  name ^ "," ^ (Int.toString num) 
   2.538 +fun string_of_arity (name, num) =  "(" ^ name ^ "," ^ Int.toString num ^ ")"
   2.539  
   2.540  fun string_of_preds preds = 
   2.541 -  "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n";
   2.542 +  "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";
   2.543  
   2.544  fun string_of_funcs funcs =
   2.545 -  "functions[" ^ (concat_with ", " (map string_of_arity funcs)) ^ "].\n" ;
   2.546 -
   2.547 +  "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ;
   2.548  
   2.549  fun string_of_symbols predstr funcstr = 
   2.550    "list_of_symbols.\n" ^ predstr  ^ funcstr  ^ "end_of_list.\n\n";
   2.551  
   2.552 -
   2.553  fun string_of_axioms axstr = 
   2.554    "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n";
   2.555  
   2.556 -
   2.557  fun string_of_conjectures conjstr = 
   2.558    "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n";
   2.559  
   2.560 -fun string_of_descrip () = 
   2.561 -  "list_of_descriptions.\nname({*[ File     : ],[ Names    :]*}).\nauthor({*[ Source   :]*}).\nstatus(unknown).\ndescription({*[ Refs     :]*}).\nend_of_list.\n\n"
   2.562 -
   2.563 -
   2.564 -fun string_of_start name = "%------------------------------------------------------------------------------\nbegin_problem(" ^ name ^ ").\n\n";
   2.565 -
   2.566 -
   2.567 -fun string_of_end () = "end_problem.\n%------------------------------------------------------------------------------";
   2.568 -
   2.569 +fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n";
   2.570  
   2.571 -fun clause2dfg cls =
   2.572 -    let val (lits,tfree_lits) = dfg_clause_aux cls 
   2.573 -            (*"lits" includes the typing assumptions (TVars)*)
   2.574 -	val cls_id = get_clause_id cls
   2.575 -	val ax_name = get_axiomName cls
   2.576 -        val vars = dfg_vars cls
   2.577 -        val tvars = dfg_tvars cls
   2.578 -        val funcs = funcs_of_cls cls
   2.579 -        val preds = preds_of_cls cls
   2.580 -	val knd = string_of_kind cls
   2.581 -	val lits_str = commas lits
   2.582 -	val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars,vars) 
   2.583 -    in
   2.584 -	(cls_str,tfree_lits) 
   2.585 -    end;
   2.586 -
   2.587 -
   2.588 +fun string_of_descrip name = "list_of_descriptions.\nname({*" ^ name ^ "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n"
   2.589  
   2.590  fun tfree_dfg_clause tfree_lit =
   2.591    "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ")."
   2.592  
   2.593 -
   2.594  fun gen_dfg_file probname axioms conjectures funcs preds = 
   2.595      let val axstrs_tfrees = (map clause2dfg axioms)
   2.596  	val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
   2.597 @@ -1102,35 +960,47 @@
   2.598          val funcstr = string_of_funcs funcs
   2.599          val predstr = string_of_preds preds
   2.600      in
   2.601 -       (string_of_start probname) ^ (string_of_descrip ()) ^ 
   2.602 -       (string_of_symbols funcstr predstr) ^  
   2.603 -       (string_of_axioms axstr) ^
   2.604 -       (string_of_conjectures conjstr) ^ (string_of_end ())
   2.605 +       string_of_start probname ^ string_of_descrip probname ^
   2.606 +       string_of_symbols funcstr predstr ^  
   2.607 +       string_of_axioms axstr ^
   2.608 +       string_of_conjectures conjstr ^ "end_problem.\n"
   2.609      end;
   2.610     
   2.611 -fun clauses2dfg [] probname axioms conjectures funcs preds = 
   2.612 -      let val funcs' = (union_all(map funcs_of_cls axioms)) @ funcs
   2.613 -	  val preds' = (union_all(map preds_of_cls axioms)) @ preds
   2.614 -      in
   2.615 -	 gen_dfg_file probname axioms conjectures funcs' preds' 
   2.616 -      end
   2.617 - | clauses2dfg (cls::clss) probname axioms conjectures funcs preds = 
   2.618 -     let val (lits,tfree_lits) = dfg_clause_aux cls
   2.619 -	       (*"lits" includes the typing assumptions (TVars)*)
   2.620 -	 val cls_id = get_clause_id cls
   2.621 -	 val ax_name = get_axiomName cls
   2.622 -	 val vars = dfg_vars cls
   2.623 -	 val tvars = dfg_tvars cls
   2.624 -	 val funcs' = (funcs_of_cls cls) union funcs
   2.625 -	 val preds' = (preds_of_cls cls) union preds
   2.626 -	 val knd = string_of_kind cls
   2.627 -	 val lits_str = concat_with ", " lits
   2.628 -	 val axioms' = if knd = "axiom" then (cls::axioms) else axioms
   2.629 -	 val conjectures' = 
   2.630 -	     if knd = "conjecture" then (cls::conjectures) else conjectures
   2.631 -     in
   2.632 -	 clauses2dfg clss probname axioms' conjectures' funcs' preds' 
   2.633 -     end;
   2.634 +fun add_clause_preds (cls,preds) = (preds_of_cls cls) union preds;
   2.635 +val preds_of_clauses = foldl add_clause_preds []
   2.636 +
   2.637 +(*FIXME: can replace expensive list operations (ins) by trees (symtab)*)
   2.638 +
   2.639 +fun add_foltype_funcs (AtomV _, funcs) = funcs
   2.640 +  | add_foltype_funcs (AtomF a, funcs) = (a,0) ins funcs
   2.641 +  | add_foltype_funcs (Comp(a,tys), funcs) = 
   2.642 +      foldl add_foltype_funcs ((a, length tys) ins funcs) tys;
   2.643 +
   2.644 +fun add_folterm_funcs (UVar _, funcs) = funcs
   2.645 +  | add_folterm_funcs (Fun(a,tys,[]), funcs) = (a,0) ins funcs
   2.646 +      (*A constant is a special case: it has no type argument even if overloaded*)
   2.647 +  | add_folterm_funcs (Fun(a,tys,tms), funcs) = 
   2.648 +      foldl add_foltype_funcs 
   2.649 +	    (foldl add_folterm_funcs ((a, length tys + length tms) ins funcs) tms) 
   2.650 +	    tys
   2.651 +
   2.652 +fun add_predicate_funcs (Predicate(_,tys,tms), funcs) = 
   2.653 +    foldl add_foltype_funcs (foldl add_folterm_funcs funcs tms) tys;
   2.654 +
   2.655 +fun add_literal_funcs (Literal(_,pred,_), funcs) = add_predicate_funcs (pred,funcs)
   2.656 +
   2.657 +fun add_clause_funcs (Clause {literals, ...}, funcs) =
   2.658 +  foldl add_literal_funcs funcs literals;
   2.659 +
   2.660 +val funcs_of_clauses = foldl add_clause_funcs []
   2.661 +
   2.662 +
   2.663 +fun clauses2dfg probname axioms conjectures = 
   2.664 +  let val clss = conjectures @ axioms
   2.665 +  in
   2.666 +     gen_dfg_file probname axioms conjectures 
   2.667 +       (funcs_of_clauses clss) (preds_of_clauses clss)
   2.668 +  end
   2.669  
   2.670  
   2.671  fun string_of_arClauseID (ArityClause {clause_id,axiom_name,...}) =
   2.672 @@ -1186,8 +1056,8 @@
   2.673  	tagged_pol ^ pred_string
   2.674      end;
   2.675  
   2.676 -fun tptp_of_typeLit (LTVar x) = "--" ^ x
   2.677 -  | tptp_of_typeLit (LTFree x) = "++" ^ x;
   2.678 +fun tptp_of_typeLit (LTVar (s,ty)) = "--" ^ s ^ "(" ^ ty ^ ")"
   2.679 +  | tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")";
   2.680   
   2.681  
   2.682  fun gen_tptp_cls (cls_id,ax_name,knd,lits) =