# HG changeset patch
# User bulwahn
# Date 1320996765 -3600
# Node ID dc2236b19a3def67a26b312b46425abc986460f3
# Parent  eeffd04cd89957e39695541554afc81830ac6edf
adding CPS compilation to predicate compiler;
removing function_flattening reference;
new testers smart_exhaustive and smart_slow_exhaustive;
renaming PredicateCompFuns to Predicate_Comp_Funs;

diff -r eeffd04cd899 -r dc2236b19a3d src/HOL/Library/Predicate_Compile_Quickcheck.thy
--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Fri Nov 11 08:32:44 2011 +0100
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Fri Nov 11 08:32:45 2011 +0100
@@ -9,12 +9,4 @@
 
 setup {* Predicate_Compile_Quickcheck.setup *}
 
-(*setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term
-  Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4)) *}
-setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_fs",
-  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4)) *}
-setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_nofs",
-  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4)) *}
-*)
-
 end
\ No newline at end of file
diff -r eeffd04cd899 -r dc2236b19a3d src/HOL/Predicate_Compile.thy
--- a/src/HOL/Predicate_Compile.thy	Fri Nov 11 08:32:44 2011 +0100
+++ b/src/HOL/Predicate_Compile.thy	Fri Nov 11 08:32:45 2011 +0100
@@ -5,7 +5,7 @@
 header {* A compiler for predicates defined by introduction rules *}
 
 theory Predicate_Compile
-imports New_Random_Sequence
+imports New_Random_Sequence Quickcheck_Exhaustive
 uses
   "Tools/Predicate_Compile/predicate_compile_aux.ML"
   "Tools/Predicate_Compile/predicate_compile_compilations.ML"
diff -r eeffd04cd899 -r dc2236b19a3d src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Nov 11 08:32:44 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Nov 11 08:32:45 2011 +0100
@@ -427,7 +427,6 @@
 
 subsection {* Fast exhaustive combinators *}
 
-
 class fast_exhaustive = term_of +
   fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
 
@@ -439,6 +438,89 @@
 code_const catch_Counterexample
   (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
 
+subsection {* Continuation passing style functions as plus monad *}
+  
+type_synonym 'a cps = "('a => term list option) => term list option"
+
+definition cps_empty :: "'a cps"
+where
+  "cps_empty = (%cont. None)"
+
+definition cps_single :: "'a => 'a cps"
+where
+  "cps_single v = (%cont. cont v)"
+
+definition cps_bind :: "'a cps => ('a => 'b cps) => 'b cps" 
+where
+  "cps_bind m f = (%cont. m (%a. (f a) cont))"
+
+definition cps_plus :: "'a cps => 'a cps => 'a cps"
+where
+  "cps_plus a b = (%c. case a c of None => b c | Some x => Some x)"
+
+definition cps_if :: "bool => unit cps"
+where
+  "cps_if b = (if b then cps_single () else cps_empty)"
+
+definition cps_not :: "unit cps => unit cps"
+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"
+
+definition pos_bound_cps_empty :: "'a pos_bound_cps"
+where
+  "pos_bound_cps_empty = (%cont i. None)"
+
+definition pos_bound_cps_single :: "'a => 'a pos_bound_cps"
+where
+  "pos_bound_cps_single v = (%cont i. cont v)"
+
+definition pos_bound_cps_bind :: "'a pos_bound_cps => ('a => 'b pos_bound_cps) => 'b pos_bound_cps" 
+where
+  "pos_bound_cps_bind m f = (%cont i. if i = 0 then None else (m (%a. (f a) cont i) (i - 1)))"
+
+definition pos_bound_cps_plus :: "'a pos_bound_cps => 'a pos_bound_cps => 'a pos_bound_cps"
+where
+  "pos_bound_cps_plus a b = (%c i. case a c i of None => b c i | Some x => Some x)"
+
+definition pos_bound_cps_if :: "bool => unit pos_bound_cps"
+where
+  "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
+
+datatype 'a unknown = Unknown | Known 'a
+datatype 'a three_valued = Unknown_value | Value 'a | No_value
+
+type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => code_numeral => term list three_valued"
+
+definition neg_bound_cps_empty :: "'a neg_bound_cps"
+where
+  "neg_bound_cps_empty = (%cont i. No_value)"
+
+definition neg_bound_cps_single :: "'a => 'a neg_bound_cps"
+where
+  "neg_bound_cps_single v = (%cont i. cont (Known v))"
+
+definition neg_bound_cps_bind :: "'a neg_bound_cps => ('a => 'b neg_bound_cps) => 'b neg_bound_cps" 
+where
+  "neg_bound_cps_bind m f = (%cont i. if i = 0 then cont Unknown else m (%a. case a of Unknown => cont Unknown | Known a' => f a' cont i) (i - 1))"
+
+definition neg_bound_cps_plus :: "'a neg_bound_cps => 'a neg_bound_cps => 'a neg_bound_cps"
+where
+  "neg_bound_cps_plus a b = (%c i. case a c i of No_value => b c i | Value x => Value x | Unknown_value => (case b c i of No_value => Unknown_value | Value x => Value x | Unknown_value => Unknown_value))"
+
+definition neg_bound_cps_if :: "bool => unit neg_bound_cps"
+where
+  "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
+
+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)"
+
+definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps"
+where
+  "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
+
 subsection {* Defining combinators for any first-order data type *}
 
 definition catch_match :: "term list option => term list option => term list option"
