# HG changeset patch
# User bulwahn
# Date 1267187383 -3600
# Node ID f5fa7c72937edbf0f4dc85861f096120b70d4229
# Parent  598ee3a4c1aae70cb2f48364b91506b5240b80b6# Parent  d84eec57969577c2f3c1a9e0e836e44af70bcd39
merged

diff -r d84eec579695 -r f5fa7c72937e src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Feb 26 10:57:35 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Feb 26 13:29:43 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]") ^ ": " ^
diff -r d84eec579695 -r f5fa7c72937e src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Feb 26 10:57:35 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Feb 26 13:29:43 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
diff -r d84eec579695 -r f5fa7c72937e src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Feb 26 10:57:35 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Feb 26 13:29:43 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),*)
diff -r d84eec579695 -r f5fa7c72937e src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Feb 26 10:57:35 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Feb 26 13:29:43 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 =
diff -r d84eec579695 -r f5fa7c72937e src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Fri Feb 26 10:57:35 2010 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Fri Feb 26 13:29:43 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 =
diff -r d84eec579695 -r f5fa7c72937e src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Fri Feb 26 10:57:35 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Feb 26 13:29:43 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 **)
diff -r d84eec579695 -r f5fa7c72937e src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Feb 26 10:57:35 2010 +0100
+++ b/src/Pure/codegen.ML	Fri Feb 26 13:29:43 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;
 
 
 
diff -r d84eec579695 -r f5fa7c72937e src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Feb 26 10:57:35 2010 +0100
+++ b/src/Tools/quickcheck.ML	Fri Feb 26 13:29:43 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