author  haftmann 
Thu, 25 Sep 2008 19:15:50 +0200  
changeset 28360  cf3542e34726 
parent 28335  25326092cf9a 
child 28370  37f56e6e702d 
permissions  rwrr 
26265  1 
(* ID: $Id$ 
2 
Author: Florian Haftmann, TU Muenchen 

3 
*) 

4 

5 
header {* A simple counterexample generator *} 

6 

7 
theory Quickcheck 

28228  8 
imports Random Code_Eval 
26265  9 
begin 
10 

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

12 

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

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

16 
text {* Type @{typ "'a itself"} *} 
26265  17 

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

21 
definition 

28335  22 
"random _ = return (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))" 
26265  23 

24 
instance .. 

25 

26 
end 

27 

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

28 
text {* Datatypes *} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

29 

28145  30 
definition 
31 
collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where 

32 
"collapse f = (do g \<leftarrow> f; g done)" 

33 

34 
ML {* 

35 
structure StateMonad = 

36 
struct 

37 

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

39 
fun liftT' sT = sT > sT; 

40 

41 
fun return T sT x = Const (@{const_name return}, T > liftT T sT) $ x; 

42 

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

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

45 

46 
end; 

47 
*} 

48 

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

49 
lemma random'_if: 
26325  50 
fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed" 
26265  51 
assumes "random' 0 j = undefined" 
52 
and "\<And>i. random' (Suc_index i) j = rhs2 i" 

53 
shows "random' i j s = (if i = 0 then undefined else rhs2 (i  1) s)" 

54 
by (cases i rule: index.exhaust) (insert assms, simp_all add: undefined_fun) 

55 

56 
setup {* 

57 
let 

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

58 
exception REC of string; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

59 
fun mk_collapse thy ty = Sign.mk_const thy 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

60 
(@{const_name collapse}, [@{typ seed}, ty]); 
26325  61 
fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"}); 
62 
fun mk_split thy ty ty' = Sign.mk_const thy 

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

26589  64 
fun mk_scomp_split thy ty ty' t t' = 
65 
StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t 

26325  66 
(mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t'))) 
67 
fun mk_cons thy this_ty (c, args) = 

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

69 
val tys = map (fst o fst) args; 
26325  70 
val c_ty = tys > this_ty; 
71 
val c = Const (c, tys > this_ty); 

72 
val t_indices = map (curry ( op * ) 2) (length tys  1 downto 0); 

73 
val c_indices = map (curry ( op + ) 1) t_indices; 

74 
val c_t = list_comb (c, map Bound c_indices); 

28335  75 
val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep 
26325  76 
(list_comb (c, map (fn k => Bound (k + 1)) t_indices)) 
77 
> map_aterms (fn t as Bound _ => t $ @{term "()"}  t => t)); 

78 
val return = StateMonad.return (term_ty this_ty) @{typ seed} 

79 
(HOLogic.mk_prod (c_t, t_t)); 

80 
val t = fold_rev (fn ((ty, _), random) => 

26589  81 
mk_scomp_split thy ty this_ty random) 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

82 
args return; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

83 
val is_rec = exists (snd o fst) args; 
28145  84 
in (is_rec, t) end; 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

85 
fun mk_conss thy ty [] = NONE 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

86 
 mk_conss thy ty [(_, t)] = SOME t 
26325  87 
 mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $ 
88 
(Sign.mk_const thy (@{const_name select}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $ 

89 
HOLogic.mk_list (StateMonad.liftT (term_ty ty) @{typ seed}) (map snd ts))); 

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

90 
fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) = 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

92 
val SOME t_atom = mk_conss thy ty ts_atom; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

93 
in case mk_conss thy ty ts_rec 
26325  94 
of SOME t_rec => mk_collapse thy (term_ty ty) $ 
95 
(Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $ 

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

96 
@{term "i\<Colon>index"} $ t_rec $ t_atom) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

97 
 NONE => t_atom 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

98 
end; 
26325  99 
fun mk_random_eqs thy vs tycos = 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

101 
val this_ty = Type (hd tycos, map TFree vs); 
26325  102 
val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed}; 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

103 
val random_name = NameSpace.base @{const_name random}; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

104 
val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'"; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

105 
fun random ty = Sign.mk_const thy (@{const_name random}, [ty]); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

106 
val random' = Free (random'_name, 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

107 
@{typ index} > @{typ index} > this_ty'); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

108 
fun atom ty = ((ty, false), random ty $ @{term "j\<Colon>index"}); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

109 
fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"}); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

110 
fun rtyp tyco tys = raise REC 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

111 
("Will not generate random elements for mutual recursive type " ^ quote (hd tycos)); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

112 
val rhss = DatatypePackage.construction_interpretation thy 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

