--- a/NEWS Mon Dec 05 14:44:46 2011 +0100
+++ b/NEWS Mon Dec 05 14:47:01 2011 +0100
@@ -145,6 +145,21 @@
produces a rule which can be used to perform case distinction on both
a list and a nat.
+* Quickcheck:
+ - Quickcheck returns variable assignments as counterexamples, which
+ allows to reveal the underspecification of functions under test.
+ For example, refuting "hd xs = x", it presents the variable
+ assignment xs = [] and x = a1 as a counterexample, assuming that
+ any property is false whenever "hd []" occurs in it.
+ These counterexample are marked as potentially spurious, as
+ Quickcheck also returns "xs = []" as a counterexample to the
+ obvious theorem "hd xs = hd xs".
+ After finding a potentially spurious counterexample, Quickcheck
+ continues searching for genuine ones.
+ By default, Quickcheck shows potentially spurious and genuine
+ counterexamples. The option "genuine_only" sets quickcheck to
+ only show genuine counterexamples.
+
* Nitpick:
- Fixed infinite loop caused by the 'peephole_optim' option and
affecting 'rat' and 'real'.
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Dec 05 14:44:46 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Dec 05 14:47:01 2011 +0100
@@ -1592,6 +1592,10 @@
\item[@{text size}] specifies the maximum size of the search space
for assignment values.
+ \item[@{text genuine_only}] sets quickcheck only to return genuine
+ counterexample, but not potentially spurious counterexamples due
+ to underspecified functions.
+
\item[@{text eval}] takes a term or a list of terms and evaluates
these terms under the variable assignment found by quickcheck.
@@ -1609,8 +1613,11 @@
\item[@{text report}] if set quickcheck reports how many tests
fulfilled the preconditions.
- \item[@{text quiet}] if not set quickcheck informs about the
- current size for assignment values.
+ \item[@{text quiet}] if set quickcheck does not output anything
+ while testing.
+
+ \item[@{text verbose}] if set quickcheck informs about the
+ current size and cardinality while testing.
\item[@{text expect}] can be used to check if the user's
expectation was met (@{text no_expectation}, @{text
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Dec 05 14:44:46 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Dec 05 14:47:01 2011 +0100
@@ -2346,6 +2346,10 @@
\item[\isa{size}] specifies the maximum size of the search space
for assignment values.
+ \item[\isa{genuine{\isaliteral{5F}{\isacharunderscore}}only}] sets quickcheck only to return genuine
+ counterexample, but not potentially spurious counterexamples due
+ to underspecified functions.
+
\item[\isa{eval}] takes a term or a list of terms and evaluates
these terms under the variable assignment found by quickcheck.
@@ -2363,8 +2367,11 @@
\item[\isa{report}] if set quickcheck reports how many tests
fulfilled the preconditions.
- \item[\isa{quiet}] if not set quickcheck informs about the
- current size for assignment values.
+ \item[\isa{quiet}] if set quickcheck does not output anything
+ while testing.
+
+ \item[\isa{verbose}] if set quickcheck informs about the
+ current size and cardinality while testing.
\item[\isa{expect}] can be used to check if the user's
expectation was met (\isa{no{\isaliteral{5F}{\isacharunderscore}}expectation}, \isa{no{\isaliteral{5F}{\isacharunderscore}}counterexample}, or \isa{counterexample}).
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Mon Dec 05 14:47:01 2011 +0100
@@ -38,9 +38,9 @@
Left e -> throw e);
answer :: Bool -> Bool -> (Bool -> Bool -> IO b) -> (Pos -> IO b) -> IO b;
-answer potential a known unknown =
+answer genuine_only a known unknown =
Control.Exception.catch (answeri a known unknown)
- (\ (PatternMatchFail _) -> known False (not potential));
+ (\ (PatternMatchFail _) -> known False genuine_only);
-- Refute
@@ -52,14 +52,14 @@
", " ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
eval :: Bool -> Bool -> (Bool -> Bool -> IO a) -> (Pos -> IO a) -> IO a;
-eval potential p k u = answer potential p (\genuine p -> answer potential p k u) u;
+eval genuine_only p k u = answer genuine_only p k u;
ref :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
-ref potential r xs = eval potential (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs)
- (\p -> sumMapM (ref potential r) 1 (refineList xs p));
-
+ref genuine_only r xs = eval genuine_only (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs)
+ (\p -> sumMapM (ref genuine_only r) 1 (refineList xs p));
+
refute :: Bool -> Result -> IO Int;
-refute potential r = ref potential r (args r);
+refute genuine_only r = ref genuine_only r (args r);
sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
sumMapM f n [] = return n;
@@ -109,10 +109,10 @@
-- Top-level interface
depthCheck :: Testable a => Bool -> Int -> a -> IO ();
-depthCheck potential d p =
- (refute potential $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
+depthCheck genuine_only d p =
+ (refute genuine_only $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
smallCheck :: Testable a => Bool -> Int -> a -> IO ();
-smallCheck potential d p = mapM_ (\d -> depthCheck potential d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
+smallCheck genuine_only d p = mapM_ (\d -> depthCheck genuine_only d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
}
--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs Mon Dec 05 14:47:01 2011 +0100
@@ -57,9 +57,9 @@
Left e -> throw e
answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
-answer potential a known unknown =
+answer genuine_only a known unknown =
Control.Exception.catch (answeri a known unknown)
- (\ (PatternMatchFail _) -> known (not potential))
+ (\ (PatternMatchFail _) -> known genuine_only)
-- Proofs and Refutation
@@ -154,19 +154,19 @@
-- refute
refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> QuantTree -> IO QuantTree
-refute exec potential d t = ref t
+refute exec genuine_only d t = ref t
where
ref t =
let path = find t in
do
- t' <- answer potential (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
+ t' <- answer genuine_only (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
(\p -> return (if length p < d then refineTree path p t else updateNode path unknown t));
case evalOf t' of
UnknownValue True -> ref t'
_ -> return t'
depthCheck :: Bool -> Int -> Generated_Code.Property -> IO ()
-depthCheck potential d p = refute (checkOf p) potential d (treeOf 0 p) >>= (\t ->
+depthCheck genuine_only d p = refute (checkOf p) genuine_only d (treeOf 0 p) >>= (\t ->
case evalOf t of
Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")
_ -> putStrLn ("NONE"))
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Dec 05 14:47:01 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
@@ -289,7 +289,7 @@
let
fun mk_naive_test_term t =
fold_rev mk_closure (map lookup (Term.add_free_names t []))
- (mk_if (t, none_t, return))
+ (mk_if (t, none_t, return) true)
fun mk_smart_test_term' concl bound_vars assms genuine =
let
fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
@@ -298,7 +298,7 @@
| assm :: assms => (vars_of assm, (HOLogic.mk_not assm, none_t,
mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms))
in
- fold_rev mk_closure (map lookup vars) (mk_if check)
+ fold_rev mk_closure (map lookup vars) (mk_if check genuine)
end
val mk_smart_test_term =
Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms true)
@@ -323,7 +323,7 @@
fast_exhaustiveT T)
$ lambda free t $ depth
val none_t = @{term "()"}
- fun mk_safe_if (cond, then_t, else_t) = mk_if (cond, then_t, else_t true)
+ fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if none_t return ctxt
in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end
@@ -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 none_t
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
@@ -360,9 +362,11 @@
val ctxt' = Variable.auto_fixes t ctxt
val names = Term.add_free_names t []
val frees = map Free (Term.add_frees t [])
- val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+ val ([depth_name, genuine_only_name], ctxt'') =
+ Variable.variant_fixes ["depth", "genuine_only"] ctxt'
val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") names) ctxt''
val depth = Free (depth_name, @{typ code_numeral})
+ val genuine_only = Free (depth_name, @{typ bool})
val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
val return = mk_return (HOLogic.mk_list @{typ term}
@@ -370,21 +374,22 @@
fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
if Sign.of_sort thy (T, @{sort enum}) then
Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
- $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
+ $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
$ lambda free (lambda term_var t))
else
Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
$ (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 none_t
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_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
@@ -399,7 +404,7 @@
fun mk_bounded_forall (Free (s, T)) t =
Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)
$ lambda (Free (s, T)) t $ depth
- fun mk_safe_if (cond, then_t, else_t) = mk_if (cond, then_t, else_t true)
+ fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
val mk_test_term =
mk_test_term lookup mk_bounded_forall mk_safe_if @{term True} (K @{term False}) ctxt
in lambda depth (mk_test_term t) end
@@ -422,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"
);
@@ -458,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/narrowing_generators.ML Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Dec 05 14:47:01 2011 +0100
@@ -222,10 +222,11 @@
let val ({elapsed, ...}, result) = Timing.timing e ()
in (result, (description, Time.toMilliseconds elapsed)) end
-fun value (contains_existentials, ((potential, quiet), size)) ctxt cookie (code, value_name) =
+fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code, value_name) =
let
- val (get, put, put_ml) = cookie
+ val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
fun message s = if quiet then () else Output.urgent_message s
+ fun verbose_message s = if not quiet andalso verbose then Output.urgent_message s else ()
val current_size = Unsynchronized.ref 0
val current_result = Unsynchronized.ref Quickcheck.empty_result
fun excipit () =
@@ -260,20 +261,20 @@
val _ = Quickcheck.add_timing compilation_time current_result
fun haskell_string_of_bool v = if v then "True" else "False"
val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
- fun with_size k =
+ fun with_size genuine_only k =
if k > size then
(NONE, !current_result)
else
let
- val _ = message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
+ val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
val _ = current_size := k
val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
(fn () => Isabelle_System.bash_output
- (executable ^ " " ^ haskell_string_of_bool potential ^ " " ^ string_of_int k))
+ (executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k))
val _ = Quickcheck.add_timing timing current_result
in
if response = "NONE\n" then
- with_size (k + 1)
+ with_size genuine_only (k + 1)
else
let
val output_value = the_default "NONE"
@@ -283,10 +284,22 @@
^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
val ctxt' = ctxt
|> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
- |> Context.proof_map (exec false ml_code);
- in (get ctxt' (), !current_result) end
+ |> Context.proof_map (exec false ml_code);
+ val counterexample = get ctxt' ()
+ in
+ if is_genuine counterexample then
+ (counterexample, !current_result)
+ else
+ let
+ val cex = Option.map (rpair []) (counterexample_of counterexample)
+ in
+ (message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+ message "Quickcheck continues to find a genuine counterexample...";
+ with_size true (k + 1))
+ end
+ end
end
- in with_size 0 end
+ in with_size genuine_only 0 end
in
with_tmp_dir tmp_prefix run
end;
@@ -294,8 +307,9 @@
fun dynamic_value_strict opts cookie thy postproc t =
let
val ctxt = Proof_Context.init_global thy
- fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value opts ctxt cookie)
- (Code_Target.evaluator thy target naming program deps (vs_ty, t));
+ fun evaluator naming program ((_, vs_ty), t) deps =
+ Exn.interruptible_capture (value opts ctxt cookie)
+ (Code_Target.evaluator thy target naming program deps (vs_ty, t));
in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
(** counterexample generator **)
@@ -418,7 +432,8 @@
let
fun dest_result (Quickcheck.Result r) = r
val opts =
- ((Config.get ctxt Quickcheck.potential, Config.get ctxt Quickcheck.quiet),
+ ((Config.get ctxt Quickcheck.genuine_only,
+ (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.verbose)),
Config.get ctxt Quickcheck.size)
val thy = Proof_Context.theory_of ctxt
val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
@@ -432,8 +447,8 @@
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
val (counterexample, result) = dynamic_value_strict (true, opts)
- (Existential_Counterexample.get, Existential_Counterexample.put,
- "Narrowing_Generators.put_existential_counterexample")
+ ((K true, fn _ => error ""), (Existential_Counterexample.get, Existential_Counterexample.put,
+ "Narrowing_Generators.put_existential_counterexample"))
thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t)
in
Quickcheck.Result
@@ -443,18 +458,22 @@
end
else
let
- val t' = fold_rev absfree (Term.add_frees t []) t
+ val frees = Term.add_frees t []
+ val t' = fold_rev absfree frees t
fun wrap f t = list_abs (f (strip_abs t))
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
fun ensure_testable t =
Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
+ fun is_genuine (SOME (true, _)) = true
+ | is_genuine _ = false
+ val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
val (counterexample, result) = dynamic_value_strict (false, opts)
- (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
+ ((is_genuine, counterexample_of),
+ (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample"))
thy (apfst o Option.map o apsnd o map) (ensure_testable (finitize t'))
in
Quickcheck.Result
- {counterexample =
- Option.map (apsnd (((curry (op ~~)) (Term.add_free_names t [])) o map post_process)) counterexample,
+ {counterexample = counterexample_of counterexample,
evaluation_terms = Option.map (K []) counterexample,
timings = #timings (dest_result result), reports = #reports (dest_result result)}
end
@@ -463,6 +482,7 @@
fun test_goals ctxt _ insts goals =
if (not (getenv "ISABELLE_GHC" = "")) then
let
+ val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-narrowing...")
val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
in
Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) []
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 05 14:47:01 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 * term * (bool -> term) -> bool -> 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,31 +69,44 @@
fun test_term (name, compile) ctxt catch_code_errors (t, eval_terms) =
let
+ val genuine_only = Config.get ctxt Quickcheck.genuine_only
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)
+ val _ = Quickcheck.verbose_message ctxt
+ ("[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) | SOME q => SOME q
+ case result of
+ NONE => with_size test_fun genuine_only (k + 1)
+ | SOME (true, ts) => SOME (true, ts)
+ | SOME (false, ts) =>
+ let
+ val (ts1, ts2) = chop (length names) ts
+ val (eval_terms', _) = chop (length ts2) eval_terms
+ val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
+ in
+ (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+ Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
+ with_size test_fun true k)
+ end
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);
@@ -101,7 +114,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
@@ -147,25 +160,26 @@
fun test_term_with_cardinality (name, compile) ctxt catch_code_errors ts =
let
+ val genuine_only = Config.get ctxt Quickcheck.genuine_only
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 _ =
- Quickcheck.message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
+ Quickcheck.verbose_message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
(if size = 0 then "" else "data size: " ^ string_of_int (size - 1) ^ " and ") ^
"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
+ Option.map (pair (card, size)) ts
end
val enumeration_card_size =
if forall (fn T => Sign.of_sort thy (T, ["Enum.enum"])) Ts then
@@ -184,10 +198,22 @@
!current_result)
| SOME test_fun =>
let
- val _ = case get_first (test_card_size test_fun) enumeration_card_size of
- SOME (card, ts) => Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
+ val _ = Quickcheck.message ctxt ("Testing conjecture with with Quickcheck-" ^ name ^ "...");
+ fun test genuine_only enum = case get_first (test_card_size test_fun genuine_only) enum of
+ SOME ((card, _), (true, ts)) =>
+ Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (true, ts)) current_result
+ | SOME ((card, size), (false, ts)) =>
+ let
+ val (ts1, ts2) = chop (length names) ts
+ val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1))
+ val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
+ in
+ (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+ Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
+ test true (snd (take_prefix (fn x => not (x = (card, size))) enum)))
+ end
| NONE => ()
- in !current_result end
+ in (test genuine_only enumeration_card_size; !current_result) end
end
fun get_finite_types ctxt =
@@ -270,11 +296,15 @@
(* compilation of testing functions *)
-fun mk_safe_if ctxt (cond, then_t, else_t) =
- @{term "Quickcheck.catch_match :: (bool * term list) option => (bool * term list) option => (bool * term list) option"}
- $ (@{term "If :: bool => (bool * term list) option => (bool * term list) option => (bool * term list) option"}
- $ cond $ then_t $ else_t true)
- $ (if Config.get ctxt Quickcheck.potential then else_t false else @{term "None :: (bool * term list) option"});
+fun mk_safe_if genuine_only none (cond, then_t, else_t) genuine =
+ let
+ val T = fastype_of then_t
+ val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
+ in
+ Const (@{const_name "Quickcheck.catch_match"}, T --> T --> T) $
+ (if_t $ cond $ then_t $ else_t genuine) $
+ (if_t $ genuine_only $ none $ else_t false)
+ end
fun collect_results f [] results = results
| collect_results f (t :: ts) results =
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Dec 05 14:47:01 2011 +0100
@@ -11,10 +11,10 @@
-> (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)
+ val put_counterexample_report: (unit -> int -> bool -> int -> seed -> ((bool * term list) option * (bool list * bool)) * seed)
-> Proof.context -> Proof.context
val setup: theory -> theory
end;
@@ -60,7 +60,11 @@
fun term_fun' () = #3 (! state) ();
in ((random_fun', term_fun'), seed''') end;
-
+fun mk_if (b, t, e) =
+ let
+ val T = fastype_of t
+ in Const (@{const_name "HOL.If"}, @{typ bool} --> T --> T --> T) $ b $ t $ e end
+
(** datatypes **)
(* definitional scheme for random instances on datatypes *)
@@ -272,7 +276,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"
);
@@ -280,7 +284,7 @@
structure Counterexample_Report = Proof_Data
(
- type T = unit -> int -> int -> seed -> (term list option * (bool list * bool)) * seed
+ type T = unit -> int -> bool -> int -> seed -> ((bool * term list) option * (bool list * bool)) * seed
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Counterexample_Report"
);
@@ -298,7 +302,10 @@
(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 none_t = Const (@{const_name "None"}, resultT)
+ val check = Quickcheck_Common.mk_safe_if genuine_only none_t (result, none_t,
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,11 +320,15 @@
(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 true)))
+ end;
fun mk_reporting_generator_expr ctxt (t, eval_terms) =
let
val thy = Proof_Context.theory_of ctxt
+ val resultT = @{typ "(bool * term list) option * (bool list * bool)"}
val prop = fold_rev absfree (Term.add_frees t []) t
val Ts = (map snd o fst o strip_abs) prop
val bound_max = length Ts - 1
@@ -326,55 +337,52 @@
val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
val (assms, concl) = Quickcheck_Common.strip_imp prop'
- val return =
- @{term "Pair :: term list option * (bool list * bool) => Random.seed => (term list option * (bool list * bool)) * Random.seed"};
+ val return = HOLogic.pair_const resultT @{typ "Random.seed"};
fun mk_assms_report i =
- HOLogic.mk_prod (@{term "None :: term list option"},
+ HOLogic.mk_prod (@{term "None :: (bool * term list) option"},
HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT
(replicate i @{term True} @ replicate (length assms - i) @{term False}),
@{term False}))
fun mk_concl_report b =
HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT (replicate (length assms) @{term True}),
- if b then @{term True} else @{term False})
- val If =
- @{term "If :: bool => term list option * (bool list * bool) => term list option * (bool list * bool) => term list option * (bool list * bool)"}
- val concl_check = If $ concl $
- HOLogic.mk_prod (@{term "None :: term list option"}, mk_concl_report true) $
- HOLogic.mk_prod (@{term "Some :: term list => term list option"} $ terms, mk_concl_report false)
- val check = fold_rev (fn (i, assm) => fn t => If $ assm $ t $ mk_assms_report i)
+ Quickcheck_Common.reflect_bool b)
+ val ([genuine_only_name], ctxt') = Variable.variant_fixes ["genuine_only"] ctxt
+ val genuine_only = Free (genuine_only_name, @{typ bool})
+ val none_t = HOLogic.mk_prod (@{term "None :: (bool * term list) option"}, mk_concl_report true)
+ val concl_check = Quickcheck_Common.mk_safe_if genuine_only none_t (concl, none_t,
+ fn genuine => HOLogic.mk_prod (@{term "Some :: bool * term list => (bool * term list) option"} $
+ HOLogic.mk_prod (Quickcheck_Common.reflect_bool genuine, terms), mk_concl_report false))
+ val check = fold_rev (fn (i, assm) => fn t => Quickcheck_Common.mk_safe_if genuine_only
+ (mk_assms_report i) (HOLogic.mk_not assm, mk_assms_report i, t))
(map_index I assms) concl_check
- val check' = @{term "Quickcheck.catch_match :: term list option * bool list * bool =>
- term list option * bool list * bool => term list option * bool list * bool"} $ check $
- (if Config.get ctxt Quickcheck.potential then
- HOLogic.mk_prod (@{term "Some :: term list => term list option"} $ terms, mk_concl_report false)
- else
- HOLogic.mk_prod (@{term "None :: term list option"}, mk_concl_report true))
fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
fun mk_split T = Sign.mk_const thy
- (@{const_name prod_case}, [T, @{typ "unit => term"},
- liftT @{typ "term list option * (bool list * bool)"} @{typ Random.seed}]);
+ (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
fun mk_scomp_split T t t' =
- mk_scomp (mk_termtyp T) @{typ "term list option * (bool list * bool)"} @{typ Random.seed} t
+ mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
(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'))
+ lambda genuine_only
+ (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
end
val mk_parametric_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr
((mk_generator_expr,
- absdummy @{typ code_numeral} @{term "Pair None :: Random.seed => (bool * term list) option * Random.seed"}),
- @{typ "code_numeral => Random.seed => (bool * term list) option * Random.seed"})
+ absdummy @{typ bool} (absdummy @{typ code_numeral}
+ @{term "Pair None :: Random.seed => (bool * term list) option * Random.seed"})),
+ @{typ "bool => code_numeral => Random.seed => (bool * term list) option * Random.seed"})
val mk_parametric_reporting_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr
((mk_reporting_generator_expr,
- absdummy @{typ code_numeral}
- @{term "Pair (None, ([], False)) :: Random.seed => (term list option * (bool list * bool)) * Random.seed"}),
- @{typ "code_numeral => Random.seed => (term list option * (bool list * bool)) * Random.seed"})
+ absdummy @{typ bool} (absdummy @{typ code_numeral}
+ @{term "Pair (None, ([], False)) :: Random.seed =>
+ ((bool * term list) option * (bool list * bool)) * Random.seed"})),
+ @{typ "bool => code_numeral => Random.seed => ((bool * term list) option * (bool list * bool)) * Random.seed"})
(* single quickcheck report *)
@@ -408,19 +416,22 @@
val t' = mk_parametric_reporting_generator_expr ctxt ts;
val compile = Code_Runtime.dynamic_value_strict
(Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
- thy (SOME target) (fn proc => fn g => fn c => fn s => g c s #>> (apfst o Option.map o map) proc) t' [];
- fun single_tester c s = compile c s |> Random_Engine.run
- fun iterate_and_collect (card, size) 0 report = (NONE, report)
- | iterate_and_collect (card, size) j report =
+ thy (SOME target)
+ (fn proc => fn g => fn c => fn b => fn s => g c b s
+ #>> (apfst o Option.map o apsnd o map) proc) t' [];
+ fun single_tester c b s = compile c b s |> Random_Engine.run
+ fun iterate_and_collect _ (card, size) 0 report = (NONE, report)
+ | iterate_and_collect genuine_only (card, size) j report =
let
- val (test_result, single_report) = apsnd Run (single_tester card size)
+ val (test_result, single_report) = apsnd Run (single_tester card genuine_only size)
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 (true, q), report)
+ case test_result of NONE => iterate_and_collect genuine_only (card, size) (j - 1) report
+ | SOME q => (SOME q, report)
end
in
- fn [card, size] => apsnd SOME (iterate_and_collect (card, size) iterations empty_report)
+ fn genuine_only => fn [card, size] =>
+ apsnd SOME (iterate_and_collect genuine_only (card, size) iterations empty_report)
end
else
let
@@ -428,13 +439,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;
--- a/src/HOL/ex/Quickcheck_Examples.thy Mon Dec 05 14:44:46 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Mon Dec 05 14:47:01 2011 +0100
@@ -411,25 +411,22 @@
lemma
"xs = [] ==> hd xs \<noteq> x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
-quickcheck[random, potential = false, report = false, expect = no_counterexample]
-quickcheck[random, potential = true, report = false, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
oops
lemma
"xs = [] ==> hd xs = x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
-quickcheck[random, potential = false, report = false, expect = no_counterexample]
-quickcheck[random, potential = true, report = false, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
oops
lemma "xs = [] ==> hd xs = x ==> x = y"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
-quickcheck[random, potential = false, report = false, expect = no_counterexample]
-quickcheck[random, potential = true, report = false, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
oops
text {* with the simple testing scheme *}
@@ -439,19 +436,16 @@
lemma
"xs = [] ==> hd xs \<noteq> x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
oops
lemma
"xs = [] ==> hd xs = x"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
oops
lemma "xs = [] ==> hd xs = x ==> x = y"
-quickcheck[exhaustive, potential = false, expect = no_counterexample]
-quickcheck[exhaustive, potential = true, expect = counterexample]
+quickcheck[exhaustive, expect = no_counterexample]
oops
declare [[quickcheck_full_support = true]]
--- a/src/Tools/quickcheck.ML Mon Dec 05 14:44:46 2011 +0100
+++ b/src/Tools/quickcheck.ML Mon Dec 05 14:47:01 2011 +0100
@@ -20,8 +20,9 @@
val no_assms : bool Config.T
val report : bool Config.T
val timing : bool Config.T
- val potential : bool Config.T
+ val genuine_only : bool Config.T
val quiet : bool Config.T
+ val verbose : bool Config.T
val timeout : real Config.T
val allow_function_inversion : bool Config.T;
val finite_types : bool Config.T
@@ -62,7 +63,10 @@
-> Context.generic -> Context.generic
(* basic operations *)
val message : Proof.context -> string -> unit
+ val verbose_message : Proof.context -> string -> unit
val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a
+ val pretty_counterex : Proof.context -> bool ->
+ ((bool * (string * term) list) * (term * term) list) option -> Pretty.T
(* testing terms and proof states *)
val mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
val mk_batch_tester : Proof.context -> term list -> (int -> term list option) list option
@@ -172,8 +176,9 @@
val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
-val potential = Attrib.setup_config_bool @{binding quickcheck_potential} (K true)
+val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
+val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false)
val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
val allow_function_inversion =
Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false)
@@ -288,11 +293,15 @@
f ()
fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s
-
+
+fun verbose_message ctxt s = if not (Config.get ctxt quiet) andalso Config.get ctxt verbose
+ then Output.urgent_message s else ()
+
fun test_terms ctxt (limit_time, is_interactive) insts goals =
case active_testers ctxt of
[] => error "No active testers for quickcheck"
- | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
+ | testers =>
+ limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
(fn () => Par_List.get_some (fn tester =>
tester ctxt (length testers > 1) insts goals |>
(fn result => if exists found_counterexample result then SOME result else NONE)) testers)
@@ -302,6 +311,7 @@
let
val lthy = Proof.context_of state;
val thy = Proof.theory_of state;
+ val _ = message lthy "Quickchecking..."
fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
| strip t = t;
val {goal = st, ...} = Proof.raw_goal state;
@@ -412,8 +422,9 @@
| parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
| parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg)))
| parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
- | parse_test_param ("potential", [arg]) = apsnd (Config.put_generic potential (read_bool arg))
+ | parse_test_param ("genuine_only", [arg]) = apsnd (Config.put_generic genuine_only (read_bool arg))
| parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
+ | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
| parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
| parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
| parse_test_param ("allow_function_inversion", [arg]) =