--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Dec 05 12:35:04 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Dec 05 12:35:05 2011 +0100
@@ -7,10 +7,10 @@
signature EXHAUSTIVE_GENERATORS =
sig
val compile_generator_expr:
- Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
+ Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list
- val put_counterexample: (unit -> int -> int -> (bool * term list) option)
+ val put_counterexample: (unit -> int -> bool -> int -> (bool * term list) option)
-> Proof.context -> Proof.context
val put_counterexample_batch: (unit -> (int -> term list option) list)
-> Proof.context -> Proof.context
@@ -342,17 +342,19 @@
val names = Term.add_free_names t []
val frees = map Free (Term.add_frees t [])
fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
- val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+ val ([depth_name, genuine_only_name], ctxt'') =
+ Variable.variant_fixes ["depth", "genuine_only"] ctxt'
val depth = Free (depth_name, @{typ code_numeral})
+ val genuine_only = Free (genuine_only_name, @{typ bool})
val return = mk_return (HOLogic.mk_list @{typ "term"}
(map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms))
fun mk_exhaustive_closure (free as Free (_, T)) t =
Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
$ lambda free t $ depth
val none_t = Const (@{const_name "None"}, resultT)
- val mk_if = Quickcheck_Common.mk_safe_if ctxt
+ val mk_if = Quickcheck_Common.mk_safe_if genuine_only
val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
- in lambda depth (mk_test_term t) end
+ in lambda genuine_only (lambda depth (mk_test_term t)) end
fun mk_full_generator_expr ctxt (t, eval_terms) =
let
@@ -379,14 +381,15 @@
$ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
$ lambda free (lambda term_var t)) $ depth
val none_t = Const (@{const_name "None"}, resultT)
- val mk_if = Quickcheck_Common.mk_safe_if ctxt
+ val mk_if = Quickcheck_Common.mk_safe_if genuine_only
val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
in lambda genuine_only (lambda depth (mk_test_term t)) end
fun mk_parametric_generator_expr mk_generator_expr =
Quickcheck_Common.gen_mk_parametric_generator_expr
- ((mk_generator_expr, absdummy @{typ "code_numeral"} (Const (@{const_name "None"}, resultT))),
- @{typ "code_numeral"} --> resultT)
+ ((mk_generator_expr,
+ absdummy @{typ bool} (absdummy @{typ "code_numeral"} (Const (@{const_name "None"}, resultT)))),
+ @{typ bool} --> @{typ "code_numeral"} --> resultT)
fun mk_validator_expr ctxt t =
let
@@ -424,7 +427,7 @@
structure Counterexample = Proof_Data
(
- type T = unit -> int -> int -> (bool * term list) option
+ type T = unit -> int -> bool -> int -> (bool * term list) option
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Counterexample"
);
@@ -460,9 +463,10 @@
val compile = Code_Runtime.dynamic_value_strict
(Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
thy (SOME target) (fn proc => fn g =>
- fn card => fn size => g card size |> (Option.map o apsnd o map) proc) t' []
+ fn card => fn genuine_only => fn size => g card genuine_only size
+ |> (Option.map o apsnd o map) proc) t' []
in
- fn [card, size] => rpair NONE (compile card size |>
+ fn genuine_only => fn [card, size] => rpair NONE (compile card genuine_only size |>
(if Config.get ctxt quickcheck_pretty then
Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I))
end;
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 05 12:35:04 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 05 12:35:05 2011 +0100
@@ -14,10 +14,10 @@
-> (string * sort -> string * sort) option
val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
-> (typ option * (term * term list)) list list
- val mk_safe_if : Proof.context -> term * term * (bool -> term) -> term
+ val mk_safe_if : term -> 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 -> (bool * term list) option * Quickcheck.report option
+ Proof.context -> (term * term list) list -> bool -> 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 -> (bool * term list) option * Quickcheck.report option
+ Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
fun check_test_term t =
let
@@ -69,34 +69,35 @@
fun test_term (name, compile) ctxt catch_code_errors (t, eval_terms) =
let
+ val genuine_only = not (Config.get ctxt Quickcheck.potential)
val _ = check_test_term t
val names = Term.add_free_names t []
val current_size = Unsynchronized.ref 0
val current_result = Unsynchronized.ref Quickcheck.empty_result
fun excipit () =
"Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
- fun with_size test_fun k =
+ val act = if catch_code_errors then try else (fn f => SOME o f)
+ val (test_fun, comp_time) = cpu_time "quickcheck compilation"
+ (fn () => act (compile ctxt) [(t, eval_terms)]);
+ val _ = Quickcheck.add_timing comp_time current_result
+ fun with_size test_fun genuine_only k =
if k > Config.get ctxt Quickcheck.size then
NONE
else
let
val _ = Quickcheck.message ctxt
- ("[Quickcheck-" ^ name ^ "]Test data size: " ^ string_of_int k)
+ ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
val _ = current_size := k
val ((result, report), timing) =
- cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1])
+ cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1])
val _ = Quickcheck.add_timing timing current_result
val _ = Quickcheck.add_report k report current_result
in
case result of
- NONE => with_size test_fun (k + 1)
+ NONE => with_size test_fun genuine_only (k + 1)
| SOME (true, ts) => SOME (true, ts)
| SOME (false, ts) => SOME (false, ts) (* FIXME: output message & restart *)
end;
- val act = if catch_code_errors then try else (fn f => SOME o f)
- val (test_fun, comp_time) = cpu_time "quickcheck compilation"
- (fn () => act (compile ctxt) [(t, eval_terms)]);
- val _ = Quickcheck.add_timing comp_time current_result
in
case test_fun of
NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
@@ -104,7 +105,7 @@
| SOME test_fun =>
let
val (response, exec_time) =
- cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
+ cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1)
val _ = Quickcheck.add_response names eval_terms response current_result
val _ = Quickcheck.add_timing exec_time current_result
in !current_result end
@@ -150,13 +151,14 @@
fun test_term_with_cardinality (name, compile) ctxt catch_code_errors ts =
let
+ val genuine_only = not (Config.get ctxt Quickcheck.potential)
val thy = Proof_Context.theory_of ctxt
val (ts', eval_terms) = split_list ts
val _ = map check_test_term ts'
val names = Term.add_free_names (hd ts') []
val Ts = map snd (Term.add_frees (hd ts') [])
val current_result = Unsynchronized.ref Quickcheck.empty_result
- fun test_card_size test_fun (card, size) =
+ fun test_card_size test_fun genuine_only (card, size) =
(* FIXME: why decrement size by one? *)
let
val _ =
@@ -165,7 +167,7 @@
"cardinality: " ^ string_of_int card)
val (ts, timing) =
cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
- (fn () => fst (test_fun [card, size - 1]))
+ (fn () => fst (test_fun genuine_only [card, size - 1]))
val _ = Quickcheck.add_timing timing current_result
in
Option.map (pair card) ts
@@ -187,7 +189,7 @@
!current_result)
| SOME test_fun =>
let
- val _ = case get_first (test_card_size test_fun) enumeration_card_size of
+ val _ = case get_first (test_card_size test_fun genuine_only) enumeration_card_size of
SOME (card, ts) => Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
| NONE => ()
in !current_result end
@@ -276,11 +278,11 @@
fun mk_safe_if genuine_only (cond, then_t, else_t) =
let
val T = @{typ "(bool * term list) option"}
- val if = Const (@{const_name "If"}, T --> T --> T)
+ val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
in
Const (@{const_name "Quickcheck.catch_match"}, T --> T --> T) $
- (if $ cond $ then_t $ else_t true) $
- (if $ genuine_only $ Const (@{const_name "None", T) $ else_t false);
+ (if_t $ cond $ then_t $ else_t true) $
+ (if_t $ genuine_only $ Const (@{const_name "None"}, T) $ else_t false)
end
fun collect_results f [] results = results
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Mon Dec 05 12:35:04 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Dec 05 12:35:05 2011 +0100
@@ -11,8 +11,8 @@
-> (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 -> (bool * term list) option * Quickcheck.report option
- val put_counterexample: (unit -> int -> int -> seed -> (bool * term list) option * seed)
+ Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
+ val put_counterexample: (unit -> int -> bool -> 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)
-> Proof.context -> Proof.context
@@ -272,7 +272,7 @@
structure Counterexample = Proof_Data
(
- type T = unit -> int -> int -> int * int -> (bool * term list) option * (int * int)
+ type T = unit -> int -> bool -> int -> int * int -> (bool * term list) option * (int * int)
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Counterexample"
);
@@ -298,7 +298,9 @@
(2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
- val check = Quickcheck_Common.mk_safe_if ctxt (result, Const (@{const_name "None"}, resultT),
+ val ([genuine_only_name], ctxt') = Variable.variant_fixes ["genuine_only"] ctxt
+ val genuine_only = Free (genuine_only_name, @{typ bool})
+ val check = Quickcheck_Common.mk_safe_if genuine_only (result, Const (@{const_name "None"}, resultT),
fn genuine => @{term "Some :: bool * term list => (bool * term list) option"} $
HOLogic.mk_prod (Quickcheck_Common.reflect_bool genuine, terms))
val return = HOLogic.pair_const resultT @{typ Random.seed};
@@ -313,7 +315,10 @@
(mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
fun mk_bindclause (_, _, i, T) = mk_scomp_split T
(Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
- in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
+ in
+ lambda genuine_only
+ (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)))
+ end;
fun mk_reporting_generator_expr ctxt (t, eval_terms) =
let
@@ -420,7 +425,7 @@
| SOME q => (SOME (true, q), report)
end
in
- fn [card, size] => apsnd SOME (iterate_and_collect (card, size) iterations empty_report)
+ fn _ => fn [card, size] => apsnd SOME (iterate_and_collect (card, size) iterations empty_report)
end
else
let
@@ -428,13 +433,17 @@
val compile = Code_Runtime.dynamic_value_strict
(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
- 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
+ (fn proc => fn g => fn c => fn b => fn s => g c b s
+ #>> (Option.map o apsnd o map) proc) t' [];
+ fun single_tester c b s = compile c b s |> Random_Engine.run
+ fun iterate _ (card, size) 0 = NONE
+ | iterate genuine_only (card, size) j =
+ case single_tester card genuine_only size of
+ NONE => iterate genuine_only (card, size) (j - 1)
+ | SOME q => SOME q
in
- fn [card, size] => (rpair NONE (iterate (card, size) iterations))
+ fn genuine_only => fn [card, size] =>
+ (rpair NONE (iterate genuine_only (card, size) iterations))
end
end;