4 Exhaustive generators for various types. |
4 Exhaustive generators for various types. |
5 *) |
5 *) |
6 |
6 |
7 signature EXHAUSTIVE_GENERATORS = |
7 signature EXHAUSTIVE_GENERATORS = |
8 sig |
8 sig |
9 val exhaustive_plugin: string |
|
10 val bounded_forall_plugin: string |
|
11 val full_exhaustive_plugin: string |
|
12 |
|
13 val compile_generator_expr: |
9 val compile_generator_expr: |
14 Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option |
10 Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option |
15 val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list |
11 val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list |
16 val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list |
12 val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list |
17 val put_counterexample: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) |
13 val put_counterexample: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) |
36 |
32 |
37 structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS = |
33 structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS = |
38 struct |
34 struct |
39 |
35 |
40 (* basics *) |
36 (* basics *) |
41 |
|
42 val exhaustive_plugin = "quickcheck_exhaustive" |
|
43 val bounded_forall_plugin = "quickcheck_bounded_forall" |
|
44 val full_exhaustive_plugin = "quickcheck_full_exhaustive" |
|
45 |
|
46 |
37 |
47 (** dynamic options **) |
38 (** dynamic options **) |
48 |
39 |
49 val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true) |
40 val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true) |
50 val optimise_equality = Attrib.setup_config_bool @{binding quickcheck_optimise_equality} (K true) |
41 val optimise_equality = Attrib.setup_config_bool @{binding quickcheck_optimise_equality} (K true) |
542 Quickcheck_Common.generator_test_goal_terms ("exhaustive", (size_matters_for, compile_generator_expr)); |
533 Quickcheck_Common.generator_test_goal_terms ("exhaustive", (size_matters_for, compile_generator_expr)); |
543 |
534 |
544 (* setup *) |
535 (* setup *) |
545 |
536 |
546 val setup_exhaustive_datatype_interpretation = |
537 val setup_exhaustive_datatype_interpretation = |
547 Quickcheck_Common.datatype_interpretation exhaustive_plugin |
538 Quickcheck_Common.datatype_interpretation @{plugin quickcheck_exhaustive} |
548 (@{sort exhaustive}, instantiate_exhaustive_datatype) |
539 (@{sort exhaustive}, instantiate_exhaustive_datatype) |
549 |
540 |
550 val setup_bounded_forall_datatype_interpretation = |
541 val setup_bounded_forall_datatype_interpretation = |
551 BNF_LFP_Compat.interpretation bounded_forall_plugin Quickcheck_Common.compat_prefs |
542 BNF_LFP_Compat.interpretation @{plugin quickcheck_bounded_forall} Quickcheck_Common.compat_prefs |
552 (Quickcheck_Common.ensure_sort |
543 (Quickcheck_Common.ensure_sort |
553 (((@{sort type}, @{sort type}), @{sort bounded_forall}), |
544 (((@{sort type}, @{sort type}), @{sort bounded_forall}), |
554 (fn thy => BNF_LFP_Compat.the_descr thy Quickcheck_Common.compat_prefs, |
545 (fn thy => BNF_LFP_Compat.the_descr thy Quickcheck_Common.compat_prefs, |
555 instantiate_bounded_forall_datatype))) |
546 instantiate_bounded_forall_datatype))) |
556 |
547 |
557 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true); |
548 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true); |
558 |
549 |
559 val setup = |
550 val setup = |
560 Quickcheck_Common.datatype_interpretation full_exhaustive_plugin |
551 Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive} |
561 (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype) |
552 (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype) |
562 #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals))) |
553 #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals))) |
563 #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs)) |
554 #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs)) |
564 #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)); |
555 #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)); |
565 |
556 |