equal
deleted
inserted
replaced
1 (* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML |
|
2 Author: Jasmin Blanchette and Sascha Boehme, TU Munich |
|
3 *) |
|
4 |
|
5 structure Mirabelle_Quickcheck : MIRABELLE_ACTION = |
|
6 struct |
|
7 |
|
8 fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: " |
|
9 |
|
10 fun init _ = I |
|
11 fun done _ _ = () |
|
12 |
|
13 fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) = |
|
14 let |
|
15 val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst |
|
16 val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1 |
|
17 in |
|
18 (case Timeout.apply timeout quickcheck pre of |
|
19 NONE => log (qc_tag id ^ "no counterexample") |
|
20 | SOME _ => log (qc_tag id ^ "counterexample found")) |
|
21 end |
|
22 handle Timeout.TIMEOUT _ => log (qc_tag id ^ "timeout") |
|
23 | ERROR msg => log (qc_tag id ^ "error: " ^ msg) |
|
24 |
|
25 fun invoke args = |
|
26 Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done) |
|
27 |
|
28 end |
|