# HG changeset patch
# User bulwahn
# Date 1323084905 -3600
# Node ID 394ecd91434a34f790b55958873613805811c73c
# Parent  196697f714883092961b66339e2145eb7346224d
dynamic genuine_flag in compilation of random and exhaustive

diff -r 196697f71488 -r 394ecd91434a src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Dec 05 12:35:04 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Dec 05 12:35:05 2011 +0100
@@ -7,10 +7,10 @@
 signature EXHAUSTIVE_GENERATORS =
 sig
   val compile_generator_expr:
-    Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
+    Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
   val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
   val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list
-  val put_counterexample: (unit -> int -> int -> (bool * term list) option)
+  val put_counterexample: (unit -> int -> bool -> int -> (bool * term list) option)
     -> Proof.context -> Proof.context
   val put_counterexample_batch: (unit -> (int -> term list option) list)
     -> Proof.context -> Proof.context
@@ -342,17 +342,19 @@
     val names = Term.add_free_names t []
     val frees = map Free (Term.add_frees t [])
     fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
-    val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+    val ([depth_name, genuine_only_name], ctxt'') =
+      Variable.variant_fixes ["depth", "genuine_only"] ctxt'
     val depth = Free (depth_name, @{typ code_numeral})
+    val genuine_only = Free (genuine_only_name, @{typ bool}) 
     val return = mk_return (HOLogic.mk_list @{typ "term"}
         (map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms))
     fun mk_exhaustive_closure (free as Free (_, T)) t =
       Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
         $ lambda free t $ depth
     val none_t = Const (@{const_name "None"}, resultT)
-    val mk_if = Quickcheck_Common.mk_safe_if ctxt
+    val mk_if = Quickcheck_Common.mk_safe_if genuine_only
     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_full_generator_expr ctxt (t, eval_terms) =
   let
@@ -379,14 +381,15 @@
           $ (HOLogic.split_const (T, @{typ "unit => term"}, resultT)
             $ lambda free (lambda term_var t)) $ depth
     val none_t = Const (@{const_name "None"}, resultT)
-    val mk_if = Quickcheck_Common.mk_safe_if ctxt
+    val mk_if = Quickcheck_Common.mk_safe_if genuine_only
     val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
   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 
-    ((mk_generator_expr, absdummy @{typ "code_numeral"} (Const (@{const_name "None"}, resultT))),
-      @{typ "code_numeral"} --> resultT)
+    ((mk_generator_expr,
+      absdummy @{typ bool} (absdummy @{typ "code_numeral"} (Const (@{const_name "None"}, resultT)))),
+      @{typ bool} --> @{typ "code_numeral"} --> resultT)
 
 fun mk_validator_expr ctxt t =
   let
@@ -424,7 +427,7 @@
 
 structure Counterexample = Proof_Data
 (
-  type T = unit -> int -> int -> (bool * term list) option
+  type T = unit -> int -> bool -> int -> (bool * term list) option
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample"
 );
@@ -460,9 +463,10 @@
     val compile = Code_Runtime.dynamic_value_strict
       (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
       thy (SOME target) (fn proc => fn g =>
-        fn card => fn size => g card size |> (Option.map o apsnd o map) proc) t' []
+        fn card => fn genuine_only => fn size => g card genuine_only size
+          |> (Option.map o apsnd o map) proc) t' []
   in
-    fn [card, size] => rpair NONE (compile card size |> 
+    fn genuine_only => fn [card, size] => rpair NONE (compile card genuine_only size |> 
       (if Config.get ctxt quickcheck_pretty then
         Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I))
   end;
diff -r 196697f71488 -r 394ecd91434a src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Dec 05 12:35:04 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Dec 05 12:35:05 2011 +0100
@@ -14,10 +14,10 @@
     -> (string * sort -> string * sort) option
   val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
     -> (typ option * (term * term list)) list list
-  val mk_safe_if : Proof.context -> term * term * (bool -> term) -> term
+  val mk_safe_if : term -> term * term * (bool -> term) -> term
   val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
   type compile_generator =
-    Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
+    Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
   val generator_test_goal_terms :
     string * compile_generator -> Proof.context -> bool -> (string * typ) list
     -> (term * term list) list -> Quickcheck.result list
@@ -53,7 +53,7 @@
 (* testing functions: testing with increasing sizes (and cardinalities) *)
 
 type compile_generator =
-  Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
+  Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
 
 fun check_test_term t =
   let
@@ -69,34 +69,35 @@
 
 fun test_term (name, compile) ctxt catch_code_errors (t, eval_terms) =
   let
+    val genuine_only = not (Config.get ctxt Quickcheck.potential)
     val _ = check_test_term t
     val names = Term.add_free_names t []
     val current_size = Unsynchronized.ref 0
     val current_result = Unsynchronized.ref Quickcheck.empty_result 
     fun excipit () =
       "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
-    fun with_size test_fun k =
+    val act = if catch_code_errors then try else (fn f => SOME o f) 
+    val (test_fun, comp_time) = cpu_time "quickcheck compilation"
+        (fn () => act (compile ctxt) [(t, eval_terms)]);
+    val _ = Quickcheck.add_timing comp_time current_result
+    fun with_size test_fun genuine_only k =
       if k > Config.get ctxt Quickcheck.size then
         NONE
       else
         let
           val _ = Quickcheck.message ctxt
-            ("[Quickcheck-" ^ name ^ "]Test data size: " ^ string_of_int k)
+            ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
           val _ = current_size := k
           val ((result, report), timing) =
-            cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1])
+            cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1])
           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)
