# HG changeset patch # User bulwahn # Date 1323084982 -3600 # Node ID cb6ddee6a4633931f20c92dc4a80f8c08c4be366 # Parent 1672be34581a6392193cea56c385bff428ff9b6e making the default behaviour of quickcheck a little bit less verbose; adapting quickcheck examples diff -r 1672be34581a -r cb6ddee6a463 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Dec 05 12:36:21 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Dec 05 12:36:22 2011 +0100 @@ -222,10 +222,11 @@ let val ({elapsed, ...}, result) = Timing.timing e () in (result, (description, Time.toMilliseconds elapsed)) end -fun value (contains_existentials, ((genuine_only, quiet), size)) ctxt cookie (code, value_name) = +fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code, value_name) = let 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 () = @@ -265,7 +266,7 @@ (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 @@ -292,8 +293,8 @@ let val cex = Option.map (rpair []) (counterexample_of counterexample) in - (Output.urgent_message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); - Output.urgent_message "Quickcheck continues to find a genuine counterexample..."; + (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 @@ -431,7 +432,8 @@ let fun dest_result (Quickcheck.Result r) = r val opts = - ((Config.get ctxt Quickcheck.genuine_only, 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 @@ -480,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) [] diff -r 1672be34581a -r cb6ddee6a463 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 05 12:36:21 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Dec 05 12:36:22 2011 +0100 @@ -85,7 +85,7 @@ NONE else let - val _ = Quickcheck.message ctxt + val _ = Quickcheck.verbose_message ctxt ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k) val _ = current_size := k val ((result, report), timing) = @@ -102,8 +102,8 @@ val (eval_terms', _) = chop (length ts2) eval_terms val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2) in - (Output.urgent_message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); - Output.urgent_message "Quickcheck continues to find a genuine counterexample..."; + (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; @@ -171,7 +171,7 @@ (* 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) = @@ -198,6 +198,7 @@ !current_result) | SOME test_fun => let + 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 @@ -207,8 +208,8 @@ val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1)) val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2) in - (Output.urgent_message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); - Output.urgent_message "Quickcheck continues to find a genuine counterexample..."; + (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 => () diff -r 1672be34581a -r cb6ddee6a463 src/HOL/ex/Quickcheck_Examples.thy --- a/src/HOL/ex/Quickcheck_Examples.thy Mon Dec 05 12:36:21 2011 +0100 +++ b/src/HOL/ex/Quickcheck_Examples.thy Mon Dec 05 12:36:22 2011 +0100 @@ -413,22 +413,20 @@ "xs = [] ==> hd xs \ x" quickcheck[exhaustive, expect = no_counterexample] quickcheck[random, report = false, expect = no_counterexample] -quickcheck[random, report = true, expect = 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 *} @@ -438,19 +436,16 @@ 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" -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]] diff -r 1672be34581a -r cb6ddee6a463 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Mon Dec 05 12:36:21 2011 +0100 +++ b/src/Tools/quickcheck.ML Mon Dec 05 12:36:22 2011 +0100 @@ -63,6 +63,7 @@ -> 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 @@ -292,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) @@ -306,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;