author | bulwahn |
Fri, 11 Mar 2011 15:21:13 +0100 | |
changeset 41919 | e180c2a9873b |
parent 40919 | cdb34f393a7e |
child 42029 | da92153d6dff |
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", |
11 |
fn ctxt => fn t => |
|
12 |
let |
|
13 |
val test_fun = Codegen.test_term ctxt t |
|
14 |
val iterations = Config.get ctxt Quickcheck.iterations |
|
15 |
fun iterate size 0 = NONE |
|
16 |
| iterate size j = |
|
17 |
let |
|
18 |
val result = test_fun size handle Match => |
|
19 |
(if Config.get ctxt Quickcheck.quiet then () |
|
20 |
else warning "Exception Match raised during quickcheck"; NONE) |
|
21 |
in |
|
22 |
case result of NONE => iterate size (j - 1) | SOME q => SOME q |
|
23 |
end |
|
24 |
in fn size => (iterate size iterations, NONE) end)) |
|
33084 | 25 |
*} |
26 |
||
27 |
end |