# HG changeset patch
# User bulwahn
# Date 1323025508 -3600
# Node ID 17100f4ce0b5d7977d4570337592f7bd0610723a
# Parent  92c6ddca552ec85e8c3933399dcc682a43aceb3c
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
adjusting smart quickcheck compilation to new signature of exhaustive generators (cf. 1f5fc44254d7);

diff -r 92c6ddca552e -r 17100f4ce0b5 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Dec 04 18:30:57 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Dec 04 20:05:08 2011 +0100
@@ -466,7 +466,7 @@
 where
   "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)"
 
-type_synonym 'a pos_bound_cps = "('a => term list option) => code_numeral => term list option"
+type_synonym 'a pos_bound_cps = "('a => (bool * term list) option) => code_numeral => (bool * term list) option"
 
 definition pos_bound_cps_empty :: "'a pos_bound_cps"
 where
@@ -515,7 +515,7 @@
 
 definition neg_bound_cps_not :: "unit pos_bound_cps => unit neg_bound_cps"
 where
-  "neg_bound_cps_not n = (%c i. case n (%u. Some []) i of None => c (Known ()) | Some _ => No_value)"
+  "neg_bound_cps_not n = (%c i. case n (%u. Some (True, [])) i of None => c (Known ()) | Some _ => No_value)"
 
 definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps"
 where
diff -r 92c6ddca552e -r 17100f4ce0b5 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Dec 04 18:30:57 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Dec 04 20:05:08 2011 +0100
@@ -1039,7 +1039,7 @@
       | _ => NONE
   in
     Quickcheck.Result
-      {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample,
+      {counterexample = Option.map (pair true o curry (op ~~) (Term.add_free_names t [])) counterexample,
        evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
   end;
 
diff -r 92c6ddca552e -r 17100f4ce0b5 src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Sun Dec 04 18:30:57 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Sun Dec 04 20:05:08 2011 +0100
@@ -114,9 +114,11 @@
 structure Pos_Bounded_CPS_Comp_Funs =
 struct
 
-fun mk_monadT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "code_numeral => Code_Evaluation.term list option"}
+val resultT = @{typ "(bool * Code_Evaluation.term list) option"}
+fun mk_monadT T = (T --> resultT) --> @{typ "code_numeral"} --> resultT
 
-fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "code_numeral => term list option"}])) = T
+fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "(bool * term list) option"}]),
+  @{typ "code_numeral => (bool * term list) option"}])) = T
   | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
 
 fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T);
@@ -196,7 +198,8 @@
 fun mk_not t =
   let
     val T = mk_monadT HOLogic.unitT
-    val pT = @{typ "(unit => Code_Evaluation.term list option) => code_numeral => Code_Evaluation.term list option"}
+    val pT = @{typ "(unit => (bool * Code_Evaluation.term list) option)"}
+      --> @{typ "code_numeral => (bool * Code_Evaluation.term list) option"}
   in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end
 
 fun mk_Enum f = error "not implemented"
diff -r 92c6ddca552e -r 17100f4ce0b5 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Dec 04 18:30:57 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Dec 04 20:05:08 2011 +0100
@@ -550,7 +550,8 @@
   mk_random =
     (fn T => fn additional_arguments =>
        Const (@{const_name "Quickcheck_Exhaustive.exhaustive"},
-       (T --> @{typ "term list option"}) --> @{typ "code_numeral => term list option"})),
+       (T --> @{typ "(bool * term list) option"}) -->
+         @{typ "code_numeral => (bool * term list) option"})),
   modify_funT = I,
   additional_arguments = K [],
   wrap_compilation = K (K (K (K (K I))))
diff -r 92c6ddca552e -r 17100f4ce0b5 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sun Dec 04 18:30:57 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sun Dec 04 20:05:08 2011 +0100
@@ -18,7 +18,7 @@
       Proof.context -> Proof.context;
   val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) ->
     Proof.context -> Proof.context
-  val put_cps_result : (unit -> int -> term list option) ->
+  val put_cps_result : (unit -> int -> (bool * term list) option) ->
     Proof.context -> Proof.context
   val test_goals : (Predicate_Compile_Aux.compilation * bool) ->
     Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list
@@ -70,7 +70,7 @@
 
 structure CPS_Result = Proof_Data
 (
-  type T = unit -> int -> term list option
+  type T = unit -> int -> (bool * term list) option
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "CPS_Result"
 );
@@ -278,8 +278,9 @@
             mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
             (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
         | Pos_Generator_CPS => prog $
-            mk_split_lambda (map Free vs') (mk_Some @{typ "term list"} $ (HOLogic.mk_list @{typ term}
-            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))     
+            mk_split_lambda (map Free vs') (mk_Some @{typ "bool * term list"} $
+            HOLogic.mk_prod (@{term "True"}, HOLogic.mk_list @{typ term}
+                (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))     
         | Depth_Limited_Random => fold_rev absdummy
             [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
              @{typ "code_numeral * code_numeral"}]
@@ -333,10 +334,10 @@
               Code_Runtime.dynamic_value_strict
                 (CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
                 thy4 (SOME target)
-                (fn proc => fn g => fn depth => g depth |> Option.map (map proc))
+                (fn proc => fn g => fn depth => g depth |> Option.map (apsnd (map proc)))
                 qc_term []
           in
-            fn size => fn nrandom => compiled_term
+            fn size => fn nrandom => Option.map snd o compiled_term
           end
        | Depth_Limited_Random =>
           let
@@ -385,7 +386,7 @@
     val counterexample = try_upto_depth ctxt (c size (!nrandom))
   in
     Quickcheck.Result
-      {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample,
+      {counterexample = Option.map (pair true o (curry (op ~~)) (Term.add_free_names t [])) counterexample,
        evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
   end