moving iteration of tests to the testers in quickcheck
authorbulwahn
Fri Dec 03 08:40:47 2010 +0100 (2010-12-03)
changeset 409117febf76e0a69
parent 40910 508c83827364
child 40912 1108529100ce
moving iteration of tests to the testers in quickcheck
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/smallvalue_generators.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Dec 03 08:40:47 2010 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Dec 03 08:40:47 2010 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4    val add : string option -> int option -> attribute
     1.5    val test_fn : (int * int * int -> term list option) Unsynchronized.ref
     1.6    val test_term:
     1.7 -    Proof.context -> term -> int -> term list option * (bool list * bool)
     1.8 +    Proof.context -> term -> int -> term list option * Quickcheck.report option
     1.9    val setup : theory -> theory
    1.10    val quickcheck_setup : theory -> theory
    1.11  end;
    1.12 @@ -842,10 +842,9 @@
    1.13      val start = Config.get ctxt depth_start;
    1.14      val offset = Config.get ctxt size_offset;
    1.15      val test_fn' = !test_fn;
    1.16 -    val dummy_report = ([], false)
    1.17      fun test k = (deepen bound (fn i =>
    1.18        (Output.urgent_message ("Search depth: " ^ string_of_int i);
    1.19 -       test_fn' (i, values, k+offset))) start, dummy_report);
    1.20 +       test_fn' (i, values, k+offset))) start, NONE);
    1.21    in test end;
    1.22  
    1.23  val quickcheck_setup =
     2.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Fri Dec 03 08:40:47 2010 +0100
     2.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Dec 03 08:40:47 2010 +0100
     2.3 @@ -17,7 +17,7 @@
     2.4        string list * string list -> typ list * typ list -> theory -> theory)
     2.5      -> Datatype.config -> string list -> theory -> theory
     2.6    val compile_generator_expr:
     2.7 -    Proof.context -> term -> int -> term list option * (bool list * bool)
     2.8 +    Proof.context -> term -> int -> term list option * Quickcheck.report option
     2.9    val put_counterexample: (unit -> int -> seed -> term list option * seed)
    2.10      -> Proof.context -> Proof.context
    2.11    val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed)
    2.12 @@ -387,25 +387,73 @@
    2.13      Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
    2.14    end
    2.15  
    2.16 +(* single quickcheck report *)
    2.17 +
    2.18 +datatype single_report = Run of bool list * bool | MatchExc
    2.19 +
    2.20 +fun collect_single_report single_report
    2.21 +    (Quickcheck.Report {iterations = iterations, raised_match_errors = raised_match_errors,
    2.22 +    satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
    2.23 +  case single_report
    2.24 +  of MatchExc =>
    2.25 +    Quickcheck.Report {iterations = iterations + 1, raised_match_errors = raised_match_errors + 1,
    2.26 +      satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}
    2.27 +   | Run (assms, concl) =>
    2.28 +    Quickcheck.Report {iterations = iterations + 1, raised_match_errors = raised_match_errors,
    2.29 +      satisfied_assms =
    2.30 +        map2 (fn b => fn s => if b then s + 1 else s) assms
    2.31 +         (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
    2.32 +      positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
    2.33 +
    2.34 +val empty_report = Quickcheck.Report { iterations = 0, raised_match_errors = 0,
    2.35 +  satisfied_assms = [], positive_concl_tests = 0 }
    2.36 +    
    2.37  fun compile_generator_expr ctxt t =
    2.38    let
    2.39      val Ts = (map snd o fst o strip_abs) t;
    2.40      val thy = ProofContext.theory_of ctxt
    2.41 -  in if Config.get ctxt Quickcheck.report then
    2.42 -    let
    2.43 -      val t' = mk_reporting_generator_expr thy t Ts;
    2.44 -      val compile = Code_Runtime.dynamic_value_strict
    2.45 -        (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
    2.46 -        thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
    2.47 -    in compile #> Random_Engine.run end
    2.48 -  else
    2.49 -    let
    2.50 -      val t' = mk_generator_expr thy t Ts;
    2.51 -      val compile = Code_Runtime.dynamic_value_strict
    2.52 -        (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
    2.53 -        thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
    2.54 -      val dummy_report = ([], false)
    2.55 -    in compile #> Random_Engine.run #> rpair dummy_report end
    2.56 +    val iterations = Config.get ctxt Quickcheck.iterations
    2.57 +  in
    2.58 +    if Config.get ctxt Quickcheck.report then
    2.59 +      let
    2.60 +        val t' = mk_reporting_generator_expr thy t Ts;
    2.61 +        val compile = Code_Runtime.dynamic_value_strict
    2.62 +          (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
    2.63 +          thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
    2.64 +        val single_tester = compile #> Random_Engine.run
    2.65 +        fun iterate_and_collect size 0 report = (NONE, report)
    2.66 +          | iterate_and_collect size j report =
    2.67 +            let
    2.68 +              val (test_result, single_report) = apsnd Run (single_tester size) handle Match => 
    2.69 +                (if Config.get ctxt Quickcheck.quiet then ()
    2.70 +                 else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
    2.71 +              val report = collect_single_report single_report report
    2.72 +            in
    2.73 +              case test_result of NONE => iterate_and_collect size (j - 1) report
    2.74 +                | SOME q => (SOME q, report)
    2.75 +            end
    2.76 +      in
    2.77 +        fn size => apsnd SOME (iterate_and_collect size iterations empty_report)
    2.78 +      end
    2.79 +    else
    2.80 +      let
    2.81 +        val t' = mk_generator_expr thy t Ts;
    2.82 +        val compile = Code_Runtime.dynamic_value_strict
    2.83 +          (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
    2.84 +          thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
    2.85 +        val single_tester = compile #> Random_Engine.run
    2.86 +        fun iterate size 0 = NONE
    2.87 +          | iterate size j =
    2.88 +            let
    2.89 +              val result = single_tester size handle Match => 
    2.90 +                (if Config.get ctxt Quickcheck.quiet then ()
    2.91 +                 else warning "Exception Match raised during quickcheck"; NONE)
    2.92 +            in
    2.93 +              case result of NONE => iterate size (j - 1) | SOME q => SOME q
    2.94 +            end
    2.95 +      in
    2.96 +        fn size => (rpair NONE (iterate size iterations))
    2.97 +      end
    2.98    end;
    2.99  
   2.100  
     3.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:47 2010 +0100
     3.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:47 2010 +0100
     3.3 @@ -7,7 +7,7 @@
     3.4  signature SMALLVALUE_GENERATORS =
     3.5  sig
     3.6    val compile_generator_expr:
     3.7 -    Proof.context -> term -> int -> term list option * (bool list * bool)
     3.8 +    Proof.context -> term -> int -> term list option * Quickcheck.report option
     3.9    val put_counterexample: (unit -> int -> term list option)
    3.10      -> Proof.context -> Proof.context
    3.11    val smart_quantifier : bool Config.T;
    3.12 @@ -272,19 +272,15 @@
    3.13    in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
    3.14  
    3.15  fun compile_generator_expr ctxt t =
    3.16 -  if Config.get ctxt Quickcheck.report then
    3.17 -    error "Compilation with reporting facility is not supported"
    3.18 -  else
    3.19 -    let
    3.20 -      val thy = ProofContext.theory_of ctxt
    3.21 -      val t' =
    3.22 -        (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
    3.23 -          ctxt t;
    3.24 -      val compile = Code_Runtime.dynamic_value_strict
    3.25 -        (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
    3.26 -        thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
    3.27 -      val dummy_report = ([], false)
    3.28 -    in compile #> rpair dummy_report end;
    3.29 +  let
    3.30 +    val thy = ProofContext.theory_of ctxt
    3.31 +    val t' =
    3.32 +      (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
    3.33 +        ctxt t;
    3.34 +    val compile = Code_Runtime.dynamic_value_strict
    3.35 +      (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
    3.36 +      thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
    3.37 +  in fn size => rpair NONE (compile size) end;
    3.38  
    3.39  (** setup **)
    3.40  
     4.1 --- a/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
     4.2 +++ b/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
     4.3 @@ -28,7 +28,7 @@
     4.4    val map_test_params : (typ list * expectation -> typ list * expectation)
     4.5      -> Context.generic -> Context.generic
     4.6    val add_generator:
     4.7 -    string * (Proof.context -> term -> int -> term list option * (bool list * bool))
     4.8 +    string * (Proof.context -> term -> int -> term list option * report option)
     4.9        -> Context.generic -> Context.generic
    4.10    (* testing terms and proof states *)
    4.11    val test_term: Proof.context -> bool -> term ->
    4.12 @@ -57,26 +57,10 @@
    4.13  
    4.14  (* quickcheck report *)
    4.15  
    4.16 -datatype single_report = Run of bool list * bool | MatchExc
    4.17 -
    4.18  datatype report = Report of
    4.19    { iterations : int, raised_match_errors : int,
    4.20      satisfied_assms : int list, positive_concl_tests : int }
    4.21  
    4.22 -fun collect_single_report single_report
    4.23 -    (Report {iterations = iterations, raised_match_errors = raised_match_errors,
    4.24 -    satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
    4.25 -  case single_report
    4.26 -  of MatchExc =>
    4.27 -    Report {iterations = iterations + 1, raised_match_errors = raised_match_errors + 1,
    4.28 -      satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}
    4.29 -   | Run (assms, concl) =>
    4.30 -    Report {iterations = iterations + 1, raised_match_errors = raised_match_errors,
    4.31 -      satisfied_assms =
    4.32 -        map2 (fn b => fn s => if b then s + 1 else s) assms
    4.33 -         (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
    4.34 -      positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
    4.35 -
    4.36  (* expectation *)
    4.37  
    4.38  datatype expectation = No_Expectation | No_Counterexample | Counterexample; 
    4.39 @@ -116,7 +100,7 @@
    4.40  structure Data = Generic_Data
    4.41  (
    4.42    type T =
    4.43 -    (string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list
    4.44 +    (string * (Proof.context -> term -> int -> term list option * report option)) list
    4.45        * test_params;
    4.46    val empty = ([], Test_Params {default_type = [], expect = No_Expectation});
    4.47    val extend = I;
    4.48 @@ -172,11 +156,6 @@
    4.49      val result = Exn.capture f ()
    4.50      val time = Time.toMilliseconds (#cpu (end_timing start))
    4.51    in (Exn.release result, (description, time)) end
    4.52 -
    4.53 -(* we actually assume we know the generators and its behaviour *)
    4.54 -fun is_iteratable "SML" = true
    4.55 -  | is_iteratable "random" = true
    4.56 -  | is_iteratable _ = false
    4.57    
    4.58  fun test_term ctxt is_interactive t =
    4.59    let
    4.60 @@ -185,30 +164,18 @@
    4.61      fun excipit s =
    4.62        "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
    4.63      val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt t');
    4.64 -    fun iterate f 0 report = (NONE, report)
    4.65 -      | iterate f j report =
    4.66 +    fun with_size test_fun k reports =
    4.67 +      if k > Config.get ctxt size then
    4.68 +        (NONE, reports)
    4.69 +      else
    4.70          let
    4.71 -          val (test_result, single_report) = apsnd Run (f ()) handle Match => 
    4.72 -            (if Config.get ctxt quiet then ()
    4.73 -             else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
    4.74 -          val report = collect_single_report single_report report
    4.75 -        in
    4.76 -          case test_result of NONE => iterate f (j - 1) report | SOME q => (SOME q, report)
    4.77 -        end
    4.78 -    val empty_report = Report { iterations = 0, raised_match_errors = 0,
    4.79 -      satisfied_assms = [], positive_concl_tests = 0 }
    4.80 -    fun with_size test_fun k reports =
    4.81 -      if k > Config.get ctxt size then (NONE, reports)
    4.82 -      else
    4.83 -       (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
    4.84 -        let
    4.85 +          val _ = if Config.get ctxt quiet then () else Output.urgent_message
    4.86 +            ("Test data size: " ^ string_of_int k)
    4.87            val _ = current_size := k
    4.88 -          val niterations =
    4.89 -            if is_iteratable (Config.get ctxt tester) then Config.get ctxt iterations else 1
    4.90 -          val ((result, new_report), timing) = cpu_time ("size " ^ string_of_int k)
    4.91 -            (fn () => iterate (fn () => test_fun (k - 1)) niterations empty_report)
    4.92 -          val reports = ((k, new_report) :: reports)
    4.93 -        in case result of NONE => with_size test_fun (k + 1) reports | SOME q => (SOME q, reports) end);
    4.94 +          val ((result, new_report), timing) =
    4.95 +            cpu_time ("size " ^ string_of_int k) (fn () => test_fun (k - 1))
    4.96 +          val reports = case new_report of NONE => reports | SOME rep => (k, rep) :: reports
    4.97 +        in case result of NONE => with_size test_fun (k + 1) reports | SOME q => (SOME q, reports) end;
    4.98    in
    4.99      case test_fun of NONE => (NONE, ([comp_time], NONE)) 
   4.100        | SOME test_fun =>