src/Tools/quickcheck.ML
changeset 35380 6ac5b81a763d
parent 35379 d0c779d012dc
child 35625 9c818cab0dd0
     1.1 --- a/src/Tools/quickcheck.ML	Thu Feb 25 10:04:50 2010 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Thu Feb 25 14:01:34 2010 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4      { iterations : int, raised_match_errors : int,
     1.5        satisfied_assms : int list, positive_concl_tests : int }
     1.6    val gen_test_term: Proof.context -> bool -> bool -> string option -> int -> int -> term ->
     1.7 -    ((string * term) list option * ((string * int) list * (int * report list) list))
     1.8 +    (string * term) list option * ((string * int) list * ((int * report list) list) option)
     1.9    val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
    1.10      (string * term) list option
    1.11    val add_generator:
    1.12 @@ -167,7 +167,7 @@
    1.13           (fn result => case result of NONE => NONE
    1.14          | SOME ts => SOME (names ~~ ts)) (with_size 1 []))
    1.15    in
    1.16 -    (result, ([exec_time, comp_time], reports))
    1.17 +    (result, ([exec_time, comp_time], if report then SOME reports else NONE))
    1.18    end;
    1.19  
    1.20  fun test_term ctxt quiet generator_name size i t =
    1.21 @@ -226,11 +226,12 @@
    1.22      Pretty.chunks (Pretty.str (string_of_int (i + 1) ^ ". generator:\n") :: pretty_report report))
    1.23      reports
    1.24  
    1.25 -fun pretty_reports ctxt reports =
    1.26 +fun pretty_reports ctxt (SOME reports) =
    1.27    Pretty.chunks (Pretty.str "Quickcheck report:" ::
    1.28      maps (fn (size, reports) =>
    1.29        Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_reports' reports @ [Pretty.brk 1])
    1.30        (rev reports))
    1.31 +  | pretty_reports ctxt NONE = Pretty.str ""
    1.32  
    1.33  fun pretty_counterex_and_reports ctxt (cex, (timing, reports)) =
    1.34    Pretty.chunks [pretty_counterex ctxt cex, pretty_reports ctxt reports]