737 else x :: filter_out (type_generalization ctxt T o get_T) xs |
737 else x :: filter_out (type_generalization ctxt T o get_T) xs |
738 end |
738 end |
739 |
739 |
740 (* The Booleans indicate whether all type arguments should be kept. *) |
740 (* The Booleans indicate whether all type arguments should be kept. *) |
741 datatype type_arg_policy = |
741 datatype type_arg_policy = |
742 Explicit_Type_Args of bool | |
742 Explicit_Type_Args of bool (* infer_from_term_args *) | |
743 Mangled_Type_Args | |
743 Mangled_Type_Args | |
744 No_Type_Args |
744 No_Type_Args |
745 |
745 |
746 fun type_arg_policy type_enc s = |
746 fun type_arg_policy type_enc s = |
747 let val poly = polymorphism_of_type_enc type_enc in |
747 let val poly = polymorphism_of_type_enc type_enc in |
1031 val s'' = invert_const s'' |
1031 val s'' = invert_const s'' |
1032 fun filter_T_args false = T_args |
1032 fun filter_T_args false = T_args |
1033 | filter_T_args true = filter_const_type_args thy s'' ary T_args |
1033 | filter_T_args true = filter_const_type_args thy s'' ary T_args |
1034 in |
1034 in |
1035 case type_arg_policy type_enc s'' of |
1035 case type_arg_policy type_enc s'' of |
1036 Explicit_Type_Args drop_args => (name, filter_T_args drop_args) |
1036 Explicit_Type_Args infer_from_term_args => |
|
1037 (name, filter_T_args infer_from_term_args) |
1037 | No_Type_Args => (name, []) |
1038 | No_Type_Args => (name, []) |
1038 | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol" |
1039 | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol" |
1039 end) |
1040 end) |
1040 |> (fn (name, T_args) => IConst (name, T, T_args)) |
1041 |> (fn (name, T_args) => IConst (name, T, T_args)) |
1041 | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm) |
1042 | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm) |
2414 lam_trans |
2415 lam_trans |
2415 val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses, |
2416 val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses, |
2416 lifted) = |
2417 lifted) = |
2417 translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts |
2418 translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts |
2418 concl_t facts |
2419 concl_t facts |
2419 val sym_tab = |
2420 val sym_tab = sym_table_for_facts ctxt type_enc explicit_apply conjs facts |
2420 sym_table_for_facts ctxt type_enc explicit_apply conjs facts |
|
2421 val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc |
2421 val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc |
2422 val firstorderize = firstorderize_fact thy format type_enc sym_tab |
2422 val firstorderize = firstorderize_fact thy format type_enc sym_tab |
2423 val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize) |
2423 val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize) |
2424 val sym_tab = sym_table_for_facts ctxt type_enc (SOME false) conjs facts |
2424 val sym_tab = sym_table_for_facts ctxt type_enc (SOME false) conjs facts |
2425 val helpers = |
2425 val helpers = |
2426 sym_tab |> helper_facts_for_sym_table ctxt format type_enc |
2426 sym_tab |> helper_facts_for_sym_table ctxt format type_enc |
2427 |> map firstorderize |
2427 |> map firstorderize |
2428 val mono_Ts = |
2428 val mono_Ts = |
2429 helpers @ conjs @ facts |
2429 helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc |
2430 |> monotonic_types_for_facts ctxt mono type_enc |
|
2431 val class_decl_lines = decl_lines_for_classes type_enc classes |
2430 val class_decl_lines = decl_lines_for_classes type_enc classes |
2432 val sym_decl_lines = |
2431 val sym_decl_lines = |
2433 (conjs, helpers @ facts) |
2432 (conjs, helpers @ facts) |
2434 |> sym_decl_table_for_facts ctxt format type_enc sym_tab |
2433 |> sym_decl_table_for_facts ctxt format type_enc sym_tab |
2435 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono |
2434 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono |