author  haftmann 
Fri, 06 Feb 2009 15:15:32 +0100  
changeset 29823  0ab754d13ccd 
parent 29808  b8b9d529663b 
child 30945  0418e9bffbba 
permissions  rwrr 
29132  1 
(* Author: Florian Haftmann, TU Muenchen *) 
26265  2 

3 
header {* A simple counterexample generator *} 

4 

5 
theory Quickcheck 

29132  6 
imports Random Code_Eval Map 
26265  7 
begin 
8 

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

10 

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

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

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

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

19 
definition 

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

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

22 
instance .. 

23 

24 
end 

25 

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

26 

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

27 
subsection {* Quickcheck generator *} 
29132  28 

29 
ML {* 

30 
structure StateMonad = 

31 
struct 

32 

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

34 
fun liftT' sT = sT > sT; 

35 

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

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

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

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

40 

41 
end; 

42 

26265  43 
structure Quickcheck = 
44 
struct 

45 

28309  46 
open Quickcheck; 
47 

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

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

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

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

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

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

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

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

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

70 

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

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

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

26265  77 

78 
end 

79 
*} 

80 

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

83 
*} 

84 

26265  85 
end 