@@ -456,6 +538,12 @@
 
 hide_fact orelse_def catch_match_def
 no_notation orelse (infixr "orelse" 55)
-hide_const (open) orelse catch_match mk_map_term check_all_n_lists
+hide_const (open) orelse catch_match mk_map_term check_all_n_lists 
 
-end
\ No newline at end of file
+hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
+hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
+  pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
+  neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
+  Unknown Known Unknown_value Value No_value
+
+end
diff -r eeffd04cd899 -r dc2236b19a3d src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 11 08:32:44 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 11 08:32:45 2011 +0100
@@ -90,8 +90,8 @@
   val funT_of : compilation_funs -> mode -> typ -> typ
   (* Different compilations *)
   datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
-    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
-    | Pos_Generator_DSeq | Neg_Generator_DSeq
+    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq 
+    | Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS
   val negative_compilation_of : compilation -> compilation
   val compilation_for_polarity : bool -> compilation -> compilation
   val is_depth_limited_compilation : compilation -> bool 
@@ -642,14 +642,16 @@
 
 datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
   | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq |
-    Pos_Generator_DSeq | Neg_Generator_DSeq
+    Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS
 
 fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq
   | negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq
   | negative_compilation_of New_Pos_Random_DSeq = New_Neg_Random_DSeq
   | negative_compilation_of New_Neg_Random_DSeq = New_Pos_Random_DSeq
   | negative_compilation_of Pos_Generator_DSeq = Neg_Generator_DSeq
-  | negative_compilation_of Pos_Generator_DSeq = Pos_Generator_DSeq
+  | negative_compilation_of Neg_Generator_DSeq = Pos_Generator_DSeq
+  | negative_compilation_of Pos_Generator_CPS = Neg_Generator_CPS
+  | negative_compilation_of Neg_Generator_CPS = Pos_Generator_CPS  
   | negative_compilation_of c = c
   
 fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
@@ -674,7 +676,9 @@
   | New_Neg_Random_DSeq => "new_neg_random_dseq"
   | Pos_Generator_DSeq => "pos_generator_dseq"
   | Neg_Generator_DSeq => "neg_generator_dseq"
-
+  | Pos_Generator_CPS => "pos_generator_cps"
+  | Neg_Generator_CPS => "neg_generator_cps"
+  
 val compilation_names = [("pred", Pred),
   ("random", Random),
   ("depth_limited", Depth_Limited),
@@ -683,13 +687,14 @@
   ("dseq", DSeq),
   ("random_dseq", Pos_Random_DSeq),
   ("new_random_dseq", New_Pos_Random_DSeq),
-  ("generator_dseq", Pos_Generator_DSeq)]
+  ("generator_dseq", Pos_Generator_DSeq),
+  ("generator_cps", Pos_Generator_CPS)]
 
 val non_random_compilations = [Pred, Depth_Limited, DSeq, Annotated]
 
 
 val random_compilations = [Random, Depth_Limited_Random,
-  Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq]
+  Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq, Pos_Generator_CPS]
 
 (* datastructures and setup for generic compilation *)
 