+            NONE => with_size test_fun genuine_only (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"
-        (fn () => act (compile ctxt) [(t, eval_terms)]);
-    val _ = Quickcheck.add_timing comp_time current_result
   in
     case test_fun of
       NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
@@ -104,7 +105,7 @@
     | SOME test_fun =>
       let
         val (response, exec_time) =
-          cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
+          cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1)
         val _ = Quickcheck.add_response names eval_terms response current_result
         val _ = Quickcheck.add_timing exec_time current_result
       in !current_result end
@@ -150,13 +151,14 @@
 
 fun test_term_with_cardinality (name, compile) ctxt catch_code_errors ts =
   let
+    val genuine_only = not (Config.get ctxt Quickcheck.potential)
     val thy = Proof_Context.theory_of ctxt
     val (ts', eval_terms) = split_list ts
     val _ = map check_test_term ts'
     val names = Term.add_free_names (hd ts') []
     val Ts = map snd (Term.add_frees (hd ts') [])
     val current_result = Unsynchronized.ref Quickcheck.empty_result
-    fun test_card_size test_fun (card, size) =
+    fun test_card_size test_fun genuine_only (card, size) =
       (* FIXME: why decrement size by one? *)
       let
         val _ =
@@ -165,7 +167,7 @@
             "cardinality: " ^ string_of_int card)          
         val (ts, timing) =
           cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
-            (fn () => fst (test_fun [card, size - 1]))
+            (fn () => fst (test_fun genuine_only [card, size - 1]))
         val _ = Quickcheck.add_timing timing current_result
       in
         Option.map (pair card) ts
@@ -187,7 +189,7 @@
         !current_result)
     | SOME test_fun =>
       let
-        val _ = case get_first (test_card_size test_fun) enumeration_card_size of
+        val _ = case get_first (test_card_size test_fun genuine_only) enumeration_card_size of
           SOME (card, ts) => Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
         | NONE => ()
       in !current_result end
@@ -276,11 +278,11 @@
 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)
+    val if_t = Const (@{const_name "If"}, @{typ bool} --> 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);
+      (if_t $ cond $ then_t $ else_t true) $
+      (if_t $ genuine_only $ Const (@{const_name "None"}, T) $ else_t false)
   end
 
 fun collect_results f [] results = results
diff -r 196697f71488 -r 394ecd91434a src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Dec 05 12:35:04 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Dec 05 12:35:05 2011 +0100
@@ -11,8 +11,8 @@
     -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     -> seed -> (('a -> 'b) * (unit -> term)) * seed
   val compile_generator_expr:
-    Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
-  val put_counterexample: (unit -> int -> int -> seed -> (bool * term list) option * seed)
+    Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
+  val put_counterexample: (unit -> int -> bool -> int -> seed -> (bool * term list) option * seed)
     -> Proof.context -> Proof.context
   val put_counterexample_report: (unit -> int -> int -> seed -> (term list option * (bool list * bool)) * seed)
     -> Proof.context -> Proof.context
@@ -272,7 +272,7 @@
 
 structure Counterexample = Proof_Data
 (
-  type T = unit -> int -> int -> int * int -> (bool * term list) option * (int * int)
+  type T = unit -> int -> bool -> int -> int * int -> (bool * term list) option * (int * int)
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample"
 );
@@ -298,7 +298,9 @@
       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
     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 = Quickcheck_Common.mk_safe_if ctxt (result, Const (@{const_name "None"}, resultT),
+    val ([genuine_only_name], ctxt') = Variable.variant_fixes ["genuine_only"] ctxt
+    val genuine_only = Free (genuine_only_name, @{typ bool})
+    val check = Quickcheck_Common.mk_safe_if genuine_only (result, Const (@{const_name "None"}, resultT),
       fn genuine => @{term "Some :: bool * term list => (bool * term list) option"} $
         HOLogic.mk_prod (Quickcheck_Common.reflect_bool genuine, terms))
     val return = HOLogic.pair_const resultT @{typ Random.seed};
@@ -313,7 +315,10 @@
         (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;
+  in
+    lambda genuine_only
+      (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)))
+  end;
 
 fun mk_reporting_generator_expr ctxt (t, eval_terms) =
   let
@@ -420,7 +425,7 @@
                 | SOME q => (SOME (true, q), report)
             end
       in
-        fn [card, size] => apsnd SOME (iterate_and_collect (card, size) iterations empty_report)
+        fn _ => fn [card, size] => apsnd SOME (iterate_and_collect (card, size) iterations empty_report)
       end
     else
       let
@@ -428,13 +433,17 @@
         val compile = Code_Runtime.dynamic_value_strict
           (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
           thy (SOME target)
-          (fn proc => fn g => fn c => fn s =>g c s #>> (Option.map o apsnd o map) proc) t' [];
-        fun single_tester c s = compile c s |> Random_Engine.run
-        fun iterate (card, size) 0 = NONE
-          | iterate (card, size) j =
-            case single_tester card size of NONE => iterate (card, size) (j - 1) | SOME q => SOME q
+          (fn proc => fn g => fn c => fn b => fn s => g c b s
+            #>> (Option.map o apsnd o map) proc) t' [];
+        fun single_tester c b s = compile c b s |> Random_Engine.run
+        fun iterate _ (card, size) 0 = NONE
+          | iterate genuine_only (card, size) j =
+            case single_tester card genuine_only size of
+              NONE => iterate genuine_only (card, size) (j - 1)
+            | SOME q => SOME q
       in
-        fn [card, size] => (rpair NONE (iterate (card, size) iterations))
+        fn genuine_only => fn [card, size] =>
+          (rpair NONE (iterate genuine_only (card, size) iterations))
       end
   end;