| author | wenzelm |
| Wed, 10 Jun 2015 21:49:02 +0200 | |
| changeset 60422 | be7565a1115b |
| parent 47847 | 7cddb6c8f93c |
| child 62519 | a564458f94db |
| permissions | -rw-r--r-- |
| 47847 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML |
| 32564 | 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 |