# 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))