src/HOL/Tools/quickcheck_generators.ML

--- a/src/HOL/Tools/quickcheck_generators.ML	Tue Feb 23 16:58:21 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Feb 25 09:28:01 2010 +0100
@@ -15,8 +15,11 @@
     -> string list -> string list * string list -> typ list * typ list
     -> term list * (term * term) list
   val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
-  val compile_generator_expr: theory -> term -> int -> term list option
+  val compile_generator_expr:
+    theory -> bool -> term -> int -> term list option * (bool list * bool)
   val eval_ref: (unit -> int -> seed -> term list option * seed) option Unsynchronized.ref
+  val eval_report_ref:
+    (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref
   val setup: theory -> theory
 end;
 
@@ -350,6 +353,10 @@
     (unit -> int -> int * int -> term list option * (int * int)) option Unsynchronized.ref =
   Unsynchronized.ref NONE;
 
+val eval_report_ref :
+    (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref =
+  Unsynchronized.ref NONE;
+
 val target = "Quickcheck";
 
 fun mk_generator_expr thy prop Ts =
@@ -360,7 +367,7 @@
     val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
     val check = @{term "If :: bool => term list option => term list option => term list option"}
-      $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option "} $ terms);
+      $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms);
     val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"};
     fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
     fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
@@ -375,13 +382,69 @@
       (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
   in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
 
-fun compile_generator_expr thy t =
+fun mk_reporting_generator_expr thy prop Ts =
+  let
+    val bound_max = length Ts - 1;
+    val bounds = map_index (fn (i, ty) =>
+      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
+    fun strip_imp (Const("op -->",_) $ A $ B) = apfst (cons A) (strip_imp B)
+      | strip_imp A = ([], A)
+    val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
+    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
+    val (assms, concl) = strip_imp prop'
+    val return =
+      @{term "Pair :: term list option * (bool list * bool) => Random.seed => (term list option * (bool list * bool)) * Random.seed"};
+    fun mk_assms_report i =
+      HOLogic.mk_prod (@{term "None :: term list option"},
+        HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"}
+          (replicate i @{term "True"} @ replicate (length assms - i) @{term "False"}),
+        @{term "False"}))
+    fun mk_concl_report b =
+      HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"} (replicate (length assms) @{term "True"}),
+        if b then @{term True} else @{term False})
+    val If =
+      @{term "If :: bool => term list option * (bool list * bool) => term list option * (bool list * bool) => term list option * (bool list * bool)"}
+    val concl_check = If $ concl $
+      HOLogic.mk_prod (@{term "None :: term list option"}, mk_concl_report true) $
+      HOLogic.mk_prod (@{term "Some :: term list  => term list option"} $ terms, mk_concl_report false)
+    val check = fold_rev (fn (i, assm) => fn t => If $ assm $ t $ mk_assms_report i)
+      (map_index I assms) concl_check
+    fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
+    fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
+    fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
+      liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
+    fun mk_split T = Sign.mk_const thy
+      (@{const_name split}, [T, @{typ "unit => term"},
+        liftT @{typ "term list option * (bool list * bool)"} @{typ Random.seed}]);
+    fun mk_scomp_split T t t' =
+      mk_scomp (mk_termtyp T) @{typ "term list option * (bool list * bool)"} @{typ Random.seed} t
+        (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
+    fun mk_bindclause (_, _, i, T) = mk_scomp_split T
+      (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
+  in
+    Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
+  end
+
+fun compile_generator_expr thy report t =
   let
     val Ts = (map snd o fst o strip_abs) t;
-    val t' = mk_generator_expr thy t Ts;
-    val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
-      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
-  in compile #> Random_Engine.run end;
+  in
+    if report then
+      let
+        val t' = mk_reporting_generator_expr thy t Ts;
+        val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref)
+          (fn proc => fn g => fn s => g s #>> ((apfst o Option.map o map) proc)) thy t' [];
+      in
+        compile #> Random_Engine.run
+      end
+    else
+      let
+        val t' = mk_generator_expr thy t Ts;
+        val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
+          (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+        val dummy_report = ([], false)
+      in fn s => ((compile #> Random_Engine.run) s, dummy_report) end
+  end;
 
 
 (** setup **)