--- a/src/Tools/quickcheck.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Tools/quickcheck.ML Wed Jul 21 18:11:51 2010 +0200
@@ -19,7 +19,7 @@
string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))
-> theory -> theory
val setup: theory -> theory
- val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
+ val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
end;
structure Quickcheck : QUICKCHECK =
@@ -63,7 +63,7 @@
(* quickcheck configuration -- default parameters, test generators *)
datatype test_params = Test_Params of
- { size: int, iterations: int, default_type: typ option, no_assms: bool, report: bool, quiet : bool};
+ { size: int, iterations: int, default_type: typ list, no_assms: bool, report: bool, quiet : bool};
fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, report, quiet }) =
((size, iterations), ((default_type, no_assms), (report, quiet)));
@@ -77,7 +77,7 @@
Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
no_assms = no_assms2, report = report2, quiet = quiet2 }) =
make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
- ((case default_type1 of NONE => default_type2 | _ => default_type1, no_assms1 orelse no_assms2),
+ ((default_type1 @ default_type2, no_assms1 orelse no_assms2),
(report1 orelse report2, quiet1 orelse quiet2)));
structure Data = Theory_Data
@@ -85,7 +85,7 @@
type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
* test_params;
val empty = ([], Test_Params
- { size = 10, iterations = 100, default_type = NONE, no_assms = false, report = false, quiet = false});
+ { size = 10, iterations = 100, default_type = [], no_assms = false, report = false, quiet = false});
val extend = I;
fun merge ((generators1, params1), (generators2, params2)) : T =
(AList.merge (op =) (K true) (generators1, generators2),
@@ -196,9 +196,14 @@
| strip t = t;
val {goal = st, ...} = Proof.raw_goal state;
val (gi, frees) = Logic.goal_params (prop_of st) i;
+ val default_T' =
+ case default_T of
+ [] => NONE
+ | [T] => SOME T
+ | _ => error "Multiple default types not yet supported"
val gi' = Logic.list_implies (if no_assms then [] else assms,
subst_bounds (frees, strip gi))
- |> monomorphic_term thy insts default_T
+ |> monomorphic_term thy insts default_T'
|> Object_Logic.atomize_term thy;
in gen_test_term ctxt quiet report generator_name size iterations gi' end;
@@ -266,31 +271,32 @@
of (k, []) => if k >= 0 then k
else error ("Not a natural number: " ^ s)
| (_, _ :: _) => error ("Not a natural number: " ^ s);
+
fun read_bool "false" = false
| read_bool "true" = true
| read_bool s = error ("Not a Boolean value: " ^ s)
-fun parse_test_param ctxt ("size", arg) =
+fun parse_test_param ctxt ("size", [arg]) =
(apfst o apfst o K) (read_nat arg)
- | parse_test_param ctxt ("iterations", arg) =
+ | parse_test_param ctxt ("iterations", [arg]) =
(apfst o apsnd o K) (read_nat arg)
| parse_test_param ctxt ("default_type", arg) =
- (apsnd o apfst o apfst o K o SOME) (ProofContext.read_typ ctxt arg)
- | parse_test_param ctxt ("no_assms", arg) =
+ (apsnd o apfst o apfst o K) (map (ProofContext.read_typ ctxt) arg)
+ | parse_test_param ctxt ("no_assms", [arg]) =
(apsnd o apfst o apsnd o K) (read_bool arg)
- | parse_test_param ctxt ("report", arg) =
+ | parse_test_param ctxt ("report", [arg]) =
(apsnd o apsnd o apfst o K) (read_bool arg)
- | parse_test_param ctxt ("quiet", arg) =
+ | parse_test_param ctxt ("quiet", [arg]) =
(apsnd o apsnd o apsnd o K) (read_bool arg)
| parse_test_param ctxt (name, _) =
error ("Unknown test parameter: " ^ name);
-fun parse_test_param_inst ctxt ("generator", arg) =
+fun parse_test_param_inst ctxt ("generator", [arg]) =
(apsnd o apfst o K o SOME) arg
| parse_test_param_inst ctxt (name, arg) =
case try (ProofContext.read_typ ctxt) name
of SOME (TFree (v, _)) => (apsnd o apsnd o AList.update (op =))
- (v, ProofContext.read_typ ctxt arg)
+ (v, ProofContext.read_typ ctxt (the_single arg))
| _ => (apfst o parse_test_param ctxt) (name, arg);
fun quickcheck_params_cmd args thy =
@@ -321,7 +327,8 @@
gen_quickcheck args i (Toplevel.proof_of state)
|> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state);
-val parse_arg = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true");
+val parse_arg = Parse.name -- (Scan.optional (Parse.$$$ "=" |--
+ ((Parse.name >> single) || (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]);
val parse_args = Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]"
|| Scan.succeed [];