# HG changeset patch
# User paulson
# Date 1179849366 -7200
# Node ID 69e30a7e888018ac7e819d39b6d8f1f269324717
# Parent  a53cb8ddb052718df93e092842e04a1543321caf
Some hacks for SPASS format

diff -r a53cb8ddb052 -r 69e30a7e8880 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Tue May 22 17:25:26 2007 +0200
+++ b/src/HOL/Tools/res_clause.ML	Tue May 22 17:56:06 2007 +0200
@@ -179,15 +179,24 @@
       tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
 
+(*HACK because SPASS truncates identifiers to 63 characters :-(( *)
+val dfg_format = ref false;
+
+(*32-bit hash,so we expect no collisions unless there are around 65536 long identifiers...*)
+fun controlled_length s =
+  if size s > 60 andalso !dfg_format   
+  then Word.toString (Polyhash.hashw_string(s,0w0))
+  else s;
+
 fun lookup_const c =
     case Symtab.lookup const_trans_table c of
         SOME c' => c'
-      | NONE => ascii_of c;
+      | NONE => controlled_length (ascii_of c);
 
 fun lookup_type_const c = 
     case Symtab.lookup type_const_trans_table c of
         SOME c' => c'
-      | NONE => ascii_of c;
+      | NONE => controlled_length (ascii_of c);
 
 fun make_fixed_const "op =" = "equal"   (*MUST BE "equal" because it's built-in to ATPs*)
   | make_fixed_const c      = const_prefix ^ lookup_const c;
@@ -611,9 +620,12 @@
        literals
   handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
 
+(*This type can be overlooked because it is built-in...*)
+val init_functab = Symtab.update ("tc_itself", 1) Symtab.empty;
+
 fun funcs_of_clauses clauses arity_clauses = 
   Symtab.dest (foldl add_arityClause_funcs 
-                     (foldl add_clause_funcs Symtab.empty clauses)
+                     (foldl add_clause_funcs init_functab clauses)
                      arity_clauses)
 
 
@@ -739,6 +751,7 @@
 fun dfg_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) = 
   let 
     val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
+    val _ = dfg_format := true
     val conjectures = make_conjecture_clauses thms
     val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
     val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
@@ -825,6 +838,7 @@
 fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) =
   let
     val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
+    val _ = dfg_format := false
     val clss = make_conjecture_clauses thms
     val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
     val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)