19 val depth : int Config.T |
19 val depth : int Config.T |
20 val no_assms : bool Config.T |
20 val no_assms : bool Config.T |
21 val report : bool Config.T |
21 val report : bool Config.T |
22 val timing : bool Config.T |
22 val timing : bool Config.T |
23 val genuine_only : bool Config.T |
23 val genuine_only : bool Config.T |
|
24 val abort_potential : bool Config.T |
24 val quiet : bool Config.T |
25 val quiet : bool Config.T |
25 val verbose : bool Config.T |
26 val verbose : bool Config.T |
26 val timeout : real Config.T |
27 val timeout : real Config.T |
27 val allow_function_inversion : bool Config.T; |
28 val allow_function_inversion : bool Config.T; |
28 val finite_types : bool Config.T |
29 val finite_types : bool Config.T |
175 |
176 |
176 val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false) |
177 val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false) |
177 val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true) |
178 val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true) |
178 val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false) |
179 val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false) |
179 val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false) |
180 val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false) |
|
181 val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false) |
180 val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false) |
182 val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false) |
181 val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false) |
183 val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false) |
182 val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0) |
184 val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0) |
183 val allow_function_inversion = |
185 val allow_function_inversion = |
184 Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false) |
186 Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false) |
431 ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt)) |
433 ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt)) |
432 | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg)) |
434 | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg)) |
433 | parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg))) |
435 | parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg))) |
434 | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg)) |
436 | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg)) |
435 | parse_test_param ("genuine_only", [arg]) = apsnd (Config.put_generic genuine_only (read_bool arg)) |
437 | parse_test_param ("genuine_only", [arg]) = apsnd (Config.put_generic genuine_only (read_bool arg)) |
|
438 | parse_test_param ("abort_potential", [arg]) = apsnd (Config.put_generic abort_potential (read_bool arg)) |
436 | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg)) |
439 | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg)) |
437 | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg)) |
440 | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg)) |
438 | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg)) |
441 | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg)) |
439 | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg)) |
442 | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg)) |
440 | parse_test_param ("allow_function_inversion", [arg]) = |
443 | parse_test_param ("allow_function_inversion", [arg]) = |