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 


13 
class random = type +


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


15 


16 
print_classes


17 


18 
instantiation itself :: (type) random


19 
begin


20 


21 
definition


22 
"random _ = return TYPE('a)"


23 


24 
instance ..


25 


26 
end


27 


28 
lemma random_aux_if:


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


30 
assumes "random' 0 j = undefined"


31 
and "\<And>i. random' (Suc_index i) j = rhs2 i"


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


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


34 


35 
setup {*


36 
let


37 
exception REC;


38 
fun random_inst tyco thy =


39 
let


40 
val { descr, index, ... } = DatatypePackage.the_datatype thy tyco;


41 
val _ = if length descr > 1 then raise REC else ();


42 
val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco;


43 
val vs = (map o apsnd)


44 
(curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;


45 
val ty = Type (tyco, map TFree vs);


46 
val typ_of = DatatypeAux.typ_of_dtyp descr vs;


47 
val SOME (_, _, constrs) = AList.lookup (op =) descr index;


48 
val randomN = NameSpace.base @{const_name random};


49 
val random_aux_name = randomN ^ "_" ^ Class.type_name tyco ^ "'";


50 
fun lift_ty ty = StateMonad.liftT ty @{typ seed};


51 
val ty_aux = @{typ index} > @{typ index} > lift_ty ty;


52 
fun random ty =


53 
Const (@{const_name random}, @{typ index} > lift_ty ty);


54 
val random_aux = Free (random_aux_name, ty_aux);


55 
fun add_cons_arg dty (is_rec, t) =


56 
let


57 
val ty' = typ_of dty;


58 
val rec_call = case try DatatypeAux.dest_DtRec dty


59 
of SOME index' => index = index'


60 
 NONE => false


61 
val random' = if rec_call


62 
then random_aux $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"}


63 
else random ty' $ @{term "j\<Colon>index"}


64 
val is_rec' = is_rec orelse DatatypeAux.is_rec_type dty;


65 
val t' = StateMonad.mbind ty' ty @{typ seed} random' (Abs ("", ty', t))


66 
in (is_rec', t') end;


67 
fun mk_cons_t (c, dtys) =


68 
let


69 
val ty' = map typ_of dtys > ty;


