104 | is_type_system_sound No_Types = false |
104 | is_type_system_sound No_Types = false |
105 |
105 |
106 fun type_system_types_dangerous_types (Tags _) = true |
106 fun type_system_types_dangerous_types (Tags _) = true |
107 | type_system_types_dangerous_types type_sys = is_type_system_sound type_sys |
107 | type_system_types_dangerous_types type_sys = is_type_system_sound type_sys |
108 |
108 |
109 fun dont_need_type_args type_sys s = |
109 val boring_consts = [explicit_app_base, @{const_name Metis.fequal}] |
|
110 |
|
111 fun should_omit_type_args type_sys s = |
110 s <> type_pred_base andalso |
112 s <> type_pred_base andalso |
111 (member (op =) [@{const_name HOL.eq}] s orelse |
113 (s = @{const_name HOL.eq} orelse |
112 case type_sys of |
114 case type_sys of |
113 Many_Typed => false |
115 Many_Typed => false |
114 | Mangled _ => false |
116 | Mangled _ => false |
115 | Args _ => s = explicit_app_base |
117 | No_Types => true |
116 | Tags full_types => full_types orelse s = explicit_app_base |
118 | Tags true => true |
117 | No_Types => true) |
119 | _ => member (op =) boring_consts s) |
118 |
120 |
119 datatype type_arg_policy = No_Type_Args | Mangled_Types | Explicit_Type_Args |
121 datatype type_arg_policy = No_Type_Args | Mangled_Types | Explicit_Type_Args |
120 |
122 |
121 fun general_type_arg_policy Many_Typed = Mangled_Types |
123 fun general_type_arg_policy Many_Typed = Mangled_Types |
122 | general_type_arg_policy (Mangled _) = Mangled_Types |
124 | general_type_arg_policy (Mangled _) = Mangled_Types |
123 | general_type_arg_policy _ = Explicit_Type_Args |
125 | general_type_arg_policy _ = Explicit_Type_Args |
124 |
126 |
125 fun type_arg_policy type_sys s = |
127 fun type_arg_policy type_sys s = |
126 if dont_need_type_args type_sys s then No_Type_Args |
128 if should_omit_type_args type_sys s then No_Type_Args |
127 else general_type_arg_policy type_sys |
129 else general_type_arg_policy type_sys |
128 |
130 |
129 fun num_atp_type_args thy type_sys s = |
131 fun num_atp_type_args thy type_sys s = |
130 if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s |
132 if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s |
131 else 0 |
133 else 0 |