--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML Fri May 14 21:32:11 2021 +0200
@@ -0,0 +1,23 @@
+(* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
+ Author: Jasmin Blanchette and Sascha Boehme, TU Munich
+
+Mirabelle action: "quickcheck".
+*)
+
+structure Mirabelle_Quickcheck: sig end =
+struct
+
+val _ =
+ Theory.setup (Mirabelle.command_action \<^binding>\<open>quickcheck\<close>
+ (fn {arguments, timeout, ...} => fn {pre, ...} =>
+ let
+ val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst;
+ val quickcheck =
+ Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key arguments)) 1;
+ in
+ (case Timeout.apply timeout quickcheck pre of
+ NONE => "no counterexample"
+ | SOME _ => "counterexample found")
+ end));
+
+end