diff -r eeffd04cd899 -r dc2236b19a3d src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Fri Nov 11 08:32:44 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Fri Nov 11 08:32:45 2011 +0100
@@ -4,7 +4,7 @@
 Structures for different compilations of the predicate compiler.
 *)
 
-structure PredicateCompFuns =
+structure Predicate_Comp_Funs =
 struct
 
 fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
@@ -64,11 +64,162 @@
 
 end;
 
+structure CPS_Comp_Funs =
+struct
+
+fun mk_predT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"}
+
+fun dest_predT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T
+  | dest_predT T = raise TYPE ("dest_predT", [T], []);
+
+fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_predT T);
+
+fun mk_single t =
+  let val T = fastype_of t
+  in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_predT T) $ t end;
+
+fun mk_bind (x, f) =
+  let val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name Quickcheck_Exhaustive.cps_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus};
+
+fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if},
+  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
+
+fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
+
+fun mk_not t =
+  let
+    val T = mk_predT HOLogic.unitT
+  in Const (@{const_name Quickcheck_Exhaustive.cps_not}, T --> T) $ t end
+
+fun mk_Enum f = error "not implemented"
+
+fun mk_Eval (f, x) = error "not implemented"
+
+fun dest_Eval t = error "not implemented"
+
+fun mk_map T1 T2 tf tp = error "not implemented"
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
+    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
+
+end;
+
+structure Pos_Bounded_CPS_Comp_Funs =
+struct
+
+fun mk_predT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "code_numeral => Code_Evaluation.term list option"}
+
+fun dest_predT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "code_numeral => term list option"}])) = T
+  | dest_predT T = raise TYPE ("dest_predT", [T], []);
+
+fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_predT T);
+
+fun mk_single t =
+  let val T = fastype_of t
+  in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_predT T) $ t end;
+
+fun mk_bind (x, f) =
+  let val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus};
+
+fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
+  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
+
+fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
+
+fun mk_not t =
+  let
+    val nT = @{typ "(unit Quickcheck_Exhaustive.unknown =>
+      Code_Evaluation.term list Quickcheck_Exhaustive.three_valued) => code_numeral =>
+      Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
+    val T = mk_predT HOLogic.unitT
+  in Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_not}, nT --> T) $ t end
+
+fun mk_Enum f = error "not implemented"
+
+fun mk_Eval (f, x) = error "not implemented"
+
+fun dest_Eval t = error "not implemented"
+
+fun mk_map T1 T2 tf tp = error "not implemented"
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
+    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
+
+end;
+
+structure Neg_Bounded_CPS_Comp_Funs =
+struct
+
+fun mk_predT T =
+  (Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T])
+    --> @{typ "Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"})
+    --> @{typ "code_numeral => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
+
+fun dest_predT (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]),
+    @{typ "term list Quickcheck_Exhaustive.three_valued"}]),
+    @{typ "code_numeral => term list Quickcheck_Exhaustive.three_valued"}])) = T
+  | dest_predT T = raise TYPE ("dest_predT", [T], []);
+
+fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_predT T);
+
+fun mk_single t =
+  let val T = fastype_of t
+  in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_predT T) $ t end;
+
+fun mk_bind (x, f) =
+  let val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus};
+
+fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if},
+  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
+
+fun mk_iterate_upto T (f, from, to) = error "not implemented"
+
+fun mk_not t =
+  let
+    val T = mk_predT HOLogic.unitT
+    val pT = @{typ "(unit => Code_Evaluation.term list option) => code_numeral => 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"
+
+fun mk_Eval (f, x) = error "not implemented"
+
+fun dest_Eval t = error "not implemented"
+
+fun mk_map T1 T2 tf tp = error "not implemented"
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
+    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
+
+end;
+
+
 structure RandomPredCompFuns =
 struct
 
 fun mk_randompredT T =
-  @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
+  @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_predT T, @{typ Random.seed})
 
 fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
   [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
@@ -157,48 +308,6 @@
 
 end;
 
-structure DSequence_CompFuns =
-struct
-
-fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
-  Type (@{type_name Option.option}, [Type  (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
-
-fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
-  Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
-  | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
-
-fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
-
-fun mk_single t =
-  let val T = fastype_of t
-  in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
-
-fun mk_bind (x, f) =
-  let val T as Type ("fun", [_, U]) = fastype_of f
-  in
-    Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
-  end;
-
-val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
-
-fun mk_if cond = Const (@{const_name DSequence.if_seq},
-  HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
-
-fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
-
-fun mk_not t = let val T = mk_dseqT HOLogic.unitT
-  in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
-  (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
-
-val compfuns = Predicate_Compile_Aux.CompilationFuns
-    {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
-    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
-    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
-
-end;
-
 structure New_Pos_DSequence_CompFuns =
 struct
 
diff -r eeffd04cd899 -r dc2236b19a3d src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 11 08:32:44 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 11 08:32:45 2011 +0100
@@ -45,6 +45,7 @@
   val add_random_dseq_equations : options -> string list -> theory -> theory
   val add_new_random_dseq_equations : options -> string list -> theory -> theory
   val add_generator_dseq_equations : options -> string list -> theory -> theory
+  val add_generator_cps_equations : options -> string list -> theory -> theory
   val mk_tracing : string -> term -> term
   val prepare_intrs : options -> Proof.context -> string list -> thm list ->
     ((string * typ) list * string list * string list * (string * mode list) list *
@@ -298,7 +299,7 @@
   {
   compilation = Depth_Limited,
   function_name_prefix = "depth_limited_",
-  compfuns = PredicateCompFuns.compfuns,
+  compfuns = Predicate_Comp_Funs.compfuns,
   mk_random = (fn _ => error "no random generation"),
   additional_arguments = fn names =>
     let
@@ -332,11 +333,11 @@
   {
   compilation = Random,
   function_name_prefix = "random_",
-  compfuns = PredicateCompFuns.compfuns,
+  compfuns = Predicate_Comp_Funs.compfuns,
   mk_random = (fn T => fn additional_arguments =>
   list_comb (Const(@{const_name Quickcheck.iter},
   [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
-    PredicateCompFuns.mk_predT T), additional_arguments)),
+    Predicate_Comp_Funs.mk_predT T), additional_arguments)),
   modify_funT = (fn T =>
     let
       val (Ts, U) = strip_type T
@@ -358,11 +359,11 @@
   {
   compilation = Depth_Limited_Random,
   function_name_prefix = "depth_limited_random_",
-  compfuns = PredicateCompFuns.compfuns,
+  compfuns = Predicate_Comp_Funs.compfuns,
   mk_random = (fn T => fn additional_arguments =>
   list_comb (Const(@{const_name Quickcheck.iter},
   [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
-    PredicateCompFuns.mk_predT T), tl additional_arguments)),
+    Predicate_Comp_Funs.mk_predT T), tl additional_arguments)),
   modify_funT = (fn T =>
     let
       val (Ts, U) = strip_type T
@@ -403,7 +404,7 @@
   {
   compilation = Pred,
   function_name_prefix = "",
-  compfuns = PredicateCompFuns.compfuns,
+  compfuns = Predicate_Comp_Funs.compfuns,
   mk_random = (fn _ => error "no random generation"),
   modify_funT = I,
   additional_arguments = K [],
@@ -416,7 +417,7 @@
   {
   compilation = Annotated,
   function_name_prefix = "annotated_",
-  compfuns = PredicateCompFuns.compfuns,
+  compfuns = Predicate_Comp_Funs.compfuns,
   mk_random = (fn _ => error "no random generation"),
   modify_funT = I,
   additional_arguments = K [],
@@ -527,7 +528,7 @@
    : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   transform_additional_arguments = K I : (indprem -> term list -> term list)
   }
-
+  
 val neg_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   {
   compilation = Neg_Generator_DSeq,
@@ -541,6 +542,35 @@
   transform_additional_arguments = K I : (indprem -> term list -> term list)
   }
 
+val pos_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = Pos_Generator_CPS,
+  function_name_prefix = "generator_cps_pos_",
+  compfuns = Pos_Bounded_CPS_Comp_Funs.compfuns,
+  mk_random =
+    (fn T => fn additional_arguments =>
+       Const (@{const_name "Quickcheck_Exhaustive.exhaustive"},
+       (T --> @{typ "term list option"}) --> @{typ "code_numeral => term list option"})),
+  modify_funT = I,
+  additional_arguments = K [],
+  wrap_compilation = K (K (K (K (K I))))
+   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
+  transform_additional_arguments = K I : (indprem -> term list -> term list)
+  }  
+
+val neg_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = Neg_Generator_CPS,
+  function_name_prefix = "generator_cps_neg_",
+  compfuns = Neg_Bounded_CPS_Comp_Funs.compfuns,
+  mk_random = (fn _ => error "No enumerators"),
+  modify_funT = I,
+  additional_arguments = K [],
+  wrap_compilation = K (K (K (K (K I))))
+   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
+  transform_additional_arguments = K I : (indprem -> term list -> term list)
+  }
+  
 fun negative_comp_modifiers_of comp_modifiers =
     (case Comp_Mod.compilation comp_modifiers of
       Pos_Random_DSeq => neg_random_dseq_comp_modifiers
@@ -549,6 +579,8 @@
     | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers 
     | Pos_Generator_DSeq => neg_generator_dseq_comp_modifiers
     | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
+    | Pos_Generator_CPS => neg_generator_cps_comp_modifiers
+    | Neg_Generator_CPS => pos_generator_cps_comp_modifiers
     | c => comp_modifiers)
 
 (* term construction *)
@@ -593,7 +625,7 @@
     val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
     val (inargs, outargs) = split_mode mode args
     val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
-    val inner_term = PredicateCompFuns.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
+    val inner_term = Predicate_Comp_Funs.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
   in
     fold_rev mk_split_abs (binder_types T) inner_term
   end
@@ -1018,11 +1050,11 @@
       end
   | mk_args is_eval ((m as Fun _), T) names =
     let
-      val funT = funT_of PredicateCompFuns.compfuns m T
+      val funT = funT_of Predicate_Comp_Funs.compfuns m T
       val x = singleton (Name.variant_list names) "x"
       val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
       val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
-      val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
+      val t = fold_rev HOLogic.tupled_lambda args (Predicate_Comp_Funs.mk_Eval
         (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
     in
       (if is_eval then t else Free (x, funT), x :: names)
@@ -1042,7 +1074,7 @@
     fun strip_eval _ t =
       let
         val t' = strip_split_abs t
-        val (r, _) = PredicateCompFuns.dest_Eval t'
+        val (r, _) = Predicate_Comp_Funs.dest_Eval t'
       in (SOME (fst (strip_comb r)), NONE) end
     val (inargs, outargs) = split_map_mode strip_eval mode args
     val eval_hoargs = ho_args_of mode args
@@ -1054,9 +1086,9 @@
     val predpropI = HOLogic.mk_Trueprop (list_comb (pred, args'))
     val predpropE = HOLogic.mk_Trueprop (list_comb (pred, args))
     val param_eqs = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) eval_hoargs hoargs'
-    val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, inargs),
+    val funpropE = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs),
                     if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs))
-    val funpropI = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, inargs),
+    val funpropI = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs),
                      HOLogic.mk_tuple outargs))
     val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
     val simprules = [defthm, @{thm eval_pred},
@@ -1073,8 +1105,8 @@
         let
           val neg_predpropI = HOLogic.mk_Trueprop (HOLogic.mk_not (list_comb (pred, args')))
           val neg_funpropI =
-            HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval
-              (PredicateCompFuns.mk_not (list_comb (funtrm, inargs)), HOLogic.unit))
+            HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval
+              (Predicate_Comp_Funs.mk_not (list_comb (funtrm, inargs)), HOLogic.unit))
           val neg_introtrm = Logic.list_implies (neg_predpropI :: param_eqs, neg_funpropI)
           val tac =
             Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps
@@ -1099,7 +1131,7 @@
 
 fun create_definitions options preds (name, modes) thy =
   let
-    val compfuns = PredicateCompFuns.compfuns
+    val compfuns = Predicate_Comp_Funs.compfuns
     val T = AList.lookup (op =) preds name |> the
     fun create_definition mode thy =
       let
@@ -1110,11 +1142,11 @@
         fun strip_eval m t =
           let
             val t' = strip_split_abs t
-            val (r, _) = PredicateCompFuns.dest_Eval t'
+            val (r, _) = Predicate_Comp_Funs.dest_Eval t'
           in (SOME (fst (strip_comb r)), NONE) end
         val (inargs, outargs) = split_map_mode strip_eval mode args
         val predterm = fold_rev HOLogic.tupled_lambda inargs
-          (PredicateCompFuns.mk_Enum (HOLogic.tupled_lambda (HOLogic.mk_tuple outargs)
+          (Predicate_Comp_Funs.mk_Enum (HOLogic.tupled_lambda (HOLogic.mk_tuple outargs)
             (list_comb (Const (name, T), args))))
         val lhs = Const (mode_cname, funT)
         val def = Logic.mk_equals (lhs, predterm)
@@ -1309,7 +1341,7 @@
               (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
             val args = map2 (curry Free) arg_names Ts
             val predfun = Const (function_name_of Pred ctxt predname full_mode,
-              Ts ---> PredicateCompFuns.mk_predT @{typ unit})
+              Ts ---> Predicate_Comp_Funs.mk_predT @{typ unit})
             val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
             val eq_term = HOLogic.mk_Trueprop
               (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
@@ -1440,7 +1472,7 @@
   (Steps {
   define_functions =
     fn options => fn preds => fn (s, modes) =>
-    define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns
+    define_functions depth_limited_comp_modifiers Predicate_Comp_Funs.compfuns
     options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   prove = prove_by_skip,
   add_code_equations = K (K I),
@@ -1452,7 +1484,7 @@
   (Steps {
   define_functions =
     fn options => fn preds => fn (s, modes) =>
-      define_functions annotated_comp_modifiers PredicateCompFuns.compfuns options preds
+      define_functions annotated_comp_modifiers Predicate_Comp_Funs.compfuns options preds
       (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   prove = prove_by_skip,
   add_code_equations = K (K I),
@@ -1464,7 +1496,7 @@
   (Steps {
   define_functions =
     fn options => fn preds => fn (s, modes) =>
-      define_functions random_comp_modifiers PredicateCompFuns.compfuns options preds
+      define_functions random_comp_modifiers Predicate_Comp_Funs.compfuns options preds
       (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   comp_modifiers = random_comp_modifiers,
   prove = prove_by_skip,
@@ -1476,7 +1508,7 @@
   (Steps {
   define_functions =
     fn options => fn preds => fn (s, modes) =>
-      define_functions depth_limited_random_comp_modifiers PredicateCompFuns.compfuns options preds
+      define_functions depth_limited_random_comp_modifiers Predicate_Comp_Funs.compfuns options preds
       (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   comp_modifiers = depth_limited_random_comp_modifiers,
   prove = prove_by_skip,
@@ -1551,6 +1583,26 @@
   use_generators = true,
   qname = "generator_dseq_equation"})
 
+val add_generator_cps_equations = gen_add_equations
+  (Steps {
+  define_functions =
+  fn options => fn preds => fn (s, modes) =>
+    let
+      val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
+      val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
+    in 
+      define_functions pos_generator_cps_comp_modifiers Pos_Bounded_CPS_Comp_Funs.compfuns
+        options preds (s, pos_modes)
+      #> define_functions neg_generator_cps_comp_modifiers Neg_Bounded_CPS_Comp_Funs.compfuns
+        options preds (s, neg_modes)
+    end,
+  prove = prove_by_skip,
+  add_code_equations = K (K I),
+  comp_modifiers = pos_generator_cps_comp_modifiers,
+  use_generators = true,
+  qname = "generator_cps_equation"})
+  
+  
 (** user interface **)
 
 (* code_pred_intro attribute *)
@@ -1616,6 +1668,7 @@
            | Depth_Limited_Random => add_depth_limited_random_equations
            | New_Pos_Random_DSeq => add_new_random_dseq_equations
            | Pos_Generator_DSeq => add_generator_dseq_equations
+           | Pos_Generator_CPS => add_generator_cps_equations
            | compilation => error ("Compilation not supported")
            ) options [const]))
       end
diff -r eeffd04cd899 -r dc2236b19a3d src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Nov 11 08:32:44 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Nov 11 08:32:45 2011 +0100
@@ -142,7 +142,7 @@
   let
     val concl' = Logic.strip_assums_concl (hd (prems_of st))
     val concl = HOLogic.dest_Trueprop concl'
-    val expr = fst (strip_comb (fst (PredicateCompFuns.dest_Eval concl)))
+    val expr = fst (strip_comb (fst (Predicate_Comp_Funs.dest_Eval concl)))
     fun valid_expr (Const (@{const_name Predicate.bind}, _)) = true
       | valid_expr (Const (@{const_name Predicate.single}, _)) = true
       | valid_expr _ = false
diff -r eeffd04cd899 -r dc2236b19a3d src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 11 08:32:44 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 11 08:32:45 2011 +0100
@@ -18,12 +18,13 @@
       Proof.context -> Proof.context;
   val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) ->
     Proof.context -> Proof.context
-  val test_goals : (Predicate_Compile_Aux.compilation * bool * bool) ->
+  val put_cps_result : (unit -> int -> 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
       -> Quickcheck.result list
   val nrandom : int Unsynchronized.ref;
   val debug : bool Unsynchronized.ref;
-  val function_flattening : bool Unsynchronized.ref;
   val no_higher_order_predicate : string list Unsynchronized.ref;
   val setup : theory -> theory
 end;
@@ -67,14 +68,20 @@
 );
 val put_new_dseq_result = New_Dseq_Result.put;
 
+structure CPS_Result = Proof_Data
+(
+  type T = unit -> int -> term list option
+  (* FIXME avoid user error with non-user text *)
+  fun init _ () = error "CPS_Result"
+);
+val put_cps_result = CPS_Result.put;
+
 val target = "Quickcheck"
 
 val nrandom = Unsynchronized.ref 3;
 
 val debug = Unsynchronized.ref false;
 
-val function_flattening = Unsynchronized.ref true;
-
 val no_higher_order_predicate = Unsynchronized.ref ([] : string list);
 
 val options = Options {
@@ -177,12 +184,11 @@
 
 fun get_options () = 
   set_no_higher_order_predicate (!no_higher_order_predicate)
-    (set_function_flattening (!function_flattening)
-      (if !debug then debug_options else options))
+    (if !debug then debug_options else options)
 
-val mk_predT = Predicate_Compile_Aux.mk_predT PredicateCompFuns.compfuns
-val mk_return' = Predicate_Compile_Aux.mk_single PredicateCompFuns.compfuns
-val mk_bind' = Predicate_Compile_Aux.mk_bind PredicateCompFuns.compfuns
+val mk_predT = Predicate_Compile_Aux.mk_predT Predicate_Comp_Funs.compfuns
+val mk_return' = Predicate_Compile_Aux.mk_single Predicate_Comp_Funs.compfuns
+val mk_bind' = Predicate_Compile_Aux.mk_bind Predicate_Comp_Funs.compfuns
 
 val mk_randompredT = Predicate_Compile_Aux.mk_predT RandomPredCompFuns.compfuns
 val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns
@@ -203,6 +209,13 @@
   Predicate_Compile_Aux.mk_bind New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
   
 
+val mk_cpsT =
+  Predicate_Compile_Aux.mk_predT Pos_Bounded_CPS_Comp_Funs.compfuns
+val mk_cps_return =
+  Predicate_Compile_Aux.mk_single Pos_Bounded_CPS_Comp_Funs.compfuns
+val mk_cps_bind =
+  Predicate_Compile_Aux.mk_bind Pos_Bounded_CPS_Comp_Funs.compfuns
+
 val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
 
 fun cpu_time description e =
@@ -227,11 +240,11 @@
               Predicate_Compile_Core.add_new_random_dseq_equations options [full_constname] thy3
           | Pos_Generator_DSeq =>
               Predicate_Compile_Core.add_generator_dseq_equations options [full_constname] thy3
+          | Pos_Generator_CPS =>
+               Predicate_Compile_Core.add_generator_cps_equations options [full_constname] thy3
           (*| Depth_Limited_Random =>
               Predicate_Compile_Core.add_depth_limited_random_equations options [full_constname] thy3*))
     (*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*)
-    val _ = Output.tracing ("Preprocessing time: " ^ string_of_int (snd preproc_time))
-    val _ = Output.tracing ("Core compilation time: " ^ string_of_int (snd core_comp_time))
     val ctxt4 = Proof_Context.init_global thy4
     val modes = Core_Data.modes_of compilation ctxt4 full_constname
     val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
@@ -247,10 +260,12 @@
             | Depth_Limited_Random =>
               [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
               @{typ "code_numeral * code_numeral"}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
+            | Pos_Generator_CPS => mk_cpsT (HOLogic.mk_tupleT (map snd vs'))
         in
           Const (name, T)
         end
       else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes))
+    fun mk_Some T = Const (@{const_name "Option.Some"}, T --> Type (@{type_name "Option.option"}, [T]))
     val qc_term =
       case compilation of
           Pos_Random_DSeq => mk_bind (prog,
@@ -262,6 +277,9 @@
         | Pos_Generator_DSeq => mk_gen_bind (prog,
             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'))))     
         | Depth_Limited_Random => fold_rev absdummy
             [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
              @{typ "code_numeral * code_numeral"}]
@@ -309,6 +327,17 @@
           in
             fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth))
           end
+      | Pos_Generator_CPS =>
+          let
+            val compiled_term =
+              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))
+                qc_term []
+          in
+            fn size => fn nrandom => compiled_term
+          end
        | Depth_Limited_Random =>
           let
             val compiled_term = Code_Runtime.dynamic_value_strict
@@ -370,9 +399,10 @@
   end
 
 
-fun test_goals options ctxt (limit_time, is_interactive) insts goals =
+fun test_goals options ctxt catch_code_errors insts goals =
   let
-    val (compilation, function_flattening, fail_safe_function_flattening) = options
+    val (compilation, fail_safe_function_flattening) = options
+    val function_flattening = Config.get ctxt (Quickcheck.allow_function_inversion)
     val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
     val test_term =
       quickcheck_compile_term compilation function_flattening fail_safe_function_flattening
@@ -380,18 +410,14 @@
     Quickcheck_Common.collect_results (test_term ctxt)
       (maps (map snd) correct_inst_goals) []
   end
-  
-val wo_ff_active = Attrib.setup_config_bool @{binding quickcheck_pc_wo_ff_active} (K false);
-val ff_active = Attrib.setup_config_bool @{binding quickcheck_pc_ff_active} (K false);
-val ff_nofs_active = Attrib.setup_config_bool @{binding quickcheck_pc_ff_nofs_active} (K false);
+
+val smart_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_smart_exhaustive_active} (K true);
+val smart_slow_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_slow_smart_exhaustive_active} (K false);
 
 val setup = 
-  Context.theory_map (Quickcheck.add_tester ("predicate_compile_wo_ff",
-    (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, false, true))))
-  #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_fs",
-    (ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true))))
-  #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_nofs",
-    (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true))))
-
+  Context.theory_map (Quickcheck.add_tester ("smart_exhaustive",
+    (smart_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_CPS, false))))
+  #> Context.theory_map (Quickcheck.add_tester ("smart_slow_exhaustive",
+    (smart_slow_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_DSeq, false))))
 
 end;