--- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu Feb 25 22:46:52 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Feb 26 09:49:00 2010 +0100
@@ -12,9 +12,9 @@
datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
type timing = (string * int) list
-type mtd = string * (theory -> term -> outcome * timing)
+type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
-type mutant_subentry = term * (string * (outcome * timing)) list
+type mutant_subentry = term * (string * (outcome * (timing * Quickcheck.report option))) list
type detailed_entry = string * bool * term * mutant_subentry list
type subentry = string * int * int * int * int * int * int
@@ -54,7 +54,7 @@
(* quickcheck options *)
(*val quickcheck_generator = "SML"*)
-val iterations = 1
+val iterations = 100
val size = 5
exception RANDOM;
@@ -79,9 +79,9 @@
datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
type timing = (string * int) list
-type mtd = string * (theory -> term -> outcome * timing)
+type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
-type mutant_subentry = term * (string * (outcome * timing)) list
+type mutant_subentry = term * (string * (outcome * (timing * Quickcheck.report option))) list
type detailed_entry = string * bool * term * mutant_subentry list
type subentry = string * int * int * int * int * int * int
@@ -97,11 +97,11 @@
fun invoke_quickcheck quickcheck_generator thy t =
TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit))
(fn _ =>
- case Quickcheck.timed_test_term (ProofContext.init thy) false (SOME quickcheck_generator)
+ case Quickcheck.gen_test_term (ProofContext.init thy) true true (SOME quickcheck_generator)
size iterations (preprocess thy [] t) of
- (NONE, time_report) => (NoCex, time_report)
- | (SOME _, time_report) => (GenuineCex, time_report)) ()
- handle TimeLimit.TimeOut => (Timeout, [("timelimit", !Auto_Counterexample.time_limit)])
+ (NONE, (time_report, report)) => (NoCex, (time_report, report))
+ | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
+ handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Counterexample.time_limit)], NONE))
fun quickcheck_mtd quickcheck_generator =
("quickcheck_" ^ quickcheck_generator, invoke_quickcheck quickcheck_generator)
@@ -258,13 +258,13 @@
fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
let
val _ = priority ("Invoking " ^ mtd_name)
- val ((res, timing), time) = cpu_time "total time"
+ val ((res, (timing, reports)), time) = cpu_time "total time"
(fn () => case try (invoke_mtd thy) t of
- SOME (res, timing) => (res, timing)
+ SOME (res, (timing, reports)) => (res, (timing, reports))
| NONE => (priority ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
- (Error , [])))
+ (Error , ([], NONE))))
val _ = priority (" Done")
- in (res, time :: timing) end
+ in (res, (time :: timing, reports)) end
(* theory -> term list -> mtd -> subentry *)
(*
@@ -341,10 +341,21 @@
"\n"
fun string_of_mutant_subentry' thy thm_name (t, results) =
- "mutant of " ^ thm_name ^ ":" ^
- cat_lines (map (fn (mtd_name, (outcome, timing)) =>
+ let
+ fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
+ satisfied_assms = s, positive_concl_tests = p}) =
+ "errors: " ^ string_of_int e ^ "; conclusion tests: " ^ string_of_int p
+ fun string_of_reports NONE = ""
+ | string_of_reports (SOME reports) =
+ cat_lines (map (fn (size, [report]) =>
+ "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))
+ fun string_of_mtd_result (mtd_name, (outcome, (timing, reports))) =
mtd_name ^ ": " ^ string_of_outcome outcome ^ "; " ^
- space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing)) results)
+ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing)
+ ^ "\n" ^ string_of_reports reports
+ in
+ "mutant of " ^ thm_name ^ ":\n" ^ cat_lines (map string_of_mtd_result results)
+ end
fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Feb 25 22:46:52 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Feb 26 09:49:00 2010 +0100
@@ -151,7 +151,7 @@
skip_proof = chk "skip_proof",
function_flattening = not (chk "no_function_flattening"),
fail_safe_function_flattening = false,
- no_topmost_reordering = false,
+ no_topmost_reordering = (chk "no_topmost_reordering"),
no_higher_order_predicate = [],
inductify = chk "inductify",
compilation = compilation
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Feb 25 22:46:52 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Feb 26 09:49:00 2010 +0100
@@ -556,7 +556,8 @@
}
val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
- "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening"]
+ "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
+ "no_topmost_reordering"]
val compilation_names = [("pred", Pred),
(*("random", Random), ("depth_limited", Depth_Limited), ("annotated", Annotated),*)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Feb 25 22:46:52 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Feb 26 09:49:00 2010 +0100
@@ -10,7 +10,8 @@
val test_ref :
((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref
val tracing : bool Unsynchronized.ref;
- val quickcheck_compile_term : bool -> bool -> Proof.context -> term -> int -> term list option
+ val quickcheck_compile_term : bool -> bool ->
+ Proof.context -> bool -> term -> int -> term list option * (bool list * bool);
(* val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
val quiet : bool Unsynchronized.ref;
val nrandom : int Unsynchronized.ref;
@@ -216,7 +217,7 @@
fun try' j =
if j <= i then
let
- val _ = priority ("Executing depth " ^ string_of_int j)
+ val _ = if quiet then () else priority ("Executing depth " ^ string_of_int j)
in
case f j handle Match => (if quiet then ()
else warning "Exception Match raised during quickcheck"; NONE)
@@ -230,11 +231,12 @@
(* quickcheck interface functions *)
-fun compile_term' options ctxt t =
+fun compile_term' options ctxt report t =
let
val c = compile_term options ctxt t
+ val dummy_report = ([], false)
in
- (fn size => try_upto (!quiet) (c size (!nrandom)) (!depth))
+ fn size => (try_upto (!quiet) (c size (!nrandom)) (!depth), dummy_report)
end
fun quickcheck_compile_term function_flattening fail_safe_function_flattening ctxt t =
--- a/src/HOL/Tools/inductive_codegen.ML Thu Feb 25 22:46:52 2010 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Feb 26 09:49:00 2010 +0100
@@ -8,7 +8,8 @@
sig
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
+ val test_term:
+ Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
val setup : theory -> theory
val quickcheck_setup : theory -> theory
end;
@@ -809,7 +810,7 @@
Config.declare false "ind_quickcheck_size_offset" (Config.Int 0);
val size_offset = Config.int size_offset_value;
-fun test_term ctxt t =
+fun test_term ctxt report t =
let
val thy = ProofContext.theory_of ctxt;
val (xs, p) = strip_abs t;
@@ -852,9 +853,10 @@
val start = Config.get ctxt depth_start;
val offset = Config.get ctxt size_offset;
val test_fn' = !test_fn;
- fun test k = deepen bound (fn i =>
+ val dummy_report = ([], false)
+ fun test k = (deepen bound (fn i =>
(priority ("Search depth: " ^ string_of_int i);
- test_fn' (i, values, k+offset))) start;
+ test_fn' (i, values, k+offset))) start, dummy_report);
in test end;
val quickcheck_setup =
--- a/src/HOL/Tools/quickcheck_generators.ML Thu Feb 25 22:46:52 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML Fri Feb 26 09:49:00 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/Pure/codegen.ML Thu Feb 25 22:46:52 2010 +0100
+++ b/src/Pure/codegen.ML Fri Feb 26 09:49:00 2010 +0100
@@ -76,7 +76,7 @@
val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
val test_fn: (int -> term list option) Unsynchronized.ref
- val test_term: Proof.context -> term -> int -> term list option
+ val test_term: Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
val eval_result: (unit -> term) Unsynchronized.ref
val eval_term: theory -> term -> term
val evaluation_conv: cterm -> thm
@@ -871,7 +871,7 @@
val test_fn : (int -> term list option) Unsynchronized.ref =
Unsynchronized.ref (fn _ => NONE);
-fun test_term ctxt t =
+fun test_term ctxt report t =
let
val thy = ProofContext.theory_of ctxt;
val (code, gr) = setmp_CRITICAL mode ["term_of", "test"]
@@ -897,7 +897,8 @@
str ");"]) ^
"\n\nend;\n";
val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
- in ! test_fn end;
+ val dummy_report = ([], false)
+ in (fn size => (! test_fn size, dummy_report)) end;
--- a/src/Tools/quickcheck.ML Thu Feb 25 22:46:52 2010 +0100
+++ b/src/Tools/quickcheck.ML Fri Feb 26 09:49:00 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) option)
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, quiet : 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, quiet }) =
+ ((size, iterations), ((default_type, no_assms), (report, quiet)));
+fun make_test_params ((size, iterations), ((default_type, no_assms), (report, quiet))) =
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, quiet = quiet };
+fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, report, quiet }) =
+ make_test_params (f ((size, iterations), ((default_type, no_assms), (report, quiet))));
fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
- no_assms = no_assms1 },
+ no_assms = no_assms1, report = report1, quiet = quiet1 },
Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
- no_assms = no_assms2 }) =
+ no_assms = no_assms2, report = report2, quiet = quiet2 }) =
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, quiet1 orelse quiet2)));
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, quiet = 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], if report then SOME reports else NONE))
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,33 @@
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 (SOME 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))
+ | pretty_reports ctxt NONE = Pretty.str ""
+
+fun pretty_counterex_and_reports ctxt (cex, (timing, reports)) =
+ Pretty.chunks [pretty_counterex ctxt cex, pretty_reports ctxt reports]
(* automatic testing *)
@@ -182,15 +245,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, quiet } =
(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,9 +275,13 @@
| 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 apsnd o K) (read_bool arg)
+ (apsnd o apfst o apsnd o K) (read_bool arg)
+ | parse_test_param ctxt ("report", arg) =
+ (apsnd o apsnd o apfst o K) (read_bool arg)
+ | parse_test_param ctxt ("quiet", arg) =
+ (apsnd o apsnd o apsnd o K) (read_bool arg)
| parse_test_param ctxt (name, _) =
error ("Unknown test parameter: " ^ name);
@@ -235,22 +302,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, quiet))), (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 quiet 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