# HG changeset patch
# User blanchet
# Date 1304267845 -7200
# Node ID 77f94ac04f320a53fdbebed17808e4227022a696
# Parent  5737947e4c776127e1ede404a0a3bc563eb68a76
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0

diff -r 5737947e4c77 -r 77f94ac04f32 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
@@ -123,7 +123,7 @@
             case strip_prefix_and_unascii const_prefix a of
                 SOME b =>
                   let
-                    val c = invert_const b
+                    val c = b |> invert_const |> unproxify_const
                     val ntypes = num_type_args thy c
                     val nterms = length ts - ntypes
                     val tts = map tm_to_tt ts
@@ -168,7 +168,7 @@
   let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
                                        Metis_Term.toString fol_tm)
       fun do_const c =
-        let val c = c |> invert_const in
+        let val c = c |> invert_const |> unproxify_const in
           if String.isPrefix new_skolem_const_prefix c then
             Var ((new_skolem_var_name_from_const c, 1), dummyT)
           else
diff -r 5737947e4c77 -r 77f94ac04f32 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:25 2011 +0200
@@ -43,9 +43,9 @@
   val type_const_prefix: string
   val class_prefix: string
   val new_skolem_const_prefix : string
-  val metis_proxies : (string * (string * string)) list
-  val safe_invert_const: string -> string
+  val proxify_const : string -> (string * string) option
   val invert_const: string -> string
+  val unproxify_const: string -> string
   val ascii_of: string -> string
   val unascii_of: string -> string
   val strip_prefix_and_unascii: string -> string -> string option
@@ -104,13 +104,16 @@
 fun union_all xss = fold (union (op =)) xss []
 
 val metis_proxies =
-  [("c_False", ("fFalse", @{const_name Metis.fFalse})),
-   ("c_True", ("fTrue", @{const_name Metis.fTrue})),
-   ("c_Not", ("fNot", @{const_name Metis.fNot})),
-   ("c_conj", ("fconj", @{const_name Metis.fconj})),
-   ("c_disj", ("fdisj", @{const_name Metis.fdisj})),
-   ("c_implies", ("fimplies", @{const_name Metis.fimplies})),
-   ("equal", ("fequal", @{const_name Metis.fequal}))]
+  [("c_False", (@{const_name False}, ("fFalse", @{const_name Metis.fFalse}))),
+   ("c_True", (@{const_name True}, ("fTrue", @{const_name Metis.fTrue}))),
+   ("c_Not", (@{const_name Not}, ("fNot", @{const_name Metis.fNot}))),
+   ("c_conj", (@{const_name conj}, ("fconj", @{const_name Metis.fconj}))),
+   ("c_disj", (@{const_name disj}, ("fdisj", @{const_name Metis.fdisj}))),
+   ("c_implies", (@{const_name implies},
+                  ("fimplies", @{const_name Metis.fimplies}))),
+   ("equal", (@{const_name HOL.eq}, ("fequal", @{const_name Metis.fequal})))]
+
+val proxify_const = AList.lookup (op =) metis_proxies #> Option.map snd
 
 (* Readable names for the more common symbolic functions. Do not mess with the
    table unless you know what you are doing. *)
@@ -130,25 +133,20 @@
    (@{const_name Meson.COMBK}, "COMBK"),
    (@{const_name Meson.COMBB}, "COMBB"),
    (@{const_name Meson.COMBC}, "COMBC"),
-   (@{const_name Meson.COMBS}, "COMBS")] @
-   (metis_proxies |> map (swap o snd))
+   (@{const_name Meson.COMBS}, "COMBS")]
   |> Symtab.make
+  |> fold (Symtab.update o swap o snd o snd) metis_proxies
 
-(* Invert the table of translations between Isabelle and ATPs. *)
-val const_trans_table_safe_inv =
+(* Invert the table of translations between Isabelle and Metis. *)
+val const_trans_table_inv =
   const_trans_table |> Symtab.dest |> map swap |> Symtab.make
-val const_trans_table_inv =
-  const_trans_table_safe_inv
-  |> fold Symtab.update [("fFalse", @{const_name False}),
-                         ("fTrue", @{const_name True}),
-                         ("fNot", @{const_name Not}),
-                         ("fconj", @{const_name conj}),
-                         ("fdisj", @{const_name disj}),
-                         ("fimplies", @{const_name implies}),
-                         ("fequal", @{const_name HOL.eq})]
+val const_trans_table_unprox =
+  Symtab.empty
+  |> fold (fn (_, (isa, (_, meson))) => Symtab.update (meson, isa))
+          metis_proxies
 
