16 val put_lseq_result : |
16 val put_lseq_result : |
17 (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) -> |
17 (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) -> |
18 Proof.context -> Proof.context; |
18 Proof.context -> Proof.context; |
19 val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) -> |
19 val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) -> |
20 Proof.context -> Proof.context |
20 Proof.context -> Proof.context |
21 |
21 val test_goals : (Predicate_Compile_Aux.compilation * bool * bool) -> |
22 val tracing : bool Unsynchronized.ref; |
|
23 val quiet : bool Unsynchronized.ref; |
|
24 val test_goals : (Predicate_Compile_Aux.compilation * bool * bool * int) -> |
|
25 Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list |
22 Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list |
26 -> Quickcheck.result list |
23 -> Quickcheck.result list |
27 val nrandom : int Unsynchronized.ref; |
24 val nrandom : int Unsynchronized.ref; |
28 val debug : bool Unsynchronized.ref; |
25 val debug : bool Unsynchronized.ref; |
29 val function_flattening : bool Unsynchronized.ref; |
26 val function_flattening : bool Unsynchronized.ref; |
329 end |
322 end |
330 in |
323 in |
331 prog |
324 prog |
332 end |
325 end |
333 |
326 |
334 fun try_upto quiet f i = |
327 fun try_upto_depth ctxt f = |
335 let |
328 let |
336 fun try' j = |
329 val max_depth = Config.get ctxt Quickcheck.depth |
337 if j <= i then |
330 fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s |
|
331 fun try' i = |
|
332 if i <= max_depth then |
338 let |
333 let |
339 val _ = if quiet then () else Output.urgent_message ("Executing depth " ^ string_of_int j) |
334 val _ = message ("Depth: " ^ string_of_int i) |
|
335 val (result, time) = |
|
336 cpu_time ("Depth " ^ string_of_int i) (fn () => |
|
337 f i handle Match => (if Config.get ctxt Quickcheck.quiet then () |
|
338 else warning "Exception Match raised during quickcheck"; NONE)) |
|
339 val _ = if Config.get ctxt Quickcheck.timing then |
|
340 message (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else () |
340 in |
341 in |
341 case f j handle Match => (if quiet then () |
342 case result of NONE => try' (i + 1) | SOME q => SOME q |
342 else warning "Exception Match raised during quickcheck"; NONE) |
|
343 of NONE => try' (j + 1) | SOME q => SOME q |
|
344 end |
343 end |
345 else |
344 else |
346 NONE |
345 NONE |
347 in |
346 in |
348 try' 0 |
347 try' 0 |
349 end |
348 end |
350 |
349 |
351 (* quickcheck interface functions *) |
350 (* quickcheck interface functions *) |
352 |
351 |
353 fun compile_term' compilation options depth ctxt (t, eval_terms) = |
352 fun compile_term' compilation options ctxt (t, eval_terms) = |
354 let |
353 let |
355 val size = Config.get ctxt Quickcheck.size |
354 val size = Config.get ctxt Quickcheck.size |
356 val c = compile_term compilation options ctxt t |
355 val c = compile_term compilation options ctxt t |
357 val counterexample = try_upto (!quiet) (c size (!nrandom)) depth |
356 val counterexample = try_upto_depth ctxt (c size (!nrandom)) |
358 in |
357 in |
359 Quickcheck.Result |
358 Quickcheck.Result |
360 {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample, |
359 {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample, |
361 evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []} |
360 evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []} |
362 end |
361 end |
363 |
362 |
364 fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth = |
363 fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening = |
365 let |
364 let |
366 val options = |
365 val options = |
367 set_fail_safe_function_flattening fail_safe_function_flattening |
366 set_fail_safe_function_flattening fail_safe_function_flattening |
368 (set_function_flattening function_flattening (get_options ())) |
367 (set_function_flattening function_flattening (get_options ())) |
369 in |
368 in |
370 compile_term' compilation options depth |
369 compile_term' compilation options |
371 end |
370 end |
372 |
371 |
373 |
372 |
374 fun test_goals options ctxt (limit_time, is_interactive) insts goals = |
373 fun test_goals options ctxt (limit_time, is_interactive) insts goals = |
375 let |
374 let |
376 val (compilation, function_flattening, fail_safe_function_flattening, depth) = options |
375 val (compilation, function_flattening, fail_safe_function_flattening) = options |
377 val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals |
376 val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals |
378 val test_term = |
377 val test_term = |
379 quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth |
378 quickcheck_compile_term compilation function_flattening fail_safe_function_flattening |
380 in |
379 in |
381 Quickcheck.collect_results (test_term ctxt) |
380 Quickcheck_Common.collect_results (test_term ctxt) |
382 (maps (map snd) correct_inst_goals) [] |
381 (maps (map snd) correct_inst_goals) [] |
383 end |
382 end |
384 |
383 |
385 val wo_ff_active = Attrib.setup_config_bool @{binding quickcheck_pc_wo_ff_active} (K false); |
384 val wo_ff_active = Attrib.setup_config_bool @{binding quickcheck_pc_wo_ff_active} (K false); |
386 val ff_active = Attrib.setup_config_bool @{binding quickcheck_pc_ff_active} (K false); |
385 val ff_active = Attrib.setup_config_bool @{binding quickcheck_pc_ff_active} (K false); |
387 val ff_nofs_active = Attrib.setup_config_bool @{binding quickcheck_pc_ff_nofs_active} (K false); |
386 val ff_nofs_active = Attrib.setup_config_bool @{binding quickcheck_pc_ff_nofs_active} (K false); |
388 |
387 |
389 val setup = |
388 val setup = |
390 Context.theory_map (Quickcheck.add_tester ("predicate_compile_wo_ff", |
389 Context.theory_map (Quickcheck.add_tester ("predicate_compile_wo_ff", |
391 (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, false, true, 4)))) |
390 (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, false, true)))) |
392 #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_fs", |
391 #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_fs", |
393 (ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true, 4)))) |
392 (ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true)))) |
394 #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_nofs", |
393 #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_nofs", |
395 (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true, 4)))) |
394 (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true)))) |
396 |
395 |
397 |
396 |
398 end; |
397 end; |