author | haftmann |
Fri, 15 May 2009 16:39:16 +0200 | |
changeset 31179 | ced817160283 |
parent 31153 | 6b31b143f18b |
permissions | -rw-r--r-- |
29132 | 1 |
(* Author: Florian Haftmann, TU Muenchen *) |
26265 | 2 |
|
3 |
header {* A simple counterexample generator *} |
|
4 |
||
5 |
theory Quickcheck |
|
31179 | 6 |
imports Main Real Random |
26265 | 7 |
begin |
8 |
||
31179 | 9 |
notation fcomp (infixl "o>" 60) |
10 |
notation scomp (infixl "o\<rightarrow>" 60) |
|
11 |
||
12 |
||
26265 | 13 |
subsection {* The @{text random} class *} |
14 |
||
28335 | 15 |
class random = typerep + |
31179 | 16 |
fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
26265 | 17 |
|
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset
|
18 |
|
29808
b8b9d529663b
split of already properly working part of Quickcheck infrastructure
haftmann
parents:
29579
diff
changeset
|
19 |
subsection {* Quickcheck generator *} |
29132 | 20 |
|
21 |
ML {* |
|
26265 | 22 |
structure Quickcheck = |
23 |
struct |
|
24 |
||
28309 | 25 |
open Quickcheck; |
26 |
||
26265 | 27 |
val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE; |
28 |
||
30945 | 29 |
val target = "Quickcheck"; |
30 |
||
26325 | 31 |
fun mk_generator_expr thy prop tys = |
26265 | 32 |
let |
26325 | 33 |
val bound_max = length tys - 1; |
34 |
val bounds = map_index (fn (i, ty) => |
|
35 |
(2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys; |
|
36 |
val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds); |
|
37 |
val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds); |
|
26265 | 38 |
val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"} |
26325 | 39 |
$ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms); |
31179 | 40 |
val return = @{term "Pair \<Colon> term list option \<Rightarrow> Random.seed \<Rightarrow> term list option \<times> Random.seed"}; |
41 |
fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); |
|
26325 | 42 |
fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"}); |
31179 | 43 |
fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp}, |
44 |
liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; |
|
26325 | 45 |
fun mk_split ty = Sign.mk_const thy |
31179 | 46 |
(@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT @{typ "term list option"} @{typ Random.seed}]); |
26589 | 47 |
fun mk_scomp_split ty t t' = |
31179 | 48 |
mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t |
26325 | 49 |
(mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t'))); |
26589 | 50 |
fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty |
31179 | 51 |
(Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i); |
52 |
in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end; |
|
26265 | 53 |
|
28309 | 54 |
fun compile_generator_expr thy t = |
26265 | 55 |
let |
28309 | 56 |
val tys = (map snd o fst o strip_abs) t; |
57 |
val t' = mk_generator_expr thy t tys; |
|
30970
3fe2e418a071
generic postprocessing scheme for term evaluations
haftmann
parents:
30945
diff
changeset
|
58 |
val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref) |
31179 | 59 |
(fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' []; |
30970
3fe2e418a071
generic postprocessing scheme for term evaluations
haftmann
parents:
30945
diff
changeset
|
60 |
in f #> Random_Engine.run end; |
26265 | 61 |
|
62 |
end |
|
63 |
*} |
|
64 |
||
28309 | 65 |
setup {* |
30945 | 66 |
Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I)) |
67 |
#> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of) |
|
28309 | 68 |
*} |
69 |
||
30945 | 70 |
|
31179 | 71 |
subsection {* Fundamental types*} |
72 |
||
73 |
definition (in term_syntax) |
|
74 |
"termify_bool b = (if b then termify True else termify False)" |
|
75 |
||
76 |
instantiation bool :: random |
|
77 |
begin |
|
78 |
||
79 |
definition |
|
80 |
"random i = Random.range i o\<rightarrow> (\<lambda>k. Pair (termify_bool (k div 2 = 0)))" |
|
81 |
||
82 |
instance .. |
|
83 |
||
84 |
end |
|
85 |
||
86 |
definition (in term_syntax) |
|
87 |
"termify_itself TYPE('a\<Colon>typerep) = termify TYPE('a)" |
|
88 |
||
89 |
instantiation itself :: (typerep) random |
|
90 |
begin |
|
91 |
||
92 |
definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where |
|
93 |
"random_itself _ = Pair (termify_itself TYPE('a))" |
|
94 |
||
95 |
instance .. |
|
96 |
||
97 |
end |
|
98 |
||
99 |
text {* Type @{typ "'a \<Rightarrow> 'b"} *} |
|
30945 | 100 |
|
101 |
ML {* |
|
102 |
structure Random_Engine = |
|
103 |
struct |
|
104 |
||
105 |
open Random_Engine; |
|
106 |
||
107 |
fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term) |
|
108 |
(random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed) |
|
109 |
(random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed) |
|
110 |
(seed : Random_Engine.seed) = |
|
111 |
let |
|
112 |
val (seed', seed'') = random_split seed; |
|
113 |
val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2)); |
|
114 |
val fun_upd = Const (@{const_name fun_upd}, |
|
115 |
(T1 --> T2) --> T1 --> T2 --> T1 --> T2); |
|
116 |
fun random_fun' x = |
|
117 |
let |
|
118 |
val (seed, fun_map, f_t) = ! state; |
|
119 |
in case AList.lookup (uncurry eq) fun_map x |
|
120 |
of SOME y => y |
|
121 |
| NONE => let |
|
122 |
val t1 = term_of x; |
|
123 |
val ((y, t2), seed') = random seed; |
|
124 |
val fun_map' = (x, y) :: fun_map; |
|
125 |
val f_t' = fun_upd $ f_t $ t1 $ t2 (); |
|
126 |
val _ = state := (seed', fun_map', f_t'); |
|
127 |
in y end |
|
128 |
end; |
|
129 |
fun term_fun' () = #3 (! state); |
|
130 |
in ((random_fun', term_fun'), seed'') end; |
|
131 |
||
26265 | 132 |
end |
30945 | 133 |
*} |
134 |
||
31179 | 135 |
axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) |
136 |
\<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed) |
|
137 |
\<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
|
30945 | 138 |
|
139 |
code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun") |
|
140 |
-- {* With enough criminal energy this can be abused to derive @{prop False}; |
|
141 |
for this reason we use a distinguished target @{text Quickcheck} |
|
142 |
not spoiling the regular trusted code generation *} |
|
143 |
||
144 |
instantiation "fun" :: ("{eq, term_of}", "{type, random}") random |
|
145 |
begin |
|
146 |
||
31179 | 147 |
definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where |
148 |
"random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed" |
|
30945 | 149 |
|
150 |
instance .. |
|
151 |
||
152 |
end |
|
153 |
||
154 |
code_reserved Quickcheck Random_Engine |
|
155 |
||
31179 | 156 |
|
157 |
subsection {* Numeric types *} |
|
158 |
||
159 |
function (in term_syntax) termify_numeral :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where |
|
160 |
"termify_numeral k = (if k = 0 then termify Int.Pls |
|
161 |
else (if k mod 2 = 0 then termify Int.Bit0 else termify Int.Bit1) <\<cdot>> termify_numeral (k div 2))" |
|
162 |
by pat_completeness auto |
|
163 |
||
164 |
declare (in term_syntax) termify_numeral.psimps [simp del] |
|
165 |
||
166 |
termination termify_numeral by (relation "measure Code_Index.nat_of") |
|
167 |
(simp_all add: index) |
|
168 |
||
169 |
definition (in term_syntax) termify_int_number :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where |
|
170 |
"termify_int_number k = termify number_of <\<cdot>> termify_numeral k" |
|
171 |
||
172 |
definition (in term_syntax) termify_nat_number :: "index \<Rightarrow> nat \<times> (unit \<Rightarrow> term)" where |
|
173 |
"termify_nat_number k = (nat \<circ> number_of, snd (termify (number_of :: int \<Rightarrow> nat))) <\<cdot>> termify_numeral k" |
|
174 |
||
175 |
declare termify_nat_number_def [simplified snd_conv, code] |
|
176 |
||
177 |
instantiation nat :: random |
|
178 |
begin |
|
179 |
||
180 |
definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where |
|
181 |
"random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (termify_nat_number k))" |
|
182 |
||
183 |
instance .. |
|
184 |
||
30945 | 185 |
end |
31179 | 186 |
|
187 |
definition (in term_syntax) term_uminus :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where |
|
188 |
[code inline]: "term_uminus k = termify uminus <\<cdot>> k" |
|
189 |
||
190 |
instantiation int :: random |
|
191 |
begin |
|
192 |
||
193 |
definition |
|
194 |
"random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (if k \<ge> i |
|
195 |
then let j = k - i in termify_int_number j |
|
196 |
else let j = i - k in term_uminus (termify_int_number j)))" |
|
197 |
||
198 |
instance .. |
|
199 |
||
200 |
end |
|
201 |
||
202 |
definition (in term_syntax) term_fract :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term) \<Rightarrow> rat \<times> (unit \<Rightarrow> term)" where |
|
203 |
[code inline]: "term_fract k l = termify Fract <\<cdot>> k <\<cdot>> l" |
|
204 |
||
205 |
instantiation rat :: random |
|
206 |
begin |
|
207 |
||
208 |
definition |
|
209 |
"random i = random i o\<rightarrow> (\<lambda>num. Random.range (i + 1) o\<rightarrow> (\<lambda>denom. Pair (term_fract num (termify_int_number denom))))" |
|
210 |
||
211 |
instance .. |
|
212 |
||
213 |
end |
|
214 |
||
215 |
definition (in term_syntax) term_ratreal :: "rat \<times> (unit \<Rightarrow> term) \<Rightarrow> real \<times> (unit \<Rightarrow> term)" where |
|
216 |
[code inline]: "term_ratreal k = termify Ratreal <\<cdot>> k" |
|
217 |
||
218 |
instantiation real :: random |
|
219 |
begin |
|
220 |
||
221 |
definition |
|
222 |
"random i = random i o\<rightarrow> (\<lambda>r. Pair (term_ratreal r))" |
|
223 |
||
224 |
instance .. |
|
225 |
||
226 |
end |
|
227 |
||
228 |
||
229 |
no_notation fcomp (infixl "o>" 60) |
|
230 |
no_notation scomp (infixl "o\<rightarrow>" 60) |
|
231 |
||
232 |
end |