34 fp_co_induct_sugar = {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) = |
34 fp_co_induct_sugar = {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) = |
35 {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, |
35 {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, |
36 recx = recx, rec_thms = rec_thms}; |
36 recx = recx, rec_thms = rec_thms}; |
37 |
37 |
38 fun basic_lfp_sugars_of _ [@{typ nat}] _ _ lthy = |
38 fun basic_lfp_sugars_of _ [@{typ nat}] _ _ lthy = |
39 ([], [0], [nat_basic_lfp_sugar], [], [], TrueI (*dummy*), [], false, lthy) |
39 ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, lthy) |
40 | basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 = |
40 | basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 = |
41 let |
41 let |
42 val ((missing_arg_Ts, perm0_kks, |
42 val ((missing_arg_Ts, perm0_kks, |
43 fp_sugars as {fp_nesting_bnfs, |
43 fp_sugars as {fp_nesting_bnfs, |
44 fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _, |
44 fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _, |
61 val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) fp_sugars; |
61 val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) fp_sugars; |
62 val fun_arg_Tssss = map (map (map zip_XrecT)) ctrXs_Tsss; |
62 val fun_arg_Tssss = map (map (map zip_XrecT)) ctrXs_Tsss; |
63 |
63 |
64 val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs; |
64 val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs; |
65 val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs; |
65 val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs; |
|
66 val fp_nesting_pred_maps = map pred_map_of_bnf fp_nesting_bnfs; |
66 in |
67 in |
67 (missing_arg_Ts, perm0_kks, @{map 3} basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars, |
68 (missing_arg_Ts, perm0_kks, @{map 3} basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars, |
68 fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, induct_attrs, |
69 fp_nesting_map_ident0s, fp_nesting_map_comps, fp_nesting_pred_maps, common_induct, |
69 is_some lfp_sugar_thms, lthy) |
70 induct_attrs, is_some lfp_sugar_thms, lthy) |
70 end; |
71 end; |
71 |
72 |
72 exception NO_MAP of term; |
73 exception NO_MAP of term; |
73 |
74 |
74 fun ill_formed_rec_call ctxt t = |
75 fun ill_formed_rec_call ctxt t = |
106 val map' = mk_map (length fs) Us ran_Ts map0; |
107 val map' = mk_map (length fs) Us ran_Ts map0; |
107 val fs' = map_flattened_map_args ctxt s (@{map 3} massage_map_or_map_arg Us Ts) fs; |
108 val fs' = map_flattened_map_args ctxt s (@{map 3} massage_map_or_map_arg Us Ts) fs; |
108 in |
109 in |
109 Term.list_comb (map', fs') |
110 Term.list_comb (map', fs') |
110 end |
111 end |
111 | NONE => raise NO_MAP t) |
112 | NONE => |
|
113 (case try (dest_pred ctxt s) t of |
|
114 SOME (pred0, fs) => |
|
115 let |
|
116 val pred' = mk_pred Us pred0; |
|
117 val fs' = map_flattened_map_args ctxt s (@{map 3} massage_map_or_map_arg Us Ts) fs; |
|
118 in |
|
119 Term.list_comb (pred', fs') |
|
120 end |
|
121 | NONE => raise NO_MAP t)) |
112 | massage_map _ _ t = raise NO_MAP t |
122 | massage_map _ _ t = raise NO_MAP t |
113 and massage_map_or_map_arg U T t = |
123 and massage_map_or_map_arg U T t = |
114 if T = U then |
124 if T = U then |
115 tap check_no_call t |
125 tap check_no_call t |
116 else |
126 else |