113 
{ atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos 
26325  114 
> (map o apsnd o map) (mk_cons thy this_ty) 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

115 
> (map o apsnd) (List.partition fst) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

116 
> map (mk_clauses thy this_ty) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

117 
val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [ 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

118 
(random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Const (@{const_name undefined}, this_ty')), 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

119 
(random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

120 
]))) rhss; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

121 
in eqss end; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

122 
fun random_inst [tyco] thy = 
26265  123 
let 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

124 
val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

125 
val vs = (map o apsnd) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

126 
(curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

127 
val { descr, index, ... } = DatatypePackage.the_datatype thy tyco; 
26325  128 
val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco; 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

129 
val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

130 
(Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>index"}, 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

131 
random' $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"}) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

132 
val del_func = Attrib.internal (fn _ => Thm.declaration_attribute 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

133 
(fn thm => Context.mapping (Code.del_func thm) I)); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

134 
fun add_code simps lthy = 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

136 
val thy = ProofContext.theory_of lthy; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

137 
val thm = @{thm random'_if} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

138 
> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')] 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

139 
> (fn thm => thm OF simps) 
28360  140 
> singleton (ProofContext.export lthy (ProofContext.init thy)); 
141 
val c = (fst o dest_Const o fst o strip_comb o fst 

142 
o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm; 

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

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

144 
lthy 
28360  145 
> LocalTheory.theory (Code.del_funcs c 
146 
#> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal]) 

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

147 
#> Code.add_func) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

148 
end; 
26265  149 
in 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

151 
> TheoryTarget.instantiation ([tyco], vs, @{sort random}) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

152 
> PrimrecPackage.add_primrec 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28054
diff
changeset

153 
[(Name.binding (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)] 
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28054
diff
changeset

154 
(map (fn eq => ((Name.no_binding, [del_func]), eq)) eqs') 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

155 
> add_code 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

156 
> `(fn lthy => Syntax.check_term lthy eq) 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

157 
> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq))) 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

158 
> snd 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

159 
> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

160 
> LocalTheory.exit 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

161 
> ProofContext.theory_of 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

163 
 random_inst tycos thy = raise REC 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

164 
("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos)); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

165 
fun add_random_inst tycos thy = random_inst tycos thy 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

166 
handle REC msg => (warning msg; thy); 
26265  167 
in DatatypePackage.interpretation add_random_inst end 
168 
*} 

169 

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

170 
text {* Type @{typ int} *} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

171 

26265  172 
instantiation int :: random 
173 
begin 

174 

175 
definition 

176 
"random n = (do 

26325  177 
(b, _) \<leftarrow> random n; 
178 
(m, t) \<leftarrow> random n; 

28335  179 
return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ())) 
180 
else ( int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \<Rightarrow> int)) 

181 
(Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ())))) 

26265  182 
done)" 
183 

184 
instance .. 

185 

186 
end 

187 

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

188 
text {* Type @{typ "'a \<Rightarrow> 'b"} *} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

189 

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

190 
ML {* 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

191 
structure Random_Engine = 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

193 

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

194 
open Random_Engine; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

195 

26325  196 
fun random_fun (T1 : typ) (T2 : typ) (eq : 'a > 'a > bool) (term_of : 'a > term) 
197 
(random : Random_Engine.seed > ('b * (unit > term)) * Random_Engine.seed) 

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

198 
(random_split : Random_Engine.seed > Random_Engine.seed * Random_Engine.seed) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

199 
(seed : Random_Engine.seed) = 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

201 
val (seed', seed'') = random_split seed; 
26325  202 
val state = ref (seed', [], Const (@{const_name arbitrary}, T1 > T2)); 
203 
val fun_upd = Const (@{const_name fun_upd}, 

204 
(T1 > T2) > T1 > T2 > T1 > T2); 

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

205 
fun random_fun' x = 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

206 
let 
26325  207 
val (seed, fun_map, f_t) = ! state; 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

208 
in case AList.lookup (uncurry eq) fun_map x 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

209 
of SOME y => y 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

210 
 NONE => let 
26325  211 
val t1 = term_of x; 
212 
val ((y, t2), seed') = random seed; 

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

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

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

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

216 
in y end 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

217 
end; 
26325  218 
fun term_fun' () = #3 (! state); 
219 
in ((random_fun', term_fun'), seed'') end; 

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

220 

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

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

222 
*} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

223 

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

224 
axiomatization 
28335  225 
random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) 
26325  226 
\<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) 
227 
\<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" 

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

228 

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

229 
code_const random_fun_aux (SML "Random'_Engine.random'_fun") 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

230 

26325  231 
instantiation "fun" :: ("{eq, term_of}", "{type, random}") random 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

233 

26325  234 
definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where 
28335  235 
"random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) split_seed" 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

236 

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

237 
instance .. 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

238 

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

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

240 

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

241 
code_reserved SML Random_Engine 
26265  242 

243 

244 
subsection {* Quickcheck generator *} 

245 

246 
ML {* 

247 
structure Quickcheck = 

248 
struct 

249 

28309  250 
open Quickcheck; 
251 

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

26325  254 
fun mk_generator_expr thy prop tys = 
26265  255 
let 
26325  256 
val bound_max = length tys  1; 
257 
val bounds = map_index (fn (i, ty) => 

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

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

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

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

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

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

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

274 

28309  275 
fun compile_generator_expr thy t = 
26265  276 
let 
28309  277 
val tys = (map snd o fst o strip_abs) t; 
278 
val t' = mk_generator_expr thy t tys; 

279 
val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy t' []; 

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

26265  281 

282 
end 

283 
*} 

284 

28309  285 
setup {* 
286 
Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of) 

287 
*} 

288 

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

289 
subsection {* Examples *} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

290 

28315  291 
theorem "map g (map f xs) = map (g o f) xs" 
292 
quickcheck [generator = code] 

293 
by (induct xs) simp_all 

26325  294 

28315  295 
theorem "map g (map f xs) = map (f o g) xs" 
296 
quickcheck [generator = code] 

297 
oops 

298 

299 
theorem "rev (xs @ ys) = rev ys @ rev xs" 

300 
quickcheck [generator = code] 

301 
by simp 

26265  302 

28315  303 
theorem "rev (xs @ ys) = rev xs @ rev ys" 
304 
quickcheck [generator = code] 

305 
oops 

306 

307 
theorem "rev (rev xs) = xs" 

308 
quickcheck [generator = code] 

309 
by simp 

310 

311 
theorem "rev xs = xs" 

312 
quickcheck [generator = code] 

313 
oops 

314 

315 
primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where 

316 
"app [] x = x" 

317 
 "app (f # fs) x = app fs (f x)" 

26265  318 

28315  319 
lemma "app (fs @ gs) x = app gs (app fs x)" 
320 
quickcheck [generator = code] 

321 
by (induct fs arbitrary: x) simp_all 

322 

323 
lemma "app (fs @ gs) x = app fs (app gs x)" 

324 
quickcheck [generator = code] 

325 
oops 

326 

327 
primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where 

328 
"occurs a [] = 0" 

329 
 "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)" 

26265  330 

28315  331 
primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
332 
"del1 a [] = []" 

333 
 "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))" 

334 

335 
lemma "Suc (occurs a (del1 a xs)) = occurs a xs" 

336 
 {* Wrong. Precondition needed.*} 

337 
quickcheck [generator = code] 

338 
oops 

26265  339 

28315  340 
lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" 
341 
quickcheck [generator = code] 

342 
 {* Also wrong.*} 

343 
oops 

344 

345 
lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" 

346 
quickcheck [generator = code] 

347 
by (induct xs) auto 

26265  348 

28315  349 
primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
350 
"replace a b [] = []" 

351 
 "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 

352 
else (x#(replace a b xs)))" 

353 

354 
lemma "occurs a xs = occurs b (replace a b xs)" 

355 
quickcheck [generator = code] 

356 
 {* Wrong. Precondition needed.*} 

357 
oops 

358 

359 
lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)" 

360 
quickcheck [generator = code] 

361 
by (induct xs) simp_all 

362 

363 

364 
subsection {* Trees *} 

365 

366 
datatype 'a tree = Twig  Leaf 'a  Branch "'a tree" "'a tree" 

367 

368 
primrec leaves :: "'a tree \<Rightarrow> 'a list" where 

369 
"leaves Twig = []" 

370 
 "leaves (Leaf a) = [a]" 

371 
 "leaves (Branch l r) = (leaves l) @ (leaves r)" 

372 

373 
primrec plant :: "'a list \<Rightarrow> 'a tree" where 

374 
"plant [] = Twig " 

375 
 "plant (x#xs) = Branch (Leaf x) (plant xs)" 

26265  376 

28315  377 
primrec mirror :: "'a tree \<Rightarrow> 'a tree" where 
378 
"mirror (Twig) = Twig " 

379 
 "mirror (Leaf a) = Leaf a " 

380 
 "mirror (Branch l r) = Branch (mirror r) (mirror l)" 

26265  381 

28315  382 
theorem "plant (rev (leaves xt)) = mirror xt" 
383 
quickcheck [generator = code] 

384 
{* Wrong! *} 

385 
oops 

386 

387 
theorem "plant (leaves xt @ leaves yt) = Branch xt yt" 

388 
quickcheck [generator = code] 

389 
{* Wrong! *} 

390 
oops 

391 

392 
datatype 'a ntree = Tip "'a"  Node "'a" "'a ntree" "'a ntree" 

26265  393 

28315  394 
primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where 
395 
"inOrder (Tip a)= [a]" 

396 
 "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)" 

397 

398 
primrec root :: "'a ntree \<Rightarrow> 'a" where 

399 
"root (Tip a) = a" 

400 
 "root (Node f x y) = f" 

26265  401 

28315  402 
theorem "hd (inOrder xt) = root xt" 
403 
quickcheck [generator = code] 

404 
{* Wrong! *} 

405 
oops 

26325  406 

28315  407 
lemma "int (f k) = k" 
408 
quickcheck [generator = code] 

409 
oops 

26325  410 

26265  411 
end 