474 |
474 |
475 datatype coeqn_data = |
475 datatype coeqn_data = |
476 Disc of coeqn_data_disc | |
476 Disc of coeqn_data_disc | |
477 Sel of coeqn_data_sel; |
477 Sel of coeqn_data_sel; |
478 |
478 |
479 fun dissect_coeqn_disc seq fun_names (ctr_specss : corec_ctr_spec list list) maybe_ctr_rhs |
479 fun dissect_coeqn_disc seq fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) |
480 maybe_code_rhs prems' concl matchedsss = |
480 maybe_ctr_rhs maybe_code_rhs prems' concl matchedsss = |
481 let |
481 let |
482 fun find_subterm p = let (* FIXME \<exists>? *) |
482 fun find_subterm p = let (* FIXME \<exists>? *) |
483 fun f (t as u $ v) = if p t then SOME t else merge_options (f u, f v) |
483 fun f (t as u $ v) = if p t then SOME t else merge_options (f u, f v) |
484 | f t = if p t then SOME t else NONE |
484 | f t = if p t then SOME t else NONE |
485 in f end; |
485 in f end; |
487 val applied_fun = concl |
487 val applied_fun = concl |
488 |> find_subterm (member ((op =) o apsnd SOME) fun_names o try (fst o dest_Free o head_of)) |
488 |> find_subterm (member ((op =) o apsnd SOME) fun_names o try (fst o dest_Free o head_of)) |
489 |> the |
489 |> the |
490 handle Option.Option => primrec_error_eqn "malformed discriminator equation" concl; |
490 handle Option.Option => primrec_error_eqn "malformed discriminator equation" concl; |
491 val ((fun_name, fun_T), fun_args) = strip_comb applied_fun |>> dest_Free; |
491 val ((fun_name, fun_T), fun_args) = strip_comb applied_fun |>> dest_Free; |
492 val ctr_specs = the (AList.lookup (op =) (fun_names ~~ ctr_specss) fun_name); |
492 val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name); |
493 |
493 |
494 val discs = map #disc ctr_specs; |
494 val discs = map #disc basic_ctr_specs; |
495 val ctrs = map #ctr ctr_specs; |
495 val ctrs = map #ctr basic_ctr_specs; |
496 val not_disc = head_of concl = @{term Not}; |
496 val not_disc = head_of concl = @{term Not}; |
497 val _ = not_disc andalso length ctrs <> 2 andalso |
497 val _ = not_disc andalso length ctrs <> 2 andalso |
498 primrec_error_eqn "\<not>ed discriminator for a type with \<noteq> 2 constructors" concl; |
498 primrec_error_eqn "\<not>ed discriminator for a type with \<noteq> 2 constructors" concl; |
499 val disc = find_subterm (member (op =) discs o head_of) concl; |
499 val disc' = find_subterm (member (op =) discs o head_of) concl; |
500 val eq_ctr0 = concl |> perhaps (try (HOLogic.dest_not)) |> try (HOLogic.dest_eq #> snd) |
500 val eq_ctr0 = concl |> perhaps (try (HOLogic.dest_not)) |> try (HOLogic.dest_eq #> snd) |
501 |> (fn SOME t => let val n = find_index (equal t) ctrs in |
501 |> (fn SOME t => let val n = find_index (equal t) ctrs in |
502 if n >= 0 then SOME n else NONE end | _ => NONE); |
502 if n >= 0 then SOME n else NONE end | _ => NONE); |
503 val _ = is_some disc orelse is_some eq_ctr0 orelse |
503 val _ = is_some disc' orelse is_some eq_ctr0 orelse |
504 primrec_error_eqn "no discriminator in equation" concl; |
504 primrec_error_eqn "no discriminator in equation" concl; |
505 val ctr_no' = |
505 val ctr_no' = |
506 if is_none disc then the eq_ctr0 else find_index (equal (head_of (the disc))) discs; |
506 if is_none disc' then the eq_ctr0 else find_index (equal (head_of (the disc'))) discs; |
507 val ctr_no = if not_disc then 1 - ctr_no' else ctr_no'; |
507 val ctr_no = if not_disc then 1 - ctr_no' else ctr_no'; |
508 val ctr = #ctr (nth ctr_specs ctr_no); |
508 val {ctr, disc, ...} = nth basic_ctr_specs ctr_no; |
509 |
509 |
510 val catch_all = try (fst o dest_Free o the_single) prems' = SOME Name.uu_; |
510 val catch_all = try (fst o dest_Free o the_single) prems' = SOME Name.uu_; |
511 val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default []; |
511 val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default []; |
512 val prems = map (abstract (List.rev fun_args)) prems'; |
512 val prems = map (abstract (List.rev fun_args)) prems'; |
513 val real_prems = |
513 val real_prems = |
526 fun_name = fun_name, |
526 fun_name = fun_name, |
527 fun_T = fun_T, |
527 fun_T = fun_T, |
528 fun_args = fun_args, |
528 fun_args = fun_args, |
529 ctr = ctr, |
529 ctr = ctr, |
530 ctr_no = ctr_no, |
530 ctr_no = ctr_no, |
531 disc = #disc (nth ctr_specs ctr_no), |
531 disc = disc, |
532 prems = real_prems, |
532 prems = real_prems, |
533 auto_gen = catch_all, |
533 auto_gen = catch_all, |
534 maybe_ctr_rhs = maybe_ctr_rhs, |
534 maybe_ctr_rhs = maybe_ctr_rhs, |
535 maybe_code_rhs = maybe_code_rhs, |
535 maybe_code_rhs = maybe_code_rhs, |
536 user_eqn = user_eqn |
536 user_eqn = user_eqn |
537 }, matchedsss') |
537 }, matchedsss') |
538 end; |
538 end; |
539 |
539 |
540 fun dissect_coeqn_sel fun_names (ctr_specss : corec_ctr_spec list list) eqn' of_spec eqn = |
540 fun dissect_coeqn_sel fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn' of_spec |
|
541 eqn = |
541 let |
542 let |
542 val (lhs, rhs) = HOLogic.dest_eq eqn |
543 val (lhs, rhs) = HOLogic.dest_eq eqn |
543 handle TERM _ => |
544 handle TERM _ => |
544 primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn; |
545 primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn; |
545 val sel = head_of lhs; |
546 val sel = head_of lhs; |
546 val ((fun_name, fun_T), fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst dest_Free |
547 val ((fun_name, fun_T), fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst dest_Free |
547 handle TERM _ => |
548 handle TERM _ => |
548 primrec_error_eqn "malformed selector argument in left-hand side" eqn; |
549 primrec_error_eqn "malformed selector argument in left-hand side" eqn; |
549 val ctr_specs = the (AList.lookup (op =) (fun_names ~~ ctr_specss) fun_name) |
550 val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name) |
550 handle Option.Option => primrec_error_eqn "malformed selector argument in left-hand side" eqn; |
551 handle Option.Option => primrec_error_eqn "malformed selector argument in left-hand side" eqn; |
551 val ctr_spec = |
552 val {ctr, ...} = |
552 if is_some of_spec |
553 if is_some of_spec |
553 then the (find_first (equal (the of_spec) o #ctr) ctr_specs) |
554 then the (find_first (equal (the of_spec) o #ctr) basic_ctr_specs) |
554 else ctr_specs |> filter (exists (equal sel) o #sels) |> the_single |
555 else filter (exists (equal sel) o #sels) basic_ctr_specs |> the_single |
555 handle List.Empty => primrec_error_eqn "ambiguous selector - use \"of\"" eqn; |
556 handle List.Empty => primrec_error_eqn "ambiguous selector - use \"of\"" eqn; |
556 val user_eqn = drop_All eqn'; |
557 val user_eqn = drop_All eqn'; |
557 in |
558 in |
558 Sel { |
559 Sel { |
559 fun_name = fun_name, |
560 fun_name = fun_name, |
560 fun_T = fun_T, |
561 fun_T = fun_T, |
561 fun_args = fun_args, |
562 fun_args = fun_args, |
562 ctr = #ctr ctr_spec, |
563 ctr = ctr, |
563 sel = sel, |
564 sel = sel, |
564 rhs_term = rhs, |
565 rhs_term = rhs, |
565 user_eqn = user_eqn |
566 user_eqn = user_eqn |
566 } |
567 } |
567 end; |
568 end; |
568 |
569 |
569 fun dissect_coeqn_ctr seq fun_names (ctr_specss : corec_ctr_spec list list) eqn' maybe_code_rhs |
570 fun dissect_coeqn_ctr seq fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn' |
570 prems concl matchedsss = |
571 maybe_code_rhs prems concl matchedsss = |
571 let |
572 let |
572 val (lhs, rhs) = HOLogic.dest_eq concl; |
573 val (lhs, rhs) = HOLogic.dest_eq concl; |
573 val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free; |
574 val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free; |
574 val ctr_specs = the (AList.lookup (op =) (fun_names ~~ ctr_specss) fun_name); |
575 val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name); |
575 val (ctr, ctr_args) = strip_comb (unfold_let rhs); |
576 val (ctr, ctr_args) = strip_comb (unfold_let rhs); |
576 val {disc, sels, ...} = the (find_first (equal ctr o #ctr) ctr_specs) |
577 val {disc, sels, ...} = the (find_first (equal ctr o #ctr) basic_ctr_specs) |
577 handle Option.Option => primrec_error_eqn "not a constructor" ctr; |
578 handle Option.Option => primrec_error_eqn "not a constructor" ctr; |
578 |
579 |
579 val disc_concl = betapply (disc, lhs); |
580 val disc_concl = betapply (disc, lhs); |
580 val (maybe_eqn_data_disc, matchedsss') = if length ctr_specs = 1 |
581 val (maybe_eqn_data_disc, matchedsss') = if length basic_ctr_specs = 1 |
581 then (NONE, matchedsss) |
582 then (NONE, matchedsss) |
582 else apfst SOME (dissect_coeqn_disc seq fun_names ctr_specss |
583 else apfst SOME (dissect_coeqn_disc seq fun_names basic_ctr_specss |
583 (SOME (abstract (List.rev fun_args) rhs)) maybe_code_rhs prems disc_concl matchedsss); |
584 (SOME (abstract (List.rev fun_args) rhs)) maybe_code_rhs prems disc_concl matchedsss); |
584 |
585 |
585 val sel_concls = (sels ~~ ctr_args) |
586 val sel_concls = (sels ~~ ctr_args) |
586 |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)); |
587 |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)); |
587 |
588 |
591 space_implode "\n \<cdot> " (map (Syntax.string_of_term @{context}) sel_concls) ^ |
592 space_implode "\n \<cdot> " (map (Syntax.string_of_term @{context}) sel_concls) ^ |
592 "\nfor premise(s)\n \<cdot> " ^ |
593 "\nfor premise(s)\n \<cdot> " ^ |
593 space_implode "\n \<cdot> " (map (Syntax.string_of_term @{context}) prems)); |
594 space_implode "\n \<cdot> " (map (Syntax.string_of_term @{context}) prems)); |
594 *) |
595 *) |
595 |
596 |
596 val eqns_data_sel = map (dissect_coeqn_sel fun_names ctr_specss eqn' (SOME ctr)) sel_concls; |
597 val eqns_data_sel = |
|
598 map (dissect_coeqn_sel fun_names basic_ctr_specss eqn' (SOME ctr)) sel_concls; |
597 in |
599 in |
598 (the_list maybe_eqn_data_disc @ eqns_data_sel, matchedsss') |
600 (the_list maybe_eqn_data_disc @ eqns_data_sel, matchedsss') |
599 end; |
601 end; |
600 |
602 |
601 fun dissect_coeqn_code lthy has_call fun_names ctr_specss eqn' concl matchedsss = |
603 fun dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn' concl matchedsss = |
602 let |
604 let |
603 val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl ||> `(expand_corec_code_rhs lthy has_call []); |
605 val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl ||> `(expand_corec_code_rhs lthy has_call []); |
604 val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free; |
606 val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free; |
605 val ctr_specs = the (AList.lookup (op =) (fun_names ~~ ctr_specss) fun_name); |
607 val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name); |
606 |
608 |
607 val cond_ctrs = fold_rev_corec_code_rhs lthy (fn cs => fn ctr => fn _ => |
609 val cond_ctrs = fold_rev_corec_code_rhs lthy (fn cs => fn ctr => fn _ => |
608 if member ((op =) o apsnd #ctr) ctr_specs ctr |
610 if member ((op =) o apsnd #ctr) basic_ctr_specs ctr |
609 then cons (ctr, cs) |
611 then cons (ctr, cs) |
610 else primrec_error_eqn "not a constructor" ctr) [] rhs' [] |
612 else primrec_error_eqn "not a constructor" ctr) [] rhs' [] |
611 |> AList.group (op =); |
613 |> AList.group (op =); |
612 |
614 |
613 val ctr_premss = (case cond_ctrs of [_] => [[]] | _ => map (s_dnf o snd) cond_ctrs); |
615 val ctr_premss = (case cond_ctrs of [_] => [[]] | _ => map (s_dnf o snd) cond_ctrs); |
616 |> map_index (fn (n, T) => massage_corec_code_rhs lthy (fn _ => fn ctr' => fn args => |
618 |> map_index (fn (n, T) => massage_corec_code_rhs lthy (fn _ => fn ctr' => fn args => |
617 if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs') |
619 if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs') |
618 |> curry list_comb ctr |
620 |> curry list_comb ctr |
619 |> curry HOLogic.mk_eq lhs); |
621 |> curry HOLogic.mk_eq lhs); |
620 in |
622 in |
621 fold_map2 (dissect_coeqn_ctr false fun_names ctr_specss eqn' |
623 fold_map2 (dissect_coeqn_ctr false fun_names basic_ctr_specss eqn' |
622 (SOME (abstract (List.rev fun_args) rhs))) |
624 (SOME (abstract (List.rev fun_args) rhs))) |
623 ctr_premss ctr_concls matchedsss |
625 ctr_premss ctr_concls matchedsss |
624 end; |
626 end; |
625 |
627 |
626 fun dissect_coeqn lthy seq has_call fun_names (ctr_specss : corec_ctr_spec list list) eqn' of_spec |
628 fun dissect_coeqn lthy seq has_call fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) |
627 matchedsss = |
629 eqn' of_spec matchedsss = |
628 let |
630 let |
629 val eqn = drop_All eqn' |
631 val eqn = drop_All eqn' |
630 handle TERM _ => primrec_error_eqn "malformed function equation" eqn'; |
632 handle TERM _ => primrec_error_eqn "malformed function equation" eqn'; |
631 val (prems, concl) = Logic.strip_horn eqn |
633 val (prems, concl) = Logic.strip_horn eqn |
632 |> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop; |
634 |> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop; |
635 |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq)) |
637 |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq)) |
636 |> head_of; |
638 |> head_of; |
637 |
639 |
638 val maybe_rhs = concl |> perhaps (try (HOLogic.dest_not)) |> try (snd o HOLogic.dest_eq); |
640 val maybe_rhs = concl |> perhaps (try (HOLogic.dest_not)) |> try (snd o HOLogic.dest_eq); |
639 |
641 |
640 val discs = maps (map #disc) ctr_specss; |
642 val discs = maps (map #disc) basic_ctr_specss; |
641 val sels = maps (maps #sels) ctr_specss; |
643 val sels = maps (maps #sels) basic_ctr_specss; |
642 val ctrs = maps (map #ctr) ctr_specss; |
644 val ctrs = maps (map #ctr) basic_ctr_specss; |
643 in |
645 in |
644 if member (op =) discs head orelse |
646 if member (op =) discs head orelse |
645 is_some maybe_rhs andalso |
647 is_some maybe_rhs andalso |
646 member (op =) (filter (null o binder_types o fastype_of) ctrs) (the maybe_rhs) then |
648 member (op =) (filter (null o binder_types o fastype_of) ctrs) (the maybe_rhs) then |
647 dissect_coeqn_disc seq fun_names ctr_specss NONE NONE prems concl matchedsss |
649 dissect_coeqn_disc seq fun_names basic_ctr_specss NONE NONE prems concl matchedsss |
648 |>> single |
650 |>> single |
649 else if member (op =) sels head then |
651 else if member (op =) sels head then |
650 ([dissect_coeqn_sel fun_names ctr_specss eqn' of_spec concl], matchedsss) |
652 ([dissect_coeqn_sel fun_names basic_ctr_specss eqn' of_spec concl], matchedsss) |
651 else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso |
653 else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso |
652 member (op =) ctrs (head_of (unfold_let (the maybe_rhs))) then |
654 member (op =) ctrs (head_of (unfold_let (the maybe_rhs))) then |
653 dissect_coeqn_ctr seq fun_names ctr_specss eqn' NONE prems concl matchedsss |
655 dissect_coeqn_ctr seq fun_names basic_ctr_specss eqn' NONE prems concl matchedsss |
654 else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso |
656 else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) andalso |
655 null prems then |
657 null prems then |
656 dissect_coeqn_code lthy has_call fun_names ctr_specss eqn' concl matchedsss |
658 dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn' concl matchedsss |
657 |>> flat |
659 |>> flat |
658 else |
660 else |
659 primrec_error_eqn "malformed function equation" eqn |
661 primrec_error_eqn "malformed function equation" eqn |
660 end; |
662 end; |
661 |
663 |
745 end; |
747 end; |
746 |
748 |
747 fun build_codefs lthy bs mxs has_call arg_Tss (corec_specs : corec_spec list) |
749 fun build_codefs lthy bs mxs has_call arg_Tss (corec_specs : corec_spec list) |
748 (disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) = |
750 (disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) = |
749 let |
751 let |
750 val corec_specs' = take (length bs) corec_specs; |
752 val corecs = map #corec corec_specs; |
751 val corecs = map #corec corec_specs'; |
753 val ctr_specss = map #ctr_specs corec_specs; |
752 val ctr_specss = map #ctr_specs corec_specs'; |
|
753 val corec_args = hd corecs |
754 val corec_args = hd corecs |
754 |> fst o split_last o binder_types o fastype_of |
755 |> fst o split_last o binder_types o fastype_of |
755 |> map (Const o pair @{const_name undefined}) |
756 |> map (Const o pair @{const_name undefined}) |
756 |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss |
757 |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss |
757 |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss; |
758 |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss; |
806 user_eqn = undef_const}; |
807 user_eqn = undef_const}; |
807 in |
808 in |
808 chop n disc_eqns ||> cons extra_disc_eqn |> (op @) |
809 chop n disc_eqns ||> cons extra_disc_eqn |> (op @) |
809 end; |
810 end; |
810 |
811 |
|
812 fun find_corec_calls has_call basic_ctr_specs {ctr, sel, rhs_term, ...} = |
|
813 let |
|
814 val sel_no = find_first (equal ctr o #ctr) basic_ctr_specs |
|
815 |> find_index (equal sel) o #sels o the; |
|
816 fun find (Abs (_, _, b)) = find b |
|
817 | find (t as _ $ _) = strip_comb t |>> find ||> maps find |> (op @) |
|
818 | find f = if is_Free f andalso has_call f then [f] else []; |
|
819 in |
|
820 find rhs_term |
|
821 |> K |> nth_map sel_no |> AList.map_entry (op =) ctr |
|
822 end; |
|
823 |
811 fun add_primcorec simple seq fixes specs of_specs lthy = |
824 fun add_primcorec simple seq fixes specs of_specs lthy = |
812 let |
825 let |
813 val (bs, mxs) = map_split (apfst fst) fixes; |
826 val (bs, mxs) = map_split (apfst fst) fixes; |
814 val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list; |
827 val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list; |
815 |
828 |
816 val callssss = []; (* FIXME *) |
829 val fun_names = map Binding.name_of bs; |
|
830 val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts; |
|
831 val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =)); |
|
832 val eqns_data = |
|
833 fold_map2 (dissect_coeqn lthy seq has_call fun_names basic_ctr_specss) (map snd specs) |
|
834 of_specs [] |
|
835 |> flat o fst; |
|
836 |
|
837 val callssss = |
|
838 map_filter (try (fn Sel x => x)) eqns_data |
|
839 |> partition_eq ((op =) o pairself #fun_name) |
|
840 |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |
|
841 |> map (flat o snd) |> map2 (fold o find_corec_calls has_call) basic_ctr_specss |
|
842 |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} => |
|
843 (ctr, map (K []) sels))) basic_ctr_specss); |
|
844 |
|
845 (* |
|
846 val _ = tracing ("callssss = " ^ @{make_string} callssss); |
|
847 *) |
817 |
848 |
818 val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms, |
849 val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms, |
819 strong_coinduct_thms), lthy') = |
850 strong_coinduct_thms), lthy') = |
820 corec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy; |
851 corec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy; |
821 |
|
822 val actual_nn = length bs; |
852 val actual_nn = length bs; |
823 val fun_names = map Binding.name_of bs; |
|
824 val corec_specs = take actual_nn corec_specs'; (*###*) |
853 val corec_specs = take actual_nn corec_specs'; (*###*) |
825 |
|
826 val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =)); |
|
827 val eqns_data = |
|
828 fold_map2 (dissect_coeqn lthy seq has_call fun_names (map #ctr_specs corec_specs)) |
|
829 (map snd specs) of_specs [] |
|
830 |> flat o fst; |
|
831 |
854 |
832 val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data |
855 val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data |
833 |> partition_eq ((op =) o pairself #fun_name) |
856 |> partition_eq ((op =) o pairself #fun_name) |
834 |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |
857 |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |
835 |> map (sort ((op <) o pairself #ctr_no |> make_ord) o flat o snd); |
858 |> map (sort ((op <) o pairself #ctr_no |> make_ord) o flat o snd); |