115 |
115 |
116 definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option" |
116 definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option" |
117 where |
117 where |
118 "full_small_fun f d = full_small_fun' f d d" |
118 "full_small_fun f d = full_small_fun' f d d" |
119 |
119 |
120 |
|
121 instance .. |
120 instance .. |
122 |
121 |
123 end |
122 end |
124 |
123 |
125 subsubsection {* A smarter enumeration scheme for functions over finite datatypes *} |
124 subsubsection {* A smarter enumeration scheme for functions over finite datatypes *} |
126 |
125 |
127 |
126 |
128 class check_all = enum + term_of + |
127 class check_all = enum + term_of + |
129 fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option" |
128 fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option" |
130 |
129 fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list" |
|
130 |
131 fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option" |
131 fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option" |
132 where |
132 where |
133 "check_all_n_lists f n = |
133 "check_all_n_lists f n = |
134 (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))" |
134 (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))" |
135 |
135 |
136 instantiation "fun" :: ("{equal, check_all}", check_all) check_all |
136 definition mk_map_term :: " (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term" |
137 begin |
137 where |
138 |
138 "mk_map_term T1 T2 domm rng = |
139 definition mk_map_term :: "'a list \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> unit \<Rightarrow> term" |
139 (%_. let T1 = T1 (); |
140 where |
|
141 "mk_map_term domm rng T2 = |
|
142 (%_. let T1 = (Typerep.typerep (TYPE('a))); |
|
143 T2 = T2 (); |
140 T2 = T2 (); |
144 update_term = (%g (a, b). |
141 update_term = (%g (a, b). |
145 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App |
142 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App |
146 (Code_Evaluation.Const (STR ''Fun.fun_upd'') |
143 (Code_Evaluation.Const (STR ''Fun.fun_upd'') |
147 (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], |
144 (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], |
148 Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) g) (Code_Evaluation.term_of a)) b) |
145 Typerep.Typerep (STR ''fun'') [T1, |
|
146 Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) |
|
147 g) a) b) |
149 in |
148 in |
150 List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip domm (rng ())))" |
149 List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))" |
151 |
150 |
152 definition |
151 instantiation "fun" :: ("{equal, check_all}", check_all) check_all |
153 "check_all f = check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip (Enum.enum\<Colon>'a list) ys), mk_map_term (Enum.enum::'a list) yst (%_. Typerep.typerep (TYPE('b))))) (Code_Numeral.of_nat (length (Enum.enum :: 'a list)))" |
152 begin |
154 |
153 |
|
154 definition |
|
155 "check_all f = |
|
156 (let |
|
157 mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a))); |
|
158 enum = (Enum.enum :: 'a list) |
|
159 in check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst)) (Code_Numeral.of_nat (length enum)))" |
|
160 |
|
161 definition enum_term_of_fun :: "('a => 'b) itself => unit => term list" |
|
162 where |
|
163 "enum_term_of_fun = (%_ _. let |
|
164 enum_term_of_a = enum_term_of (TYPE('a)); |
|
165 mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a |
|
166 in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))" |
|
167 |
155 instance .. |
168 instance .. |
156 |
169 |
157 end |
170 end |
158 |
171 |
159 |
172 |
172 begin |
189 begin |
173 |
190 |
174 definition |
191 definition |
175 "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))" |
192 "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))" |
176 |
193 |
|
194 definition enum_term_of_bool :: "bool itself => unit => term list" |
|
195 where |
|
196 "enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))" |
|
197 |
177 instance .. |
198 instance .. |
178 |
199 |
179 end |
200 end |
180 |
201 |
181 |
202 |
182 instantiation prod :: (check_all, check_all) check_all |
203 instantiation prod :: (check_all, check_all) check_all |
183 begin |
204 begin |
184 |
205 |
185 definition |
206 definition |
186 "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))))" |
207 "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))))" |
|
208 |
|
209 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list" |
|
210 where |
|
211 "enum_term_of_prod = (%_ _. map (%(x, y). Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) x) y) (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))" |
187 |
212 |
188 instance .. |
213 instance .. |
189 |
214 |
190 end |
215 end |
191 |
216 |
254 begin |
296 begin |
255 |
297 |
256 definition |
298 definition |
257 "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)" |
299 "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)" |
258 |
300 |
|
301 definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list" |
|
302 where |
|
303 "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])" |
|
304 |
259 instance .. |
305 instance .. |
260 |
306 |
261 end |
307 end |
262 |
308 |
263 instantiation Enum.finite_2 :: check_all |
309 instantiation Enum.finite_2 :: check_all |
264 begin |
310 begin |
265 |
311 |
266 definition |
312 definition |
267 "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))" |
313 "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))" |
268 |
314 |
|
315 definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list" |
|
316 where |
|
317 "enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))" |
|
318 |
269 instance .. |
319 instance .. |
270 |
320 |
271 end |
321 end |
272 |
322 |
273 instantiation Enum.finite_3 :: check_all |
323 instantiation Enum.finite_3 :: check_all |
274 begin |
324 begin |
275 |
325 |
276 definition |
326 definition |
277 "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3)))" |
327 "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3)))" |
|
328 |
|
329 definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list" |
|
330 where |
|
331 "enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))" |
278 |
332 |
279 instance .. |
333 instance .. |
280 |
334 |
281 end |
335 end |
282 |
336 |