| author | boehmes |
| Thu, 03 Sep 2009 22:47:31 +0200 | |
| changeset 32515 | e7c0d3c0494a |
| parent 32498 | 1132c7c13f36 |
| child 32518 | e3c4e337196c |
| permissions | -rw-r--r-- |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
1 |
(* Title: mirabelle_quickcheck.ML |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette and Sascha Boehme |
|
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 |
|
| 32497 | 8 |
fun quickcheck_action args {pre, timeout, log, ...} =
|
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
9 |
let |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
10 |
val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst |
| 32469 | 11 |
val quickcheck = Quickcheck.quickcheck (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
|
12 |
in |
| 32497 | 13 |
(case TimeLimit.timeLimit timeout quickcheck pre of |
|
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
14 |
NONE => log "quickcheck: no counterexample" |
|
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
15 |
| SOME _ => log "quickcheck: counterexample found") |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
16 |
end |
|
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
17 |
handle TimeLimit.TimeOut => log "quickcheck: time out" |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
18 |
|
|
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32498
diff
changeset
|
19 |
fun invoke args = |
|
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32498
diff
changeset
|
20 |
Mirabelle.register (Mirabelle.catch "quickcheck: " (quickcheck_action args)) |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
21 |
|
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
22 |
end |