3 header {* Experimental counterexample generators *} |
3 header {* Experimental counterexample generators *} |
4 |
4 |
5 theory Quickcheck_Generators |
5 theory Quickcheck_Generators |
6 imports Quickcheck State_Monad |
6 imports Quickcheck State_Monad |
7 begin |
7 begin |
8 |
|
9 subsection {* Type @{typ "'a \<Rightarrow> 'b"} *} |
|
10 |
|
11 ML {* |
|
12 structure Random_Engine = |
|
13 struct |
|
14 |
|
15 open Random_Engine; |
|
16 |
|
17 fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term) |
|
18 (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed) |
|
19 (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed) |
|
20 (seed : Random_Engine.seed) = |
|
21 let |
|
22 val (seed', seed'') = random_split seed; |
|
23 val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2)); |
|
24 val fun_upd = Const (@{const_name fun_upd}, |
|
25 (T1 --> T2) --> T1 --> T2 --> T1 --> T2); |
|
26 fun random_fun' x = |
|
27 let |
|
28 val (seed, fun_map, f_t) = ! state; |
|
29 in case AList.lookup (uncurry eq) fun_map x |
|
30 of SOME y => y |
|
31 | NONE => let |
|
32 val t1 = term_of x; |
|
33 val ((y, t2), seed') = random seed; |
|
34 val fun_map' = (x, y) :: fun_map; |
|
35 val f_t' = fun_upd $ f_t $ t1 $ t2 (); |
|
36 val _ = state := (seed', fun_map', f_t'); |
|
37 in y end |
|
38 end; |
|
39 fun term_fun' () = #3 (! state); |
|
40 in ((random_fun', term_fun'), seed'') end; |
|
41 |
|
42 end |
|
43 *} |
|
44 |
|
45 axiomatization |
|
46 random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) |
|
47 \<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) |
|
48 \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" |
|
49 |
|
50 code_const random_fun_aux (SML "Random'_Engine.random'_fun") |
|
51 |
|
52 instantiation "fun" :: ("{eq, term_of}", "{type, random}") random |
|
53 begin |
|
54 |
|
55 definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where |
|
56 "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) split_seed" |
|
57 |
|
58 instance .. |
|
59 |
|
60 end |
|
61 |
|
62 code_reserved SML Random_Engine |
|
63 |
|
64 |
8 |
65 subsection {* Datatypes *} |
9 subsection {* Datatypes *} |
66 |
10 |
67 definition |
11 definition |
68 collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where |
12 collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where |