src/Tools/quickcheck.ML
changeset 40366 a2866dbfbe6b
parent 40253 f99ec71de82d
child 40381 96c37a685a13
     1.1 --- a/src/Tools/quickcheck.ML	Fri Nov 05 08:16:34 2010 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Fri Nov 05 08:16:35 2010 +0100
     1.3 @@ -16,12 +16,12 @@
     1.4    datatype expectation = No_Expectation | No_Counterexample | Counterexample;
     1.5    datatype test_params = Test_Params of
     1.6    { size: int, iterations: int, default_type: typ list, no_assms: bool,
     1.7 -    expect : expectation, report: bool, quiet : bool, timeout : int};
     1.8 +    expect : expectation, report: bool, quiet : bool, timeout : real};
     1.9    val test_params_of : Proof.context -> test_params
    1.10    val report : Proof.context -> bool
    1.11    val map_test_params :
    1.12 -    ((int * int) * ((typ list * bool) * ((expectation * bool) * (bool * int)))
    1.13 -      -> (int * int) * ((typ list * bool) * ((expectation * bool) * (bool * int))))
    1.14 +    ((int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real)))
    1.15 +      -> (int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real))))
    1.16      -> Context.generic -> Context.generic
    1.17    val add_generator:
    1.18      string * (Proof.context -> term -> int -> term list option * (bool list * bool))
    1.19 @@ -81,7 +81,7 @@
    1.20  
    1.21  datatype test_params = Test_Params of
    1.22    { size: int, iterations: int, default_type: typ list, no_assms: bool,
    1.23 -    expect : expectation, report: bool, quiet : bool, timeout : int};
    1.24 +    expect : expectation, report: bool, quiet : bool, timeout : real};
    1.25  
    1.26  fun dest_test_params
    1.27      (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
    1.28 @@ -105,7 +105,7 @@
    1.29    make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
    1.30      ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
    1.31      ((merge_expectation (expect1, expect2), report1 orelse report2),
    1.32 -    (quiet1 orelse quiet2, Int.min (timeout1, timeout2)))));
    1.33 +    (quiet1 orelse quiet2, Real.min (timeout1, timeout2)))));
    1.34  
    1.35  structure Data = Generic_Data
    1.36  (
    1.37 @@ -114,7 +114,7 @@
    1.38        * test_params;
    1.39    val empty = ([], Test_Params
    1.40      { size = 10, iterations = 100, default_type = [], no_assms = false,
    1.41 -      expect = No_Expectation, report = false, quiet = false, timeout = 30});
    1.42 +      expect = No_Expectation, report = false, quiet = false, timeout = 30.0});
    1.43    val extend = I;
    1.44    fun merge ((generators1, params1), (generators2, params2)) : T =
    1.45      (AList.merge (op =) (K true) (generators1, generators2),
    1.46 @@ -200,6 +200,9 @@
    1.47  fun test_term ctxt generator_name t =
    1.48    let
    1.49      val (names, t') = prep_test_term t;
    1.50 +    val current_size = Unsynchronized.ref 0
    1.51 +    fun excipit s =
    1.52 +      "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
    1.53      val (testers, comp_time) = cpu_time "quickcheck compilation"
    1.54        (fn () => (case generator_name
    1.55         of NONE => if quiet ctxt then mk_testers ctxt t' else mk_testers_strict ctxt t'
    1.56 @@ -225,15 +228,18 @@
    1.57        else
    1.58         (if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
    1.59          let
    1.60 +          val _ = current_size := k  
    1.61            val (result, new_report) = with_testers k testers
    1.62            val reports = ((k, new_report) :: reports)
    1.63          in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
    1.64      val ((result, reports), exec_time) =
    1.65 -      TimeLimit.timeLimit (Time.fromSeconds (timeout ctxt)) (fn () => cpu_time "quickcheck execution"
    1.66 +      TimeLimit.timeLimit (seconds (timeout ctxt)) (fn () => cpu_time "quickcheck execution"
    1.67        (fn () => apfst
    1.68           (fn result => case result of NONE => NONE
    1.69          | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
    1.70 -      handle TimeLimit.TimeOut => error "Reached timeout during Quickcheck"
    1.71 +      handle TimeLimit.TimeOut =>
    1.72 +        error (excipit "ran out of time")
    1.73 +     | Exn.Interrupt => error (excipit "was interrupted")
    1.74    in
    1.75      (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
    1.76    end;
    1.77 @@ -367,6 +373,11 @@
    1.78    | read_bool "true" = true
    1.79    | read_bool s = error ("Not a Boolean value: " ^ s)
    1.80  
    1.81 +fun read_real s =
    1.82 +  case (Real.fromString s) of
    1.83 +    SOME s => s
    1.84 +  | NONE => error ("Not a real number: " ^ s)
    1.85 +
    1.86  fun read_expectation "no_expectation" = No_Expectation
    1.87    | read_expectation "no_counterexample" = No_Counterexample 
    1.88    | read_expectation "counterexample" = Counterexample
    1.89 @@ -387,7 +398,7 @@
    1.90    | parse_test_param ctxt ("quiet", [arg]) =
    1.91        (apsnd o apsnd o apsnd o apfst o K) (read_bool arg)
    1.92    | parse_test_param ctxt ("timeout", [arg]) =
    1.93 -      (apsnd o apsnd o apsnd o apsnd o K) (read_nat arg)
    1.94 +      (apsnd o apsnd o apsnd o apsnd o K) (read_real arg)
    1.95    | parse_test_param ctxt (name, _) =
    1.96        error ("Unknown test parameter: " ^ name);
    1.97  
    1.98 @@ -431,7 +442,7 @@
    1.99    |> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state) false;
   1.100  
   1.101  val parse_arg = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- 
   1.102 -  ((Parse.name >> single) || (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]);
   1.103 +  (((Parse.name || Parse.float_number) >> single) || (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]);
   1.104  
   1.105  val parse_args = Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]"
   1.106    || Scan.succeed [];