--- a/src/Tools/quickcheck.ML Thu Feb 25 10:04:50 2010 +0100
+++ b/src/Tools/quickcheck.ML Thu Feb 25 14:01:34 2010 +0100
@@ -12,7 +12,7 @@
{ 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))
+ (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 add_generator:
@@ -167,7 +167,7 @@
(fn result => case result of NONE => NONE
| SOME ts => SOME (names ~~ ts)) (with_size 1 []))
in
- (result, ([exec_time, comp_time], reports))
+ (result, ([exec_time, comp_time], if report then SOME reports else NONE))
end;
fun test_term ctxt quiet generator_name size i t =
@@ -226,11 +226,12 @@
Pretty.chunks (Pretty.str (string_of_int (i + 1) ^ ". generator:\n") :: pretty_report report))
reports
-fun pretty_reports ctxt 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]