src/Tools/quickcheck.ML
changeset 45213 92e03ea2b5cf
parent 45159 3f1d1ce024cb
child 45313 16bab9f1bb37
     1.1 --- a/src/Tools/quickcheck.ML	Wed Oct 19 23:07:48 2011 +0200
     1.2 +++ b/src/Tools/quickcheck.ML	Thu Oct 20 08:20:35 2011 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4    val batch_tester : string Config.T
     1.5    val size : int Config.T
     1.6    val iterations : int Config.T
     1.7 +  val depth : int Config.T
     1.8    val no_assms : bool Config.T
     1.9    val report : bool Config.T
    1.10    val timing : bool Config.T
    1.11 @@ -163,6 +164,8 @@
    1.12  val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "")
    1.13  val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10)
    1.14  val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100)
    1.15 +val depth = Attrib.setup_config_int @{binding quickcheck_depth} (K 10)
    1.16 +
    1.17  val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
    1.18  val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
    1.19  val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
    1.20 @@ -397,6 +400,7 @@
    1.21  fun parse_test_param ("tester", args) = fold parse_tester args
    1.22    | parse_test_param ("size", [arg]) = apsnd (Config.put_generic size (read_nat arg))
    1.23    | parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg))
    1.24 +  | parse_test_param ("depth", [arg]) = apsnd (Config.put_generic depth (read_nat arg))  
    1.25    | parse_test_param ("default_type", arg) = (fn (testers, gen_ctxt) =>
    1.26      (testers, map_test_params
    1.27        ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt))