1 (* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)
3 header {* A simple counterexample generator performing random testing *}
6 imports Random Code_Evaluation Enum
8 ("Tools/Quickcheck/quickcheck_common.ML")
9 ("Tools/Quickcheck/random_generators.ML")
12 notation fcomp (infixl "\<circ>>" 60)
13 notation scomp (infixl "\<circ>\<rightarrow>" 60)
15 setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
17 subsection {* Catching Match exceptions *}
19 axiomatization catch_match :: "'a => 'a => 'a"
21 code_const catch_match
22 (Quickcheck "(_) handle Match => _")
24 subsection {* The @{text random} class *}
26 class random = typerep +
27 fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
30 subsection {* Fundamental and numeric types*}
32 instantiation bool :: random
36 "random i = Random.range 2 \<circ>\<rightarrow>
37 (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
43 instantiation itself :: (typerep) random
47 random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
48 where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
54 instantiation char :: random
58 "random _ = Random.select chars \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
64 instantiation String.literal :: random
68 "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
74 instantiation nat :: random
77 definition random_nat :: "code_numeral \<Rightarrow> Random.seed
78 \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
80 "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
81 let n = Code_Numeral.nat_of k
82 in (n, \<lambda>_. Code_Evaluation.term_of n)))"
88 instantiation int :: random
92 "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
93 let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
94 in (j, \<lambda>_. Code_Evaluation.term_of j)))"
101 subsection {* Complex generators *}
103 text {* Towards @{typ "'a \<Rightarrow> 'b"} *}
105 axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
106 \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
107 \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
108 \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
110 definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
111 \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
114 random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
116 instantiation "fun" :: ("{equal, term_of}", random) random
120 random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
121 where "random i = random_fun_lift (random i)"
127 text {* Towards type copies and datatypes *}
129 definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
130 where "collapse f = (f \<circ>\<rightarrow> id)"
132 definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
133 where "beyond k l = (if l > k then l else 0)"
135 lemma beyond_zero: "beyond k 0 = 0"
136 by (simp add: beyond_def)
139 definition (in term_syntax) [code_unfold]:
140 "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
142 definition (in term_syntax) [code_unfold]:
143 "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
145 instantiation set :: (random) random
148 primrec random_aux_set
150 "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
151 | "random_aux_set (Code_Numeral.Suc i) j =
152 collapse (Random.select_weight
153 [(1, Pair valterm_emptyset),
155 random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
158 "random_aux_set i j =
159 collapse (Random.select_weight [(1, Pair valterm_emptyset),
160 (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
161 proof (induct i rule: code_numeral.induct)
163 show ?case by (subst select_weight_drop_zero[symmetric])
164 (simp add: filter.simps random_aux_set.simps[simplified])
167 show ?case by (simp only: random_aux_set.simps(2)[of "i"] Suc_code_numeral_minus_one)
170 definition "random_set i = random_aux_set i i"
176 lemma random_aux_rec:
177 fixes random_aux :: "code_numeral \<Rightarrow> 'a"
178 assumes "random_aux 0 = rhs 0"
179 and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)"
180 shows "random_aux k = rhs k"
181 using assms by (rule code_numeral.induct)
183 subsection {* Deriving random generators for datatypes *}
185 use "Tools/Quickcheck/quickcheck_common.ML"
186 use "Tools/Quickcheck/random_generators.ML"
187 setup Random_Generators.setup
190 subsection {* Code setup *}
192 code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun")
193 -- {* With enough criminal energy this can be abused to derive @{prop False};
194 for this reason we use a distinguished target @{text Quickcheck}
195 not spoiling the regular trusted code generation *}
197 code_reserved Quickcheck Random_Generators
199 no_notation fcomp (infixl "\<circ>>" 60)
200 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
202 subsection {* The Random-Predicate Monad *}
205 "'a itself => code_numeral => code_numeral => code_numeral * code_numeral
206 => ('a::random) Predicate.pred"
208 "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
209 let ((x, _), seed') = random sz seed
210 in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
212 definition iter :: "code_numeral => code_numeral => code_numeral * code_numeral
213 => ('a::random) Predicate.pred"
215 "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
218 "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
219 let ((x, _), seed') = random sz seed
220 in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
221 unfolding iter_def iter'.simps[of _ nrandom] ..
223 type_synonym 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
225 definition empty :: "'a randompred"
226 where "empty = Pair (bot_class.bot)"
228 definition single :: "'a => 'a randompred"
229 where "single x = Pair (Predicate.single x)"
231 definition bind :: "'a randompred \<Rightarrow> ('a \<Rightarrow> 'b randompred) \<Rightarrow> 'b randompred"
233 "bind R f = (\<lambda>s. let
235 (s1, s2) = Random.split_seed s'
236 in (Predicate.bind P (%a. fst (f a s1)), s2))"
238 definition union :: "'a randompred \<Rightarrow> 'a randompred \<Rightarrow> 'a randompred"
240 "union R1 R2 = (\<lambda>s. let
241 (P1, s') = R1 s; (P2, s'') = R2 s'
242 in (sup_class.sup P1 P2, s''))"
244 definition if_randompred :: "bool \<Rightarrow> unit randompred"
246 "if_randompred b = (if b then single () else empty)"
248 definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred"
250 "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
252 definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
254 "not_randompred P = (\<lambda>s. let
256 in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
258 definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a randompred"
259 where "Random g = scomp g (Pair o (Predicate.single o fst))"
261 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
262 where "map f P = bind P (single o f)"
265 random_bool_def random_bool_def_raw
266 random_itself_def random_itself_def_raw
267 random_char_def random_char_def_raw
268 random_literal_def random_literal_def_raw
269 random_nat_def random_nat_def_raw
270 random_int_def random_int_def_raw
271 random_fun_lift_def random_fun_lift_def_raw
272 random_fun_def random_fun_def_raw
273 collapse_def collapse_def_raw
274 beyond_def beyond_def_raw beyond_zero
277 hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
279 hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def
280 if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
281 hide_type (open) randompred
282 hide_const (open) iter' iter empty single bind union if_randompred
283 iterate_upto not_randompred Random map