quickcheck fails with code generator errors only if one tester is invoked
authorbulwahn
Wed Nov 09 11:34:59 2011 +0100 (2011-11-09)
changeset 4541910ba32c347b0
parent 45418 e5ef7aa77fde
child 45420 d17556b9a89b
quickcheck fails with code generator errors only if one tester is invoked
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Nov 09 11:34:57 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Nov 09 11:34:59 2011 +0100
     1.3 @@ -456,7 +456,7 @@
     1.4        end
     1.5    end;
     1.6  
     1.7 -fun test_goals ctxt insts goals =
     1.8 +fun test_goals ctxt _ insts goals =
     1.9    if (not (getenv "ISABELLE_GHC" = "")) then
    1.10      let
    1.11        val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
     2.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Nov 09 11:34:57 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Nov 09 11:34:59 2011 +0100
     2.3 @@ -16,7 +16,7 @@
     2.4    val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
     2.5    type compile_generator =
     2.6      Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
     2.7 -  val generator_test_goal_terms : compile_generator -> Proof.context -> (string * typ) list
     2.8 +  val generator_test_goal_terms : compile_generator -> Proof.context -> bool -> (string * typ) list
     2.9      -> (term * term list) list -> Quickcheck.result list
    2.10    val ensure_sort_datatype:
    2.11      ((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list
    2.12 @@ -27,7 +27,7 @@
    2.13       -> Proof.context -> (term * term list) list -> term
    2.14    val mk_fun_upd : typ -> typ -> term * term -> term -> term
    2.15    val post_process_term : term -> term
    2.16 -  val test_term : compile_generator -> Proof.context -> term * term list -> Quickcheck.result
    2.17 +  val test_term : compile_generator -> Proof.context -> bool -> term * term list -> Quickcheck.result
    2.18  end;
    2.19  
    2.20  structure Quickcheck_Common : QUICKCHECK_COMMON =
    2.21 @@ -61,7 +61,7 @@
    2.22    let val ({cpu, ...}, result) = Timing.timing e ()
    2.23    in (result, (description, Time.toMilliseconds cpu)) end
    2.24  
    2.25 -fun test_term compile ctxt (t, eval_terms) =
    2.26 +fun test_term compile ctxt catch_code_errors (t, eval_terms) =
    2.27    let
    2.28      val _ = check_test_term t
    2.29      val names = Term.add_free_names t []
    2.30 @@ -83,8 +83,9 @@
    2.31          in
    2.32            case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q
    2.33          end;
    2.34 +    val act = if catch_code_errors then try else (fn f => SOME o f) 
    2.35      val (test_fun, comp_time) = cpu_time "quickcheck compilation"
    2.36 -        (fn () => try (compile ctxt) [(t, eval_terms)]);
    2.37 +        (fn () => act (compile ctxt) [(t, eval_terms)]);
    2.38      val _ = Quickcheck.add_timing comp_time current_result
    2.39    in
    2.40      case test_fun of
    2.41 @@ -135,7 +136,7 @@
    2.42    end
    2.43  
    2.44  
    2.45 -fun test_term_with_increasing_cardinality compile ctxt ts =
    2.46 +fun test_term_with_increasing_cardinality compile ctxt catch_code_errors ts =
    2.47    let
    2.48      val thy = Proof_Context.theory_of ctxt
    2.49      val (ts', eval_terms) = split_list ts
    2.50 @@ -161,7 +162,8 @@
    2.51          (* size does matter *)
    2.52          map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size))
    2.53          |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
    2.54 -    val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => try (compile ctxt) ts)
    2.55 +    val act = if catch_code_errors then try else (fn f => SOME o f)
    2.56 +    val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => act (compile ctxt) ts)
    2.57      val _ = Quickcheck.add_timing comp_time current_result
    2.58    in
    2.59      case test_fun of
    2.60 @@ -245,19 +247,19 @@
    2.61      SOME (lhs, rhs) => (t, eval_terms @ [rhs, lhs])
    2.62    | NONE => (t, eval_terms)
    2.63  
    2.64 -fun generator_test_goal_terms compile ctxt insts goals =
    2.65 +fun generator_test_goal_terms compile ctxt catch_code_errors insts goals =
    2.66    let
    2.67      fun test_term' goal =
    2.68        case goal of
    2.69 -        [(NONE, t)] => test_term compile ctxt t
    2.70 -      | ts => test_term_with_increasing_cardinality compile ctxt (map snd ts)
    2.71 +        [(NONE, t)] => test_term compile ctxt catch_code_errors t
    2.72 +      | ts => test_term_with_increasing_cardinality compile ctxt catch_code_errors (map snd ts)
    2.73      val goals' = instantiate_goals ctxt insts goals
    2.74        |> map (map (apsnd add_equation_eval_terms))
    2.75    in
    2.76      if Config.get ctxt Quickcheck.finite_types then
    2.77        collect_results test_term' goals' []
    2.78      else
    2.79 -      collect_results (test_term compile ctxt)
    2.80 +      collect_results (test_term compile ctxt catch_code_errors)
    2.81          (maps (map snd) goals') []
    2.82    end;
    2.83  
     3.1 --- a/src/Tools/quickcheck.ML	Wed Nov 09 11:34:57 2011 +0100
     3.2 +++ b/src/Tools/quickcheck.ML	Wed Nov 09 11:34:59 2011 +0100
     3.3 @@ -50,7 +50,7 @@
     3.4    val timings_of : result -> (string * int) list
     3.5    (* registering testers & generators *) 
     3.6    type tester =
     3.7 -    Proof.context -> (string * typ) list -> (term * term list) list -> result list
     3.8 +    Proof.context -> bool -> (string * typ) list -> (term * term list) list -> result list
     3.9    val add_tester : string * (bool Config.T * tester) -> Context.generic -> Context.generic
    3.10    val add_batch_generator :
    3.11      string * (Proof.context -> term list -> (int -> term list option) list)
    3.12 @@ -192,7 +192,7 @@
    3.13      (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
    3.14  
    3.15  type tester =
    3.16 -  Proof.context -> (string * typ) list -> (term * term list) list -> result list
    3.17 +  Proof.context -> bool -> (string * typ) list -> (term * term list) list -> result list
    3.18  
    3.19  structure Data = Generic_Data
    3.20  (
    3.21 @@ -288,7 +288,7 @@
    3.22      [] => error "No active testers for quickcheck"
    3.23    | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
    3.24        (fn () => Par_List.get_some (fn tester =>
    3.25 -      tester ctxt insts goals |>
    3.26 +      tester ctxt (length testers > 1) insts goals |>
    3.27        (fn result => if exists found_counterexample result then SOME result else NONE)) testers)
    3.28        (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ();
    3.29