src/HOL/Mutabelle/mutabelle_extra.ML

 val take_random : int -> 'a list -> 'a list
 
 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
 type timing = (string * int) list
 
-type mtd = string * (theory -> term -> outcome * timing)
-
-type mutant_subentry = term * (string * (outcome * timing)) list
+type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
+
+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
 type entry = string * bool * subentry list
 type report = entry list

 val max_mutants = 1
 val num_mutations = 0
 
 (* quickcheck options *)
 (*val quickcheck_generator = "SML"*)
-val iterations = 1
+val iterations = 100
 val size = 5
 
 exception RANDOM;
 
 fun rmod x y = x - y * Real.realFloor (x / y);

   else l + Real.floor (rmod (random ()) (real (h - l + 1)));
 
 datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
 type timing = (string * int) list
 
-type mtd = string * (theory -> term -> outcome * timing)
-
-type mutant_subentry = term * (string * (outcome * timing)) list
+type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
+
+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
 type entry = string * bool * subentry list
 type report = entry list

  (map_types (inst_type insts) (Mutabelle.freeze t));
 
 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)
 
   (*

   in (Exn.release result, (description, time)) end
 
 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 *)
 (*
 fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
   let

   space_implode "; "
     (map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
   "\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]") ^ ": " ^
    Syntax.string_of_term_global thy t ^ "\n" ^
    cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"