more precise messages with the tester's name in quickcheck; tuned
authorbulwahn
Wed Nov 09 11:35:09 2011 +0100 (2011-11-09)
changeset 45420d17556b9a89b
parent 45419 10ba32c347b0
child 45421 2bef6da4a6a6
child 45438 1006cba234e3
more precise messages with the tester's name in quickcheck; tuned
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/Quickcheck/random_generators.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Nov 09 11:34:59 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Nov 09 11:35:09 2011 +0100
     1.3 @@ -488,7 +488,7 @@
     1.4        thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
     1.5    end;
     1.6  
     1.7 -val test_goals = Quickcheck_Common.generator_test_goal_terms compile_generator_expr;
     1.8 +val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive", compile_generator_expr);
     1.9    
    1.10  (* setup *)
    1.11  
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Nov 09 11:34:59 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Nov 09 11:35:09 2011 +0100
     2.3 @@ -263,7 +263,7 @@
     2.4              (NONE, !current_result)
     2.5            else
     2.6              let
     2.7 -              val _ = message ("[Quickcheck-Narrowing] Test data size: " ^ string_of_int k)
     2.8 +              val _ = message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
     2.9                val _ = current_size := k
    2.10                val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
    2.11                  (fn () => Isabelle_System.bash_output (executable ^ " " ^ string_of_int k))
     3.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Nov 09 11:34:59 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Nov 09 11:35:09 2011 +0100
     3.3 @@ -16,7 +16,8 @@
     3.4    val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
     3.5    type compile_generator =
     3.6      Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
     3.7 -  val generator_test_goal_terms : compile_generator -> Proof.context -> bool -> (string * typ) list
     3.8 +  val generator_test_goal_terms :
     3.9 +    string * compile_generator -> Proof.context -> bool -> (string * typ) list
    3.10      -> (term * term list) list -> Quickcheck.result list
    3.11    val ensure_sort_datatype:
    3.12      ((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list
    3.13 @@ -27,7 +28,8 @@
    3.14       -> Proof.context -> (term * term list) list -> term
    3.15    val mk_fun_upd : typ -> typ -> term * term -> term -> term
    3.16    val post_process_term : term -> term
    3.17 -  val test_term : compile_generator -> Proof.context -> bool -> term * term list -> Quickcheck.result
    3.18 +  val test_term : string * compile_generator
    3.19 +    -> Proof.context -> bool -> term * term list -> Quickcheck.result
    3.20  end;
    3.21  
    3.22  structure Quickcheck_Common : QUICKCHECK_COMMON =
    3.23 @@ -61,7 +63,7 @@
    3.24    let val ({cpu, ...}, result) = Timing.timing e ()
    3.25    in (result, (description, Time.toMilliseconds cpu)) end
    3.26  
    3.27 -fun test_term compile ctxt catch_code_errors (t, eval_terms) =
    3.28 +fun test_term (name, compile) ctxt catch_code_errors (t, eval_terms) =
    3.29    let
    3.30      val _ = check_test_term t
    3.31      val names = Term.add_free_names t []
    3.32 @@ -74,7 +76,8 @@
    3.33          NONE
    3.34        else
    3.35          let
    3.36 -          val _ = Quickcheck.message ctxt ("Test data size: " ^ string_of_int k)
    3.37 +          val _ = Quickcheck.message ctxt
    3.38 +            ("[Quickcheck-" ^ name ^ "]Test data size: " ^ string_of_int k)
    3.39            val _ = current_size := k
    3.40            val ((result, report), timing) =
    3.41              cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1])
    3.42 @@ -89,7 +92,8 @@
    3.43      val _ = Quickcheck.add_timing comp_time current_result
    3.44    in
    3.45      case test_fun of
    3.46 -      NONE => (Quickcheck.message ctxt "Conjecture is not executable with quickcheck"; !current_result)
    3.47 +      NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
    3.48 +        !current_result)
    3.49      | SOME test_fun =>
    3.50        let
    3.51          val (response, exec_time) =
    3.52 @@ -109,7 +113,8 @@
    3.53        if k > size then true
    3.54        else if tester k then with_size tester (k + 1) else false
    3.55      val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
    3.56 -        Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
    3.57 +        Option.map (map (fn test_fun =>
    3.58 +          TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
    3.59                (fn () => with_size test_fun 1) ()
    3.60               handle TimeLimit.TimeOut => true)) test_funs)
    3.61    in
    3.62 @@ -127,7 +132,8 @@
    3.63        if k > size then NONE
    3.64        else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
    3.65      val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
    3.66 -        Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
    3.67 +        Option.map (map (fn test_fun =>
    3.68 +          TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
    3.69                (fn () => with_size test_fun 1) ()
    3.70               handle TimeLimit.TimeOut => NONE)) test_funs)
    3.71    in
    3.72 @@ -136,7 +142,7 @@
    3.73    end
    3.74  
    3.75  
    3.76 -fun test_term_with_increasing_cardinality compile ctxt catch_code_errors ts =
    3.77 +fun test_term_with_cardinality (name, compile) ctxt catch_code_errors ts =
    3.78    let
    3.79      val thy = Proof_Context.theory_of ctxt
    3.80      val (ts', eval_terms) = split_list ts
    3.81 @@ -167,7 +173,8 @@
    3.82      val _ = Quickcheck.add_timing comp_time current_result
    3.83    in
    3.84      case test_fun of
    3.85 -      NONE => (Quickcheck.message ctxt "Conjecture is not executable with quickcheck"; !current_result)
    3.86 +      NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
    3.87 +        !current_result)
    3.88      | SOME test_fun =>
    3.89        let
    3.90          val _ = case get_first (test_card_size test_fun) enumeration_card_size of
    3.91 @@ -207,14 +214,14 @@
    3.92      fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
    3.93      val thy = Proof_Context.theory_of lthy
    3.94      val default_insts =
    3.95 -      if Config.get lthy Quickcheck.finite_types then (get_finite_types lthy) else (Quickcheck.default_type lthy)
    3.96 +      if Config.get lthy Quickcheck.finite_types then get_finite_types else Quickcheck.default_type
    3.97      val inst_goals =
    3.98        map (fn (check_goal, eval_terms) =>
    3.99          if not (null (Term.add_tfree_names check_goal [])) then
   3.100            map (fn T =>
   3.101              (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy))
   3.102                (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
   3.103 -              handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts
   3.104 +              handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts lthy)
   3.105          else
   3.106            [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals
   3.107      val error_msg =
   3.108 @@ -247,19 +254,19 @@
   3.109      SOME (lhs, rhs) => (t, eval_terms @ [rhs, lhs])
   3.110    | NONE => (t, eval_terms)
   3.111  
   3.112 -fun generator_test_goal_terms compile ctxt catch_code_errors insts goals =
   3.113 +fun generator_test_goal_terms (name, compile) ctxt catch_code_errors insts goals =
   3.114    let
   3.115      fun test_term' goal =
   3.116        case goal of
   3.117 -        [(NONE, t)] => test_term compile ctxt catch_code_errors t
   3.118 -      | ts => test_term_with_increasing_cardinality compile ctxt catch_code_errors (map snd ts)
   3.119 +        [(NONE, t)] => test_term (name, compile) ctxt catch_code_errors t
   3.120 +      | ts => test_term_with_cardinality (name, compile) ctxt catch_code_errors (map snd ts)
   3.121      val goals' = instantiate_goals ctxt insts goals
   3.122        |> map (map (apsnd add_equation_eval_terms))
   3.123    in
   3.124      if Config.get ctxt Quickcheck.finite_types then
   3.125        collect_results test_term' goals' []
   3.126      else
   3.127 -      collect_results (test_term compile ctxt catch_code_errors)
   3.128 +      collect_results (test_term (name, compile) ctxt catch_code_errors)
   3.129          (maps (map snd) goals') []
   3.130    end;
   3.131  
   3.132 @@ -411,6 +418,5 @@
   3.133          | NONE => process_args t)
   3.134      | _ => process_args t
   3.135    end
   3.136 -  
   3.137  
   3.138  end;
     4.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Nov 09 11:34:59 2011 +0100
     4.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Nov 09 11:35:09 2011 +0100
     4.3 @@ -438,7 +438,7 @@
     4.4        end
     4.5    end;
     4.6  
     4.7 -val test_goals = Quickcheck_Common.generator_test_goal_terms compile_generator_expr;
     4.8 +val test_goals = Quickcheck_Common.generator_test_goal_terms ("random", compile_generator_expr);
     4.9    
    4.10  (** setup **)
    4.11