author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
parent 37920 | 581c1e5f53e0 |
permissions | -rw-r--r-- |
32564 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML |
2 |
Author: Jasmin Blanchette and Sascha Boehme, TU Munich |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
3 |
*) |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
4 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
5 |
structure Mirabelle_Quickcheck : MIRABELLE_ACTION = |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
6 |
struct |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
7 |
|
32521 | 8 |
fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: " |
9 |
||
10 |
fun init _ = I |
|
11 |
fun done _ _ = () |
|
12 |
||
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
13 |
fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) = |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
14 |
let |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
15 |
val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst |
37920 | 16 |
val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1 |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
17 |
in |
32497 | 18 |
(case TimeLimit.timeLimit timeout quickcheck pre of |
32521 | 19 |
NONE => log (qc_tag id ^ "no counterexample") |
20 |
| SOME _ => log (qc_tag id ^ "counterexample found")) |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
21 |
end |
32521 | 22 |
handle TimeLimit.TimeOut => log (qc_tag id ^ "timeout") |
23 |
| ERROR msg => log (qc_tag id ^ "error: " ^ msg) |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
24 |
|
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32498
diff
changeset
|
25 |
fun invoke args = |
32521 | 26 |
Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done) |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
27 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
28 |
end |