author  haftmann 
Wed, 09 Apr 2008 17:46:17 +0200  
changeset 26589  43cb72871897 
parent 26325  6ecae5c8175b 
child 26829  229e8078b1e0 
permissions  rwrr 
26265  1 
(* ID: $Id$ 
2 
Author: Florian Haftmann, TU Muenchen 

3 
*) 

4 

5 
header {* A simple counterexample generator *} 

6 

7 
theory Quickcheck 

8 
imports Random Eval 

9 
begin 

10 

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

12 

26325  13 
class random = rtype + 
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 

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

21 
definition 

26325  22 
"random _ = return (TYPE('a), \<lambda>u. Eval.Const (STR ''TYPE'') RTYPE('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 

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

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

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

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

36 

37 
setup {* 

38 
let 

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

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

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

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

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

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

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

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

50 
val tys = map (fst o fst) args; 
26325  51 
val c_ty = tys > this_ty; 
52 
val c = Const (c, tys > this_ty); 

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

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

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

56 
val t_t = Abs ("", @{typ unit}, Eval.mk_term Free RType.rtype 

57 
(list_comb (c, map (fn k => Bound (k + 1)) t_indices)) 

58 
> map_aterms (fn t as Bound _ => t $ @{term "()"}  t => t)); 

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

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

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

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

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

64 
val is_rec = exists (snd o fst) args; 
26325  65 
in (is_rec, StateMonad.run (term_ty this_ty) @{typ seed} t) end; 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

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

70 
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

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

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

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

74 
in case mk_conss thy ty ts_rec 
26325  75 
of SOME t_rec => mk_collapse thy (term_ty ty) $ 
76 
(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

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

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

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

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

82 
val this_ty = Type (hd tycos, map TFree vs); 
26325  83 
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

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

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

86 
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

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

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

89 
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

90 
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

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

92 
("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

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

94 
{ atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos 
26325  95 
> (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

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

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

98 
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

99 
(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

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

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

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

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

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

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

107 
(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

108 
val { descr, index, ... } = DatatypePackage.the_datatype thy tyco; 
26325  109 
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

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

111 
(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

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

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

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

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

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

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

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

119 
> 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

120 
> (fn thm => thm OF simps) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

121 
> singleton (ProofContext.export lthy (ProofContext.init thy)) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

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

124 
> LocalTheory.theory (PureThy.note Thm.internalK (fst (dest_Free random') ^ "_code", thm) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

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

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

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

130 
> PrimrecPackage.add_primrec 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

131 
[(fst (dest_Free random'), SOME (snd (dest_Free random')), NoSyn)] 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

132 
(map (fn eq => (("", [del_func]), eq)) eqs') 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

134 
> `(fn lthy => Syntax.check_term lthy eq) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

135 
> (fn eq => Specification.definition (NONE, (("", []), eq))) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

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

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

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

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

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

142 
("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

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

144 
handle REC msg => (warning msg; thy); 
26265  145 
in DatatypePackage.interpretation add_random_inst end 
146 
*} 

147 

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

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

149 

26265  150 
instantiation int :: random 
151 
begin 

152 

153 
definition 

154 
"random n = (do 

26325  155 
(b, _) \<leftarrow> random n; 
156 
(m, t) \<leftarrow> random n; 

157 
return (if b then (int m, \<lambda>u. Eval.App (Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ())) 

158 
else ( int m, \<lambda>u. Eval.App (Eval.Const (STR ''HOL.uminus_class.uminus'') RTYPE(int \<Rightarrow> int)) 

159 
(Eval.App (Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ())))) 

26265  160 
done)" 
161 

162 
instance .. 

163 

164 
end 

165 

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

166 
text {* Type @{typ "'a set"} *} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

167 

26325  168 
instantiation set :: ("{random, type}") random 
26265  169 
begin 
170 

26325  171 
primrec random_set' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a\<Colon>{random, type} set \<times> (unit \<Rightarrow> term)) \<times> seed" where 
26265  172 
"random_set' 0 j = undefined" 
173 
 "random_set' (Suc_index i) j = collapse (select_default i 

26325  174 
(do (x, t) \<leftarrow> random i; 
175 
(xs, ts) \<leftarrow> random_set' i j; 

176 
return (insert x xs, \<lambda>u. Eval.App (Eval.App (Eval.Const (STR ''insert'') RTYPE('a \<Rightarrow> 'a set \<Rightarrow> 'a set)) (t ())) (ts ())) done) 

177 
(return ({}, \<lambda>u. Eval.Const (STR ''{}'') RTYPE('a set))))" 

26265  178 

179 
lemma random_set'_code [code func]: 

180 
"random_set' i j s = (if i = 0 then undefined else collapse (select_default (i  1) 

26325  181 
(do (x \<Colon> 'a\<Colon>{random, type}, t) \<leftarrow> random (i  1); 
182 
(xs, ts) \<leftarrow> random_set' (i  1) j; 

183 
return (insert x xs, \<lambda>u. Eval.App (Eval.App (Eval.Const (STR ''insert'') RTYPE('a \<Rightarrow> 'a set \<Rightarrow> 'a set)) (t ())) (ts ())) done) 

184 
(return ({}, \<lambda>u. Eval.Const (STR ''{}'') RTYPE('a set)))) s)" 

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

185 
by (rule random'_if random_set'.simps)+ 
26265  186 

187 
definition 

188 
"random i = random_set' i i" 

189 

190 
instance .. 

191 

192 
end 

193 

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

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

195 

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

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

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

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

199 

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

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

201 

26325  202 
fun random_fun (T1 : typ) (T2 : typ) (eq : 'a > 'a > bool) (term_of : 'a > term) 
203 
(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

204 
(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

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

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

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

210 
(T1 > T2) > T1 > T2 > T1 > T2); 

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

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

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

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

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

216 
 NONE => let 
26325  217 
val t1 = term_of x; 
218 
val ((y, t2), seed') = random seed; 

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

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

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

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

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

223 
end; 
26325  224 
fun term_fun' () = #3 (! state); 
225 
in ((random_fun', term_fun'), seed'') end; 

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

226 

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

227 
end 
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 

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

230 
axiomatization 
26325  231 
random_fun_aux :: "rtype \<Rightarrow> rtype \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) 
232 
\<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) 

233 
\<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

234 

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

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

236 

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

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

239 

26325  240 
definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where 
241 
"random n = random_fun_aux RTYPE('a) RTYPE('b) (op =) Eval.term_of (random n) split_seed" 

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

242 

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

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

244 

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

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

246 

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

247 
code_reserved SML Random_Engine 
26265  248 

249 

250 
subsection {* Quickcheck generator *} 

251 

252 
ML {* 

253 
structure Quickcheck = 

254 
struct 

255 

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

257 

26325  258 
fun mk_generator_expr thy prop tys = 
26265  259 
let 
26325  260 
val bound_max = length tys  1; 
261 
val bounds = map_index (fn (i, ty) => 

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

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

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

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

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

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

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

278 

279 
fun compile_generator_expr thy prop tys = 

280 
let 

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

26325  282 
(mk_generator_expr thy prop tys) []; 
26265  283 
in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end; 
284 

285 
fun VALUE prop tys thy = 

286 
let 

26325  287 
val t = mk_generator_expr thy prop tys; 
26265  288 
val eq = Logic.mk_equals (Free ("VALUE", fastype_of t), t) 
289 
in 

290 
thy 

291 
> TheoryTarget.init NONE 

292 
> Specification.definition (NONE, (("", []), eq)) 

293 
> snd 

294 
> LocalTheory.exit 

295 
> ProofContext.theory_of 

296 
end; 

297 

298 
end 

299 
*} 

300 

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

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

302 

26325  303 
(*export_code "random :: index \<Rightarrow> seed \<Rightarrow> ((_ \<Rightarrow> _) \<times> (unit \<Rightarrow> term)) \<times> seed" 
304 
in SML file *) 

26275  305 

26325  306 
(*setup {* Quickcheck.VALUE 
307 
@{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *} 

308 

26265  309 
export_code VALUE in SML module_name QuickcheckExample file "~~/../../gen_code/quickcheck.ML" 
310 
use "~~/../../gen_code/quickcheck.ML" 

311 
ML {* Random_Engine.run (QuickcheckExample.range 1) *}*) 

312 

26325  313 
(*definition "FOO = (True, Suc 0)" 
314 

315 
code_module (test) QuickcheckExample 

316 
file "~~/../../gen_code/quickcheck'.ML" 

317 
contains FOO*) 

318 

26265  319 
ML {* val f = Quickcheck.compile_generator_expr @{theory} 
320 
@{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *} 

321 

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

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

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

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

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

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

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

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

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

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

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

333 

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

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

336 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

351 

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

353 
@{term "\<lambda>(xs\<Colon>int list) ys. rev (xs @ ys) = rev xs @ rev ys"} 

354 
[@{typ "int list"}, @{typ "int list"}] *} 

355 

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

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

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

359 
ML {* f 20 > (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 25 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

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

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

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

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

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

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

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

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

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

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

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

374 

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

376 
@{term "\<lambda>(A \<Colon> nat set) B. card (A \<union> B) = card A + card B"} [@{typ "nat set"}, @{typ "nat set"}] *} 

377 

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

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

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

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

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

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

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

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

386 

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

388 
@{term "\<lambda>(s \<Colon> string). s \<noteq> rev s"} [@{typ string}] *} 

389 

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

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

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

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

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

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

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

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

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

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

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

401 

26325  402 
ML {* val f = Quickcheck.compile_generator_expr @{theory} 
403 
@{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *} 

404 

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

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

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

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

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

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

411 

26265  412 
end 