author  haftmann 
Thu, 21 May 2009 09:07:25 +0200  
changeset 31223  87bde6b5f793 
parent 31211  ba0ad1c020ee 
child 31245  f8dcca332d4e 
permissions  rwrr 
29132  1 
(* Author: Florian Haftmann, TU Muenchen *) 
26265  2 

3 
header {* A simple counterexample generator *} 

4 

5 
theory Quickcheck 

31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31194
diff
changeset

6 
imports Random Code_Eval 
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 + 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

16 
fixes random :: "code_numeral \<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); 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

52 
in Abs ("n", @{typ code_numeral}, 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 
instantiation bool :: random 

74 
begin 

75 

76 
definition 

31194  77 
"random i = Random.range i o\<rightarrow> 
78 
(\<lambda>k. Pair (if (k div 2 = 0) then Code_Eval.valtermify True else Code_Eval.valtermify False))" 

31179  79 

80 
instance .. 

81 

82 
end 

83 

84 
instantiation itself :: (typerep) random 

85 
begin 

86 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

87 
definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where 
31194  88 
"random_itself _ = Pair (Code_Eval.valtermify TYPE('a))" 
31179  89 

90 
instance .. 

91 

92 
end 

93 

94 
text {* Type @{typ "'a \<Rightarrow> 'b"} *} 

30945  95 

96 
ML {* 

97 
structure Random_Engine = 

98 
struct 

99 

100 
open Random_Engine; 

101 

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

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

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

105 
(seed : Random_Engine.seed) = 

106 
let 

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

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

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

110 
(T1 > T2) > T1 > T2 > T1 > T2); 

111 
fun random_fun' x = 

112 
let 

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

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

115 
of SOME y => y 

116 
 NONE => let 

117 
val t1 = term_of x; 

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

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

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

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

122 
in y end 

123 
end; 

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

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

126 

26265  127 
end 
30945  128 
*} 
129 

31179  130 
axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) 
131 
\<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed) 

132 
\<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" 

30945  133 

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

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

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

137 
not spoiling the regular trusted code generation *} 

138 

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

140 
begin 

141 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

142 
definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where 
31179  143 
"random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed" 
30945  144 

145 
instance .. 

146 

147 
end 

148 

149 
code_reserved Quickcheck Random_Engine 

150 

31179  151 

152 
subsection {* Numeric types *} 

153 

154 
instantiation nat :: random 

155 
begin 

156 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

157 
definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where 
31194  158 
"random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair ( 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

159 
let n = Code_Numeral.nat_of k 
31194  160 
in (n, \<lambda>_. Code_Eval.term_of n)))" 
161 

162 
instance .. 

163 

164 
end 

165 

166 
instantiation int :: random 

167 
begin 

168 

169 
definition 

170 
"random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair ( 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

171 
let j = (if k \<ge> i then Code_Numeral.int_of (k  i) else  Code_Numeral.int_of (i  k)) 
31194  172 
in (j, \<lambda>_. Code_Eval.term_of j)))" 
31179  173 

174 
instance .. 

175 

30945  176 
end 
31179  177 

31223
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

178 
subsection {* Type copies *} 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

179 

87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

180 
setup {* 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

181 
let 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

182 

87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

183 
fun mk_random_typecopy tyco vs constr typ thy = 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

184 
let 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

185 
val Ts = map TFree vs; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

186 
val T = Type (tyco, Ts); 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

187 
fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"}) 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

188 
val Ttm = mk_termifyT T; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

189 
val typtm = mk_termifyT typ; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

190 
fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts)); 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

191 
fun mk_random T = mk_const @{const_name random} [T]; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

192 
val size = @{term "k\<Colon>code_numeral"}; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

193 
val v = "x"; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

194 
val t_v = Free (v, typtm); 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

195 
val t_constr = mk_const constr Ts; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

196 
val lhs = mk_random T $ size; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

197 
val rhs = HOLogic.mk_ST [(((mk_random typ) $ size, @{typ Random.seed}), SOME (v, typtm))] 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

198 
(HOLogic.mk_return Ttm @{typ Random.seed} 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

199 
(mk_const "Code_Eval.valapp" [typ, T] 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

200 
$ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v)) 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

201 
@{typ Random.seed} (SOME Ttm, @{typ Random.seed}); 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

202 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

203 
in 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

204 
thy 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

205 
> TheoryTarget.instantiation ([tyco], vs, @{sort random}) 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

206 
> `(fn lthy => Syntax.check_term lthy eq) 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

207 
> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

208 
> snd 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

209 
> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

210 
end; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

211 

87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

212 
fun ensure_random_typecopy tyco thy = 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

213 
let 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

214 
val SOME { vs = raw_vs, constr, typ = raw_typ, ... } = 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

215 
TypecopyPackage.get_info thy tyco; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

216 
val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)); 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

217 
val typ = map_atyps (fn TFree (v, sort) => 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

218 
TFree (v, constrain sort @{sort random})) raw_typ; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

219 
val vs' = Term.add_tfreesT typ []; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

220 
val vs = map (fn (v, sort) => 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

221 
(v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

222 
val do_inst = Sign.of_sort thy (typ, @{sort random}); 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

223 
in if do_inst then mk_random_typecopy tyco vs constr typ thy else thy end; 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

224 

87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

225 
in 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

226 

87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

227 
TypecopyPackage.interpretation ensure_random_typecopy 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

228 

87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

229 
end 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

230 
*} 
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

231 

31179  232 

233 
no_notation fcomp (infixl "o>" 60) 

234 
no_notation scomp (infixl "o\<rightarrow>" 60) 

235 

236 
end 