8 sig |
8 sig |
9 val setup: theory -> theory |
9 val setup: theory -> theory |
10 (* configuration *) |
10 (* configuration *) |
11 val auto: bool Unsynchronized.ref |
11 val auto: bool Unsynchronized.ref |
12 val timing : bool Unsynchronized.ref |
12 val timing : bool Unsynchronized.ref |
|
13 val size : int Config.T |
|
14 val iterations : int Config.T |
|
15 val no_assms : bool Config.T |
|
16 val report : bool Config.T |
|
17 val quiet : bool Config.T |
|
18 val timeout : real Config.T |
13 datatype report = Report of |
19 datatype report = Report of |
14 { iterations : int, raised_match_errors : int, |
20 { iterations : int, raised_match_errors : int, |
15 satisfied_assms : int list, positive_concl_tests : int } |
21 satisfied_assms : int list, positive_concl_tests : int } |
16 datatype expectation = No_Expectation | No_Counterexample | Counterexample; |
22 datatype expectation = No_Expectation | No_Counterexample | Counterexample; |
17 datatype test_params = Test_Params of |
23 datatype test_params = Test_Params of {default_type: typ list, expect : expectation}; |
18 { size: int, iterations: int, default_type: typ list, no_assms: bool, |
|
19 expect : expectation, report: bool, quiet : bool, timeout : real}; |
|
20 val test_params_of : Proof.context -> test_params |
24 val test_params_of : Proof.context -> test_params |
21 val report : Proof.context -> bool |
25 val map_test_params : (typ list * expectation -> typ list * expectation) |
22 val map_test_params : |
|
23 ((int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real))) |
|
24 -> (int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real)))) |
|
25 -> Context.generic -> Context.generic |
26 -> Context.generic -> Context.generic |
26 val add_generator: |
27 val add_generator: |
27 string * (Proof.context -> term -> int -> term list option * (bool list * bool)) |
28 string * (Proof.context -> term -> int -> term list option * (bool list * bool)) |
28 -> Context.generic -> Context.generic |
29 -> Context.generic -> Context.generic |
29 (* testing terms and proof states *) |
30 (* testing terms and proof states *) |
78 |
79 |
79 fun merge_expectation (expect1, expect2) = |
80 fun merge_expectation (expect1, expect2) = |
80 if expect1 = expect2 then expect1 else No_Expectation |
81 if expect1 = expect2 then expect1 else No_Expectation |
81 |
82 |
82 (* quickcheck configuration -- default parameters, test generators *) |
83 (* quickcheck configuration -- default parameters, test generators *) |
83 |
84 val (size, setup_size) = Attrib.config_int "quickcheck_size" (K 10) |
|
85 val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100) |
|
86 val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false) |
|
87 val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true) |
|
88 val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false) |
|
89 val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0) |
|
90 |
|
91 val setup_config = |
|
92 setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet #> setup_timeout |
|
93 |
84 datatype test_params = Test_Params of |
94 datatype test_params = Test_Params of |
85 { size: int, iterations: int, default_type: typ list, no_assms: bool, |
95 {default_type: typ list, expect : expectation}; |
86 expect : expectation, report: bool, quiet : bool, timeout : real}; |
96 |
87 |
97 fun dest_test_params (Test_Params {default_type, expect}) = (default_type, expect); |
88 fun dest_test_params |
98 |
89 (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) = |
99 fun make_test_params (default_type, expect) = Test_Params {default_type = default_type, expect = expect}; |
90 ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))); |
100 |
91 |
101 fun map_test_params' f (Test_Params {default_type, expect}) = make_test_params (f (default_type, expect)); |
92 fun make_test_params |
|
93 ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))) = |
|
94 Test_Params { size = size, iterations = iterations, default_type = default_type, |
|
95 no_assms = no_assms, expect = expect, report = report, quiet = quiet, timeout = timeout }; |
|
96 |
|
97 fun map_test_params' f |
|
98 (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) = |
|
99 make_test_params |
|
100 (f ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout))))); |
|
101 |
102 |
102 fun merge_test_params |
103 fun merge_test_params |
103 (Test_Params { size = size1, iterations = iterations1, default_type = default_type1, |
104 (Test_Params {default_type = default_type1, expect = expect1}, |
104 no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1, timeout = timeout1 }, |
105 Test_Params {default_type = default_type2, expect = expect2}) = |
105 Test_Params { size = size2, iterations = iterations2, default_type = default_type2, |
106 make_test_params (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2)); |
106 no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2, timeout = timeout2}) = |
|
107 make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)), |
|
108 ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2), |
|
109 ((merge_expectation (expect1, expect2), report1 orelse report2), |
|
110 (quiet1 orelse quiet2, Real.min (timeout1, timeout2))))); |
|
111 |
107 |
112 structure Data = Generic_Data |
108 structure Data = Generic_Data |
113 ( |
109 ( |
114 type T = |
110 type T = |
115 (string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list |
111 (string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list |
116 * test_params; |
112 * test_params; |
117 val empty = ([], Test_Params |
113 val empty = ([], Test_Params {default_type = [], expect = No_Expectation}); |
118 { size = 10, iterations = 100, default_type = [], no_assms = false, |
|
119 expect = No_Expectation, report = false, quiet = false, timeout = 30.0}); |
|
120 val extend = I; |
114 val extend = I; |
121 fun merge ((generators1, params1), (generators2, params2)) : T = |
115 fun merge ((generators1, params1), (generators2, params2)) : T = |
122 (AList.merge (op =) (K true) (generators1, generators2), |
116 (AList.merge (op =) (K true) (generators1, generators2), |
123 merge_test_params (params1, params2)); |
117 merge_test_params (params1, params2)); |
124 ); |
118 ); |
125 |
119 |
126 val test_params_of = snd o Data.get o Context.Proof; |
120 val test_params_of = snd o Data.get o Context.Proof; |
127 |
121 |
128 val size = fst o fst o dest_test_params o test_params_of |
122 val default_type = fst o dest_test_params o test_params_of |
129 |
123 |
130 val iterations = snd o fst o dest_test_params o test_params_of |
124 val expect = snd o dest_test_params o test_params_of |
131 |
|
132 val default_type = fst o fst o snd o dest_test_params o test_params_of |
|
133 |
|
134 val no_assms = snd o fst o snd o dest_test_params o test_params_of |
|
135 |
|
136 val expect = fst o fst o snd o snd o dest_test_params o test_params_of |
|
137 |
|
138 val report = snd o fst o snd o snd o dest_test_params o test_params_of |
|
139 |
|
140 val quiet = fst o snd o snd o snd o dest_test_params o test_params_of |
|
141 |
|
142 val timeout = snd o snd o snd o snd o dest_test_params o test_params_of |
|
143 |
|
144 fun map_report f |
|
145 (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) = |
|
146 make_test_params |
|
147 ((size, iterations), ((default_type, no_assms), ((expect, f report), (quiet, timeout)))); |
|
148 |
|
149 fun map_quiet f |
|
150 (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) = |
|
151 make_test_params |
|
152 ((size, iterations), ((default_type, no_assms), ((expect, report), (f quiet, timeout)))); |
|
153 |
|
154 fun set_report report = Data.map (apsnd (map_report (K report))) |
|
155 |
|
156 fun set_quiet quiet = Data.map (apsnd (map_quiet (K quiet))) |
|
157 |
125 |
158 val map_test_params = Data.map o apsnd o map_test_params' |
126 val map_test_params = Data.map o apsnd o map_test_params' |
159 |
127 |
160 val add_generator = Data.map o apfst o AList.update (op =); |
128 val add_generator = Data.map o apfst o AList.update (op =); |
161 |
129 |
208 val (tester, comp_time) = cpu_time "compilation" |
176 val (tester, comp_time) = cpu_time "compilation" |
209 (fn () => the (AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) "small") ctxt t'); |
177 (fn () => the (AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) "small") ctxt t'); |
210 val empty_report = Report { iterations = 0, raised_match_errors = 0, |
178 val empty_report = Report { iterations = 0, raised_match_errors = 0, |
211 satisfied_assms = [], positive_concl_tests = 0 } |
179 satisfied_assms = [], positive_concl_tests = 0 } |
212 fun with_size k timings = |
180 fun with_size k timings = |
213 if k > size ctxt then (NONE, timings) |
181 if k > Config.get ctxt size then (NONE, timings) |
214 else |
182 else |
215 let |
183 let |
216 val _ = if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k); |
184 val _ = if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k); |
217 val _ = current_size := k |
185 val _ = current_size := k |
218 val (result, timing) = cpu_time ("size " ^ string_of_int k) (fn () => (fst (tester k)) handle Match => (if quiet ctxt then () |
186 val (result, timing) = cpu_time ("size " ^ string_of_int k) |
|
187 (fn () => (fst (tester k)) handle Match => (if Config.get ctxt quiet then () |
219 else warning "Exception Match raised during quickcheck"; NONE)) |
188 else warning "Exception Match raised during quickcheck"; NONE)) |
220 in |
189 in |
221 case result of |
190 case result of |
222 NONE => with_size (k + 1) (timing :: timings) |
191 NONE => with_size (k + 1) (timing :: timings) |
223 | SOME q => (SOME q, (timing :: timings)) |
192 | SOME q => (SOME q, (timing :: timings)) |
233 val current_size = Unsynchronized.ref 0 |
202 val current_size = Unsynchronized.ref 0 |
234 fun excipit s = |
203 fun excipit s = |
235 "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size) |
204 "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size) |
236 val (testers, comp_time) = cpu_time "quickcheck compilation" |
205 val (testers, comp_time) = cpu_time "quickcheck compilation" |
237 (fn () => (case generator_name |
206 (fn () => (case generator_name |
238 of NONE => if quiet ctxt then mk_testers ctxt t' else mk_testers_strict ctxt t' |
207 of NONE => if Config.get ctxt quiet then mk_testers ctxt t' else mk_testers_strict ctxt t' |
239 | SOME name => [mk_tester_select name ctxt t'])); |
208 | SOME name => [mk_tester_select name ctxt t'])); |
240 fun iterate f 0 report = (NONE, report) |
209 fun iterate f 0 report = (NONE, report) |
241 | iterate f j report = |
210 | iterate f j report = |
242 let |
211 let |
243 val (test_result, single_report) = apsnd Run (f ()) handle Match => (if quiet ctxt then () |
212 val (test_result, single_report) = apsnd Run (f ()) handle Match => |
|
213 (if Config.get ctxt quiet then () |
244 else warning "Exception Match raised during quickcheck"; (NONE, MatchExc)) |
214 else warning "Exception Match raised during quickcheck"; (NONE, MatchExc)) |
245 val report = collect_single_report single_report report |
215 val report = collect_single_report single_report report |
246 in |
216 in |
247 case test_result of NONE => iterate f (j - 1) report | SOME q => (SOME q, report) |
217 case test_result of NONE => iterate f (j - 1) report | SOME q => (SOME q, report) |
248 end |
218 end |
249 val empty_report = Report { iterations = 0, raised_match_errors = 0, |
219 val empty_report = Report { iterations = 0, raised_match_errors = 0, |
250 satisfied_assms = [], positive_concl_tests = 0 } |
220 satisfied_assms = [], positive_concl_tests = 0 } |
251 fun with_testers k [] = (NONE, []) |
221 fun with_testers k [] = (NONE, []) |
252 | with_testers k (tester :: testers) = |
222 | with_testers k (tester :: testers) = |
253 case iterate (fn () => tester (k - 1)) (iterations ctxt) empty_report |
223 case iterate (fn () => tester (k - 1)) (Config.get ctxt iterations) empty_report |
254 of (NONE, report) => apsnd (cons report) (with_testers k testers) |
224 of (NONE, report) => apsnd (cons report) (with_testers k testers) |
255 | (SOME q, report) => (SOME q, [report]); |
225 | (SOME q, report) => (SOME q, [report]); |
256 fun with_size k reports = |
226 fun with_size k reports = |
257 if k > size ctxt then (NONE, reports) |
227 if k > Config.get ctxt size then (NONE, reports) |
258 else |
228 else |
259 (if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k); |
229 (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k); |
260 let |
230 let |
261 val _ = current_size := k |
231 val _ = current_size := k |
262 val (result, new_report) = with_testers k testers |
232 val (result, new_report) = with_testers k testers |
263 val reports = ((k, new_report) :: reports) |
233 val reports = ((k, new_report) :: reports) |
264 in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end); |
234 in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end); |
265 val ((result, reports), exec_time) = |
235 val ((result, reports), exec_time) = |
266 TimeLimit.timeLimit (seconds (timeout ctxt)) (fn () => cpu_time "quickcheck execution" |
236 TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () => cpu_time "quickcheck execution" |
267 (fn () => apfst |
237 (fn () => apfst |
268 (fn result => case result of NONE => NONE |
238 (fn result => case result of NONE => NONE |
269 | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) () |
239 | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) () |
270 handle TimeLimit.TimeOut => |
240 handle TimeLimit.TimeOut => |
271 error (excipit "ran out of time") |
241 error (excipit "ran out of time") |
272 | Exn.Interrupt => error (excipit "was interrupted") (* FIXME violates Isabelle/ML exception model *) |
242 | Exn.Interrupt => error (excipit "was interrupted") (* FIXME violates Isabelle/ML exception model *) |
273 in |
243 in |
274 (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE)) |
244 (result, ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE)) |
275 end; |
245 end; |
276 |
246 |
277 exception WELLSORTED of string |
247 exception WELLSORTED of string |
278 |
248 |
279 fun monomorphic_term thy insts default_T = |
249 fun monomorphic_term thy insts default_T = |
411 fun read_expectation "no_expectation" = No_Expectation |
381 fun read_expectation "no_expectation" = No_Expectation |
412 | read_expectation "no_counterexample" = No_Counterexample |
382 | read_expectation "no_counterexample" = No_Counterexample |
413 | read_expectation "counterexample" = Counterexample |
383 | read_expectation "counterexample" = Counterexample |
414 | read_expectation s = error ("Not an expectation value: " ^ s) |
384 | read_expectation s = error ("Not an expectation value: " ^ s) |
415 |
385 |
416 fun parse_test_param ctxt ("size", [arg]) = |
386 fun parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg) |
417 (apfst o apfst o K) (read_nat arg) |
387 | parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg) |
418 | parse_test_param ctxt ("iterations", [arg]) = |
388 | parse_test_param ("default_type", arg) = (fn gen_ctxt => |
419 (apfst o apsnd o K) (read_nat arg) |
389 map_test_params ((apfst o K) (map (ProofContext.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt) |
420 | parse_test_param ctxt ("default_type", arg) = |
390 | parse_test_param ("no_assms", [arg]) = Config.put_generic no_assms (read_bool arg) |
421 (apsnd o apfst o apfst o K) (map (ProofContext.read_typ ctxt) arg) |
391 | parse_test_param ("expect", [arg]) = map_test_params ((apsnd o K) (read_expectation arg)) |
422 | parse_test_param ctxt ("no_assms", [arg]) = |
392 | parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg) |
423 (apsnd o apfst o apsnd o K) (read_bool arg) |
393 | parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg) |
424 | parse_test_param ctxt ("expect", [arg]) = |
394 | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg) |
425 (apsnd o apsnd o apfst o apfst o K) (read_expectation arg) |
395 | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name); |
426 | parse_test_param ctxt ("report", [arg]) = |
396 |
427 (apsnd o apsnd o apfst o apsnd o K) (read_bool arg) |
397 fun parse_test_param_inst ("generator", [arg]) ((generator, insts), ctxt) = |
428 | parse_test_param ctxt ("quiet", [arg]) = |
398 (apfst o apfst o K o SOME) arg ((generator, insts), ctxt) |
429 (apsnd o apsnd o apsnd o apfst o K) (read_bool arg) |
399 | parse_test_param_inst (name, arg) ((generator, insts), ctxt) = |
430 | parse_test_param ctxt ("timeout", [arg]) = |
|
431 (apsnd o apsnd o apsnd o apsnd o K) (read_real arg) |
|
432 | parse_test_param ctxt (name, _) = |
|
433 error ("Unknown test parameter: " ^ name); |
|
434 |
|
435 fun parse_test_param_inst ctxt ("generator", [arg]) = |
|
436 (apsnd o apfst o K o SOME) arg |
|
437 | parse_test_param_inst ctxt (name, arg) = |
|
438 case try (ProofContext.read_typ ctxt) name |
400 case try (ProofContext.read_typ ctxt) name |
439 of SOME (TFree (v, _)) => (apsnd o apsnd o AList.update (op =)) |
401 of SOME (TFree (v, _)) => (apfst o apsnd o AList.update (op =)) |
440 (v, ProofContext.read_typ ctxt (the_single arg)) |
402 (v, ProofContext.read_typ ctxt (the_single arg)) ((generator, insts), ctxt) |
441 | _ => (apfst o parse_test_param ctxt) (name, arg); |
403 | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) ((generator, insts), ctxt); |
442 |
404 |
443 fun quickcheck_params_cmd args thy = |
405 fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args); |
444 let |
406 |
445 val ctxt = ProofContext.init_global thy |
|
446 val f = fold (parse_test_param ctxt) args; |
|
447 in |
|
448 thy |
|
449 |> (Context.theory_map o map_test_params) f |
|
450 end; |
|
451 |
|
452 fun gen_quickcheck args i state = |
407 fun gen_quickcheck args i state = |
453 let |
408 state |
454 val ctxt = Proof.context_of state; |
409 |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ((NONE, []), ctxt)) |
455 val default_params = (dest_test_params o snd o Data.get o Context.Proof) ctxt; |
410 |> (fn ((generator, insts), state') => test_goal (generator, insts) i state' |
456 val f = fold (parse_test_param_inst ctxt) args; |
411 |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then |
457 val (test_params, (generator_name, insts)) = f (default_params, (NONE, [])); |
412 error ("quickcheck expected to find no counterexample but found one") else () |
458 in |
413 | (NONE, _) => if expect (Proof.context_of state') = Counterexample then |
459 state |
414 error ("quickcheck expected to find a counterexample but did not find one") else ())) |
460 |> Proof.map_context (Context.proof_map (map_test_params (K test_params))) |
|
461 |> (fn state' => test_goal generator_name insts i state' |
|
462 |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then |
|
463 error ("quickcheck expected to find no counterexample but found one") else () |
|
464 | (NONE, _) => if expect (Proof.context_of state') = Counterexample then |
|
465 error ("quickcheck expected to find a counterexample but did not find one") else ())) |
|
466 end; |
|
467 |
415 |
468 fun quickcheck args i state = fst (gen_quickcheck args i state); |
416 fun quickcheck args i state = fst (gen_quickcheck args i state); |
469 |
417 |
470 fun quickcheck_cmd args i state = |
418 fun quickcheck_cmd args i state = |
471 gen_quickcheck args i (Toplevel.proof_of state) |
419 gen_quickcheck args i (Toplevel.proof_of state) |