196 subsection {* The @{text random} class *} |
196 subsection {* The @{text random} class *} |
197 |
197 |
198 class random = |
198 class random = |
199 fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a\<Colon>{} \<times> seed" |
199 fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a\<Colon>{} \<times> seed" |
200 |
200 |
201 -- {* FIXME dummy implementations *} |
201 instantiation itself :: (type) random |
202 |
|
203 instantiation nat :: random |
|
204 begin |
202 begin |
205 |
203 |
206 definition |
204 definition |
207 "random k = (if k = 0 then return 0 else apfst nat_of_index \<circ> range k)" |
205 "random _ = return TYPE('a)" |
208 |
206 |
209 instance .. |
207 instance .. |
210 |
208 |
211 end |
209 end |
212 |
210 |
213 instantiation bool :: random |
211 lemma random_aux_if: |
214 begin |
212 fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" |
215 |
213 assumes "random' 0 j = undefined" |
216 definition |
214 and "\<And>i. random' (Suc_index i) j = rhs2 i" |
217 "random _ = apfst (op = 0) \<circ> range 2" |
215 shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)" |
218 |
216 by (cases i rule: index.exhaust) (insert assms, simp_all add: undefined_fun) |
219 instance .. |
217 |
220 |
218 setup {* |
221 end |
219 let |
222 |
220 fun random_inst tyco thy = |
223 instantiation unit :: random |
221 let |
224 begin |
222 val { descr, index, ... } = DatatypePackage.the_datatype thy tyco; |
225 |
223 val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco; |
226 definition |
224 val vs = (map o apsnd) |
227 "random _ = return ()" |
225 (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs; |
228 |
226 val ty = Type (tyco, map TFree vs); |
229 instance .. |
227 val typ_of = DatatypeAux.typ_of_dtyp descr vs; |
230 |
228 val SOME (_, _, constrs) = AList.lookup (op =) descr index; |
231 end |
229 val randomN = NameSpace.base @{const_name random}; |
232 |
230 val random_aux_name = randomN ^ "_" ^ Class.type_name tyco ^ "'"; |
233 instantiation "+" :: ("{type, random}", "{type, random}") random |
231 fun lift_ty ty = StateMonad.liftT ty @{typ seed}; |
234 begin |
232 val ty_aux = @{typ index} --> @{typ index} --> lift_ty ty; |
235 |
233 fun random ty = |
236 definition |
234 Const (@{const_name random}, @{typ index} --> lift_ty ty); |
237 "random n = (do |
235 val random_aux = Free (random_aux_name, ty_aux); |
238 k \<leftarrow> next; |
236 fun add_cons_arg dty (is_rec, t) = |
239 let l = k div 2; |
237 let |
240 (if k mod 2 = 0 then do |
238 val ty' = typ_of dty; |
241 x \<leftarrow> random l; |
239 val random' = if can DatatypeAux.dest_DtRec dty |
242 return (Inl x) |
240 then random_aux $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"} |
243 done else do |
241 else random ty' $ @{term "j\<Colon>index"} |
244 x \<leftarrow> random l; |
242 val is_rec' = is_rec orelse DatatypeAux.is_rec_type dty; |
245 return (Inr x) |
243 val t' = StateMonad.mbind ty' ty @{typ seed} random' (Abs ("", ty', t)) |
246 done) |
244 in (is_rec', t') end; |
247 done)" |
245 fun mk_cons_t (c, dtys) = |
248 |
246 let |
249 instance .. |
247 val ty' = map typ_of dtys ---> ty; |
250 |
248 val t = StateMonad.return ty @{typ seed} (list_comb (Const (c, ty'), |
251 end |
249 map Bound (length dtys - 1 downto 0))); |
252 |
250 val (is_rec, t') = fold_rev add_cons_arg dtys (false, t); |
253 instantiation "*" :: ("{type, random}", "{type, random}") random |
251 in (is_rec, StateMonad.run ty @{typ seed} t') end; |
254 begin |
252 fun check_empty [] = NONE |
255 |
253 | check_empty xs = SOME xs; |
256 definition |
254 fun bundle_cons_ts cons_ts = |
257 "random n = (do |
255 let |
258 x \<leftarrow> random n; |
256 val ts = map snd cons_ts; |
259 y \<leftarrow> random n; |
257 val t = HOLogic.mk_list (lift_ty ty) ts; |
260 return (x, y) |
258 val t' = Const (@{const_name select}, HOLogic.listT (lift_ty ty) --> lift_ty (lift_ty ty)) $ t; |
261 done)" |
259 val t'' = Const (@{const_name collapse}, lift_ty (lift_ty ty) --> lift_ty ty) $ t'; |
262 |
260 in t'' end; |
263 instance .. |
261 fun bundle_conss (some_rec_t, nonrec_t) = |
264 |
262 let |
265 end |
263 val rec' = case some_rec_t |
|
264 of SOME rec_t => SOME (HOLogic.mk_prod (@{term "i\<Colon>index"}, rec_t)) |
|
265 | NONE => NONE; |
|
266 val nonrec' = HOLogic.mk_prod (@{term "1\<Colon>index"}, nonrec_t); |
|
267 val i_ty = HOLogic.mk_prodT (@{typ index}, lift_ty ty); |
|
268 val t = HOLogic.mk_list i_ty (the_list rec' @ single nonrec'); |
|
269 val t' = Const (@{const_name select_weight}, HOLogic.listT i_ty --> lift_ty (lift_ty ty)) $ t; |
|
270 val t'' = Const (@{const_name collapse}, lift_ty (lift_ty ty) --> lift_ty ty) $ t'; |
|
271 in t'' end; |
|
272 val random_rhs = constrs |
|
273 |> map mk_cons_t |
|
274 |> List.partition fst |
|
275 |> apfst (Option.map bundle_cons_ts o check_empty) |
|
276 |> apsnd bundle_cons_ts |
|
277 |> bundle_conss; |
|
278 val random_aux_undef = (HOLogic.mk_Trueprop o HOLogic.mk_eq) |
|
279 (random_aux $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Const (@{const_name undefined}, lift_ty ty)) |
|
280 val random_aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) |
|
281 (random_aux $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, random_rhs); |
|
282 val random_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (Const (@{const_name random}, |
|
283 @{typ index} --> lift_ty ty) $ @{term "i\<Colon>index"}, |
|
284 random_aux $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"}); |
|
285 val del_func = Attrib.internal (fn _ => Thm.declaration_attribute |
|
286 (fn thm => Context.mapping (Code.del_func thm) I)); |
|
287 fun add_code simps lthy = |
|
288 let |
|
289 val thy = ProofContext.theory_of lthy; |
|
290 val thm = @{thm random_aux_if} |
|
291 |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] [SOME (Thm.cterm_of thy random_aux)] |
|
292 |> (fn thm => thm OF simps) |
|
293 |> singleton (ProofContext.export lthy (ProofContext.init thy)) |
|
294 in |
|
295 lthy |
|
296 |> LocalTheory.theory (PureThy.note Thm.internalK (random_aux_name ^ "_code", thm) |
|
297 #-> Code.add_func) |
|
298 end; |
|
299 in |
|
300 thy |
|
301 |> TheoryTarget.instantiation ([tyco], vs, @{sort random}) |
|
302 |> PrimrecPackage.add_primrec [(random_aux_name, SOME ty_aux, NoSyn)] |
|
303 [(("", [del_func]), random_aux_undef), (("", [del_func]), random_aux_eq)] |
|
304 |-> add_code |
|
305 |> `(fn lthy => Syntax.check_term lthy random_eq) |
|
306 |-> (fn eq => Specification.definition (NONE, (("", []), eq))) |
|
307 |> snd |
|
308 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
|
309 |> LocalTheory.exit |
|
310 |> ProofContext.theory_of |
|
311 end; |
|
312 fun add_random_inst [tyco] = (fn thy => case try (random_inst tyco) thy |
|
313 of SOME thy => thy |
|
314 | NONE => (warning ("Failed to generate random elements for type" ^ tyco); thy)) |
|
315 | add_random_inst tycos = tap (fn _ => warning |
|
316 ("Will not generated random elements for mutual recursive types " ^ commas (map quote tycos))); |
|
317 in DatatypePackage.interpretation add_random_inst end |
|
318 *} |
266 |
319 |
267 instantiation int :: random |
320 instantiation int :: random |
268 begin |
321 begin |
269 |
322 |
270 definition |
323 definition |
271 "random n = (do |
324 "random n = (do |
272 (b, m) \<leftarrow> random n; |
325 (b, m) \<leftarrow> random n; |
273 return (if b then int m else - int m) |
326 return (if b then int m else - int m) |
274 done)" |
327 done)" |
275 |
|
276 instance .. |
|
277 |
|
278 end |
|
279 |
|
280 instantiation list :: ("{type, random}") random |
|
281 begin |
|
282 |
|
283 primrec random_list' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> 'a\<Colon>{type, random} list \<times> seed" |
|
284 where |
|
285 "random_list' 0 j = undefined" |
|
286 | "random_list' (Suc_index i) j = collapse (select_weight [ |
|
287 (i, collapse (select [do x \<leftarrow> random i; xs \<leftarrow> random_list' i j; return (x#xs) done])), |
|
288 (1, collapse (select [do return [] done])) |
|
289 ])" |
|
290 |
|
291 declare random_list'.simps [code func del] |
|
292 |
|
293 lemma random_list'_code [code func]: |
|
294 "random_list' i j = (if i = 0 then undefined else collapse (select_weight [ |
|
295 (i - 1, collapse (select [do x \<leftarrow> random (i - 1); xs \<leftarrow> random_list' (i - 1) j; return (x#xs) done])), |
|
296 (1, collapse (select [do return [] done])) |
|
297 ]))" |
|
298 apply (cases i rule: index.exhaust) |
|
299 apply (simp only:, subst random_list'.simps(1), simp only: Suc_not_Zero refl if_False if_True) |
|
300 apply (simp only:, subst random_list'.simps(2), simp only: Suc_not_Zero refl if_False if_True Suc_index_minus_one Suc_not_Zero_index) |
|
301 done |
|
302 |
|
303 definition "random i = random_list' i i" |
|
304 |
328 |
305 instance .. |
329 instance .. |
306 |
330 |
307 end |
331 end |
308 |
332 |
371 ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
418 ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
372 ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
419 ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
373 ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
420 ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
374 ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
421 ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
375 ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
422 ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
|
423 ML {* f 3 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
|
424 ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
|
425 ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
376 |
426 |
377 ML {* val f = Quickcheck.compile_generator_expr @{theory} |
427 ML {* val f = Quickcheck.compile_generator_expr @{theory} |
378 @{term "\<lambda>(xs\<Colon>int list) ys. rev (xs @ ys) = rev xs @ rev ys"} |
428 @{term "\<lambda>(xs\<Colon>nat list) ys. rev (xs @ ys) = rev xs @ rev ys"} |
379 [@{typ "int list"}, @{typ "int list"}] *} |
429 [@{typ "nat list"}, @{typ "nat list"}] *} |
380 |
430 |
381 ML {* f 15 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
431 ML {* f 15 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
382 ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
432 ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
383 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
433 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
384 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |
434 ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} |