# HG changeset patch # User bulwahn # Date 1320834899 -3600 # Node ID 10ba32c347b05061a7101aa2680bcd81775e0a3a # Parent e5ef7aa77fdea2e58a33bf11601ad7adbbbf27af quickcheck fails with code generator errors only if one tester is invoked diff -r e5ef7aa77fde -r 10ba32c347b0 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Nov 09 11:34:57 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Nov 09 11:34:59 2011 +0100 @@ -456,7 +456,7 @@ end end; -fun test_goals ctxt insts goals = +fun test_goals ctxt _ insts goals = if (not (getenv "ISABELLE_GHC" = "")) then let val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals diff -r e5ef7aa77fde -r 10ba32c347b0 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Nov 09 11:34:57 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Nov 09 11:34:59 2011 +0100 @@ -16,7 +16,7 @@ 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 - val generator_test_goal_terms : compile_generator -> Proof.context -> (string * typ) list + val generator_test_goal_terms : compile_generator -> Proof.context -> bool -> (string * typ) list -> (term * term list) list -> Quickcheck.result list val ensure_sort_datatype: ((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list @@ -27,7 +27,7 @@ -> Proof.context -> (term * term list) list -> term val mk_fun_upd : typ -> typ -> term * term -> term -> term val post_process_term : term -> term - val test_term : compile_generator -> Proof.context -> term * term list -> Quickcheck.result + val test_term : compile_generator -> Proof.context -> bool -> term * term list -> Quickcheck.result end; structure Quickcheck_Common : QUICKCHECK_COMMON = @@ -61,7 +61,7 @@ let val ({cpu, ...}, result) = Timing.timing e () in (result, (description, Time.toMilliseconds cpu)) end -fun test_term compile ctxt (t, eval_terms) = +fun test_term compile ctxt catch_code_errors (t, eval_terms) = let val _ = check_test_term t val names = Term.add_free_names t [] @@ -83,8 +83,9 @@ in case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q 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 () => try (compile ctxt) [(t, eval_terms)]); + (fn () => act (compile ctxt) [(t, eval_terms)]); val _ = Quickcheck.add_timing comp_time current_result in case test_fun of @@ -135,7 +136,7 @@ end -fun test_term_with_increasing_cardinality compile ctxt ts = +fun test_term_with_increasing_cardinality compile ctxt catch_code_errors ts = let val thy = Proof_Context.theory_of ctxt val (ts', eval_terms) = split_list ts @@ -161,7 +162,8 @@ (* size does matter *) map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size)) |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2))) - val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => try (compile ctxt) ts) + 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) ts) val _ = Quickcheck.add_timing comp_time current_result in case test_fun of @@ -245,19 +247,19 @@ SOME (lhs, rhs) => (t, eval_terms @ [rhs, lhs]) | NONE => (t, eval_terms) -fun generator_test_goal_terms compile ctxt insts goals = +fun generator_test_goal_terms compile ctxt catch_code_errors insts goals = let fun test_term' goal = case goal of - [(NONE, t)] => test_term compile ctxt t - | ts => test_term_with_increasing_cardinality compile ctxt (map snd ts) + [(NONE, t)] => test_term compile ctxt catch_code_errors t + | ts => test_term_with_increasing_cardinality compile ctxt catch_code_errors (map snd ts) val goals' = instantiate_goals ctxt insts goals |> map (map (apsnd add_equation_eval_terms)) in if Config.get ctxt Quickcheck.finite_types then collect_results test_term' goals' [] else - collect_results (test_term compile ctxt) + collect_results (test_term compile ctxt catch_code_errors) (maps (map snd) goals') [] end; diff -r e5ef7aa77fde -r 10ba32c347b0 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Wed Nov 09 11:34:57 2011 +0100 +++ b/src/Tools/quickcheck.ML Wed Nov 09 11:34:59 2011 +0100 @@ -50,7 +50,7 @@ val timings_of : result -> (string * int) list (* registering testers & generators *) type tester = - Proof.context -> (string * typ) list -> (term * term list) list -> result list + Proof.context -> bool -> (string * typ) list -> (term * term list) list -> result list val add_tester : string * (bool Config.T * tester) -> Context.generic -> Context.generic val add_batch_generator : string * (Proof.context -> term list -> (int -> term list option) list) @@ -192,7 +192,7 @@ (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2)); type tester = - Proof.context -> (string * typ) list -> (term * term list) list -> result list + Proof.context -> bool -> (string * typ) list -> (term * term list) list -> result list structure Data = Generic_Data ( @@ -288,7 +288,7 @@ [] => error "No active testers for quickcheck" | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () => Par_List.get_some (fn tester => - tester ctxt insts goals |> + tester ctxt (length testers > 1) insts goals |> (fn result => if exists found_counterexample result then SOME result else NONE)) testers) (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ();