author | bulwahn |
Fri, 08 Apr 2011 16:31:14 +0200 | |
changeset 42306 | 51a08b2699d5 |
parent 42304 | 34366f39d32d |
child 42307 | 72e2fabb4bc2 |
permissions | -rw-r--r-- |
41923
f05fc0711bc7
renaming signatures and structures; correcting header
bulwahn
parents:
41920
diff
changeset
|
1 |
(* Title: HOL/Tools/Quickcheck/exhaustive_generators.ML |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
2 |
Author: Lukas Bulwahn, TU Muenchen |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
3 |
|
41918 | 4 |
Exhaustive generators for various types. |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
5 |
*) |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
6 |
|
41918 | 7 |
signature EXHAUSTIVE_GENERATORS = |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
8 |
sig |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
9 |
val compile_generator_expr: |
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
10 |
Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
11 |
val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
12 |
val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list |
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
13 |
val put_counterexample: (unit -> int -> int -> term list option) |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
14 |
-> Proof.context -> Proof.context |
41861
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
15 |
val put_counterexample_batch: (unit -> (int -> term list option) list) |
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
16 |
-> Proof.context -> Proof.context |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
17 |
val put_validator_batch: (unit -> (int -> bool) list) -> Proof.context -> Proof.context |
42306 | 18 |
exception Counterexample of term list |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
19 |
val smart_quantifier : bool Config.T |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
20 |
val quickcheck_pretty : bool Config.T |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
21 |
val setup: theory -> theory |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
22 |
end; |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
23 |
|
41918 | 24 |
structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS = |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
25 |
struct |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
26 |
|
40907 | 27 |
(* dynamic options *) |
28 |
||
29 |
val (smart_quantifier, setup_smart_quantifier) = |
|
30 |
Attrib.config_bool "quickcheck_smart_quantifier" (K true) |
|
31 |
||
42306 | 32 |
val (fast, setup_fast) = |
33 |
Attrib.config_bool "quickcheck_fast" (K true) |
|
34 |
||
42304 | 35 |
val (full_support, setup_full_support) = |
36 |
Attrib.config_bool "quickcheck_full_support" (K true) |
|
37 |
||
41903
39fd77f0ae59
fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample
bulwahn
parents:
41902
diff
changeset
|
38 |
val (quickcheck_pretty, setup_quickcheck_pretty) = |
39fd77f0ae59
fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample
bulwahn
parents:
41902
diff
changeset
|
39 |
Attrib.config_bool "quickcheck_pretty" (K true) |
39fd77f0ae59
fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample
bulwahn
parents:
41902
diff
changeset
|
40 |
|
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
41 |
(** general term functions **) |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
42 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
43 |
fun mk_measure f = |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
44 |
let |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
45 |
val Type ("fun", [T, @{typ nat}]) = fastype_of f |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
46 |
in |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
47 |
Const (@{const_name Wellfounded.measure}, |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
48 |
(T --> @{typ nat}) --> HOLogic.mk_prodT (T, T) --> @{typ bool}) |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
49 |
$ f |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
50 |
end |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
51 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
52 |
fun mk_sumcases rT f (Type (@{type_name Sum_Type.sum}, [TL, TR])) = |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
53 |
let |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
54 |
val lt = mk_sumcases rT f TL |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
55 |
val rt = mk_sumcases rT f TR |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
56 |
in |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
57 |
SumTree.mk_sumcase TL TR rT lt rt |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
58 |
end |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
59 |
| mk_sumcases _ f T = f T |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
60 |
|
40901
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
61 |
fun mk_undefined T = Const(@{const_name undefined}, T) |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
62 |
|
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
63 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
64 |
(** abstract syntax **) |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
65 |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
66 |
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"}); |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
67 |
|
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
68 |
val size = @{term "i :: code_numeral"} |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
69 |
val size_pred = @{term "(i :: code_numeral) - 1"} |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
70 |
val size_ge_zero = @{term "(i :: code_numeral) > 0"} |
42304 | 71 |
|
72 |
fun test_function T = Free ("f", T --> @{typ "term list option"}) |
|
73 |
fun full_test_function T = Free ("f", termifyT T --> @{typ "term list option"}) |
|
42306 | 74 |
fun fast_test_function T = Free ("f", T --> @{typ "unit"}) |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
75 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
76 |
fun mk_none_continuation (x, y) = |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
77 |
let |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
78 |
val (T as Type(@{type_name "option"}, [T'])) = fastype_of x |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
79 |
in |
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
80 |
Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
81 |
end |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
82 |
|
42306 | 83 |
fun mk_unit_let (x, y) = |
84 |
Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ (absdummy (@{typ unit}, y)) |
|
85 |
||
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
86 |
(** datatypes **) |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
87 |
|
41918 | 88 |
(* constructing exhaustive generator instances on datatypes *) |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
89 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
90 |
exception FUNCTION_TYPE; |
42306 | 91 |
|
92 |
exception Counterexample of term list |
|
93 |
||
41918 | 94 |
val exhaustiveN = "exhaustive"; |
42304 | 95 |
val full_exhaustiveN = "full_exhaustive"; |
42306 | 96 |
val fast_exhaustiveN = "fast_exhaustive"; |
97 |
||
98 |
fun fast_exhaustiveT T = (T --> @{typ unit}) |
|
99 |
--> @{typ code_numeral} --> @{typ unit} |
|
100 |
||
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
101 |
|
42304 | 102 |
fun exhaustiveT T = (T --> @{typ "Code_Evaluation.term list option"}) |
103 |
--> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"} |
|
104 |
||
105 |
fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"}) |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
106 |
--> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"} |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40913
diff
changeset
|
107 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40913
diff
changeset
|
108 |
fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"}) |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40913
diff
changeset
|
109 |
--> @{typ "Code_Evaluation.term list option"} |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40913
diff
changeset
|
110 |
|
42306 | 111 |
|
112 |
fun mk_fast_equations descr vs tycos fast_exhaustives (Ts, Us) = |
|
113 |
let |
|
114 |
fun mk_call T = |
|
115 |
let |
|
116 |
val fast_exhaustive = |
|
117 |
Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"}, fast_exhaustiveT T) |
|
118 |
in |
|
119 |
(T, fn t => fast_exhaustive $ absdummy (T, t) $ size_pred) |
|
120 |
end |
|
121 |
fun mk_aux_call fTs (k, _) (tyco, Ts) = |
|
122 |
let |
|
123 |
val T = Type (tyco, Ts) |
|
124 |
val _ = if not (null fTs) then raise FUNCTION_TYPE else () |
|
125 |
in |
|
126 |
(T, fn t => nth fast_exhaustives k $ absdummy (T, t) $ size_pred) |
|
127 |
end |
|
128 |
fun mk_consexpr simpleT (c, xs) = |
|
129 |
let |
|
130 |
val (Ts, fns) = split_list xs |
|
131 |
val constr = Const (c, Ts ---> simpleT) |
|
132 |
val bounds = map Bound (((length xs) - 1) downto 0) |
|
133 |
val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0) |
|
134 |
val start_term = fast_test_function simpleT $ list_comb (constr, bounds) |
|
135 |
in fold_rev (fn f => fn t => f t) fns start_term end |
|
136 |
fun mk_rhs exprs = |
|
137 |
@{term "If :: bool => unit => unit => unit"} |
|
138 |
$ size_ge_zero $ (foldr1 mk_unit_let exprs) $ @{term "()"} |
|
139 |
val rhss = |
|
140 |
Datatype_Aux.interpret_construction descr vs |
|
141 |
{ atyp = mk_call, dtyp = mk_aux_call } |
|
142 |
|> (map o apfst) Type |
|
143 |
|> map (fn (T, cs) => map (mk_consexpr T) cs) |
|
144 |
|> map mk_rhs |
|
145 |
val lhss = map2 (fn t => fn T => t $ fast_test_function T $ size) fast_exhaustives (Ts @ Us) |
|
146 |
val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) |
|
147 |
in |
|
148 |
eqs |
|
149 |
end |
|
150 |
||
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41935
diff
changeset
|
151 |
fun mk_equations descr vs tycos exhaustives (Ts, Us) = |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
152 |
let |
41918 | 153 |
fun mk_call T = |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
154 |
let |
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41935
diff
changeset
|
155 |
val exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T) |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
156 |
in |
42304 | 157 |
(T, fn t => exhaustive $ absdummy (T, t) $ size_pred) |
158 |
end |
|
159 |
fun mk_aux_call fTs (k, _) (tyco, Ts) = |
|
160 |
let |
|
161 |
val T = Type (tyco, Ts) |
|
162 |
val _ = if not (null fTs) then raise FUNCTION_TYPE else () |
|
163 |
in |
|
164 |
(T, fn t => nth exhaustives k $ absdummy (T, t) $ size_pred) |
|
165 |
end |
|
166 |
fun mk_consexpr simpleT (c, xs) = |
|
167 |
let |
|
168 |
val (Ts, fns) = split_list xs |
|
169 |
val constr = Const (c, Ts ---> simpleT) |
|
170 |
val bounds = map Bound (((length xs) - 1) downto 0) |
|
171 |
val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0) |
|
172 |
val start_term = test_function simpleT $ list_comb (constr, bounds) |
|
173 |
in fold_rev (fn f => fn t => f t) fns start_term end |
|
174 |
fun mk_rhs exprs = |
|
175 |
@{term "If :: bool => term list option => term list option => term list option"} |
|
176 |
$ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"} |
|
177 |
val rhss = |
|
178 |
Datatype_Aux.interpret_construction descr vs |
|
179 |
{ atyp = mk_call, dtyp = mk_aux_call } |
|
180 |
|> (map o apfst) Type |
|
181 |
|> map (fn (T, cs) => map (mk_consexpr T) cs) |
|
182 |
|> map mk_rhs |
|
183 |
val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives (Ts @ Us) |
|
184 |
val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) |
|
185 |
in |
|
186 |
eqs |
|
187 |
end |
|
188 |
||
189 |
fun mk_full_equations descr vs tycos full_exhaustives (Ts, Us) = |
|
190 |
let |
|
191 |
fun mk_call T = |
|
192 |
let |
|
193 |
val full_exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.full_exhaustive"}, full_exhaustiveT T) |
|
194 |
in |
|
195 |
(T, (fn t => full_exhaustive $ |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
196 |
(HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"}) |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
197 |
$ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred)) |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
198 |
end |
41918 | 199 |
fun mk_aux_call fTs (k, _) (tyco, Ts) = |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
200 |
let |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
201 |
val T = Type (tyco, Ts) |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
202 |
val _ = if not (null fTs) then raise FUNCTION_TYPE else () |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
203 |
in |
42304 | 204 |
(T, (fn t => nth full_exhaustives k $ |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
205 |
(HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"}) |
41918 | 206 |
$ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred)) |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
207 |
end |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
208 |
fun mk_consexpr simpleT (c, xs) = |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
209 |
let |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
210 |
val (Ts, fns) = split_list xs |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
211 |
val constr = Const (c, Ts ---> simpleT) |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
212 |
val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0) |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
213 |
val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0) |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
214 |
val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT) |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
215 |
val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT) |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
216 |
val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"})) |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
217 |
bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT)) |
42304 | 218 |
val start_term = full_test_function simpleT $ |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
219 |
(HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"} |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
220 |
$ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term)) |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
221 |
in fold_rev (fn f => fn t => f t) fns start_term end |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
222 |
fun mk_rhs exprs = |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
223 |
@{term "If :: bool => term list option => term list option => term list option"} |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
224 |
$ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"} |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
225 |
val rhss = |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
226 |
Datatype_Aux.interpret_construction descr vs |
41918 | 227 |
{ atyp = mk_call, dtyp = mk_aux_call } |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
228 |
|> (map o apfst) Type |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
229 |
|> map (fn (T, cs) => map (mk_consexpr T) cs) |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
230 |
|> map mk_rhs |
42304 | 231 |
val lhss = map2 (fn t => fn T => t $ full_test_function T $ size) full_exhaustives (Ts @ Us); |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
232 |
val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
233 |
in |
40901
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
234 |
eqs |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
235 |
end |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
236 |
|
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
237 |
(* foundational definition with the function package *) |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
238 |
|
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
239 |
val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto} |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
240 |
|
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
241 |
fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"}, |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
242 |
Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"})) |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
243 |
|
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
244 |
fun mk_termination_measure T = |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
245 |
let |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
246 |
val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T)) |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
247 |
in |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
248 |
mk_measure (mk_sumcases @{typ nat} mk_single_measure T') |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
249 |
end |
40901
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
250 |
|
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
251 |
fun termination_tac ctxt = |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
252 |
Function_Relation.relation_tac ctxt mk_termination_measure 1 |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
253 |
THEN rtac @{thm wf_measure} 1 |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
254 |
THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
255 |
(HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv}, |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
256 |
@{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1)) |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
257 |
|
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
258 |
(* creating the instances *) |
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
259 |
|
41918 | 260 |
fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
261 |
let |
42230
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
262 |
val _ = Datatype_Aux.message config "Creating exhaustive generators..."; |
42304 | 263 |
val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames) |
264 |
val full_exhaustivesN = map (prefix (full_exhaustiveN ^ "_")) (names @ auxnames) |
|
40901
8fdfa9c4e7ed
smallvalue_generator are defined quick via oracle or sound via function package
bulwahn
parents:
40899
diff
changeset
|
265 |
in |
40641
5615cc557120
moving the error handling to the right scope in smallvalue_generators
bulwahn
parents:
40640
diff
changeset
|
266 |
thy |
41918 | 267 |
|> Class.instantiation (tycos, vs, @{sort exhaustive}) |
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
268 |
|> Quickcheck_Common.define_functions |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
269 |
(fn exhaustives => mk_equations descr vs tycos exhaustives (Ts, Us), SOME termination_tac) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
270 |
prfx ["f", "i"] exhaustivesN (map exhaustiveT (Ts @ Us)) |
42304 | 271 |
|> Quickcheck_Common.define_functions |
272 |
(fn full_exhaustives => mk_full_equations descr vs tycos full_exhaustives (Ts, Us), |
|
273 |
SOME termination_tac) |
|
274 |
prfx ["f", "i"] full_exhaustivesN (map full_exhaustiveT (Ts @ Us)) |
|
40641
5615cc557120
moving the error handling to the right scope in smallvalue_generators
bulwahn
parents:
40640
diff
changeset
|
275 |
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
5615cc557120
moving the error handling to the right scope in smallvalue_generators
bulwahn
parents:
40640
diff
changeset
|
276 |
end handle FUNCTION_TYPE => |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
277 |
(Datatype_Aux.message config |
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41935
diff
changeset
|
278 |
"Creation of exhaustive generators failed because the datatype contains a function type"; |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40420
diff
changeset
|
279 |
thy) |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
280 |
|
42306 | 281 |
fun instantiate_fast_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = |
282 |
let |
|
283 |
val _ = Datatype_Aux.message config "Creating fast exhaustive generators..."; |
|
284 |
val fast_exhaustivesN = map (prefix (fast_exhaustiveN ^ "_")) (names @ auxnames) |
|
285 |
in |
|
286 |
thy |
|
287 |
|> Class.instantiation (tycos, vs, @{sort fast_exhaustive}) |
|
288 |
|> Quickcheck_Common.define_functions |
|
289 |
(fn exhaustives => mk_fast_equations descr vs tycos exhaustives (Ts, Us), SOME termination_tac) |
|
290 |
prfx ["f", "i"] fast_exhaustivesN (map fast_exhaustiveT (Ts @ Us)) |
|
291 |
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
|
292 |
end handle FUNCTION_TYPE => |
|
293 |
(Datatype_Aux.message config |
|
294 |
"Creation of exhaustive generators failed because the datatype contains a function type"; |
|
295 |
thy) |
|
296 |
||
42230
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
297 |
(* constructing bounded_forall instances on datatypes *) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
298 |
|
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
299 |
val bounded_forallN = "bounded_forall"; |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
300 |
|
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
301 |
fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool} |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
302 |
|
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
303 |
fun mk_bounded_forall_equations descr vs tycos bounded_foralls (Ts, Us) = |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
304 |
let |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
305 |
fun mk_call T = |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
306 |
let |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
307 |
val bounded_forall = |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
308 |
Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
309 |
bounded_forallT T) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
310 |
in |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
311 |
(T, (fn t => bounded_forall $ absdummy (T, t) $ size_pred)) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
312 |
end |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
313 |
fun mk_aux_call fTs (k, _) (tyco, Ts) = |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
314 |
let |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
315 |
val T = Type (tyco, Ts) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
316 |
val _ = if not (null fTs) then raise FUNCTION_TYPE else () |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
317 |
in |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
318 |
(T, (fn t => nth bounded_foralls k $ absdummy (T, t) $ size_pred)) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
319 |
end |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
320 |
fun mk_consexpr simpleT (c, xs) = |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
321 |
let |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
322 |
val (Ts, fns) = split_list xs |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
323 |
val constr = Const (c, Ts ---> simpleT) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
324 |
val bounds = map Bound (((length xs) - 1) downto 0) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
325 |
val start_term = Free ("P", simpleT --> @{typ bool}) $ list_comb (constr, bounds) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
326 |
in fold_rev (fn f => fn t => f t) fns start_term end |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
327 |
fun mk_rhs exprs = |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
328 |
@{term "If :: bool => bool => bool => bool"} $ size_ge_zero $ |
42273 | 329 |
(foldr1 HOLogic.mk_conj exprs) $ @{term "True"} |
42230
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
330 |
val rhss = |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
331 |
Datatype_Aux.interpret_construction descr vs |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
332 |
{ atyp = mk_call, dtyp = mk_aux_call } |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
333 |
|> (map o apfst) Type |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
334 |
|> map (fn (T, cs) => map (mk_consexpr T) cs) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
335 |
|> map mk_rhs |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
336 |
val lhss = |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
337 |
map2 (fn t => fn T => t $ Free ("P", T --> @{typ bool}) $ size) bounded_foralls (Ts @ Us) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
338 |
val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
339 |
in |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
340 |
eqs |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
341 |
end |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
342 |
|
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
343 |
(* creating the bounded_forall instances *) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
344 |
|
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
345 |
fun instantiate_bounded_forall_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
346 |
let |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
347 |
val _ = Datatype_Aux.message config "Creating bounded universal quantifiers..."; |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
348 |
val bounded_forallsN = map (prefix (bounded_forallN ^ "_")) (names @ auxnames); |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
349 |
in |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
350 |
thy |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
351 |
|> Class.instantiation (tycos, vs, @{sort bounded_forall}) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
352 |
|> Quickcheck_Common.define_functions |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
353 |
(fn bounded_foralls => |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
354 |
mk_bounded_forall_equations descr vs tycos bounded_foralls (Ts, Us), NONE) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
355 |
prfx ["P", "i"] bounded_forallsN (map bounded_forallT (Ts @ Us)) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
356 |
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
357 |
end handle FUNCTION_TYPE => |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
358 |
(Datatype_Aux.message config |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
359 |
"Creation of bounded universal quantifiers failed because the datatype contains a function type"; |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
360 |
thy) |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
361 |
|
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
362 |
(** building and compiling generator expressions **) |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
363 |
|
42306 | 364 |
fun mk_fast_generator_expr ctxt (t, eval_terms) = |
365 |
let |
|
366 |
val thy = ProofContext.theory_of ctxt |
|
367 |
val ctxt' = Variable.auto_fixes t ctxt |
|
368 |
val names = Term.add_free_names t [] |
|
369 |
val frees = map Free (Term.add_frees t []) |
|
370 |
val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt' |
|
371 |
val depth = Free (depth_name, @{typ code_numeral}) |
|
372 |
val return = @{term "throw_Counterexample :: term list => unit"} $ |
|
373 |
(HOLogic.mk_list @{typ "term"} |
|
374 |
(map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms))) |
|
375 |
fun mk_exhaustive_closure (free as Free (_, T)) t = |
|
376 |
Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"}, fast_exhaustiveT T) |
|
377 |
$ lambda free t $ depth |
|
378 |
val none_t = @{term "()"} |
|
379 |
fun mk_safe_if (cond, then_t, else_t) = |
|
380 |
@{term "If :: bool => unit => unit => unit"} $ cond $ then_t $ else_t |
|
381 |
fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) |
|
382 |
fun mk_naive_test_term t = |
|
383 |
fold_rev mk_exhaustive_closure frees (mk_safe_if (t, none_t, return)) |
|
384 |
fun mk_smart_test_term' concl bound_vars assms = |
|
385 |
let |
|
386 |
fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t []) |
|
387 |
val (vars, check) = |
|
388 |
case assms of [] => (vars_of concl, (concl, none_t, return)) |
|
389 |
| assm :: assms => (vars_of assm, (assm, |
|
390 |
mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t)) |
|
391 |
in |
|
392 |
fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check) |
|
393 |
end |
|
394 |
fun mk_smart_test_term t = |
|
395 |
let |
|
396 |
val (assms, concl) = Quickcheck_Common.strip_imp t |
|
397 |
in |
|
398 |
mk_smart_test_term' concl [] assms |
|
399 |
end |
|
400 |
val mk_test_term = |
|
401 |
if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term |
|
402 |
in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end |
|
403 |
||
42028
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
404 |
fun mk_generator_expr ctxt (t, eval_terms) = |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
405 |
let |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
406 |
val thy = ProofContext.theory_of ctxt |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
407 |
val ctxt' = Variable.auto_fixes t ctxt |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
408 |
val names = Term.add_free_names t [] |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
409 |
val frees = map Free (Term.add_frees t []) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
410 |
val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt' |
42304 | 411 |
val depth = Free (depth_name, @{typ code_numeral}) |
412 |
val return = @{term "Some :: term list => term list option"} $ |
|
413 |
(HOLogic.mk_list @{typ "term"} |
|
414 |
(map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms))) |
|
415 |
fun mk_exhaustive_closure (free as Free (_, T)) t = |
|
416 |
Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T) |
|
417 |
$ lambda free t $ depth |
|
418 |
val none_t = @{term "None :: term list option"} |
|
419 |
fun mk_safe_if (cond, then_t, else_t) = |
|
420 |
@{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $ |
|
421 |
(@{term "If :: bool => term list option => term list option => term list option"} |
|
422 |
$ cond $ then_t $ else_t) $ none_t; |
|
423 |
fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) |
|
424 |
fun mk_naive_test_term t = |
|
425 |
fold_rev mk_exhaustive_closure frees (mk_safe_if (t, none_t, return)) |
|
426 |
fun mk_smart_test_term' concl bound_vars assms = |
|
427 |
let |
|
428 |
fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t []) |
|
429 |
val (vars, check) = |
|
430 |
case assms of [] => (vars_of concl, (concl, none_t, return)) |
|
431 |
| assm :: assms => (vars_of assm, (assm, |
|
432 |
mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t)) |
|
433 |
in |
|
434 |
fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check) |
|
435 |
end |
|
436 |
fun mk_smart_test_term t = |
|
437 |
let |
|
438 |
val (assms, concl) = Quickcheck_Common.strip_imp t |
|
439 |
in |
|
440 |
mk_smart_test_term' concl [] assms |
|
441 |
end |
|
442 |
val mk_test_term = |
|
443 |
if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term |
|
444 |
in lambda depth (mk_test_term t) end |
|
445 |
||
446 |
fun mk_full_generator_expr ctxt (t, eval_terms) = |
|
447 |
let |
|
448 |
val thy = ProofContext.theory_of ctxt |
|
449 |
val ctxt' = Variable.auto_fixes t ctxt |
|
450 |
val names = Term.add_free_names t [] |
|
451 |
val frees = map Free (Term.add_frees t []) |
|
452 |
val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt' |
|
42028
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
453 |
val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") names) ctxt'' |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
454 |
val depth = Free (depth_name, @{typ code_numeral}) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
455 |
val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
456 |
val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
457 |
val appendC = @{term "List.append :: term list => term list => term list"} |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
458 |
val return = @{term "Some :: term list => term list option"} $ (appendC $ terms $ |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
459 |
(HOLogic.mk_list @{typ "term"} (map (fn t => HOLogic.mk_term_of (fastype_of t) t) eval_terms))) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
460 |
fun mk_exhaustive_closure (free as Free (_, T), term_var) t = |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
461 |
if Sign.of_sort thy (T, @{sort enum}) then |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
462 |
Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
463 |
$ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
464 |
$ lambda free (lambda term_var t)) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
465 |
else |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
466 |
Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
467 |
$ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
468 |
$ lambda free (lambda term_var t)) $ depth |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
469 |
val none_t = @{term "None :: term list option"} |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
470 |
fun mk_safe_if (cond, then_t, else_t) = |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
471 |
@{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $ |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
472 |
(@{term "If :: bool => term list option => term list option => term list option"} |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
473 |
$ cond $ then_t $ else_t) $ none_t; |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
474 |
fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
475 |
fun mk_naive_test_term t = |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
476 |
fold_rev mk_exhaustive_closure (frees ~~ term_vars) (mk_safe_if (t, none_t, return)) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
477 |
fun mk_smart_test_term' concl bound_vars assms = |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
478 |
let |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
479 |
fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t []) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
480 |
val (vars, check) = |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
481 |
case assms of [] => (vars_of concl, (concl, none_t, return)) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
482 |
| assm :: assms => (vars_of assm, (assm, |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
483 |
mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t)) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
484 |
in |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
485 |
fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
486 |
end |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
487 |
fun mk_smart_test_term t = |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
488 |
let |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
489 |
val (assms, concl) = Quickcheck_Common.strip_imp t |
42028
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
490 |
in |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
491 |
mk_smart_test_term' concl [] assms |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
492 |
end |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
493 |
val mk_test_term = |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
494 |
if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
495 |
in lambda depth (mk_test_term t) end |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
496 |
|
42304 | 497 |
fun mk_parametric_generator_expr mk_generator_expr = |
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
498 |
Quickcheck_Common.gen_mk_parametric_generator_expr |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
499 |
((mk_generator_expr, absdummy (@{typ "code_numeral"}, @{term "None :: term list option"})), |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
500 |
@{typ "code_numeral => term list option"}) |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
501 |
|
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
502 |
fun mk_validator_expr ctxt t = |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
503 |
let |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
504 |
fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool} |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
505 |
val thy = ProofContext.theory_of ctxt |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
506 |
val ctxt' = Variable.auto_fixes t ctxt |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
507 |
val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt' |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
508 |
val depth = Free (depth_name, @{typ code_numeral}) |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
509 |
fun mk_bounded_forall (s, T) t = |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
510 |
Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T) |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
511 |
$ lambda (Free (s, T)) t $ depth |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
512 |
fun mk_implies (cond, then_t) = |
42273 | 513 |
@{term "If :: bool => bool => bool => bool"} $ cond $ then_t $ @{term True} |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
514 |
fun mk_naive_test_term t = fold_rev mk_bounded_forall (Term.add_frees t []) t |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
515 |
fun mk_smart_test_term' concl bound_frees assms = |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
516 |
let |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
517 |
fun vars_of t = subtract (op =) bound_frees (Term.add_frees t []) |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
518 |
val (vars, check) = |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
519 |
case assms of [] => (vars_of concl, concl) |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
520 |
| assm :: assms => (vars_of assm, mk_implies (assm, |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
521 |
mk_smart_test_term' concl (union (op =) (vars_of assm) bound_frees) assms)) |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
522 |
in |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
523 |
fold_rev mk_bounded_forall vars check |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
524 |
end |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
525 |
fun mk_smart_test_term t = |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
526 |
let |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
527 |
val (assms, concl) = Quickcheck_Common.strip_imp t |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
528 |
in |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
529 |
mk_smart_test_term' concl [] assms |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
530 |
end |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
531 |
val mk_test_term = |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
532 |
if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
533 |
in lambda depth (mk_test_term t) end |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
534 |
|
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
535 |
|
42028
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
536 |
(** generator compiliation **) |
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
537 |
|
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41178
diff
changeset
|
538 |
structure Counterexample = Proof_Data |
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41178
diff
changeset
|
539 |
( |
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
540 |
type T = unit -> int -> int -> term list option |
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41178
diff
changeset
|
541 |
(* FIXME avoid user error with non-user text *) |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
542 |
fun init _ () = error "Counterexample" |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
543 |
); |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
544 |
val put_counterexample = Counterexample.put; |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
545 |
|
41861
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
546 |
structure Counterexample_Batch = Proof_Data |
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
547 |
( |
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
548 |
type T = unit -> (int -> term list option) list |
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
549 |
(* FIXME avoid user error with non-user text *) |
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
550 |
fun init _ () = error "Counterexample" |
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
551 |
); |
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
552 |
val put_counterexample_batch = Counterexample_Batch.put; |
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
553 |
|
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
554 |
structure Validator_Batch = Proof_Data |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
555 |
( |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
556 |
type T = unit -> (int -> bool) list |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
557 |
(* FIXME avoid user error with non-user text *) |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
558 |
fun init _ () = error "Counterexample" |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
559 |
); |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
560 |
val put_validator_batch = Validator_Batch.put; |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
561 |
|
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
562 |
|
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
563 |
val target = "Quickcheck"; |
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
564 |
|
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
565 |
fun compile_generator_expr ctxt ts = |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
566 |
let |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
567 |
val thy = ProofContext.theory_of ctxt |
42306 | 568 |
val mk_generator_expr = |
569 |
if Config.get ctxt fast then mk_fast_generator_expr |
|
570 |
else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr |
|
42304 | 571 |
val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts; |
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
572 |
val compile = Code_Runtime.dynamic_value_strict |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
573 |
(Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample") |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
574 |
thy (SOME target) (fn proc => fn g => |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
575 |
fn card => fn size => g card size |> (Option.map o map) proc) t' [] |
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
576 |
in |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
577 |
fn [card, size] => rpair NONE (compile card size |> |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
578 |
(if Config.get ctxt quickcheck_pretty then |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
579 |
Option.map (map Quickcheck_Common.post_process_term) else I)) |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
580 |
end; |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42028
diff
changeset
|
581 |
|
41861
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
582 |
fun compile_generator_exprs ctxt ts = |
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
583 |
let |
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
584 |
val thy = ProofContext.theory_of ctxt |
42028
bd6515e113b2
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
bulwahn
parents:
42027
diff
changeset
|
585 |
val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts; |
41861
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
586 |
val compiles = Code_Runtime.dynamic_value_strict |
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
587 |
(Counterexample_Batch.get, put_counterexample_batch, |
41918 | 588 |
"Exhaustive_Generators.put_counterexample_batch") |
41861
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
589 |
thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc)) |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
590 |
(HOLogic.mk_list @{typ "code_numeral => term list option"} ts') [] |
41861
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
591 |
in |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41928
diff
changeset
|
592 |
map (fn compile => fn size => compile size |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41928
diff
changeset
|
593 |
|> Option.map (map Quickcheck_Common.post_process_term)) compiles |
41861
77d87dc50e5a
adding a function to compile a batch of terms for quickcheck with one code generation invocation
bulwahn
parents:
41472
diff
changeset
|
594 |
end; |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
595 |
|
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
596 |
fun compile_validator_exprs ctxt ts = |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
597 |
let |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
598 |
val thy = ProofContext.theory_of ctxt |
42273 | 599 |
val ts' = map (mk_validator_expr ctxt) ts |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
600 |
in |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
601 |
Code_Runtime.dynamic_value_strict |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
602 |
(Validator_Batch.get, put_validator_batch, "Exhaustive_Generators.put_validator_batch") |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
603 |
thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') [] |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
604 |
end; |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
605 |
|
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
606 |
(** setup **) |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
607 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
608 |
val setup = |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
609 |
Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
610 |
(((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype)) |
42230
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
611 |
#> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
594480d25aaa
deriving bounded_forall instances in quickcheck_exhaustive
bulwahn
parents:
42229
diff
changeset
|
612 |
(((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype)) |
42306 | 613 |
#> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
614 |
(((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype)) |
|
40907 | 615 |
#> setup_smart_quantifier |
42304 | 616 |
#> setup_full_support |
42306 | 617 |
#> setup_fast |
41903
39fd77f0ae59
fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample
bulwahn
parents:
41902
diff
changeset
|
618 |
#> setup_quickcheck_pretty |
41900 | 619 |
#> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr)) |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
620 |
#> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs)) |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42176
diff
changeset
|
621 |
#> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)); |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
622 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
623 |
end; |