# HG changeset patch
# User blanchet
# Date 1341497235 -7200
# Node ID 0e552737cc5a7199bd09ab5dc37d1588c606bd5b
# Parent  76b6207eb000a197c169e56d25eb86f1e4a43a50
remove needless type arguments to "tags_at" encoding

diff -r 76b6207eb000 -r 0e552737cc5a src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jul 05 14:13:14 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jul 05 16:07:15 2012 +0200
@@ -837,7 +837,6 @@
   Mangled_Type_Args |
   All_Type_Args |
   Not_Input_Type_Args |
-  Only_In_Or_Output_Type_Args |
   Constr_Input_Type_Args |
   No_Type_Args
 
@@ -856,12 +855,8 @@
           No_Type_Args
         else if poly = Mangled_Monomorphic then
           Mangled_Type_Args
-        else if level = All_Types then
+        else if level = All_Types orelse level = Undercover_Types then
           Not_Input_Type_Args
-        else if level = Undercover_Types then
-          case type_enc of
-            Tags _ => Only_In_Or_Output_Type_Args
-          | _ => Not_Input_Type_Args
         else if member (op =) constrs s andalso
                 level <> Const_Types Without_Constr_Optim then
           Constr_Input_Type_Args
@@ -1177,8 +1172,6 @@
         | All_Type_Args => T_args
         | Not_Input_Type_Args =>
           filter_type_args (not o fst) thy s'' (chop_fun ary) T_args
-        | Only_In_Or_Output_Type_Args =>
-          filter_type_args (op <>) thy s'' (chop_fun ary) T_args
         | Constr_Input_Type_Args =>
           filter_type_args fst thy s'' strip_type T_args
         | No_Type_Args => []
@@ -1344,20 +1337,27 @@
 
 (** Finite and infinite type inference **)
 
-fun tvar_footprint thy s ary =
+fun tvar_footprint thy body s ary =
   (case unprefix_and_unascii const_prefix s of
      SOME s =>
-     s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
-       |> map (fn T => Term.add_tvarsT T [] |> map fst)
+     let
+       val (binder_Ts, body_T) =
+         s |> invert_const |> robust_const_type thy |> chop_fun ary
+       fun tvars_of T =
+         [] |> Term.add_tvarsT T
+            |> (fn Ts => if body then Ts
+                         else subtract (op =) (Term.add_tvarsT body_T []) Ts)
+            |> map fst
+     in binder_Ts |> map tvars_of end
    | NONE => [])
   handle TYPE _ => []
 
-fun type_arg_cover thy pos s ary =
+fun type_arg_cover thy pos body s ary =
   if is_tptp_equal s then
     if pos = SOME false then [] else 0 upto ary - 1
   else
     let
-      val footprint = tvar_footprint thy s ary
+      val footprint = tvar_footprint thy body s ary
       val eq = (s = @{const_name HOL.eq})
       fun cover _ [] = []
         | cover seen ((i, tvars) :: args) =
@@ -1433,7 +1433,7 @@
         (case (site, is_maybe_universal_var u) of
            (Eq_Arg pos, true) => pos <> SOME false
          | (Arg (s, j, ary), true) =>
-           member (op =) (type_arg_cover thy NONE s ary) j
+           member (op =) (type_arg_cover thy NONE true s ary) j
          | _ => false)
       | _ => should_encode_type ctxt mono level T
     end
@@ -1998,7 +1998,7 @@
       | is_undercover (ATerm (((s, _), _), tms)) =
         let
           val ary = length tms
-          val cover = type_arg_cover thy pos s ary
+          val cover = type_arg_cover thy pos true s ary
         in
           exists (fn (j, tm) => tm = var andalso member (op =) cover j)
                  (0 upto ary - 1 ~~ tms) orelse
@@ -2420,7 +2420,7 @@
       bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
     val bound_Ts =
       if exists (curry (op =) dummyT) T_args then
-        let val cover = type_arg_cover thy NONE s ary in
+        let val cover = type_arg_cover thy NONE true s ary in
           map2 (fn j => if member (op =) cover j then SOME else K NONE)
                (0 upto ary - 1) arg_Ts
         end
@@ -2460,17 +2460,20 @@
     val add_formula_for_res =
       if should_encode res_T then
         let
-          val tagged_bounds =
+          val (lhs, rhs) =
             if level = Undercover_Types then
-              let val cover = type_arg_cover thy NONE s ary in
-                map2 (fn (j, arg_T) => member (op =) cover j ? tag_with arg_T)
-                     (0 upto ary - 1 ~~ arg_Ts) bounds
-              end
+              let
+                val lhs_cover = type_arg_cover thy NONE false s ary
+                val rhs_cover = type_arg_cover thy NONE true s ary
+                fun maybe_tag cover (j, arg_T) =
+                  member (op =) cover j ? tag_with arg_T
+                fun covered_bounds cover =
+                  map2 (maybe_tag cover) (0 upto ary - 1 ~~ arg_Ts) bounds
+              in (lhs_cover, rhs_cover) |> pairself (covered_bounds #> cst) end
             else
-              bounds
+              `I (cst bounds)
         in
-          cons (Formula (ident, role,
-                         eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
+          cons (Formula (ident, role, eq (tag_with res_T lhs) rhs,
                          NONE, isabelle_info defN helper_rank))
         end
       else