6 Composition of bounded natural functors. |
6 Composition of bounded natural functors. |
7 *) |
7 *) |
8 |
8 |
9 signature BNF_COMP = |
9 signature BNF_COMP = |
10 sig |
10 sig |
11 type unfold_thms |
11 type unfold_set |
12 val empty_unfold: unfold_thms |
12 val empty_unfolds: unfold_set |
13 val map_unfolds_of: unfold_thms -> thm list |
13 val map_unfolds_of: unfold_set -> thm list |
14 val set_unfoldss_of: unfold_thms -> thm list list |
14 val set_unfoldss_of: unfold_set -> thm list list |
15 val pred_unfolds_of: unfold_thms -> thm list |
15 val pred_unfolds_of: unfold_set -> thm list |
16 val rel_unfolds_of: unfold_thms -> thm list |
16 val rel_unfolds_of: unfold_set -> thm list |
17 |
17 |
18 val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) -> |
18 val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) -> |
19 ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context -> |
19 ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context -> |
20 (BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context) |
20 (BNF_Def.BNF * (typ list * typ list)) * (unfold_set * Proof.context) |
21 val default_comp_sort: (string * sort) list list -> (string * sort) list |
21 val default_comp_sort: (string * sort) list list -> (string * sort) list |
22 val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list -> |
22 val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list -> |
23 (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context -> |
23 (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_set -> Proof.context -> |
24 (int list list * ''a list) * (BNF_Def.BNF list * (unfold_thms * Proof.context)) |
24 (int list list * ''a list) * (BNF_Def.BNF list * (unfold_set * Proof.context)) |
25 val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context -> |
25 val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.BNF -> Proof.context -> |
26 (BNF_Def.BNF * typ list) * local_theory |
26 (BNF_Def.BNF * typ list) * local_theory |
27 end; |
27 end; |
28 |
28 |
29 structure BNF_Comp : BNF_COMP = |
29 structure BNF_Comp : BNF_COMP = |
30 struct |
30 struct |
44 fun add_to_thms thms NONE = thms |
44 fun add_to_thms thms NONE = thms |
45 | add_to_thms thms (SOME new) = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new; |
45 | add_to_thms thms (SOME new) = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new; |
46 fun adds_to_thms thms NONE = thms |
46 fun adds_to_thms thms NONE = thms |
47 | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (no_reflexive news) thms; |
47 | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (no_reflexive news) thms; |
48 |
48 |
49 val empty_unfold = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []}; |
49 val empty_unfolds = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []}; |
50 |
50 |
51 fun add_to_unfold_opt map_opt sets_opt pred_opt rel_opt |
51 fun add_to_unfolds_opt map_opt sets_opt pred_opt rel_opt |
52 {map_unfolds, set_unfoldss, pred_unfolds, rel_unfolds} = |
52 {map_unfolds, set_unfoldss, pred_unfolds, rel_unfolds} = |
53 {map_unfolds = add_to_thms map_unfolds map_opt, |
53 {map_unfolds = add_to_thms map_unfolds map_opt, |
54 set_unfoldss = adds_to_thms set_unfoldss sets_opt, |
54 set_unfoldss = adds_to_thms set_unfoldss sets_opt, |
55 pred_unfolds = add_to_thms pred_unfolds pred_opt, |
55 pred_unfolds = add_to_thms pred_unfolds pred_opt, |
56 rel_unfolds = add_to_thms rel_unfolds rel_opt}; |
56 rel_unfolds = add_to_thms rel_unfolds rel_opt}; |
57 |
57 |
58 fun add_to_unfold map sets pred rel = |
58 fun add_to_unfolds map sets pred rel = |
59 add_to_unfold_opt (SOME map) (SOME sets) (SOME pred) (SOME rel); |
59 add_to_unfolds_opt (SOME map) (SOME sets) (SOME pred) (SOME rel); |
60 |
60 |
61 val map_unfolds_of = #map_unfolds; |
61 val map_unfolds_of = #map_unfolds; |
62 val set_unfoldss_of = #set_unfoldss; |
62 val set_unfoldss_of = #set_unfoldss; |
63 val pred_unfolds_of = #pred_unfolds; |
63 val pred_unfolds_of = #pred_unfolds; |
64 val rel_unfolds_of = #rel_unfolds; |
64 val rel_unfolds_of = #rel_unfolds; |
75 let |
75 let |
76 val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs; |
76 val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs; |
77 val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE; |
77 val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE; |
78 in Envir.expand_term get end; |
78 in Envir.expand_term get end; |
79 |
79 |
80 fun clean_compose_bnf const_policy qualify b outer inners (unfold, lthy) = |
80 fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) = |
81 let |
81 let |
82 val olive = live_of_bnf outer; |
82 val olive = live_of_bnf outer; |
83 val onwits = nwits_of_bnf outer; |
83 val onwits = nwits_of_bnf outer; |
84 val odead = dead_of_bnf outer; |
84 val odead = dead_of_bnf outer; |
85 val inner = hd inners; |
85 val inner = hd inners; |
272 |
272 |
273 val (bnf', lthy') = |
273 val (bnf', lthy') = |
274 bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) |
274 bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) |
275 (((((b, mapx), sets), bd), wits), SOME pred) lthy; |
275 (((((b, mapx), sets), bd), wits), SOME pred) lthy; |
276 |
276 |
277 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') |
277 val unfold_set' = |
278 (rel_def_of_bnf bnf') unfold; |
278 add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') |
|
279 (rel_def_of_bnf bnf') unfold_set; |
279 in |
280 in |
280 (bnf', (unfold', lthy')) |
281 (bnf', (unfold_set', lthy')) |
281 end; |
282 end; |
282 |
283 |
283 (* Killing live variables *) |
284 (* Killing live variables *) |
284 |
285 |
285 fun kill_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else |
286 fun kill_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else |
286 let |
287 let |
287 val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf); |
288 val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf); |
288 val live = live_of_bnf bnf; |
289 val live = live_of_bnf bnf; |
289 val dead = dead_of_bnf bnf; |
290 val dead = dead_of_bnf bnf; |
290 val nwits = nwits_of_bnf bnf; |
291 val nwits = nwits_of_bnf bnf; |
373 |
374 |
374 val (bnf', lthy') = |
375 val (bnf', lthy') = |
375 bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) |
376 bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) |
376 (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; |
377 (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; |
377 |
378 |
378 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') |
379 val unfold_set' = |
379 (rel_def_of_bnf bnf') unfold; |
380 add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') |
|
381 (rel_def_of_bnf bnf') unfold_set; |
380 in |
382 in |
381 (bnf', (unfold', lthy')) |
383 (bnf', (unfold_set', lthy')) |
382 end; |
384 end; |
383 |
385 |
384 (* Adding dummy live variables *) |
386 (* Adding dummy live variables *) |
385 |
387 |
386 fun lift_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else |
388 fun lift_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else |
387 let |
389 let |
388 val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf); |
390 val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf); |
389 val live = live_of_bnf bnf; |
391 val live = live_of_bnf bnf; |
390 val dead = dead_of_bnf bnf; |
392 val dead = dead_of_bnf bnf; |
391 val nwits = nwits_of_bnf bnf; |
393 val nwits = nwits_of_bnf bnf; |
460 |
462 |
461 val (bnf', lthy') = |
463 val (bnf', lthy') = |
462 bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) |
464 bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) |
463 (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; |
465 (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; |
464 |
466 |
465 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') |
467 val unfold_set' = |
466 (pred_def_of_bnf bnf') unfold; |
468 add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') |
|
469 (pred_def_of_bnf bnf') unfold_set; |
467 in |
470 in |
468 (bnf', (unfold', lthy')) |
471 (bnf', (unfold_set', lthy')) |
469 end; |
472 end; |
470 |
473 |
471 (* Changing the order of live variables *) |
474 (* Changing the order of live variables *) |
472 |
475 |
473 fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else |
476 fun permute_bnf qualify src dest bnf (unfold_set, lthy) = |
|
477 if src = dest then (bnf, (unfold_set, lthy)) else |
474 let |
478 let |
475 val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf); |
479 val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf); |
476 val live = live_of_bnf bnf; |
480 val live = live_of_bnf bnf; |
477 val dead = dead_of_bnf bnf; |
481 val dead = dead_of_bnf bnf; |
478 val nwits = nwits_of_bnf bnf; |
482 val nwits = nwits_of_bnf bnf; |
538 |
542 |
539 val (bnf', lthy') = |
543 val (bnf', lthy') = |
540 bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) |
544 bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) |
541 (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; |
545 (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy; |
542 |
546 |
543 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') |
547 val unfold_set' = |
544 (pred_def_of_bnf bnf') unfold; |
548 add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf') |
|
549 (pred_def_of_bnf bnf') unfold_set; |
545 in |
550 in |
546 (bnf', (unfold', lthy')) |
551 (bnf', (unfold_set', lthy')) |
547 end; |
552 end; |
548 |
553 |
549 (* Composition pipeline *) |
554 (* Composition pipeline *) |
550 |
555 |
551 fun permute_and_kill qualify n src dest bnf = |
556 fun permute_and_kill qualify n src dest bnf = |
556 fun lift_and_permute qualify n src dest bnf = |
561 fun lift_and_permute qualify n src dest bnf = |
557 bnf |
562 bnf |
558 |> lift_bnf qualify n |
563 |> lift_bnf qualify n |
559 #> uncurry (permute_bnf qualify src dest); |
564 #> uncurry (permute_bnf qualify src dest); |
560 |
565 |
561 fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy = |
566 fun normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy = |
562 let |
567 let |
563 val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; |
568 val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; |
564 val kill_poss = map (find_indices Ds) Ass; |
569 val kill_poss = map (find_indices Ds) Ass; |
565 val live_poss = map2 (subtract (op =)) kill_poss before_kill_src; |
570 val live_poss = map2 (subtract (op =)) kill_poss before_kill_src; |
566 val before_kill_dest = map2 append kill_poss live_poss; |
571 val before_kill_dest = map2 append kill_poss live_poss; |
567 val kill_ns = map length kill_poss; |
572 val kill_ns = map length kill_poss; |
568 val (inners', (unfold', lthy')) = |
573 val (inners', (unfold_set', lthy')) = |
569 fold_map5 (fn i => permute_and_kill (qualify i)) |
574 fold_map5 (fn i => permute_and_kill (qualify i)) |
570 (if length bnfs = 1 then [0] else (1 upto length bnfs)) |
575 (if length bnfs = 1 then [0] else (1 upto length bnfs)) |
571 kill_ns before_kill_src before_kill_dest bnfs (unfold, lthy); |
576 kill_ns before_kill_src before_kill_dest bnfs (unfold_set, lthy); |
572 |
577 |
573 val Ass' = map2 (map o nth) Ass live_poss; |
578 val Ass' = map2 (map o nth) Ass live_poss; |
574 val As = sort Ass'; |
579 val As = sort Ass'; |
575 val after_lift_dest = replicate (length Ass') (0 upto (length As - 1)); |
580 val after_lift_dest = replicate (length Ass') (0 upto (length As - 1)); |
576 val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass'; |
581 val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass'; |
578 val after_lift_src = map2 append new_poss old_poss; |
583 val after_lift_src = map2 append new_poss old_poss; |
579 val lift_ns = map (fn xs => length As - length xs) Ass'; |
584 val lift_ns = map (fn xs => length As - length xs) Ass'; |
580 in |
585 in |
581 ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i)) |
586 ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i)) |
582 (if length bnfs = 1 then [0] else (1 upto length bnfs)) |
587 (if length bnfs = 1 then [0] else (1 upto length bnfs)) |
583 lift_ns after_lift_src after_lift_dest inners' (unfold', lthy')) |
588 lift_ns after_lift_src after_lift_dest inners' (unfold_set', lthy')) |
584 end; |
589 end; |
585 |
590 |
586 fun default_comp_sort Ass = |
591 fun default_comp_sort Ass = |
587 Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []); |
592 Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []); |
588 |
593 |
589 fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold, lthy) = |
594 fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold_set, lthy) = |
590 let |
595 let |
591 val b = name_of_bnf outer; |
596 val b = name_of_bnf outer; |
592 |
597 |
593 val Ass = map (map Term.dest_TFree) tfreess; |
598 val Ass = map (map Term.dest_TFree) tfreess; |
594 val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; |
599 val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; |
595 |
600 |
596 val ((kill_poss, As), (inners', (unfold', lthy'))) = |
601 val ((kill_poss, As), (inners', (unfold_set', lthy'))) = |
597 normalize_bnfs qualify Ass Ds sort inners unfold lthy; |
602 normalize_bnfs qualify Ass Ds sort inners unfold_set lthy; |
598 |
603 |
599 val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss); |
604 val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss); |
600 val As = map TFree As; |
605 val As = map TFree As; |
601 in |
606 in |
602 apfst (rpair (Ds, As)) |
607 apfst (rpair (Ds, As)) |
603 (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold', lthy')) |
608 (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy')) |
604 end; |
609 end; |
605 |
610 |
606 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *) |
611 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *) |
607 |
612 |
608 fun seal_bnf unfold b Ds bnf lthy = |
613 fun seal_bnf unfold_set b Ds bnf lthy = |
609 let |
614 let |
610 val live = live_of_bnf bnf; |
615 val live = live_of_bnf bnf; |
611 val nwits = nwits_of_bnf bnf; |
616 val nwits = nwits_of_bnf bnf; |
612 |
617 |
613 val (As, lthy1) = apfst (map TFree) |
618 val (As, lthy1) = apfst (map TFree) |
614 (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy)); |
619 (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy)); |
615 val (Bs, _) = apfst (map TFree) |
620 val (Bs, _) = apfst (map TFree) |
616 (Variable.invent_types (replicate live HOLogic.typeS) lthy1); |
621 (Variable.invent_types (replicate live HOLogic.typeS) lthy1); |
617 |
622 |
618 val map_unfolds = map_unfolds_of unfold; |
623 val map_unfolds = map_unfolds_of unfold_set; |
619 val set_unfoldss = set_unfoldss_of unfold; |
624 val set_unfoldss = set_unfoldss_of unfold_set; |
620 val pred_unfolds = pred_unfolds_of unfold; |
625 val pred_unfolds = pred_unfolds_of unfold_set; |
621 val rel_unfolds = rel_unfolds_of unfold; |
626 val rel_unfolds = rel_unfolds_of unfold_set; |
622 |
627 |
623 val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) |
628 val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) |
624 map_unfolds); |
629 map_unfolds); |
625 val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) |
630 val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) |
626 set_unfoldss); |
631 set_unfoldss); |
693 val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID"); |
698 val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID"); |
694 val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID"); |
699 val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID"); |
695 |
700 |
696 fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum) |
701 fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum) |
697 | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable" |
702 | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable" |
698 | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold, lthy) = |
703 | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold_set, lthy) = |
699 let |
704 let |
700 val tfrees = Term.add_tfreesT T []; |
705 val tfrees = Term.add_tfreesT T []; |
701 val bnf_opt = if null tfrees then NONE else bnf_of lthy C; |
706 val bnf_opt = if null tfrees then NONE else bnf_of lthy C; |
702 in |
707 in |
703 (case bnf_opt of |
708 (case bnf_opt of |
704 NONE => ((DEADID_bnf, ([T], [])), (unfold, lthy)) |
709 NONE => ((DEADID_bnf, ([T], [])), (unfold_set, lthy)) |
705 | SOME bnf => |
710 | SOME bnf => |
706 if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then |
711 if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then |
707 let |
712 let |
708 val T' = T_of_bnf bnf; |
713 val T' = T_of_bnf bnf; |
709 val deads = deads_of_bnf bnf; |
714 val deads = deads_of_bnf bnf; |
710 val lives = lives_of_bnf bnf; |
715 val lives = lives_of_bnf bnf; |
711 val tvars' = Term.add_tvarsT T' []; |
716 val tvars' = Term.add_tvarsT T' []; |
712 val deads_lives = |
717 val deads_lives = |
713 pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees))) |
718 pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees))) |
714 (deads, lives); |
719 (deads, lives); |
715 in ((bnf, deads_lives), (unfold, lthy)) end |
720 in ((bnf, deads_lives), (unfold_set, lthy)) end |
716 else |
721 else |
717 let |
722 let |
718 val name = Long_Name.base_name C; |
723 val name = Long_Name.base_name C; |
719 fun qualify i = |
724 fun qualify i = |
720 let val namei = name ^ nonzero_string_of_int i; |
725 let val namei = name ^ nonzero_string_of_int i; |
723 val olive = live_of_bnf bnf; |
728 val olive = live_of_bnf bnf; |
724 val oDs_pos = find_indices [TFree ("dead", [])] (snd (Term.dest_Type |
729 val oDs_pos = find_indices [TFree ("dead", [])] (snd (Term.dest_Type |
725 (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf))); |
730 (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf))); |
726 val oDs = map (nth Ts) oDs_pos; |
731 val oDs = map (nth Ts) oDs_pos; |
727 val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1)); |
732 val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1)); |
728 val ((inners, (Dss, Ass)), (unfold', lthy')) = |
733 val ((inners, (Dss, Ass)), (unfold_set', lthy')) = |
729 apfst (apsnd split_list o split_list) |
734 apfst (apsnd split_list o split_list) |
730 (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort) |
735 (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort) |
731 (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold, lthy)); |
736 (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold_set, lthy)); |
732 in |
737 in |
733 compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold', lthy') |
738 compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold_set', lthy') |
734 end) |
739 end) |
735 end; |
740 end; |
736 |
741 |
737 end; |
742 end; |