# HG changeset patch
# User blanchet
# Date 1315379441 -7200
# Node ID 72785558a6fff38ecbe51bb65971672bff99f332
# Parent  e701dabbfe37871861731c85174c67a6484222f0
separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed

diff -r e701dabbfe37 -r 72785558a6ff src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 09:10:41 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 09:10:41 2011 +0200
@@ -710,23 +710,22 @@
     level_of_type_enc type_enc = All_Types
 
 fun type_arg_policy type_enc s =
-  if s = type_tag_name then
-    if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
-      Mangled_Type_Args
-    else
-      Explicit_Type_Args false
-  else case type_enc of
-    Tags (_, All_Types) => No_Type_Args
-  | _ =>
-    let val level = level_of_type_enc type_enc in
-      if level = No_Types orelse s = @{const_name HOL.eq} orelse
-         (s = app_op_name andalso level = Const_Arg_Types) then
-        No_Type_Args
-      else if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
-        Mangled_Type_Args
-      else
-        Explicit_Type_Args (should_drop_arg_type_args type_enc)
-    end
+  let val mangled = (polymorphism_of_type_enc type_enc = Mangled_Monomorphic) in
+    if s = type_tag_name then
+      if mangled then Mangled_Type_Args else Explicit_Type_Args false
+    else case type_enc of
+      Tags (_, All_Types) => No_Type_Args
+    | _ =>
+      let val level = level_of_type_enc type_enc in
+        if level = No_Types orelse s = @{const_name HOL.eq} orelse
+           (s = app_op_name andalso level = Const_Arg_Types) then
+          No_Type_Args
+        else if mangled then
+          Mangled_Type_Args
+        else
+          Explicit_Type_Args (should_drop_arg_type_args type_enc)
+      end
+  end
 
 (* Make atoms for sorted type variables. *)
 fun generic_add_sorts_on_type (_, []) = I
@@ -955,13 +954,32 @@
       | intro _ _ tm = tm
   in intro true [] end
 
+fun mangle_type_args_in_iterm format type_enc =
+  if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
+    let
+      fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
+        | mangle (tm as IConst (_, _, [])) = tm
+        | mangle (tm as IConst (name as (s, _), T, T_args)) =
+          (case strip_prefix_and_unascii const_prefix s of
+             NONE => tm
+           | SOME s'' =>
+             case type_arg_policy type_enc (invert_const s'') of
+               Mangled_Type_Args =>
+               IConst (mangled_const_name format type_enc T_args name, T, [])
+             | _ => tm)
+        | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
+        | mangle tm = tm
+    in mangle end
+  else
+    I
+
 fun chop_fun 0 T = ([], T)
   | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
     chop_fun (n - 1) ran_T |>> cons dom_T
   | chop_fun _ T = ([], T)
 
-fun filter_type_args _ _ _ [] = []
-  | filter_type_args thy s ary T_args =
+fun filter_const_type_args _ _ _ [] = []
+  | filter_const_type_args thy s ary T_args =
     let
       val U = robust_const_type thy s
       val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
@@ -973,31 +991,33 @@
     end
     handle TYPE _ => T_args
 
-fun enforce_type_arg_policy_in_iterm ctxt format type_enc =
+fun filter_type_args_in_iterm thy type_enc =
   let
-    val thy = Proof_Context.theory_of ctxt
-    fun aux ary (IApp (tm1, tm2)) = IApp (aux (ary + 1) tm1, aux 0 tm2)
-      | aux ary (IConst (name as (s, _), T, T_args)) =
+    fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
+      | filt _ (tm as IConst (_, _, [])) = tm
+      | filt ary (IConst (name as (s, _), T, T_args)) =
         (case strip_prefix_and_unascii const_prefix s of
            NONE =>
-           (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice
-                  then [] else T_args)
+           (name,
+            if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
+              []
+            else
+              T_args)
          | SOME s'' =>
            let
              val s'' = invert_const s''
              fun filter_T_args false = T_args
-               | filter_T_args true = filter_type_args thy s'' ary T_args
+               | filter_T_args true = filter_const_type_args thy s'' ary T_args
            in
              case type_arg_policy type_enc s'' of
                Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
-             | Mangled_Type_Args =>
-               (mangled_const_name format type_enc T_args name, [])
              | No_Type_Args => (name, [])
+             | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
            end)
         |> (fn (name, T_args) => IConst (name, T, T_args))
