22528

1 
(* ID: $Id$


2 
Author: Florian Haftmann, TU Muenchen


3 
*)


4 

26038

5 
header {* A simple term generator *}

22528

6 


7 
theory Random

26038

8 
imports State_Monad Code_Index List Eval

22528

9 
begin


10 

26038

11 
subsection {* The random engine *}


12 


13 
types seed = "index \<times> index"

22528

14 

26038

15 
definition


16 
"next" :: "seed \<Rightarrow> index \<times> seed"


17 
where


18 
"next s = (let


19 
(v, w) = s;


20 
k = v div 53668;


21 
v' = 40014 * (v  k * 53668)  k * 12211;


22 
v'' = (if v' < 0 then v' + 2147483563 else v');


23 
l = w div 52774;


24 
w' = 40692 * (w  l * 52774)  l * 3791;


25 
w'' = (if w' < 0 then w' + 2147483399 else w');


26 
z = v''  w'';


27 
z' = (if z < 1 then z + 2147483562 else z)


28 
in (z', (v'', w'')))"

22528

29 


30 
definition

26038

31 
split_seed :: "seed \<Rightarrow> seed \<times> seed"


32 
where


33 
"split_seed s = (let


34 
(v, w) = s;


35 
(v', w') = snd (next s);


36 
v'' = (if v = 2147483562 then 1 else v + 1);


37 
s'' = (v'', w');


38 
w'' = (if w = 2147483398 then 1 else w + 1);


39 
s''' = (v', w'')


40 
in (s'', s'''))"


41 


42 
text {* Base selectors *}


43 


44 
primrec


45 
pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"


46 
where


47 
"pick (x#xs) n = (if n < fst x then snd x else pick xs (n  fst x))"

22528

48 

26038

49 
function


50 
iLogBase :: "index \<Rightarrow> index \<Rightarrow> index"


51 
where


52 
"iLogBase b i = (if b \<le> 1 \<or> i < b then 1 else 1 + iLogBase b (i div b))"


53 
by pat_completeness auto


54 
termination


55 
by (relation "measure (nat_of_index o snd)")


56 
(auto simp add: index)

22528

57 

26038

58 
function


59 
range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"


60 
where


61 
"range_aux k l s = (if k = 0 then (l, s) else


62 
let (v, s') = next s


63 
in range_aux (k  1) (v + l * 2147483561) s')"


64 
by pat_completeness auto


65 
termination


66 
by (relation "measure (nat_of_index o fst)")


67 
(auto simp add: index)

22528

68 


69 
definition

26038

70 
range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"


71 
where


72 
"range k s = (let


73 
b = 2147483561;


74 
n = iLogBase b k;


75 
(v, s') = range_aux n 1 s


76 
in (v mod k, s'))"


77 

22528

78 
definition

26038

79 
select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"


80 
where


81 
[simp]: "select xs s = (let


82 
(k, s') = range (index_of_nat (length xs)) s


83 
in (nth xs (nat_of_index k), s'))"

22528

84 

26038

85 
definition


86 
select_weight :: "(nat \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"


87 
where


88 
[simp]: "select_weight xs s = (let


89 
(k, s') = range (foldr (op + \<circ> index_of_nat \<circ> fst) xs 0) s


90 
in (pick xs (nat_of_index k), s'))"


91 


92 
(*lemma

22528

93 
"select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"


94 
proof (induct xs)

26038

95 
case Nil show ?case apply (auto simp add: Let_def split_def)

22528

96 
next


97 
have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"


98 
proof 


99 
fix xs


100 
fix y


101 
show "map fst (map (Pair y) xs) = replicate (length xs) y"


102 
by (induct xs) simp_all


103 
qed


104 
have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n"


105 
proof 


106 
fix xs


107 
fix n


108 
assume "n < length xs"


109 
then show "pick (map (Pair 1) xs) n = nth xs n"


110 
proof (induct xs arbitrary: n)


111 
case Nil then show ?case by simp


112 
next


113 
case (Cons x xs) show ?case


114 
proof (cases n)


115 
case 0 then show ?thesis by simp


116 
next


117 
case (Suc _)


118 
from Cons have "n < length (x # xs)" by auto


119 
then have "n < Suc (length xs)" by simp


120 
with Suc have "n  1 < Suc (length xs)  1" by auto


121 
with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n  1) = xs ! (n  1)" by auto


122 
with Suc show ?thesis by auto


123 
qed


124 
qed


125 
qed


126 
have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"


127 
proof 


128 
have replicate_append:


129 
"!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]"


130 
by (simp add: replicate_app_Cons_same)


131 
fix xs


132 
show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"


133 
unfolding map_fst_Pair proof (induct xs)


134 
case Nil show ?case by simp


135 
next


136 
case (Cons x xs) then show ?case unfolding replicate_append by simp


137 
qed


138 
qed


139 
have pick_nth_random:


140 
"!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))"


141 
proof 


142 
fix s


143 
fix x


144 
fix xs


145 
have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp


146 
from pick_nth [OF bound] show


147 
"pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .


148 
qed


149 
have pick_nth_random_do:


150 
"!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s =


151 
(do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s"


152 
unfolding monad_collapse split_def unfolding pick_nth_random ..


153 
case (Cons x xs) then show ?case


154 
unfolding select_weight_def sum_length pick_nth_random_do


155 
by simp

26038

156 
qed*)

22528

157 

26038

158 
text {* The @{text ML} interface *}

22528

159 


160 
ML {*

26038

161 
structure Quickcheck =

22528

162 
struct


163 

26038

164 
type seed = int * int;

22528

165 


166 
local

26038

167 


168 
val seed = ref (0, 0);


169 


170 
fun init () =


171 
let


172 
val now = Time.toNanoseconds (Time.now ());


173 
val (q, s1) = IntInf.divMod (now, 2147483562);


174 
val s2 = q mod 2147483398;


175 
in seed := (s1 + 1, s2 + 1) end;


176 

22528

177 
in

26038

178 


179 
val seed = seed; (* FIXME *)


180 


181 
fun run f =


182 
let


183 
val (x, seed') = f (!seed);


184 
val _ = seed := seed'


185 
val _ = if fst (! seed) = 0 orelse snd (! seed) = 0 then


186 
(warning "broken random seed"; init ())


187 
else ()


188 
in x end;


189 

22528

190 
end;


191 


192 
end;


193 
*}


194 

26038

195 


196 
subsection {* The @{text random} class *}


197 


198 
class random = type +


199 
fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"


200 


201 
 {* FIXME dummy implementations *}


202 


203 
instantiation nat :: random


204 
begin


205 


206 
definition


207 
"random k = apfst nat_of_index \<circ> range k"


208 


209 
instance ..


210 


211 
end


212 


213 
instantiation bool :: random


214 
begin


215 


216 
definition


217 
"random _ = apfst (op = 0) \<circ> range 2"


218 


219 
instance ..


220 


221 
end

24226

222 

26038

223 
instantiation unit :: random


224 
begin


225 


226 
definition


227 
"random _ = Pair ()"


228 


229 
instance ..


230 


231 
end


232 


233 
instantiation "+" :: (random, random) random


234 
begin


235 


236 
definition


237 
"random n = (do


238 
k \<leftarrow> next;


239 
let l = k div 2;


240 
(if k mod 2 = 0 then do


241 
x \<leftarrow> random l;


242 
return (Inl x)


243 
done else do


244 
x \<leftarrow> random l;


245 
return (Inr x)


246 
done)


247 
done)"


248 


249 
instance ..


250 


251 
end

22528

252 

26038

253 
instantiation "*" :: (random, random) random


254 
begin


255 


256 
definition


257 
"random n = (do


258 
x \<leftarrow> random n;


259 
y \<leftarrow> random n;


260 
return (x, y)


261 
done)"


262 


263 
instance ..


264 


265 
end


266 


267 
instantiation int :: random


268 
begin


269 


270 
definition


271 
"random n = (do


272 
(b, m) \<leftarrow> random n;


273 
return (if b then int m else  int m)


274 
done)"


275 


276 
instance ..


277 


278 
end


279 


280 
instantiation list :: (random) random


281 
begin

22528

282 

26038

283 
primrec


284 
random_list_aux


285 
where


286 
"random_list_aux 0 = Pair []"


287 
 "random_list_aux (Suc n) = (do


288 
x \<leftarrow> random (index_of_nat (Suc n));


289 
xs \<leftarrow> random_list_aux n;


290 
return (x#xs)


291 
done)"


292 


293 
definition


294 
[code func del]: "random n = random_list_aux (nat_of_index n)"


295 


296 
lemma [code func]:


297 
"random n = (if n = 0 then return ([]::'a list)


298 
else do


299 
x \<leftarrow> random n;


300 
xs \<leftarrow> random (n  1);


301 
return (x#xs)


302 
done)"


303 
unfolding random_list_def


304 
by (cases "nat_of_index n", auto)


305 
(cases n, auto)+


306 


307 
(*fun


308 
random_list


309 
where


310 
"random_list n = (if n = 0 then (\<lambda>_. ([]::'a list))


311 
else random n \<guillemotright>=\<^isub>R (\<lambda>x::'a. random_list (n  1) \<guillemotright>=\<^isub>R (\<lambda>(xs::'a list) _. x#xs)))"*)


312 


313 
instance ..

22528

314 


315 
end

26038

316 


317 
code_reserved SML Quickcheck


318 


319 


320 
subsection {* Quickcheck generator *}


321 


322 
ML {*


323 
structure Quickcheck =


324 
struct


325 


326 
open Quickcheck;


327 


328 
val eval_ref : (unit > int > int * int > term list option * (int * int)) option ref = ref NONE;


329 


330 
fun mk_generator_expr prop tys =


331 
let


332 
val bounds = map_index (fn (i, ty) => (i, ty)) tys;


333 
val result = list_comb (prop, map (fn (i, _) => Bound (length tys  i  1)) bounds);


334 
val terms = map (fn (i, ty) => Const (@{const_name Eval.term_of}, ty > @{typ term}) $ Bound (length tys  i  1)) bounds;


335 
val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}


336 
$ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ HOLogic.mk_list @{typ term} terms);


337 
val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};


338 
fun mk_bindtyp ty = @{typ seed} > HOLogic.mk_prodT (ty, @{typ seed});


339 
fun mk_bindclause (i, ty) t = Const (@{const_name mbind}, mk_bindtyp ty


340 
> (ty > mk_bindtyp @{typ "term list option"}) > mk_bindtyp @{typ "term list option"})


341 
$ (Const (@{const_name random}, @{typ index} > mk_bindtyp ty)


342 
$ Bound i) $ Abs ("a", ty, t);


343 
val t = fold_rev mk_bindclause bounds (return $ check);


344 
in Abs ("n", @{typ index}, t) end;


345 


346 
fun compile_generator_expr thy prop tys =


347 
let


348 
val f = CodePackage.eval_term ("Quickcheck.eval_ref", eval_ref) thy


349 
(mk_generator_expr prop tys) [];


350 
in f #> run #> (Option.map o map) (Code.postprocess_term thy) end;


351 


352 
end


353 
*}


354 


355 
ML {* val f = Quickcheck.compile_generator_expr @{theory}


356 
@{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}


357 


358 
ML {* f 5 > (Option.map o map) (Sign.string_of_term @{theory}) *}


359 
ML {* f 5 > (Option.map o map) (Sign.string_of_term @{theory}) *}


360 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


361 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


362 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


363 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


364 
ML {* f 25 > (Option.map o map) (Sign.string_of_term @{theory}) *}


365 
ML {* f 1 > (Option.map o map) (Sign.string_of_term @{theory}) *}


366 
ML {* f 1 > (Option.map o map) (Sign.string_of_term @{theory}) *}


367 
ML {* f 2 > (Option.map o map) (Sign.string_of_term @{theory}) *}


368 
ML {* f 2 > (Option.map o map) (Sign.string_of_term @{theory}) *}


369 


370 
ML {* val f = Quickcheck.compile_generator_expr @{theory}


371 
@{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *}


372 


373 
ML {* f 5 > (Option.map o map) (Sign.string_of_term @{theory}) *}


374 
ML {* f 5 > (Option.map o map) (Sign.string_of_term @{theory}) *}


375 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


376 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


377 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


378 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


379 
ML {* f 25 > (Option.map o map) (Sign.string_of_term @{theory}) *}


380 
ML {* f 1 > (Option.map o map) (Sign.string_of_term @{theory}) *}


381 
ML {* f 1 > (Option.map o map) (Sign.string_of_term @{theory}) *}


382 
ML {* f 2 > (Option.map o map) (Sign.string_of_term @{theory}) *}


383 
ML {* f 2 > (Option.map o map) (Sign.string_of_term @{theory}) *}


384 


385 


386 
subsection {* Incremental function generator *}


387 


388 
ML {*


389 
structure Quickcheck =


390 
struct


391 


392 
open Quickcheck;


393 


394 
fun random_fun (eq : 'a > 'a > bool)


395 
(random : seed > 'b * seed)


396 
(random_split : seed > seed * seed)


397 
(seed : seed) =


398 
let


399 
val (seed', seed'') = random_split seed;


400 
val state = ref (seed', []);


401 
fun random_fun' x =


402 
let


403 
val (seed, fun_map) = ! state;


404 
in case AList.lookup (uncurry eq) fun_map x


405 
of SOME y => y


406 
 NONE => let


407 
val (y, seed') = random seed;


408 
val _ = state := (seed', (x, y) :: fun_map);


409 
in y end


410 
end;


411 
in (random_fun', seed'') end;


412 


413 
end


414 
*}


415 


416 
axiomatization


417 
random_fun_aux :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> (seed \<Rightarrow> 'b \<times> seed)


418 
\<Rightarrow> (seed \<Rightarrow> seed \<times> seed) \<Rightarrow> seed \<Rightarrow> ('a \<Rightarrow> 'b) \<times> seed"


419 


420 
code_const random_fun_aux (SML "Quickcheck.random'_fun")


421 


422 
instantiation "fun" :: (term_of, term_of) term_of


423 
begin


424 


425 
instance ..


426 


427 
end


428 


429 
code_const "Eval.term_of :: ('a\<Colon>term_of \<Rightarrow> 'b\<Colon>term_of) \<Rightarrow> _"


430 
(SML "(fn '_ => Const (\"arbitrary\", dummyT))")


431 


432 
instantiation "fun" :: (eq, random) random


433 
begin


434 


435 
definition


436 
"random n = random_fun_aux (op =) (random n) split_seed"


437 


438 
instance ..


439 


440 
end


441 


442 
ML {* val f = Quickcheck.compile_generator_expr @{theory}


443 
@{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}


444 


445 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


446 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


447 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


448 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


449 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


450 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *}


451 


452 
end
