added basic reporting of test cases to quickcheck
authorbulwahn
Thu Feb 25 09:28:01 2010 +0100 (2010-02-25)
changeset 3537895d0e3adf38e
parent 35327 c76b7dcd77ce
child 35379 d0c779d012dc
added basic reporting of test cases to quickcheck
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/quickcheck_generators.ML
src/Pure/codegen.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Feb 23 16:58:21 2010 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Feb 25 09:28:01 2010 +0100
     1.3 @@ -10,7 +10,8 @@
     1.4    val test_ref :
     1.5      ((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref
     1.6    val tracing : bool Unsynchronized.ref;
     1.7 -  val quickcheck_compile_term : bool -> bool -> Proof.context -> term -> int -> term list option
     1.8 +  val quickcheck_compile_term : bool -> bool -> 
     1.9 +    Proof.context -> bool -> term -> int -> term list option * (bool list * bool);
    1.10  (*  val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
    1.11    val quiet : bool Unsynchronized.ref;
    1.12    val nrandom : int Unsynchronized.ref;
    1.13 @@ -230,11 +231,12 @@
    1.14  
    1.15  (* quickcheck interface functions *)
    1.16  
    1.17 -fun compile_term' options ctxt t =
    1.18 +fun compile_term' options ctxt report t =
    1.19    let
    1.20      val c = compile_term options ctxt t
    1.21 +    val dummy_report = ([], false)
    1.22    in
    1.23 -    (fn size => try_upto (!quiet) (c size (!nrandom)) (!depth))
    1.24 +    fn size => (try_upto (!quiet) (c size (!nrandom)) (!depth), dummy_report)
    1.25    end
    1.26  
    1.27  fun quickcheck_compile_term function_flattening fail_safe_function_flattening ctxt t =
     2.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Feb 23 16:58:21 2010 +0100
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Feb 25 09:28:01 2010 +0100
     2.3 @@ -8,7 +8,8 @@
     2.4  sig
     2.5    val add : string option -> int option -> attribute
     2.6    val test_fn : (int * int * int -> term list option) Unsynchronized.ref
     2.7 -  val test_term: Proof.context -> term -> int -> term list option
     2.8 +  val test_term:
     2.9 +    Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
    2.10    val setup : theory -> theory
    2.11    val quickcheck_setup : theory -> theory
    2.12  end;
    2.13 @@ -805,7 +806,7 @@
    2.14    Config.declare false "ind_quickcheck_size_offset" (Config.Int 0);
    2.15  val size_offset = Config.int size_offset_value;
    2.16  
    2.17 -fun test_term ctxt t =
    2.18 +fun test_term ctxt report t =
    2.19    let
    2.20      val thy = ProofContext.theory_of ctxt;
    2.21      val (xs, p) = strip_abs t;
    2.22 @@ -848,9 +849,10 @@
    2.23      val start = Config.get ctxt depth_start;
    2.24      val offset = Config.get ctxt size_offset;
    2.25      val test_fn' = !test_fn;
    2.26 -    fun test k = deepen bound (fn i =>
    2.27 +    val dummy_report = ([], false)
    2.28 +    fun test k = (deepen bound (fn i =>
    2.29        (priority ("Search depth: " ^ string_of_int i);
    2.30 -       test_fn' (i, values, k+offset))) start;
    2.31 +       test_fn' (i, values, k+offset))) start, dummy_report);
    2.32    in test end;
    2.33  
    2.34  val quickcheck_setup =
     3.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Tue Feb 23 16:58:21 2010 +0100
     3.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Feb 25 09:28:01 2010 +0100
     3.3 @@ -15,8 +15,11 @@
     3.4      -> string list -> string list * string list -> typ list * typ list
     3.5      -> term list * (term * term) list
     3.6    val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
     3.7 -  val compile_generator_expr: theory -> term -> int -> term list option
     3.8 +  val compile_generator_expr:
     3.9 +    theory -> bool -> term -> int -> term list option * (bool list * bool)
    3.10    val eval_ref: (unit -> int -> seed -> term list option * seed) option Unsynchronized.ref
    3.11 +  val eval_report_ref:
    3.12 +    (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref
    3.13    val setup: theory -> theory
    3.14  end;
    3.15  
    3.16 @@ -350,6 +353,10 @@
    3.17      (unit -> int -> int * int -> term list option * (int * int)) option Unsynchronized.ref =
    3.18    Unsynchronized.ref NONE;
    3.19  
    3.20 +val eval_report_ref :
    3.21 +    (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref =
    3.22 +  Unsynchronized.ref NONE;
    3.23 +
    3.24  val target = "Quickcheck";
    3.25  
    3.26  fun mk_generator_expr thy prop Ts =
    3.27 @@ -360,7 +367,7 @@
    3.28      val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
    3.29      val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
    3.30      val check = @{term "If :: bool => term list option => term list option => term list option"}
    3.31 -      $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option "} $ terms);
    3.32 +      $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms);
    3.33      val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"};
    3.34      fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    3.35      fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
    3.36 @@ -375,13 +382,69 @@
    3.37        (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
    3.38    in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
    3.39  
    3.40 -fun compile_generator_expr thy t =
    3.41 +fun mk_reporting_generator_expr thy prop Ts =
    3.42 +  let
    3.43 +    val bound_max = length Ts - 1;
    3.44 +    val bounds = map_index (fn (i, ty) =>
    3.45 +      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
    3.46 +    fun strip_imp (Const("op -->",_) $ A $ B) = apfst (cons A) (strip_imp B)
    3.47 +      | strip_imp A = ([], A)
    3.48 +    val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
    3.49 +    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
    3.50 +    val (assms, concl) = strip_imp prop'
    3.51 +    val return =
    3.52 +      @{term "Pair :: term list option * (bool list * bool) => Random.seed => (term list option * (bool list * bool)) * Random.seed"};
    3.53 +    fun mk_assms_report i =
    3.54 +      HOLogic.mk_prod (@{term "None :: term list option"},
    3.55 +        HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"}
    3.56 +          (replicate i @{term "True"} @ replicate (length assms - i) @{term "False"}),
    3.57 +        @{term "False"}))
    3.58 +    fun mk_concl_report b =
    3.59 +      HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"} (replicate (length assms) @{term "True"}),
    3.60 +        if b then @{term True} else @{term False})
    3.61 +    val If =
    3.62 +      @{term "If :: bool => term list option * (bool list * bool) => term list option * (bool list * bool) => term list option * (bool list * bool)"}
    3.63 +    val concl_check = If $ concl $
    3.64 +      HOLogic.mk_prod (@{term "None :: term list option"}, mk_concl_report true) $
    3.65 +      HOLogic.mk_prod (@{term "Some :: term list  => term list option"} $ terms, mk_concl_report false)
    3.66 +    val check = fold_rev (fn (i, assm) => fn t => If $ assm $ t $ mk_assms_report i)
    3.67 +      (map_index I assms) concl_check
    3.68 +    fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    3.69 +    fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
    3.70 +    fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
    3.71 +      liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    3.72 +    fun mk_split T = Sign.mk_const thy
    3.73 +      (@{const_name split}, [T, @{typ "unit => term"},
    3.74 +        liftT @{typ "term list option * (bool list * bool)"} @{typ Random.seed}]);
    3.75 +    fun mk_scomp_split T t t' =
    3.76 +      mk_scomp (mk_termtyp T) @{typ "term list option * (bool list * bool)"} @{typ Random.seed} t
    3.77 +        (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
    3.78 +    fun mk_bindclause (_, _, i, T) = mk_scomp_split T
    3.79 +      (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
    3.80 +  in
    3.81 +    Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
    3.82 +  end
    3.83 +
    3.84 +fun compile_generator_expr thy report t =
    3.85    let
    3.86      val Ts = (map snd o fst o strip_abs) t;
    3.87 -    val t' = mk_generator_expr thy t Ts;
    3.88 -    val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
    3.89 -      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
    3.90 -  in compile #> Random_Engine.run end;
    3.91 +  in
    3.92 +    if report then
    3.93 +      let
    3.94 +        val t' = mk_reporting_generator_expr thy t Ts;
    3.95 +        val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref)
    3.96 +          (fn proc => fn g => fn s => g s #>> ((apfst o Option.map o map) proc)) thy t' [];
    3.97 +      in
    3.98 +        compile #> Random_Engine.run
    3.99 +      end
   3.100 +    else
   3.101 +      let
   3.102 +        val t' = mk_generator_expr thy t Ts;
   3.103 +        val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
   3.104 +          (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
   3.105 +        val dummy_report = ([], false)
   3.106 +      in fn s => ((compile #> Random_Engine.run) s, dummy_report) end
   3.107 +  end;
   3.108  
   3.109  
   3.110  (** setup **)
     4.1 --- a/src/Pure/codegen.ML	Tue Feb 23 16:58:21 2010 +0100
     4.2 +++ b/src/Pure/codegen.ML	Thu Feb 25 09:28:01 2010 +0100
     4.3 @@ -76,7 +76,7 @@
     4.4    val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
     4.5    val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
     4.6    val test_fn: (int -> term list option) Unsynchronized.ref
     4.7 -  val test_term: Proof.context -> term -> int -> term list option
     4.8 +  val test_term: Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
     4.9    val eval_result: (unit -> term) Unsynchronized.ref
    4.10    val eval_term: theory -> term -> term
    4.11    val evaluation_conv: cterm -> thm
    4.12 @@ -871,7 +871,7 @@
    4.13  val test_fn : (int -> term list option) Unsynchronized.ref =
    4.14    Unsynchronized.ref (fn _ => NONE);
    4.15  
    4.16 -fun test_term ctxt t =
    4.17 +fun test_term ctxt report t =
    4.18    let
    4.19      val thy = ProofContext.theory_of ctxt;
    4.20      val (code, gr) = setmp_CRITICAL mode ["term_of", "test"]
    4.21 @@ -897,7 +897,8 @@
    4.22            str ");"]) ^
    4.23        "\n\nend;\n";
    4.24      val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
    4.25 -  in ! test_fn end;
    4.26 +    val dummy_report = ([], false)
    4.27 +  in (fn size => (! test_fn size, dummy_report)) end;
    4.28  
    4.29  
    4.30  
     5.1 --- a/src/Tools/quickcheck.ML	Tue Feb 23 16:58:21 2010 +0100
     5.2 +++ b/src/Tools/quickcheck.ML	Thu Feb 25 09:28:01 2010 +0100
     5.3 @@ -8,11 +8,16 @@
     5.4  sig
     5.5    val auto: bool Unsynchronized.ref
     5.6    val timing : bool Unsynchronized.ref
     5.7 +  datatype report = Report of
     5.8 +    { iterations : int, raised_match_errors : int,
     5.9 +      satisfied_assms : int list, positive_concl_tests : int }
    5.10 +  val gen_test_term: Proof.context -> bool -> bool -> string option -> int -> int -> term ->
    5.11 +    ((string * term) list option * ((string * int) list * (int * report list) list))
    5.12    val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
    5.13      (string * term) list option
    5.14 -  val timed_test_term: Proof.context -> bool -> string option -> int -> int -> term ->
    5.15 -    ((string * term) list option * (string * int) list)
    5.16 -  val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
    5.17 +  val add_generator:
    5.18 +    string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))
    5.19 +      -> theory -> theory
    5.20    val setup: theory -> theory
    5.21    val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
    5.22  end;
    5.23 @@ -33,31 +38,54 @@
    5.24        "auto-quickcheck"
    5.25        "Whether to run Quickcheck automatically.") ());
    5.26  
    5.27 +(* quickcheck report *)
    5.28 +
    5.29 +datatype single_report = Run of bool list * bool | MatchExc
    5.30 +
    5.31 +datatype report = Report of
    5.32 +  { iterations : int, raised_match_errors : int,
    5.33 +    satisfied_assms : int list, positive_concl_tests : int }
    5.34 +
    5.35 +fun collect_single_report single_report
    5.36 +    (Report {iterations = iterations, raised_match_errors = raised_match_errors,
    5.37 +    satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
    5.38 +  case single_report
    5.39 +  of MatchExc =>
    5.40 +    Report {iterations = iterations + 1, raised_match_errors = raised_match_errors + 1,
    5.41 +      satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}
    5.42 +   | Run (assms, concl) =>
    5.43 +    Report {iterations = iterations + 1, raised_match_errors = raised_match_errors,
    5.44 +      satisfied_assms =
    5.45 +        map2 (fn b => fn s => if b then s + 1 else s) assms
    5.46 +         (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
    5.47 +      positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
    5.48  
    5.49  (* quickcheck configuration -- default parameters, test generators *)
    5.50  
    5.51  datatype test_params = Test_Params of
    5.52 -  { size: int, iterations: int, default_type: typ option, no_assms: bool };
    5.53 +  { size: int, iterations: int, default_type: typ option, no_assms: bool, report: bool};
    5.54  
    5.55 -fun dest_test_params (Test_Params { size, iterations, default_type, no_assms }) =
    5.56 -  ((size, iterations), (default_type, no_assms));
    5.57 -fun make_test_params ((size, iterations), (default_type, no_assms)) =
    5.58 +fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, report }) =
    5.59 +  ((size, iterations), ((default_type, no_assms), report));
    5.60 +fun make_test_params ((size, iterations), ((default_type, no_assms), report)) =
    5.61    Test_Params { size = size, iterations = iterations, default_type = default_type,
    5.62 -                no_assms = no_assms };
    5.63 -fun map_test_params f (Test_Params { size, iterations, default_type, no_assms }) =
    5.64 -  make_test_params (f ((size, iterations), (default_type, no_assms)));
    5.65 +                no_assms = no_assms, report = report };
    5.66 +fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, report }) =
    5.67 +  make_test_params (f ((size, iterations), ((default_type, no_assms), report)));
    5.68  fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
    5.69 -                                     no_assms = no_assms1 },
    5.70 +                                     no_assms = no_assms1, report = report1 },
    5.71    Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
    5.72 -                no_assms = no_assms2 }) =
    5.73 +                no_assms = no_assms2, report = report2 }) =
    5.74    make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
    5.75 -    (case default_type1 of NONE => default_type2 | _ => default_type1, no_assms1 orelse no_assms2));
    5.76 +    ((case default_type1 of NONE => default_type2 | _ => default_type1, no_assms1 orelse no_assms2),
    5.77 +    report1 orelse report2));
    5.78  
    5.79  structure Data = Theory_Data
    5.80  (
    5.81 -  type T = (string * (Proof.context -> term -> int -> term list option)) list
    5.82 +  type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
    5.83      * test_params;
    5.84 -  val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE, no_assms = false });
    5.85 +  val empty = ([], Test_Params
    5.86 +    { size = 10, iterations = 100, default_type = NONE, no_assms = false, report = false});
    5.87    val extend = I;
    5.88    fun merge ((generators1, params1), (generators2, params2)) : T =
    5.89      (AList.merge (op =) (K true) (generators1, generators2),
    5.90 @@ -66,7 +94,6 @@
    5.91  
    5.92  val add_generator = Data.map o apfst o AList.update (op =);
    5.93  
    5.94 -
    5.95  (* generating tests *)
    5.96  
    5.97  fun mk_tester_select name ctxt =
    5.98 @@ -74,14 +101,14 @@
    5.99     of NONE => error ("No such quickcheck generator: " ^ name)
   5.100      | SOME generator => generator ctxt;
   5.101  
   5.102 -fun mk_testers ctxt t =
   5.103 +fun mk_testers ctxt report t =
   5.104    (map snd o fst o Data.get o ProofContext.theory_of) ctxt
   5.105 -  |> map_filter (fn generator => try (generator ctxt) t);
   5.106 +  |> map_filter (fn generator => try (generator ctxt report) t);
   5.107  
   5.108 -fun mk_testers_strict ctxt t =
   5.109 +fun mk_testers_strict ctxt report t =
   5.110    let
   5.111      val generators = ((map snd o fst o Data.get o ProofContext.theory_of) ctxt)
   5.112 -    val testers = map (fn generator => Exn.capture (generator ctxt) t) generators;
   5.113 +    val testers = map (fn generator => Exn.capture (generator ctxt report) t) generators;
   5.114    in if forall (is_none o Exn.get_result) testers
   5.115      then [(Exn.release o snd o split_last) testers]
   5.116      else map_filter Exn.get_result testers
   5.117 @@ -106,36 +133,45 @@
   5.118      val time = Time.toMilliseconds (#cpu (end_timing start))
   5.119    in (Exn.release result, (description, time)) end
   5.120  
   5.121 -fun timed_test_term ctxt quiet generator_name size i t =
   5.122 +fun gen_test_term ctxt quiet report generator_name size i t =
   5.123    let
   5.124      val (names, t') = prep_test_term t;
   5.125      val (testers, comp_time) = cpu_time "quickcheck compilation"
   5.126        (fn () => (case generator_name
   5.127 -       of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
   5.128 -        | SOME name => [mk_tester_select name ctxt t']));
   5.129 -    fun iterate f 0 = NONE
   5.130 -      | iterate f j = case f () handle Match => (if quiet then ()
   5.131 -             else warning "Exception Match raised during quickcheck"; NONE)
   5.132 -          of NONE => iterate f (j - 1) | SOME q => SOME q;
   5.133 -    fun with_testers k [] = NONE
   5.134 +       of NONE => if quiet then mk_testers ctxt report t' else mk_testers_strict ctxt report t'
   5.135 +        | SOME name => [mk_tester_select name ctxt report t']));
   5.136 +    fun iterate f 0 report = (NONE, report)
   5.137 +      | iterate f j report =
   5.138 +        let
   5.139 +          val (test_result, single_report) = apsnd Run (f ()) handle Match => (if quiet then ()
   5.140 +             else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
   5.141 +          val report = collect_single_report single_report report
   5.142 +        in
   5.143 +          case test_result of NONE => iterate f (j - 1) report | SOME q => (SOME q, report)
   5.144 +        end
   5.145 +    val empty_report = Report { iterations = 0, raised_match_errors = 0,
   5.146 +      satisfied_assms = [], positive_concl_tests = 0 }
   5.147 +    fun with_testers k [] = (NONE, [])
   5.148        | with_testers k (tester :: testers) =
   5.149 -          case iterate (fn () => tester (k - 1)) i
   5.150 -           of NONE => with_testers k testers
   5.151 -            | SOME q => SOME q;
   5.152 -    fun with_size k = if k > size then NONE
   5.153 +          case iterate (fn () => tester (k - 1)) i empty_report
   5.154 +           of (NONE, report) => apsnd (cons report) (with_testers k testers)
   5.155 +            | (SOME q, report) => (SOME q, [report]);
   5.156 +    fun with_size k reports = if k > size then (NONE, reports)
   5.157        else (if quiet then () else priority ("Test data size: " ^ string_of_int k);
   5.158 -        case with_testers k testers
   5.159 -         of NONE => with_size (k + 1) | SOME q => SOME q);
   5.160 -    val (result, exec_time) = cpu_time "quickcheck execution"
   5.161 -      (fn () => case with_size 1
   5.162 -        of NONE => NONE
   5.163 -        | SOME ts => SOME (names ~~ ts))
   5.164 +        let
   5.165 +          val (result, new_report) = with_testers k testers
   5.166 +          val reports = ((k, new_report) :: reports)
   5.167 +        in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
   5.168 +    val ((result, reports), exec_time) = cpu_time "quickcheck execution"
   5.169 +      (fn () => apfst
   5.170 +         (fn result => case result of NONE => NONE
   5.171 +        | SOME ts => SOME (names ~~ ts)) (with_size 1 []))
   5.172    in
   5.173 -    (result, [exec_time, comp_time])
   5.174 +    (result, ([exec_time, comp_time], reports))
   5.175    end;
   5.176  
   5.177  fun test_term ctxt quiet generator_name size i t =
   5.178 -  fst (timed_test_term ctxt quiet generator_name size i t)
   5.179 +  fst (gen_test_term ctxt quiet false generator_name size i t)
   5.180  
   5.181  fun monomorphic_term thy insts default_T = 
   5.182    let
   5.183 @@ -152,7 +188,7 @@
   5.184        | subst T = T;
   5.185    in (map_types o map_atyps) subst end;
   5.186  
   5.187 -fun test_goal quiet generator_name size iterations default_T no_assms insts i assms state =
   5.188 +fun test_goal quiet report generator_name size iterations default_T no_assms insts i assms state =
   5.189    let
   5.190      val ctxt = Proof.context_of state;
   5.191      val thy = Proof.theory_of state;
   5.192 @@ -164,7 +200,7 @@
   5.193                                    subst_bounds (frees, strip gi))
   5.194        |> monomorphic_term thy insts default_T
   5.195        |> ObjectLogic.atomize_term thy;
   5.196 -  in test_term ctxt quiet generator_name size iterations gi' end;
   5.197 +  in gen_test_term ctxt quiet report generator_name size iterations gi' end;
   5.198  
   5.199  fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."
   5.200    | pretty_counterex ctxt (SOME cex) =
   5.201 @@ -172,6 +208,32 @@
   5.202          map (fn (s, t) =>
   5.203            Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
   5.204  
   5.205 +fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors,
   5.206 +    satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
   5.207 +  let
   5.208 +    fun pretty_stat s i = Pretty.block ([Pretty.str (s ^ ": " ^ string_of_int i)])
   5.209 +  in
   5.210 +     ([pretty_stat "iterations" iterations,
   5.211 +     pretty_stat "match exceptions" raised_match_errors]
   5.212 +     @ map_index (fn (i, n) => pretty_stat ("satisfied " ^ string_of_int (i + 1) ^ ". assumption") n)
   5.213 +       satisfied_assms
   5.214 +     @ [pretty_stat "positive conclusion tests" positive_concl_tests])
   5.215 +  end
   5.216 +
   5.217 +fun pretty_reports' [report] = [Pretty.chunks (pretty_report report)]
   5.218 +  | pretty_reports' reports =
   5.219 +  map_index (fn (i, report) =>
   5.220 +    Pretty.chunks (Pretty.str (string_of_int (i + 1) ^ ". generator:\n") :: pretty_report report))
   5.221 +    reports
   5.222 +
   5.223 +fun pretty_reports ctxt reports =
   5.224 +  Pretty.chunks (Pretty.str "Quickcheck report:" ::
   5.225 +    maps (fn (size, reports) =>
   5.226 +      Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_reports' reports @ [Pretty.brk 1])
   5.227 +      (rev reports))
   5.228 +
   5.229 +fun pretty_counterex_and_reports ctxt (cex, (timing, reports)) =
   5.230 +  Pretty.chunks [pretty_counterex ctxt cex, pretty_reports ctxt reports]
   5.231  
   5.232  (* automatic testing *)
   5.233  
   5.234 @@ -182,15 +244,15 @@
   5.235      let
   5.236        val ctxt = Proof.context_of state;
   5.237        val assms = map term_of (Assumption.all_assms_of ctxt);
   5.238 -      val Test_Params { size, iterations, default_type, no_assms } =
   5.239 +      val Test_Params { size, iterations, default_type, no_assms, report } =
   5.240          (snd o Data.get o Proof.theory_of) state;
   5.241        val res =
   5.242 -        try (test_goal true NONE size iterations default_type no_assms [] 1 assms) state;
   5.243 +        try (test_goal true false NONE size iterations default_type no_assms [] 1 assms) state;
   5.244      in
   5.245        case res of
   5.246          NONE => (false, state)
   5.247 -      | SOME NONE => (false, state)
   5.248 -      | SOME cex => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
   5.249 +      | SOME (NONE, report) => (false, state)
   5.250 +      | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
   5.251            Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state)
   5.252      end
   5.253  
   5.254 @@ -212,8 +274,10 @@
   5.255    | parse_test_param ctxt ("iterations", arg) =
   5.256        (apfst o apsnd o K) (read_nat arg)
   5.257    | parse_test_param ctxt ("default_type", arg) =
   5.258 -      (apsnd o apfst o K o SOME) (ProofContext.read_typ ctxt arg)
   5.259 +      (apsnd o apfst o apfst o K o SOME) (ProofContext.read_typ ctxt arg)
   5.260    | parse_test_param ctxt ("no_assms", arg) =
   5.261 +      (apsnd o apfst o apsnd o K) (read_bool arg)
   5.262 +  | parse_test_param ctxt ("report", arg) =
   5.263        (apsnd o apsnd o K) (read_bool arg)
   5.264    | parse_test_param ctxt (name, _) =
   5.265        error ("Unknown test parameter: " ^ name);
   5.266 @@ -235,22 +299,24 @@
   5.267      |> (Data.map o apsnd o map_test_params) f
   5.268    end;
   5.269  
   5.270 -fun quickcheck args i state =
   5.271 +fun gen_quickcheck args i state =
   5.272    let
   5.273      val thy = Proof.theory_of state;
   5.274      val ctxt = Proof.context_of state;
   5.275      val assms = map term_of (Assumption.all_assms_of ctxt);
   5.276      val default_params = (dest_test_params o snd o Data.get) thy;
   5.277      val f = fold (parse_test_param_inst ctxt) args;
   5.278 -    val (((size, iterations), (default_type, no_assms)), (generator_name, insts)) =
   5.279 +    val (((size, iterations), ((default_type, no_assms), report)), (generator_name, insts)) =
   5.280        f (default_params, (NONE, []));
   5.281    in
   5.282 -    test_goal false generator_name size iterations default_type no_assms insts i assms state
   5.283 +    test_goal false report generator_name size iterations default_type no_assms insts i assms state
   5.284    end;
   5.285  
   5.286 +fun quickcheck args i state = fst (gen_quickcheck args i state)
   5.287 +
   5.288  fun quickcheck_cmd args i state =
   5.289 -  quickcheck args i (Toplevel.proof_of state)
   5.290 -  |> Pretty.writeln o pretty_counterex (Toplevel.context_of state);
   5.291 +  gen_quickcheck args i (Toplevel.proof_of state)
   5.292 +  |> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state);
   5.293  
   5.294  local structure P = OuterParse and K = OuterKeyword in
   5.295