-      | aux _ (IAbs (bound, tm)) = IAbs (bound, aux 0 tm)
-      | aux _ tm = tm
-  in aux 0 end
+      | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
+      | filt _ tm = tm
+  in filt 0 end
 
 fun iformula_from_prop ctxt format type_enc eq_as_iff =
   let
@@ -1005,7 +1025,7 @@
     fun do_term bs t atomic_types =
       iterm_from_term thy format bs (Envir.eta_contract t)
       |>> (introduce_proxies_in_iterm type_enc
-           #> enforce_type_arg_policy_in_iterm ctxt format type_enc
+           #> mangle_type_args_in_iterm format type_enc
            #> AAtom)
       ||> union (op =) atomic_types
     fun do_quant bs q pos s T t' =
@@ -1393,7 +1413,7 @@
 fun list_app head args = fold (curry (IApp o swap)) args head
 fun predicator tm = IApp (predicator_combconst, tm)
 
-fun firstorderize_fact ctxt format type_enc sym_tab =
+fun firstorderize_fact thy format type_enc sym_tab =
   let
     fun do_app arg head =
       let
@@ -1401,7 +1421,7 @@
         val (arg_T, res_T) = dest_funT head_T
         val app =
           IConst (app_op, head_T --> head_T, [arg_T, res_T])
-          |> enforce_type_arg_policy_in_iterm ctxt format type_enc
+          |> mangle_type_args_in_iterm format type_enc
       in list_app app [head, arg] end
     fun list_app_ops head args = fold do_app args head
     fun introduce_app_ops tm =
@@ -1420,6 +1440,7 @@
     val do_iterm =
       not (is_type_enc_higher_order type_enc)
       ? (introduce_app_ops #> introduce_predicators)
+      #> filter_type_args_in_iterm thy type_enc
   in update_iformula (formula_map do_iterm) end
 
 (** Helper facts **)
@@ -1621,9 +1642,9 @@
 
 val type_guard = `(make_fixed_const NONE) type_guard_name
 
-fun type_guard_iterm ctxt format type_enc T tm =
+fun type_guard_iterm format type_enc T tm =
   IApp (IConst (type_guard, T --> @{typ bool}, [T])
-        |> enforce_type_arg_policy_in_iterm ctxt format type_enc, tm)
+        |> mangle_type_args_in_iterm format type_enc, tm)
 
 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
   | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
@@ -1644,7 +1665,7 @@
 
 fun tag_with_type ctxt format mono type_enc pos T tm =
   IConst (type_tag, T --> T, [T])
-  |> enforce_type_arg_policy_in_iterm ctxt format type_enc
+  |> mangle_type_args_in_iterm format type_enc
   |> ho_term_from_iterm ctxt format mono type_enc (Top_Level pos)
   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
        | _ => raise Fail "unexpected lambda-abstraction")
@@ -1692,7 +1713,7 @@
       if should_guard_type ctxt mono type_enc
              (fn () => should_guard_var pos phi universal name) T then
         IVar (name, T)
-        |> type_guard_iterm ctxt format type_enc T
+        |> type_guard_iterm format type_enc T
         |> do_term pos |> AAtom |> SOME
       else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
         let
@@ -1950,7 +1971,7 @@
            ascii_of (mangled_type format type_enc T),
            Axiom,
            IConst (`make_bound_var "X", T, [])
-           |> type_guard_iterm ctxt format type_enc T
+           |> type_guard_iterm format type_enc T
            |> AAtom
            |> formula_from_iformula ctxt format mono type_enc
                                     (K (K (K (K true)))) (SOME true)
@@ -2026,7 +2047,7 @@
              (if n > 1 then "_" ^ string_of_int j else ""), kind,
              IConst ((s, s'), T, T_args)
              |> fold (curry (IApp o swap)) bounds
-             |> type_guard_iterm ctxt format type_enc res_T
+             |> type_guard_iterm format type_enc res_T
              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
              |> formula_from_iformula ctxt format mono type_enc
                                       (K (K (K (K true)))) (SOME true)
@@ -2156,6 +2177,7 @@
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
         lambda_trans readable_names preproc hyp_ts concl_t facts =
   let
+    val thy = Proof_Context.theory_of ctxt
     val type_enc = type_enc |> adjust_type_enc format
     val lambda_trans =
       if lambda_trans = smartN then
@@ -2189,7 +2211,7 @@
                          hyp_ts concl_t facts
     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
     val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
-    val firstorderize = firstorderize_fact ctxt format type_enc sym_tab
+    val firstorderize = firstorderize_fact thy format type_enc sym_tab
     val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt (SOME false)
     val helpers =