author  haftmann 
Fri, 24 Apr 2009 08:24:54 +0200  
changeset 30970  3fe2e418a071 
parent 30945  0418e9bffbba 
child 31153  6b31b143f18b 
permissions  rwrr 
29132  1 
(* Author: Florian Haftmann, TU Muenchen *) 
26265  2 

3 
header {* A simple counterexample generator *} 

4 

5 
theory Quickcheck 

29132  6 
imports Random Code_Eval Map 
26265  7 
begin 
8 

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

10 

28335  11 
class random = typerep + 
26325  12 
fixes random :: "index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed" 
26265  13 

26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

14 
text {* Type @{typ "'a itself"} *} 
26265  15 

28335  16 
instantiation itself :: ("{type, typerep}") random 
26265  17 
begin 
18 

19 
definition 

29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29808
diff
changeset

20 
"random _ = Pair (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))" 
26265  21 

22 
instance .. 

23 

24 
end 

25 

26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

26 

29808
b8b9d529663b
split of already properly working part of Quickcheck infrastructure
haftmann
parents:
29579
diff
changeset

27 
subsection {* Quickcheck generator *} 
29132  28 

29 
ML {* 

30 
structure StateMonad = 

31 
struct 

32 

33 
fun liftT T sT = sT > HOLogic.mk_prodT (T, sT); 

34 
fun liftT' sT = sT > sT; 

35 

29808
b8b9d529663b
split of already properly working part of Quickcheck infrastructure
haftmann
parents:
29579
diff
changeset

36 
fun return T sT x = Const (@{const_name Pair}, T > liftT T sT) $ x; 
29132  37 

38 
fun scomp T1 T2 sT f g = Const (@{const_name scomp}, 

39 
liftT T1 sT > (T1 > liftT T2 sT) > liftT T2 sT) $ f $ g; 

40 

41 
end; 

42 

26265  43 
structure Quickcheck = 
44 
struct 

45 

28309  46 
open Quickcheck; 
47 

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

30945  50 
val target = "Quickcheck"; 
51 

26325  52 
fun mk_generator_expr thy prop tys = 
26265  53 
let 
26325  54 
val bound_max = length tys  1; 
55 
val bounds = map_index (fn (i, ty) => 

56 
(2 * (bound_max  i) + 1, 2 * (bound_max  i), 2 * i, ty)) tys; 

57 
val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds); 

58 
val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds); 

26265  59 
val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"} 
26325  60 
$ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms); 
26265  61 
val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"}; 
26325  62 
fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"}); 
63 
fun mk_split ty = Sign.mk_const thy 

64 
(@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]); 

26589  65 
fun mk_scomp_split ty t t' = 
66 
StateMonad.scomp (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*) 

26325  67 
(mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t'))); 
26589  68 
fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty 
26325  69 
(Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i) 
26265  70 
val t = fold_rev mk_bindclause bounds (return $ check); 
71 
in Abs ("n", @{typ index}, t) end; 

72 

28309  73 
fun compile_generator_expr thy t = 
26265  74 
let 
28309  75 
val tys = (map snd o fst o strip_abs) t; 
76 
val t' = mk_generator_expr thy t tys; 

30970
3fe2e418a071
generic postprocessing scheme for term evaluations
haftmann
parents:
30945
diff
changeset

77 
val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref) 
3fe2e418a071
generic postprocessing scheme for term evaluations
haftmann
parents:
30945
diff
changeset

78 
(fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' []; 
3fe2e418a071
generic postprocessing scheme for term evaluations
haftmann
parents:
30945
diff
changeset

79 
in f #> Random_Engine.run end; 
26265  80 

81 
end 

82 
*} 

83 

28309  84 
setup {* 
30945  85 
Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I)) 
86 
#> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of) 

28309  87 
*} 
88 

30945  89 

90 
subsection {* Type @{typ "'a \<Rightarrow> 'b"} *} 

91 

92 
ML {* 

93 
structure Random_Engine = 

94 
struct 

95 

96 
open Random_Engine; 

97 

98 
fun random_fun (T1 : typ) (T2 : typ) (eq : 'a > 'a > bool) (term_of : 'a > term) 

99 
(random : Random_Engine.seed > ('b * (unit > term)) * Random_Engine.seed) 

100 
(random_split : Random_Engine.seed > Random_Engine.seed * Random_Engine.seed) 

101 
(seed : Random_Engine.seed) = 

102 
let 

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

104 
val state = ref (seed', [], Const (@{const_name undefined}, T1 > T2)); 

105 
val fun_upd = Const (@{const_name fun_upd}, 

106 
(T1 > T2) > T1 > T2 > T1 > T2); 

107 
fun random_fun' x = 

108 
let 

109 
val (seed, fun_map, f_t) = ! state; 

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

111 
of SOME y => y 

112 
 NONE => let 

113 
val t1 = term_of x; 

114 
val ((y, t2), seed') = random seed; 

115 
val fun_map' = (x, y) :: fun_map; 

116 
val f_t' = fun_upd $ f_t $ t1 $ t2 (); 

117 
val _ = state := (seed', fun_map', f_t'); 

118 
in y end 

119 
end; 

120 
fun term_fun' () = #3 (! state); 

121 
in ((random_fun', term_fun'), seed'') end; 

122 

26265  123 
end 
30945  124 
*} 
125 

126 
axiomatization 

127 
random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) 

128 
\<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) 

129 
\<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" 

130 

131 
code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun") 

132 
 {* With enough criminal energy this can be abused to derive @{prop False}; 

133 
for this reason we use a distinguished target @{text Quickcheck} 

134 
not spoiling the regular trusted code generation *} 

135 

136 
instantiation "fun" :: ("{eq, term_of}", "{type, random}") random 

137 
begin 

138 

139 
definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where 

140 
"random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) split_seed" 

141 

142 
instance .. 

143 

144 
end 

145 

146 
code_reserved Quickcheck Random_Engine 

147 

148 
end 