equal
deleted
inserted
replaced
623 val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs |
623 val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs |
624 in |
624 in |
625 map_index (prep_typ binds) annos |
625 map_index (prep_typ binds) annos |
626 end |
626 end |
627 |
627 |
628 in |
628 val result = map (map (map (map (fn (a, b, c) => |
629 map (map (map (map (fn (a, b, c) => (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type))))) |
629 (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type))))) |
630 (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) |
630 (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) |
|
631 |
|
632 val _ = warning (@{make_string} result) |
|
633 |
|
634 in |
|
635 result |
631 end |
636 end |
632 *} |
637 *} |
633 |
638 |
634 ML {* |
639 ML {* |
635 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
640 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
658 OuterSyntax.local_theory "nominal_datatype" "test" kind |
663 OuterSyntax.local_theory "nominal_datatype" "test" kind |
659 (main_parser >> nominal_datatype2_cmd) |
664 (main_parser >> nominal_datatype2_cmd) |
660 end |
665 end |
661 *} |
666 *} |
662 |
667 |
663 |
668 atom_decl name |
664 end |
669 |
665 |
670 nominal_datatype exp = |
666 |
671 EVar name |
667 |
672 | EUnit |
|
673 | EPair exp exp |
|
674 | ELetRec l::lrbs e::exp bind "b_lrbs l" in e |
|
675 |
|
676 and fnclause = |
|
677 K x::name p::pat f::exp bind "b_pat p" in f |
|
678 |
|
679 and fnclauses = |
|
680 S fnclause |
|
681 | ORs fnclause fnclauses |
|
682 |
|
683 and lrb = |
|
684 Clause fnclauses |
|
685 |
|
686 and lrbs = |
|
687 Single lrb |
|
688 | More lrb lrbs |
|
689 |
|
690 and pat = |
|
691 PVar name |
|
692 | PUnit |
|
693 | PPair pat pat |
|
694 |
|
695 binder |
|
696 b_lrbs :: "lrbs \<Rightarrow> atom set" and |
|
697 b_pat :: "pat \<Rightarrow> atom set" and |
|
698 b_fnclauses :: "fnclauses \<Rightarrow> atom set" and |
|
699 b_fnclause :: "fnclause \<Rightarrow> atom set" and |
|
700 b_lrb :: "lrb \<Rightarrow> atom set" |
|
701 |
|
702 where |
|
703 "b_lrbs (Single l) = b_lrb l" |
|
704 | "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls" |
|
705 | "b_pat (PVar x) = {atom x}" |
|
706 | "b_pat (PUnit) = {}" |
|
707 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2" |
|
708 | "b_fnclauses (S fc) = (b_fnclause fc)" |
|
709 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
|
710 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
|
711 | "b_fnclause (K x pat exp) = {atom x}" |
|
712 |
|
713 |
|
714 end |
|
715 |
|
716 |
|
717 |