author | blanchet |
Tue, 02 Jan 2018 16:40:54 +0100 | |
changeset 67320 | 6afba546f0e5 |
parent 67317 | 15ea49331fc7 |
child 68961 | 22a3790eecae |
permissions | -rw-r--r-- |
58309
a09ec6daaa19
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet
parents:
58305
diff
changeset
|
1 |
(* Title: HOL/Datatype_Examples/Compat.thy |
57634 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Copyright 2014 |
|
4 |
||
5 |
Tests for compatibility with the old datatype package. |
|
6 |
*) |
|
7 |
||
63167 | 8 |
section \<open>Tests for Compatibility with the Old Datatype Package\<close> |
57634 | 9 |
|
56454 | 10 |
theory Compat |
67320 | 11 |
imports Main |
56454 | 12 |
begin |
13 |
||
63167 | 14 |
subsection \<open>Viewing and Registering New-Style Datatypes as Old-Style Ones\<close> |
58125 | 15 |
|
63167 | 16 |
ML \<open> |
58124 | 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)), |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
25 |
these (Option.map #descr (BNF_LFP_Compat.get_info thy [] T_name)), |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
26 |
these (Option.map #descr (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] T_name))) |
58124 | 27 |
|> tap (check_lens lens); |
63167 | 28 |
\<close> |
58124 | 29 |
|
58310 | 30 |
datatype 'b w = W | W' "'b w \<times> 'b list" |
58124 | 31 |
|
63167 | 32 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name w}\<close> |
58358 | 33 |
|
56454 | 34 |
datatype_compat w |
35 |
||
63167 | 36 |
ML \<open>get_descrs @{theory} (2, 2, 1) @{type_name w}\<close> |
58124 | 37 |
|
58310 | 38 |
datatype ('c, 'b) s = L 'c | R 'b |
58124 | 39 |
|
63167 | 40 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name s}\<close> |
58124 | 41 |
|
67317
15ea49331fc7
don't test 'old_datatype', which is on its way out
blanchet
parents:
66453
diff
changeset
|
42 |
datatype 'd x = X | X' "('d x list, 'd list) s" |
58124 | 43 |
|
63167 | 44 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name x}\<close> |
58124 | 45 |
|
56454 | 46 |
datatype_compat s |
58124 | 47 |
|
63167 | 48 |
ML \<open>get_descrs @{theory} (1, 1, 1) @{type_name s}\<close> |
49 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name x}\<close> |
|
58124 | 50 |
|
56454 | 51 |
datatype_compat x |
52 |
||
63167 | 53 |
ML \<open>get_descrs @{theory} (3, 3, 1) @{type_name x}\<close> |
58124 | 54 |
|
58216 | 55 |
thm x.induct x.rec |
56 |
thm compat_x.induct compat_x.rec |
|
57 |
||
67317
15ea49331fc7
don't test 'old_datatype', which is on its way out
blanchet
parents:
66453
diff
changeset
|
58 |
datatype 'a tttre = TTTre 'a "'a tttre list list list" |
58124 | 59 |
|
63167 | 60 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name tttre}\<close> |
58124 | 61 |
|
56454 | 62 |
datatype_compat tttre |
63 |
||
63167 | 64 |
ML \<open>get_descrs @{theory} (4, 4, 1) @{type_name tttre}\<close> |
58124 | 65 |
|
58216 | 66 |
thm tttre.induct tttre.rec |
67 |
thm compat_tttre.induct compat_tttre.rec |
|
68 |
||
67317
15ea49331fc7
don't test 'old_datatype', which is on its way out
blanchet
parents:
66453
diff
changeset
|
69 |
datatype 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre list" |
58124 | 70 |
|
63167 | 71 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name ftre}\<close> |
58124 | 72 |
|
56454 | 73 |
datatype_compat ftre |
74 |
||
63167 | 75 |
ML \<open>get_descrs @{theory} (2, 2, 1) @{type_name ftre}\<close> |
58124 | 76 |
|
58216 | 77 |
thm ftre.induct ftre.rec |
78 |
thm compat_ftre.induct compat_ftre.rec |
|
79 |
||
67317
15ea49331fc7
don't test 'old_datatype', which is on its way out
blanchet
parents:
66453
diff
changeset
|
80 |
datatype 'a btre = BTre 'a "'a btre list" "'a btre list" |
58124 | 81 |
|
63167 | 82 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name btre}\<close> |
58124 | 83 |
|
56454 | 84 |
datatype_compat btre |
85 |
||
63167 | 86 |
ML \<open>get_descrs @{theory} (3, 3, 1) @{type_name btre}\<close> |
58124 | 87 |
|
58216 | 88 |
thm btre.induct btre.rec |
89 |
thm compat_btre.induct compat_btre.rec |
|
90 |
||
58310 | 91 |
datatype 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo" |
58124 | 92 |
|
63167 | 93 |
ML \<open>get_descrs @{theory} (0, 2, 2) @{type_name foo}\<close> |
94 |
ML \<open>get_descrs @{theory} (0, 2, 2) @{type_name bar}\<close> |
|
58124 | 95 |
|
56454 | 96 |
datatype_compat foo bar |
97 |
||
63167 | 98 |
ML \<open>get_descrs @{theory} (2, 2, 2) @{type_name foo}\<close> |
99 |
ML \<open>get_descrs @{theory} (2, 2, 2) @{type_name bar}\<close> |
|
58124 | 100 |
|
67317
15ea49331fc7
don't test 'old_datatype', which is on its way out
blanchet
parents:
66453
diff
changeset
|
101 |
datatype 'a tre = Tre 'a "'a tre list" |
58124 | 102 |
|
63167 | 103 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name tre}\<close> |
58124 | 104 |
|
56454 | 105 |
datatype_compat tre |
106 |
||
63167 | 107 |
ML \<open>get_descrs @{theory} (2, 2, 1) @{type_name tre}\<close> |
58124 | 108 |
|
58216 | 109 |
thm tre.induct tre.rec |
110 |
thm compat_tre.induct compat_tre.rec |
|
56454 | 111 |
|
58310 | 112 |
datatype 'a f = F 'a and 'a g = G 'a |
58124 | 113 |
|
63167 | 114 |
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> |
|
58124 | 116 |
|
58310 | 117 |
datatype h = H "h f" | H' |
58124 | 118 |
|
63167 | 119 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name h}\<close> |
58124 | 120 |
|
56454 | 121 |
datatype_compat f g |
58124 | 122 |
|
63167 | 123 |
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> |
|
125 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name h}\<close> |
|
58124 | 126 |
|
56454 | 127 |
datatype_compat h |
128 |
||
63167 | 129 |
ML \<open>get_descrs @{theory} (3, 3, 1) @{type_name h}\<close> |
58124 | 130 |
|
58216 | 131 |
thm h.induct h.rec |
132 |
thm compat_h.induct compat_h.rec |
|
133 |
||
58310 | 134 |
datatype myunit = MyUnity |
58124 | 135 |
|
63167 | 136 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name myunit}\<close> |
58124 | 137 |
|
56454 | 138 |
datatype_compat myunit |
139 |
||
63167 | 140 |
ML \<open>get_descrs @{theory} (1, 1, 1) @{type_name myunit}\<close> |
58124 | 141 |
|
58310 | 142 |
datatype mylist = MyNil | MyCons nat mylist |
58124 | 143 |
|
63167 | 144 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name mylist}\<close> |
58124 | 145 |
|
56454 | 146 |
datatype_compat mylist |
147 |
||
63167 | 148 |
ML \<open>get_descrs @{theory} (1, 1, 1) @{type_name mylist}\<close> |
58124 | 149 |
|
58310 | 150 |
datatype foo' = FooNil | FooCons bar' foo' and bar' = Bar |
58124 | 151 |
|
63167 | 152 |
ML \<open>get_descrs @{theory} (0, 2, 2) @{type_name foo'}\<close> |
153 |
ML \<open>get_descrs @{theory} (0, 2, 2) @{type_name bar'}\<close> |
|
58124 | 154 |
|
56454 | 155 |
datatype_compat bar' foo' |
156 |
||
63167 | 157 |
ML \<open>get_descrs @{theory} (2, 2, 2) @{type_name foo'}\<close> |
158 |
ML \<open>get_descrs @{theory} (2, 2, 2) @{type_name bar'}\<close> |
|
58124 | 159 |
|
58310 | 160 |
datatype tree = Tree "tree foo" |
58124 | 161 |
|
63167 | 162 |
ML \<open>get_descrs @{theory} (0, 1, 1) @{type_name tree}\<close> |
58124 | 163 |
|
56488 | 164 |
datatype_compat tree |
56454 | 165 |
|
63167 | 166 |
ML \<open>get_descrs @{theory} (3, 3, 1) @{type_name tree}\<close> |
58125 | 167 |
|
58216 | 168 |
thm tree.induct tree.rec |
169 |
thm compat_tree.induct compat_tree.rec |
|
58125 | 170 |
|
58216 | 171 |
|
63167 | 172 |
subsection \<open>Creating New-Style Datatypes Using Old-Style Interfaces\<close> |
58125 | 173 |
|
63167 | 174 |
ML \<open> |
58125 | 175 |
val l_specs = |
176 |
[((@{binding l}, [("'a", @{sort type})], NoSyn), |
|
177 |
[(@{binding N}, [], NoSyn), |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
178 |
(@{binding C}, [@{typ 'a}, Type (Sign.full_name @{theory} @{binding l}, [@{typ 'a}])], |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
179 |
NoSyn)])]; |
63167 | 180 |
\<close> |
58125 | 181 |
|
63167 | 182 |
setup \<open>snd o BNF_LFP_Compat.add_datatype [] l_specs\<close> |
58125 | 183 |
|
63167 | 184 |
ML \<open>get_descrs @{theory} (1, 1, 1) @{type_name l}\<close> |
58125 | 185 |
|
186 |
thm l.exhaust l.map l.induct l.rec l.size |
|
187 |
||
63167 | 188 |
ML \<open> |
58125 | 189 |
val t_specs = |
190 |
[((@{binding t}, [("'b", @{sort type})], NoSyn), |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
191 |
[(@{binding T}, [@{typ 'b}, |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
192 |
Type (@{type_name l}, [Type (Sign.full_name @{theory} @{binding t}, [@{typ 'b}])])], |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
193 |
NoSyn)])]; |
63167 | 194 |
\<close> |
58125 | 195 |
|
63167 | 196 |
setup \<open>snd o BNF_LFP_Compat.add_datatype [] t_specs\<close> |
58125 | 197 |
|
63167 | 198 |
ML \<open>get_descrs @{theory} (2, 2, 1) @{type_name t}\<close> |
58125 | 199 |
|
200 |
thm t.exhaust t.map t.induct t.rec t.size |
|
58216 | 201 |
thm compat_t.induct compat_t.rec |
202 |
||
63167 | 203 |
ML \<open> |
58216 | 204 |
val ft_specs = |
205 |
[((@{binding ft}, [("'a", @{sort type})], NoSyn), |
|
206 |
[(@{binding FT0}, [], NoSyn), |
|
207 |
(@{binding FT}, [@{typ 'a} --> Type (Sign.full_name @{theory} @{binding ft}, [@{typ 'a}])], |
|
208 |
NoSyn)])]; |
|
63167 | 209 |
\<close> |
58216 | 210 |
|
63167 | 211 |
setup \<open>snd o BNF_LFP_Compat.add_datatype [] ft_specs\<close> |
58216 | 212 |
|
63167 | 213 |
ML \<open>get_descrs @{theory} (1, 1, 1) @{type_name ft}\<close> |
58216 | 214 |
|
215 |
thm ft.exhaust ft.induct ft.rec ft.size |
|
216 |
thm compat_ft.induct compat_ft.rec |
|
56454 | 217 |
|
218 |
end |