45 |
45 |
46 open Quickcheck; |
46 open Quickcheck; |
47 |
47 |
48 val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE; |
48 val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE; |
49 |
49 |
|
50 val target = "Quickcheck"; |
|
51 |
50 fun mk_generator_expr thy prop tys = |
52 fun mk_generator_expr thy prop tys = |
51 let |
53 let |
52 val bound_max = length tys - 1; |
54 val bound_max = length tys - 1; |
53 val bounds = map_index (fn (i, ty) => |
55 val bounds = map_index (fn (i, ty) => |
54 (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys; |
56 (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys; |
70 |
72 |
71 fun compile_generator_expr thy t = |
73 fun compile_generator_expr thy t = |
72 let |
74 let |
73 val tys = (map snd o fst o strip_abs) t; |
75 val tys = (map snd o fst o strip_abs) t; |
74 val t' = mk_generator_expr thy t tys; |
76 val t' = mk_generator_expr thy t tys; |
75 val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy t' []; |
77 val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref) thy t' []; |
76 in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end; |
78 in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end; |
77 |
79 |
78 end |
80 end |
79 *} |
81 *} |
80 |
82 |
81 setup {* |
83 setup {* |
82 Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of) |
84 Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I)) |
|
85 #> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of) |
83 *} |
86 *} |
84 |
87 |
|
88 |
|
89 subsection {* Type @{typ "'a \<Rightarrow> 'b"} *} |
|
90 |
|
91 ML {* |
|
92 structure Random_Engine = |
|
93 struct |
|
94 |
|
95 open Random_Engine; |
|
96 |
|
97 fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term) |
|
98 (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed) |
|
99 (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed) |
|
100 (seed : Random_Engine.seed) = |
|
101 let |
|
102 val (seed', seed'') = random_split seed; |
|
103 val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2)); |
|
104 val fun_upd = Const (@{const_name fun_upd}, |
|
105 (T1 --> T2) --> T1 --> T2 --> T1 --> T2); |
|
106 fun random_fun' x = |
|
107 let |
|
108 val (seed, fun_map, f_t) = ! state; |
|
109 in case AList.lookup (uncurry eq) fun_map x |
|
110 of SOME y => y |
|
111 | NONE => let |
|
112 val t1 = term_of x; |
|
113 val ((y, t2), seed') = random seed; |
|
114 val fun_map' = (x, y) :: fun_map; |
|
115 val f_t' = fun_upd $ f_t $ t1 $ t2 (); |
|
116 val _ = state := (seed', fun_map', f_t'); |
|
117 in y end |
|
118 end; |
|
119 fun term_fun' () = #3 (! state); |
|
120 in ((random_fun', term_fun'), seed'') end; |
|
121 |
85 end |
122 end |
|
123 *} |
|
124 |
|
125 axiomatization |
|
126 random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) |
|
127 \<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) |
|
128 \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" |
|
129 |
|
130 code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun") |
|
131 -- {* With enough criminal energy this can be abused to derive @{prop False}; |
|
132 for this reason we use a distinguished target @{text Quickcheck} |
|
133 not spoiling the regular trusted code generation *} |
|
134 |
|
135 instantiation "fun" :: ("{eq, term_of}", "{type, random}") random |
|
136 begin |
|
137 |
|
138 definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where |
|
139 "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) split_seed" |
|
140 |
|
141 instance .. |
|
142 |
|
143 end |
|
144 |
|
145 code_reserved Quickcheck Random_Engine |
|
146 |
|
147 end |