117 |
117 |
118 instance .. |
118 instance .. |
119 |
119 |
120 end |
120 end |
121 |
121 |
|
122 definition (in term_syntax) [code_unfold]: "valtermify_pair x y = Code_Evaluation.valtermify (Pair :: 'a :: typerep => 'b :: typerep => 'a * 'b) {\<cdot>} x {\<cdot>} y" |
|
123 |
122 instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive |
124 instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive |
123 begin |
125 begin |
124 |
126 |
125 definition |
127 definition |
126 "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y), |
128 "full_exhaustive f d = full_exhaustive (%x. full_exhaustive (%y. f (valtermify_pair x y)) d) d" |
127 %u. let T1 = (Typerep.typerep (TYPE('a))); |
|
128 T2 = (Typerep.typerep (TYPE('b))) |
|
129 in Code_Evaluation.App (Code_Evaluation.App ( |
|
130 Code_Evaluation.Const (STR ''Product_Type.Pair'') |
|
131 (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) |
|
132 (t1 ())) (t2 ()))) d) d" |
|
133 |
129 |
134 instance .. |
130 instance .. |
135 |
131 |
136 end |
132 end |
137 |
133 |
138 instantiation set :: (exhaustive) exhaustive |
134 instantiation set :: (exhaustive) exhaustive |
139 begin |
135 begin |
140 |
136 |
141 fun exhaustive_set |
137 fun exhaustive_set |
142 where |
138 where |
143 "exhaustive_set f i = (if i = 0 then None else (f {} orelse exhaustive_set (%A. f A orelse Quickcheck_Exhaustive.exhaustive (%x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1)))" |
139 "exhaustive_set f i = (if i = 0 then None else (f {} orelse exhaustive_set (%A. f A orelse exhaustive (%x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1)))" |
144 |
140 |
145 instance .. |
141 instance .. |
146 |
142 |
147 end |
143 end |
148 |
144 |
176 |
172 |
177 instance .. |
173 instance .. |
178 |
174 |
179 end |
175 end |
180 |
176 |
|
177 definition [code_unfold]: "valtermify_absdummy = (%(v, t). (%_::'a. v, %u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))" |
|
178 |
|
179 definition (in term_syntax) [code_unfold]: "valtermify_fun_upd g a b = Code_Evaluation.valtermify (fun_upd :: ('a :: typerep => 'b :: typerep) => 'a => 'b => 'a => 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b" |
|
180 |
181 instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive |
181 instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive |
182 begin |
182 begin |
183 |
183 |
184 fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option" |
184 fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option" |
185 where |
185 where |
186 "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d) |
186 "full_exhaustive_fun' f i d = (full_exhaustive (%v. f (valtermify_absdummy v)) d) |
187 orelse (if i > 1 then |
187 orelse (if i > 1 then |
188 full_exhaustive_fun' (%(g, gt). full_exhaustive (%(a, at). full_exhaustive (%(b, bt). |
188 full_exhaustive_fun' (%g. full_exhaustive (%a. full_exhaustive (%b. |
189 f (g(a := b), |
189 f (valtermify_fun_upd g a b)) d) d) (i - 1) d else None)" |
190 (%_. let A = (Typerep.typerep (TYPE('a))); |
|
191 B = (Typerep.typerep (TYPE('b))); |
|
192 fun = (%T U. Typerep.Typerep (STR ''fun'') [T, U]) |
|
193 in |
|
194 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App |
|
195 (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B))))) |
|
196 (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)" |
|
197 |
190 |
198 definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option" |
191 definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option" |
199 where |
192 where |
200 "full_exhaustive_fun f d = full_exhaustive_fun' f d d" |
193 "full_exhaustive_fun f d = full_exhaustive_fun' f d d" |
201 |
194 |
211 |
204 |
212 fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option" |
205 fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option" |
213 where |
206 where |
214 "check_all_n_lists f n = |
207 "check_all_n_lists f n = |
215 (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))" |
208 (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))" |
|
209 |
|
210 definition (in term_syntax) [code_unfold]: "termify_fun_upd g a b = (Code_Evaluation.termify (fun_upd :: ('a :: typerep => 'b :: typerep) => 'a => 'b => 'a => 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)" |
216 |
211 |
217 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" |
212 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" |
218 where |
213 where |
219 "mk_map_term T1 T2 domm rng = |
214 "mk_map_term T1 T2 domm rng = |
220 (%_. let T1 = T1 (); |
215 (%_. let T1 = T1 (); |
305 |
300 |
306 instance .. |
301 instance .. |
307 |
302 |
308 end |
303 end |
309 |
304 |
|
305 definition (in term_syntax) [code_unfold]: "termify_pair x y = Code_Evaluation.termify (Pair :: 'a :: typerep => 'b :: typerep => 'a * 'b) <\<cdot>> x <\<cdot>> y" |
310 |
306 |
311 instantiation prod :: (check_all, check_all) check_all |
307 instantiation prod :: (check_all, check_all) check_all |
312 begin |
308 begin |
313 |
309 |
314 definition |
310 definition |
315 "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), |
311 "check_all f = check_all (%x. check_all (%y. f (valtermify_pair x y)))" |
316 %u. let T1 = (Typerep.typerep (TYPE('a))); |
|
317 T2 = (Typerep.typerep (TYPE('b))) |
|
318 in Code_Evaluation.App (Code_Evaluation.App ( |
|
319 Code_Evaluation.Const (STR ''Product_Type.Pair'') |
|
320 (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) |
|
321 (t1 ())) (t2 ()))))" |
|
322 |
312 |
323 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list" |
313 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list" |
324 where |
314 where |
325 "enum_term_of_prod = (%_ _. map (%(x, y). |
315 "enum_term_of_prod = (%_ _. map (%(x, y). termify_pair TYPE('a) TYPE('b) x y) |
326 let T1 = (Typerep.typerep (TYPE('a))); |
316 (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))" |
327 T2 = (Typerep.typerep (TYPE('b))) |
317 |
328 in Code_Evaluation.App (Code_Evaluation.App ( |
318 instance .. |
329 Code_Evaluation.Const (STR ''Product_Type.Pair'') |
319 |
330 (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y) |
320 end |
331 (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ()))) " |
321 |
332 |
322 definition (in term_syntax) [code_unfold]: "valtermify_Inl x = Code_Evaluation.valtermify (Inl :: 'a :: typerep => 'a + 'b :: typerep) {\<cdot>} x" |
333 instance .. |
323 definition (in term_syntax) [code_unfold]: "valtermify_Inr x = Code_Evaluation.valtermify (Inr :: 'b :: typerep => 'a ::typerep + 'b) {\<cdot>} x" |
334 |
|
335 end |
|
336 |
|
337 |
324 |
338 instantiation sum :: (check_all, check_all) check_all |
325 instantiation sum :: (check_all, check_all) check_all |
339 begin |
326 begin |
340 |
327 |
341 definition |
328 definition |
342 "check_all f = (case check_all (%(a, t). f (Inl a, %_. |
329 "check_all f = check_all (%a. f (valtermify_Inl a)) orelse check_all (%b. f (valtermify_Inr b))" |
343 let T1 = (Typerep.typerep (TYPE('a))); |
|
344 T2 = (Typerep.typerep (TYPE('b))) |
|
345 in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') |
|
346 (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))) of Some x' => Some x' |
|
347 | None => check_all (%(b, t). f (Inr b, %_. let |
|
348 T1 = (Typerep.typerep (TYPE('a))); |
|
349 T2 = (Typerep.typerep (TYPE('b))) |
|
350 in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') |
|
351 (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))))" |
|
352 |
330 |
353 definition enum_term_of_sum :: "('a + 'b) itself => unit => term list" |
331 definition enum_term_of_sum :: "('a + 'b) itself => unit => term list" |
354 where |
332 where |
355 "enum_term_of_sum = (%_ _. |
333 "enum_term_of_sum = (%_ _. |
356 let |
334 let |
596 |
574 |
597 hide_fact |
575 hide_fact |
598 exhaustive'_def |
576 exhaustive'_def |
599 exhaustive_code_numeral'_def |
577 exhaustive_code_numeral'_def |
600 |
578 |
601 hide_const valterm_emptyset valtermify_insert term_emptyset termify_insert setify |
579 hide_const valtermify_absdummy valtermify_fun_upd valterm_emptyset valtermify_insert valtermify_pair |
|
580 valtermify_Inl valtermify_Inr |
|
581 termify_fun_upd term_emptyset termify_insert termify_pair setify |
602 |
582 |
603 hide_const (open) |
583 hide_const (open) |
604 exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral' |
584 exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral' |
605 throw_Counterexample catch_Counterexample |
585 throw_Counterexample catch_Counterexample |
606 check_all enum_term_of |
586 check_all enum_term_of |