--- a/src/HOL/Tools/inductive_codegen.ML Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Dec 03 08:40:47 2010 +0100
@@ -9,7 +9,7 @@
val add : string option -> int option -> attribute
val test_fn : (int * int * int -> term list option) Unsynchronized.ref
val test_term:
- Proof.context -> term -> int -> term list option * (bool list * bool)
+ Proof.context -> term -> int -> term list option * Quickcheck.report option
val setup : theory -> theory
val quickcheck_setup : theory -> theory
end;
@@ -842,10 +842,9 @@
val start = Config.get ctxt depth_start;
val offset = Config.get ctxt size_offset;
val test_fn' = !test_fn;
- val dummy_report = ([], false)
fun test k = (deepen bound (fn i =>
(Output.urgent_message ("Search depth: " ^ string_of_int i);
- test_fn' (i, values, k+offset))) start, dummy_report);
+ test_fn' (i, values, k+offset))) start, NONE);
in test end;
val quickcheck_setup =
--- a/src/HOL/Tools/quickcheck_generators.ML Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML Fri Dec 03 08:40:47 2010 +0100
@@ -17,7 +17,7 @@
string list * string list -> typ list * typ list -> theory -> theory)
-> Datatype.config -> string list -> theory -> theory
val compile_generator_expr:
- Proof.context -> term -> int -> term list option * (bool list * bool)
+ Proof.context -> term -> int -> term list option * Quickcheck.report option
val put_counterexample: (unit -> int -> seed -> term list option * seed)
-> Proof.context -> Proof.context
val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed)
@@ -387,25 +387,73 @@
Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
end
+(* single quickcheck report *)
+
+datatype single_report = Run of bool list * bool | MatchExc
+
+fun collect_single_report single_report
+ (Quickcheck.Report {iterations = iterations, raised_match_errors = raised_match_errors,
+ satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
+ case single_report
+ of MatchExc =>
+ Quickcheck.Report {iterations = iterations + 1, raised_match_errors = raised_match_errors + 1,
+ satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}
+ | Run (assms, concl) =>
+ Quickcheck.Report {iterations = iterations + 1, raised_match_errors = raised_match_errors,
+ satisfied_assms =
+ map2 (fn b => fn s => if b then s + 1 else s) assms
+ (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
+ positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
+
+val empty_report = Quickcheck.Report { iterations = 0, raised_match_errors = 0,
+ satisfied_assms = [], positive_concl_tests = 0 }
+
fun compile_generator_expr ctxt t =
let
val Ts = (map snd o fst o strip_abs) t;
val thy = ProofContext.theory_of ctxt
- in if Config.get ctxt Quickcheck.report then
- let
- val t' = mk_reporting_generator_expr thy t Ts;
- val compile = Code_Runtime.dynamic_value_strict
- (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
- thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
- in compile #> Random_Engine.run end
- else
- let
- val t' = mk_generator_expr thy t Ts;
- val compile = Code_Runtime.dynamic_value_strict
- (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
- thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
- val dummy_report = ([], false)
- in compile #> Random_Engine.run #> rpair dummy_report end
+ val iterations = Config.get ctxt Quickcheck.iterations
+ in
+ if Config.get ctxt Quickcheck.report then
+ let
+ val t' = mk_reporting_generator_expr thy t Ts;
+ val compile = Code_Runtime.dynamic_value_strict
+ (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
+ thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
+ val single_tester = compile #> Random_Engine.run
+ fun iterate_and_collect size 0 report = (NONE, report)
+ | iterate_and_collect size j report =
+ let
+ val (test_result, single_report) = apsnd Run (single_tester size) handle Match =>
+ (if Config.get ctxt Quickcheck.quiet then ()
+ else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
+ val report = collect_single_report single_report report
+ in
+ case test_result of NONE => iterate_and_collect size (j - 1) report
+ | SOME q => (SOME q, report)
+ end
+ in
+ fn size => apsnd SOME (iterate_and_collect size iterations empty_report)
+ end
+ else
+ let
+ val t' = mk_generator_expr thy t Ts;
+ val compile = Code_Runtime.dynamic_value_strict
+ (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
+ thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
+ val single_tester = compile #> Random_Engine.run
+ fun iterate size 0 = NONE
+ | iterate size j =
+ let
+ val result = single_tester size handle Match =>
+ (if Config.get ctxt Quickcheck.quiet then ()
+ else warning "Exception Match raised during quickcheck"; NONE)
+ in
+ case result of NONE => iterate size (j - 1) | SOME q => SOME q
+ end
+ in
+ fn size => (rpair NONE (iterate size iterations))
+ end
end;
--- a/src/HOL/Tools/smallvalue_generators.ML Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML Fri Dec 03 08:40:47 2010 +0100
@@ -7,7 +7,7 @@
signature SMALLVALUE_GENERATORS =
sig
val compile_generator_expr:
- Proof.context -> term -> int -> term list option * (bool list * bool)
+ Proof.context -> term -> int -> term list option * Quickcheck.report option
val put_counterexample: (unit -> int -> term list option)
-> Proof.context -> Proof.context
val smart_quantifier : bool Config.T;
@@ -272,19 +272,15 @@
in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
fun compile_generator_expr ctxt t =
- if Config.get ctxt Quickcheck.report then
- error "Compilation with reporting facility is not supported"
- else
- let
- val thy = ProofContext.theory_of ctxt
- val t' =
- (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
- ctxt t;
- val compile = Code_Runtime.dynamic_value_strict
- (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
- thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
- val dummy_report = ([], false)
- in compile #> rpair dummy_report end;
+ let
+ val thy = ProofContext.theory_of ctxt
+ val t' =
+ (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
+ ctxt t;
+ val compile = Code_Runtime.dynamic_value_strict
+ (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
+ thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
+ in fn size => rpair NONE (compile size) end;
(** setup **)
--- a/src/Tools/quickcheck.ML Fri Dec 03 08:40:47 2010 +0100
+++ b/src/Tools/quickcheck.ML Fri Dec 03 08:40:47 2010 +0100
@@ -28,7 +28,7 @@
val map_test_params : (typ list * expectation -> typ list * expectation)
-> Context.generic -> Context.generic
val add_generator:
- string * (Proof.context -> term -> int -> term list option * (bool list * bool))
+ string * (Proof.context -> term -> int -> term list option * report option)
-> Context.generic -> Context.generic
(* testing terms and proof states *)
val test_term: Proof.context -> bool -> term ->
@@ -57,26 +57,10 @@
(* quickcheck report *)
-datatype single_report = Run of bool list * bool | MatchExc
-
datatype report = Report of
{ iterations : int, raised_match_errors : int,
satisfied_assms : int list, positive_concl_tests : int }
-fun collect_single_report single_report
- (Report {iterations = iterations, raised_match_errors = raised_match_errors,
- satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
- case single_report
- of MatchExc =>
- Report {iterations = iterations + 1, raised_match_errors = raised_match_errors + 1,
- satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}
- | Run (assms, concl) =>
- Report {iterations = iterations + 1, raised_match_errors = raised_match_errors,
- satisfied_assms =
- map2 (fn b => fn s => if b then s + 1 else s) assms
- (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
- positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
-
(* expectation *)
datatype expectation = No_Expectation | No_Counterexample | Counterexample;
@@ -116,7 +100,7 @@
structure Data = Generic_Data
(
type T =
- (string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list
+ (string * (Proof.context -> term -> int -> term list option * report option)) list
* test_params;
val empty = ([], Test_Params {default_type = [], expect = No_Expectation});
val extend = I;
@@ -172,11 +156,6 @@
val result = Exn.capture f ()
val time = Time.toMilliseconds (#cpu (end_timing start))
in (Exn.release result, (description, time)) end
-
-(* we actually assume we know the generators and its behaviour *)
-fun is_iteratable "SML" = true
- | is_iteratable "random" = true
- | is_iteratable _ = false
fun test_term ctxt is_interactive t =
let
@@ -185,30 +164,18 @@
fun excipit s =
"Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt t');
- fun iterate f 0 report = (NONE, report)
- | iterate f j report =
+ fun with_size test_fun k reports =
+ if k > Config.get ctxt size then
+ (NONE, reports)
+ else
let
- val (test_result, single_report) = apsnd Run (f ()) handle Match =>
- (if Config.get ctxt quiet then ()
- else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
- val report = collect_single_report single_report report
- in
- case test_result of NONE => iterate f (j - 1) report | SOME q => (SOME q, report)
- end
- val empty_report = Report { iterations = 0, raised_match_errors = 0,
- satisfied_assms = [], positive_concl_tests = 0 }
- fun with_size test_fun k reports =
- if k > Config.get ctxt size then (NONE, reports)
- else
- (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
- let
+ val _ = if Config.get ctxt quiet then () else Output.urgent_message
+ ("Test data size: " ^ string_of_int k)
val _ = current_size := k
- val niterations =
- if is_iteratable (Config.get ctxt tester) then Config.get ctxt iterations else 1
- val ((result, new_report), timing) = cpu_time ("size " ^ string_of_int k)
- (fn () => iterate (fn () => test_fun (k - 1)) niterations empty_report)
- val reports = ((k, new_report) :: reports)
- in case result of NONE => with_size test_fun (k + 1) reports | SOME q => (SOME q, reports) end);
+ val ((result, new_report), timing) =
+ cpu_time ("size " ^ string_of_int k) (fn () => test_fun (k - 1))
+ val reports = case new_report of NONE => reports | SOME rep => (k, rep) :: reports
+ in case result of NONE => with_size test_fun (k + 1) reports | SOME q => (SOME q, reports) end;
in
case test_fun of NONE => (NONE, ([comp_time], NONE))
| SOME test_fun =>