--- a/src/HOL/Tools/quickcheck_generators.ML Tue Feb 23 16:58:21 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML Thu Feb 25 09:28:01 2010 +0100
@@ -15,8 +15,11 @@
-> string list -> string list * string list -> typ list * typ list
-> term list * (term * term) list
val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
- val compile_generator_expr: theory -> term -> int -> term list option
+ val compile_generator_expr:
+ theory -> bool -> term -> int -> term list option * (bool list * bool)
val eval_ref: (unit -> int -> seed -> term list option * seed) option Unsynchronized.ref
+ val eval_report_ref:
+ (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref
val setup: theory -> theory
end;
@@ -350,6 +353,10 @@
(unit -> int -> int * int -> term list option * (int * int)) option Unsynchronized.ref =
Unsynchronized.ref NONE;
+val eval_report_ref :
+ (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref =
+ Unsynchronized.ref NONE;
+
val target = "Quickcheck";
fun mk_generator_expr thy prop Ts =
@@ -360,7 +367,7 @@
val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
val check = @{term "If :: bool => term list option => term list option => term list option"}
- $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option "} $ terms);
+ $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms);
val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"};
fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
@@ -375,13 +382,69 @@
(Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
-fun compile_generator_expr thy t =
+fun mk_reporting_generator_expr thy prop Ts =
+ let
+ val bound_max = length Ts - 1;
+ val bounds = map_index (fn (i, ty) =>
+ (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
+ fun strip_imp (Const("op -->",_) $ A $ B) = apfst (cons A) (strip_imp B)
+ | strip_imp A = ([], A)
+ val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
+ val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
+ val (assms, concl) = strip_imp prop'
+ val return =
+ @{term "Pair :: term list option * (bool list * bool) => Random.seed => (term list option * (bool list * bool)) * Random.seed"};
+ fun mk_assms_report i =
+ HOLogic.mk_prod (@{term "None :: term list option"},
+ HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"}
+ (replicate i @{term "True"} @ replicate (length assms - i) @{term "False"}),
+ @{term "False"}))
+ fun mk_concl_report b =
+ HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"} (replicate (length assms) @{term "True"}),
+ if b then @{term True} else @{term False})
+ val If =
+ @{term "If :: bool => term list option * (bool list * bool) => term list option * (bool list * bool) => term list option * (bool list * bool)"}
+ val concl_check = If $ concl $
+ HOLogic.mk_prod (@{term "None :: term list option"}, mk_concl_report true) $
+ HOLogic.mk_prod (@{term "Some :: term list => term list option"} $ terms, mk_concl_report false)
+ val check = fold_rev (fn (i, assm) => fn t => If $ assm $ t $ mk_assms_report i)
+ (map_index I assms) concl_check
+ fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
+ fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
+ fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
+ liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
+ fun mk_split T = Sign.mk_const thy
+ (@{const_name split}, [T, @{typ "unit => term"},
+ liftT @{typ "term list option * (bool list * bool)"} @{typ Random.seed}]);
+ fun mk_scomp_split T t t' =
+ mk_scomp (mk_termtyp T) @{typ "term list option * (bool list * bool)"} @{typ Random.seed} t
+ (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
+ fun mk_bindclause (_, _, i, T) = mk_scomp_split T
+ (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
+ in
+ Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
+ end
+
+fun compile_generator_expr thy report t =
let
val Ts = (map snd o fst o strip_abs) t;
- val t' = mk_generator_expr thy t Ts;
- val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
- (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
- in compile #> Random_Engine.run end;
+ in
+ if report then
+ let
+ val t' = mk_reporting_generator_expr thy t Ts;
+ val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref)
+ (fn proc => fn g => fn s => g s #>> ((apfst o Option.map o map) proc)) thy t' [];
+ in
+ compile #> Random_Engine.run
+ end
+ else
+ let
+ val t' = mk_generator_expr thy t Ts;
+ val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
+ (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+ val dummy_report = ([], false)
+ in fn s => ((compile #> Random_Engine.run) s, dummy_report) end
+ end;
(** setup **)
--- a/src/Tools/quickcheck.ML Tue Feb 23 16:58:21 2010 +0100
+++ b/src/Tools/quickcheck.ML Thu Feb 25 09:28:01 2010 +0100
@@ -8,11 +8,16 @@
sig
val auto: bool Unsynchronized.ref
val timing : bool Unsynchronized.ref
+ datatype report = Report of
+ { iterations : int, raised_match_errors : int,
+ satisfied_assms : int list, positive_concl_tests : int }
+ val gen_test_term: Proof.context -> bool -> bool -> string option -> int -> int -> term ->
+ ((string * term) list option * ((string * int) list * (int * report list) list))
val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
(string * term) list option
- val timed_test_term: Proof.context -> bool -> string option -> int -> int -> term ->
- ((string * term) list option * (string * int) list)
- val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
+ val add_generator:
+ string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))
+ -> theory -> theory
val setup: theory -> theory
val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
end;
@@ -33,31 +38,54 @@
"auto-quickcheck"
"Whether to run Quickcheck automatically.") ());
+(* 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}
(* quickcheck configuration -- default parameters, test generators *)
datatype test_params = Test_Params of
- { size: int, iterations: int, default_type: typ option, no_assms: bool };
+ { size: int, iterations: int, default_type: typ option, no_assms: bool, report: bool};
-fun dest_test_params (Test_Params { size, iterations, default_type, no_assms }) =
- ((size, iterations), (default_type, no_assms));
-fun make_test_params ((size, iterations), (default_type, no_assms)) =
+fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, report }) =
+ ((size, iterations), ((default_type, no_assms), report));
+fun make_test_params ((size, iterations), ((default_type, no_assms), report)) =
Test_Params { size = size, iterations = iterations, default_type = default_type,
- no_assms = no_assms };
-fun map_test_params f (Test_Params { size, iterations, default_type, no_assms }) =
- make_test_params (f ((size, iterations), (default_type, no_assms)));
+ no_assms = no_assms, report = report };
+fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, report }) =
+ make_test_params (f ((size, iterations), ((default_type, no_assms), report)));
fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
- no_assms = no_assms1 },
+ no_assms = no_assms1, report = report1 },
Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
- no_assms = no_assms2 }) =
+ no_assms = no_assms2, report = report2 }) =
make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
- (case default_type1 of NONE => default_type2 | _ => default_type1, no_assms1 orelse no_assms2));
+ ((case default_type1 of NONE => default_type2 | _ => default_type1, no_assms1 orelse no_assms2),
+ report1 orelse report2));
structure Data = Theory_Data
(
- type T = (string * (Proof.context -> term -> int -> term list option)) list
+ type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
* test_params;
- val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE, no_assms = false });
+ val empty = ([], Test_Params
+ { size = 10, iterations = 100, default_type = NONE, no_assms = false, report = false});
val extend = I;
fun merge ((generators1, params1), (generators2, params2)) : T =
(AList.merge (op =) (K true) (generators1, generators2),
@@ -66,7 +94,6 @@
val add_generator = Data.map o apfst o AList.update (op =);
-
(* generating tests *)
fun mk_tester_select name ctxt =
@@ -74,14 +101,14 @@
of NONE => error ("No such quickcheck generator: " ^ name)
| SOME generator => generator ctxt;
-fun mk_testers ctxt t =
+fun mk_testers ctxt report t =
(map snd o fst o Data.get o ProofContext.theory_of) ctxt
- |> map_filter (fn generator => try (generator ctxt) t);
+ |> map_filter (fn generator => try (generator ctxt report) t);
-fun mk_testers_strict ctxt t =
+fun mk_testers_strict ctxt report t =
let
val generators = ((map snd o fst o Data.get o ProofContext.theory_of) ctxt)
- val testers = map (fn generator => Exn.capture (generator ctxt) t) generators;
+ val testers = map (fn generator => Exn.capture (generator ctxt report) t) generators;
in if forall (is_none o Exn.get_result) testers
then [(Exn.release o snd o split_last) testers]
else map_filter Exn.get_result testers
@@ -106,36 +133,45 @@
val time = Time.toMilliseconds (#cpu (end_timing start))
in (Exn.release result, (description, time)) end
-fun timed_test_term ctxt quiet generator_name size i t =
+fun gen_test_term ctxt quiet report generator_name size i t =
let
val (names, t') = prep_test_term t;
val (testers, comp_time) = cpu_time "quickcheck compilation"
(fn () => (case generator_name
- of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
- | SOME name => [mk_tester_select name ctxt t']));
- fun iterate f 0 = NONE
- | iterate f j = case f () handle Match => (if quiet then ()
- else warning "Exception Match raised during quickcheck"; NONE)
- of NONE => iterate f (j - 1) | SOME q => SOME q;
- fun with_testers k [] = NONE
+ of NONE => if quiet then mk_testers ctxt report t' else mk_testers_strict ctxt report t'
+ | SOME name => [mk_tester_select name ctxt report t']));
+ fun iterate f 0 report = (NONE, report)
+ | iterate f j report =
+ let
+ val (test_result, single_report) = apsnd Run (f ()) handle Match => (if 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_testers k [] = (NONE, [])
| with_testers k (tester :: testers) =
- case iterate (fn () => tester (k - 1)) i
- of NONE => with_testers k testers
- | SOME q => SOME q;
- fun with_size k = if k > size then NONE
+ case iterate (fn () => tester (k - 1)) i empty_report
+ of (NONE, report) => apsnd (cons report) (with_testers k testers)
+ | (SOME q, report) => (SOME q, [report]);
+ fun with_size k reports = if k > size then (NONE, reports)
else (if quiet then () else priority ("Test data size: " ^ string_of_int k);
- case with_testers k testers
- of NONE => with_size (k + 1) | SOME q => SOME q);
- val (result, exec_time) = cpu_time "quickcheck execution"
- (fn () => case with_size 1
- of NONE => NONE
- | SOME ts => SOME (names ~~ ts))
+ let
+ val (result, new_report) = with_testers k testers
+ val reports = ((k, new_report) :: reports)
+ in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
+ val ((result, reports), exec_time) = cpu_time "quickcheck execution"
+ (fn () => apfst
+ (fn result => case result of NONE => NONE
+ | SOME ts => SOME (names ~~ ts)) (with_size 1 []))
in
- (result, [exec_time, comp_time])
+ (result, ([exec_time, comp_time], reports))
end;
fun test_term ctxt quiet generator_name size i t =
- fst (timed_test_term ctxt quiet generator_name size i t)
+ fst (gen_test_term ctxt quiet false generator_name size i t)
fun monomorphic_term thy insts default_T =
let
@@ -152,7 +188,7 @@
| subst T = T;
in (map_types o map_atyps) subst end;
-fun test_goal quiet generator_name size iterations default_T no_assms insts i assms state =
+fun test_goal quiet report generator_name size iterations default_T no_assms insts i assms state =
let
val ctxt = Proof.context_of state;
val thy = Proof.theory_of state;
@@ -164,7 +200,7 @@
subst_bounds (frees, strip gi))
|> monomorphic_term thy insts default_T
|> ObjectLogic.atomize_term thy;
- in test_term ctxt quiet generator_name size iterations gi' end;
+ in gen_test_term ctxt quiet report generator_name size iterations gi' end;
fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."
| pretty_counterex ctxt (SOME cex) =
@@ -172,6 +208,32 @@
map (fn (s, t) =>
Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
+fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors,
+ satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
+ let
+ fun pretty_stat s i = Pretty.block ([Pretty.str (s ^ ": " ^ string_of_int i)])
+ in
+ ([pretty_stat "iterations" iterations,
+ pretty_stat "match exceptions" raised_match_errors]
+ @ map_index (fn (i, n) => pretty_stat ("satisfied " ^ string_of_int (i + 1) ^ ". assumption") n)
+ satisfied_assms
+ @ [pretty_stat "positive conclusion tests" positive_concl_tests])
+ end
+
+fun pretty_reports' [report] = [Pretty.chunks (pretty_report report)]
+ | pretty_reports' reports =
+ map_index (fn (i, report) =>
+ Pretty.chunks (Pretty.str (string_of_int (i + 1) ^ ". generator:\n") :: pretty_report report))
+ reports
+
+fun pretty_reports ctxt reports =
+ Pretty.chunks (Pretty.str "Quickcheck report:" ::
+ maps (fn (size, reports) =>
+ Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_reports' reports @ [Pretty.brk 1])
+ (rev reports))
+
+fun pretty_counterex_and_reports ctxt (cex, (timing, reports)) =
+ Pretty.chunks [pretty_counterex ctxt cex, pretty_reports ctxt reports]
(* automatic testing *)
@@ -182,15 +244,15 @@
let
val ctxt = Proof.context_of state;
val assms = map term_of (Assumption.all_assms_of ctxt);
- val Test_Params { size, iterations, default_type, no_assms } =
+ val Test_Params { size, iterations, default_type, no_assms, report } =
(snd o Data.get o Proof.theory_of) state;
val res =
- try (test_goal true NONE size iterations default_type no_assms [] 1 assms) state;
+ try (test_goal true false NONE size iterations default_type no_assms [] 1 assms) state;
in
case res of
NONE => (false, state)
- | SOME NONE => (false, state)
- | SOME cex => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
+ | SOME (NONE, report) => (false, state)
+ | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state)
end
@@ -212,8 +274,10 @@
| parse_test_param ctxt ("iterations", arg) =
(apfst o apsnd o K) (read_nat arg)
| parse_test_param ctxt ("default_type", arg) =
- (apsnd o apfst o K o SOME) (ProofContext.read_typ ctxt arg)
+ (apsnd o apfst o apfst o K o SOME) (ProofContext.read_typ ctxt arg)
| parse_test_param ctxt ("no_assms", arg) =
+ (apsnd o apfst o apsnd o K) (read_bool arg)
+ | parse_test_param ctxt ("report", arg) =
(apsnd o apsnd o K) (read_bool arg)
| parse_test_param ctxt (name, _) =
error ("Unknown test parameter: " ^ name);
@@ -235,22 +299,24 @@
|> (Data.map o apsnd o map_test_params) f
end;
-fun quickcheck args i state =
+fun gen_quickcheck args i state =
let
val thy = Proof.theory_of state;
val ctxt = Proof.context_of state;
val assms = map term_of (Assumption.all_assms_of ctxt);
val default_params = (dest_test_params o snd o Data.get) thy;
val f = fold (parse_test_param_inst ctxt) args;
- val (((size, iterations), (default_type, no_assms)), (generator_name, insts)) =
+ val (((size, iterations), ((default_type, no_assms), report)), (generator_name, insts)) =
f (default_params, (NONE, []));
in
- test_goal false generator_name size iterations default_type no_assms insts i assms state
+ test_goal false report generator_name size iterations default_type no_assms insts i assms state
end;
+fun quickcheck args i state = fst (gen_quickcheck args i state)
+
fun quickcheck_cmd args i state =
- quickcheck args i (Toplevel.proof_of state)
- |> Pretty.writeln o pretty_counterex (Toplevel.context_of state);
+ gen_quickcheck args i (Toplevel.proof_of state)
+ |> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state);
local structure P = OuterParse and K = OuterKeyword in