1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jul 05 16:15:52 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jul 05 16:30:50 2012 +0200
     1.3 @@ -835,38 +835,56 @@
     1.4      else x :: filter_out (type_generalization thy T o get_T) xs
     1.5    end
     1.6  
     1.7 -(* The Booleans indicate whether all type arguments should be kept. *)
     1.8 -datatype type_arg_policy =
     1.9 -  All_Type_Args |
    1.10 -  Noninfer_Type_Args |
    1.11 -  Constr_Infer_Type_Args |
    1.12 -  No_Type_Args
    1.13 +fun chop_fun 0 T = ([], T)
    1.14 +  | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
    1.15 +    chop_fun (n - 1) ran_T |>> cons dom_T
    1.16 +  | chop_fun _ T = ([], T)
    1.17  
    1.18 -fun type_arg_policy constrs type_enc s =
    1.19 +fun filter_type_args thy constrs type_enc s ary T_args =
    1.20    let val poly = polymorphism_of_type_enc type_enc in
    1.21      if s = type_tag_name then (* ### FIXME: why not "type_guard_name" as well? *)
    1.22 -      All_Type_Args
    1.23 +      T_args
    1.24      else case type_enc of
    1.25 -      Native (_, Raw_Polymorphic _, _) => All_Type_Args
    1.26 -    | Native (_, Type_Class_Polymorphic, _) => All_Type_Args
    1.27 +      Native (_, Raw_Polymorphic _, _) => T_args
    1.28 +    | Native (_, Type_Class_Polymorphic, _) => T_args
    1.29      | _ =>
    1.30 -      let val level = level_of_type_enc type_enc in
    1.31 +      let
    1.32 +        fun gen_type_args _ _ [] = []
    1.33 +          | gen_type_args keep strip_ty T_args =
    1.34 +            let
    1.35 +              val U = robust_const_type thy s
    1.36 +              val (binder_Us, body_U) = strip_ty U
    1.37 +              val in_U_vars = fold Term.add_tvarsT binder_Us []
    1.38 +              val out_U_vars = Term.add_tvarsT body_U []
    1.39 +              fun filt (U_var, T) =
    1.40 +                if keep (member (op =) in_U_vars U_var,
    1.41 +                         member (op =) out_U_vars U_var) then
    1.42 +                  T
    1.43 +                else
    1.44 +                  dummyT
    1.45 +              val U_args = (s, U) |> robust_const_typargs thy
    1.46 +            in map (filt o apfst dest_TVar) (U_args ~~ T_args) end
    1.47 +            handle TYPE _ => T_args
    1.48 +        val noninfer_type_args = gen_type_args (not o fst) (chop_fun ary)
    1.49 +        val constr_infer_type_args = gen_type_args fst strip_type
    1.50 +        val level = level_of_type_enc type_enc
    1.51 +      in
    1.52          if level = No_Types orelse s = @{const_name HOL.eq} orelse
    1.53             (case level of Const_Types _ => s = app_op_name | _ => false) then
    1.54 -          No_Type_Args
    1.55 +          []
    1.56          else if poly = Mangled_Monomorphic then
    1.57 -          All_Type_Args
    1.58 +          T_args
    1.59          else if level = All_Types then
    1.60            case type_enc of
    1.61 -            Guards _ => Noninfer_Type_Args
    1.62 -          | Tags _ => No_Type_Args
    1.63 +            Guards _ => noninfer_type_args T_args
    1.64 +          | Tags _ => []
    1.65          else if level = Undercover_Types then
    1.66 -          Noninfer_Type_Args
    1.67 +          noninfer_type_args T_args
    1.68          else if member (op =) constrs s andalso
    1.69                  level <> Const_Types Without_Constr_Optim then
    1.70 -          Constr_Infer_Type_Args
    1.71 +          constr_infer_type_args T_args
    1.72          else
    1.73 -          All_Type_Args
    1.74 +          T_args
    1.75        end
    1.76    end
    1.77  
    1.78 @@ -1143,28 +1161,6 @@
    1.79    else
    1.80      I
    1.81  
    1.82 -fun chop_fun 0 T = ([], T)
    1.83 -  | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
    1.84 -    chop_fun (n - 1) ran_T |>> cons dom_T
    1.85 -  | chop_fun _ T = ([], T)
    1.86 -
    1.87 -fun filter_type_args _ _ _ _ [] = []
    1.88 -  | filter_type_args keep thy s strip_ty T_args =
    1.89 -    let
    1.90 -      val U = robust_const_type thy s
    1.91 -      val (binder_Us, body_U) = strip_ty U
    1.92 -      val in_U_vars = fold Term.add_tvarsT binder_Us []
    1.93 -      val out_U_vars = Term.add_tvarsT body_U []
    1.94 -      fun filt (U_var, T) =
    1.95 -        if keep (member (op =) in_U_vars U_var,
    1.96 -                 member (op =) out_U_vars U_var) then
    1.97 -          T
    1.98 -        else
    1.99 -          dummyT
   1.100 -      val U_args = (s, U) |> robust_const_typargs thy
   1.101 -    in map (filt o apfst dest_TVar) (U_args ~~ T_args) end
   1.102 -    handle TYPE _ => T_args
   1.103 -
   1.104  fun filter_type_args_in_const _ _ _ _ _ [] = []
   1.105    | filter_type_args_in_const thy constrs type_enc ary s T_args =
   1.106      case unprefix_and_unascii const_prefix s of
   1.107 @@ -1172,15 +1168,7 @@
   1.108        if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
   1.109        else T_args
   1.110      | SOME s'' =>
   1.111 -      let val s'' = invert_const s'' in
   1.112 -        case type_arg_policy constrs type_enc s'' of
   1.113 -          All_Type_Args => T_args
   1.114 -        | Noninfer_Type_Args =>
   1.115 -          filter_type_args (not o fst) thy s'' (chop_fun ary) T_args
   1.116 -        | Constr_Infer_Type_Args =>
   1.117 -          filter_type_args fst thy s'' strip_type T_args
   1.118 -        | No_Type_Args => []
   1.119 -      end
   1.120 +      filter_type_args thy constrs type_enc (invert_const s'') ary T_args
   1.121  fun filter_type_args_in_iterm thy constrs type_enc =
   1.122    let
   1.123      fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)