# HG changeset patch
# User blanchet
# Date 1324403990 -3600
# Node ID 711fec5b4f6116337d0496d9bedcba0698f5a968
# Parent  c99af5431dfe4a1b2a4e021eee35ebe5ee35bc20
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers

diff -r c99af5431dfe -r 711fec5b4f61 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Dec 20 18:59:50 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Dec 20 18:59:50 2011 +0100
@@ -109,7 +109,7 @@
     (string * string) problem -> (string * string) problem
   val declared_syms_in_problem : (string * ''a) problem -> (string * ''a) list
   val nice_atp_problem :
-    bool -> ('a * (string * string) problem_line list) list
+    bool -> atp_format -> ('a * (string * string) problem_line list) list
     -> ('a * string problem_line list) list
        * (string Symtab.table * string Symtab.table) option
 end;
@@ -619,9 +619,6 @@
 
 (** Nice names **)
 
-fun empty_name_pool readable_names =
-  if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
-
 fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
 fun pool_map f xs =
   pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
@@ -643,39 +640,36 @@
    unreadable "op_1", "op_2", etc., in the problem files. "eq" is reserved to
    ensure that "HOL.eq" is correctly mapped to equality (not clear whether this
    is still necessary). *)
-val spass_reserved_nice_names =
-  ["and", "def", "equal", "equiv", "exists", "false", "forall", "fract", "ge",
-   "gs", "id", "implied", "implies", "le", "lr", "ls", "minus", "mult", "not",
-   "or", "plus", "true"]
-val reserved_nice_names =
-  [tptp_old_equal, "op", "eq"] @ spass_reserved_nice_names
+val reserved_nice_names = [tptp_old_equal, "op", "eq"]
 
-fun readable_name full_name s =
-  if s = full_name then
-    s
-  else
-    s |> no_qualifiers
-      |> perhaps (try (unprefix "'"))
-      |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
-      |> (fn s =>
-             if size s > max_readable_name_size then
-               String.substring (s, 0, max_readable_name_size div 2 - 4) ^
-               string_of_int (hash_string full_name) ^
-               String.extract (s, size s - max_readable_name_size div 2 + 4,
-                               NONE)
-             else
-               s)
-      |> (fn s => if member (op =) reserved_nice_names s then full_name else s)
+fun readable_name underscore full_name s =
+  (if s = full_name then
+     s
+   else
+     s |> no_qualifiers
+       |> perhaps (try (unprefix "'"))
+       |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
+       |> (fn s =>
+              if size s > max_readable_name_size then
+                String.substring (s, 0, max_readable_name_size div 2 - 4) ^
+                string_of_int (hash_string full_name) ^
+                String.extract (s, size s - max_readable_name_size div 2 + 4,
+                                NONE)
+              else
+                s)
+       |> (fn s =>
+              if member (op =) reserved_nice_names s then full_name else s))
+  |> underscore ? suffix "_"
 
-fun nice_name (full_name, _) NONE = (full_name, NONE)
-  | nice_name (full_name, desired_name) (SOME the_pool) =
+fun nice_name _ (full_name, _) NONE = (full_name, NONE)
+  | nice_name underscore (full_name, desired_name) (SOME the_pool) =
     if is_built_in_tptp_symbol full_name then
       (full_name, SOME the_pool)
     else case Symtab.lookup (fst the_pool) full_name of
       SOME nice_name => (nice_name, SOME the_pool)
     | NONE =>
       let
-        val nice_prefix = readable_name full_name desired_name
+        val nice_prefix = readable_name underscore full_name desired_name
         fun add j =
           let
             val nice_name =
@@ -692,32 +686,37 @@
           end
       in add 0 |> apsnd SOME end
 
-fun nice_type (AType (name, tys)) =
-    nice_name name ##>> pool_map nice_type tys #>> AType
-  | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
-  | nice_type (ATyAbs (names, ty)) =
-    pool_map nice_name names ##>> nice_type ty #>> ATyAbs
-fun nice_term (ATerm (name, ts)) =
-    nice_name name ##>> pool_map nice_term ts #>> ATerm
-  | nice_term (AAbs ((name, ty), tm)) =
-    nice_name name ##>> nice_type ty ##>> nice_term tm #>> AAbs
-fun nice_formula (AQuant (q, xs, phi)) =
-    pool_map nice_name (map fst xs)
-    ##>> pool_map (fn NONE => pair NONE
-                    | SOME ty => nice_type ty #>> SOME) (map snd xs)
-    ##>> nice_formula phi
-    #>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
-  | nice_formula (AConn (c, phis)) =
-    pool_map nice_formula phis #>> curry AConn c
-  | nice_formula (AAtom tm) = nice_term tm #>> AAtom
-fun nice_problem_line (Decl (ident, sym, ty)) =
-    nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Decl (ident, sym, ty))
-  | nice_problem_line (Formula (ident, kind, phi, source, info)) =
-    nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
-fun nice_problem problem =
-  pool_map (fn (heading, lines) =>
-               pool_map nice_problem_line lines #>> pair heading) problem
-fun nice_atp_problem readable_names problem =
-  nice_problem problem (empty_name_pool readable_names)
+fun nice_atp_problem readable_names format problem =
+  let
+    val empty_pool =
+      if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
+    val underscore = case format of DFG _ => true | _ => false
+    val nice_name = nice_name underscore
+    fun nice_type (AType (name, tys)) =
+        nice_name name ##>> pool_map nice_type tys #>> AType
+      | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
+      | nice_type (ATyAbs (names, ty)) =
+        pool_map nice_name names ##>> nice_type ty #>> ATyAbs
+    fun nice_term (ATerm (name, ts)) =
+        nice_name name ##>> pool_map nice_term ts #>> ATerm
+      | nice_term (AAbs ((name, ty), tm)) =
+        nice_name name ##>> nice_type ty ##>> nice_term tm #>> AAbs
+    fun nice_formula (AQuant (q, xs, phi)) =
+        pool_map nice_name (map fst xs)
+        ##>> pool_map (fn NONE => pair NONE
+                        | SOME ty => nice_type ty #>> SOME) (map snd xs)
+        ##>> nice_formula phi
+        #>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
+      | nice_formula (AConn (c, phis)) =
+        pool_map nice_formula phis #>> curry AConn c
+      | nice_formula (AAtom tm) = nice_term tm #>> AAtom
+    fun nice_problem_line (Decl (ident, sym, ty)) =
+        nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Decl (ident, sym, ty))
+      | nice_problem_line (Formula (ident, kind, phi, source, info)) =
+        nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
+    fun nice_problem problem =
+      pool_map (fn (heading, lines) =>
+                   pool_map nice_problem_line lines #>> pair heading) problem
+  in nice_problem problem empty_pool end
 
 end;
diff -r c99af5431dfe -r 711fec5b4f61 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 20 18:59:50 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 20 18:59:50 2011 +0100
@@ -2467,7 +2467,7 @@
           | TFF (_, TPTP_Implicit) => I
           | THF (_, TPTP_Implicit, _) => I
           | _ => declare_undeclared_syms_in_atp_problem type_enc)
-    val (problem, pool) = problem |> nice_atp_problem readable_names
+    val (problem, pool) = problem |> nice_atp_problem readable_names format
     fun add_sym_ary (s, {min_ary, ...} : sym_info) =
       min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
   in