author | blanchet |
Mon, 08 Sep 2014 14:03:02 +0200 | |
changeset 58216 | e02d867dfbc6 |
parent 58150 | 2bf3ed0f62cf |
child 58305 | 57752a91eec4 |
permissions | -rw-r--r-- |
57634 | 1 |
(* Title: HOL/BNF_Examples/Compat.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
Copyright 2014 |
|
4 |
||
5 |
Tests for compatibility with the old datatype package. |
|
6 |
*) |
|
7 |
||
58125 | 8 |
header \<open> Tests for Compatibility with the Old Datatype Package \<close> |
57634 | 9 |
|
56454 | 10 |
theory Compat |
11 |
imports Main |
|
12 |
begin |
|
13 |
||
58125 | 14 |
subsection \<open> Viewing and Registering New-Style Datatypes as Old-Style Ones \<close> |
15 |
||
58124 | 16 |
ML \<open> |
17 |
fun check_len n xs label = |
|
18 |
length xs = n orelse error ("Expected length " ^ string_of_int (length xs) ^ " for " ^ label); |
|
19 |
||
20 |
fun check_lens (n1, n2, n3) (xs1, xs2, xs3) = |
|
21 |
check_len n1 xs1 "old" andalso check_len n2 xs2 "unfold" andalso check_len n3 xs3 "keep"; |
|
22 |
||
23 |
fun get_descrs thy lens T_name = |
|
24 |
(these (Option.map #descr (Old_Datatype_Data.get_info thy T_name)), |
|
25 |
these (Option.map #descr (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting T_name)), |
|
26 |
these (Option.map #descr (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting T_name))) |
|
27 |
|> tap (check_lens lens); |
|
28 |
\<close> |
|
29 |
||
30 |
datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst" |
|
31 |
||
58125 | 32 |
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name old_lst}; \<close> |
58124 | 33 |
|
56454 | 34 |
datatype_new 'a lst = Nl | Cns 'a "'a lst" |
58124 | 35 |
|
58125 | 36 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name lst}; \<close> |
58124 | 37 |
|
56454 | 38 |
datatype_compat lst |
39 |
||
58125 | 40 |
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name lst}; \<close> |
58124 | 41 |
|
56456 | 42 |
datatype_new 'b w = W | W' "'b w \<times> 'b list" |
58124 | 43 |
|
44 |
(* no support for sums of products: |
|
56454 | 45 |
datatype_compat w |
46 |
*) |
|
47 |
||
58125 | 48 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name w}; \<close> |
58124 | 49 |
|
56454 | 50 |
datatype_new ('c, 'b) s = L 'c | R 'b |
58124 | 51 |
|
58125 | 52 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name s}; \<close> |
58124 | 53 |
|
56454 | 54 |
datatype_new 'd x = X | X' "('d x lst, 'd list) s" |
58124 | 55 |
|
58125 | 56 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name x}; \<close> |
58124 | 57 |
|
56454 | 58 |
datatype_compat s |
58124 | 59 |
|
58125 | 60 |
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name s}; \<close> |
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58125
diff
changeset
|
61 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name x}; \<close> |
58124 | 62 |
|
56454 | 63 |
datatype_compat x |
64 |
||
58125 | 65 |
ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name x}; \<close> |
58124 | 66 |
|
58216 | 67 |
thm x.induct x.rec |
68 |
thm compat_x.induct compat_x.rec |
|
69 |
||
56454 | 70 |
datatype_new 'a tttre = TTTre 'a "'a tttre lst lst lst" |
58124 | 71 |
|
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58125
diff
changeset
|
72 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tttre}; \<close> |
58124 | 73 |
|
56454 | 74 |
datatype_compat tttre |
75 |
||
58125 | 76 |
ML \<open> get_descrs @{theory} (4, 4, 1) @{type_name tttre}; \<close> |
58124 | 77 |
|
58216 | 78 |
thm tttre.induct tttre.rec |
79 |
thm compat_tttre.induct compat_tttre.rec |
|
80 |
||
56454 | 81 |
datatype_new 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst" |
58124 | 82 |
|
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58125
diff
changeset
|
83 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name ftre}; \<close> |
58124 | 84 |
|
56454 | 85 |
datatype_compat ftre |
86 |
||
58125 | 87 |
ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name ftre}; \<close> |
58124 | 88 |
|
58216 | 89 |
thm ftre.induct ftre.rec |
90 |
thm compat_ftre.induct compat_ftre.rec |
|
91 |
||
56454 | 92 |
datatype_new 'a btre = BTre 'a "'a btre lst" "'a btre lst" |
58124 | 93 |
|
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58125
diff
changeset
|
94 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name btre}; \<close> |
58124 | 95 |
|
56454 | 96 |
datatype_compat btre |
97 |
||
58125 | 98 |
ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name btre}; \<close> |
58124 | 99 |
|
58216 | 100 |
thm btre.induct btre.rec |
101 |
thm compat_btre.induct compat_btre.rec |
|
102 |
||
56454 | 103 |
datatype_new 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo" |
58124 | 104 |
|
58125 | 105 |
ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo}; \<close> |
106 |
ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar}; \<close> |
|
58124 | 107 |
|
56454 | 108 |
datatype_compat foo bar |
109 |
||
58125 | 110 |
ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo}; \<close> |
111 |
ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar}; \<close> |
|
58124 | 112 |
|
56454 | 113 |
datatype_new 'a tre = Tre 'a "'a tre lst" |
58124 | 114 |
|
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58125
diff
changeset
|
115 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tre}; \<close> |
58124 | 116 |
|
56454 | 117 |
datatype_compat tre |
118 |
||
58125 | 119 |
ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name tre}; \<close> |
58124 | 120 |
|
58216 | 121 |
thm tre.induct tre.rec |
122 |
thm compat_tre.induct compat_tre.rec |
|
56454 | 123 |
|
124 |
datatype_new 'a f = F 'a and 'a g = G 'a |
|
58124 | 125 |
|
58125 | 126 |
ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name f}; \<close> |
127 |
ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name g}; \<close> |
|
58124 | 128 |
|
56454 | 129 |
datatype_new h = H "h f" | H' |
58124 | 130 |
|
58125 | 131 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name h}; \<close> |
58124 | 132 |
|
56454 | 133 |
datatype_compat f g |
58124 | 134 |
|
58125 | 135 |
ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name f}; \<close> |
136 |
ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name g}; \<close> |
|
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58125
diff
changeset
|
137 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name h}; \<close> |
58124 | 138 |
|
56454 | 139 |
datatype_compat h |
140 |
||
58125 | 141 |
ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name h}; \<close> |
58124 | 142 |
|
58216 | 143 |
thm h.induct h.rec |
144 |
thm compat_h.induct compat_h.rec |
|
145 |
||
56454 | 146 |
datatype_new myunit = MyUnity |
58124 | 147 |
|
58125 | 148 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name myunit}; \<close> |
58124 | 149 |
|
56454 | 150 |
datatype_compat myunit |
151 |
||
58125 | 152 |
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name myunit}; \<close> |
58124 | 153 |
|
56454 | 154 |
datatype_new mylist = MyNil | MyCons nat mylist |
58124 | 155 |
|
58125 | 156 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name mylist}; \<close> |
58124 | 157 |
|
56454 | 158 |
datatype_compat mylist |
159 |
||
58125 | 160 |
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name mylist}; \<close> |
58124 | 161 |
|
56454 | 162 |
datatype_new foo' = FooNil | FooCons bar' foo' and bar' = Bar |
58124 | 163 |
|
58125 | 164 |
ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo'}; \<close> |
165 |
ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar'}; \<close> |
|
58124 | 166 |
|
56454 | 167 |
datatype_compat bar' foo' |
168 |
||
58125 | 169 |
ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo'}; \<close> |
170 |
ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar'}; \<close> |
|
58124 | 171 |
|
56454 | 172 |
datatype funky = Funky "funky tre" | Funky' |
58124 | 173 |
|
58125 | 174 |
ML \<open> get_descrs @{theory} (3, 3, 3) @{type_name funky}; \<close> |
58124 | 175 |
|
56454 | 176 |
datatype fnky = Fnky "nat tre" |
177 |
||
58125 | 178 |
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name fnky}; \<close> |
58124 | 179 |
|
56454 | 180 |
datatype_new tree = Tree "tree foo" |
58124 | 181 |
|
58131
1abeda3c3bc2
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
blanchet
parents:
58125
diff
changeset
|
182 |
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tree}; \<close> |
58124 | 183 |
|
56488 | 184 |
datatype_compat tree |
56454 | 185 |
|
58125 | 186 |
ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name tree}; \<close> |
187 |
||
58216 | 188 |
thm tree.induct tree.rec |
189 |
thm compat_tree.induct compat_tree.rec |
|
58125 | 190 |
|
58216 | 191 |
|
192 |
subsection \<open> Creating New-Style Datatypes Using Old-Style Interfaces \<close> |
|
58125 | 193 |
|
194 |
ML \<open> |
|
195 |
val l_specs = |
|
196 |
[((@{binding l}, [("'a", @{sort type})], NoSyn), |
|
197 |
[(@{binding N}, [], NoSyn), |
|
198 |
(@{binding C}, [@{typ 'a}, Type (Sign.full_name @{theory} @{binding l}, [@{typ 'a}])], NoSyn)])]; |
|
199 |
\<close> |
|
200 |
||
58216 | 201 |
setup \<open> snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting l_specs; \<close> |
58125 | 202 |
|
203 |
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name l}; \<close> |
|
204 |
||
205 |
thm l.exhaust l.map l.induct l.rec l.size |
|
206 |
||
207 |
ML \<open> |
|
208 |
val t_specs = |
|
209 |
[((@{binding t}, [("'b", @{sort type})], NoSyn), |
|
210 |
[(@{binding T}, [@{typ 'b}, Type (@{type_name l}, |
|
211 |
[Type (Sign.full_name @{theory} @{binding t}, [@{typ 'b}])])], NoSyn)])]; |
|
212 |
\<close> |
|
213 |
||
58216 | 214 |
setup \<open> snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting t_specs; \<close> |
58125 | 215 |
|
216 |
ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name t}; \<close> |
|
217 |
||
218 |
thm t.exhaust t.map t.induct t.rec t.size |
|
58216 | 219 |
thm compat_t.induct compat_t.rec |
220 |
||
221 |
ML \<open> |
|
222 |
val ft_specs = |
|
223 |
[((@{binding ft}, [("'a", @{sort type})], NoSyn), |
|
224 |
[(@{binding FT0}, [], NoSyn), |
|
225 |
(@{binding FT}, [@{typ 'a} --> Type (Sign.full_name @{theory} @{binding ft}, [@{typ 'a}])], |
|
226 |
NoSyn)])]; |
|
227 |
\<close> |
|
228 |
||
229 |
setup \<open> snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting ft_specs; \<close> |
|
230 |
||
231 |
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name ft}; \<close> |
|
232 |
||
233 |
thm ft.exhaust ft.induct ft.rec ft.size |
|
234 |
thm compat_ft.induct compat_ft.rec |
|
56454 | 235 |
|
236 |
end |