# HG changeset patch
# User bulwahn
# Date 1322774075 -3600
# Node ID 123e3a9a3bb3b5b6baf326e8e1106d8b779cd692
# Parent  5e46c225370e5ee02c66e3fc8d03088c09e68383
compilations return genuine flag to quickcheck framework

diff -r 5e46c225370e -r 123e3a9a3bb3 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -489,8 +489,7 @@
       thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
   end;
 
-val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive",
-  apfst (Option.map snd) ooo compile_generator_expr);
+val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive", compile_generator_expr);
   
 (* setup *)
 
diff -r 5e46c225370e -r 123e3a9a3bb3 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -437,7 +437,7 @@
           thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t)
       in
         Quickcheck.Result
-         {counterexample = Option.map (mk_terms ctxt qs) counterexample,
+         {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
           evaluation_terms = Option.map (K []) counterexample,
           timings = #timings (dest_result result), reports = #reports (dest_result result)}
       end
@@ -454,7 +454,7 @@
       in
         Quickcheck.Result
          {counterexample =
-           Option.map (((curry (op ~~)) (Term.add_free_names t [])) o map post_process o snd) counterexample,
+           Option.map (apsnd (((curry (op ~~)) (Term.add_free_names t [])) o map post_process)) counterexample,
           evaluation_terms = Option.map (K []) counterexample,
           timings = #timings (dest_result result), reports = #reports (dest_result result)}
       end
diff -r 5e46c225370e -r 123e3a9a3bb3 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -17,7 +17,7 @@
   val mk_safe_if : Proof.context -> term * term * (bool -> term) -> term
   val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
   type compile_generator =
-    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
+    Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
   val generator_test_goal_terms :
     string * compile_generator -> Proof.context -> bool -> (string * typ) list
     -> (term * term list) list -> Quickcheck.result list
@@ -53,7 +53,7 @@
 (* testing functions: testing with increasing sizes (and cardinalities) *)
 
 type compile_generator =
-  Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
+  Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
 
 fun check_test_term t =
   let
diff -r 5e46c225370e -r 123e3a9a3bb3 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -11,7 +11,7 @@
     -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     -> seed -> (('a -> 'b) * (unit -> term)) * seed
   val compile_generator_expr:
-    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
+    Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
   val put_counterexample: (unit -> int -> int -> seed -> (bool * term list) option * seed)
     -> Proof.context -> Proof.context
   val put_counterexample_report: (unit -> int -> int -> seed -> (term list option * (bool list * bool)) * seed)
@@ -417,7 +417,7 @@
               val report = collect_single_report single_report report
             in
               case test_result of NONE => iterate_and_collect (card, size) (j - 1) report
-                | SOME q => (SOME q, report)
+                | SOME q => (SOME (true, q), report)
             end
       in
         fn [card, size] => apsnd SOME (iterate_and_collect (card, size) iterations empty_report)
@@ -429,7 +429,7 @@
           (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
           thy (SOME target)
           (fn proc => fn g => fn c => fn s =>g c s #>> (Option.map o apsnd o map) proc) t' [];
-        fun single_tester c s = compile c s |> Random_Engine.run |> Option.map snd
+        fun single_tester c s = compile c s |> Random_Engine.run
         fun iterate (card, size) 0 = NONE
           | iterate (card, size) j =
             case single_tester card size of NONE => iterate (card, size) (j - 1) | SOME q => SOME q