# HG changeset patch
# User bulwahn
# Date 1284045783 -7200
# Node ID 0c47d615a69bcc6cf4a25bae0e968dbfbc91dbea
# Parent  8f176e575a49ba46c22e54d55565ab53a902c56f
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context

diff -r 8f176e575a49 -r 0c47d615a69b src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Sep 09 16:43:57 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Sep 09 17:23:03 2010 +0200
@@ -96,7 +96,7 @@
 fun invoke_quickcheck quickcheck_generator thy t =
   TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit))
       (fn _ =>
-          case Quickcheck.gen_test_term (ProofContext.init_global thy) true true (SOME quickcheck_generator)
+          case Quickcheck.gen_test_term (ProofContext.init_global thy) true (SOME quickcheck_generator)
                                     size iterations (preprocess thy [] t) of
             (NONE, (time_report, report)) => (NoCex, (time_report, report))
           | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
diff -r 8f176e575a49 -r 0c47d615a69b src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Sep 09 16:43:57 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Sep 09 17:23:03 2010 +0200
@@ -17,7 +17,7 @@
   val tracing : bool Unsynchronized.ref;
   val quiet : bool Unsynchronized.ref;
   val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
-    Proof.context -> bool -> term -> int -> term list option * (bool list * bool);
+    Proof.context -> term -> int -> term list option * (bool list * bool);
 (*  val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
   val nrandom : int Unsynchronized.ref;
   val debug : bool Unsynchronized.ref;
@@ -310,7 +310,7 @@
 
 (* quickcheck interface functions *)
 
-fun compile_term' compilation options depth ctxt report t =
+fun compile_term' compilation options depth ctxt t =
   let
     val c = compile_term compilation options ctxt t
     val dummy_report = ([], false)
diff -r 8f176e575a49 -r 0c47d615a69b src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Sep 09 16:43:57 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Sep 09 17:23:03 2010 +0200
@@ -9,7 +9,7 @@
   val add : string option -> int option -> attribute
   val test_fn : (int * int * int -> term list option) Unsynchronized.ref
   val test_term:
-    Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
+    Proof.context -> term -> int -> term list option * (bool list * bool)
   val setup : theory -> theory
   val quickcheck_setup : theory -> theory
 end;
@@ -799,7 +799,7 @@
 val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5);
 val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0);
 
-fun test_term ctxt report t =
+fun test_term ctxt t =
   let
     val thy = ProofContext.theory_of ctxt;
     val (xs, p) = strip_abs t;
diff -r 8f176e575a49 -r 0c47d615a69b src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 09 16:43:57 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 09 17:23:03 2010 +0200
@@ -14,7 +14,7 @@
     -> (string * sort -> string * sort) option
   val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
   val compile_generator_expr:
-    theory -> bool -> term -> int -> term list option * (bool list * bool)
+    Proof.context -> 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
@@ -380,10 +380,11 @@
     Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
   end
 
-fun compile_generator_expr thy report t =
+fun compile_generator_expr ctxt t =
   let
     val Ts = (map snd o fst o strip_abs) t;
-  in if report then
+    val thy = ProofContext.theory_of ctxt
+  in if Quickcheck.report ctxt 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)
@@ -405,6 +406,6 @@
   Datatype.interpretation ensure_random_datatype
   #> Code_Target.extend_target (target, (Code_Eval.target, K I))
   #> Context.theory_map
-    (Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of));
+    (Quickcheck.add_generator ("code", compile_generator_expr));
 
 end;
diff -r 8f176e575a49 -r 0c47d615a69b src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Sep 09 16:43:57 2010 +0200
+++ b/src/Pure/codegen.ML	Thu Sep 09 17:23:03 2010 +0200
@@ -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 -> bool -> term -> int -> term list option * (bool list * bool)
+  val test_term: Proof.context -> 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
@@ -869,7 +869,7 @@
 val test_fn : (int -> term list option) Unsynchronized.ref =
   Unsynchronized.ref (fn _ => NONE);
 
-fun test_term ctxt report t =
+fun test_term ctxt t =
   let
     val thy = ProofContext.theory_of ctxt;
     val (code, gr) = setmp_CRITICAL mode ["term_of", "test"]
diff -r 8f176e575a49 -r 0c47d615a69b src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Sep 09 16:43:57 2010 +0200
+++ b/src/Tools/quickcheck.ML	Thu Sep 09 17:23:03 2010 +0200
@@ -18,11 +18,13 @@
   { size: int, iterations: int, default_type: typ list, no_assms: bool,
     expect : expectation, report: bool, quiet : bool};
   val test_params_of: Proof.context -> test_params 
+  val report : Proof.context -> bool
+  val set_reporting : bool -> Proof.context -> Proof.context
   val add_generator:
-    string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))
+    string * (Proof.context -> term -> int -> term list option * (bool list * bool))
       -> Context.generic -> Context.generic
   (* testing terms and proof states *)
-  val gen_test_term: Proof.context -> bool -> bool -> string option -> int -> int -> term ->
+  val gen_test_term: Proof.context -> 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
@@ -102,7 +104,7 @@
 structure Data = Generic_Data
 (
   type T =
-    (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
+    (string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list
       * test_params;
   val empty = ([], Test_Params
     { size = 10, iterations = 100, default_type = [], no_assms = false,
@@ -115,6 +117,13 @@
 
 val test_params_of = snd o Data.get o Context.Proof;
 
+val report = snd o fst o snd o snd o dest_test_params o test_params_of
+
+fun map_report f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
+  make_test_params ((size, iterations), ((default_type, no_assms), ((expect, f report), quiet)));
+
+fun set_reporting report = Context.proof_map (Data.map (apsnd (map_report (K report))))
+
 val add_generator = Data.map o apfst o AList.update (op =);
 
 (* generating tests *)
@@ -124,14 +133,14 @@
    of NONE => error ("No such quickcheck generator: " ^ name)
     | SOME generator => generator ctxt;
 
-fun mk_testers ctxt report t =
+fun mk_testers ctxt t =
   (map snd o fst o Data.get o Context.Proof) ctxt
-  |> map_filter (fn generator => try (generator ctxt report) t);
+  |> map_filter (fn generator => try (generator ctxt) t);
 
-fun mk_testers_strict ctxt report t =
+fun mk_testers_strict ctxt t =
   let
     val generators = ((map snd o fst o Data.get  o Context.Proof) ctxt)
-    val testers = map (fn generator => Exn.capture (generator ctxt report) t) generators;
+    val testers = map (fn generator => Exn.capture (generator ctxt) 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
@@ -156,13 +165,13 @@
     val time = Time.toMilliseconds (#cpu (end_timing start))
   in (Exn.release result, (description, time)) end
 
-fun gen_test_term ctxt quiet report generator_name size i t =
+fun gen_test_term ctxt quiet 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 report t' else mk_testers_strict ctxt report t'
-        | SOME name => [mk_tester_select name ctxt report t']));
+       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 report = (NONE, report)
       | iterate f j report =
         let
@@ -190,11 +199,13 @@
          (fn result => case result of NONE => NONE
         | SOME ts => SOME (names ~~ ts)) (with_size 1 []))
   in
-    (result, ([exec_time, comp_time], if report then SOME reports else NONE))
+    (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
   end;
 
 fun test_term ctxt quiet generator_name size i t =
-  fst (gen_test_term ctxt quiet false generator_name size i t)
+  ctxt
+  |> set_reporting false
+  |> (fn ctxt' => fst (gen_test_term ctxt' quiet generator_name size i t))
 
 exception WELLSORTED of string
 
@@ -216,7 +227,7 @@
 
 datatype wellsorted_error = Wellsorted_Error of string | Term of term
 
-fun test_goal quiet report generator_name size iterations default_Ts no_assms insts i state =
+fun test_goal quiet generator_name size iterations default_Ts no_assms insts i state =
   let
     val lthy = Proof.context_of state;
     val thy = Proof.theory_of state;
@@ -249,7 +260,7 @@
         case f t of
           (SOME res, report) => (SOME res, rev (report :: reports))
         | (NONE, report) => collect_results f (report :: reports) ts
-  in collect_results (gen_test_term lthy quiet report generator_name size iterations) [] correct_inst_goals end;
+  in collect_results (gen_test_term lthy quiet generator_name size iterations) [] correct_inst_goals end;
 
 (* pretty printing *)
 
@@ -298,7 +309,9 @@
       val Test_Params {size, iterations, default_type, no_assms, ...} =
         (snd o Data.get o Context.Proof) ctxt;
       val res =
-        try (test_goal true false NONE size iterations default_type no_assms [] 1) state;
+        state
+        |> Proof.map_context (set_reporting false)
+        |> try (test_goal true NONE size iterations default_type no_assms [] 1);
     in
       case res of
         NONE => (false, state)
@@ -368,7 +381,9 @@
     val (((size, iterations), ((default_type, no_assms), ((expect, report), quiet))), (generator_name, insts)) =
       f (default_params, (NONE, []));
   in
-    test_goal quiet report generator_name size iterations default_type no_assms insts i state
+    state
+    |> Proof.map_context (set_reporting report)
+    |> test_goal quiet generator_name size iterations default_type no_assms insts i
     |> tap (fn (SOME x, _) => if expect = No_Counterexample then
                  error ("quickcheck expected to find no counterexample but found one") else ()
              | (NONE, _) => if expect = Counterexample then