indicating where the restart should occur; making safe_if dynamic

--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Dec 05 07:31:11 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Dec 05 12:35:04 2011 +0100
@@ -360,9 +360,11 @@
     val ctxt' = Variable.auto_fixes t ctxt
     val names = Term.add_free_names t []
     val frees = map Free (Term.add_frees t [])
-    val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+    val ([depth_name, genuine_only_name], ctxt'') =
+      Variable.variant_fixes ["depth", "genuine_only"] ctxt'
     val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") names) ctxt''
     val depth = Free (depth_name, @{typ code_numeral})
+    val genuine_only = Free (depth_name, @{typ bool})    
     val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
     fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
     val return = mk_return (HOLogic.mk_list @{typ term}
@@ -370,7 +372,7 @@
     fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
       if Sign.of_sort thy (T, @{sort enum}) then
         Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
-          $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT) 
+          $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
             $ lambda free (lambda term_var t))
       else
         Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
@@ -379,7 +381,7 @@
     val none_t = Const (@{const_name "None"}, resultT)
     val mk_if = Quickcheck_Common.mk_safe_if ctxt
     val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
-  in lambda depth (mk_test_term t) end
+  in lambda genuine_only (lambda depth (mk_test_term t)) end
 
 fun mk_parametric_generator_expr mk_generator_expr =
   Quickcheck_Common.gen_mk_parametric_generator_expr 

--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Dec 05 07:31:11 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Dec 05 12:35:04 2011 +0100
@@ -88,7 +88,10 @@
           val _ = Quickcheck.add_timing timing current_result
           val _ = Quickcheck.add_report k report current_result
         in
-          case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q
+          case result of
+            NONE => with_size test_fun (k + 1)
+          | SOME (true, ts) => SOME (true, ts)
+          | SOME (false, ts) => SOME (false, ts) (* FIXME: output message & restart *) 
         end;
     val act = if catch_code_errors then try else (fn f => SOME o f) 
     val (test_fun, comp_time) = cpu_time "quickcheck compilation"
@@ -270,11 +273,15 @@
 
 (* compilation of testing functions *)
 
-fun mk_safe_if ctxt (cond, then_t, else_t) =
-  @{term "Quickcheck.catch_match :: (bool * term list) option => (bool * term list) option => (bool * term list) option"}
-    $ (@{term "If :: bool => (bool * term list) option => (bool * term list) option => (bool * term list) option"}
-      $ cond $ then_t $ else_t true)
-    $ (if Config.get ctxt Quickcheck.potential then else_t false else @{term "None :: (bool * term list) option"});
+fun mk_safe_if genuine_only (cond, then_t, else_t) =
+  let
+    val T = @{typ "(bool * term list) option"}
+    val if = Const (@{const_name "If"}, T --> T --> T)
+  in
+    Const (@{const_name "Quickcheck.catch_match"}, T --> T --> T) $ 
+      (if $ cond $ then_t $ else_t true) $
+      (if $ genuine_only $ Const (@{const_name "None", T) $ else_t false);
+  end
 
 fun collect_results f [] results = results
   | collect_results f (t :: ts) results =