# HG changeset patch
# User blanchet
# Date 1301936015 -7200
# Node ID 662b50b7126fcee4251cf734d026b19eda517232
# Parent  183ea7f77b72d18a914045045e62de8c2eda27ee
if "monomorphize" is enabled, mangle the type information in the names by default

diff -r 183ea7f77b72 -r 662b50b7126f src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Apr 04 16:35:46 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Apr 04 18:53:35 2011 +0200
@@ -123,6 +123,16 @@
 fun pool_map f xs =
   pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
 
+val no_qualifiers =
+  let
+    fun skip [] = []
+      | skip (#"." :: cs) = skip cs
+      | skip (c :: cs) = if Char.isAlphaNum c then skip cs else c :: keep cs
+    and keep [] = []
+      | keep (#"." :: cs) = skip cs
+      | keep (c :: cs) = c :: keep cs
+  in String.explode #> rev #> keep #> rev #> String.implode end
+
 (* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the
    problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure
    that "HOL.eq" is correctly mapped to equality. *)
@@ -132,7 +142,7 @@
     s
   else
     let
-      val s = s |> Long_Name.base_name
+      val s = s |> no_qualifiers
                 |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
     in if member (op =) reserved_nice_names s then full_name else s end
 
diff -r 183ea7f77b72 -r 662b50b7126f src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Mon Apr 04 16:35:46 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Mon Apr 04 18:53:35 2011 +0200
@@ -345,23 +345,23 @@
           end
         | SOME b =>
           let
-            val c = invert_const b
+            val (c, mangled_us) = b |> unmangled_const |>> invert_const
             val num_ty_args = num_atp_type_args thy type_sys c
-            val (type_us, term_us) = chop num_ty_args us
+            val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
             (* Extra args from "hAPP" come after any arguments given directly to
                the constant. *)
             val term_ts = map (aux NONE []) term_us
             val extra_ts = map (aux NONE []) extra_us
-            val t =
-              Const (c, case opt_T of
-                          SOME T => map fastype_of term_ts ---> T
-                        | NONE =>
-                          if num_type_args thy c = length type_us then
-                            Sign.const_instance thy (c,
-                                map (type_from_fo_term tfrees) type_us)
-                          else
-                            HOLogic.typeT)
-          in list_comb (t, term_ts @ extra_ts) end
+            val T =
+              case opt_T of
+                SOME T => map fastype_of term_ts ---> T
+              | NONE =>
+                if num_type_args thy c = length type_us then
+                  Sign.const_instance thy (c,
+                      map (type_from_fo_term tfrees) type_us)
+                else
+                  HOLogic.typeT
+          in list_comb (Const (c, T), term_ts @ extra_ts) end
         | NONE => (* a free or schematic variable *)
           let
             val ts = map (aux NONE []) (us @ extra_us)
@@ -399,7 +399,8 @@
   | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
   | uncombine_term (t as Const (x as (s, _))) =
     (case AList.lookup (op =) combinator_table s of
-       SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
+       SOME thm => thm |> prop_of |> specialize_type @{theory} x
+                       |> Logic.dest_equals |> snd
      | NONE => t)
   | uncombine_term t = t
 
diff -r 183ea7f77b72 -r 662b50b7126f src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon Apr 04 16:35:46 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon Apr 04 18:53:35 2011 +0200
@@ -8,6 +8,7 @@
 
 signature SLEDGEHAMMER_ATP_TRANSLATE =
 sig
+  type 'a fo_term = 'a ATP_Problem.fo_term
   type 'a problem = 'a ATP_Problem.problem
   type translated_formula
 
@@ -15,6 +16,7 @@
     Tags of bool |
     Preds of bool |
     Const_Args |
+    Mangled |
     No_Types
 
   val precise_overloaded_args : bool Unsynchronized.ref
@@ -25,6 +27,7 @@
   val translate_atp_fact :
     Proof.context -> bool -> (string * 'a) * thm
     -> translated_formula option * ((string * 'a) * thm)
+  val unmangled_const : string -> string * string fo_term list
   val prepare_atp_problem :
     Proof.context -> bool -> bool -> type_system -> bool -> term list -> term
     -> (translated_formula option * ((string * 'a) * thm)) list
@@ -63,6 +66,7 @@
   Tags of bool |
   Preds of bool |
   Const_Args |
+  Mangled |
   No_Types
 
 fun types_dangerous_types (Tags _) = true
@@ -84,10 +88,22 @@
     Tags full_types => not full_types andalso is_overloaded thy s
   | Preds _ => is_overloaded thy s (* FIXME: could be more precise *)
   | Const_Args => is_overloaded thy s
+  | Mangled => true
   | No_Types => false
 
+datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types
+
+fun type_arg_policy thy type_sys s =
+  if needs_type_args thy type_sys s then
+    if type_sys = Mangled then Mangled_Types else Explicit_Type_Args
+  else
+    No_Type_Args
+
 fun num_atp_type_args thy type_sys s =
-  if needs_type_args thy type_sys s then num_type_args thy s else 0
+  if type_arg_policy thy type_sys s = Explicit_Type_Args then
+    num_type_args thy s
+  else
+    0
 
 fun atp_type_literals_for_types type_sys Ts =
   if type_sys = No_Types then [] else type_literals_for_types Ts
@@ -389,6 +405,41 @@
    ("c_implies", (2, ("c_fimplies", @{const_name Metis.fimplies}))),
    ("equal", (2, ("c_fequal", @{const_name Metis.fequal})))]
 
+(* We are crossing our fingers that it doesn't clash with anything else. *)
+val mangled_type_sep = "\000"
+
+fun mangled_combtyp f (CombTFree name) = f name
+  | mangled_combtyp f (CombType (name, tys)) =
+    "(" ^ commas (map (mangled_combtyp f) tys) ^ ")" ^ f name
+  | mangled_combtyp _ _ = raise Fail "impossible schematic type variable"
+
+fun mangled_type_suffix f g tys =
+  fold_rev (curry (op ^) o g o prefix mangled_type_sep o mangled_combtyp f)
+           tys ""
+
+val parse_mangled_ident =
+  Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
+
+fun parse_mangled_type x =
+  ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")"
+      -- parse_mangled_ident >> (ATerm o swap)
+   || parse_mangled_ident >> (ATerm o rpair [])) x
+and parse_mangled_types x =
+  (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
+
+fun unmangled_type s =
+  s |> suffix ")" |> raw_explode
+    |> Scan.finite Symbol.stopper
+           (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
+                                                quote s)) parse_mangled_type))
+    |> fst
+    |> tap (fn u => PolyML.makestring u |> warning) (*###*)
+
+fun unmangled_const s =
+  let val ss = space_explode mangled_type_sep s in
+    (hd ss, map unmangled_type (tl ss))
+  end
+
 fun fo_term_for_combterm ctxt type_sys =
   let
     val thy = ProofContext.theory_of ctxt
@@ -411,11 +462,14 @@
                case strip_prefix_and_unascii const_prefix s of
                  NONE => (name, ty_args)
                | SOME s'' =>
-                 let
-                   val s'' = invert_const s''
-                   val ty_args =
-                     if needs_type_args thy type_sys s'' then ty_args else []
-                  in (name, ty_args) end)
+                 let val s'' = invert_const s'' in
+                   case type_arg_policy thy type_sys s'' of
+                     No_Type_Args => (name, [])
+                   | Explicit_Type_Args => (name, ty_args)
+                   | Mangled_Types =>
+                     ((s ^ mangled_type_suffix fst ascii_of ty_args,
+                       s' ^ mangled_type_suffix snd I ty_args), [])
+                 end)
           | CombVar (name, _) => (name, [])
           | CombApp _ => raise Fail "impossible \"CombApp\""
         val t =
@@ -529,7 +583,9 @@
         String.isPrefix class_prefix s then
        16383 (* large number *)
      else case strip_prefix_and_unascii const_prefix s of
-       SOME s' => num_atp_type_args thy type_sys (invert_const s')
+       SOME s' =>
+       s' |> unmangled_const |> fst |> invert_const
+          |> num_atp_type_args thy type_sys
      | NONE => 0)
   | min_arity_of _ _ (SOME the_const_tab) s =
     case Symtab.lookup the_const_tab s of
diff -r 183ea7f77b72 -r 662b50b7126f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Apr 04 16:35:46 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Apr 04 18:53:35 2011 +0200
@@ -190,9 +190,6 @@
                          end)]
   end
 
-val smart_full_type_sys = Tags true
-val smart_partial_type_sys = Const_Args
-
 val infinity_time_in_secs = 60 * 60 * 24 * 365
 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
 
@@ -245,10 +242,14 @@
         ("tags", full_types) => Tags full_types
       | ("preds", full_types) => Preds full_types
       | ("const_args", false) => Const_Args
+      | ("mangled", false) => if monomorphize then Mangled else Const_Args
       | ("none", false) => No_Types
       | (type_sys, full_types) =>
-        if member (op =) ["const_args", "none", "smart"] type_sys then
-          if full_types then smart_full_type_sys else smart_partial_type_sys
+        if member (op =) ["const_args", "mangled", "none", "smart"]
+                  type_sys then
+          if full_types then Tags true
+          else if monomorphize then Mangled
+          else Const_Args
         else
           error ("Unknown type system: " ^ quote type_sys ^ ".")
     val explicit_apply = lookup_bool "explicit_apply"