26 |
26 |
27 (* basics *) |
27 (* basics *) |
28 |
28 |
29 (** dynamic options **) |
29 (** dynamic options **) |
30 |
30 |
31 val (smart_quantifier, setup_smart_quantifier) = |
31 val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true) |
32 Attrib.config_bool "quickcheck_smart_quantifier" (K true) |
32 val fast = Attrib.setup_config_bool @{binding quickcheck_fast} (K false) |
33 |
33 val bounded_forall = Attrib.setup_config_bool @{binding quickcheck_bounded_forall} (K false) |
34 val (fast, setup_fast) = |
34 val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true) |
35 Attrib.config_bool "quickcheck_fast" (K false) |
35 val quickcheck_pretty = Attrib.setup_config_bool @{binding quickcheck_pretty} (K true) |
36 |
|
37 val (bounded_forall, setup_bounded_forall) = |
|
38 Attrib.config_bool "quickcheck_bounded_forall" (K false) |
|
39 |
|
40 val (full_support, setup_full_support) = |
|
41 Attrib.config_bool "quickcheck_full_support" (K true) |
|
42 |
|
43 val (quickcheck_pretty, setup_quickcheck_pretty) = |
|
44 Attrib.config_bool "quickcheck_pretty" (K true) |
|
45 |
36 |
46 (** general term functions **) |
37 (** general term functions **) |
47 |
38 |
48 fun mk_measure f = |
39 fun mk_measure f = |
49 let |
40 let |
506 (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype)) |
497 (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype)) |
507 #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
498 #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
508 (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype)) |
499 (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype)) |
509 #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
500 #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
510 (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*) |
501 (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*) |
511 #> setup_smart_quantifier |
|
512 #> setup_full_support |
|
513 #> setup_fast |
|
514 #> setup_bounded_forall |
|
515 #> setup_quickcheck_pretty |
|
516 #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr)) |
502 #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr)) |
517 #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs)) |
503 #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs)) |
518 #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)); |
504 #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)); |
519 |
505 |
520 end; |
506 end; |