19 open BNF_LFP |
19 open BNF_LFP |
20 open BNF_GFP |
20 open BNF_GFP |
21 open BNF_FP_Sugar_Tactics |
21 open BNF_FP_Sugar_Tactics |
22 |
22 |
23 val caseN = "case"; |
23 val caseN = "case"; |
|
24 val coitersN = "iters"; |
|
25 val corecsN = "recs"; |
24 val itersN = "iters"; |
26 val itersN = "iters"; |
25 val recsN = "recs"; |
27 val recsN = "recs"; |
26 |
28 |
27 fun split_list7 xs = (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs); |
29 fun split_list7 xs = (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs); |
28 |
30 |
29 fun retype_free (Free (s, _)) T = Free (s, T); |
31 fun retype_free (Free (s, _)) T = Free (s, T); |
30 |
32 |
31 fun flat_list_comb (f, xss) = fold (fn xs => fn t => Term.list_comb (t, xs)) xss f |
33 val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs)) |
32 |
34 |
33 fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs)); |
35 fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs)); |
34 fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs; |
36 fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs; |
35 fun mk_uncurried2_fun f xss = |
37 fun mk_uncurried2_fun f xss = |
36 mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss); |
38 mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss); |
|
39 |
|
40 fun popescu_zip [] [fs] = fs |
|
41 | popescu_zip (p :: ps) (fs :: fss) = p :: fs @ popescu_zip ps fss; |
37 |
42 |
38 fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters"; |
43 fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters"; |
39 |
44 |
40 fun merge_type_arg_constrained ctxt (T, c) (T', c') = |
45 fun merge_type_arg_constrained ctxt (T, c) (T', c') = |
41 if T = T' then |
46 if T = T' then |
166 end; |
171 end; |
167 |
172 |
168 val fp_iters as fp_iter1 :: _ = map (mk_iter_like As Cs) fp_iters0; |
173 val fp_iters as fp_iter1 :: _ = map (mk_iter_like As Cs) fp_iters0; |
169 val fp_recs as fp_rec1 :: _ = map (mk_iter_like As Cs) fp_recs0; |
174 val fp_recs as fp_rec1 :: _ = map (mk_iter_like As Cs) fp_recs0; |
170 |
175 |
171 val fp_iter_g_Ts = fst (split_last (binder_types (fastype_of fp_iter1))); |
176 val fp_iter_fun_Ts = fst (split_last (binder_types (fastype_of fp_iter1))); |
172 val fp_rec_h_Ts = fst (split_last (binder_types (fastype_of fp_rec1))); |
177 val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1))); |
173 |
178 |
174 fun dest_rec_pair (T as Type (@{type_name prod}, Us as [_, U])) = |
179 fun dest_rec_pair (T as Type (@{type_name prod}, Us as [_, U])) = |
175 if member (op =) Cs U then Us else [T] |
180 if member (op =) Cs U then Us else [T] |
176 | dest_rec_pair T = [T]; |
181 | dest_rec_pair T = [T]; |
177 |
182 |
178 val (((gss, g_Tss, ysss, y_Tsss), (hss, h_Tss, zssss, z_Tssss)), |
183 val (((gss, g_Tss, ysss), (hss, h_Tss, zssss)), |
179 (cs, pss, p_Tss, coiter_extra, corec_extra)) = |
184 (cs, cpss, p_Tss, coiter_extra as ((pgss, cgsss), g_sum_prod_Ts, g_prod_Tss, g_Tsss), |
|
185 corec_extra as ((phss, chsss), h_sum_prod_Ts, h_prod_Tss, h_Tsss))) = |
180 if lfp then |
186 if lfp then |
181 let |
187 let |
182 val y_Tsss = |
188 val y_Tsss = |
183 map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN n o domain_type) |
189 map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN n o domain_type) |
184 ns mss fp_iter_g_Ts; |
190 ns mss fp_iter_fun_Ts; |
185 val g_Tss = map2 (map2 (curry (op --->))) y_Tsss Css; |
191 val g_Tss = map2 (map2 (curry (op --->))) y_Tsss Css; |
186 |
192 |
187 val ((gss, ysss), _) = |
193 val ((gss, ysss), _) = |
188 lthy |
194 lthy |
189 |> mk_Freess "f" g_Tss |
195 |> mk_Freess "f" g_Tss |
190 ||>> mk_Freesss "x" y_Tsss; |
196 ||>> mk_Freesss "x" y_Tsss; |
191 |
197 |
192 val z_Tssss = |
198 val z_Tssss = |
193 map3 (fn n => fn ms => map2 (map dest_rec_pair oo dest_tupleT) ms o dest_sumTN n |
199 map3 (fn n => fn ms => map2 (map dest_rec_pair oo dest_tupleT) ms o dest_sumTN n |
194 o domain_type) ns mss fp_rec_h_Ts; |
200 o domain_type) ns mss fp_rec_fun_Ts; |
195 val h_Tss = map2 (map2 (fold_rev (curry (op --->)))) z_Tssss Css; |
201 val h_Tss = map2 (map2 (fold_rev (curry (op --->)))) z_Tssss Css; |
196 |
202 |
197 val hss = map2 (map2 retype_free) gss h_Tss; |
203 val hss = map2 (map2 retype_free) gss h_Tss; |
198 val (zssss, _) = |
204 val (zssss, _) = |
199 lthy |
205 lthy |
200 |> mk_Freessss "x" z_Tssss; |
206 |> mk_Freessss "x" z_Tssss; |
201 in |
207 in |
202 (((gss, g_Tss, ysss, y_Tsss), (hss, h_Tss, zssss, z_Tssss)), |
208 (((gss, g_Tss, ysss), (hss, h_Tss, zssss)), |
203 ([], [], [], ([], [], [], []), ([], [], [], []))) |
209 ([], [], [], (([], []), [], [], []), (([], []), [], [], []))) |
204 end |
210 end |
205 else |
211 else |
206 let |
212 let |
207 fun mk_to_dest_prodT C = map2 (map (curry (op -->) C) oo dest_tupleT); |
|
208 |
|
209 val p_Tss = |
213 val p_Tss = |
210 map2 (fn C => fn n => replicate (Int.max (0, n - 1)) (C --> HOLogic.boolT)) Cs ns; |
214 map2 (fn C => fn n => replicate (Int.max (0, n - 1)) (C --> HOLogic.boolT)) Cs ns; |
211 |
215 |
212 val g_sum_prod_Ts = map range_type fp_iter_g_Ts; |
216 fun mk_types fun_Ts = |
213 val g_prod_Tss = map2 dest_sumTN ns g_sum_prod_Ts; |
217 let |
214 val g_Tsss = map3 mk_to_dest_prodT Cs mss g_prod_Tss; |
218 val f_sum_prod_Ts = map range_type fun_Ts; |
215 |
219 val f_prod_Tss = map2 dest_sumTN ns f_sum_prod_Ts; |
216 val h_sum_prod_Ts = map range_type fp_rec_h_Ts; |
220 val f_Tsss = |
217 val h_prod_Tss = map2 dest_sumTN ns h_sum_prod_Ts; |
221 map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss f_prod_Tss; |
218 val h_Tsss = map3 mk_to_dest_prodT Cs mss h_prod_Tss; |
222 val pf_Tss = map2 popescu_zip p_Tss f_Tsss |
|
223 in (f_sum_prod_Ts, f_prod_Tss, f_Tsss, pf_Tss) end; |
|
224 |
|
225 val (g_sum_prod_Ts, g_prod_Tss, g_Tsss, pg_Tss) = mk_types fp_iter_fun_Ts; |
|
226 val (h_sum_prod_Ts, h_prod_Tss, h_Tsss, ph_Tss) = mk_types fp_rec_fun_Ts; |
219 |
227 |
220 val (((c, pss), gsss), _) = |
228 val (((c, pss), gsss), _) = |
221 lthy |
229 lthy |
222 |> yield_singleton (mk_Frees "c") dummyT |
230 |> yield_singleton (mk_Frees "c") dummyT |
223 ||>> mk_Freess "p" p_Tss |
231 ||>> mk_Freess "p" p_Tss |
224 ||>> mk_Freesss "g" g_Tsss; |
232 ||>> mk_Freesss "g" g_Tsss; |
225 |
233 |
226 val hsss = map2 (map2 (map2 retype_free)) gsss h_Tsss; |
234 val hsss = map2 (map2 (map2 retype_free)) gsss h_Tsss; |
227 |
235 |
228 val cs = map (retype_free c) Cs; |
236 val cs = map (retype_free c) Cs; |
|
237 val cpss = map2 (fn c => map (fn p => p $ c)) cs pss; |
|
238 |
|
239 fun mk_terms fsss = |
|
240 let |
|
241 val pfss = map2 popescu_zip pss fsss; |
|
242 val cfsss = map2 (fn c => map (map (fn f => f $ c))) cs fsss |
|
243 in (pfss, cfsss) end; |
229 in |
244 in |
230 ((([], [], [], []), ([], [], [], [])), |
245 ((([], [], []), ([], [], [])), |
231 (cs, pss, p_Tss, (gsss, g_sum_prod_Ts, g_prod_Tss, g_Tsss), |
246 (cs, cpss, p_Tss, (mk_terms gsss, g_sum_prod_Ts, g_prod_Tss, pg_Tss), |
232 (hsss, h_sum_prod_Ts, h_prod_Tss, h_Tsss))) |
247 (mk_terms hsss, h_sum_prod_Ts, h_prod_Tss, ph_Tss))) |
233 end; |
248 end; |
234 |
249 |
235 fun pour_some_sugar_on_type ((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec), fld_unf), |
250 fun pour_some_sugar_on_type (((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec), |
236 unf_fld), fld_inject), ctr_binders), ctr_mixfixes), ctr_Tss), disc_binders), |
251 fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_binders), ctr_mixfixes), ctr_Tss), |
237 sel_binderss) no_defs_lthy = |
252 disc_binders), sel_binderss) no_defs_lthy = |
238 let |
253 let |
239 val n = length ctr_Tss; |
|
240 val ks = 1 upto n; |
|
241 val ms = map length ctr_Tss; |
|
242 |
|
243 val unfT = domain_type (fastype_of fld); |
254 val unfT = domain_type (fastype_of fld); |
244 val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss; |
255 val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss; |
245 val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss; |
256 val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss; |
246 |
257 |
247 val ((((u, v), fs), xss), _) = |
258 val ((((u, v), fs), xss), _) = |
322 |
333 |
323 val iter_binder = Binding.suffix_name ("_" ^ iterN) b; |
334 val iter_binder = Binding.suffix_name ("_" ^ iterN) b; |
324 val rec_binder = Binding.suffix_name ("_" ^ recN) b; |
335 val rec_binder = Binding.suffix_name ("_" ^ recN) b; |
325 |
336 |
326 val iter_spec = |
337 val iter_spec = |
327 mk_Trueprop_eq (flat_list_comb (Free (Binding.name_of iter_binder, iter_T), gss), |
338 mk_Trueprop_eq (lists_bmoc gss (Free (Binding.name_of iter_binder, iter_T)), |
328 Term.list_comb (fp_iter, map2 (mk_sum_caseN oo map2 mk_uncurried_fun) gss ysss)); |
339 Term.list_comb (fp_iter, map2 (mk_sum_caseN oo map2 mk_uncurried_fun) gss ysss)); |
329 val rec_spec = |
340 val rec_spec = |
330 mk_Trueprop_eq (flat_list_comb (Free (Binding.name_of rec_binder, rec_T), hss), |
341 mk_Trueprop_eq (lists_bmoc hss (Free (Binding.name_of rec_binder, rec_T)), |
331 Term.list_comb (fp_rec, map2 (mk_sum_caseN oo map2 mk_uncurried2_fun) hss zssss)); |
342 Term.list_comb (fp_rec, map2 (mk_sum_caseN oo map2 mk_uncurried2_fun) hss zssss)); |
332 |
343 |
333 val (([raw_iter, raw_rec], [raw_iter_def, raw_rec_def]), (lthy', lthy)) = no_defs_lthy |
344 val (([raw_iter, raw_rec], [raw_iter_def, raw_rec_def]), (lthy', lthy)) = no_defs_lthy |
334 |> apfst split_list o fold_map2 (fn b => fn spec => |
345 |> apfst split_list o fold_map2 (fn b => fn spec => |
335 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) |
346 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) |
351 ((ctrs, iter, recx, xss, ctr_defs, iter_def, rec_def), lthy) |
362 ((ctrs, iter, recx, xss, ctr_defs, iter_def, rec_def), lthy) |
352 end; |
363 end; |
353 |
364 |
354 fun some_gfp_sugar no_defs_lthy = |
365 fun some_gfp_sugar no_defs_lthy = |
355 let |
366 let |
356 fun zip_preds_and_getters ps fss = ps @ flat fss; |
|
357 |
|
358 val B_to_fpT = C --> fpT; |
367 val B_to_fpT = C --> fpT; |
359 |
368 |
360 val cpss = map2 (fn c => map (fn p => p $ c)) cs pss; |
369 fun generate_coiter_like (suf, fp_iter_like, ((pfss, cfsss), f_sum_prod_Ts, f_prod_Tss, |
361 |
370 pf_Tss)) = |
362 fun generate_coiter_like (suf, fp_iter_like, |
|
363 (fsss, f_sum_prod_Ts, f_prod_Tss, f_Tsss)) = |
|
364 let |
371 let |
365 val pf_Tss = map2 zip_preds_and_getters p_Tss f_Tsss; |
|
366 val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT; |
372 val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT; |
367 |
|
368 val pfss = map2 zip_preds_and_getters pss fsss; |
|
369 val cfsss = map2 (fn c => map (map (fn f => f $ c))) cs fsss; |
|
370 |
373 |
371 val binder = Binding.suffix_name ("_" ^ suf) b; |
374 val binder = Binding.suffix_name ("_" ^ suf) b; |
372 |
375 |
373 fun mk_join c n cps sum_prod_T prod_Ts cfss = |
376 fun mk_join c n cps sum_prod_T prod_Ts cfss = |
374 Term.lambda c (mk_IfN sum_prod_T cps |
377 Term.lambda c (mk_IfN sum_prod_T cps |
375 (map2 (mk_InN prod_Ts) (map HOLogic.mk_tuple cfss) (1 upto n))); |
378 (map2 (mk_InN prod_Ts) (map HOLogic.mk_tuple cfss) (1 upto n))); |
376 |
379 |
377 val spec = |
380 val spec = |
378 mk_Trueprop_eq (flat_list_comb (Free (Binding.name_of binder, res_T), pfss), |
381 mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)), |
379 Term.list_comb (fp_iter_like, |
382 Term.list_comb (fp_iter_like, |
380 map6 mk_join cs ns cpss f_sum_prod_Ts f_prod_Tss cfsss)); |
383 map6 mk_join cs ns cpss f_sum_prod_Ts f_prod_Tss cfsss)); |
381 in (binder, spec) end; |
384 in (binder, spec) end; |
382 |
385 |
383 val coiter_likes = [(coiterN, fp_iter, coiter_extra), (corecN, fp_rec, corec_extra)]; |
386 val coiter_likes = |
|
387 [(coiterN, fp_iter, coiter_extra), |
|
388 (corecN, fp_rec, corec_extra)]; |
|
389 |
384 val (binders, specs) = map generate_coiter_like coiter_likes |> split_list; |
390 val (binders, specs) = map generate_coiter_like coiter_likes |> split_list; |
385 |
391 |
386 val ((csts, defs), (lthy', lthy)) = no_defs_lthy |
392 val ((csts, defs), (lthy', lthy)) = no_defs_lthy |
387 |> apfst split_list o fold_map2 (fn b => fn spec => |
393 |> apfst split_list o fold_map2 (fn b => fn spec => |
388 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) |
394 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) |
401 in |
407 in |
402 wrap_datatype tacss ((ctrs0, casex0), (disc_binders, sel_binderss)) lthy' |
408 wrap_datatype tacss ((ctrs0, casex0), (disc_binders, sel_binderss)) lthy' |
403 |> (if lfp then some_lfp_sugar else some_gfp_sugar) |
409 |> (if lfp then some_lfp_sugar else some_gfp_sugar) |
404 end; |
410 end; |
405 |
411 |
406 fun pour_more_sugar_on_datatypes ((ctrss, iters, recs, xsss, ctr_defss, iter_defs, rec_defs), |
412 fun pour_more_sugar_on_lfps ((ctrss, iters, recs, xsss, ctr_defss, iter_defs, rec_defs), |
407 lthy) = |
413 lthy) = |
408 let |
414 let |
409 val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; |
415 val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; |
410 val giters = map (fn iter => flat_list_comb (iter, gss)) iters; |
416 val giters = map (lists_bmoc gss) iters; |
411 val hrecs = map (fn recx => flat_list_comb (recx, hss)) recs; |
417 val hrecs = map (lists_bmoc hss) recs; |
412 |
418 |
413 val (iter_thmss, rec_thmss) = |
419 val (iter_thmss, rec_thmss) = |
414 let |
420 let |
415 fun mk_goal_iter_like fss fc xctr f xs xs' = |
421 fun mk_goal_iter_like fss fiter_like xctr f xs fxs = |
416 fold_rev (fold_rev Logic.all) (xs :: fss) |
422 fold_rev (fold_rev Logic.all) (xs :: fss) |
417 (mk_Trueprop_eq (fc $ xctr, Term.list_comb (f, xs'))); |
423 (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs))); |
418 |
424 |
419 fun fix_iter_free (x as Free (_, T)) = |
425 fun repair_iter_call (x as Free (_, T)) = |
420 (case find_index (eq_fpT T) fpTs of ~1 => x | j => nth giters j $ x); |
426 (case find_index (curry (op =) T) fpTs of ~1 => x | j => nth giters j $ x); |
421 fun fix_rec_free (x as Free (_, T)) = |
427 fun repair_rec_call (x as Free (_, T)) = |
422 (case find_index (eq_fpT T) fpTs of ~1 => [x] | j => [x, nth hrecs j $ x]); |
428 (case find_index (curry (op =) T) fpTs of ~1 => [x] | j => [x, nth hrecs j $ x]); |
423 |
429 |
424 val iter_xsss = map (map (map fix_iter_free)) xsss; |
430 val gxsss = map (map (map repair_iter_call)) xsss; |
425 val rec_xsss = map (map (maps fix_rec_free)) xsss; |
431 val hxsss = map (map (maps repair_rec_call)) xsss; |
426 |
432 |
427 val goal_iterss = map5 (map4 o mk_goal_iter_like gss) giters xctrss gss xsss iter_xsss; |
433 val goal_iterss = map5 (map4 o mk_goal_iter_like gss) giters xctrss gss xsss gxsss; |
428 val goal_recss = map5 (map4 o mk_goal_iter_like hss) hrecs xctrss hss xsss rec_xsss; |
434 val goal_recss = map5 (map4 o mk_goal_iter_like hss) hrecs xctrss hss xsss hxsss; |
429 |
435 |
430 val iter_tacss = |
436 val iter_tacss = |
431 map2 (map o mk_iter_like_tac pre_map_defs iter_defs) fp_iter_thms ctr_defss; |
437 map2 (map o mk_iter_like_tac pre_map_defs iter_defs) fp_iter_thms ctr_defss; |
432 val rec_tacss = |
438 val rec_tacss = |
433 map2 (map o mk_iter_like_tac pre_map_defs rec_defs) fp_rec_thms ctr_defss; |
439 map2 (map o mk_iter_like_tac pre_map_defs rec_defs) fp_rec_thms ctr_defss; |
447 bs thmss); |
453 bs thmss); |
448 in |
454 in |
449 lthy |> Local_Theory.notes notes |> snd |
455 lthy |> Local_Theory.notes notes |> snd |
450 end; |
456 end; |
451 |
457 |
|
458 fun pour_more_sugar_on_gfps ((ctrss, coiters, corecs, xsss, ctr_defss, coiter_defs, corec_defs), |
|
459 lthy) = |
|
460 let |
|
461 val gcoiters = map (lists_bmoc pgss) coiters; |
|
462 val hcorecs = map (lists_bmoc phss) corecs; |
|
463 |
|
464 val (coiter_thmss, corec_thmss) = |
|
465 let |
|
466 fun mk_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not); |
|
467 |
|
468 fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr cfs' = |
|
469 fold_rev (fold_rev Logic.all) ([c] :: pfss) |
|
470 (Logic.list_implies (seq_conds mk_cond n k cps, |
|
471 mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, cfs')))); |
|
472 |
|
473 fun repair_coiter_like_call fcoiter_likes (cf as Free (_, Type (_, [_, T])) $ _) = |
|
474 (case find_index (curry (op =) T) Cs of ~1 => cf | j => nth fcoiter_likes j $ cf); |
|
475 |
|
476 val cgsss = map (map (map (repair_coiter_like_call gcoiters))) cgsss; |
|
477 val chsss = map (map (map (repair_coiter_like_call hcorecs))) chsss; |
|
478 |
|
479 val goal_coiterss = |
|
480 map7 (map3 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss cgsss; |
|
481 val goal_corecss = |
|
482 map7 (map3 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss chsss; |
|
483 in |
|
484 (map (map (Skip_Proof.make_thm (Proof_Context.theory_of lthy))) goal_coiterss, |
|
485 map (map (Skip_Proof.make_thm (Proof_Context.theory_of lthy))) goal_coiterss (*### goal_corecss*)) |
|
486 end; |
|
487 |
|
488 val notes = |
|
489 [(coitersN, coiter_thmss), |
|
490 (corecsN, corec_thmss)] |
|
491 |> maps (fn (thmN, thmss) => |
|
492 map2 (fn b => fn thms => |
|
493 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
|
494 bs thmss); |
|
495 in |
|
496 lthy |> Local_Theory.notes notes |> snd |
|
497 end; |
|
498 |
452 val lthy' = lthy |
499 val lthy' = lthy |
453 |> fold_map pour_some_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ |
500 |> fold_map pour_some_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ |
454 fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ctr_binderss ~~ ctr_mixfixess ~~ |
501 fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~ |
455 ctr_Tsss ~~ disc_binderss ~~ sel_bindersss) |
502 ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss) |
456 |>> split_list7 |
503 |>> split_list7 |
457 |> (if lfp then pour_more_sugar_on_datatypes else snd); |
504 |> (if lfp then pour_more_sugar_on_lfps else pour_more_sugar_on_gfps); |
458 |
505 |
459 val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^ |
506 val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^ |
460 (if lfp then "" else "co") ^ "datatype")); |
507 (if lfp then "" else "co") ^ "datatype")); |
461 in |
508 in |
462 (timer; lthy') |
509 (timer; lthy') |