833 let val T = get_T x in |
833 let val T = get_T x in |
834 if exists (type_instance thy T o get_T) xs then xs |
834 if exists (type_instance thy T o get_T) xs then xs |
835 else x :: filter_out (type_generalization thy T o get_T) xs |
835 else x :: filter_out (type_generalization thy T o get_T) xs |
836 end |
836 end |
837 |
837 |
838 (* The Booleans indicate whether all type arguments should be kept. *) |
838 fun chop_fun 0 T = ([], T) |
839 datatype type_arg_policy = |
839 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) = |
840 All_Type_Args | |
840 chop_fun (n - 1) ran_T |>> cons dom_T |
841 Noninfer_Type_Args | |
841 | chop_fun _ T = ([], T) |
842 Constr_Infer_Type_Args | |
842 |
843 No_Type_Args |
843 fun filter_type_args thy constrs type_enc s ary T_args = |
844 |
|
845 fun type_arg_policy constrs type_enc s = |
|
846 let val poly = polymorphism_of_type_enc type_enc in |
844 let val poly = polymorphism_of_type_enc type_enc in |
847 if s = type_tag_name then (* ### FIXME: why not "type_guard_name" as well? *) |
845 if s = type_tag_name then (* ### FIXME: why not "type_guard_name" as well? *) |
848 All_Type_Args |
846 T_args |
849 else case type_enc of |
847 else case type_enc of |
850 Native (_, Raw_Polymorphic _, _) => All_Type_Args |
848 Native (_, Raw_Polymorphic _, _) => T_args |
851 | Native (_, Type_Class_Polymorphic, _) => All_Type_Args |
849 | Native (_, Type_Class_Polymorphic, _) => T_args |
852 | _ => |
850 | _ => |
853 let val level = level_of_type_enc type_enc in |
851 let |
|
852 fun gen_type_args _ _ [] = [] |
|
853 | gen_type_args keep strip_ty T_args = |
|
854 let |
|
855 val U = robust_const_type thy s |
|
856 val (binder_Us, body_U) = strip_ty U |
|
857 val in_U_vars = fold Term.add_tvarsT binder_Us [] |
|
858 val out_U_vars = Term.add_tvarsT body_U [] |
|
859 fun filt (U_var, T) = |
|
860 if keep (member (op =) in_U_vars U_var, |
|
861 member (op =) out_U_vars U_var) then |
|
862 T |
|
863 else |
|
864 dummyT |
|
865 val U_args = (s, U) |> robust_const_typargs thy |
|
866 in map (filt o apfst dest_TVar) (U_args ~~ T_args) end |
|
867 handle TYPE _ => T_args |
|
868 val noninfer_type_args = gen_type_args (not o fst) (chop_fun ary) |
|
869 val constr_infer_type_args = gen_type_args fst strip_type |
|
870 val level = level_of_type_enc type_enc |
|
871 in |
854 if level = No_Types orelse s = @{const_name HOL.eq} orelse |
872 if level = No_Types orelse s = @{const_name HOL.eq} orelse |
855 (case level of Const_Types _ => s = app_op_name | _ => false) then |
873 (case level of Const_Types _ => s = app_op_name | _ => false) then |
856 No_Type_Args |
874 [] |
857 else if poly = Mangled_Monomorphic then |
875 else if poly = Mangled_Monomorphic then |
858 All_Type_Args |
876 T_args |
859 else if level = All_Types then |
877 else if level = All_Types then |
860 case type_enc of |
878 case type_enc of |
861 Guards _ => Noninfer_Type_Args |
879 Guards _ => noninfer_type_args T_args |
862 | Tags _ => No_Type_Args |
880 | Tags _ => [] |
863 else if level = Undercover_Types then |
881 else if level = Undercover_Types then |
864 Noninfer_Type_Args |
882 noninfer_type_args T_args |
865 else if member (op =) constrs s andalso |
883 else if member (op =) constrs s andalso |
866 level <> Const_Types Without_Constr_Optim then |
884 level <> Const_Types Without_Constr_Optim then |
867 Constr_Infer_Type_Args |
885 constr_infer_type_args T_args |
868 else |
886 else |
869 All_Type_Args |
887 T_args |
870 end |
888 end |
871 end |
889 end |
872 |
890 |
873 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *) |
891 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *) |
874 val fused_infinite_type = Type (fused_infinite_type_name, []) |
892 val fused_infinite_type = Type (fused_infinite_type_name, []) |
1141 | mangle tm = tm |
1159 | mangle tm = tm |
1142 in mangle end |
1160 in mangle end |
1143 else |
1161 else |
1144 I |
1162 I |
1145 |
1163 |
1146 fun chop_fun 0 T = ([], T) |
|
1147 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) = |
|
1148 chop_fun (n - 1) ran_T |>> cons dom_T |
|
1149 | chop_fun _ T = ([], T) |
|
1150 |
|
1151 fun filter_type_args _ _ _ _ [] = [] |
|
1152 | filter_type_args keep thy s strip_ty T_args = |
|
1153 let |
|
1154 val U = robust_const_type thy s |
|
1155 val (binder_Us, body_U) = strip_ty U |
|
1156 val in_U_vars = fold Term.add_tvarsT binder_Us [] |
|
1157 val out_U_vars = Term.add_tvarsT body_U [] |
|
1158 fun filt (U_var, T) = |
|
1159 if keep (member (op =) in_U_vars U_var, |
|
1160 member (op =) out_U_vars U_var) then |
|
1161 T |
|
1162 else |
|
1163 dummyT |
|
1164 val U_args = (s, U) |> robust_const_typargs thy |
|
1165 in map (filt o apfst dest_TVar) (U_args ~~ T_args) end |
|
1166 handle TYPE _ => T_args |
|
1167 |
|
1168 fun filter_type_args_in_const _ _ _ _ _ [] = [] |
1164 fun filter_type_args_in_const _ _ _ _ _ [] = [] |
1169 | filter_type_args_in_const thy constrs type_enc ary s T_args = |
1165 | filter_type_args_in_const thy constrs type_enc ary s T_args = |
1170 case unprefix_and_unascii const_prefix s of |
1166 case unprefix_and_unascii const_prefix s of |
1171 NONE => |
1167 NONE => |
1172 if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then [] |
1168 if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then [] |
1173 else T_args |
1169 else T_args |
1174 | SOME s'' => |
1170 | SOME s'' => |
1175 let val s'' = invert_const s'' in |
1171 filter_type_args thy constrs type_enc (invert_const s'') ary T_args |
1176 case type_arg_policy constrs type_enc s'' of |
|
1177 All_Type_Args => T_args |
|
1178 | Noninfer_Type_Args => |
|
1179 filter_type_args (not o fst) thy s'' (chop_fun ary) T_args |
|
1180 | Constr_Infer_Type_Args => |
|
1181 filter_type_args fst thy s'' strip_type T_args |
|
1182 | No_Type_Args => [] |
|
1183 end |
|
1184 fun filter_type_args_in_iterm thy constrs type_enc = |
1172 fun filter_type_args_in_iterm thy constrs type_enc = |
1185 let |
1173 let |
1186 fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2) |
1174 fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2) |
1187 | filt ary (IConst (name as (s, _), T, T_args)) = |
1175 | filt ary (IConst (name as (s, _), T, T_args)) = |
1188 filter_type_args_in_const thy constrs type_enc ary s T_args |
1176 filter_type_args_in_const thy constrs type_enc ary s T_args |