equal
deleted
inserted
replaced
145 end; |
145 end; |
146 |
146 |
147 val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1); |
147 val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1); |
148 |
148 |
149 (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*) |
149 (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*) |
150 val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd); |
150 val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd; |
151 |
151 |
152 fun map_id0_tac _ = |
152 fun map_id0_tac _ = |
153 mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer) |
153 mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer) |
154 (map map_id0_of_bnf inners); |
154 (map map_id0_of_bnf inners); |
155 |
155 |
255 mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer) |
255 mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer) |
256 (maps wit_thms_of_bnf inners); |
256 (maps wit_thms_of_bnf inners); |
257 |
257 |
258 val (bnf', lthy') = |
258 val (bnf', lthy') = |
259 bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty |
259 bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty |
260 Binding.empty [] (((((b, mapx), sets), bd), wits), SOME rel) lthy; |
260 Binding.empty [] ((((((b, CCA), mapx), sets), bd), wits), SOME rel) lthy; |
261 in |
261 in |
262 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) |
262 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) |
263 end; |
263 end; |
264 |
264 |
265 (* Killing live variables *) |
265 (* Killing live variables *) |
349 |
349 |
350 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
350 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
351 |
351 |
352 val (bnf', lthy') = |
352 val (bnf', lthy') = |
353 bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty |
353 bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty |
354 Binding.empty [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; |
354 Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; |
355 in |
355 in |
356 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) |
356 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) |
357 end; |
357 end; |
358 |
358 |
359 (* Adding dummy live variables *) |
359 (* Adding dummy live variables *) |
431 |
431 |
432 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
432 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
433 |
433 |
434 val (bnf', lthy') = |
434 val (bnf', lthy') = |
435 bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty |
435 bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty |
436 [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; |
436 [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; |
437 in |
437 in |
438 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) |
438 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) |
439 end; |
439 end; |
440 |
440 |
441 (* Changing the order of live variables *) |
441 (* Changing the order of live variables *) |
504 |
504 |
505 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
505 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); |
506 |
506 |
507 val (bnf', lthy') = |
507 val (bnf', lthy') = |
508 bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty |
508 bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty |
509 [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; |
509 [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; |
510 in |
510 in |
511 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) |
511 (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) |
512 end; |
512 end; |
513 |
513 |
514 (* Composition pipeline *) |
514 (* Composition pipeline *) |
641 fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf)); |
641 fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf)); |
642 |
642 |
643 val (bnf', lthy') = |
643 val (bnf', lthy') = |
644 bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads) |
644 bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads) |
645 Binding.empty Binding.empty [] |
645 Binding.empty Binding.empty [] |
646 (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy; |
646 ((((((b, T), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy; |
647 in |
647 in |
648 ((bnf', deads), lthy') |
648 ((bnf', deads), lthy') |
649 end; |
649 end; |
650 |
650 |
651 exception BAD_DEAD of typ * typ; |
651 exception BAD_DEAD of typ * typ; |