209 | subst T = T; |
209 | subst T = T; |
210 in (map_types o map_atyps) subst end; |
210 in (map_types o map_atyps) subst end; |
211 |
211 |
212 datatype wellsorted_error = Wellsorted_Error of string | Term of term |
212 datatype wellsorted_error = Wellsorted_Error of string | Term of term |
213 |
213 |
214 fun test_goal quiet report generator_name size iterations default_T no_assms insts i assms state = |
214 fun test_goal quiet report generator_name size iterations default_Ts no_assms insts i state = |
215 let |
215 let |
216 val ctxt = Proof.context_of state; |
216 val lthy = Proof.context_of state; |
217 val thy = Proof.theory_of state; |
217 val thy = Proof.theory_of state; |
218 fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t |
218 fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t |
219 | strip t = t; |
219 | strip t = t; |
220 val {goal = st, ...} = Proof.raw_goal state; |
220 val {goal = st, ...} = Proof.raw_goal state; |
221 val (gi, frees) = Logic.goal_params (prop_of st) i; |
221 val (gi, frees) = Logic.goal_params (prop_of st) i; |
222 val gi' = Logic.list_implies (if no_assms then [] else assms, |
222 val some_locale = case (#target o Theory_Target.peek) lthy |
223 subst_bounds (frees, strip gi)) |
223 of "" => NONE |
224 val inst_goals = map (fn T => |
224 | locale => SOME locale; |
225 Term (monomorphic_term thy insts T gi |> Object_Logic.atomize_term thy) |
225 val assms = if no_assms then [] else case some_locale |
226 handle WELLSORTED s => Wellsorted_Error s) default_T |
226 of NONE => Assumption.all_assms_of lthy |
|
227 | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy); |
|
228 val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi)); |
|
229 val check_goals = case some_locale |
|
230 of NONE => [proto_goal] |
|
231 | SOME locale => map (fn phi => Morphism.term phi proto_goal) (Locale.get_registrations thy locale); |
|
232 val inst_goals = maps (fn check_goal => map (fn T => |
|
233 Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal) |
|
234 handle WELLSORTED s => Wellsorted_Error s) default_Ts) check_goals |
227 val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals) |
235 val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals) |
228 val correct_inst_goals = |
236 val correct_inst_goals = |
229 case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of |
237 case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of |
230 [] => error error_msg |
238 [] => error error_msg |
231 | xs => xs |
239 | xs => xs |
233 fun collect_results f reports [] = (NONE, rev reports) |
241 fun collect_results f reports [] = (NONE, rev reports) |
234 | collect_results f reports (t :: ts) = |
242 | collect_results f reports (t :: ts) = |
235 case f t of |
243 case f t of |
236 (SOME res, report) => (SOME res, rev (report :: reports)) |
244 (SOME res, report) => (SOME res, rev (report :: reports)) |
237 | (NONE, report) => collect_results f (report :: reports) ts |
245 | (NONE, report) => collect_results f (report :: reports) ts |
238 in collect_results (gen_test_term ctxt quiet report generator_name size iterations) [] correct_inst_goals end; |
246 in collect_results (gen_test_term lthy quiet report generator_name size iterations) [] correct_inst_goals end; |
239 |
247 |
240 (* pretty printing *) |
248 (* pretty printing *) |
241 |
249 |
242 fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample." |
250 fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample." |
243 | pretty_counterex ctxt (SOME cex) = |
251 | pretty_counterex ctxt (SOME cex) = |
279 if not (!auto) then |
287 if not (!auto) then |
280 (false, state) |
288 (false, state) |
281 else |
289 else |
282 let |
290 let |
283 val ctxt = Proof.context_of state; |
291 val ctxt = Proof.context_of state; |
284 val assms = map term_of (Assumption.all_assms_of ctxt); |
|
285 val Test_Params {size, iterations, default_type, no_assms, ...} = |
292 val Test_Params {size, iterations, default_type, no_assms, ...} = |
286 (snd o Data.get o Proof.theory_of) state; |
293 (snd o Data.get o Proof.theory_of) state; |
287 val res = |
294 val res = |
288 try (test_goal true false NONE size iterations default_type no_assms [] 1 assms) state; |
295 try (test_goal true false NONE size iterations default_type no_assms [] 1) state; |
289 in |
296 in |
290 case res of |
297 case res of |
291 NONE => (false, state) |
298 NONE => (false, state) |
292 | SOME (NONE, report) => (false, state) |
299 | SOME (NONE, report) => (false, state) |
293 | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "", |
300 | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "", |
349 |
356 |
350 fun gen_quickcheck args i state = |
357 fun gen_quickcheck args i state = |
351 let |
358 let |
352 val thy = Proof.theory_of state; |
359 val thy = Proof.theory_of state; |
353 val ctxt = Proof.context_of state; |
360 val ctxt = Proof.context_of state; |
354 val assms = map term_of (Assumption.all_assms_of ctxt); |
|
355 val default_params = (dest_test_params o snd o Data.get) thy; |
361 val default_params = (dest_test_params o snd o Data.get) thy; |
356 val f = fold (parse_test_param_inst ctxt) args; |
362 val f = fold (parse_test_param_inst ctxt) args; |
357 val (((size, iterations), ((default_type, no_assms), ((expect, report), quiet))), (generator_name, insts)) = |
363 val (((size, iterations), ((default_type, no_assms), ((expect, report), quiet))), (generator_name, insts)) = |
358 f (default_params, (NONE, [])); |
364 f (default_params, (NONE, [])); |
359 in |
365 in |
360 test_goal quiet report generator_name size iterations default_type no_assms insts i assms state |
366 test_goal quiet report generator_name size iterations default_type no_assms insts i state |
361 |> tap (fn (SOME x, _) => if expect = No_Counterexample then |
367 |> tap (fn (SOME x, _) => if expect = No_Counterexample then |
362 error ("quickcheck expect to find no counterexample but found one") else () |
368 error ("quickcheck expected to find no counterexample but found one") else () |
363 | (NONE, _) => if expect = Counterexample then |
369 | (NONE, _) => if expect = Counterexample then |
364 error ("quickcheck expected to find a counterexample but did not find one") else ()) |
370 error ("quickcheck expected to find a counterexample but did not find one") else ()) |
365 end; |
371 end; |
366 |
372 |
367 fun quickcheck args i state = fst (gen_quickcheck args i state); |
373 fun quickcheck args i state = fst (gen_quickcheck args i state); |