18 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
18 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
19 val rsp_attrib = Attrib.internal (K Quotient_Info.rsp_rules_add) |
19 val rsp_attrib = Attrib.internal (K Quotient_Info.rsp_rules_add) |
20 |
20 |
21 *} |
21 *} |
22 |
22 |
23 |
23 ML {* print_depth 50 *} |
24 ML {* |
|
25 (* nominal datatype parser *) |
|
26 local |
|
27 structure P = Parse; |
|
28 structure S = Scan |
|
29 |
|
30 fun triple1 ((x, y), z) = (x, y, z) |
|
31 fun triple2 (x, (y, z)) = (x, y, z) |
|
32 fun tuple ((x, y, z), u) = (x, y, z, u) |
|
33 fun tswap (((x, y), z), u) = (x, y, u, z) |
|
34 in |
|
35 |
|
36 val _ = Keyword.keyword "bind" |
|
37 val _ = Keyword.keyword "bind_set" |
|
38 val _ = Keyword.keyword "bind_res" |
|
39 |
|
40 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ |
|
41 |
|
42 val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res" |
|
43 |
|
44 val bind_clauses = |
|
45 P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1) |
|
46 |
|
47 val cnstr_parser = |
|
48 P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap |
|
49 |
|
50 (* datatype parser *) |
|
51 val dt_parser = |
|
52 (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- |
|
53 (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple |
|
54 |
|
55 (* binding function parser *) |
|
56 val bnfun_parser = |
|
57 S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], []) |
|
58 |
|
59 (* main parser *) |
|
60 val main_parser = |
|
61 P.and_list1 dt_parser -- bnfun_parser >> triple2 |
|
62 |
|
63 end |
|
64 *} |
|
65 |
24 |
66 ML {* |
25 ML {* |
67 fun get_cnstrs dts = |
26 fun get_cnstrs dts = |
68 map (fn (_, _, _, constrs) => constrs) dts |
27 map (fn (_, _, _, constrs) => constrs) dts |
69 |
28 |
742 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) |
701 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) |
743 | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") |
702 | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") |
744 |
703 |
745 fun prep_body env bn_str = index_lookup env bn_str |
704 fun prep_body env bn_str = index_lookup env bn_str |
746 |
705 |
747 fun prep_mode "bind" = Lst |
|
748 | prep_mode "bind_set" = Set |
|
749 | prep_mode "bind_res" = Res |
|
750 |
|
751 fun prep_bclause env (mode, binders, bodies) = |
706 fun prep_bclause env (mode, binders, bodies) = |
752 let |
707 let |
753 val binders' = map (prep_binder env) binders |
708 val binders' = map (prep_binder env) binders |
754 val bodies' = map (prep_body env) bodies |
709 val bodies' = map (prep_body env) bodies |
755 in |
710 in |
756 BC (prep_mode mode, binders', bodies') |
711 BC (mode, binders', bodies') |
757 end |
712 end |
758 |
713 |
759 fun prep_bclauses (annos, bclause_strs) = |
714 fun prep_bclauses (annos, bclause_strs) = |
760 let |
715 let |
761 val env = indexify annos (* for every label, associate the index *) |
716 val env = indexify annos (* for every label, associate the index *) |
810 val bclauses = prepare_bclauses dt_strs lthy2 |
765 val bclauses = prepare_bclauses dt_strs lthy2 |
811 val bclauses' = complete dt_strs bclauses |
766 val bclauses' = complete dt_strs bclauses |
812 in |
767 in |
813 timeit (fn () => nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd) |
768 timeit (fn () => nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd) |
814 end |
769 end |
815 |
770 *} |
|
771 |
|
772 ML {* |
|
773 (* nominal datatype parser *) |
|
774 local |
|
775 structure P = Parse; |
|
776 structure S = Scan |
|
777 |
|
778 fun triple1 ((x, y), z) = (x, y, z) |
|
779 fun triple2 (x, (y, z)) = (x, y, z) |
|
780 fun tuple ((x, y, z), u) = (x, y, z, u) |
|
781 fun tswap (((x, y), z), u) = (x, y, u, z) |
|
782 in |
|
783 |
|
784 val _ = Keyword.keyword "bind" |
|
785 val _ = Keyword.keyword "set" |
|
786 val _ = Keyword.keyword "res" |
|
787 val _ = Keyword.keyword "list" |
|
788 |
|
789 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ |
|
790 |
|
791 val bind_mode = P.$$$ "bind" |-- |
|
792 S.optional (Args.parens |
|
793 (P.$$$ "list" >> K Lst || P.$$$ "set" >> K Set || P.$$$ "res" >> K Res)) Lst |
|
794 |
|
795 val bind_clauses = |
|
796 P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1) |
|
797 |
|
798 val cnstr_parser = |
|
799 P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap |
|
800 |
|
801 (* datatype parser *) |
|
802 val dt_parser = |
|
803 (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- |
|
804 (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple |
|
805 |
|
806 (* binding function parser *) |
|
807 val bnfun_parser = |
|
808 S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], []) |
|
809 |
|
810 (* main parser *) |
|
811 val main_parser = |
|
812 P.and_list1 dt_parser -- bnfun_parser >> triple2 |
|
813 |
|
814 end |
816 |
815 |
817 (* Command Keyword *) |
816 (* Command Keyword *) |
818 |
817 |
819 val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl |
818 val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl |
820 (main_parser >> nominal_datatype2_cmd) |
819 (main_parser >> nominal_datatype2_cmd) |