498 val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive", compile_generator_expr); |
498 val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive", compile_generator_expr); |
499 |
499 |
500 (* setup *) |
500 (* setup *) |
501 |
501 |
502 val setup_exhaustive_datatype_interpretation = |
502 val setup_exhaustive_datatype_interpretation = |
503 Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
503 Quickcheck_Common.datatype_interpretation (@{sort exhaustive}, instantiate_exhaustive_datatype) |
504 (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype)) |
|
505 |
504 |
506 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true); |
505 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true); |
507 |
506 |
508 val setup = |
507 val setup = |
509 Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
508 Quickcheck_Common.datatype_interpretation (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype) |
510 (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype)) |
|
511 (* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
509 (* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
512 (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype)) |
510 (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype)) |
513 #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
511 #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
514 (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype)) |
512 (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype)) |
515 #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
513 #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |