| author | krauss |
| Wed, 08 Jun 2011 00:01:20 +0200 | |
| changeset 43252 | b142ae3e9478 |
| parent 42427 | 5611f178a747 |
| child 43875 | 485d2ad43528 |
| permissions | -rw-r--r-- |
| 33084 | 1 |
|
2 |
header {* Install quickcheck of SML code generator *}
|
|
3 |
||
4 |
theory SML_Quickcheck |
|
5 |
imports Main |
|
6 |
begin |
|
7 |
||
8 |
setup {*
|
|
|
37390
8781d80026fc
moved inductive_codegen to place where product type is available; tuned structure name
haftmann
parents:
33771
diff
changeset
|
9 |
Inductive_Codegen.quickcheck_setup #> |
| 40919 | 10 |
Context.theory_map (Quickcheck.add_generator ("SML",
|
|
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:
42029
diff
changeset
|
11 |
fn ctxt => fn [(t, eval_terms)] => |
| 40919 | 12 |
let |
|
42161
d1b39536e1fb
adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape
bulwahn
parents:
42159
diff
changeset
|
13 |
val prop = list_abs_free (Term.add_frees t [], t) |
|
42427
5611f178a747
eliminated global references / critical sections via context data;
wenzelm
parents:
42161
diff
changeset
|
14 |
val test_fun = Codegen.test_term ctxt prop |
| 40919 | 15 |
val iterations = Config.get ctxt Quickcheck.iterations |
16 |
fun iterate size 0 = NONE |
|
17 |
| iterate size j = |
|
|
42427
5611f178a747
eliminated global references / critical sections via context data;
wenzelm
parents:
42161
diff
changeset
|
18 |
let |
|
5611f178a747
eliminated global references / critical sections via context data;
wenzelm
parents:
42161
diff
changeset
|
19 |
val result = test_fun size handle Match => |
|
5611f178a747
eliminated global references / critical sections via context data;
wenzelm
parents:
42161
diff
changeset
|
20 |
(if Config.get ctxt Quickcheck.quiet then () |
|
5611f178a747
eliminated global references / critical sections via context data;
wenzelm
parents:
42161
diff
changeset
|
21 |
else warning "Exception Match raised during quickcheck"; NONE) |
|
5611f178a747
eliminated global references / critical sections via context data;
wenzelm
parents:
42161
diff
changeset
|
22 |
in |
|
5611f178a747
eliminated global references / critical sections via context data;
wenzelm
parents:
42161
diff
changeset
|
23 |
case result of NONE => iterate size (j - 1) | SOME q => SOME q |
|
5611f178a747
eliminated global references / critical sections via context data;
wenzelm
parents:
42161
diff
changeset
|
24 |
end |
|
42161
d1b39536e1fb
adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape
bulwahn
parents:
42159
diff
changeset
|
25 |
in fn [_, size] => (iterate size iterations, NONE) end)) |
| 33084 | 26 |
*} |
27 |
||
28 |
end |