# HG changeset patch
# User bulwahn
# Date 1279728711 -7200
# Node ID 555287ba8d8d5d829e1bdb6e40926e108e9319ea
# Parent  583543ad6ad1ac6f5af82af1067707c4b97a70fd
reordering quickcheck signature; exporting test_params and inspection function

diff -r 583543ad6ad1 -r 555287ba8d8d src/Tools/quickcheck.ML
--- 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 *)