# HG changeset patch
# User bulwahn
# Date 1290418926 -3600
# Node ID 3bba5e71a8731e76c26f4e052fb77d56616b697b
# Parent  99c6ce92669be4d3469025277814406453e35c8c
adding temporary function test_test_small to Quickcheck

diff -r 99c6ce92669b -r 3bba5e71a873 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon Nov 22 10:42:04 2010 +0100
+++ b/src/Tools/quickcheck.ML	Mon Nov 22 10:42:06 2010 +0100
@@ -27,6 +27,8 @@
     string * (Proof.context -> term -> int -> term list option * (bool list * bool))
       -> Context.generic -> Context.generic
   (* testing terms and proof states *)
+  val test_term_small: Proof.context -> term ->
+    (string * term) list option * ((string * int) list * ((int * report list) list) option)
   val test_term: Proof.context -> string option -> term ->
     (string * term) list option * ((string * int) list * ((int * report list) list) option)
   val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
@@ -197,6 +199,34 @@
     val time = Time.toMilliseconds (#cpu (end_timing start))
   in (Exn.release result, (description, time)) end
 
+fun test_term_small ctxt t =
+  let
+    val (names, t') = prep_test_term t;
+    val current_size = Unsynchronized.ref 0
+    fun excipit s =
+      "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
+    val (tester, comp_time) = cpu_time "compilation"
+      (fn () => the (AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) "small") ctxt t');
+    val empty_report = Report { iterations = 0, raised_match_errors = 0,
+      satisfied_assms = [], positive_concl_tests = 0 }
+    fun with_size k timings =
+      if k > size ctxt then (NONE, timings)
+      else
+         let
+           val _ = if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
+           val _ = current_size := k
+           val (result, timing) = cpu_time ("size " ^ string_of_int k) (fn () => (fst (tester k)) handle Match => (if quiet ctxt then ()
+             else warning "Exception Match raised during quickcheck"; NONE))
+        in
+          case result of
+            NONE => with_size (k + 1) (timing :: timings)
+          | SOME q => (SOME q, (timing :: timings))
+        end;
+     val result = with_size 1 [comp_time]
+   in
+     apsnd (rpair NONE) (apfst (Option.map (curry (op ~~) names)) result)
+   end
+
 fun test_term ctxt generator_name t =
   let
     val (names, t') = prep_test_term t;