adding CPS compilation to predicate compiler;
authorbulwahn
Fri Nov 11 08:32:45 2011 +0100 (2011-11-11)
changeset 45450dc2236b19a3d
parent 45449 eeffd04cd899
child 45451 74515e8e6046
adding CPS compilation to predicate compiler;
removing function_flattening reference;
new testers smart_exhaustive and smart_slow_exhaustive;
renaming PredicateCompFuns to Predicate_Comp_Funs;
src/HOL/Library/Predicate_Compile_Quickcheck.thy
src/HOL/Predicate_Compile.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
     1.1 --- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Fri Nov 11 08:32:44 2011 +0100
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Fri Nov 11 08:32:45 2011 +0100
     1.3 @@ -9,12 +9,4 @@
     1.4  
     1.5  setup {* Predicate_Compile_Quickcheck.setup *}
     1.6  
     1.7 -(*setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term
     1.8 -  Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4)) *}
     1.9 -setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_fs",
    1.10 -  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4)) *}
    1.11 -setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_nofs",
    1.12 -  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4)) *}
    1.13 -*)
    1.14 -
    1.15  end
    1.16 \ No newline at end of file
     2.1 --- a/src/HOL/Predicate_Compile.thy	Fri Nov 11 08:32:44 2011 +0100
     2.2 +++ b/src/HOL/Predicate_Compile.thy	Fri Nov 11 08:32:45 2011 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* A compiler for predicates defined by introduction rules *}
     2.5  
     2.6  theory Predicate_Compile
     2.7 -imports New_Random_Sequence
     2.8 +imports New_Random_Sequence Quickcheck_Exhaustive
     2.9  uses
    2.10    "Tools/Predicate_Compile/predicate_compile_aux.ML"
    2.11    "Tools/Predicate_Compile/predicate_compile_compilations.ML"
     3.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Nov 11 08:32:44 2011 +0100
     3.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Nov 11 08:32:45 2011 +0100
     3.3 @@ -427,7 +427,6 @@
     3.4  
     3.5  subsection {* Fast exhaustive combinators *}
     3.6  
     3.7 -
     3.8  class fast_exhaustive = term_of +
     3.9    fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
    3.10  
    3.11 @@ -439,6 +438,89 @@
    3.12  code_const catch_Counterexample
    3.13    (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
    3.14  
    3.15 +subsection {* Continuation passing style functions as plus monad *}
    3.16 +  
    3.17 +type_synonym 'a cps = "('a => term list option) => term list option"
    3.18 +
    3.19 +definition cps_empty :: "'a cps"
    3.20 +where
    3.21 +  "cps_empty = (%cont. None)"
    3.22 +
    3.23 +definition cps_single :: "'a => 'a cps"
    3.24 +where
    3.25 +  "cps_single v = (%cont. cont v)"
    3.26 +
    3.27 +definition cps_bind :: "'a cps => ('a => 'b cps) => 'b cps" 
    3.28 +where
    3.29 +  "cps_bind m f = (%cont. m (%a. (f a) cont))"
    3.30 +
    3.31 +definition cps_plus :: "'a cps => 'a cps => 'a cps"
    3.32 +where
    3.33 +  "cps_plus a b = (%c. case a c of None => b c | Some x => Some x)"
    3.34 +
    3.35 +definition cps_if :: "bool => unit cps"
    3.36 +where
    3.37 +  "cps_if b = (if b then cps_single () else cps_empty)"
    3.38 +
    3.39 +definition cps_not :: "unit cps => unit cps"
    3.40 +where
    3.41 +  "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)"
    3.42 +
    3.43 +type_synonym 'a pos_bound_cps = "('a => term list option) => code_numeral => term list option"
    3.44 +
    3.45 +definition pos_bound_cps_empty :: "'a pos_bound_cps"
    3.46 +where
    3.47 +  "pos_bound_cps_empty = (%cont i. None)"
    3.48 +
    3.49 +definition pos_bound_cps_single :: "'a => 'a pos_bound_cps"
    3.50 +where
    3.51 +  "pos_bound_cps_single v = (%cont i. cont v)"
    3.52 +
    3.53 +definition pos_bound_cps_bind :: "'a pos_bound_cps => ('a => 'b pos_bound_cps) => 'b pos_bound_cps" 
    3.54 +where
    3.55 +  "pos_bound_cps_bind m f = (%cont i. if i = 0 then None else (m (%a. (f a) cont i) (i - 1)))"
    3.56 +
    3.57 +definition pos_bound_cps_plus :: "'a pos_bound_cps => 'a pos_bound_cps => 'a pos_bound_cps"
    3.58 +where
    3.59 +  "pos_bound_cps_plus a b = (%c i. case a c i of None => b c i | Some x => Some x)"
    3.60 +
    3.61 +definition pos_bound_cps_if :: "bool => unit pos_bound_cps"
    3.62 +where
    3.63 +  "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
    3.64 +
    3.65 +datatype 'a unknown = Unknown | Known 'a
    3.66 +datatype 'a three_valued = Unknown_value | Value 'a | No_value
    3.67 +
    3.68 +type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => code_numeral => term list three_valued"
    3.69 +
    3.70 +definition neg_bound_cps_empty :: "'a neg_bound_cps"
    3.71 +where
    3.72 +  "neg_bound_cps_empty = (%cont i. No_value)"
    3.73 +
    3.74 +definition neg_bound_cps_single :: "'a => 'a neg_bound_cps"
    3.75 +where
    3.76 +  "neg_bound_cps_single v = (%cont i. cont (Known v))"
    3.77 +
    3.78 +definition neg_bound_cps_bind :: "'a neg_bound_cps => ('a => 'b neg_bound_cps) => 'b neg_bound_cps" 
    3.79 +where
    3.80 +  "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))"
    3.81 +
    3.82 +definition neg_bound_cps_plus :: "'a neg_bound_cps => 'a neg_bound_cps => 'a neg_bound_cps"
    3.83 +where
    3.84 +  "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))"
    3.85 +
    3.86 +definition neg_bound_cps_if :: "bool => unit neg_bound_cps"
    3.87 +where
    3.88 +  "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
    3.89 +
    3.90 +definition neg_bound_cps_not :: "unit pos_bound_cps => unit neg_bound_cps"
    3.91 +where
    3.92 +  "neg_bound_cps_not n = (%c i. case n (%u. Some []) i of None => c (Known ()) | Some _ => No_value)"
    3.93 +
    3.94 +definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps"
    3.95 +where
    3.96 +  "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
    3.97 +
    3.98  subsection {* Defining combinators for any first-order data type *}
    3.99  
   3.100  definition catch_match :: "term list option => term list option => term list option"
   3.101 @@ -456,6 +538,12 @@
   3.102  
   3.103  hide_fact orelse_def catch_match_def
   3.104  no_notation orelse (infixr "orelse" 55)
   3.105 -hide_const (open) orelse catch_match mk_map_term check_all_n_lists
   3.106 +hide_const (open) orelse catch_match mk_map_term check_all_n_lists 
   3.107  
   3.108 -end
   3.109 \ No newline at end of file
   3.110 +hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
   3.111 +hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
   3.112 +  pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
   3.113 +  neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
   3.114 +  Unknown Known Unknown_value Value No_value
   3.115 +
   3.116 +end
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 11 08:32:44 2011 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 11 08:32:45 2011 +0100
     4.3 @@ -90,8 +90,8 @@
     4.4    val funT_of : compilation_funs -> mode -> typ -> typ
     4.5    (* Different compilations *)
     4.6    datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
     4.7 -    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
     4.8 -    | Pos_Generator_DSeq | Neg_Generator_DSeq
     4.9 +    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq 
    4.10 +    | Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS
    4.11    val negative_compilation_of : compilation -> compilation
    4.12    val compilation_for_polarity : bool -> compilation -> compilation
    4.13    val is_depth_limited_compilation : compilation -> bool 
    4.14 @@ -642,14 +642,16 @@
    4.15  
    4.16  datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
    4.17    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq |
    4.18 -    Pos_Generator_DSeq | Neg_Generator_DSeq
    4.19 +    Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS
    4.20  
    4.21  fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq
    4.22    | negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq
    4.23    | negative_compilation_of New_Pos_Random_DSeq = New_Neg_Random_DSeq
    4.24    | negative_compilation_of New_Neg_Random_DSeq = New_Pos_Random_DSeq
    4.25    | negative_compilation_of Pos_Generator_DSeq = Neg_Generator_DSeq
    4.26 -  | negative_compilation_of Pos_Generator_DSeq = Pos_Generator_DSeq
    4.27 +  | negative_compilation_of Neg_Generator_DSeq = Pos_Generator_DSeq
    4.28 +  | negative_compilation_of Pos_Generator_CPS = Neg_Generator_CPS
    4.29 +  | negative_compilation_of Neg_Generator_CPS = Pos_Generator_CPS  
    4.30    | negative_compilation_of c = c
    4.31    
    4.32  fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
    4.33 @@ -674,7 +676,9 @@
    4.34    | New_Neg_Random_DSeq => "new_neg_random_dseq"
    4.35    | Pos_Generator_DSeq => "pos_generator_dseq"
    4.36    | Neg_Generator_DSeq => "neg_generator_dseq"
    4.37 -
    4.38 +  | Pos_Generator_CPS => "pos_generator_cps"
    4.39 +  | Neg_Generator_CPS => "neg_generator_cps"
    4.40 +  
    4.41  val compilation_names = [("pred", Pred),
    4.42    ("random", Random),
    4.43    ("depth_limited", Depth_Limited),
    4.44 @@ -683,13 +687,14 @@
    4.45    ("dseq", DSeq),
    4.46    ("random_dseq", Pos_Random_DSeq),
    4.47    ("new_random_dseq", New_Pos_Random_DSeq),
    4.48 -  ("generator_dseq", Pos_Generator_DSeq)]
    4.49 +  ("generator_dseq", Pos_Generator_DSeq),
    4.50 +  ("generator_cps", Pos_Generator_CPS)]
    4.51  
    4.52  val non_random_compilations = [Pred, Depth_Limited, DSeq, Annotated]
    4.53  
    4.54  
    4.55  val random_compilations = [Random, Depth_Limited_Random,
    4.56 -  Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq]
    4.57 +  Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq, Pos_Generator_CPS]
    4.58  
    4.59  (* datastructures and setup for generic compilation *)
    4.60  
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Fri Nov 11 08:32:44 2011 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Fri Nov 11 08:32:45 2011 +0100
     5.3 @@ -4,7 +4,7 @@
     5.4  Structures for different compilations of the predicate compiler.
     5.5  *)
     5.6  
     5.7 -structure PredicateCompFuns =
     5.8 +structure Predicate_Comp_Funs =
     5.9  struct
    5.10  
    5.11  fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
    5.12 @@ -64,11 +64,162 @@
    5.13  
    5.14  end;
    5.15  
    5.16 +structure CPS_Comp_Funs =
    5.17 +struct
    5.18 +
    5.19 +fun mk_predT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"}
    5.20 +
    5.21 +fun dest_predT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T
    5.22 +  | dest_predT T = raise TYPE ("dest_predT", [T], []);
    5.23 +
    5.24 +fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_predT T);
    5.25 +
    5.26 +fun mk_single t =
    5.27 +  let val T = fastype_of t
    5.28 +  in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_predT T) $ t end;
    5.29 +
    5.30 +fun mk_bind (x, f) =
    5.31 +  let val T as Type ("fun", [_, U]) = fastype_of f
    5.32 +  in
    5.33 +    Const (@{const_name Quickcheck_Exhaustive.cps_bind}, fastype_of x --> T --> U) $ x $ f
    5.34 +  end;
    5.35 +
    5.36 +val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus};
    5.37 +
    5.38 +fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if},
    5.39 +  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
    5.40 +
    5.41 +fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
    5.42 +
    5.43 +fun mk_not t =
    5.44 +  let
    5.45 +    val T = mk_predT HOLogic.unitT
    5.46 +  in Const (@{const_name Quickcheck_Exhaustive.cps_not}, T --> T) $ t end
    5.47 +
    5.48 +fun mk_Enum f = error "not implemented"
    5.49 +
    5.50 +fun mk_Eval (f, x) = error "not implemented"
    5.51 +
    5.52 +fun dest_Eval t = error "not implemented"
    5.53 +
    5.54 +fun mk_map T1 T2 tf tp = error "not implemented"
    5.55 +
    5.56 +val compfuns = Predicate_Compile_Aux.CompilationFuns
    5.57 +    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
    5.58 +    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
    5.59 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
    5.60 +
    5.61 +end;
    5.62 +
    5.63 +structure Pos_Bounded_CPS_Comp_Funs =
    5.64 +struct
    5.65 +
    5.66 +fun mk_predT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "code_numeral => Code_Evaluation.term list option"}
    5.67 +
    5.68 +fun dest_predT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "code_numeral => term list option"}])) = T
    5.69 +  | dest_predT T = raise TYPE ("dest_predT", [T], []);
    5.70 +
    5.71 +fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_predT T);
    5.72 +
    5.73 +fun mk_single t =
    5.74 +  let val T = fastype_of t
    5.75 +  in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_predT T) $ t end;
    5.76 +
    5.77 +fun mk_bind (x, f) =
    5.78 +  let val T as Type ("fun", [_, U]) = fastype_of f
    5.79 +  in
    5.80 +    Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
    5.81 +  end;
    5.82 +
    5.83 +val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus};
    5.84 +
    5.85 +fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
    5.86 +  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
    5.87 +
    5.88 +fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
    5.89 +
    5.90 +fun mk_not t =
    5.91 +  let
    5.92 +    val nT = @{typ "(unit Quickcheck_Exhaustive.unknown =>
    5.93 +      Code_Evaluation.term list Quickcheck_Exhaustive.three_valued) => code_numeral =>
    5.94 +      Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
    5.95 +    val T = mk_predT HOLogic.unitT
    5.96 +  in Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_not}, nT --> T) $ t end
    5.97 +
    5.98 +fun mk_Enum f = error "not implemented"
    5.99 +
   5.100 +fun mk_Eval (f, x) = error "not implemented"
   5.101 +
   5.102 +fun dest_Eval t = error "not implemented"
   5.103 +
   5.104 +fun mk_map T1 T2 tf tp = error "not implemented"
   5.105 +
   5.106 +val compfuns = Predicate_Compile_Aux.CompilationFuns
   5.107 +    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
   5.108 +    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   5.109 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
   5.110 +
   5.111 +end;
   5.112 +
   5.113 +structure Neg_Bounded_CPS_Comp_Funs =
   5.114 +struct
   5.115 +
   5.116 +fun mk_predT T =
   5.117 +  (Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T])
   5.118 +    --> @{typ "Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"})
   5.119 +    --> @{typ "code_numeral => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
   5.120 +
   5.121 +fun dest_predT (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]),
   5.122 +    @{typ "term list Quickcheck_Exhaustive.three_valued"}]),
   5.123 +    @{typ "code_numeral => term list Quickcheck_Exhaustive.three_valued"}])) = T
   5.124 +  | dest_predT T = raise TYPE ("dest_predT", [T], []);
   5.125 +
   5.126 +fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_predT T);
   5.127 +
   5.128 +fun mk_single t =
   5.129 +  let val T = fastype_of t
   5.130 +  in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_predT T) $ t end;
   5.131 +
   5.132 +fun mk_bind (x, f) =
   5.133 +  let val T as Type ("fun", [_, U]) = fastype_of f
   5.134 +  in
   5.135 +    Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
   5.136 +  end;
   5.137 +
   5.138 +val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus};
   5.139 +
   5.140 +fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if},
   5.141 +  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
   5.142 +
   5.143 +fun mk_iterate_upto T (f, from, to) = error "not implemented"
   5.144 +
   5.145 +fun mk_not t =
   5.146 +  let
   5.147 +    val T = mk_predT HOLogic.unitT
   5.148 +    val pT = @{typ "(unit => Code_Evaluation.term list option) => code_numeral => Code_Evaluation.term list option"}
   5.149 +  in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end
   5.150 +
   5.151 +fun mk_Enum f = error "not implemented"
   5.152 +
   5.153 +fun mk_Eval (f, x) = error "not implemented"
   5.154 +
   5.155 +fun dest_Eval t = error "not implemented"
   5.156 +
   5.157 +fun mk_map T1 T2 tf tp = error "not implemented"
   5.158 +
   5.159 +val compfuns = Predicate_Compile_Aux.CompilationFuns
   5.160 +    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
   5.161 +    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   5.162 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
   5.163 +
   5.164 +end;
   5.165 +
   5.166 +
   5.167  structure RandomPredCompFuns =
   5.168  struct
   5.169  
   5.170  fun mk_randompredT T =
   5.171 -  @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
   5.172 +  @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_predT T, @{typ Random.seed})
   5.173  
   5.174  fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
   5.175    [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
   5.176 @@ -157,48 +308,6 @@
   5.177  
   5.178  end;
   5.179  
   5.180 -structure DSequence_CompFuns =
   5.181 -struct
   5.182 -
   5.183 -fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
   5.184 -  Type (@{type_name Option.option}, [Type  (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
   5.185 -
   5.186 -fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
   5.187 -  Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
   5.188 -  | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
   5.189 -
   5.190 -fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
   5.191 -
   5.192 -fun mk_single t =
   5.193 -  let val T = fastype_of t
   5.194 -  in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
   5.195 -
   5.196 -fun mk_bind (x, f) =
   5.197 -  let val T as Type ("fun", [_, U]) = fastype_of f
   5.198 -  in
   5.199 -    Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
   5.200 -  end;
   5.201 -
   5.202 -val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
   5.203 -
   5.204 -fun mk_if cond = Const (@{const_name DSequence.if_seq},
   5.205 -  HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
   5.206 -
   5.207 -fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
   5.208 -
   5.209 -fun mk_not t = let val T = mk_dseqT HOLogic.unitT
   5.210 -  in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
   5.211 -
   5.212 -fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
   5.213 -  (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
   5.214 -
   5.215 -val compfuns = Predicate_Compile_Aux.CompilationFuns
   5.216 -    {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
   5.217 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   5.218 -    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   5.219 -
   5.220 -end;
   5.221 -
   5.222  structure New_Pos_DSequence_CompFuns =
   5.223  struct
   5.224  
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 11 08:32:44 2011 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 11 08:32:45 2011 +0100
     6.3 @@ -45,6 +45,7 @@
     6.4    val add_random_dseq_equations : options -> string list -> theory -> theory
     6.5    val add_new_random_dseq_equations : options -> string list -> theory -> theory
     6.6    val add_generator_dseq_equations : options -> string list -> theory -> theory
     6.7 +  val add_generator_cps_equations : options -> string list -> theory -> theory
     6.8    val mk_tracing : string -> term -> term
     6.9    val prepare_intrs : options -> Proof.context -> string list -> thm list ->
    6.10      ((string * typ) list * string list * string list * (string * mode list) list *
    6.11 @@ -298,7 +299,7 @@
    6.12    {
    6.13    compilation = Depth_Limited,
    6.14    function_name_prefix = "depth_limited_",
    6.15 -  compfuns = PredicateCompFuns.compfuns,
    6.16 +  compfuns = Predicate_Comp_Funs.compfuns,
    6.17    mk_random = (fn _ => error "no random generation"),
    6.18    additional_arguments = fn names =>
    6.19      let
    6.20 @@ -332,11 +333,11 @@
    6.21    {
    6.22    compilation = Random,
    6.23    function_name_prefix = "random_",
    6.24 -  compfuns = PredicateCompFuns.compfuns,
    6.25 +  compfuns = Predicate_Comp_Funs.compfuns,
    6.26    mk_random = (fn T => fn additional_arguments =>
    6.27    list_comb (Const(@{const_name Quickcheck.iter},
    6.28    [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
    6.29 -    PredicateCompFuns.mk_predT T), additional_arguments)),
    6.30 +    Predicate_Comp_Funs.mk_predT T), additional_arguments)),
    6.31    modify_funT = (fn T =>
    6.32      let
    6.33        val (Ts, U) = strip_type T
    6.34 @@ -358,11 +359,11 @@
    6.35    {
    6.36    compilation = Depth_Limited_Random,
    6.37    function_name_prefix = "depth_limited_random_",
    6.38 -  compfuns = PredicateCompFuns.compfuns,
    6.39 +  compfuns = Predicate_Comp_Funs.compfuns,
    6.40    mk_random = (fn T => fn additional_arguments =>
    6.41    list_comb (Const(@{const_name Quickcheck.iter},
    6.42    [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
    6.43 -    PredicateCompFuns.mk_predT T), tl additional_arguments)),
    6.44 +    Predicate_Comp_Funs.mk_predT T), tl additional_arguments)),
    6.45    modify_funT = (fn T =>
    6.46      let
    6.47        val (Ts, U) = strip_type T
    6.48 @@ -403,7 +404,7 @@
    6.49    {
    6.50    compilation = Pred,
    6.51    function_name_prefix = "",
    6.52 -  compfuns = PredicateCompFuns.compfuns,
    6.53 +  compfuns = Predicate_Comp_Funs.compfuns,
    6.54    mk_random = (fn _ => error "no random generation"),
    6.55    modify_funT = I,
    6.56    additional_arguments = K [],
    6.57 @@ -416,7 +417,7 @@
    6.58    {
    6.59    compilation = Annotated,
    6.60    function_name_prefix = "annotated_",
    6.61 -  compfuns = PredicateCompFuns.compfuns,
    6.62 +  compfuns = Predicate_Comp_Funs.compfuns,
    6.63    mk_random = (fn _ => error "no random generation"),
    6.64    modify_funT = I,
    6.65    additional_arguments = K [],
    6.66 @@ -527,7 +528,7 @@
    6.67     : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
    6.68    transform_additional_arguments = K I : (indprem -> term list -> term list)
    6.69    }
    6.70 -
    6.71 +  
    6.72  val neg_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
    6.73    {
    6.74    compilation = Neg_Generator_DSeq,
    6.75 @@ -541,6 +542,35 @@
    6.76    transform_additional_arguments = K I : (indprem -> term list -> term list)
    6.77    }
    6.78  
    6.79 +val pos_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers
    6.80 +  {
    6.81 +  compilation = Pos_Generator_CPS,
    6.82 +  function_name_prefix = "generator_cps_pos_",
    6.83 +  compfuns = Pos_Bounded_CPS_Comp_Funs.compfuns,
    6.84 +  mk_random =
    6.85 +    (fn T => fn additional_arguments =>
    6.86 +       Const (@{const_name "Quickcheck_Exhaustive.exhaustive"},
    6.87 +       (T --> @{typ "term list option"}) --> @{typ "code_numeral => term list option"})),
    6.88 +  modify_funT = I,
    6.89 +  additional_arguments = K [],
    6.90 +  wrap_compilation = K (K (K (K (K I))))
    6.91 +   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
    6.92 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
    6.93 +  }  
    6.94 +
    6.95 +val neg_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers
    6.96 +  {
    6.97 +  compilation = Neg_Generator_CPS,
    6.98 +  function_name_prefix = "generator_cps_neg_",
    6.99 +  compfuns = Neg_Bounded_CPS_Comp_Funs.compfuns,
   6.100 +  mk_random = (fn _ => error "No enumerators"),
   6.101 +  modify_funT = I,
   6.102 +  additional_arguments = K [],
   6.103 +  wrap_compilation = K (K (K (K (K I))))
   6.104 +   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   6.105 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
   6.106 +  }
   6.107 +  
   6.108  fun negative_comp_modifiers_of comp_modifiers =
   6.109      (case Comp_Mod.compilation comp_modifiers of
   6.110        Pos_Random_DSeq => neg_random_dseq_comp_modifiers
   6.111 @@ -549,6 +579,8 @@
   6.112      | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers 
   6.113      | Pos_Generator_DSeq => neg_generator_dseq_comp_modifiers
   6.114      | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
   6.115 +    | Pos_Generator_CPS => neg_generator_cps_comp_modifiers
   6.116 +    | Neg_Generator_CPS => pos_generator_cps_comp_modifiers
   6.117      | c => comp_modifiers)
   6.118  
   6.119  (* term construction *)
   6.120 @@ -593,7 +625,7 @@
   6.121      val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
   6.122      val (inargs, outargs) = split_mode mode args
   6.123      val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
   6.124 -    val inner_term = PredicateCompFuns.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
   6.125 +    val inner_term = Predicate_Comp_Funs.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
   6.126    in
   6.127      fold_rev mk_split_abs (binder_types T) inner_term
   6.128    end
   6.129 @@ -1018,11 +1050,11 @@
   6.130        end
   6.131    | mk_args is_eval ((m as Fun _), T) names =
   6.132      let
   6.133 -      val funT = funT_of PredicateCompFuns.compfuns m T
   6.134 +      val funT = funT_of Predicate_Comp_Funs.compfuns m T
   6.135        val x = singleton (Name.variant_list names) "x"
   6.136        val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
   6.137        val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
   6.138 -      val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
   6.139 +      val t = fold_rev HOLogic.tupled_lambda args (Predicate_Comp_Funs.mk_Eval
   6.140          (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
   6.141      in
   6.142        (if is_eval then t else Free (x, funT), x :: names)
   6.143 @@ -1042,7 +1074,7 @@
   6.144      fun strip_eval _ t =
   6.145        let
   6.146          val t' = strip_split_abs t
   6.147 -        val (r, _) = PredicateCompFuns.dest_Eval t'
   6.148 +        val (r, _) = Predicate_Comp_Funs.dest_Eval t'
   6.149        in (SOME (fst (strip_comb r)), NONE) end
   6.150      val (inargs, outargs) = split_map_mode strip_eval mode args
   6.151      val eval_hoargs = ho_args_of mode args
   6.152 @@ -1054,9 +1086,9 @@
   6.153      val predpropI = HOLogic.mk_Trueprop (list_comb (pred, args'))
   6.154      val predpropE = HOLogic.mk_Trueprop (list_comb (pred, args))
   6.155      val param_eqs = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) eval_hoargs hoargs'
   6.156 -    val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, inargs),
   6.157 +    val funpropE = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs),
   6.158                      if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs))
   6.159 -    val funpropI = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, inargs),
   6.160 +    val funpropI = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs),
   6.161                       HOLogic.mk_tuple outargs))
   6.162      val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
   6.163      val simprules = [defthm, @{thm eval_pred},
   6.164 @@ -1073,8 +1105,8 @@
   6.165          let
   6.166            val neg_predpropI = HOLogic.mk_Trueprop (HOLogic.mk_not (list_comb (pred, args')))
   6.167            val neg_funpropI =
   6.168 -            HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval
   6.169 -              (PredicateCompFuns.mk_not (list_comb (funtrm, inargs)), HOLogic.unit))
   6.170 +            HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval
   6.171 +              (Predicate_Comp_Funs.mk_not (list_comb (funtrm, inargs)), HOLogic.unit))
   6.172            val neg_introtrm = Logic.list_implies (neg_predpropI :: param_eqs, neg_funpropI)
   6.173            val tac =
   6.174              Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps
   6.175 @@ -1099,7 +1131,7 @@
   6.176  
   6.177  fun create_definitions options preds (name, modes) thy =
   6.178    let
   6.179 -    val compfuns = PredicateCompFuns.compfuns
   6.180 +    val compfuns = Predicate_Comp_Funs.compfuns
   6.181      val T = AList.lookup (op =) preds name |> the
   6.182      fun create_definition mode thy =
   6.183        let
   6.184 @@ -1110,11 +1142,11 @@
   6.185          fun strip_eval m t =
   6.186            let
   6.187              val t' = strip_split_abs t
   6.188 -            val (r, _) = PredicateCompFuns.dest_Eval t'
   6.189 +            val (r, _) = Predicate_Comp_Funs.dest_Eval t'
   6.190            in (SOME (fst (strip_comb r)), NONE) end
   6.191          val (inargs, outargs) = split_map_mode strip_eval mode args
   6.192          val predterm = fold_rev HOLogic.tupled_lambda inargs
   6.193 -          (PredicateCompFuns.mk_Enum (HOLogic.tupled_lambda (HOLogic.mk_tuple outargs)
   6.194 +          (Predicate_Comp_Funs.mk_Enum (HOLogic.tupled_lambda (HOLogic.mk_tuple outargs)
   6.195              (list_comb (Const (name, T), args))))
   6.196          val lhs = Const (mode_cname, funT)
   6.197          val def = Logic.mk_equals (lhs, predterm)
   6.198 @@ -1309,7 +1341,7 @@
   6.199                (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
   6.200              val args = map2 (curry Free) arg_names Ts
   6.201              val predfun = Const (function_name_of Pred ctxt predname full_mode,
   6.202 -              Ts ---> PredicateCompFuns.mk_predT @{typ unit})
   6.203 +              Ts ---> Predicate_Comp_Funs.mk_predT @{typ unit})
   6.204              val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
   6.205              val eq_term = HOLogic.mk_Trueprop
   6.206                (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
   6.207 @@ -1440,7 +1472,7 @@
   6.208    (Steps {
   6.209    define_functions =
   6.210      fn options => fn preds => fn (s, modes) =>
   6.211 -    define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns
   6.212 +    define_functions depth_limited_comp_modifiers Predicate_Comp_Funs.compfuns
   6.213      options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   6.214    prove = prove_by_skip,
   6.215    add_code_equations = K (K I),
   6.216 @@ -1452,7 +1484,7 @@
   6.217    (Steps {
   6.218    define_functions =
   6.219      fn options => fn preds => fn (s, modes) =>
   6.220 -      define_functions annotated_comp_modifiers PredicateCompFuns.compfuns options preds
   6.221 +      define_functions annotated_comp_modifiers Predicate_Comp_Funs.compfuns options preds
   6.222        (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   6.223    prove = prove_by_skip,
   6.224    add_code_equations = K (K I),
   6.225 @@ -1464,7 +1496,7 @@
   6.226    (Steps {
   6.227    define_functions =
   6.228      fn options => fn preds => fn (s, modes) =>
   6.229 -      define_functions random_comp_modifiers PredicateCompFuns.compfuns options preds
   6.230 +      define_functions random_comp_modifiers Predicate_Comp_Funs.compfuns options preds
   6.231        (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   6.232    comp_modifiers = random_comp_modifiers,
   6.233    prove = prove_by_skip,
   6.234 @@ -1476,7 +1508,7 @@
   6.235    (Steps {
   6.236    define_functions =
   6.237      fn options => fn preds => fn (s, modes) =>
   6.238 -      define_functions depth_limited_random_comp_modifiers PredicateCompFuns.compfuns options preds
   6.239 +      define_functions depth_limited_random_comp_modifiers Predicate_Comp_Funs.compfuns options preds
   6.240        (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   6.241    comp_modifiers = depth_limited_random_comp_modifiers,
   6.242    prove = prove_by_skip,
   6.243 @@ -1551,6 +1583,26 @@
   6.244    use_generators = true,
   6.245    qname = "generator_dseq_equation"})
   6.246  
   6.247 +val add_generator_cps_equations = gen_add_equations
   6.248 +  (Steps {
   6.249 +  define_functions =
   6.250 +  fn options => fn preds => fn (s, modes) =>
   6.251 +    let
   6.252 +      val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
   6.253 +      val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
   6.254 +    in 
   6.255 +      define_functions pos_generator_cps_comp_modifiers Pos_Bounded_CPS_Comp_Funs.compfuns
   6.256 +        options preds (s, pos_modes)
   6.257 +      #> define_functions neg_generator_cps_comp_modifiers Neg_Bounded_CPS_Comp_Funs.compfuns
   6.258 +        options preds (s, neg_modes)
   6.259 +    end,
   6.260 +  prove = prove_by_skip,
   6.261 +  add_code_equations = K (K I),
   6.262 +  comp_modifiers = pos_generator_cps_comp_modifiers,
   6.263 +  use_generators = true,
   6.264 +  qname = "generator_cps_equation"})
   6.265 +  
   6.266 +  
   6.267  (** user interface **)
   6.268  
   6.269  (* code_pred_intro attribute *)
   6.270 @@ -1616,6 +1668,7 @@
   6.271             | Depth_Limited_Random => add_depth_limited_random_equations
   6.272             | New_Pos_Random_DSeq => add_new_random_dseq_equations
   6.273             | Pos_Generator_DSeq => add_generator_dseq_equations
   6.274 +           | Pos_Generator_CPS => add_generator_cps_equations
   6.275             | compilation => error ("Compilation not supported")
   6.276             ) options [const]))
   6.277        end
     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Nov 11 08:32:44 2011 +0100
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Nov 11 08:32:45 2011 +0100
     7.3 @@ -142,7 +142,7 @@
     7.4    let
     7.5      val concl' = Logic.strip_assums_concl (hd (prems_of st))
     7.6      val concl = HOLogic.dest_Trueprop concl'
     7.7 -    val expr = fst (strip_comb (fst (PredicateCompFuns.dest_Eval concl)))
     7.8 +    val expr = fst (strip_comb (fst (Predicate_Comp_Funs.dest_Eval concl)))
     7.9      fun valid_expr (Const (@{const_name Predicate.bind}, _)) = true
    7.10        | valid_expr (Const (@{const_name Predicate.single}, _)) = true
    7.11        | valid_expr _ = false
     8.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 11 08:32:44 2011 +0100
     8.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 11 08:32:45 2011 +0100
     8.3 @@ -18,12 +18,13 @@
     8.4        Proof.context -> Proof.context;
     8.5    val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) ->
     8.6      Proof.context -> Proof.context
     8.7 -  val test_goals : (Predicate_Compile_Aux.compilation * bool * bool) ->
     8.8 +  val put_cps_result : (unit -> int -> term list option) ->
     8.9 +    Proof.context -> Proof.context
    8.10 +  val test_goals : (Predicate_Compile_Aux.compilation * bool) ->
    8.11      Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list
    8.12        -> Quickcheck.result list
    8.13    val nrandom : int Unsynchronized.ref;
    8.14    val debug : bool Unsynchronized.ref;
    8.15 -  val function_flattening : bool Unsynchronized.ref;
    8.16    val no_higher_order_predicate : string list Unsynchronized.ref;
    8.17    val setup : theory -> theory
    8.18  end;
    8.19 @@ -67,14 +68,20 @@
    8.20  );
    8.21  val put_new_dseq_result = New_Dseq_Result.put;
    8.22  
    8.23 +structure CPS_Result = Proof_Data
    8.24 +(
    8.25 +  type T = unit -> int -> term list option
    8.26 +  (* FIXME avoid user error with non-user text *)
    8.27 +  fun init _ () = error "CPS_Result"
    8.28 +);
    8.29 +val put_cps_result = CPS_Result.put;
    8.30 +
    8.31  val target = "Quickcheck"
    8.32  
    8.33  val nrandom = Unsynchronized.ref 3;
    8.34  
    8.35  val debug = Unsynchronized.ref false;
    8.36  
    8.37 -val function_flattening = Unsynchronized.ref true;
    8.38 -
    8.39  val no_higher_order_predicate = Unsynchronized.ref ([] : string list);
    8.40  
    8.41  val options = Options {
    8.42 @@ -177,12 +184,11 @@
    8.43  
    8.44  fun get_options () = 
    8.45    set_no_higher_order_predicate (!no_higher_order_predicate)
    8.46 -    (set_function_flattening (!function_flattening)
    8.47 -      (if !debug then debug_options else options))
    8.48 +    (if !debug then debug_options else options)
    8.49  
    8.50 -val mk_predT = Predicate_Compile_Aux.mk_predT PredicateCompFuns.compfuns
    8.51 -val mk_return' = Predicate_Compile_Aux.mk_single PredicateCompFuns.compfuns
    8.52 -val mk_bind' = Predicate_Compile_Aux.mk_bind PredicateCompFuns.compfuns
    8.53 +val mk_predT = Predicate_Compile_Aux.mk_predT Predicate_Comp_Funs.compfuns
    8.54 +val mk_return' = Predicate_Compile_Aux.mk_single Predicate_Comp_Funs.compfuns
    8.55 +val mk_bind' = Predicate_Compile_Aux.mk_bind Predicate_Comp_Funs.compfuns
    8.56  
    8.57  val mk_randompredT = Predicate_Compile_Aux.mk_predT RandomPredCompFuns.compfuns
    8.58  val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns
    8.59 @@ -203,6 +209,13 @@
    8.60    Predicate_Compile_Aux.mk_bind New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
    8.61    
    8.62  
    8.63 +val mk_cpsT =
    8.64 +  Predicate_Compile_Aux.mk_predT Pos_Bounded_CPS_Comp_Funs.compfuns
    8.65 +val mk_cps_return =
    8.66 +  Predicate_Compile_Aux.mk_single Pos_Bounded_CPS_Comp_Funs.compfuns
    8.67 +val mk_cps_bind =
    8.68 +  Predicate_Compile_Aux.mk_bind Pos_Bounded_CPS_Comp_Funs.compfuns
    8.69 +
    8.70  val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
    8.71  
    8.72  fun cpu_time description e =
    8.73 @@ -227,11 +240,11 @@
    8.74                Predicate_Compile_Core.add_new_random_dseq_equations options [full_constname] thy3
    8.75            | Pos_Generator_DSeq =>
    8.76                Predicate_Compile_Core.add_generator_dseq_equations options [full_constname] thy3
    8.77 +          | Pos_Generator_CPS =>
    8.78 +               Predicate_Compile_Core.add_generator_cps_equations options [full_constname] thy3
    8.79            (*| Depth_Limited_Random =>
    8.80                Predicate_Compile_Core.add_depth_limited_random_equations options [full_constname] thy3*))
    8.81      (*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*)
    8.82 -    val _ = Output.tracing ("Preprocessing time: " ^ string_of_int (snd preproc_time))
    8.83 -    val _ = Output.tracing ("Core compilation time: " ^ string_of_int (snd core_comp_time))
    8.84      val ctxt4 = Proof_Context.init_global thy4
    8.85      val modes = Core_Data.modes_of compilation ctxt4 full_constname
    8.86      val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
    8.87 @@ -247,10 +260,12 @@
    8.88              | Depth_Limited_Random =>
    8.89                [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
    8.90                @{typ "code_numeral * code_numeral"}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
    8.91 +            | Pos_Generator_CPS => mk_cpsT (HOLogic.mk_tupleT (map snd vs'))
    8.92          in
    8.93            Const (name, T)
    8.94          end
    8.95        else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes))
    8.96 +    fun mk_Some T = Const (@{const_name "Option.Some"}, T --> Type (@{type_name "Option.option"}, [T]))
    8.97      val qc_term =
    8.98        case compilation of
    8.99            Pos_Random_DSeq => mk_bind (prog,
   8.100 @@ -262,6 +277,9 @@
   8.101          | Pos_Generator_DSeq => mk_gen_bind (prog,
   8.102              mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
   8.103              (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
   8.104 +        | Pos_Generator_CPS => prog $
   8.105 +            mk_split_lambda (map Free vs') (mk_Some @{typ "term list"} $ (HOLogic.mk_list @{typ term}
   8.106 +            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))     
   8.107          | Depth_Limited_Random => fold_rev absdummy
   8.108              [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
   8.109               @{typ "code_numeral * code_numeral"}]
   8.110 @@ -309,6 +327,17 @@
   8.111            in
   8.112              fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth))
   8.113            end
   8.114 +      | Pos_Generator_CPS =>
   8.115 +          let
   8.116 +            val compiled_term =
   8.117 +              Code_Runtime.dynamic_value_strict
   8.118 +                (CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
   8.119 +                thy4 (SOME target)
   8.120 +                (fn proc => fn g => fn depth => g depth |> Option.map (map proc))
   8.121 +                qc_term []
   8.122 +          in
   8.123 +            fn size => fn nrandom => compiled_term
   8.124 +          end
   8.125         | Depth_Limited_Random =>
   8.126            let
   8.127              val compiled_term = Code_Runtime.dynamic_value_strict
   8.128 @@ -370,9 +399,10 @@
   8.129    end
   8.130  
   8.131  
   8.132 -fun test_goals options ctxt (limit_time, is_interactive) insts goals =
   8.133 +fun test_goals options ctxt catch_code_errors insts goals =
   8.134    let
   8.135 -    val (compilation, function_flattening, fail_safe_function_flattening) = options
   8.136 +    val (compilation, fail_safe_function_flattening) = options
   8.137 +    val function_flattening = Config.get ctxt (Quickcheck.allow_function_inversion)
   8.138      val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
   8.139      val test_term =
   8.140        quickcheck_compile_term compilation function_flattening fail_safe_function_flattening
   8.141 @@ -380,18 +410,14 @@
   8.142      Quickcheck_Common.collect_results (test_term ctxt)
   8.143        (maps (map snd) correct_inst_goals) []
   8.144    end
   8.145 -  
   8.146 -val wo_ff_active = Attrib.setup_config_bool @{binding quickcheck_pc_wo_ff_active} (K false);
   8.147 -val ff_active = Attrib.setup_config_bool @{binding quickcheck_pc_ff_active} (K false);
   8.148 -val ff_nofs_active = Attrib.setup_config_bool @{binding quickcheck_pc_ff_nofs_active} (K false);
   8.149 +
   8.150 +val smart_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_smart_exhaustive_active} (K true);
   8.151 +val smart_slow_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_slow_smart_exhaustive_active} (K false);
   8.152  
   8.153  val setup = 
   8.154 -  Context.theory_map (Quickcheck.add_tester ("predicate_compile_wo_ff",
   8.155 -    (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, false, true))))
   8.156 -  #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_fs",
   8.157 -    (ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true))))
   8.158 -  #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_nofs",
   8.159 -    (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true))))
   8.160 -
   8.161 +  Context.theory_map (Quickcheck.add_tester ("smart_exhaustive",
   8.162 +    (smart_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_CPS, false))))
   8.163 +  #> Context.theory_map (Quickcheck.add_tester ("smart_slow_exhaustive",
   8.164 +    (smart_slow_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_DSeq, false))))
   8.165  
   8.166  end;