| author | wenzelm |
| Fri, 29 Oct 2021 11:59:02 +0200 | |
| changeset 74620 | d622d1dce05c |
| parent 73847 | 58f6b41efe88 |
| child 74948 | 15ce207f69c8 |
| permissions | -rw-r--r-- |
| 47847 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML |
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Munich |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
3 |
Author: Sascha Boehme, TU Munich |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
4 |
Author: Martin Desharnais, UniBw Munich |
|
73691
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
67405
diff
changeset
|
5 |
|
|
2f9877db82a1
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
67405
diff
changeset
|
6 |
Mirabelle action: "quickcheck". |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
7 |
*) |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
8 |
|
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
9 |
structure Mirabelle_Quickcheck: MIRABELLE_ACTION = |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
10 |
struct |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
11 |
|
|
73847
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
12 |
fun make_action ({arguments, timeout, ...} : Mirabelle.action_context) =
|
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
13 |
let |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
14 |
val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
15 |
val quickcheck = |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
16 |
Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key arguments)) 1 |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
17 |
|
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
18 |
fun run_action ({pre, ...} : Mirabelle.command) =
|
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
19 |
(case Timeout.apply timeout quickcheck pre of |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
20 |
NONE => "no counterexample" |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
21 |
| SOME _ => "counterexample found") |
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
22 |
in {run_action = run_action, finalize = K ""} end
|
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
23 |
|
|
58f6b41efe88
refactored Mirabelle to produce output in real time
desharna
parents:
73691
diff
changeset
|
24 |
val () = Mirabelle.register_action "quickcheck" make_action |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
25 |
|
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
26 |
end |