114 |
114 |
115 val qsotm = quote o Syntax.string_of_term no_defs_lthy0; |
115 val qsotm = quote o Syntax.string_of_term no_defs_lthy0; |
116 |
116 |
117 fun incompatible_calls t1 t2 = |
117 fun incompatible_calls t1 t2 = |
118 error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ qsotm t1 ^ " vs. " ^ qsotm t2); |
118 error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ qsotm t1 ^ " vs. " ^ qsotm t2); |
|
119 fun nested_self_call t = |
|
120 error ("Unsupported nested self-call " ^ qsotm t); |
119 |
121 |
120 val b_names = map Binding.name_of bs; |
122 val b_names = map Binding.name_of bs; |
121 val fp_b_names = map base_name_of_typ fpTs; |
123 val fp_b_names = map base_name_of_typ fpTs; |
122 |
124 |
123 val nn = length fpTs; |
125 val nn = length fpTs; |
153 (case find_index (curry (op =) T) fpTs of |
155 (case find_index (curry (op =) T) fpTs of |
154 ~1 => Type (s, map freeze_fpTs_simple Ts) |
156 ~1 => Type (s, map freeze_fpTs_simple Ts) |
155 | kk => nth Xs kk) |
157 | kk => nth Xs kk) |
156 | freeze_fpTs_simple T = T; |
158 | freeze_fpTs_simple T = T; |
157 |
159 |
158 fun freeze_fpTs_map (callss, (live_call :: _, dead_calls)) s Ts = |
160 fun freeze_fpTs_map (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls)) |
159 (List.app (check_call_dead live_call) dead_calls; |
161 (T as Type (s, Ts)) = |
160 Type (s, map2 freeze_fpTs (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] |
162 if Ts' = Ts then |
161 (transpose callss)) Ts)) |
163 nested_self_call live_call |
162 and freeze_fpTs calls (T as Type (s, Ts)) = |
164 else |
|
165 (List.app (check_call_dead live_call) dead_calls; |
|
166 Type (s, map2 (freeze_fpTs fpT) (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] |
|
167 (transpose callss)) Ts)) |
|
168 and freeze_fpTs fpT calls (T as Type (s, _)) = |
163 (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of |
169 (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of |
164 ([], _) => |
170 ([], _) => |
165 (case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of |
171 (case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of |
166 ([], _) => freeze_fpTs_simple T |
172 ([], _) => freeze_fpTs_simple T |
167 | callsp => freeze_fpTs_map callsp s Ts) |
173 | callsp => freeze_fpTs_map fpT callsp T) |
168 | callsp => freeze_fpTs_map callsp s Ts) |
174 | callsp => freeze_fpTs_map fpT callsp T) |
169 | freeze_fpTs _ T = T; |
175 | freeze_fpTs _ _ T = T; |
170 |
176 |
171 val ctr_Tsss = map (map binder_types) ctr_Tss; |
177 val ctr_Tsss = map (map binder_types) ctr_Tss; |
172 val ctrXs_Tsss = map2 (map2 (map2 freeze_fpTs)) callssss ctr_Tsss; |
178 val ctrXs_Tsss = map3 (map2 o map2 o freeze_fpTs) fpTs callssss ctr_Tsss; |
173 val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; |
179 val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; |
174 val Ts = map (body_type o hd) ctr_Tss; |
180 val ctr_Ts = map (body_type o hd) ctr_Tss; |
175 |
181 |
176 val ns = map length ctr_Tsss; |
182 val ns = map length ctr_Tsss; |
177 val kss = map (fn n => 1 upto n) ns; |
183 val kss = map (fn n => 1 upto n) ns; |
178 val mss = map (map length) ctr_Tsss; |
184 val mss = map (map length) ctr_Tsss; |
179 |
185 |
206 (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types) |
212 (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types) |
207 else define_coiters [unfoldN, corecN] (the coiters_args_types)) |
213 else define_coiters [unfoldN, corecN] (the coiters_args_types)) |
208 (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy |
214 (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy |
209 |>> split_list; |
215 |>> split_list; |
210 |
216 |
211 val rho = tvar_subst thy Ts fpTs; |
217 val rho = tvar_subst thy ctr_Ts fpTs; |
212 val ctr_sugar_phi = Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho)) |
218 val ctr_sugar_phi = Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho)) |
213 (Morphism.term_morphism (Term.subst_TVars rho)); |
219 (Morphism.term_morphism (Term.subst_TVars rho)); |
214 val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi; |
220 val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi; |
215 |
221 |
216 val ctr_sugars = map inst_ctr_sugar ctr_sugars0; |
222 val ctr_sugars = map inst_ctr_sugar ctr_sugars0; |