--- a/src/Tools/quickcheck.ML Tue Mar 29 23:46:46 2011 +0200
+++ b/src/Tools/quickcheck.ML Wed Mar 30 09:44:16 2011 +0200
@@ -29,7 +29,7 @@
satisfied_assms : int list, positive_concl_tests : int }
(* registering generators *)
val add_generator:
- string * (Proof.context -> term * term list -> int -> term list option * report option)
+ string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)
-> Context.generic -> Context.generic
val add_batch_generator:
string * (Proof.context -> term list -> (int -> term list option) list)
@@ -161,7 +161,7 @@
structure Data = Generic_Data
(
type T =
- ((string * (Proof.context -> term * term list -> int -> term list option * report option)) list
+ ((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list
* (string * (Proof.context -> term list -> (int -> term list option) list)) list)
* test_params;
val empty = (([], []), Test_Params {default_type = [], expect = No_Expectation});
@@ -240,7 +240,7 @@
fun excipit () =
"Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
val (test_fun, comp_time) = cpu_time "quickcheck compilation"
- (fn () => mk_tester ctxt (t, eval_terms));
+ (fn () => mk_tester ctxt [(t, eval_terms)]);
val _ = add_timing comp_time current_result
fun with_size test_fun k =
if k > Config.get ctxt size then
@@ -250,7 +250,7 @@
val _ = message ("Test data size: " ^ string_of_int k)
val _ = current_size := k
val ((result, report), timing) =
- cpu_time ("size " ^ string_of_int k) (fn () => test_fun (k - 1))
+ cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1])
val _ = add_timing timing current_result
val _ = add_report k report current_result
in
@@ -293,19 +293,18 @@
let
val thy = ProofContext.theory_of ctxt
fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
- val (ts, eval_terms) = split_list ts
- val _ = map check_test_term ts
- val names = Term.add_free_names (hd ts) []
- val Ts = map snd (Term.add_frees (hd ts) [])
+ val (ts', eval_terms) = split_list ts
+ val _ = map check_test_term ts'
+ val names = Term.add_free_names (hd ts') []
+ val Ts = map snd (Term.add_frees (hd ts') [])
val current_result = Unsynchronized.ref empty_result
- val (test_funs, comp_time) = cpu_time "quickcheck compilation"
- (fn () => map (mk_tester ctxt) (ts ~~ eval_terms))
+ val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt ts)
val _ = add_timing comp_time current_result
fun test_card_size (card, size) =
(* FIXME: why decrement size by one? *)
let
val (ts, timing) = cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
- (fn () => fst (the (nth test_funs (card - 1)) (size - 1)))
+ (fn () => fst ((the test_fun) [card - 1, size - 1]))
val _ = add_timing timing current_result
in
Option.map (pair card) ts
@@ -319,8 +318,9 @@
map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size))
|> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
in
- if (forall is_none test_funs) then !current_result
- else if (forall is_some test_funs) then
+ case test_fun of
+ NONE => !current_result
+ | SOME test_fun =>
limit ctxt (limit_time, is_interactive) (fn () =>
let
val _ = case get_first test_card_size enumeration_card_size of
@@ -328,8 +328,6 @@
| NONE => ()
in !current_result end)
(fn () => (message "Quickcheck ran out of time"; !current_result)) ()
- else
- error "Unexpectedly, testers of some cardinalities are executable but others are not"
end
fun get_finite_types ctxt =