# HG changeset patch # User bulwahn # Date 1291362047 -3600 # Node ID 7febf76e0a69f7f55b43fee86f9a7fedc312f123 # Parent 508c838273647e7e7feaea182cebb4de077bb978 moving iteration of tests to the testers in quickcheck diff -r 508c83827364 -r 7febf76e0a69 src/HOL/Tools/inductive_codegen.ML --- 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 = diff -r 508c83827364 -r 7febf76e0a69 src/HOL/Tools/quickcheck_generators.ML --- 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; diff -r 508c83827364 -r 7febf76e0a69 src/HOL/Tools/smallvalue_generators.ML --- 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 **) diff -r 508c83827364 -r 7febf76e0a69 src/Tools/quickcheck.ML --- 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 =>