added generator_dseq compilation for a sound depth-limited compilation with small value generators
authorbulwahn
Thu Oct 21 19:13:09 2010 +0200 (2010-10-21)
changeset 40051b6acda4d1c29
parent 40050 638ce4dabe53
child 40052 ea46574ca815
added generator_dseq compilation for a sound depth-limited compilation with small value generators
src/HOL/Lazy_Sequence.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
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Thu Oct 21 19:13:08 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Thu Oct 21 19:13:09 2010 +0200
     1.3 @@ -140,6 +140,71 @@
     1.4    datatypes lazy_sequence = Lazy_Sequence
     1.5    functions map yield yieldn
     1.6  
     1.7 +subsection {* Generator Sequences *}
     1.8 +
     1.9 +
    1.10 +subsubsection {* General lazy sequence operation *}
    1.11 +
    1.12 +definition product :: "'a Lazy_Sequence.lazy_sequence \<Rightarrow> 'b Lazy_Sequence.lazy_sequence \<Rightarrow> ('a * 'b) Lazy_Sequence.lazy_sequence"
    1.13 +where
    1.14 +  "product s1 s2 = Lazy_Sequence.bind s1 (%a. Lazy_Sequence.bind s2 (%b. Lazy_Sequence.single (a, b)))"
    1.15 +
    1.16 +
    1.17 +subsubsection {* small_lazy typeclasses *}
    1.18 +
    1.19 +class small_lazy =
    1.20 +  fixes small_lazy :: "int \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
    1.21 +
    1.22 +instantiation unit :: small_lazy
    1.23 +begin
    1.24 +
    1.25 +definition "small_lazy d = Lazy_Sequence.single ()"
    1.26 +
    1.27 +instance ..
    1.28 +
    1.29 +end
    1.30 +
    1.31 +instantiation int :: small_lazy
    1.32 +begin
    1.33 +
    1.34 +text {* maybe optimise this expression -> append (single x) xs == cons x xs 
    1.35 +Performance difference? *}
    1.36 +
    1.37 +function small_lazy' :: "int => int => int Lazy_Sequence.lazy_sequence"
    1.38 +where "small_lazy' d i = (if d < i then Lazy_Sequence.empty else
    1.39 +  Lazy_Sequence.append (Lazy_Sequence.single i) (small_lazy' d (i + 1)))"
    1.40 +by pat_completeness auto
    1.41 +
    1.42 +termination 
    1.43 +  by (relation "measure (%(d, i). nat (d + 1 - i))") auto
    1.44 +
    1.45 +definition "small_lazy d = small_lazy' d (- d)"
    1.46 +
    1.47 +instance ..
    1.48 +
    1.49 +end
    1.50 +
    1.51 +instantiation prod :: (small_lazy, small_lazy) small_lazy
    1.52 +begin
    1.53 +
    1.54 +definition
    1.55 +  "small_lazy d = product (small_lazy d) (small_lazy d)"
    1.56 +
    1.57 +instance ..
    1.58 +
    1.59 +end
    1.60 +
    1.61 +instantiation list :: (small_lazy) small_lazy
    1.62 +begin
    1.63 +
    1.64 +fun small_lazy_list :: "int => 'a list Lazy_Sequence.lazy_sequence"
    1.65 +where
    1.66 +  "small_lazy_list d = Lazy_Sequence.append (Lazy_Sequence.single []) (if d > 0 then Lazy_Sequence.bind (product (small_lazy (d - 1)) (small_lazy (d - 1))) (%(x, xs). Lazy_Sequence.single (x # xs)) else Lazy_Sequence.empty)"
    1.67 +
    1.68 +instance ..
    1.69 +
    1.70 +end
    1.71 +
    1.72  subsection {* With Hit Bound Value *}
    1.73  text {* assuming in negative context *}
    1.74  
    1.75 @@ -149,7 +214,6 @@
    1.76  where
    1.77    [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
    1.78  
    1.79 -
    1.80  definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
    1.81  where
    1.82    [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
    1.83 @@ -194,7 +258,10 @@
    1.84    "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
    1.85  
    1.86  hide_type (open) lazy_sequence
    1.87 -hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
    1.88 -hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def iterate_upto.simps if_seq_def not_seq_def
    1.89 +hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq
    1.90 +  iterate_upto not_seq product
    1.91 +  
    1.92 +hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def
    1.93 +  iterate_upto.simps product_def if_seq_def not_seq_def
    1.94  
    1.95  end
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:08 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:09 2010 +0200
     2.3 @@ -90,6 +90,7 @@
     2.4    (* Different compilations *)
     2.5    datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
     2.6      | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
     2.7 +    | Pos_Generator_DSeq | Neg_Generator_DSeq
     2.8    val negative_compilation_of : compilation -> compilation
     2.9    val compilation_for_polarity : bool -> compilation -> compilation
    2.10    val is_depth_limited_compilation : compilation -> bool 
    2.11 @@ -635,12 +636,15 @@
    2.12  (* Different compilations *)
    2.13  
    2.14  datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
    2.15 -  | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
    2.16 +  | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq |
    2.17 +    Pos_Generator_DSeq | Neg_Generator_DSeq
    2.18  
    2.19  fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq
    2.20    | negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq
    2.21    | negative_compilation_of New_Pos_Random_DSeq = New_Neg_Random_DSeq
    2.22    | negative_compilation_of New_Neg_Random_DSeq = New_Pos_Random_DSeq
    2.23 +  | negative_compilation_of Pos_Generator_DSeq = Neg_Generator_DSeq
    2.24 +  | negative_compilation_of Pos_Generator_DSeq = Pos_Generator_DSeq
    2.25    | negative_compilation_of c = c
    2.26    
    2.27  fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
    2.28 @@ -648,7 +652,8 @@
    2.29    | compilation_for_polarity _ c = c
    2.30  
    2.31  fun is_depth_limited_compilation c =
    2.32 -  (c = New_Pos_Random_DSeq) orelse (c = New_Neg_Random_DSeq)
    2.33 +  (c = New_Pos_Random_DSeq) orelse (c = New_Neg_Random_DSeq) orelse
    2.34 +  (c = Pos_Generator_DSeq) orelse (c = Pos_Generator_DSeq)
    2.35  
    2.36  fun string_of_compilation c =
    2.37    case c of
    2.38 @@ -662,6 +667,8 @@
    2.39    | Neg_Random_DSeq => "neg_random_dseq"
    2.40    | New_Pos_Random_DSeq => "new_pos_random dseq"
    2.41    | New_Neg_Random_DSeq => "new_neg_random_dseq"
    2.42 +  | Pos_Generator_DSeq => "pos_generator_dseq"
    2.43 +  | Neg_Generator_DSeq => "neg_generator_dseq"
    2.44  
    2.45  val compilation_names = [("pred", Pred),
    2.46    ("random", Random),
    2.47 @@ -669,7 +676,8 @@
    2.48    ("depth_limited_random", Depth_Limited_Random),
    2.49    (*("annotated", Annotated),*)
    2.50    ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq),
    2.51 -  ("new_random_dseq", New_Pos_Random_DSeq)]
    2.52 +  ("new_random_dseq", New_Pos_Random_DSeq),
    2.53 +  ("generator_dseq", Pos_Generator_DSeq)]
    2.54  
    2.55  val non_random_compilations = [Pred, Depth_Limited, DSeq, Annotated]
    2.56  
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Oct 21 19:13:08 2010 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Oct 21 19:13:09 2010 +0200
     3.3 @@ -157,6 +157,170 @@
     3.4  
     3.5  end;
     3.6  
     3.7 +structure DSequence_CompFuns =
     3.8 +struct
     3.9 +
    3.10 +fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
    3.11 +  Type (@{type_name Option.option}, [Type  (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
    3.12 +
    3.13 +fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
    3.14 +  Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
    3.15 +  | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
    3.16 +
    3.17 +fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
    3.18 +
    3.19 +fun mk_single t =
    3.20 +  let val T = fastype_of t
    3.21 +  in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
    3.22 +
    3.23 +fun mk_bind (x, f) =
    3.24 +  let val T as Type ("fun", [_, U]) = fastype_of f
    3.25 +  in
    3.26 +    Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
    3.27 +  end;
    3.28 +
    3.29 +val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
    3.30 +
    3.31 +fun mk_if cond = Const (@{const_name DSequence.if_seq},
    3.32 +  HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
    3.33 +
    3.34 +fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
    3.35 +
    3.36 +fun mk_not t = let val T = mk_dseqT HOLogic.unitT
    3.37 +  in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
    3.38 +
    3.39 +fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
    3.40 +  (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
    3.41 +
    3.42 +val compfuns = Predicate_Compile_Aux.CompilationFuns
    3.43 +    {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
    3.44 +    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
    3.45 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
    3.46 +
    3.47 +end;
    3.48 +
    3.49 +structure New_Pos_DSequence_CompFuns =
    3.50 +struct
    3.51 +
    3.52 +fun mk_pos_dseqT T =
    3.53 +    @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
    3.54 +
    3.55 +fun dest_pos_dseqT (Type ("fun", [@{typ code_numeral},
    3.56 +    Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
    3.57 +  | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], []);
    3.58 +
    3.59 +fun mk_bot T = Const (@{const_name New_DSequence.pos_empty}, mk_pos_dseqT T);
    3.60 +
    3.61 +fun mk_single t =
    3.62 +  let
    3.63 +    val T = fastype_of t
    3.64 +  in Const(@{const_name New_DSequence.pos_single}, T --> mk_pos_dseqT T) $ t end;
    3.65 +
    3.66 +fun mk_bind (x, f) =
    3.67 +  let
    3.68 +    val T as Type ("fun", [_, U]) = fastype_of f
    3.69 +  in
    3.70 +    Const (@{const_name New_DSequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
    3.71 +  end;
    3.72 +  
    3.73 +fun mk_decr_bind (x, f) =
    3.74 +  let
    3.75 +    val T as Type ("fun", [_, U]) = fastype_of f
    3.76 +  in
    3.77 +    Const (@{const_name New_DSequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
    3.78 +  end;
    3.79 +
    3.80 +val mk_sup = HOLogic.mk_binop @{const_name New_DSequence.pos_union};
    3.81 +
    3.82 +fun mk_if cond = Const (@{const_name New_DSequence.pos_if_seq},
    3.83 +  HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
    3.84 +
    3.85 +fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
    3.86 +
    3.87 +fun mk_not t =
    3.88 +  let
    3.89 +    val pT = mk_pos_dseqT HOLogic.unitT
    3.90 +    val nT =
    3.91 +      @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
    3.92 +        [Type (@{type_name Option.option}, [@{typ unit}])])
    3.93 +  in Const (@{const_name New_DSequence.pos_not_seq}, nT --> pT) $ t end
    3.94 +
    3.95 +fun mk_map T1 T2 tf tp = Const (@{const_name New_DSequence.pos_map},
    3.96 +  (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
    3.97 +
    3.98 +val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
    3.99 +    {mk_predT = mk_pos_dseqT, dest_predT = dest_pos_dseqT,
   3.100 +    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.101 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.102 +
   3.103 +val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
   3.104 +    {mk_predT = mk_pos_dseqT, dest_predT = dest_pos_dseqT,
   3.105 +    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.106 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.107 +
   3.108 +end;
   3.109 +
   3.110 +structure New_Neg_DSequence_CompFuns =
   3.111 +struct
   3.112 +
   3.113 +fun mk_neg_dseqT T = @{typ code_numeral} -->
   3.114 +  Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
   3.115 +
   3.116 +fun dest_neg_dseqT (Type ("fun", [@{typ code_numeral},
   3.117 +    Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = T
   3.118 +  | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], []);
   3.119 +
   3.120 +fun mk_bot T = Const (@{const_name New_DSequence.neg_empty}, mk_neg_dseqT T);
   3.121 +
   3.122 +fun mk_single t =
   3.123 +  let
   3.124 +    val T = fastype_of t
   3.125 +  in Const(@{const_name New_DSequence.neg_single}, T --> mk_neg_dseqT T) $ t end;
   3.126 +
   3.127 +fun mk_bind (x, f) =
   3.128 +  let
   3.129 +    val T as Type ("fun", [_, U]) = fastype_of f
   3.130 +  in
   3.131 +    Const (@{const_name New_DSequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
   3.132 +  end;
   3.133 +  
   3.134 +fun mk_decr_bind (x, f) =
   3.135 +  let
   3.136 +    val T as Type ("fun", [_, U]) = fastype_of f
   3.137 +  in
   3.138 +    Const (@{const_name New_DSequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
   3.139 +  end;
   3.140 +
   3.141 +val mk_sup = HOLogic.mk_binop @{const_name New_DSequence.neg_union};
   3.142 +
   3.143 +fun mk_if cond = Const (@{const_name New_DSequence.neg_if_seq},
   3.144 +  HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
   3.145 +
   3.146 +fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
   3.147 +
   3.148 +fun mk_not t =
   3.149 +  let
   3.150 +    val nT = mk_neg_dseqT HOLogic.unitT
   3.151 +    val pT =
   3.152 +      @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
   3.153 +        [@{typ unit}])
   3.154 +  in Const (@{const_name New_DSequence.neg_not_seq}, pT --> nT) $ t end
   3.155 +
   3.156 +fun mk_map T1 T2 tf tp = Const (@{const_name New_DSequence.neg_map},
   3.157 +  (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
   3.158 +
   3.159 +val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
   3.160 +    {mk_predT = mk_neg_dseqT, dest_predT = dest_neg_dseqT,
   3.161 +    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.162 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.163 +
   3.164 +val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
   3.165 +    {mk_predT = mk_neg_dseqT, dest_predT = dest_neg_dseqT,
   3.166 +    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.167 +    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.168 +
   3.169 +end;
   3.170 +
   3.171  structure New_Pos_Random_Sequence_CompFuns =
   3.172  struct
   3.173  
   3.174 @@ -182,7 +346,7 @@
   3.175    in
   3.176      Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
   3.177    end;
   3.178 -  
   3.179 +
   3.180  fun mk_decr_bind (x, f) =
   3.181    let
   3.182      val T as Type ("fun", [_, U]) = fastype_of f
   3.183 @@ -222,7 +386,6 @@
   3.184      {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
   3.185      mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.186      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.187 -
   3.188  end;
   3.189  
   3.190  structure New_Neg_Random_Sequence_CompFuns =
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:08 2010 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:09 2010 +0200
     4.3 @@ -278,7 +278,7 @@
     4.4  fun function_names_of compilation ctxt name =
     4.5    case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
     4.6      NONE => error ("No " ^ string_of_compilation compilation
     4.7 -      ^ "functions defined for predicate " ^ quote name)
     4.8 +      ^ " functions defined for predicate " ^ quote name)
     4.9    | SOME fun_names => fun_names
    4.10  
    4.11  fun function_name_of compilation ctxt name mode =
    4.12 @@ -848,16 +848,27 @@
    4.13  
    4.14  end;
    4.15  
    4.16 -fun unlimited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq =
    4.17 +fun unlimited_compfuns_of true New_Pos_Random_DSeq =
    4.18      New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
    4.19 -  | unlimited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq =
    4.20 +  | unlimited_compfuns_of false New_Pos_Random_DSeq =
    4.21      New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns
    4.22 -  
    4.23 +  | unlimited_compfuns_of true Pos_Generator_DSeq =
    4.24 +    New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
    4.25 +  | unlimited_compfuns_of false Pos_Generator_DSeq =
    4.26 +    New_Neg_DSequence_CompFuns.depth_unlimited_compfuns
    4.27 +  | unlimited_compfuns_of _ c =
    4.28 +    raise Fail ("No unlimited compfuns for compilation " ^ string_of_compilation c)
    4.29 +
    4.30  fun limited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq =
    4.31      New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
    4.32    | limited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq =
    4.33      New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
    4.34 -
    4.35 +  | limited_compfuns_of true Pos_Generator_DSeq =
    4.36 +    New_Pos_DSequence_CompFuns.depth_limited_compfuns
    4.37 +  | limited_compfuns_of false Pos_Generator_DSeq =
    4.38 +    New_Neg_DSequence_CompFuns.depth_limited_compfuns
    4.39 +  | limited_compfuns_of _ c =
    4.40 +    raise Fail ("No limited compfuns for compilation " ^ string_of_compilation c)
    4.41  
    4.42  val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
    4.43    {
    4.44 @@ -997,7 +1008,7 @@
    4.45    compilation = DSeq,
    4.46    function_name_prefix = "dseq_",
    4.47    compfuns = DSequence_CompFuns.compfuns,
    4.48 -  mk_random = (fn _ => error "no random generation"),
    4.49 +  mk_random = (fn _ => error "no random generation in dseq"),
    4.50    modify_funT = I,
    4.51    additional_arguments = K [],
    4.52    wrap_compilation = K (K (K (K (K I))))
    4.53 @@ -1077,12 +1088,49 @@
    4.54    transform_additional_arguments = K I : (indprem -> term list -> term list)
    4.55    }
    4.56  
    4.57 +val pos_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
    4.58 +  {
    4.59 +  compilation = Pos_Generator_DSeq,
    4.60 +  function_name_prefix = "generator_dseq_",
    4.61 +  compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns,
    4.62 +  mk_random =
    4.63 +    (fn T => fn additional_arguments =>
    4.64 +      let
    4.65 +        val small_lazy =
    4.66 +         Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
    4.67 +         @{typ "Int.int"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T])) 
    4.68 +      in
    4.69 +        absdummy (@{typ code_numeral}, small_lazy $ HOLogic.mk_number @{typ int} 3)
    4.70 +      end
    4.71 +    ),
    4.72 +  modify_funT = I,
    4.73 +  additional_arguments = K [],
    4.74 +  wrap_compilation = K (K (K (K (K I))))
    4.75 +   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
    4.76 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
    4.77 +  }
    4.78 +
    4.79 +val neg_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
    4.80 +  {
    4.81 +  compilation = Neg_Generator_DSeq,
    4.82 +  function_name_prefix = "generator_dseq_neg_",
    4.83 +  compfuns = New_Neg_DSequence_CompFuns.depth_limited_compfuns,
    4.84 +  mk_random = (fn _ => error "no random generation"),
    4.85 +  modify_funT = I,
    4.86 +  additional_arguments = K [],
    4.87 +  wrap_compilation = K (K (K (K (K I))))
    4.88 +   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
    4.89 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
    4.90 +  }
    4.91 +
    4.92  fun negative_comp_modifiers_of comp_modifiers =
    4.93      (case Comp_Mod.compilation comp_modifiers of
    4.94        Pos_Random_DSeq => neg_random_dseq_comp_modifiers
    4.95      | Neg_Random_DSeq => pos_random_dseq_comp_modifiers
    4.96      | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers
    4.97 -    | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers
    4.98 +    | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers 
    4.99 +    | Pos_Generator_DSeq => neg_generator_dseq_comp_modifiers
   4.100 +    | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
   4.101      | c => comp_modifiers)
   4.102  
   4.103  (** mode analysis **)
   4.104 @@ -3099,6 +3147,25 @@
   4.105    use_generators = true,
   4.106    qname = "new_random_dseq_equation"})
   4.107  
   4.108 +val add_generator_dseq_equations = gen_add_equations
   4.109 +  (Steps {
   4.110 +  define_functions =
   4.111 +  fn options => fn preds => fn (s, modes) =>
   4.112 +    let
   4.113 +      val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
   4.114 +      val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
   4.115 +    in 
   4.116 +      define_functions pos_generator_dseq_comp_modifiers New_Pos_DSequence_CompFuns.depth_limited_compfuns
   4.117 +        options preds (s, pos_modes)
   4.118 +      #> define_functions neg_generator_dseq_comp_modifiers New_Neg_DSequence_CompFuns.depth_limited_compfuns
   4.119 +        options preds (s, neg_modes)
   4.120 +    end,
   4.121 +  prove = prove_by_skip,
   4.122 +  add_code_equations = K (K I),
   4.123 +  comp_modifiers = pos_generator_dseq_comp_modifiers,
   4.124 +  use_generators = true,
   4.125 +  qname = "generator_dseq_equation"})
   4.126 +
   4.127  (** user interface **)
   4.128  
   4.129  (* code_pred_intro attribute *)
   4.130 @@ -3160,6 +3227,7 @@
   4.131             | Random => add_random_equations
   4.132             | Depth_Limited_Random => add_depth_limited_random_equations
   4.133             | New_Pos_Random_DSeq => add_new_random_dseq_equations
   4.134 +           | Pos_Generator_DSeq => add_generator_dseq_equations
   4.135             | compilation => error ("Compilation not supported")
   4.136             ) options [const]))
   4.137        end