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 user_data = UserData of |
|
31 {dts : dt_info, |
|
32 cn_names : string list, |
|
33 cn_tys : (string * string) list, |
|
34 bn_funs : (binding * typ * mixfix) list, |
|
35 bn_eqs : (Attrib.binding * term) list, |
|
36 bclauses : bclause list list list} |
|
37 |
|
38 datatype raw_dt_info = RawDtInfo of |
|
39 {raw_dt_names : string list, |
|
40 raw_dts : dt_info, |
|
41 raw_tys : typ list, |
|
42 raw_ty_args : (string * sort) list, |
|
43 raw_cns_info : cns_info list, |
|
44 raw_all_cns : term list list, |
|
45 raw_inject_thms : thm list, |
|
46 raw_distinct_thms : thm list, |
|
47 raw_induct_thm : thm, |
|
48 raw_induct_thms : thm list, |
|
49 raw_exhaust_thms : thm list, |
|
50 raw_size_trms : term list, |
|
51 raw_size_thms : thm list} |
19 |
52 |
20 datatype alpha_result = AlphaResult of |
53 datatype alpha_result = AlphaResult of |
21 {alpha_names : string list, |
54 {alpha_names : string list, |
22 alpha_trms : term list, |
55 alpha_trms : term list, |
23 alpha_tys : typ list, |
56 alpha_tys : typ list, |
30 |
63 |
31 end |
64 end |
32 |
65 |
33 structure Nominal_Dt_Data: NOMINAL_DT_DATA = |
66 structure Nominal_Dt_Data: NOMINAL_DT_DATA = |
34 struct |
67 struct |
|
68 |
|
69 (* string list - type variables of a datatype |
|
70 binding - name of the datatype |
|
71 mixfix - its mixfix |
|
72 (binding * typ list * mixfix) list - datatype constructors of the type |
|
73 *) |
|
74 type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list |
|
75 |
|
76 |
|
77 (* term - is constant of the bn-function |
|
78 int - is datatype number over which the bn-function is defined |
|
79 int * term option - is number of the corresponding argument with possibly |
|
80 recursive call with bn-function term |
|
81 *) |
|
82 type bn_info = term * int * (int * term option) list list |
|
83 |
|
84 datatype bmode = Lst | Res | Set |
|
85 datatype bclause = BC of bmode * (term option * int) list * int list |
35 |
86 |
36 |
87 |
37 (* information generated by nominal_datatype *) |
88 (* information generated by nominal_datatype *) |
38 type info = |
89 type info = |
39 {inject : thm list, |
90 {inject : thm list, |
66 }) |
117 }) |
67 in |
118 in |
68 map aux ty_names |
119 map aux ty_names |
69 end |
120 end |
70 |
121 |
|
122 |
|
123 datatype user_data = UserData of |
|
124 {dts : dt_info, |
|
125 cn_names : string list, |
|
126 cn_tys : (string * string) list, |
|
127 bn_funs : (binding * typ * mixfix) list, |
|
128 bn_eqs : (Attrib.binding * term) list, |
|
129 bclauses : bclause list list list} |
|
130 |
|
131 datatype raw_dt_info = RawDtInfo of |
|
132 {raw_dt_names : string list, |
|
133 raw_dts : dt_info, |
|
134 raw_tys : typ list, |
|
135 raw_ty_args : (string * sort) list, |
|
136 raw_cns_info : cns_info list, |
|
137 raw_all_cns : term list list, |
|
138 raw_inject_thms : thm list, |
|
139 raw_distinct_thms : thm list, |
|
140 raw_induct_thm : thm, |
|
141 raw_induct_thms : thm list, |
|
142 raw_exhaust_thms : thm list, |
|
143 raw_size_trms : term list, |
|
144 raw_size_thms : thm list} |
|
145 |
71 datatype alpha_result = AlphaResult of |
146 datatype alpha_result = AlphaResult of |
72 {alpha_names : string list, |
147 {alpha_names : string list, |
73 alpha_trms : term list, |
148 alpha_trms : term list, |
74 alpha_tys : typ list, |
149 alpha_tys : typ list, |
75 alpha_bn_names : string list, |
150 alpha_bn_names : string list, |