70 
val t = StateMonad.return ty @{typ seed} (list_comb (Const (c, ty'),


71 
map Bound (length dtys  1 downto 0)));


72 
val (is_rec, t') = fold_rev add_cons_arg dtys (false, t);


73 
in (is_rec, StateMonad.run ty @{typ seed} t') end;


74 
fun check_empty [] = NONE


75 
 check_empty xs = SOME xs;


76 
fun bundle_cons_ts cons_ts =


77 
let


78 
val ts = map snd cons_ts;


79 
val t = HOLogic.mk_list (lift_ty ty) ts;


80 
val t' = Const (@{const_name select}, HOLogic.listT (lift_ty ty) > lift_ty (lift_ty ty)) $ t;


81 
val t'' = Const (@{const_name collapse}, lift_ty (lift_ty ty) > lift_ty ty) $ t';


82 
in t'' end;


83 
fun bundle_conss (some_rec_t, nonrec_t) =


84 
let


85 
val t = case some_rec_t


86 
of SOME rec_t => Const (@{const_name collapse}, lift_ty (lift_ty ty) > lift_ty ty)


87 
$ (Const (@{const_name select_default},


88 
@{typ index} > lift_ty ty > lift_ty ty > lift_ty (lift_ty ty))


89 
$ @{term "i\<Colon>index"} $ rec_t $ nonrec_t)


90 
 NONE => nonrec_t


91 
in t end;


92 
val random_rhs = constrs


93 
> map mk_cons_t


94 
> List.partition fst


95 
> apfst (Option.map bundle_cons_ts o check_empty)


96 
> apsnd bundle_cons_ts


97 
> bundle_conss;


98 
val random_aux_undef = (HOLogic.mk_Trueprop o HOLogic.mk_eq)


99 
(random_aux $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Const (@{const_name undefined}, lift_ty ty))


100 
val random_aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)


101 
(random_aux $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, random_rhs);


102 
val random_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (Const (@{const_name random},


103 
@{typ index} > lift_ty ty) $ @{term "i\<Colon>index"},


104 
random_aux $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"});


105 
val del_func = Attrib.internal (fn _ => Thm.declaration_attribute


106 
(fn thm => Context.mapping (Code.del_func thm) I));


107 
fun add_code simps lthy =


108 
let


109 
val thy = ProofContext.theory_of lthy;


110 
val thm = @{thm random_aux_if}


111 
> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] [SOME (Thm.cterm_of thy random_aux)]


112 
> (fn thm => thm OF simps)


113 
> singleton (ProofContext.export lthy (ProofContext.init thy))


114 
in


115 
lthy


116 
> LocalTheory.theory (PureThy.note Thm.internalK (random_aux_name ^ "_code", thm)


117 
#> Code.add_func)


118 
end;


119 
in


120 
thy


121 
> TheoryTarget.instantiation ([tyco], vs, @{sort random})


122 
> PrimrecPackage.add_primrec [(random_aux_name, SOME ty_aux, NoSyn)]


123 
[(("", [del_func]), random_aux_undef), (("", [del_func]), random_aux_eq)]


124 
> add_code


125 
> `(fn lthy => Syntax.check_term lthy random_eq)


126 
> (fn eq => Specification.definition (NONE, (("", []), eq)))


127 
> snd


128 
> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))


129 
> LocalTheory.exit


130 
> ProofContext.theory_of


131 
end;


132 
fun add_random_inst [tyco] = (fn thy => random_inst tyco thy handle REC =>


133 
(warning ("Will not generated random elements for mutual recursive type " ^ quote tyco); thy))


134 
 add_random_inst tycos = tap (fn _ => warning


135 
("Will not generated random elements for mutual recursive type(s) " ^ commas (map quote tycos)));


136 
in DatatypePackage.interpretation add_random_inst end


137 
*}


138 


139 
instantiation int :: random


140 
begin


141 


142 
definition


143 
"random n = (do


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


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


146 
done)"


147 


148 
instance ..


149 


150 
end


151 


152 
instantiation set :: (random) random


153 
begin


154 


155 
primrec random_set' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> 'a set \<times> seed" where


156 
"random_set' 0 j = undefined"


157 
 "random_set' (Suc_index i) j = collapse (select_default i


158 
(do x \<leftarrow> random i; xs \<leftarrow> random_set' i j; return (insert x xs) done)


159 
(return {}))"


160 


161 
lemma random_set'_code [code func]:


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


163 
(do x \<leftarrow> random (i  1); xs \<leftarrow> random_set' (i  1) j; return (insert x xs) done)


164 
(return {})) s)"


165 
by (rule random_aux_if random_set'.simps)+


166 


167 
definition


168 
"random i = random_set' i i"


169 


170 
instance ..


171 


172 
end


173 


174 
code_reserved SML Quickcheck


175 


176 


177 
subsection {* Quickcheck generator *}


178 


179 
ML {*


180 
structure Quickcheck =


181 
struct


182 


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


184 


185 
fun mk_generator_expr prop tys =


186 
let


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


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


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


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


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


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


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


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


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


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


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


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


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


200 


201 
fun compile_generator_expr thy prop tys =


202 
let


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


204 
(mk_generator_expr prop tys) [];


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


206 


207 
fun VALUE prop tys thy =


208 
let


209 
val t = mk_generator_expr prop tys;


210 
val eq = Logic.mk_equals (Free ("VALUE", fastype_of t), t)


211 
in


212 
thy


213 
> TheoryTarget.init NONE


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


215 
> snd


216 
> LocalTheory.exit


217 
> ProofContext.theory_of


218 
end;


219 


220 
end


221 
*}


222 


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


224 
export_code VALUE in SML module_name QuickcheckExample file "~~/../../gen_code/quickcheck.ML"


225 
use "~~/../../gen_code/quickcheck.ML"


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


227 


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


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


230 


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


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


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


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


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


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


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


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


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


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


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


242 


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


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


245 


246 
(*definition "FOO = (True, Suc 0)"


247 


248 
code_module (test) QuickcheckExample


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


250 
contains FOO*)


251 


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


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


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


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


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


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


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


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


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


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


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


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


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


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


266 


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


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


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


270 


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


289 


290 
subsection {* Incremental function generator *}


291 


292 
ML {*


293 
structure Quickcheck =


294 
struct


295 


296 
open Quickcheck;


297 


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


299 
(random : Random_Engine.seed > 'b * Random_Engine.seed)


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


301 
(seed : Random_Engine.seed) =


302 
let


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


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


305 
fun random_fun' x =


306 
let


307 
val (seed, fun_map) = ! state;


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


309 
of SOME y => y


310 
 NONE => let


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


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


313 
in y end


314 
end;


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


316 


317 
end


318 
*}


319 


320 
axiomatization


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


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


323 


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


325 


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


327 
begin


328 


329 
instance ..


330 


331 
end


332 


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


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


335 


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


337 
begin


338 


339 
definition


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


341 


342 
instance ..


343 


344 
end


345 


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


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


348 


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


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


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


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


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


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


355 


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


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


358 


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


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


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


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


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


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


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


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


367 


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


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


370 


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


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


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


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


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


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


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


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


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


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


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


382 


383 
end
