115 fun get_indices callers t = |
115 fun get_indices callers t = |
116 callers |
116 callers |
117 |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE) |
117 |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE) |
118 |> map_filter I; |
118 |> map_filter I; |
119 |
119 |
120 fun mutualize_fp_sugars plugins fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy = |
120 fun mutualize_fp_sugars plugins fp mutual_cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy = |
121 let |
121 let |
122 val thy = Proof_Context.theory_of no_defs_lthy; |
122 val thy = Proof_Context.theory_of no_defs_lthy; |
123 |
123 |
124 val qsotm = quote o Syntax.string_of_term no_defs_lthy; |
124 val qsotm = quote o Syntax.string_of_term no_defs_lthy; |
125 |
125 |
238 |
238 |
239 val fp_absT_infos = map #absT_info fp_sugars0; |
239 val fp_absT_infos = map #absT_info fp_sugars0; |
240 |
240 |
241 val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct, |
241 val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct, |
242 dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) = |
242 dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) = |
243 fp_bnf (construct_mutualized_fp fp cliques unsorted_fpTs fp_sugars0) fp_bs unsorted_As' |
243 fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs fp_sugars0) fp_bs |
244 killed_As' fp_eqs no_defs_lthy; |
244 unsorted_As' killed_As' fp_eqs no_defs_lthy; |
245 |
245 |
246 val fp_abs_inverses = map #abs_inverse fp_absT_infos; |
246 val fp_abs_inverses = map #abs_inverse fp_absT_infos; |
247 val fp_type_definitions = map #type_definition fp_absT_infos; |
247 val fp_type_definitions = map #type_definition fp_absT_infos; |
248 |
248 |
249 val abss = map #abs absT_infos; |
249 val abss = map #abs absT_infos; |
419 gather_types lthy' rho' (mutual_Ts :: rev_seens) (gen_seen' @ gen_mutual_Ts) Ts' |
419 gather_types lthy' rho' (mutual_Ts :: rev_seens) (gen_seen' @ gen_mutual_Ts) Ts' |
420 end |
420 end |
421 | gather_types _ _ _ _ (T :: _) = not_co_datatype T; |
421 | gather_types _ _ _ _ (T :: _) = not_co_datatype T; |
422 |
422 |
423 val (perm_Tss, perm_gen_Ts) = gather_types lthy [] [] [] sorted_actual_Ts; |
423 val (perm_Tss, perm_gen_Ts) = gather_types lthy [] [] [] sorted_actual_Ts; |
424 val (perm_cliques, perm_Ts) = |
424 val (perm_mutual_cliques, perm_Ts) = |
425 split_list (flat (map_index (fn (i, perm_Ts) => map (pair i) perm_Ts) perm_Tss)); |
425 split_list (flat (map_index (fn (i, perm_Ts) => map (pair i) perm_Ts) perm_Tss)); |
426 |
426 |
427 val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts; |
427 val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts; |
428 |
428 |
429 val missing_Ts = fold (remove1 (op =)) actual_Ts perm_Ts; |
429 val missing_Ts = fold (remove1 (op =)) actual_Ts perm_Ts; |
439 val callers = pad_list impossible_caller nn actual_callers; |
439 val callers = pad_list impossible_caller nn actual_callers; |
440 |
440 |
441 fun permute xs = permute_like (op =) Ts perm_Ts xs; |
441 fun permute xs = permute_like (op =) Ts perm_Ts xs; |
442 fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs; |
442 fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs; |
443 |
443 |
444 (* The assignment of callers to cliques is incorrect in general. This code would need to inspect |
444 (* The assignment of callers to mutual cliques is incorrect in general. This code would need to |
445 the actual calls to discover the correct cliques in the presence of type duplicates. However, |
445 inspect the actual calls to discover the correct cliques in the presence of type duplicates. |
446 the naive scheme implemented here supports "prim(co)rec" specifications following reasonable |
446 However, the naive scheme implemented here supports "prim(co)rec" specifications following |
447 ordering of the duplicates (e.g., keeping the cliques together). *) |
447 reasonable ordering of the duplicates (e.g., keeping the cliques together). *) |
448 val perm_bs = permute bs; |
448 val perm_bs = permute bs; |
449 val perm_callers = permute callers; |
449 val perm_callers = permute callers; |
450 val perm_kks = permute kks; |
450 val perm_kks = permute kks; |
451 val perm_callssss0 = permute callssss0; |
451 val perm_callssss0 = permute callssss0; |
452 val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts; |
452 val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts; |
455 |
455 |
456 val ((perm_fp_sugars, fp_sugar_thms), lthy) = |
456 val ((perm_fp_sugars, fp_sugar_thms), lthy) = |
457 if length perm_Tss = 1 then |
457 if length perm_Tss = 1 then |
458 ((perm_fp_sugars0, (NONE, NONE)), lthy) |
458 ((perm_fp_sugars0, (NONE, NONE)), lthy) |
459 else |
459 else |
460 mutualize_fp_sugars plugins fp perm_cliques perm_bs perm_frozen_gen_Ts perm_callers |
460 mutualize_fp_sugars plugins fp perm_mutual_cliques perm_bs perm_frozen_gen_Ts perm_callers |
461 perm_callssss perm_fp_sugars0 lthy; |
461 perm_callssss perm_fp_sugars0 lthy; |
462 |
462 |
463 val fp_sugars = unpermute perm_fp_sugars; |
463 val fp_sugars = unpermute perm_fp_sugars; |
464 in |
464 in |
465 ((missing_Ts, perm_kks, fp_sugars, fp_sugar_thms), lthy) |
465 ((missing_Ts, perm_kks, fp_sugars, fp_sugar_thms), lthy) |