-val safe_invert_const = perhaps (Symtab.lookup const_trans_table_safe_inv)
 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
+val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
 
 (*Escaping of special characters.
   Alphanumeric characters are left unchanged.
@@ -398,41 +396,32 @@
 (* Converts a term (with combinators) into a combterm. Also accumulates sort
    infomation. *)
 fun combterm_from_term thy bs (P $ Q) =
-      let
-        val (P', P_atomics_Ts) = combterm_from_term thy bs P
-        val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
-      in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
+    let
+      val (P', P_atomics_Ts) = combterm_from_term thy bs P
+      val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
+    in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
   | combterm_from_term thy _ (Const (c, T)) =
-      let
-        val tvar_list =
-          (if String.isPrefix old_skolem_const_prefix c then
-             [] |> Term.add_tvarsT T |> map TVar
-           else
-             (c, T) |> Sign.const_typargs thy)
-        val c' = CombConst (`make_fixed_const c, T, tvar_list)
-      in (c', atyps_of T) end
+    let
+      val tvar_list =
+        (if String.isPrefix old_skolem_const_prefix c then
+           [] |> Term.add_tvarsT T |> map TVar
+         else
+           (c, T) |> Sign.const_typargs thy)
+      val c' = CombConst (`make_fixed_const c, T, tvar_list)
+    in (c', atyps_of T) end
   | combterm_from_term _ _ (Free (v, T)) =
-      let
-        val at = atyps_of T
-        val v' = CombConst (`make_fixed_var v, T, [])
-      in (v', atyps_of T) end
+    (CombConst (`make_fixed_var v, T, []), atyps_of T)
   | combterm_from_term _ _ (Var (v as (s, _), T)) =
-    let
-      val v' =
-        if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
-          let
-            val Ts = T |> strip_type |> swap |> op ::
-            val s' = new_skolem_const_name s (length Ts)
-          in CombConst (`make_fixed_const s', T, Ts) end
-        else
-          CombVar ((make_schematic_var v, s), T)
-    in (v', atyps_of T) end
+    (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
+       let
+         val Ts = T |> strip_type |> swap |> op ::
+         val s' = new_skolem_const_name s (length Ts)
+       in CombConst (`make_fixed_const s', T, Ts) end
+     else
+       CombVar ((make_schematic_var v, s), T), atyps_of T)
   | combterm_from_term _ bs (Bound j) =
-      let
-        val (s, T) = nth bs j
-        val ts = atyps_of T
-        val v' = CombConst (`make_bound_var s, T, [])
-      in (v', atyps_of T) end
+    nth bs j
+    |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
   | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
 
 fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
diff -r 5737947e4c77 -r 77f94ac04f32 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
@@ -383,6 +383,7 @@
                           (b, map (typ_from_fo_term tfrees) type_us)
                     else
                       HOLogic.typeT
+                val b = unproxify_const b
               in list_comb (Const (b, T), term_ts @ extra_ts) end
           end
         | NONE => (* a free or schematic variable *)
diff -r 5737947e4c77 -r 77f94ac04f32 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
@@ -226,7 +226,7 @@
     fun aux top_level (CombApp (tm1, tm2)) =
         CombApp (aux top_level tm1, aux false tm2)
       | aux top_level (CombConst (name as (s, s'), ty, ty_args)) =
-        (case AList.lookup (op =) metis_proxies s of
+        (case proxify_const s of
            SOME proxy_base =>
            if top_level then
              (case s of
@@ -419,8 +419,7 @@
            t |> (general_type_arg_policy type_sys = Mangled_Types andalso
                  not (null (Term.hidden_polymorphism t)))
                 ? (case typ of
-                     SOME T =>
-                     specialize_type thy (safe_invert_const unmangled_s, T)
+                     SOME T => specialize_type thy (invert_const unmangled_s, T)
                    | NONE => I)
          end)
       fun make_facts eq_as_iff =
@@ -477,7 +476,7 @@
         (case strip_prefix_and_unascii const_prefix s of
            NONE => (name, ty_args)
          | SOME s'' =>
-           let val s'' = safe_invert_const s'' in
+           let val s'' = invert_const s'' in
              case type_arg_policy type_sys s'' of
                No_Type_Args => (name, [])
              | Mangled_Types => (mangled_const_name ty_args name, [])
@@ -682,7 +681,7 @@
   | NONE =>
     case strip_prefix_and_unascii const_prefix s of
       SOME s =>
-      let val s = s |> unmangled_const_name |> safe_invert_const in
+      let val s = s |> unmangled_const_name |> invert_const in
         if s = predicator_base then 1
         else if s = explicit_app_base then 2
         else if s = type_pred_base then 1