equal
deleted
inserted
replaced
286 comp_rel_unfold_thm comp_pred_unfold_thm unfold; |
286 comp_rel_unfold_thm comp_pred_unfold_thm unfold; |
287 in |
287 in |
288 (bnf', (unfold', lthy')) |
288 (bnf', (unfold', lthy')) |
289 end; |
289 end; |
290 |
290 |
291 fun clean_compose_bnf_cmd (outer, inners) lthy = |
|
292 let |
|
293 val outer = the (bnf_of lthy outer) |
|
294 val inners = map (the o bnf_of lthy) inners |
|
295 val b = name_of_bnf outer |
|
296 |> Binding.prefix_name compN |
|
297 |> Binding.suffix_name ("_" ^ implode (map (Binding.name_of o name_of_bnf) inners)); |
|
298 in |
|
299 (snd o snd) (clean_compose_bnf Dont_Inline I b outer inners |
|
300 (empty_unfold, lthy)) |
|
301 end; |
|
302 |
|
303 (* Killing live variables *) |
291 (* Killing live variables *) |
304 |
292 |
305 fun killN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else |
293 fun killN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else |
306 let |
294 let |
307 val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf); |
295 val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf); |
403 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') |
391 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') |
404 killN_rel_unfold_thm killN_pred_unfold_thm unfold; |
392 killN_rel_unfold_thm killN_pred_unfold_thm unfold; |
405 in |
393 in |
406 (bnf', (unfold', lthy')) |
394 (bnf', (unfold', lthy')) |
407 end; |
395 end; |
408 |
|
409 fun killN_bnf_cmd (n, raw_bnf) lthy = |
|
410 (snd o snd) (killN_bnf I n (the (bnf_of lthy raw_bnf)) (empty_unfold, lthy)); |
|
411 |
396 |
412 (* Adding dummy live variables *) |
397 (* Adding dummy live variables *) |
413 |
398 |
414 fun liftN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else |
399 fun liftN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else |
415 let |
400 let |
503 liftN_rel_unfold_thm liftN_pred_unfold_thm unfold; |
488 liftN_rel_unfold_thm liftN_pred_unfold_thm unfold; |
504 in |
489 in |
505 (bnf', (unfold', lthy')) |
490 (bnf', (unfold', lthy')) |
506 end; |
491 end; |
507 |
492 |
508 fun liftN_bnf_cmd (n, raw_bnf) lthy = |
|
509 (snd o snd) (liftN_bnf I n (the (bnf_of lthy raw_bnf)) (empty_unfold, lthy)); |
|
510 |
|
511 (* Changing the order of live variables *) |
493 (* Changing the order of live variables *) |
512 |
494 |
513 fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else |
495 fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else |
514 let |
496 let |
515 val b = Binding.prefix_name (mk_permuteN src dest) (name_of_bnf bnf); |
497 val b = Binding.prefix_name (mk_permuteN src dest) (name_of_bnf bnf); |
594 permute_rel_unfold_thm permute_pred_unfold_thm unfold; |
576 permute_rel_unfold_thm permute_pred_unfold_thm unfold; |
595 in |
577 in |
596 (bnf', (unfold', lthy')) |
578 (bnf', (unfold', lthy')) |
597 end; |
579 end; |
598 |
580 |
599 fun permute_bnf_cmd ((src, dest), raw_bnf) lthy = |
|
600 (snd o snd) (permute_bnf I src dest (the (bnf_of lthy raw_bnf)) |
|
601 (empty_unfold, lthy)); |
|
602 |
|
603 (* Composition pipeline *) |
581 (* Composition pipeline *) |
604 |
582 |
605 fun permute_and_kill qualify n src dest bnf = |
583 fun permute_and_kill qualify n src dest bnf = |
606 bnf |
584 bnf |
607 |> permute_bnf qualify src dest |
585 |> permute_bnf qualify src dest |
660 val As = map TFree As; |
638 val As = map TFree As; |
661 in |
639 in |
662 apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy')) |
640 apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy')) |
663 end; |
641 end; |
664 |
642 |
665 fun compose_bnf_cmd (((((b, outer), inners), oDs), Dss), Ass) lthy = (snd o snd) |
|
666 (compose_bnf Dont_Inline I b default_comp_sort (the (bnf_of lthy outer)) |
|
667 (map (the o bnf_of lthy) inners) |
|
668 (map (Syntax.read_typ lthy) oDs) (map (map (Syntax.read_typ lthy)) Dss) |
|
669 (map (map (Syntax.read_typ lthy)) Ass) (empty_unfold, lthy)); |
|
670 |
|
671 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *) |
643 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *) |
672 |
644 |
673 fun seal_bnf unfold b Ds bnf lthy = |
645 fun seal_bnf unfold b Ds bnf lthy = |
674 let |
646 let |
675 val live = live_of_bnf bnf; |
647 val live = live_of_bnf bnf; |
753 |
725 |
754 val rel_def = unfold_defs' (rel_def_of_bnf bnf'); |
726 val rel_def = unfold_defs' (rel_def_of_bnf bnf'); |
755 val rel_unfold = Local_Defs.unfold lthy' |
727 val rel_unfold = Local_Defs.unfold lthy' |
756 (map unfold_defs (filter_refl (rel_unfolds_of unfold))) rel_def; |
728 (map unfold_defs (filter_refl (rel_unfolds_of unfold))) rel_def; |
757 |
729 |
758 val unfold_defs'' = |
730 val unfold_defs'' = unfold_defs' o Local_Defs.unfold lthy' (filter_refl [rel_def_of_bnf bnf']); |
759 unfold_defs' o (Local_Defs.unfold lthy' (filter_refl [rel_def_of_bnf bnf'])); |
|
760 |
731 |
761 val pred_def = unfold_defs'' (pred_def_of_bnf bnf' RS abs_pred_sym_pred_abs); |
732 val pred_def = unfold_defs'' (pred_def_of_bnf bnf' RS abs_pred_sym_pred_abs); |
762 val pred_unfold = Local_Defs.unfold lthy' |
733 val pred_unfold = Local_Defs.unfold lthy' |
763 (map unfold_defs (filter_refl (pred_unfolds_of unfold))) pred_def; |
734 (map unfold_defs (filter_refl (pred_unfolds_of unfold))) pred_def; |
764 |
735 |