--- 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
@@ -6,19 +6,24 @@
signature QUICKCHECK =
sig
+ val setup: theory -> theory
+ (* configuration *)
val auto: bool Unsynchronized.ref
val timing : bool Unsynchronized.ref
datatype report = Report of
{ iterations : int, raised_match_errors : int,
satisfied_assms : int list, positive_concl_tests : int }
+ datatype test_params = Test_Params of
+ { size: int, iterations: int, default_type: typ list, no_assms: bool, report: bool, quiet : bool};
+ val test_params_of: theory -> test_params
+ val add_generator:
+ string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))
+ -> theory -> theory
+ (* testing terms and proof states *)
val gen_test_term: Proof.context -> bool -> bool -> string option -> int -> int -> term ->
(string * term) list option * ((string * int) list * ((int * report list) list) option)
val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
(string * term) list option
- val add_generator:
- string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))
- -> theory -> theory
- val setup: theory -> theory
val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
end;
@@ -92,6 +97,8 @@
merge_test_params (params1, params2));
);
+val test_params_of = snd o Data.get;
+
val add_generator = Data.map o apfst o AList.update (op =);
(* generating tests *)