344 (* Important messages are important but not so important that users want to see |
344 (* Important messages are important but not so important that users want to see |
345 them each time. *) |
345 them each time. *) |
346 val atp_important_message_keep_quotient = 10 |
346 val atp_important_message_keep_quotient = 10 |
347 |
347 |
348 val fallback_best_type_systems = |
348 val fallback_best_type_systems = |
349 [Preds (Polymorphic, Const_Arg_Types), Many_Typed All_Types] |
349 [Preds (Polymorphic, Const_Arg_Types), Simple All_Types] |
350 |
350 |
351 fun adjust_dumb_type_sys formats (Many_Typed level) = |
351 fun adjust_dumb_type_sys formats (Simple level) = |
352 if member (op =) formats Tff then (Tff, Many_Typed level) |
352 if member (op =) formats Tff then (Tff, Simple level) |
353 else (Fof, Preds (Mangled_Monomorphic, level)) |
353 else (Fof, Preds (Mangled_Monomorphic, level)) |
354 | adjust_dumb_type_sys formats type_sys = |
354 | adjust_dumb_type_sys formats type_sys = |
355 if member (op =) formats Fof then (Fof, type_sys) |
355 if member (op =) formats Fof then (Fof, type_sys) |
356 else (Tff, Many_Typed (level_of_type_sys type_sys)) |
356 else (Tff, Simple (level_of_type_sys type_sys)) |
357 fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = |
357 fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = |
358 adjust_dumb_type_sys formats type_sys |
358 adjust_dumb_type_sys formats type_sys |
359 | determine_format_and_type_sys best_type_systems formats |
359 | determine_format_and_type_sys best_type_systems formats |
360 (Smart_Type_Sys full_types) = |
360 (Smart_Type_Sys full_types) = |
361 map type_sys_from_string best_type_systems @ fallback_best_type_systems |
361 map type_sys_from_string best_type_systems @ fallback_best_type_systems |