added generator_dseq compilation for a sound depth-limited compilation with small value generators

--- a/src/HOL/Lazy_Sequence.thy	Thu Oct 21 19:13:08 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Thu Oct 21 19:13:09 2010 +0200
@@ -140,6 +140,71 @@
   datatypes lazy_sequence = Lazy_Sequence
   functions map yield yieldn
 
+subsection {* Generator Sequences *}
+
+
+subsubsection {* General lazy sequence operation *}
+
+definition product :: "'a Lazy_Sequence.lazy_sequence \<Rightarrow> 'b Lazy_Sequence.lazy_sequence \<Rightarrow> ('a * 'b) Lazy_Sequence.lazy_sequence"
+where
+  "product s1 s2 = Lazy_Sequence.bind s1 (%a. Lazy_Sequence.bind s2 (%b. Lazy_Sequence.single (a, b)))"
+
+
+subsubsection {* small_lazy typeclasses *}
+
+class small_lazy =
+  fixes small_lazy :: "int \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
+
+instantiation unit :: small_lazy
+begin
+
+definition "small_lazy d = Lazy_Sequence.single ()"
+
+instance ..
+
+end
+
+instantiation int :: small_lazy
+begin
+
+text {* maybe optimise this expression -> append (single x) xs == cons x xs 
+Performance difference? *}
+
+function small_lazy' :: "int => int => int Lazy_Sequence.lazy_sequence"
+where "small_lazy' d i = (if d < i then Lazy_Sequence.empty else
+  Lazy_Sequence.append (Lazy_Sequence.single i) (small_lazy' d (i + 1)))"
+by pat_completeness auto
+
+termination 
+  by (relation "measure (%(d, i). nat (d + 1 - i))") auto
+
+definition "small_lazy d = small_lazy' d (- d)"
+
+instance ..
+
+end
+
+instantiation prod :: (small_lazy, small_lazy) small_lazy
+begin
+
+definition
+  "small_lazy d = product (small_lazy d) (small_lazy d)"
+
+instance ..
+
+end
+
+instantiation list :: (small_lazy) small_lazy
+begin
+
+fun small_lazy_list :: "int => 'a list Lazy_Sequence.lazy_sequence"
+where
+  "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)"
+
+instance ..
+
+end
+
 subsection {* With Hit Bound Value *}
 text {* assuming in negative context *}
 
@@ -149,7 +214,6 @@
 where
   [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
 
-
 definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
 where
   [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
@@ -194,7 +258,10 @@
   "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
 
 hide_type (open) lazy_sequence
-hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
-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
+hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq
+  iterate_upto not_seq product
+  
+hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def
+  iterate_upto.simps product_def if_seq_def not_seq_def
 
 end

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:08 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:09 2010 +0200
@@ -90,6 +90,7 @@
   (* 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
   val negative_compilation_of : compilation -> compilation
   val compilation_for_polarity : bool -> compilation -> compilation
   val is_depth_limited_compilation : compilation -> bool 
@@ -635,12 +636,15 @@
 (* 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_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq |
+    Pos_Generator_DSeq | Neg_Generator_DSeq
 
 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 c = c
   
 fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
@@ -648,7 +652,8 @@
   | compilation_for_polarity _ c = c
 
 fun is_depth_limited_compilation c =
-  (c = New_Pos_Random_DSeq) orelse (c = New_Neg_Random_DSeq)
+  (c = New_Pos_Random_DSeq) orelse (c = New_Neg_Random_DSeq) orelse
+  (c = Pos_Generator_DSeq) orelse (c = Pos_Generator_DSeq)
 
 fun string_of_compilation c =
   case c of
@@ -662,6 +667,8 @@
   | Neg_Random_DSeq => "neg_random_dseq"
   | New_Pos_Random_DSeq => "new_pos_random dseq"
   | New_Neg_Random_DSeq => "new_neg_random_dseq"
+  | Pos_Generator_DSeq => "pos_generator_dseq"
+  | Neg_Generator_DSeq => "neg_generator_dseq"
 
 val compilation_names = [("pred", Pred),
   ("random", Random),
@@ -669,7 +676,8 @@
   ("depth_limited_random", Depth_Limited_Random),
   (*("annotated", Annotated),*)
   ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq),
-  ("new_random_dseq", New_Pos_Random_DSeq)]
+  ("new_random_dseq", New_Pos_Random_DSeq),
+  ("generator_dseq", Pos_Generator_DSeq)]
 
 val non_random_compilations = [Pred, Depth_Limited, DSeq, Annotated]
 

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Oct 21 19:13:08 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Oct 21 19:13:09 2010 +0200
@@ -157,6 +157,170 @@
 
 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
+
+fun mk_pos_dseqT T =
+    @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
+
+fun dest_pos_dseqT (Type ("fun", [@{typ code_numeral},
+    Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
+  | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], []);
+
+fun mk_bot T = Const (@{const_name New_DSequence.pos_empty}, mk_pos_dseqT T);
+
+fun mk_single t =
+  let
+    val T = fastype_of t
+  in Const(@{const_name New_DSequence.pos_single}, T --> mk_pos_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+  let
+    val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name New_DSequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+  
+fun mk_decr_bind (x, f) =
+  let
+    val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name New_DSequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_sup = HOLogic.mk_binop @{const_name New_DSequence.pos_union};
+
+fun mk_if cond = Const (@{const_name New_DSequence.pos_if_seq},
+  HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
+
+fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+
+fun mk_not t =
+  let
+    val pT = mk_pos_dseqT HOLogic.unitT
+    val nT =
+      @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
+        [Type (@{type_name Option.option}, [@{typ unit}])])
+  in Const (@{const_name New_DSequence.pos_not_seq}, nT --> pT) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name New_DSequence.pos_map},
+  (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
+
+val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
+    {mk_predT = mk_pos_dseqT, dest_predT = dest_pos_dseqT,
+    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
+    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
+
+val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
+    {mk_predT = mk_pos_dseqT, dest_predT = dest_pos_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_Neg_DSequence_CompFuns =
+struct
+
+fun mk_neg_dseqT T = @{typ code_numeral} -->
+  Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
+
+fun dest_neg_dseqT (Type ("fun", [@{typ code_numeral},
+    Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = T
+  | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], []);
+
+fun mk_bot T = Const (@{const_name New_DSequence.neg_empty}, mk_neg_dseqT T);
+
+fun mk_single t =
+  let
+    val T = fastype_of t
+  in Const(@{const_name New_DSequence.neg_single}, T --> mk_neg_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+  let
+    val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name New_DSequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+  
+fun mk_decr_bind (x, f) =
+  let
+    val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name New_DSequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_sup = HOLogic.mk_binop @{const_name New_DSequence.neg_union};
+
+fun mk_if cond = Const (@{const_name New_DSequence.neg_if_seq},
+  HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
+
+fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+
+fun mk_not t =
+  let
+    val nT = mk_neg_dseqT HOLogic.unitT
+    val pT =
+      @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
+        [@{typ unit}])
+  in Const (@{const_name New_DSequence.neg_not_seq}, pT --> nT) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name New_DSequence.neg_map},
+  (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
+
+val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
+    {mk_predT = mk_neg_dseqT, dest_predT = dest_neg_dseqT,
+    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
+    mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
+
+val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
+    {mk_predT = mk_neg_dseqT, dest_predT = dest_neg_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_Random_Sequence_CompFuns =
 struct
 
@@ -182,7 +346,7 @@
   in
     Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
   end;
-  
+
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
@@ -222,7 +386,6 @@
     {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_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_Neg_Random_Sequence_CompFuns =

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:08 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:09 2010 +0200
@@ -278,7 +278,7 @@
 fun function_names_of compilation ctxt name =
   case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
     NONE => error ("No " ^ string_of_compilation compilation
-      ^ "functions defined for predicate " ^ quote name)
+      ^ " functions defined for predicate " ^ quote name)
   | SOME fun_names => fun_names
 
 fun function_name_of compilation ctxt name mode =
@@ -848,16 +848,27 @@
 
 end;
 
-fun unlimited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq =
+fun unlimited_compfuns_of true New_Pos_Random_DSeq =
     New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
-  | unlimited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq =
+  | unlimited_compfuns_of false New_Pos_Random_DSeq =
     New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns
-  
+  | unlimited_compfuns_of true Pos_Generator_DSeq =
+    New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
+  | unlimited_compfuns_of false Pos_Generator_DSeq =
+    New_Neg_DSequence_CompFuns.depth_unlimited_compfuns
+  | unlimited_compfuns_of _ c =
+    raise Fail ("No unlimited compfuns for compilation " ^ string_of_compilation c)
+
 fun limited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq =
     New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
   | limited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq =
     New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
-
+  | limited_compfuns_of true Pos_Generator_DSeq =
+    New_Pos_DSequence_CompFuns.depth_limited_compfuns
+  | limited_compfuns_of false Pos_Generator_DSeq =
+    New_Neg_DSequence_CompFuns.depth_limited_compfuns
+  | limited_compfuns_of _ c =
+    raise Fail ("No limited compfuns for compilation " ^ string_of_compilation c)
 
 val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
   {
@@ -997,7 +1008,7 @@
   compilation = DSeq,
   function_name_prefix = "dseq_",
   compfuns = DSequence_CompFuns.compfuns,
-  mk_random = (fn _ => error "no random generation"),
+  mk_random = (fn _ => error "no random generation in dseq"),
   modify_funT = I,
   additional_arguments = K [],
   wrap_compilation = K (K (K (K (K I))))
@@ -1077,12 +1088,49 @@
   transform_additional_arguments = K I : (indprem -> term list -> term list)
   }
 
+val pos_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = Pos_Generator_DSeq,
+  function_name_prefix = "generator_dseq_",
+  compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns,
+  mk_random =
+    (fn T => fn additional_arguments =>
+      let
+        val small_lazy =
+         Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
+         @{typ "Int.int"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T])) 
+      in
+        absdummy (@{typ code_numeral}, small_lazy $ HOLogic.mk_number @{typ int} 3)
+      end
+    ),
+  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_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = Neg_Generator_DSeq,
+  function_name_prefix = "generator_dseq_neg_",
+  compfuns = New_Neg_DSequence_CompFuns.depth_limited_compfuns,
+  mk_random = (fn _ => error "no random generation"),
+  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
     | Neg_Random_DSeq => pos_random_dseq_comp_modifiers
     | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers
-    | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers
+    | 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
     | c => comp_modifiers)
 
 (** mode analysis **)
@@ -3099,6 +3147,25 @@
   use_generators = true,
   qname = "new_random_dseq_equation"})
 
+val add_generator_dseq_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_dseq_comp_modifiers New_Pos_DSequence_CompFuns.depth_limited_compfuns
+        options preds (s, pos_modes)
+      #> define_functions neg_generator_dseq_comp_modifiers New_Neg_DSequence_CompFuns.depth_limited_compfuns
+        options preds (s, neg_modes)
+    end,
+  prove = prove_by_skip,
+  add_code_equations = K (K I),
+  comp_modifiers = pos_generator_dseq_comp_modifiers,
+  use_generators = true,
+  qname = "generator_dseq_equation"})
+
 (** user interface **)
 
 (* code_pred_intro attribute *)
@@ -3160,6 +3227,7 @@
            | Random => add_random_equations
            | Depth_Limited_Random => add_depth_limited_random_equations
            | New_Pos_Random_DSeq => add_new_random_dseq_equations
+           | Pos_Generator_DSeq => add_generator_dseq_equations
            | compilation => error ("Compilation not supported")
            ) options [const]))
       end