author | huffman |
Wed, 18 Feb 2009 19:32:26 -0800 | |
changeset 29985 | 57975b45ab70 |
parent 29823 | 0ab754d13ccd |
child 30945 | 0418e9bffbba |
permissions | -rw-r--r-- |
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 |