DFG output now works for untyped rules (ML "ResClause.untyped();")
authorquigley
Fri Aug 26 19:36:07 2005 +0200 (2005-08-26)
changeset 17150ce2a1aeb42aa
parent 17149 e2b19c92ef51
child 17151 bc97adfeeaa7
DFG output now works for untyped rules (ML "ResClause.untyped();")
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Aug 26 10:01:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Aug 26 19:36:07 2005 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4    val use_simpset: bool ref
     1.5    val use_nameless: bool ref
     1.6    val write_out_clasimp : string -> theory -> term -> 
     1.7 -                             (ResClause.clause * thm) Array.array * int (* * ResClause.clause list *)
     1.8 +                             (ResClause.clause * thm) Array.array * int * ResClause.clause list 
     1.9  
    1.10    end;
    1.11  
    1.12 @@ -245,7 +245,7 @@
    1.13  	val _= TextIO.flushOut out;
    1.14  	val _= TextIO.closeOut out
    1.15    in
    1.16 -	(clause_arr, num_of_clauses)
    1.17 +	(clause_arr, num_of_clauses, clauses)
    1.18    end;
    1.19  
    1.20  
     2.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Aug 26 10:01:06 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Aug 26 19:36:07 2005 +0200
     2.3 @@ -274,7 +274,7 @@
     2.4      (*** hyps/local axioms just now                                                ***)
     2.5      val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])
     2.6      (*** check if the directory exists and, if not, create it***)
     2.7 -    val _ = 
     2.8 +   (* val _ = 
     2.9  	if !SpassComm.spass
    2.10  	then 
    2.11  	    if File.exists dfg_dir then warning("dfg dir exists")
    2.12 @@ -292,7 +292,16 @@
    2.13  			    dfg_path^"/ax_prob"^"_"^(probID)^".dfg" 
    2.14  
    2.15  		    else
    2.16 -			    (File.platform_path wholefile)
    2.17 +			    (File.platform_path wholefile)*)
    2.18 +
    2.19 +    (* if using spass prob_n already contains whole DFG file, otherwise need to mash axioms*)
    2.20 +    (* from clasimpset onto problem file *)
    2.21 +    val newfile =   if !SpassComm.spass 
    2.22 +		    then 
    2.23 +			 probfile
    2.24 +                    else 
    2.25 +			(File.platform_path wholefile)
    2.26 +
    2.27      val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
    2.28  	       (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")
    2.29    in
    2.30 @@ -516,10 +525,10 @@
    2.31                          val _ = File.append (File.tmp_path (Path.basic "child_command")) 
    2.32  			           (childCmd^"\n")
    2.33  			(* now get the number of the subgoal from the filename *)
    2.34 -			val sg_num = if (!SpassComm.spass )
    2.35 +			val sg_num = (*if (!SpassComm.spass )
    2.36  				     then 
    2.37  					int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
    2.38 -				     else
    2.39 +				     else*)
    2.40  					int_of_string(hd (rev(explode childCmd)))
    2.41  
    2.42  			val childIncoming = pollChildInput childInput
     3.1 --- a/src/HOL/Tools/res_atp.ML	Fri Aug 26 10:01:06 2005 +0200
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Aug 26 19:36:07 2005 +0200
     3.3 @@ -16,11 +16,17 @@
     3.4  (*val spass: bool ref*)
     3.5    val vampire: bool ref
     3.6    val custom_spass: string list ref
     3.7 +  val hook_count: int ref
     3.8 +(*  val invoke_atp: Toplevel.transition -> Toplevel.transition*)
     3.9  end;
    3.10  
    3.11  structure ResAtp: RES_ATP =
    3.12  struct
    3.13  
    3.14 +
    3.15 +val call_atp = ref false;
    3.16 +val hook_count = ref 0;
    3.17 +
    3.18  fun debug_tac tac = (debug "testing"; tac);
    3.19  
    3.20  val full_spass = ref false;
    3.21 @@ -56,6 +62,7 @@
    3.22  val hyps_file = File.tmp_path (Path.basic "hyps");
    3.23  val prob_file = File.tmp_path (Path.basic "prob");
    3.24  val dummy_tac = all_tac;
    3.25 +val _ =debug  (File.platform_path prob_file);
    3.26  
    3.27  
    3.28  (**** for Isabelle/ML interface  ****)
    3.29 @@ -135,20 +142,31 @@
    3.30  (* write out a subgoal as DFG clauses to the file "probN"           *)
    3.31  (* where N is the number of this subgoal                             *)
    3.32  (*********************************************************************)
    3.33 -(*
    3.34 -fun dfg_inputs_tfrees thms n tfrees = 
    3.35 -    let val _ = (debug ("in dfg_inputs_tfrees 0"))
    3.36 -        val clss = map (ResClause.make_conjecture_clause_thm) thms
    3.37 +
    3.38 +(*fun dfg_inputs_tfrees thms n tfrees axclauses= 
    3.39 +    let  val clss = map (ResClause.make_conjecture_clause_thm) thms
    3.40           val _ = (debug ("in dfg_inputs_tfrees 1"))
    3.41 -	val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
    3.42 -        val _ = (debug ("in dfg_inputs_tfrees 2"))
    3.43 -	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
    3.44 -         val _ = (debug ("in dfg_inputs_tfrees 3"))
    3.45 +	 val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
    3.46 +	 val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
    3.47 +         val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    3.48 +         val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) axclauses [] [] [] tfrees   
    3.49 +	 val out = TextIO.openOut(probfile)
    3.50 +    in
    3.51 +	(ResLib.writeln_strs out (tfree_clss @ dfg_clss); TextIO.closeOut out; debug probfile)
    3.52 +    end;
    3.53 +*)
    3.54 +fun dfg_inputs_tfrees thms n tfrees axclauses = 
    3.55 +    let val clss = map (ResClause.make_conjecture_clause_thm) thms
    3.56          val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    3.57 +        val _ = warning ("about to write out dfg prob file "^probfile)
    3.58 +       	(*val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
    3.59 +        val tfree_clss = map ResClause.tfree_dfg_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) *)   
    3.60 +        val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) axclauses [] [] [] tfrees   
    3.61  	val out = TextIO.openOut(probfile)
    3.62      in
    3.63 -	(ResLib.writeln_strs out (tfree_clss @ dfg_clss); TextIO.closeOut out; debug probfile
    3.64 -    end;*)
    3.65 +	(ResLib.writeln_strs out [filestr]; TextIO.closeOut out; debug probfile )
    3.66 +    end;
    3.67 +
    3.68  
    3.69  (*********************************************************************)
    3.70  (* call SPASS with settings and problem file for the current subgoal *)
    3.71 @@ -210,18 +228,22 @@
    3.72  (* then call dummy_tac - should be call_res_tac           *)
    3.73  (**********************************************************)
    3.74  
    3.75 -fun get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm n sko_thms =
    3.76 -  if n = 0 then
    3.77 -    (call_resolve_tac (rev sko_thms)
    3.78 -      sign sg_terms (childin, childout, pid) (List.length sg_terms);
    3.79 -     dummy_tac thm)
    3.80 -  else
    3.81 -    SELECT_GOAL
    3.82 -      (EVERY1 [rtac ccontr, atomize_tac, skolemize_tac,
    3.83 -        METAHYPS (fn negs =>
    3.84 -          (tptp_inputs_tfrees (make_clauses negs) n tfrees;
    3.85 -           get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm (n - 1)
    3.86 -             (negs::sko_thms); dummy_tac))]) n thm;
    3.87 +
    3.88 +fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms axclauses =
    3.89 +    if n=0 then 
    3.90 +       (call_resolve_tac  (rev sko_thms)
    3.91 +        sign  sg_terms (childin, childout, pid) (List.length sg_terms);
    3.92 +        dummy_tac thm)
    3.93 +     else
    3.94 +	
    3.95 +     ( SELECT_GOAL
    3.96 +        (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    3.97 +          METAHYPS(fn negs => (if !SpassComm.spass then 
    3.98 +				    dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses
    3.99 + 				 else
   3.100 +			  	    tptp_inputs_tfrees (make_clauses negs)  n tfrees;
   3.101 +			            get_sko_thms  tfrees sign sg_terms (childin, childout, pid) thm  (n -1) (negs::sko_thms) axclauses; dummy_tac))]) n thm )
   3.102 +
   3.103  
   3.104  
   3.105  (**********************************************)
   3.106 @@ -230,7 +252,7 @@
   3.107  (* in proof reconstruction                    *)
   3.108  (**********************************************)
   3.109  
   3.110 -fun isar_atp_goal' thm n tfree_lits (childin, childout, pid) =
   3.111 +fun isar_atp_goal' thm n tfree_lits (childin, childout, pid)  axclauses =
   3.112    let
   3.113      val prems = Thm.prems_of thm
   3.114      (*val sg_term = get_nth k prems*)
   3.115 @@ -243,7 +265,7 @@
   3.116      (* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
   3.117      (* recursive call to pick up the remaining subgoals *)
   3.118      (* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
   3.119 -    get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n []
   3.120 +    get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n []  axclauses
   3.121    end;
   3.122  
   3.123  
   3.124 @@ -255,11 +277,11 @@
   3.125  (* write to file "hyps"                           *)
   3.126  (**************************************************)
   3.127  
   3.128 -fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) =
   3.129 +fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid)  axclauses=
   3.130    let val tfree_lits = isar_atp_h thms
   3.131    in
   3.132      debug ("in isar_atp_aux");
   3.133 -    isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid)
   3.134 +    isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid)  axclauses
   3.135    end;
   3.136  
   3.137  (******************************************************************)
   3.138 @@ -281,10 +303,10 @@
   3.139        val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
   3.140  
   3.141        (*set up variables for writing out the clasimps to a tptp file*)
   3.142 -      val (clause_arr, num_of_clauses) =
   3.143 +      val (clause_arr, num_of_clauses, axclauses) =
   3.144          ResClasimp.write_out_clasimp (File.platform_path clasimp_file) thy
   3.145            (hd prems) (*FIXME: hack!! need to do all prems*)
   3.146 -      val _ = debug ("clasimp_file is " ^ File.platform_path clasimp_file)
   3.147 +      val _ = debug ("clasimp_file is " ^ File.platform_path clasimp_file ^ " with " ^ (string_of_int num_of_clauses)^ " clauses")
   3.148        val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr, num_of_clauses)
   3.149        val pid_string =
   3.150          string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
   3.151 @@ -293,7 +315,7 @@
   3.152        debug ("initial thm: " ^ thm_string);
   3.153        debug ("subgoals: " ^ prems_string);
   3.154        debug ("pid: "^ pid_string);
   3.155 -      isar_atp_aux thms thm (length prems) (childin, childout, pid);
   3.156 +      isar_atp_aux thms thm (length prems) (childin, childout, pid) axclauses;
   3.157        ()
   3.158      end);
   3.159  
   3.160 @@ -340,10 +362,13 @@
   3.161  (** the Isar toplevel hook **)
   3.162  
   3.163  val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   3.164 +
   3.165    let
   3.166 +
   3.167      val proof = Toplevel.proof_of state
   3.168      val (ctxt, (_, goal)) = Proof.get_goal proof
   3.169          handle Proof.STATE _ => error "No goal present";
   3.170 +
   3.171      val thy = ProofContext.theory_of ctxt;
   3.172  
   3.173      (* FIXME presently unused *)
   3.174 @@ -356,6 +381,8 @@
   3.175             Pretty.string_of (ProofContext.pretty_term ctxt
   3.176               (Logic.mk_conjunction_list (Thm.prems_of goal))));
   3.177      debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
   3.178 +    hook_count := !hook_count +1;
   3.179 +    debug ("in hook for time: " ^(string_of_int (!hook_count)) );
   3.180      ResClause.init thy;
   3.181      isar_atp' (ctxt, ProofContext.prems_of ctxt, goal)
   3.182    end);
     4.1 --- a/src/HOL/Tools/res_clause.ML	Fri Aug 26 10:01:06 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Aug 26 19:36:07 2005 +0200
     4.3 @@ -1,4 +1,5 @@
     4.4  (*  Author: Jia Meng, Cambridge University Computer Laboratory
     4.5 +
     4.6      ID: $Id$
     4.7      Copyright 2004 University of Cambridge
     4.8  
     4.9 @@ -6,6 +7,7 @@
    4.10  Typed equality is treated differently.
    4.11  *)
    4.12  
    4.13 +(* works for writeoutclasimp on typed *)
    4.14  signature RES_CLAUSE =
    4.15    sig
    4.16      exception ARCLAUSE of string
    4.17 @@ -20,18 +22,27 @@
    4.18         string * (string * string list list) -> arityClause
    4.19      val make_axiom_classrelClause :
    4.20         string * string option -> classrelClause
    4.21 +
    4.22      val make_axiom_clause : Term.term -> string * int -> clause
    4.23 +
    4.24      val make_conjecture_clause : Term.term -> clause
    4.25      val make_conjecture_clause_thm : Thm.thm -> clause
    4.26      val make_hypothesis_clause : Term.term -> clause
    4.27      val special_equal : bool ref
    4.28 +    val clause_info : clause ->  string * string
    4.29 +    val typed : unit -> unit
    4.30 +    val untyped : unit -> unit
    4.31 +
    4.32 +    val dfg_clauses2str : string list -> string
    4.33 +    val clause2dfg : clause -> string * string list
    4.34 +    val clauses2dfg : clause list -> string -> clause list -> clause list ->
    4.35 +                      (string * int) list -> (string * int) list -> string list -> string
    4.36 +    val tfree_dfg_clause : string -> string
    4.37 +
    4.38      val tptp_arity_clause : arityClause -> string
    4.39      val tptp_classrelClause : classrelClause -> string
    4.40      val tptp_clause : clause -> string list
    4.41 -    val clause_info : clause ->  string * string
    4.42      val tptp_clauses2str : string list -> string
    4.43 -    val typed : unit -> unit
    4.44 -    val untyped : unit -> unit
    4.45      val clause2tptp : clause -> string * string list
    4.46      val tfree_clause : string -> string
    4.47      val schematic_var_prefix : string
    4.48 @@ -45,7 +56,7 @@
    4.49      val class_prefix : string 
    4.50    end;
    4.51  
    4.52 -structure ResClause : RES_CLAUSE =
    4.53 +structure ResClause: RES_CLAUSE =
    4.54  struct
    4.55  
    4.56  (* Added for typed equality *)
    4.57 @@ -56,19 +67,22 @@
    4.58  val schematic_var_prefix = "V_";
    4.59  val fixed_var_prefix = "v_";
    4.60  
    4.61 -val tvar_prefix = "T_";
    4.62 -val tfree_prefix = "t_";
    4.63 +
    4.64 +val tvar_prefix = "Typ_";
    4.65 +val tfree_prefix = "typ_";
    4.66 +
    4.67  
    4.68  val clause_prefix = "cls_"; 
    4.69  
    4.70  val arclause_prefix = "arcls_" 
    4.71  
    4.72 -val const_prefix = "c_";
    4.73 -val tconst_prefix = "tc_"; 
    4.74 +val const_prefix = "const_";
    4.75 +val tconst_prefix = "tconst_"; 
    4.76  
    4.77  val class_prefix = "class_"; 
    4.78  
    4.79  
    4.80 +
    4.81  (**** some useful functions ****)
    4.82   
    4.83  val const_trans_table =
    4.84 @@ -82,10 +96,7 @@
    4.85  		   ("op Un", "union"),
    4.86  		   ("op Int", "inter")];
    4.87  
    4.88 -val type_const_trans_table =
    4.89 -      Symtab.make [("*", "t_prod"),
    4.90 -	  	   ("+", "t_sum"),
    4.91 -		   ("~=>", "t_map")];
    4.92 +
    4.93  
    4.94  (*Escaping of special characters.
    4.95    Alphanumeric characters are left unchanged.
    4.96 @@ -99,6 +110,7 @@
    4.97  fun ascii_of_c c =
    4.98    if Char.isAlphaNum c then String.str c
    4.99    else if c = #"_" then "__"
   4.100 +  else if c = #"'" then ""
   4.101    else if #" " <= c andalso c <= #"/" 
   4.102         then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
   4.103    else if Char.isPrint c then ("_" ^ Int.toString (Char.ord c))
   4.104 @@ -110,6 +122,7 @@
   4.105  
   4.106  end;
   4.107  
   4.108 +
   4.109  (*Remove the initial ' character from a type variable, if it is present*)
   4.110  fun trim_type_var s =
   4.111    if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
   4.112 @@ -118,25 +131,27 @@
   4.113  fun ascii_of_indexname (v,0) = ascii_of v
   4.114    | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i;
   4.115  
   4.116 -fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
   4.117 +(* another version of above functions that remove chars that may not be allowed by Vampire *)
   4.118 +fun make_schematic_var v = schematic_var_prefix ^ (ascii_of v);
   4.119  fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
   4.120  
   4.121 +
   4.122  (*Type variables contain _H because the character ' translates to that.*)
   4.123  fun make_schematic_type_var (x,i) = 
   4.124        tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
   4.125  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
   4.126  
   4.127 -fun make_fixed_const c =
   4.128 +fun make_fixed_const c = const_prefix ^ (ascii_of c);
   4.129 +fun make_fixed_type_const c = tconst_prefix ^ (ascii_of c);
   4.130 +
   4.131 +fun make_type_class clas = class_prefix ^ (ascii_of clas);
   4.132 +
   4.133 +
   4.134 +
   4.135 +fun lookup_const c =
   4.136      case Symtab.lookup (const_trans_table,c) of
   4.137          SOME c' => c'
   4.138 -      | NONE =>  const_prefix ^ (ascii_of c);
   4.139 -
   4.140 -fun make_fixed_type_const c = 
   4.141 -    case Symtab.lookup (type_const_trans_table,c) of
   4.142 -        SOME c' => c'
   4.143 -      | NONE =>  tconst_prefix ^ (ascii_of c);
   4.144 -
   4.145 -fun make_type_class clas = class_prefix ^ (ascii_of clas);
   4.146 +      | NONE =>  make_fixed_const c;
   4.147  
   4.148  
   4.149  
   4.150 @@ -165,11 +180,16 @@
   4.151  type tag = bool; 
   4.152  
   4.153  
   4.154 +
   4.155 +fun string_of_indexname (name,index) = name ^ "_" ^ (string_of_int index);
   4.156 +
   4.157 +
   4.158  val id_ref = ref 0;
   4.159 -
   4.160  fun generate_id () = 
   4.161 -    let val id = !id_ref
   4.162 -    in id_ref := id + 1; id end;
   4.163 +     let val id = !id_ref
   4.164 +     in
   4.165 +	 (id_ref:=id + 1; id)
   4.166 +     end;
   4.167  
   4.168  
   4.169  
   4.170 @@ -204,7 +224,11 @@
   4.171  		    literals: literal list,
   4.172  		    types_sorts: (typ_var * sort) list, 
   4.173                      tvar_type_literals: type_literal list, 
   4.174 -                    tfree_type_literals: type_literal list };
   4.175 +                    tfree_type_literals: type_literal list ,
   4.176 +                    tvars: string list,
   4.177 +                    predicates: (string*int) list,
   4.178 +                    functions: (string*int) list};
   4.179 +
   4.180  
   4.181  
   4.182  exception CLAUSE of string;
   4.183 @@ -214,14 +238,15 @@
   4.184  (*** make clauses ***)
   4.185  
   4.186  
   4.187 -fun make_clause (clause_id,axiom_name,kind,literals,
   4.188 -                 types_sorts,tvar_type_literals,
   4.189 -                 tfree_type_literals) =
   4.190 -     Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, 
   4.191 -             literals = literals, types_sorts = types_sorts,
   4.192 -             tvar_type_literals = tvar_type_literals,
   4.193 -             tfree_type_literals = tfree_type_literals};
   4.194 +fun make_clause (clause_id,axiom_name,kind,literals,types_sorts,tvar_type_literals,tfree_type_literals,tvars, predicates, functions) =
   4.195 +     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};
   4.196 +
   4.197 +
   4.198  
   4.199 +fun type_of (Type (a, [])) = let val t = make_fixed_type_const a
   4.200 +                                    in
   4.201 +					(t,([],[(t,0)]))
   4.202 +  				    end
   4.203  
   4.204  (*Definitions of the current theory--to allow suppressing types.*)
   4.205  val curr_defs = ref Defs.empty;
   4.206 @@ -229,32 +254,77 @@
   4.207  (*Initialize the type suppression mechanism with the current theory before
   4.208      producing any clauses!*)
   4.209  fun init thy = (curr_defs := Theory.defs_of thy);
   4.210 +(*<<<<<<< res_clause.ML
   4.211 +*)
   4.212 +
   4.213 +(*Types aren't needed if the constant has at most one definition and is monomorphic*)
   4.214 +(*fun no_types_needed s =
   4.215 +  (case Defs.fast_overloading_info (!curr_defs) s of
   4.216 +      NONE => true
   4.217 +    | SOME (T,len,_) => len <= 1 andalso null (typ_tvars T))
   4.218 +=======*)
   4.219  fun no_types_needed s = Defs.monomorphic (!curr_defs) s;
   4.220 +(*>>>>>>> 1.18*)
   4.221      
   4.222 +
   4.223  (*Flatten a type to a string while accumulating sort constraints on the TFress and
   4.224    TVars it contains.*)    
   4.225 -fun type_of (Type (a, [])) = (make_fixed_type_const a,[]) 
   4.226 +fun type_of (Type (a, [])) = let val t = make_fixed_type_const a
   4.227 +                                    in
   4.228 +					(t,([],[(t,0)]))
   4.229 +  				    end
   4.230    | type_of (Type (a, Ts)) = 
   4.231 -      let val foltyps_ts = map type_of Ts
   4.232 -	  val (folTyps,ts) = ListPair.unzip foltyps_ts
   4.233 -	  val ts' = ResLib.flat_noDup ts
   4.234 -      in    
   4.235 -	  (((make_fixed_type_const a) ^ (ResLib.list_to_string folTyps)), ts') 
   4.236 -      end
   4.237 -  | type_of (TFree (a, s)) = (make_fixed_type_var a, [((FOLTFree a),s)])
   4.238 -  | type_of (TVar (v, s))  = (make_schematic_type_var v, [((FOLTVar v),s)]);
   4.239 +    let val foltyps_ts = map type_of Ts 
   4.240 +        val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts
   4.241 +        val (ts, funcslist) = ListPair.unzip ts_funcs
   4.242 +        val ts' = ResLib.flat_noDup ts
   4.243 +        val funcs' = (ResLib.flat_noDup funcslist)
   4.244 +        val t = (make_fixed_type_const a)
   4.245 +    in    
   4.246 +        ((t ^ (ResLib.list_to_string folTyps)),(ts', ((t,(length Ts))::funcs')) )
   4.247 +    end
   4.248 +  | type_of (TFree (a, s))  = let val t = make_fixed_type_const a
   4.249 +                              in
   4.250 +				(t, ([((FOLTFree a),s)],[(t,0)]) )
   4.251 +			      end
   4.252 +
   4.253 +  | type_of (TVar (v, s))   = let val t =make_schematic_type_var ( v)
   4.254 +                              in
   4.255 +				(t, ([((FOLTVar v),s)], [(*(t,0)*)]))
   4.256 +                              end
   4.257 +
   4.258 +(* added: checkMeta: string -> bool *)
   4.259 +(* Any meta vars like ?x should be treated as universal vars,although it is represented as "Free(...)" by Isabelle *)
   4.260 +fun checkMeta s =
   4.261 +    let val chars = explode s
   4.262 +    in
   4.263 +	["M", "E", "T", "A", "H", "Y", "P", "1"] prefix chars
   4.264 +    end;
   4.265  
   4.266  fun maybe_type_of c T =
   4.267 - if no_types_needed c then ("",[]) else type_of T;
   4.268 + if no_types_needed c then ("",([],[])) else type_of T;
   4.269  
   4.270  (* Any variables created via the METAHYPS tactical should be treated as
   4.271     universal vars, although it is represented as "Free(...)" by Isabelle *)
   4.272  val isMeta = String.isPrefix "METAHYP1_"
   4.273 -    
   4.274 -fun pred_name_type (Const(c,T)) = (make_fixed_const c, maybe_type_of c T)
   4.275 +
   4.276 +fun pred_name_type (Const(c,T)) = (let val t = make_fixed_const c
   4.277 +                                      val (typof,(folTyps,funcs)) = type_of T
   4.278 +                                     
   4.279 +                                  in
   4.280 +					(t, (typof,folTyps), (funcs))
   4.281 +      				  end) 
   4.282    | pred_name_type (Free(x,T))  = 
   4.283 -      if isMeta x then raise CLAUSE("Predicate Not First Order") 
   4.284 -      else (make_fixed_var x, type_of T)
   4.285 +    let val is_meta = checkMeta x
   4.286 +    in
   4.287 +	if is_meta then (raise CLAUSE("Predicate Not First Order")) else
   4.288 +	(let val t = (make_fixed_var x)
   4.289 +                                      val (typof,(folTyps, funcs)) = type_of T
   4.290 +                                  in
   4.291 +					(t, (typof,folTyps),funcs)
   4.292 +      				  end)
   4.293 +
   4.294 +    end
   4.295    | pred_name_type (Var(_,_))   = raise CLAUSE("Predicate Not First Order")
   4.296    | pred_name_type _          = raise CLAUSE("Predicate input unexpected");
   4.297  
   4.298 @@ -267,74 +337,108 @@
   4.299      in
   4.300  	folT
   4.301      end;
   4.302 +  
   4.303  
   4.304 -fun fun_name_type (Const(c,T)) = (make_fixed_const c, maybe_type_of c T)
   4.305 -  | fun_name_type (Free(x,T)) = (make_fixed_var x,type_of T)
   4.306 -  | fun_name_type _ = raise CLAUSE("Function Not First Order");
   4.307 -    
   4.308  
   4.309 -(* FIX - add in funcs and stuff to this *)
   4.310 +(* FIX: retest with lcp's changes *)
   4.311 +fun fun_name_type (Const(c,T)) args = (let val t = make_fixed_const c
   4.312 +                                      val (typof,(folTyps,funcs)) = maybe_type_of c T
   4.313 +                                      val arity = if (!keep_types) then
   4.314 +                                       (length args)(*+ 1*) (*(length folTyps) *)
   4.315 +					  else
   4.316 +					  (length args)(* -1*)
   4.317 +                                  in
   4.318 +					(t, (typof,folTyps), ((t,arity)::funcs))
   4.319 +      				  end)
   4.320 +                                     
   4.321 +  | fun_name_type (Free(x,T)) args  = (let val t = (make_fixed_var x)
   4.322 +                                      val (typof,(folTyps,funcs)) = type_of T
   4.323 +                                      val arity = if (!keep_types) then
   4.324 +                                       (length args) (*+ 1*) (*(length folTyps)*)
   4.325 +					  else
   4.326 +					  (length args) (*-1*)(*(length args) + 1*)(*(length folTyps)*)
   4.327 +                                  in
   4.328 +					(t, (typof,folTyps), ((t,0)::funcs))
   4.329 +      				  end)
   4.330 +
   4.331 +  | fun_name_type _  args = raise CLAUSE("Function Not First Order");
   4.332 +
   4.333  
   4.334  fun term_of (Var(ind_nm,T)) = 
   4.335 -      let val (folType,ts) = type_of T
   4.336 -      in
   4.337 -	  (UVar(make_schematic_var ind_nm, folType), ts)
   4.338 -      end
   4.339 +    let val (folType,(ts,funcs)) = type_of T
   4.340 +    in
   4.341 +	(UVar(make_schematic_var(string_of_indexname ind_nm),folType),(ts, (funcs)))
   4.342 +    end
   4.343    | term_of (Free(x,T)) = 
   4.344 -      let val (folType,ts) = type_of T
   4.345 -      in
   4.346 -	  if isMeta x then (UVar(make_schematic_var(x,0), folType), ts)
   4.347 -	  else (Fun(make_fixed_var x,folType,[]), ts)
   4.348 -      end
   4.349 -  | term_of (Const(c,T)) =  (* impossible to be equality *)
   4.350 -      let val (folType,ts) = type_of T
   4.351 -      in
   4.352 -	  (Fun(make_fixed_const c,folType,[]), ts)
   4.353 -      end    
   4.354 -  | term_of (app as (t $ a)) = 
   4.355 -      let val (f,args) = strip_comb app
   4.356 -	  fun term_of_aux () = 
   4.357 -	      let val (funName,(funType,ts1)) = fun_name_type f
   4.358 -		   val (args',ts2) = ListPair.unzip (map term_of args)
   4.359 -		   val ts3 = ResLib.flat_noDup (ts1::ts2)
   4.360 -	      in
   4.361 -		  (Fun(funName,funType,args'),ts3)
   4.362 -	      end
   4.363 -	  fun term_of_eq ((Const ("op =", typ)),args) =
   4.364 -	      let val arg_typ = eq_arg_type typ
   4.365 -		  val (args',ts) = ListPair.unzip (map term_of args)
   4.366 -		  val equal_name = make_fixed_const ("op =")
   4.367 -	      in
   4.368 -		  (Fun(equal_name,arg_typ,args'),ResLib.flat_noDup ts)
   4.369 -	      end
   4.370 -      in
   4.371 -	  case f of Const ("op =", typ) => term_of_eq (f,args)
   4.372 -		  | Const(_,_) => term_of_aux ()
   4.373 -		  | Free(s,_)  => if isMeta s 
   4.374 -		                  then raise CLAUSE("Function Not First Order") 
   4.375 -		                  else term_of_aux()
   4.376 -		  | _          => raise CLAUSE("Function Not First Order")
   4.377 -      end
   4.378 +    let val is_meta = checkMeta x
   4.379 +	val (folType,(ts, funcs)) = type_of T
   4.380 +    in
   4.381 +	if is_meta then (UVar(make_schematic_var x,folType),(ts, (((make_schematic_var x),0)::funcs)))
   4.382 +	else
   4.383 +            (Fun(make_fixed_var x,folType,[]),(ts, (((make_fixed_var x),0)::funcs)))
   4.384 +    end
   4.385 +  |  term_of (Const(c,T)) =  (* impossible to be equality *)
   4.386 +    let val (folType,(ts,funcs)) = type_of T
   4.387 +     in
   4.388 +        (Fun(lookup_const c,folType,[]),(ts, (((lookup_const c),0)::funcs)))
   4.389 +    end    
   4.390 +  |  term_of (app as (t $ a)) = 
   4.391 +    let val (f,args) = strip_comb app
   4.392 +        fun term_of_aux () = 
   4.393 +            let val (funName,(funType,ts1),funcs) = fun_name_type f args
   4.394 +	        val (args',ts_funcs) = ListPair.unzip (map term_of args)
   4.395 +      	        val (ts2,funcs') = ListPair.unzip ( ts_funcs)
   4.396 +                val ts3 = ResLib.flat_noDup (ts1::ts2)
   4.397 +                val funcs'' = ResLib.flat_noDup((funcs::funcs'))
   4.398 +            in
   4.399 +		(Fun(funName,funType,args'),(ts3,funcs''))
   4.400 +            end
   4.401 +	fun term_of_eq ((Const ("op =", typ)),args) =
   4.402 +	    let val arg_typ = eq_arg_type typ
   4.403 +		val (args',ts_funcs) = ListPair.unzip (map term_of args)
   4.404 +      	        val (ts,funcs) = ListPair.unzip ( ts_funcs)
   4.405 +		val equal_name = lookup_const ("op =")
   4.406 +	    in
   4.407 +		(Fun(equal_name,arg_typ,args'),(ResLib.flat_noDup ts, (((make_fixed_var equal_name),2):: ResLib.flat_noDup (funcs))))
   4.408 +	    end
   4.409 +    in
   4.410 +        case f of Const ("op =", typ) => term_of_eq (f,args)
   4.411 +	        | Const(_,_) => term_of_aux ()
   4.412 +                | Free(s,_)  => if (checkMeta s) then (raise CLAUSE("Function Not First Order")) else term_of_aux ()
   4.413 +                | _          => raise CLAUSE("Function Not First Order")
   4.414 +    end
   4.415    | term_of _ = raise CLAUSE("Function Not First Order"); 
   4.416  
   4.417  
   4.418 +
   4.419 +
   4.420  fun pred_of_eq ((Const ("op =", typ)),args) =
   4.421      let val arg_typ = eq_arg_type typ 
   4.422 -	val (args',ts) = ListPair.unzip (map term_of args)
   4.423 -	val equal_name = make_fixed_const "op ="
   4.424 +	val (args',ts_funcs) = ListPair.unzip (map term_of args)
   4.425 +        val (ts,funcs) = ListPair.unzip ( ts_funcs)
   4.426 +	val equal_name = lookup_const "op ="
   4.427      in
   4.428 -	(Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts)
   4.429 +	(Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts,([((make_fixed_var equal_name),2)]:(string*int)list), (ResLib.flat_noDup (funcs)))
   4.430      end;
   4.431  
   4.432 -
   4.433 +(* CHECK arity for predicate is set to (2*args) to account for type info.  Is this right? *)
   4.434  (* changed for non-equality predicate *)
   4.435  (* The input "pred" cannot be an equality *)
   4.436  fun pred_of_nonEq (pred,args) = 
   4.437 -    let val (predName,(predType,ts1)) = pred_name_type pred
   4.438 -	val (args',ts2) = ListPair.unzip (map term_of args)
   4.439 +    let val (predName,(predType,ts1), pfuncs) = pred_name_type pred
   4.440 +	val (args',ts_funcs) = ListPair.unzip (map term_of args)
   4.441 +        val (ts2,ffuncs) = ListPair.unzip ( ts_funcs)
   4.442  	val ts3 = ResLib.flat_noDup (ts1::ts2)
   4.443 +        val ffuncs' = (ResLib.flat_noDup (ffuncs))
   4.444 +        val newfuncs = distinct (pfuncs@ffuncs')
   4.445 +        val pred_arity = (*if ((length ts3) <> 0) 
   4.446 +			 then 
   4.447 +			    ((length args) +(length ts3))
   4.448 +			 else*)
   4.449 +                           (* just doing length args if untyped seems to work*)
   4.450 +			    (if !keep_types then (length args)+1 else (length args))
   4.451      in
   4.452 -	(Predicate(predName,predType,args'),ts3)
   4.453 +	(Predicate(predName,predType,args'),ts3, [(predName, pred_arity)], newfuncs)
   4.454      end;
   4.455  
   4.456  
   4.457 @@ -348,44 +452,86 @@
   4.458      end;
   4.459  
   4.460   
   4.461 -fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts) = literals_of_term (P,lits_ts)
   4.462 -  | literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts)) = 
   4.463 -      let val (lits',ts') = literals_of_term (P,(lits,ts))
   4.464 -      in
   4.465 -	  literals_of_term (Q, (lits',ts'))
   4.466 -      end
   4.467 -  | literals_of_term ((Const("Not",_) $ P),(lits,ts)) = 
   4.468 -      let val (pred,ts') = predicate_of P
   4.469 -	  val lits' = Literal(false,pred,false) :: lits
   4.470 -	  val ts'' = ResLib.no_rep_app ts ts'
   4.471 -      in
   4.472 -	  (lits',ts'')
   4.473 -      end
   4.474 -  | literals_of_term (P,(lits,ts)) = 
   4.475 -      let val (pred,ts') = predicate_of P
   4.476 -	  val lits' = Literal(true,pred,false) :: lits
   4.477 -	  val ts'' = ResLib.no_rep_app ts ts' 
   4.478 -      in
   4.479 -	  (lits',ts'')
   4.480 -      end;
   4.481 -     
   4.482 -fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]));
   4.483 -    
   4.484 +
   4.485 +fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) = literals_of_term(P,lits_ts, preds, funcs)
   4.486 +  | literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts), preds,funcs) = 
   4.487 +    let val (lits',ts', preds', funcs') = literals_of_term(P,(lits,ts), preds,funcs)
   4.488 +    in
   4.489 +        literals_of_term(Q,(lits',ts'), distinct(preds'@preds), distinct(funcs'@funcs))
   4.490 +    end
   4.491 +  | literals_of_term ((Const("Not",_) $ P),(lits,ts), preds, funcs) = 
   4.492 +    let val (pred,ts', preds', funcs') = predicate_of P
   4.493 +        val lits' = Literal(false,pred,false) :: lits
   4.494 +        val ts'' = ResLib.no_rep_app ts ts'
   4.495 +    in
   4.496 +        (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
   4.497 +    end
   4.498 +  | literals_of_term (P,(lits,ts), preds, funcs) = 
   4.499 +    let val (pred,ts', preds', funcs') = predicate_of P
   4.500 +        val lits' = Literal(true,pred,false) :: lits
   4.501 +        val ts'' = ResLib.no_rep_app ts ts' 
   4.502 +    in
   4.503 +        (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
   4.504 +    end;
   4.505 +
   4.506 +
   4.507 +fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]), [], []);
   4.508 +
   4.509 +
   4.510 +(* FIX: not sure what to do with these funcs *)
   4.511 +
   4.512  (*Make literals for sorted type variables*) 
   4.513 -fun sorts_on_typs (_, []) = []
   4.514 +fun sorts_on_typs (_, [])   = ([]) 
   4.515    | sorts_on_typs (v, "HOL.type" :: s) =
   4.516        sorts_on_typs (v,s)   (*Ignore sort "type"*)
   4.517    | sorts_on_typs ((FOLTVar(indx)), (s::ss)) =
   4.518 -      LTVar((make_type_class s) ^ 
   4.519 -        "(" ^ (make_schematic_type_var indx) ^ ")") :: 
   4.520 -      (sorts_on_typs ((FOLTVar(indx)), ss))
   4.521 +      (LTVar((make_type_class s) ^ 
   4.522 +        "(" ^ (make_schematic_type_var( indx)) ^ ")") :: 
   4.523 +      (sorts_on_typs ((FOLTVar(indx)), ss)))
   4.524    | sorts_on_typs ((FOLTFree(x)), (s::ss)) =
   4.525        LTFree((make_type_class s) ^ "(" ^ (make_fixed_type_var(x)) ^ ")") :: 
   4.526        (sorts_on_typs ((FOLTFree(x)), ss));
   4.527  
   4.528 +
   4.529 +fun takeUntil ch [] res  = (res, [])
   4.530 + |   takeUntil ch (x::xs) res = if   x = ch 
   4.531 +                                then
   4.532 +                                     (res, xs)
   4.533 +                                else
   4.534 +                                     takeUntil ch xs (res@[x])
   4.535 +
   4.536 +fun remove_type str = let val exp = explode str
   4.537 +		 	  val (first,rest) =  (takeUntil "(" exp [])
   4.538 +                      in
   4.539 +                        implode first
   4.540 +		      end
   4.541 +
   4.542 +fun pred_of_sort (LTVar x) = ((remove_type x),1)
   4.543 +|   pred_of_sort (LTFree x) = ((remove_type x),1)
   4.544 +
   4.545 +
   4.546 +
   4.547 +
   4.548  (*Given a list of sorted type variables, return two separate lists.
   4.549    The first is for TVars, the second for TFrees.*)
   4.550 -fun add_typs_aux [] = ([],[])
   4.551 +fun add_typs_aux [] preds  = ([],[], preds)
   4.552 +  | add_typs_aux ((FOLTVar(indx),s)::tss) preds = 
   4.553 +      let val (vs) = sorts_on_typs (FOLTVar(indx), s)
   4.554 +          val preds' = (map pred_of_sort vs)@preds
   4.555 +	  val (vss,fss, preds'') = add_typs_aux tss preds'
   4.556 +      in
   4.557 +	  (ResLib.no_rep_app vs vss, fss, preds'')
   4.558 +      end
   4.559 +  | add_typs_aux ((FOLTFree(x),s)::tss) preds  =
   4.560 +      let val (fs) = sorts_on_typs (FOLTFree(x), s)
   4.561 +          val preds' = (map pred_of_sort fs)@preds
   4.562 +	  val (vss,fss, preds'') = add_typs_aux tss preds'
   4.563 +      in
   4.564 +	  (vss, ResLib.no_rep_app fs fss,preds'')
   4.565 +      end;
   4.566 +
   4.567 +
   4.568 +(*fun add_typs_aux [] = ([],[])
   4.569    | add_typs_aux ((FOLTVar(indx),s)::tss) = 
   4.570        let val vs = sorts_on_typs (FOLTVar(indx), s)
   4.571  	  val (vss,fss) = add_typs_aux tss
   4.572 @@ -397,46 +543,93 @@
   4.573  	  val (vss,fss) = add_typs_aux tss
   4.574        in
   4.575  	  (vss, ResLib.no_rep_app fs fss)
   4.576 -      end;
   4.577 +      end;*)
   4.578  
   4.579 -fun add_typs (Clause cls) = add_typs_aux (#types_sorts cls)
   4.580 +
   4.581 +fun add_typs (Clause cls) preds  = add_typs_aux (#types_sorts cls) preds 
   4.582  
   4.583  
   4.584  (** make axiom clauses, hypothesis clauses and conjecture clauses. **)
   4.585 -   
   4.586 +
   4.587 +local 
   4.588 +    fun replace_dot "." = "_"
   4.589 +      | replace_dot "'" = ""
   4.590 +      | replace_dot c = c;
   4.591 +
   4.592 +in
   4.593 +
   4.594 +fun proper_ax_name ax_name = 
   4.595 +    let val chars = explode ax_name
   4.596 +    in
   4.597 +	implode (map replace_dot chars)
   4.598 +    end;
   4.599 +end;
   4.600  
   4.601 -fun make_conjecture_clause_thm thm =
   4.602 -    let val (lits,types_sorts) = literals_of_thm thm
   4.603 -	val cls_id = generate_id()
   4.604 -	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   4.605 -    in
   4.606 -	make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits)
   4.607 +fun get_tvar_strs [] = []
   4.608 +  | get_tvar_strs ((FOLTVar(indx),s)::tss) = 
   4.609 +      let val vstr =(make_schematic_type_var( indx));
   4.610 +          val (vstrs) = get_tvar_strs tss
   4.611 +      in
   4.612 +	  (distinct( vstr:: vstrs))
   4.613 +      end
   4.614 +  | get_tvar_strs((FOLTFree(x),s)::tss) =
   4.615 +      let val (vstrs) = get_tvar_strs tss
   4.616 +      in
   4.617 +	  (distinct( vstrs))
   4.618 +      end;
   4.619 +
   4.620 +(* FIX add preds and funcs to add typs aux here *)
   4.621 +
   4.622 +fun make_axiom_clause_thm thm (name,number)=
   4.623 +    let val (lits,types_sorts, preds, funcs) = literals_of_thm thm
   4.624 +	val cls_id = number
   4.625 +	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
   4.626 +        val tvars = get_tvar_strs types_sorts
   4.627 +	val ax_name = proper_ax_name name
   4.628 +    in 
   4.629 +	make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs)
   4.630      end;
   4.631  
   4.632  
   4.633 -fun make_axiom_clause term (axname,cls_id) =
   4.634 -    let val (lits,types_sorts) = literals_of_term (term,([],[]))
   4.635 -	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   4.636 +
   4.637 +fun make_conjecture_clause_thm thm =
   4.638 +    let val (lits,types_sorts, preds, funcs) = literals_of_thm thm
   4.639 +	val cls_id = generate_id()
   4.640 +	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
   4.641 +        val tvars = get_tvar_strs types_sorts
   4.642 +    in
   4.643 +	make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs)
   4.644 +    end;
   4.645 +
   4.646 +
   4.647 +fun make_axiom_clause term (name,number)=
   4.648 +    let val (lits,types_sorts, preds,funcs) = literals_of_term (term,([],[]), [],[])
   4.649 +	val cls_id = number
   4.650 +	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts  preds 
   4.651 +        val tvars = get_tvar_strs types_sorts	
   4.652 +	val ax_name = proper_ax_name name
   4.653      in 
   4.654 -	make_clause(cls_id,axname,Axiom,lits,types_sorts,tvar_lits,tfree_lits)
   4.655 +	make_clause(cls_id,ax_name,Axiom,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs)
   4.656      end;
   4.657  
   4.658  
   4.659  fun make_hypothesis_clause term =
   4.660 -    let val (lits,types_sorts) = literals_of_term (term,([],[]))
   4.661 +    let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[])
   4.662  	val cls_id = generate_id()
   4.663 -	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   4.664 +	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts  preds 
   4.665 +        val tvars = get_tvar_strs types_sorts
   4.666      in
   4.667 -	make_clause(cls_id,"",Hypothesis,lits,types_sorts,tvar_lits,tfree_lits)
   4.668 +	make_clause(cls_id,"",Hypothesis,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs)
   4.669      end;
   4.670      
   4.671   
   4.672  fun make_conjecture_clause term =
   4.673 -    let val (lits,types_sorts) = literals_of_term (term,([],[]))
   4.674 +    let val (lits,types_sorts, preds, funcs) = literals_of_term (term,([],[]),[],[])
   4.675  	val cls_id = generate_id()
   4.676 -	val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
   4.677 +	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts  preds 
   4.678 +        val tvars = get_tvar_strs types_sorts	
   4.679      in
   4.680 -	make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits)
   4.681 +	make_clause(cls_id,"",Conjecture,lits,types_sorts,tvar_lits,tfree_lits,tvars, preds, funcs)
   4.682      end;
   4.683   
   4.684  
   4.685 @@ -525,11 +718,11 @@
   4.686  
   4.687  
   4.688  
   4.689 -(***** convert clauses to tptp format *****)
   4.690 +(***** convert clauses to DFG format *****)
   4.691  
   4.692  
   4.693 -fun string_of_clauseID (Clause cls) = 
   4.694 -    clause_prefix ^ string_of_int (#clause_id cls);
   4.695 +fun string_of_clauseID (Clause cls) = clause_prefix ^ (string_of_int (#clause_id cls));
   4.696 +
   4.697  
   4.698  fun string_of_kind (Clause cls) = name_of_kind (#kind cls);
   4.699  
   4.700 @@ -550,6 +743,7 @@
   4.701  	    "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")"
   4.702      end
   4.703  
   4.704 +
   4.705  and
   4.706      string_of_term (UVar(x,_)) = x
   4.707    | string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms)
   4.708 @@ -565,8 +759,128 @@
   4.709  
   4.710  (* Changed for typed equality *)
   4.711  (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
   4.712 -fun string_of_predicate (Predicate("equal",typ,terms)) = 
   4.713 -       string_of_equality(typ,terms)
   4.714 +fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms)
   4.715 +  | string_of_predicate (Predicate(name,_,[])) = name 
   4.716 +  | string_of_predicate (Predicate(name,typ,terms)) = 
   4.717 +    let val terms_as_strings = map string_of_term terms
   4.718 +    in
   4.719 +        if (!keep_types) then name ^ (ResLib.list_to_string  (typ :: terms_as_strings))
   4.720 +        else name ^ (ResLib.list_to_string terms_as_strings) 
   4.721 +    end;
   4.722 +
   4.723 +    
   4.724 +
   4.725 +(********************************)
   4.726 +(* Code for producing DFG files *)
   4.727 +(********************************)
   4.728 +
   4.729 +fun dfg_literal (Literal(pol,pred,tag)) =
   4.730 +    let val pred_string = string_of_predicate pred
   4.731 +	val tagged_pol =if pol then pred_string else "not(" ^pred_string ^ ")"
   4.732 +     in
   4.733 +	tagged_pol  
   4.734 +    end;
   4.735 +
   4.736 +
   4.737 +(* FIX: what does this mean? *)
   4.738 +(*fun dfg_of_typeLit (LTVar x) = "not(" ^ x ^ ")"
   4.739 +  | dfg_of_typeLit (LTFree x) = "(" ^ x ^ ")";*)
   4.740 +
   4.741 +fun dfg_of_typeLit (LTVar x) =  x 
   4.742 +  | dfg_of_typeLit (LTFree x) = x ;
   4.743 + 
   4.744 +
   4.745 +fun strlist [] = ""
   4.746 +|   strlist (x::[]) = x 
   4.747 +|   strlist (x::xs) = x ^ "," ^ (strlist xs)
   4.748 +
   4.749 +
   4.750 +fun gen_dfg_cls (cls_id,ax_name,knd,lits, tvars,vars) = 
   4.751 +    let val ax_str = (if ax_name = "" then "" else ("_" ^ ax_name))
   4.752 +        val forall_str = if (vars = []) andalso (tvars = []) 
   4.753 +			 then 
   4.754 +				""
   4.755 +			 else 
   4.756 +			 	"forall([" ^ (strlist (vars@tvars))^ "]"
   4.757 +    in
   4.758 +	if forall_str = "" 
   4.759 +	then 
   4.760 +		"clause( %(" ^ knd ^ ")\n" ^ "or(" ^ lits ^ ") ,\n" ^  cls_id ^ ax_str ^  ")."
   4.761 +        else	
   4.762 +		"clause( %(" ^ knd ^ ")\n" ^ forall_str ^ ",\n" ^ "or(" ^ lits ^ ")),\n" ^  cls_id ^ ax_str ^  ")."
   4.763 +    end;
   4.764 +
   4.765 +
   4.766 +
   4.767 +fun gen_dfg_type_cls (cls_id,knd,tfree_lit,idx,tvars,  vars) = 
   4.768 +    let  val forall_str = if (vars = []) andalso (tvars = []) 
   4.769 +			 then 
   4.770 +				""
   4.771 +			 else 
   4.772 +			 	"forall([" ^ (strlist (vars@tvars))^"]"
   4.773 +    in
   4.774 +	if forall_str = "" 
   4.775 +	then 
   4.776 +		"clause( %(" ^ knd ^ ")\n" ^ "or( " ^ tfree_lit ^ ") ,\n" ^  cls_id ^ "_tcs" ^ (string_of_int idx) ^  ")."
   4.777 +        else	
   4.778 +		"clause( %(" ^ knd ^ ")\n" ^ forall_str ^ ",\n" ^ "or( " ^ tfree_lit ^ ")),\n" ^  cls_id ^ "_tcs" ^ (string_of_int idx) ^  ")."
   4.779 +    end;
   4.780 +
   4.781 +
   4.782 +
   4.783 +fun dfg_clause_aux (Clause cls) = 
   4.784 +    let val lits = map dfg_literal (#literals cls)
   4.785 +	val tvar_lits_strs = if (!keep_types) then (map dfg_of_typeLit (#tvar_type_literals cls)) else []
   4.786 +	val tfree_lits = if (!keep_types) then (map dfg_of_typeLit (#tfree_type_literals cls)) else []
   4.787 +    in
   4.788 +	(tvar_lits_strs @ lits,tfree_lits)
   4.789 +    end; 
   4.790 +
   4.791 +
   4.792 +fun dfg_folterms (Literal(pol,pred,tag)) = 
   4.793 +    let val  Predicate (predname, foltype, folterms) = pred
   4.794 +    in
   4.795 +	folterms
   4.796 +    end
   4.797 +
   4.798 + 
   4.799 +fun get_uvars (UVar(str,typ)) =(*if (substring (str, 0,2))= "V_" then  *)[str] (*else []*)
   4.800 +|   get_uvars (Fun (str,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist)
   4.801 +
   4.802 +
   4.803 +fun is_uvar  (UVar(str,typ)) = true
   4.804 +|   is_uvar  (Fun (str,typ,tlist)) = false;
   4.805 +
   4.806 +fun uvar_name  (UVar(str,typ)) = str
   4.807 +|   uvar_name  _ = (raise CLAUSE("Not a variable"));
   4.808 +
   4.809 +
   4.810 +fun mergelist [] = []
   4.811 +|   mergelist (x::xs ) = x@(mergelist xs)
   4.812 +
   4.813 +
   4.814 +fun dfg_vars (Clause cls) =
   4.815 +    let val  lits =  (#literals cls)
   4.816 +        val  folterms = mergelist(map dfg_folterms lits)
   4.817 +        val vars =  ResLib.flat_noDup(map get_uvars folterms)	
   4.818 +    in 
   4.819 +        vars
   4.820 +    end
   4.821 +
   4.822 +
   4.823 +fun dfg_tvars (Clause cls) =(#tvars cls)
   4.824 +
   4.825 +
   4.826 +	
   4.827 +(* make this return funcs and preds too? *)
   4.828 +fun string_of_predname (Predicate("equal",typ,terms)) = "EQUALITY"
   4.829 +  | string_of_predname (Predicate(name,_,[])) = name 
   4.830 +  | string_of_predname (Predicate(name,typ,terms)) = name
   4.831 +    
   4.832 +	
   4.833 +(* make this return funcs and preds too? *)
   4.834 +
   4.835 +    fun string_of_predicate (Predicate("equal",typ,terms)) = string_of_equality(typ,terms)
   4.836    | string_of_predicate (Predicate(name,_,[])) = name 
   4.837    | string_of_predicate (Predicate(name,typ,terms)) = 
   4.838        let val terms_as_strings = map string_of_term terms
   4.839 @@ -576,14 +890,247 @@
   4.840  	  else name ^ (ResLib.list_to_string terms_as_strings) 
   4.841        end;
   4.842  
   4.843 +
   4.844 +
   4.845 +
   4.846 +fun concat_with sep []  = ""
   4.847 +  | concat_with sep [x] = "(" ^ x ^ ")"
   4.848 +  | concat_with sep (x::xs) = "(" ^ x ^ ")" ^  sep ^ (concat_with sep xs);
   4.849 +
   4.850 +fun concat_with_comma []  = ""
   4.851 +  | concat_with_comma [x] =  x 
   4.852 +  | concat_with_comma (x::xs) =  x  ^ ", " ^ (concat_with_comma xs);
   4.853 +
   4.854 +
   4.855 +fun dfg_pred (Literal(pol,pred,tag)) ax_name = (string_of_predname pred)^" "^ax_name
   4.856 +
   4.857 +fun dfg_clause cls =
   4.858 +    let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)
   4.859 +        val vars = dfg_vars cls
   4.860 +        val tvars = dfg_tvars cls
   4.861 +	val cls_id = string_of_clauseID cls
   4.862 +	val ax_name = string_of_axiomName cls
   4.863 +	val knd = string_of_kind cls
   4.864 +	val lits_str = concat_with_comma lits
   4.865 +	val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars, vars) 			
   4.866 +        fun typ_clss k [] = []
   4.867 +          | typ_clss k (tfree :: tfrees) = 
   4.868 +            (gen_dfg_type_cls(cls_id,knd,tfree,k, tvars,vars)) ::  (typ_clss (k+1) tfrees)
   4.869 +    in 
   4.870 +	cls_str :: (typ_clss 0 tfree_lits)
   4.871 +    end;
   4.872 +
   4.873 +fun clause_info cls =
   4.874 +    let 
   4.875 +	val cls_id = string_of_clauseID cls
   4.876 +	val ax_name = string_of_axiomName cls
   4.877 +    in 
   4.878 +	((ax_name^""), cls_id)
   4.879 +    end;
   4.880 +
   4.881 +
   4.882 +
   4.883 +fun zip_concat name  [] = []
   4.884 +|   zip_concat  name ((str, num)::xs) = (((str^name), num)::(zip_concat name xs))
   4.885 +
   4.886 +
   4.887 +(*fun funcs_of_cls (Clause cls) = let val funcs = #functions cls
   4.888 + 				    val name = #axiom_name cls
   4.889 +				in
   4.890 +				    zip_concat name funcs 
   4.891 +				end;
   4.892 +
   4.893 +
   4.894 +fun preds_of_cls (Clause cls) = let val preds = #predicates cls
   4.895 +;                                   val name = ("foo"^(#axiom_name cls))
   4.896 +				in
   4.897 +				    zip_concat name preds
   4.898 +				end
   4.899 +*)
   4.900 +
   4.901 +fun funcs_of_cls (Clause cls) = #functions cls;
   4.902 +
   4.903 +
   4.904 +fun preds_of_cls (Clause cls) = #predicates cls;
   4.905 +
   4.906 +
   4.907 +
   4.908 +
   4.909 +fun string_of_arity (name, num) =  name ^"," ^ (string_of_int num) 
   4.910 +
   4.911 +
   4.912 +fun string_of_preds preds =  "predicates[" ^ (concat_with ", " (map string_of_arity preds)) ^ "].\n";
   4.913 +
   4.914 +fun string_of_funcs funcs ="functions[" ^ (concat_with ", " (map string_of_arity funcs)) ^ "].\n" ;
   4.915 +
   4.916 +
   4.917 +fun string_of_symbols predstr funcstr = "list_of_symbols.\n" ^ predstr  ^ funcstr  ^ "end_of_list.\n\n";
   4.918 +
   4.919 +
   4.920 +fun string_of_axioms axstr = "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n";
   4.921 +
   4.922 +
   4.923 +fun string_of_conjectures conjstr = "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n";
   4.924 +
   4.925 +fun string_of_descrip () = "list_of_descriptions.\nname({*[ File     : ],[ Names    :]*}).\nauthor({*[ Source   :]*}).\nstatus(unknown).\ndescription({*[ Refs     :]*}).\nend_of_list.\n\n"
   4.926 +
   4.927 +
   4.928 +fun string_of_start name = "%------------------------------------------------------------------------------\nbegin_problem(" ^ name ^ ").\n\n";
   4.929 +
   4.930 +
   4.931 +fun string_of_end () = "end_problem.\n%------------------------------------------------------------------------------";
   4.932 +
   4.933 +val delim = "\n";
   4.934 +val dfg_clauses2str = ResLib.list2str_sep delim; 
   4.935 +     
   4.936 +
   4.937 +fun clause2dfg cls =
   4.938 +    let val (lits,tfree_lits) = dfg_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)
   4.939 +	val cls_id = string_of_clauseID cls
   4.940 +	val ax_name = string_of_axiomName cls
   4.941 +        val vars = dfg_vars cls
   4.942 +        val tvars = dfg_tvars cls
   4.943 +        val funcs = funcs_of_cls cls
   4.944 +        val preds = preds_of_cls cls
   4.945 +	val knd = string_of_kind cls
   4.946 +	val lits_str = concat_with_comma lits
   4.947 +	val cls_str = gen_dfg_cls(cls_id,ax_name,knd,lits_str,tvars,vars) 
   4.948 +    in
   4.949 +	(cls_str,tfree_lits) 
   4.950 +    end;
   4.951 +
   4.952 +
   4.953 +
   4.954 +fun tfree_dfg_clause tfree_lit = "clause( %(conjecture)\n" ^  "or( " ^ tfree_lit ^ ")),\n" ^ "tfree_tcs" ^  ")."
   4.955 +
   4.956 +
   4.957 +fun gen_dfg_file fname axioms conjectures funcs preds tfrees= 
   4.958 +    let val (axstrs_tfrees) = (map clause2dfg axioms)
   4.959 +	val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
   4.960 +        val axstr = ResLib.list2str_sep delim axstrs
   4.961 +        val (conjstrs_tfrees) = (map clause2dfg conjectures)
   4.962 +	val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
   4.963 +        val tfree_clss = map tfree_dfg_clause ((ResLib.flat_noDup atfrees) \\ tfrees) 
   4.964 +        val conjstr = ResLib.list2str_sep delim (tfree_clss@conjstrs)
   4.965 +        val funcstr = string_of_funcs funcs
   4.966 +        val predstr = string_of_preds preds
   4.967 +    in
   4.968 +  (string_of_start fname) ^ (string_of_descrip ()) ^ (string_of_symbols funcstr predstr ) ^  
   4.969 +         (string_of_axioms axstr)^
   4.970 +        (string_of_conjectures conjstr) ^ (string_of_end ())
   4.971 +    end;
   4.972 +   
   4.973 +							    
   4.974 +
   4.975 +fun clauses2dfg [] filename axioms conjectures funcs preds tfrees= 
   4.976 +   let val funcs' = ((ResLib.flat_noDup(map funcs_of_cls axioms))@funcs)
   4.977 +       val preds' = ((ResLib.flat_noDup(map preds_of_cls axioms))@preds)
   4.978 +       
   4.979 +   
   4.980 +   in
   4.981 +	gen_dfg_file filename axioms conjectures funcs' preds' tfrees 
   4.982 +       (*(filename, axioms, conjectures, funcs, preds)*)
   4.983 +   end
   4.984 +|clauses2dfg (cls::clss) filename  axioms conjectures funcs preds tfrees = 
   4.985 +    let val (lits,tfree_lits) = dfg_clause_aux (cls) (*"lits" includes the typing assumptions (TVars)*)
   4.986 +	val cls_id = string_of_clauseID cls
   4.987 +	val ax_name = string_of_axiomName cls
   4.988 +        val vars = dfg_vars cls
   4.989 +        val tvars = dfg_tvars cls
   4.990 +        val funcs' = distinct((funcs_of_cls cls)@funcs)
   4.991 +        val preds' = distinct((preds_of_cls cls)@preds)
   4.992 +	val knd = string_of_kind cls
   4.993 +	val lits_str = concat_with ", " lits
   4.994 +	val axioms' = if knd = "axiom" then (cls::axioms) else axioms
   4.995 +	val conjectures' = if knd = "conjecture" then (cls::conjectures) else conjectures
   4.996 +    in
   4.997 +	clauses2dfg clss filename axioms' conjectures' funcs' preds' tfrees 
   4.998 +    end;
   4.999 +
  4.1000 +
  4.1001 +fun fileout f str = let val out = TextIO.openOut(f)
  4.1002 +    in
  4.1003 +	ResLib.writeln_strs out (str); TextIO.closeOut out
  4.1004 +    end;
  4.1005 +
  4.1006 +(*val filestr = clauses2dfg newcls "flump" [] [] [] [];
  4.1007 +*)
  4.1008 +(* fileout "flump.dfg" [filestr];*)
  4.1009 +
  4.1010 +
  4.1011 +(*FIX: ask Jia what this is for *)
  4.1012 +
  4.1013 +
  4.1014 +fun string_of_arClauseID (ArityClause arcls) = arclause_prefix ^ string_of_int(#clause_id arcls);
  4.1015 +
  4.1016 +
  4.1017 +fun string_of_arLit (TConsLit(b,(c,t,args))) =
  4.1018 +    let val pol = if b then "++" else "--"
  4.1019 +	val  arg_strs = (case args of [] => "" | _ => ResLib.list_to_string args)
  4.1020 +    in 
  4.1021 +	pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
  4.1022 +    end
  4.1023 +  | string_of_arLit (TVarLit(b,(c,str))) =
  4.1024 +    let val pol = if b then "++" else "--"
  4.1025 +    in
  4.1026 +	pol ^ c ^ "(" ^ str ^ ")"
  4.1027 +    end;
  4.1028      
  4.1029  
  4.1030 +fun string_of_conclLit (ArityClause arcls) = string_of_arLit (#conclLit arcls);
  4.1031 +     
  4.1032 +
  4.1033 +fun strings_of_premLits (ArityClause arcls) = map string_of_arLit (#premLits arcls);
  4.1034 +		
  4.1035 +
  4.1036 +fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
  4.1037 +
  4.1038 +(*FIX: would this have variables in a forall? *)
  4.1039 +
  4.1040 +fun dfg_arity_clause arcls = 
  4.1041 +    let val arcls_id = string_of_arClauseID arcls
  4.1042 +	val concl_lit = string_of_conclLit arcls
  4.1043 +	val prems_lits = strings_of_premLits arcls
  4.1044 +	val knd = string_of_arKind arcls
  4.1045 +	val all_lits = concl_lit :: prems_lits
  4.1046 +    in
  4.1047 +
  4.1048 +	"clause( %(" ^ knd ^ ")\n" ^  "or( " ^ (ResLib.list_to_string' all_lits) ^ ")),\n" ^ arcls_id ^  ")."
  4.1049 +    end;
  4.1050 +
  4.1051 +
  4.1052 +val clrelclause_prefix = "relcls_";
  4.1053 +
  4.1054 +(* FIX later.  Doesn't seem to be used in clasimp *)
  4.1055 +
  4.1056 +(*fun tptp_classrelLits sub sup = 
  4.1057 +    let val tvar = "(T)"
  4.1058 +    in 
  4.1059 +	case sup of NONE => "[++" ^ sub ^ tvar ^ "]"
  4.1060 +		  | (SOME supcls) =>  "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]"
  4.1061 +    end;
  4.1062 +
  4.1063 +
  4.1064 +fun tptp_classrelClause (ClassrelClause cls) =
  4.1065 +    let val relcls_id = clrelclause_prefix ^ string_of_int(#clause_id cls)
  4.1066 +	val sub = #subclass cls
  4.1067 +	val sup = #superclass cls
  4.1068 +	val lits = tptp_classrelLits sub sup
  4.1069 +    in
  4.1070 +	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")."
  4.1071 +    end; 
  4.1072 +    *)
  4.1073 +
  4.1074 +(********************************)
  4.1075 +(* code to produce TPTP files   *)
  4.1076 +(********************************)
  4.1077 +
  4.1078 +
  4.1079  
  4.1080  fun tptp_literal (Literal(pol,pred,tag)) =
  4.1081      let val pred_string = string_of_predicate pred
  4.1082 -	val tagged_pol = 
  4.1083 -	      if (tag andalso !tagged) then (if pol then "+++" else "---")
  4.1084 -	      else (if pol then "++" else "--")
  4.1085 +	val tagged_pol = if (tag andalso !tagged) then (if pol then "+++" else "---")
  4.1086 +                         else (if pol then "++" else "--")
  4.1087       in
  4.1088  	tagged_pol ^ pred_string
  4.1089      end;
  4.1090 @@ -595,26 +1142,19 @@
  4.1091   
  4.1092  
  4.1093  fun gen_tptp_cls (cls_id,ax_name,knd,lits) = 
  4.1094 -    let val ax_str = (if ax_name = "" then "" else ("_" ^ ascii_of ax_name))
  4.1095 +    let val ax_str = (if ax_name = "" then "" else ("_" ^ ax_name))
  4.1096      in
  4.1097  	"input_clause(" ^ cls_id ^ ax_str ^ "," ^ knd ^ "," ^ lits ^ ")."
  4.1098      end;
  4.1099  
  4.1100 -fun gen_tptp_type_cls (cls_id,knd,tfree_lit,idx) = 
  4.1101 -    "input_clause(" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ "," ^ 
  4.1102 -    knd ^ ",[" ^ tfree_lit ^ "]).";
  4.1103 +
  4.1104 +fun gen_tptp_type_cls (cls_id,knd,tfree_lit,idx) = "input_clause(" ^ cls_id ^ "_tcs" ^ (string_of_int idx) ^ "," ^ knd ^ ",[" ^ tfree_lit ^ "]).";
  4.1105  
  4.1106  
  4.1107  fun tptp_clause_aux (Clause cls) = 
  4.1108      let val lits = map tptp_literal (#literals cls)
  4.1109 -	val tvar_lits_strs =
  4.1110 -	      if (!keep_types) 
  4.1111 -	      then (map tptp_of_typeLit (#tvar_type_literals cls)) 
  4.1112 -	      else []
  4.1113 -	val tfree_lits = 
  4.1114 -	      if (!keep_types) 
  4.1115 -	      then (map tptp_of_typeLit (#tfree_type_literals cls)) 
  4.1116 -	      else []
  4.1117 +	val tvar_lits_strs = if (!keep_types) then (map tptp_of_typeLit (#tvar_type_literals cls)) else []
  4.1118 +	val tfree_lits = if (!keep_types) then (map tptp_of_typeLit (#tfree_type_literals cls)) else []
  4.1119      in
  4.1120  	(tvar_lits_strs @ lits,tfree_lits)
  4.1121      end; 
  4.1122 @@ -633,7 +1173,13 @@
  4.1123  	cls_str :: (typ_clss 0 tfree_lits)
  4.1124      end;
  4.1125  
  4.1126 -fun clause_info cls = (string_of_axiomName cls, string_of_clauseID cls);
  4.1127 +fun clause_info cls =
  4.1128 +    let 
  4.1129 +	val cls_id = string_of_clauseID cls
  4.1130 +	val ax_name = string_of_axiomName cls
  4.1131 +    in 
  4.1132 +	((ax_name^""), cls_id)
  4.1133 +    end;
  4.1134  
  4.1135  
  4.1136  fun clause2tptp cls =
  4.1137 @@ -648,8 +1194,7 @@
  4.1138      end;
  4.1139  
  4.1140  
  4.1141 -fun tfree_clause tfree_lit =
  4.1142 -    "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).";
  4.1143 +fun tfree_clause tfree_lit = "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).";
  4.1144  
  4.1145  val delim = "\n";
  4.1146  val tptp_clauses2str = ResLib.list2str_sep delim; 
  4.1147 @@ -710,5 +1255,5 @@
  4.1148      in
  4.1149  	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")."
  4.1150      end; 
  4.1151 -    
  4.1152 +
  4.1153  end;