25 |> tap (check_lens lens); |
27 |> tap (check_lens lens); |
26 \<close> |
28 \<close> |
27 |
29 |
28 datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst" |
30 datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst" |
29 |
31 |
30 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name old_lst} \<close> |
32 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name old_lst}; \<close> |
31 |
33 |
32 datatype_new 'a lst = Nl | Cns 'a "'a lst" |
34 datatype_new 'a lst = Nl | Cns 'a "'a lst" |
33 |
35 |
34 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name lst} \<close> |
36 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name lst}; \<close> |
35 |
37 |
36 datatype_compat lst |
38 datatype_compat lst |
37 |
39 |
38 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name lst} \<close> |
40 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name lst}; \<close> |
39 |
41 |
40 datatype_new 'b w = W | W' "'b w \<times> 'b list" |
42 datatype_new 'b w = W | W' "'b w \<times> 'b list" |
41 |
43 |
42 (* no support for sums of products: |
44 (* no support for sums of products: |
43 datatype_compat w |
45 datatype_compat w |
44 *) |
46 *) |
45 |
47 |
46 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name w} \<close> |
48 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name w}; \<close> |
47 |
49 |
48 datatype_new ('c, 'b) s = L 'c | R 'b |
50 datatype_new ('c, 'b) s = L 'c | R 'b |
49 |
51 |
50 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name s} \<close> |
52 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name s}; \<close> |
51 |
53 |
52 datatype_new 'd x = X | X' "('d x lst, 'd list) s" |
54 datatype_new 'd x = X | X' "('d x lst, 'd list) s" |
53 |
55 |
54 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name x} \<close> |
56 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name x}; \<close> |
55 |
57 |
56 datatype_compat s |
58 datatype_compat s |
57 |
59 |
58 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name s} \<close> |
60 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name s}; \<close> |
59 ML \<open> get_descrs @{theory} (0, 3, 1) @{type_name x} \<close> |
61 ML \<open> get_descrs @{theory} (0, 3, 1) @{type_name x}; \<close> |
60 |
62 |
61 datatype_compat x |
63 datatype_compat x |
62 |
64 |
63 ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name x} \<close> |
65 ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name x}; \<close> |
64 |
66 |
65 datatype_new 'a tttre = TTTre 'a "'a tttre lst lst lst" |
67 datatype_new 'a tttre = TTTre 'a "'a tttre lst lst lst" |
66 |
68 |
67 ML \<open> get_descrs @{theory} (0, 4, 1) @{type_name tttre} \<close> |
69 ML \<open> get_descrs @{theory} (0, 4, 1) @{type_name tttre}; \<close> |
68 |
70 |
69 datatype_compat tttre |
71 datatype_compat tttre |
70 |
72 |
71 ML \<open> get_descrs @{theory} (4, 4, 1) @{type_name tttre} \<close> |
73 ML \<open> get_descrs @{theory} (4, 4, 1) @{type_name tttre}; \<close> |
72 |
74 |
73 datatype_new 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst" |
75 datatype_new 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst" |
74 |
76 |
75 ML \<open> get_descrs @{theory} (0, 2, 1) @{type_name ftre} \<close> |
77 ML \<open> get_descrs @{theory} (0, 2, 1) @{type_name ftre}; \<close> |
76 |
78 |
77 datatype_compat ftre |
79 datatype_compat ftre |
78 |
80 |
79 ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name ftre} \<close> |
81 ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name ftre}; \<close> |
80 |
82 |
81 datatype_new 'a btre = BTre 'a "'a btre lst" "'a btre lst" |
83 datatype_new 'a btre = BTre 'a "'a btre lst" "'a btre lst" |
82 |
84 |
83 ML \<open> get_descrs @{theory} (0, 3, 1) @{type_name btre} \<close> |
85 ML \<open> get_descrs @{theory} (0, 3, 1) @{type_name btre}; \<close> |
84 |
86 |
85 datatype_compat btre |
87 datatype_compat btre |
86 |
88 |
87 ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name btre} \<close> |
89 ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name btre}; \<close> |
88 |
90 |
89 datatype_new 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo" |
91 datatype_new 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo" |
90 |
92 |
91 ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo} \<close> |
93 ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo}; \<close> |
92 ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar} \<close> |
94 ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar}; \<close> |
93 |
95 |
94 datatype_compat foo bar |
96 datatype_compat foo bar |
95 |
97 |
96 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo} \<close> |
98 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo}; \<close> |
97 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar} \<close> |
99 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar}; \<close> |
98 |
100 |
99 datatype_new 'a tre = Tre 'a "'a tre lst" |
101 datatype_new 'a tre = Tre 'a "'a tre lst" |
100 |
102 |
101 ML \<open> get_descrs @{theory} (0, 2, 1) @{type_name tre} \<close> |
103 ML \<open> get_descrs @{theory} (0, 2, 1) @{type_name tre}; \<close> |
102 |
104 |
103 datatype_compat tre |
105 datatype_compat tre |
104 |
106 |
105 ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name tre} \<close> |
107 ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name tre}; \<close> |
106 |
108 |
107 fun f_tre and f_tres where |
109 fun f_tre and f_tres where |
108 "f_tre (Tre a ts) = {a} \<union> f_tres ts" |
110 "f_tre (Tre a ts) = {a} \<union> f_tres ts" |
109 | "f_tres Nl = {}" |
111 | "f_tres Nl = {}" |
110 | "f_tres (Cns t ts) = f_tres ts" |
112 | "f_tres (Cns t ts) = f_tres ts" |
111 |
113 |
112 datatype_new 'a f = F 'a and 'a g = G 'a |
114 datatype_new 'a f = F 'a and 'a g = G 'a |
113 |
115 |
114 ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name f} \<close> |
116 ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name f}; \<close> |
115 ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name g} \<close> |
117 ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name g}; \<close> |
116 |
118 |
117 datatype_new h = H "h f" | H' |
119 datatype_new h = H "h f" | H' |
118 |
120 |
119 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name h} \<close> |
121 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name h}; \<close> |
120 |
122 |
121 datatype_compat f g |
123 datatype_compat f g |
122 |
124 |
123 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name f} \<close> |
125 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name f}; \<close> |
124 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name g} \<close> |
126 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name g}; \<close> |
125 ML \<open> get_descrs @{theory} (0, 3, 1) @{type_name h} \<close> |
127 ML \<open> get_descrs @{theory} (0, 3, 1) @{type_name h}; \<close> |
126 |
128 |
127 datatype_compat h |
129 datatype_compat h |
128 |
130 |
129 ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name h} \<close> |
131 ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name h}; \<close> |
130 |
132 |
131 datatype_new myunit = MyUnity |
133 datatype_new myunit = MyUnity |
132 |
134 |
133 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name myunit} \<close> |
135 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name myunit}; \<close> |
134 |
136 |
135 datatype_compat myunit |
137 datatype_compat myunit |
136 |
138 |
137 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name myunit} \<close> |
139 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name myunit}; \<close> |
138 |
140 |
139 datatype_new mylist = MyNil | MyCons nat mylist |
141 datatype_new mylist = MyNil | MyCons nat mylist |
140 |
142 |
141 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name mylist} \<close> |
143 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name mylist}; \<close> |
142 |
144 |
143 datatype_compat mylist |
145 datatype_compat mylist |
144 |
146 |
145 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name mylist} \<close> |
147 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name mylist}; \<close> |
146 |
148 |
147 fun f_mylist where |
149 fun f_mylist where |
148 "f_mylist MyNil = 0" |
150 "f_mylist MyNil = 0" |
149 | "f_mylist (MyCons _ xs) = Suc (f_mylist xs)" |
151 | "f_mylist (MyCons _ xs) = Suc (f_mylist xs)" |
150 |
152 |
151 datatype_new foo' = FooNil | FooCons bar' foo' and bar' = Bar |
153 datatype_new foo' = FooNil | FooCons bar' foo' and bar' = Bar |
152 |
154 |
153 ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo'} \<close> |
155 ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo'}; \<close> |
154 ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar'} \<close> |
156 ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar'}; \<close> |
155 |
157 |
156 datatype_compat bar' foo' |
158 datatype_compat bar' foo' |
157 |
159 |
158 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo'} \<close> |
160 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo'}; \<close> |
159 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar'} \<close> |
161 ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar'}; \<close> |
160 |
162 |
161 fun f_foo and f_bar where |
163 fun f_foo and f_bar where |
162 "f_foo FooNil = 0" |
164 "f_foo FooNil = 0" |
163 | "f_foo (FooCons bar foo) = Suc (f_foo foo) + f_bar bar" |
165 | "f_foo (FooCons bar foo) = Suc (f_foo foo) + f_bar bar" |
164 | "f_bar Bar = Suc 0" |
166 | "f_bar Bar = Suc 0" |
165 |
167 |
166 locale opt begin |
168 locale opt begin |
167 |
169 |
168 datatype_new 'a opt = Non | Som 'a |
170 datatype_new 'a opt = Non | Som 'a |
169 |
171 |
170 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name opt} \<close> |
172 ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name opt}; \<close> |
171 |
173 |
172 datatype_compat opt |
174 datatype_compat opt |
173 |
175 |
174 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name opt} \<close> |
176 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name opt}; \<close> |
175 |
177 |
176 end |
178 end |
177 |
179 |
178 datatype funky = Funky "funky tre" | Funky' |
180 datatype funky = Funky "funky tre" | Funky' |
179 |
181 |
180 ML \<open> get_descrs @{theory} (3, 3, 3) @{type_name funky} \<close> |
182 ML \<open> get_descrs @{theory} (3, 3, 3) @{type_name funky}; \<close> |
181 |
183 |
182 datatype fnky = Fnky "nat tre" |
184 datatype fnky = Fnky "nat tre" |
183 |
185 |
184 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name fnky} \<close> |
186 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name fnky}; \<close> |
185 |
187 |
186 datatype_new tree = Tree "tree foo" |
188 datatype_new tree = Tree "tree foo" |
187 |
189 |
188 ML \<open> get_descrs @{theory} (0, 3, 1) @{type_name tree} \<close> |
190 ML \<open> get_descrs @{theory} (0, 3, 1) @{type_name tree}; \<close> |
189 |
191 |
190 datatype_compat tree |
192 datatype_compat tree |
191 |
193 |
192 ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name tree} \<close> |
194 ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name tree}; \<close> |
|
195 |
|
196 |
|
197 subsection \<open> Creating a New-Style Datatype Using an Old-Style Interface \<close> |
|
198 |
|
199 ML \<open> |
|
200 val l_specs = |
|
201 [((@{binding l}, [("'a", @{sort type})], NoSyn), |
|
202 [(@{binding N}, [], NoSyn), |
|
203 (@{binding C}, [@{typ 'a}, Type (Sign.full_name @{theory} @{binding l}, [@{typ 'a}])], NoSyn)])]; |
|
204 \<close> |
|
205 |
|
206 setup \<open> snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting l_specs \<close> |
|
207 |
|
208 ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name l}; \<close> |
|
209 |
|
210 thm l.exhaust l.map l.induct l.rec l.size |
|
211 |
|
212 ML \<open> |
|
213 val t_specs = |
|
214 [((@{binding t}, [("'b", @{sort type})], NoSyn), |
|
215 [(@{binding T}, [@{typ 'b}, Type (@{type_name l}, |
|
216 [Type (Sign.full_name @{theory} @{binding t}, [@{typ 'b}])])], NoSyn)])]; |
|
217 \<close> |
|
218 |
|
219 setup \<open> snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting t_specs \<close> |
|
220 |
|
221 ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name t}; \<close> |
|
222 |
|
223 thm t.exhaust t.map t.induct t.rec t.size |
193 |
224 |
194 end |
225 end |