3 data about nominal datatypes |
3 data about nominal datatypes |
4 *) |
4 *) |
5 |
5 |
6 signature NOMINAL_DT_DATA = |
6 signature NOMINAL_DT_DATA = |
7 sig |
7 sig |
|
8 (* info of raw datatypes *) |
|
9 type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list |
|
10 |
|
11 (* info of raw binding functions *) |
|
12 type bn_info = term * int * (int * term option) list list |
|
13 |
|
14 (* binding modes and binding clauses *) |
|
15 datatype bmode = Lst | Res | Set |
|
16 datatype bclause = BC of bmode * (term option * int) list * int list |
|
17 |
8 type info = |
18 type info = |
9 {inject : thm list, |
19 {inject : thm list, |
10 distinct : thm list, |
20 distinct : thm list, |
11 strong_inducts : thm list, |
21 strong_inducts : thm list, |
12 strong_exhaust : thm list} |
22 strong_exhaust : thm list} |
13 |
23 |
14 val get_all_info: Proof.context -> (string * info) list |
24 val get_all_info: Proof.context -> (string * info) list |
15 val get_info: Proof.context -> string -> info option |
25 val get_info: Proof.context -> string -> info option |
16 val the_info: Proof.context -> string -> info |
26 val the_info: Proof.context -> string -> info |
17 val register_info: (string * info) -> Context.generic -> Context.generic |
27 val register_info: (string * info) -> Context.generic -> Context.generic |
18 val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list |
28 val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list |
|
29 |
|
30 datatype raw_dt_info = RawDtInfo of |
|
31 {raw_dt_names : string list, |
|
32 raw_dts : dt_info, |
|
33 raw_tys : typ list, |
|
34 raw_ty_args : (string * sort) list, |
|
35 raw_cns_info : cns_info list, |
|
36 raw_all_cns : term list list, |
|
37 raw_inject_thms : thm list, |
|
38 raw_distinct_thms : thm list, |
|
39 raw_induct_thm : thm, |
|
40 raw_induct_thms : thm list, |
|
41 raw_exhaust_thms : thm list, |
|
42 raw_size_trms : term list, |
|
43 raw_size_thms : thm list} |
19 |
44 |
20 datatype alpha_result = AlphaResult of |
45 datatype alpha_result = AlphaResult of |
21 {alpha_names : string list, |
46 {alpha_names : string list, |
22 alpha_trms : term list, |
47 alpha_trms : term list, |
23 alpha_tys : typ list, |
48 alpha_tys : typ list, |
30 |
55 |
31 end |
56 end |
32 |
57 |
33 structure Nominal_Dt_Data: NOMINAL_DT_DATA = |
58 structure Nominal_Dt_Data: NOMINAL_DT_DATA = |
34 struct |
59 struct |
|
60 |
|
61 (* string list - type variables of a datatype |
|
62 binding - name of the datatype |
|
63 mixfix - its mixfix |
|
64 (binding * typ list * mixfix) list - datatype constructors of the type |
|
65 *) |
|
66 type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list |
|
67 |
|
68 |
|
69 (* term - is constant of the bn-function |
|
70 int - is datatype number over which the bn-function is defined |
|
71 int * term option - is number of the corresponding argument with possibly |
|
72 recursive call with bn-function term |
|
73 *) |
|
74 type bn_info = term * int * (int * term option) list list |
|
75 |
|
76 datatype bmode = Lst | Res | Set |
|
77 datatype bclause = BC of bmode * (term option * int) list * int list |
35 |
78 |
36 |
79 |
37 (* information generated by nominal_datatype *) |
80 (* information generated by nominal_datatype *) |
38 type info = |
81 type info = |
39 {inject : thm list, |
82 {inject : thm list, |
66 }) |
109 }) |
67 in |
110 in |
68 map aux ty_names |
111 map aux ty_names |
69 end |
112 end |
70 |
113 |
|
114 |
|
115 datatype raw_dt_info = RawDtInfo of |
|
116 {raw_dt_names : string list, |
|
117 raw_dts : dt_info, |
|
118 raw_tys : typ list, |
|
119 raw_ty_args : (string * sort) list, |
|
120 raw_cns_info : cns_info list, |
|
121 raw_all_cns : term list list, |
|
122 raw_inject_thms : thm list, |
|
123 raw_distinct_thms : thm list, |
|
124 raw_induct_thm : thm, |
|
125 raw_induct_thms : thm list, |
|
126 raw_exhaust_thms : thm list, |
|
127 raw_size_trms : term list, |
|
128 raw_size_thms : thm list} |
|
129 |
71 datatype alpha_result = AlphaResult of |
130 datatype alpha_result = AlphaResult of |
72 {alpha_names : string list, |
131 {alpha_names : string list, |
73 alpha_trms : term list, |
132 alpha_trms : term list, |
74 alpha_tys : typ list, |
133 alpha_tys : typ list, |
75 alpha_bn_names : string list, |
134 alpha_bn_names : string list, |