1.1 --- a/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4    val map_test_params : (typ list * expectation -> typ list * expectation)
     1.5      -> Context.generic -> Context.generic
     1.6    val add_generator:
     1.7 -    string * (Proof.context -> term -> int -> term list option * (bool list * bool))
     1.8 +    string * (Proof.context -> term -> int -> term list option * report option)
     1.9        -> Context.generic -> Context.generic
    1.10    (* testing terms and proof states *)
    1.11    val test_term: Proof.context -> bool -> term ->
    1.12 @@ -57,26 +57,10 @@
    1.13  
    1.14  (* quickcheck report *)
    1.15  
    1.16 -datatype single_report = Run of bool list * bool | MatchExc
    1.17 -
    1.18  datatype report = Report of
    1.19    { iterations : int, raised_match_errors : int,
    1.20      satisfied_assms : int list, positive_concl_tests : int }
    1.21  
    1.22 -fun collect_single_report single_report
    1.23 -    (Report {iterations = iterations, raised_match_errors = raised_match_errors,
    1.24 -    satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
    1.25 -  case single_report
    1.26 -  of MatchExc =>
    1.27 -    Report {iterations = iterations + 1, raised_match_errors = raised_match_errors + 1,
    1.28 -      satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}
    1.29 -   | Run (assms, concl) =>
    1.30 -    Report {iterations = iterations + 1, raised_match_errors = raised_match_errors,
    1.31 -      satisfied_assms =
    1.32 -        map2 (fn b => fn s => if b then s + 1 else s) assms
    1.33 -         (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
    1.34 -      positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
    1.35 -
    1.36  (* expectation *)
    1.37  
    1.38  datatype expectation = No_Expectation | No_Counterexample | Counterexample; 
    1.39 @@ -116,7 +100,7 @@
    1.40  structure Data = Generic_Data
    1.41  (
    1.42    type T =
    1.43 -    (string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list
    1.44 +    (string * (Proof.context -> term -> int -> term list option * report option)) list
    1.45        * test_params;
    1.46    val empty = ([], Test_Params {default_type = [], expect = No_Expectation});
    1.47    val extend = I;
    1.48 @@ -172,11 +156,6 @@
    1.49      val result = Exn.capture f ()
    1.50      val time = Time.toMilliseconds (#cpu (end_timing start))
    1.51    in (Exn.release result, (description, time)) end
    1.52 -
    1.53 -(* we actually assume we know the generators and its behaviour *)
    1.54 -fun is_iteratable "SML" = true
    1.55 -  | is_iteratable "random" = true
    1.56 -  | is_iteratable _ = false
    1.57    
    1.58  fun test_term ctxt is_interactive t =
    1.59    let
    1.60 @@ -185,30 +164,18 @@
    1.61      fun excipit s =
    1.62        "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
    1.63      val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt t');
    1.64 -    fun iterate f 0 report = (NONE, report)
    1.65 -      | iterate f j report =
    1.66 +    fun with_size test_fun k reports =
    1.67 +      if k > Config.get ctxt size then
    1.68 +        (NONE, reports)
    1.69 +      else
    1.70          let
    1.71 -          val (test_result, single_report) = apsnd Run (f ()) handle Match => 
    1.72 -            (if Config.get ctxt quiet then ()
    1.73 -             else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
    1.74 -          val report = collect_single_report single_report report
    1.75 -        in
    1.76 -          case test_result of NONE => iterate f (j - 1) report | SOME q => (SOME q, report)
    1.77 -        end
    1.78 -    val empty_report = Report { iterations = 0, raised_match_errors = 0,
    1.79 -      satisfied_assms = [], positive_concl_tests = 0 }
    1.80 -    fun with_size test_fun k reports =
    1.81 -      if k > Config.get ctxt size then (NONE, reports)
    1.82 -      else
    1.83 -       (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
    1.84 -        let
    1.85 +          val _ = if Config.get ctxt quiet then () else Output.urgent_message
    1.86 +            ("Test data size: " ^ string_of_int k)
    1.87            val _ = current_size := k
    1.88 -          val niterations =
    1.89 -            if is_iteratable (Config.get ctxt tester) then Config.get ctxt iterations else 1
    1.90 -          val ((result, new_report), timing) = cpu_time ("size " ^ string_of_int k)
    1.91 -            (fn () => iterate (fn () => test_fun (k - 1)) niterations empty_report)
    1.92 -          val reports = ((k, new_report) :: reports)
    1.93 -        in case result of NONE => with_size test_fun (k + 1) reports | SOME q => (SOME q, reports) end);
    1.94 +          val ((result, new_report), timing) =
    1.95 +            cpu_time ("size " ^ string_of_int k) (fn () => test_fun (k - 1))
    1.96 +          val reports = case new_report of NONE => reports | SOME rep => (k, rep) :: reports
    1.97 +        in case result of NONE => with_size test_fun (k + 1) reports | SOME q => (SOME q, reports) end;
    1.98    in
    1.99      case test_fun of NONE => (NONE, ([comp_time], NONE)) 
   1.100        | SOME test_fun =>