store nonmangled names along with mangled type names in Sledgehammer for debugging purposes

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Apr 15 13:57:17 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 16 14:48:34 2010 +0200
@@ -65,8 +65,8 @@
           else SOME "Ill-formed ATP output"
   | (failure :: _) => SOME failure
 
-fun generic_prover overlord get_facts prepare write cmd args failure_strs
-        produce_answer name ({full_types, ...} : params)
+fun generic_prover overlord get_facts prepare write_file cmd args failure_strs
+        produce_answer name ({debug, full_types, ...} : params)
         ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
          : problem) =
   let
@@ -100,7 +100,7 @@
         if destdir' = "" then File.tmp_path probfile
         else if File.exists (Path.explode destdir')
         then Path.append  (Path.explode destdir') probfile
-        else error ("No such directory: " ^ destdir')
+        else error ("No such directory: " ^ destdir' ^ ".")
       end;
 
     (* write out problem file and call prover *)
@@ -127,7 +127,7 @@
       if Config.get ctxt measure_runtime then split_time s else (s, 0)
     fun run_on probfile =
       if File.exists cmd then
-        write full_types probfile clauses
+        write_file debug full_types probfile clauses
         |> pair (apfst split_time' (bash_output (cmd_line probfile)))
       else error ("Bad executable: " ^ Path.implode cmd ^ ".");
 

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Apr 15 13:57:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Apr 16 14:48:34 2010 +0200
@@ -69,10 +69,10 @@
 
 fun metis_lit b c args = (b, (c, args));
 
-fun hol_type_to_fol (TyVar x) = Metis.Term.Var x
-  | hol_type_to_fol (TyFree x) = Metis.Term.Fn (x, [])
-  | hol_type_to_fol (TyConstr (tc, tps)) =
-    Metis.Term.Fn (tc, map hol_type_to_fol tps);
+fun hol_type_to_fol (TyVar (x, _)) = Metis.Term.Var x
+  | hol_type_to_fol (TyFree (s, _)) = Metis.Term.Fn (s, [])
+  | hol_type_to_fol (TyConstr ((s, _), tps)) =
+    Metis.Term.Fn (s, map hol_type_to_fol tps);
 
 (*These two functions insert type literals before the real literals. That is the
   opposite order from TPTP linkup, but maybe OK.*)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 15 13:57:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Apr 16 14:48:34 2010 +0200
@@ -30,12 +30,17 @@
   val make_fixed_const : bool -> string -> string
   val make_fixed_type_const : bool -> string -> string
   val make_type_class : string -> string
+  type name = string * string
+  type name_pool = string Symtab.table * string Symtab.table
+  val empty_name_pool : bool -> name_pool option
+  val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
+  val nice_name : name -> name_pool option -> string * name_pool option
   datatype kind = Axiom | Conjecture
   type axiom_name = string
   datatype fol_type =
-    TyVar of string |
-    TyFree of string |
-    TyConstr of string * fol_type list
+    TyVar of name |
+    TyFree of name |
+    TyConstr of name * fol_type list
   val string_of_fol_type : fol_type -> string
   datatype type_literal = LTVar of string * string | LTFree of string * string
   exception CLAUSE of string * term
@@ -207,7 +212,65 @@
 fun make_type_class clas = class_prefix ^ ascii_of clas;
 
 
-(***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****)
+(**** name pool ****)
+ 
+type name = string * string
+type name_pool = string Symtab.table * string Symtab.table
+
+fun empty_name_pool debug = if debug then SOME (`I Symtab.empty) else NONE
+
+fun pool_map f xs =
+  fold (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs o pair []
+
+fun add_nice_name full_name nice_prefix j the_pool =
+  let
+    val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j)
+  in
+    case Symtab.lookup (snd the_pool) nice_name of
+      SOME full_name' =>
+      if full_name = full_name' then (nice_name, the_pool)
+      else add_nice_name full_name nice_prefix (j + 1) the_pool
+    | NONE =>
+      (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool),
+                   Symtab.update_new (nice_name, full_name) (snd the_pool)))
+  end
+
+fun translate_first_char f s =
+  String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
+
+fun clean_short_name full_name s =
+  let
+    val s = s |> Long_Name.base_name
+              |> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"]
+    val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
+    val s' =
+      (s' |> rev
+          |> implode
+          |> String.translate
+                 (fn c => if Char.isAlphaNum c then String.str c else ""))
+      ^ replicate_string (String.size s - length s') "_"
+    val s' =
+      if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
+      else s'
+    val s' = if s' = "op" then full_name else s'
+  in
+    case (Char.isLower (String.sub (full_name, 0)),
+          Char.isLower (String.sub (s', 0))) of
+      (true, false) => translate_first_char Char.toLower s'
+    | (false, true) => translate_first_char Char.toUpper s'
+    | _ => s'
+  end
+
+fun nice_name (full_name, _) NONE = (full_name, NONE)
+  | nice_name (full_name, desired_name) (SOME the_pool) =
+    case Symtab.lookup (fst the_pool) full_name of
+      SOME nice_name => (nice_name, SOME the_pool)
+    | NONE => add_nice_name full_name (clean_short_name full_name desired_name)
+                            0 the_pool
+              |> apsnd SOME
+
+(**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG
+      format ****)
 
 datatype kind = Axiom | Conjecture;
 
@@ -216,13 +279,13 @@
 (**** Isabelle FOL clauses ****)
 
 datatype fol_type =
-  TyVar of string |
-  TyFree of string |
-  TyConstr of string * fol_type list
+  TyVar of name |
+  TyFree of name |
+  TyConstr of name * fol_type list
 
-fun string_of_fol_type (TyVar s) = s
-  | string_of_fol_type (TyFree s) = s
-  | string_of_fol_type (TyConstr (tcon, tps)) =
+fun string_of_fol_type (TyVar (s, _)) = s
+  | string_of_fol_type (TyFree (s, _)) = s
+  | string_of_fol_type (TyConstr ((tcon, _), tps)) =
       tcon ^ (paren_pack (map string_of_fol_type tps));
 
 (*First string is the type class; the second is a TVar or TFfree*)
@@ -230,19 +293,9 @@
 
 exception CLAUSE of string * term;
 
-fun atomic_type (TFree (a,_)) = TyFree(make_fixed_type_var a)
-  | atomic_type (TVar (v,_))  = TyVar(make_schematic_type_var v);
-
-(*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
-  TVars it contains.*)
-fun type_of dfg (Type (a, Ts)) =
-      let val (folTyps, ts) = types_of dfg Ts
-          val t = make_fixed_type_const dfg a
-      in (TyConstr (t, folTyps), ts) end
-  | type_of dfg T = (atomic_type T, [T])
-and types_of dfg Ts =
-      let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
-      in (folTyps, union_all ts) end;
+fun atomic_type (TFree (a,_)) = TyFree (`make_fixed_type_var a)
+  | atomic_type (TVar (x, _)) =
+    TyVar (make_schematic_type_var x, string_of_indexname x)
 
 (*Make literals for sorted type variables*)
 fun sorts_on_typs_aux (_, [])   = []
@@ -402,9 +455,9 @@
 (*** Find occurrences of functions in clauses ***)
 
 fun add_foltype_funcs (TyVar _, funcs) = funcs
-  | add_foltype_funcs (TyFree a, funcs) = Symtab.update (a,0) funcs
-  | add_foltype_funcs (TyConstr (a, tys), funcs) =
-      List.foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
+  | add_foltype_funcs (TyFree (s, _), funcs) = Symtab.update (s, 0) funcs
+  | add_foltype_funcs (TyConstr ((s, _), tys), funcs) =
+      List.foldl add_foltype_funcs (Symtab.update (s, length tys) funcs) tys;
 
 (*TFrees are recorded as constants*)
 fun add_type_sort_funcs (TVar _, funcs) = funcs

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 15 13:57:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Apr 16 14:48:34 2010 +0200
@@ -33,11 +33,11 @@
   val get_helper_clauses : bool -> theory -> bool ->
        hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
        hol_clause list
-  val write_tptp_file : bool -> Path.T ->
+  val write_tptp_file : bool -> bool -> Path.T ->
     hol_clause list * hol_clause list * hol_clause list * hol_clause list *
     classrel_clause list * arity_clause list ->
     int * int
-  val write_dfg_file : bool -> Path.T ->
+  val write_dfg_file : bool -> bool -> Path.T ->
     hol_clause list * hol_clause list * hol_clause list * hol_clause list *
     classrel_clause list * arity_clause list -> int * int
 end
@@ -102,19 +102,22 @@
 fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
 
 fun type_of dfg (Type (a, Ts)) =
-      let val (folTypes,ts) = types_of dfg Ts
-      in  (TyConstr (make_fixed_type_const dfg a, folTypes), ts)  end
-  | type_of _ (tp as TFree (a, _)) = (TyFree (make_fixed_type_var a), [tp])
-  | type_of _ (tp as TVar (v, _)) = (TyVar (make_schematic_type_var v), [tp])
+    let val (folTypes,ts) = types_of dfg Ts in
+      (TyConstr (`(make_fixed_type_const dfg) a, folTypes), ts)
+    end
+  | type_of _ (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
+  | type_of _ (tp as TVar (x, _)) =
+    (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
 and types_of dfg Ts =
       let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
       in  (folTyps, union_all ts)  end;
 
 (* same as above, but no gathering of sort information *)
 fun simp_type_of dfg (Type (a, Ts)) =
-      TyConstr (make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
-  | simp_type_of _ (TFree (a, _)) = TyFree (make_fixed_type_var a)
-  | simp_type_of _ (TVar (v, _)) = TyVar (make_schematic_type_var v);
+      TyConstr (`(make_fixed_type_const dfg) a, map (simp_type_of dfg) Ts)
+  | simp_type_of _ (TFree (a, _)) = TyFree (`make_fixed_type_var a)
+  | simp_type_of _ (TVar (x, _)) =
+    TyVar (make_schematic_type_var x, string_of_indexname x);
 
 
 fun const_type_of dfg thy (c,t) =
@@ -193,7 +196,7 @@
 (**********************************************************************)
 
 (*Result of a function type; no need to check that the argument type matches.*)
-fun result_type (TyConstr ("tc_fun", [_, tp2])) = tp2
+fun result_type (TyConstr (("tc_fun", _), [_, tp2])) = tp2
   | result_type _ = raise Fail "Non-function type"
 
 fun type_of_combterm (CombConst (_, tp, _)) = tp
@@ -452,7 +455,7 @@
 
 (* TPTP format *)
 
-fun write_tptp_file full_types file clauses =
+fun write_tptp_file debug full_types file clauses =
   let
     fun section _ [] = []
       | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
@@ -480,7 +483,7 @@
 
 (* DFG format *)
 
-fun write_dfg_file full_types file clauses =
+fun write_dfg_file debug full_types file clauses =
   let
     val (conjectures, axclauses, _, helper_clauses,
       classrel_clauses, arity_clauses) = clauses

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Apr 15 13:57:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 16 14:48:34 2010 +0200
@@ -8,6 +8,8 @@
 sig
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
+  val replace_all : string -> string -> string -> string
+  val remove_all : string -> string -> string
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
   val hashw : word * word -> word
@@ -26,6 +28,18 @@
   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
 
+fun replace_all bef aft =
+  let
+    fun aux seen "" = String.implode (rev seen)
+      | aux seen s =
+      if String.isPrefix bef s then
+          aux seen "" ^ aft ^ aux [] (unprefix bef s)
+        else
+          aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
+  in aux [] end
+
+fun remove_all bef = replace_all bef ""
+
 fun parse_bool_option option name s =
   (case s of
      "smart" => if option then NONE else raise Option