17 datatype test_params = Test_Params of |
17 datatype test_params = Test_Params of |
18 { size: int, iterations: int, default_type: typ list, no_assms: bool, |
18 { size: int, iterations: int, default_type: typ list, no_assms: bool, |
19 expect : expectation, report: bool, quiet : bool}; |
19 expect : expectation, report: bool, quiet : bool}; |
20 val test_params_of: Proof.context -> test_params |
20 val test_params_of: Proof.context -> test_params |
21 val report : Proof.context -> bool |
21 val report : Proof.context -> bool |
22 val set_reporting : bool -> Proof.context -> Proof.context |
22 val set_reporting : bool -> Context.generic -> Context.generic |
23 val add_generator: |
23 val add_generator: |
24 string * (Proof.context -> term -> int -> term list option * (bool list * bool)) |
24 string * (Proof.context -> term -> int -> term list option * (bool list * bool)) |
25 -> Context.generic -> Context.generic |
25 -> Context.generic -> Context.generic |
26 (* testing terms and proof states *) |
26 (* testing terms and proof states *) |
27 val gen_test_term: Proof.context -> bool -> string option -> int -> int -> term -> |
27 val gen_test_term: Proof.context -> bool -> string option -> int -> int -> term -> |
120 val report = snd o fst o snd o snd o dest_test_params o test_params_of |
120 val report = snd o fst o snd o snd o dest_test_params o test_params_of |
121 |
121 |
122 fun map_report f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) = |
122 fun map_report f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) = |
123 make_test_params ((size, iterations), ((default_type, no_assms), ((expect, f report), quiet))); |
123 make_test_params ((size, iterations), ((default_type, no_assms), ((expect, f report), quiet))); |
124 |
124 |
125 fun set_reporting report = Context.proof_map (Data.map (apsnd (map_report (K report)))) |
125 fun set_reporting report = Data.map (apsnd (map_report (K report))) |
126 |
126 |
127 val add_generator = Data.map o apfst o AList.update (op =); |
127 val add_generator = Data.map o apfst o AList.update (op =); |
128 |
128 |
129 (* generating tests *) |
129 (* generating tests *) |
130 |
130 |
202 (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE)) |
202 (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE)) |
203 end; |
203 end; |
204 |
204 |
205 fun test_term ctxt quiet generator_name size i t = |
205 fun test_term ctxt quiet generator_name size i t = |
206 ctxt |
206 ctxt |
207 |> set_reporting false |
207 |> Context.proof_map (set_reporting false) |
208 |> (fn ctxt' => fst (gen_test_term ctxt' quiet generator_name size i t)) |
208 |> (fn ctxt' => fst (gen_test_term ctxt' quiet generator_name size i t)) |
209 |
209 |
210 exception WELLSORTED of string |
210 exception WELLSORTED of string |
211 |
211 |
212 fun monomorphic_term thy insts default_T = |
212 fun monomorphic_term thy insts default_T = |
308 val ctxt = Proof.context_of state; |
308 val ctxt = Proof.context_of state; |
309 val Test_Params {size, iterations, default_type, no_assms, ...} = |
309 val Test_Params {size, iterations, default_type, no_assms, ...} = |
310 (snd o Data.get o Context.Proof) ctxt; |
310 (snd o Data.get o Context.Proof) ctxt; |
311 val res = |
311 val res = |
312 state |
312 state |
313 |> Proof.map_context (set_reporting false) |
313 |> Proof.map_context (Context.proof_map (set_reporting false)) |
314 |> try (test_goal true NONE size iterations default_type no_assms [] 1); |
314 |> try (test_goal true NONE size iterations default_type no_assms [] 1); |
315 in |
315 in |
316 case res of |
316 case res of |
317 NONE => (false, state) |
317 NONE => (false, state) |
318 | SOME (NONE, report) => (false, state) |
318 | SOME (NONE, report) => (false, state) |
380 val f = fold (parse_test_param_inst ctxt) args; |
380 val f = fold (parse_test_param_inst ctxt) args; |
381 val (((size, iterations), ((default_type, no_assms), ((expect, report), quiet))), (generator_name, insts)) = |
381 val (((size, iterations), ((default_type, no_assms), ((expect, report), quiet))), (generator_name, insts)) = |
382 f (default_params, (NONE, [])); |
382 f (default_params, (NONE, [])); |
383 in |
383 in |
384 state |
384 state |
385 |> Proof.map_context (set_reporting report) |
385 |> Proof.map_context (Context.proof_map (set_reporting report)) |
386 |> test_goal quiet generator_name size iterations default_type no_assms insts i |
386 |> test_goal quiet generator_name size iterations default_type no_assms insts i |
387 |> tap (fn (SOME x, _) => if expect = No_Counterexample then |
387 |> tap (fn (SOME x, _) => if expect = No_Counterexample then |
388 error ("quickcheck expected to find no counterexample but found one") else () |
388 error ("quickcheck expected to find no counterexample but found one") else () |
389 | (NONE, _) => if expect = Counterexample then |
389 | (NONE, _) => if expect = Counterexample then |
390 error ("quickcheck expected to find a counterexample but did not find one") else ()) |
390 error ("quickcheck expected to find a counterexample but did not find one") else ()) |