--- 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 *)
--- 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
--- 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
--- 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