--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Wed Sep 02 16:23:53 2009 +0200
@@ -0,0 +1,20 @@
+(* Title: mirabelle_quickcheck.ML
+ Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
+struct
+
+fun quickcheck_action limit args {pre=st, ...} =
+ let
+ val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
+ val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
+ in
+ (case TimeLimit.timeLimit limit quickcheck st of
+ NONE => SOME "no counterexample"
+ | SOME _ => SOME "counterexample found")
+ end
+
+fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
+
+end