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 *) |
8 (* info of raw binding functions *) |
12 type bn_info = term * int * (int * term option) list list |
9 type bn_info = term * int * (int * term option) list list |
13 |
10 |
14 (* binding modes and binding clauses *) |
11 (* binding modes and binding clauses *) |
15 datatype bmode = Lst | Res | Set |
12 datatype bmode = Lst | Res | Set |
26 val the_info: Proof.context -> string -> info |
23 val the_info: Proof.context -> string -> info |
27 val register_info: (string * info) -> Context.generic -> Context.generic |
24 val register_info: (string * info) -> Context.generic -> Context.generic |
28 val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list |
25 val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list |
29 |
26 |
30 datatype user_data = UserData of |
27 datatype user_data = UserData of |
31 {dts : dt_info, |
28 {dts : Datatype.spec list, |
32 cn_names : string list, |
29 cn_names : string list, |
33 cn_tys : (string * string) list, |
30 cn_tys : (string * string) list, |
34 bn_funs : (binding * typ * mixfix) list, |
31 bn_funs : (binding * typ * mixfix) list, |
35 bn_eqs : (Attrib.binding * term) list, |
32 bn_eqs : (Attrib.binding * term) list, |
36 bclauses : bclause list list list} |
33 bclauses : bclause list list list} |
37 |
34 |
38 datatype raw_dt_info = RawDtInfo of |
35 datatype raw_dt_info = RawDtInfo of |
39 {raw_dt_names : string list, |
36 {raw_dt_names : string list, |
40 raw_dts : dt_info, |
37 raw_dts : Datatype.spec list, |
41 raw_tys : typ list, |
38 raw_tys : typ list, |
42 raw_ty_args : (string * sort) list, |
39 raw_ty_args : (string * sort) list, |
43 raw_cns_info : cns_info list, |
40 raw_cns_info : cns_info list, |
44 raw_all_cns : term list list, |
41 raw_all_cns : term list list, |
45 raw_inject_thms : thm list, |
42 raw_inject_thms : thm list, |
63 |
60 |
64 end |
61 end |
65 |
62 |
66 structure Nominal_Dt_Data: NOMINAL_DT_DATA = |
63 structure Nominal_Dt_Data: NOMINAL_DT_DATA = |
67 struct |
64 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 |
65 |
76 |
66 |
77 (* term - is constant of the bn-function |
67 (* term - is constant of the bn-function |
78 int - is datatype number over which the bn-function is defined |
68 int - is datatype number over which the bn-function is defined |
79 int * term option - is number of the corresponding argument with possibly |
69 int * term option - is number of the corresponding argument with possibly |
119 map aux ty_names |
109 map aux ty_names |
120 end |
110 end |
121 |
111 |
122 |
112 |
123 datatype user_data = UserData of |
113 datatype user_data = UserData of |
124 {dts : dt_info, |
114 {dts : Datatype.spec list, |
125 cn_names : string list, |
115 cn_names : string list, |
126 cn_tys : (string * string) list, |
116 cn_tys : (string * string) list, |
127 bn_funs : (binding * typ * mixfix) list, |
117 bn_funs : (binding * typ * mixfix) list, |
128 bn_eqs : (Attrib.binding * term) list, |
118 bn_eqs : (Attrib.binding * term) list, |
129 bclauses : bclause list list list} |
119 bclauses : bclause list list list} |
130 |
120 |
131 datatype raw_dt_info = RawDtInfo of |
121 datatype raw_dt_info = RawDtInfo of |
132 {raw_dt_names : string list, |
122 {raw_dt_names : string list, |
133 raw_dts : dt_info, |
123 raw_dts : Datatype.spec list, |
134 raw_tys : typ list, |
124 raw_tys : typ list, |
135 raw_ty_args : (string * sort) list, |
125 raw_ty_args : (string * sort) list, |
136 raw_cns_info : cns_info list, |
126 raw_cns_info : cns_info list, |
137 raw_all_cns : term list list, |
127 raw_all_cns : term list list, |
138 raw_inject_thms : thm list, |
128 raw_inject_thms : thm list, |