equal
deleted
inserted
replaced
16 structure Narrowing_Generators : NARROWING_GENERATORS = |
16 structure Narrowing_Generators : NARROWING_GENERATORS = |
17 struct |
17 struct |
18 |
18 |
19 (* configurations *) |
19 (* configurations *) |
20 |
20 |
21 val (finite_functions, setup_finite_functions) = |
21 val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true) |
22 Attrib.config_bool "quickcheck_finite_functions" (K true) |
|
23 |
22 |
24 (* narrowing specific names and types *) |
23 (* narrowing specific names and types *) |
25 |
24 |
26 exception FUNCTION_TYPE; |
25 exception FUNCTION_TYPE; |
27 |
26 |
206 |
205 |
207 |
206 |
208 val setup = |
207 val setup = |
209 Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
208 Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype |
210 (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype)) |
209 (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype)) |
211 #> setup_finite_functions |
|
212 #> Context.theory_map |
210 #> Context.theory_map |
213 (Quickcheck.add_generator ("narrowing", compile_generator_expr)) |
211 (Quickcheck.add_generator ("narrowing", compile_generator_expr)) |
214 |
212 |
215 end; |
213 end; |