86 fun get_indices_checked call = |
86 fun get_indices_checked call = |
87 (case get_indices call of |
87 (case get_indices call of |
88 _ :: _ :: _ => heterogeneous_call call |
88 _ :: _ :: _ => heterogeneous_call call |
89 | kks => kks); |
89 | kks => kks); |
90 |
90 |
91 fun freeze_fp calls (T as Type (s, Ts)) = |
91 fun freeze_fp_map callss s Ts = |
|
92 Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] |
|
93 (transpose callss)) Ts) |
|
94 and freeze_fp calls (T as Type (s, Ts)) = |
92 (case map_filter (try (snd o dest_map no_defs_lthy s)) calls of |
95 (case map_filter (try (snd o dest_map no_defs_lthy s)) calls of |
93 [] => |
96 [] => |
94 (case union (op = o pairself fst) |
97 (case map_filter (try (snd o dest_map no_defs_lthy s o fst o dest_comb)) calls of |
95 (maps (fn call => map (rpair call) (get_indices_checked call)) calls) [] of |
98 [] => |
96 [] => freeze_fp_default T |
99 (case union (op = o pairself fst) |
97 | [(kk, _)] => nth Xs kk |
100 (maps (fn call => map (rpair call) (get_indices_checked call)) calls) [] of |
98 | (_, call1) :: (_, call2) :: _ => incompatible_calls call1 call2) |
101 [] => freeze_fp_default T |
99 | callss => |
102 | [(kk, _)] => nth Xs kk |
100 Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] |
103 | (_, call1) :: (_, call2) :: _ => incompatible_calls call1 call2) |
101 (transpose callss)) Ts)) |
104 | callss => freeze_fp_map callss s Ts) |
|
105 | callss => freeze_fp_map callss s Ts) |
102 | freeze_fp _ T = T; |
106 | freeze_fp _ T = T; |
103 |
107 |
104 val ctr_Tsss = map (map binder_types) ctr_Tss; |
108 val ctr_Tsss = map (map binder_types) ctr_Tss; |
105 val ctrXs_Tsss = map2 (map2 (map2 freeze_fp)) callssss ctr_Tsss; |
109 val ctrXs_Tsss = map2 (map2 (map2 freeze_fp)) callssss ctr_Tsss; |
106 val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; |
110 val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; |