# HG changeset patch # User bulwahn # Date 1319091635 -7200 # Node ID 92e03ea2b5cf593564b5bb4fafa74627efba7c4e # Parent 3dd426ae6bead211586ad056807a382434c8d26b adding depth as an quickcheck configuration diff -r 3dd426ae6bea -r 92e03ea2b5cf src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Wed Oct 19 23:07:48 2011 +0200 +++ b/src/Tools/quickcheck.ML Thu Oct 20 08:20:35 2011 +0200 @@ -16,6 +16,7 @@ val batch_tester : string Config.T val size : int Config.T val iterations : int Config.T + val depth : int Config.T val no_assms : bool Config.T val report : bool Config.T val timing : bool Config.T @@ -163,6 +164,8 @@ val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "") val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10) val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100) +val depth = Attrib.setup_config_int @{binding quickcheck_depth} (K 10) + val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false) val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true) val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false) @@ -397,6 +400,7 @@ fun parse_test_param ("tester", args) = fold parse_tester args | parse_test_param ("size", [arg]) = apsnd (Config.put_generic size (read_nat arg)) | parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg)) + | parse_test_param ("depth", [arg]) = apsnd (Config.put_generic depth (read_nat arg)) | parse_test_param ("default_type", arg) = (fn (testers, gen_ctxt) => (testers, map_test_params ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt))