adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible

--- a/src/HOL/New_DSequence.thy	Thu Oct 21 19:13:06 2010 +0200
+++ b/src/HOL/New_DSequence.thy	Thu Oct 21 19:13:07 2010 +0200
@@ -21,7 +21,11 @@
 
 definition pos_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq"
 where
-  "pos_bind x f = (%i. 
+  "pos_bind x f = (%i. Lazy_Sequence.bind (x i) (%a. f a i))"
+
+definition pos_decr_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq"
+where
+  "pos_decr_bind x f = (%i. 
      if i = 0 then
        Lazy_Sequence.empty
      else
@@ -57,7 +61,11 @@
 
 definition neg_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq"
 where
-  "neg_bind x f = (%i. 
+  "neg_bind x f = (%i. hb_bind (x i) (%a. f a i))"
+
+definition neg_decr_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq"
+where
+  "neg_decr_bind x f = (%i. 
      if i = 0 then
        Lazy_Sequence.hit_bound
      else
@@ -94,8 +102,8 @@
 hide_type (open) pos_dseq neg_dseq
 
 hide_const (open)
-  pos_empty pos_single pos_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
-  neg_empty neg_single neg_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
+  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
+  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
 hide_fact (open)
   pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def
   neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def

--- a/src/HOL/New_Random_Sequence.thy	Thu Oct 21 19:13:06 2010 +0200
+++ b/src/HOL/New_Random_Sequence.thy	Thu Oct 21 19:13:07 2010 +0200
@@ -20,6 +20,10 @@
 where
   "pos_bind R f = (\<lambda>nrandom size seed. New_DSequence.pos_bind (R nrandom size seed) (%a. f a nrandom size seed))"
 
+definition pos_decr_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
+where
+  "pos_decr_bind R f = (\<lambda>nrandom size seed. New_DSequence.pos_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))"
+
 definition pos_union :: "'a pos_random_dseq => 'a pos_random_dseq => 'a pos_random_dseq"
 where
   "pos_union R1 R2 = (\<lambda>nrandom size seed. New_DSequence.pos_union (R1 nrandom size seed) (R2 nrandom size seed))"
@@ -62,6 +66,10 @@
 where
   "neg_bind R f = (\<lambda>nrandom size seed. New_DSequence.neg_bind (R nrandom size seed) (%a. f a nrandom size seed))"
 
+definition neg_decr_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
+where
+  "neg_decr_bind R f = (\<lambda>nrandom size seed. New_DSequence.neg_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))"
+
 definition neg_union :: "'a neg_random_dseq => 'a neg_random_dseq => 'a neg_random_dseq"
 where
   "neg_union R1 R2 = (\<lambda>nrandom size seed. New_DSequence.neg_union (R1 nrandom size seed) (R2 nrandom size seed))"
@@ -97,8 +105,8 @@
 *)
 
 hide_const (open)
-  pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
-  neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
+  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
+  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
 hide_type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
 (* FIXME: hide facts *)
 (*hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:06 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:07 2010 +0200
@@ -92,6 +92,7 @@
     | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
   val negative_compilation_of : compilation -> compilation
   val compilation_for_polarity : bool -> compilation -> compilation
+  val is_depth_limited_compilation : compilation -> bool 
   val string_of_compilation : compilation -> string
   val compilation_names : (string * compilation) list
   val non_random_compilations : compilation list
@@ -646,6 +647,9 @@
   | compilation_for_polarity false New_Pos_Random_DSeq = New_Neg_Random_DSeq
   | compilation_for_polarity _ c = c
 
+fun is_depth_limited_compilation c =
+  (c = New_Pos_Random_DSeq) orelse (c = New_Neg_Random_DSeq)
+
 fun string_of_compilation c =
   case c of
     Pred => ""

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Oct 21 19:13:06 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Oct 21 19:13:07 2010 +0200
@@ -182,6 +182,13 @@
   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
+  in
+    Const (@{const_name New_Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
 
 val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
 
@@ -206,7 +213,12 @@
 fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.pos_map},
   (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
 
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
+    {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_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_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}
@@ -241,6 +253,13 @@
     Const (@{const_name New_Random_Sequence.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_Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
 val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
 
 fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
@@ -262,7 +281,12 @@
 fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.neg_map},
   (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
 
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
+    {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_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_random_dseqT, dest_predT = dest_neg_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}

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:06 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 21 19:13:07 2010 +0200
@@ -839,8 +839,26 @@
 val wrap_compilation = #wrap_compilation o dest_comp_modifiers
 val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers
 
+fun set_compfuns compfuns' (Comp_Modifiers {compilation, function_name_prefix, compfuns, mk_random,
+    modify_funT, additional_arguments, wrap_compilation, transform_additional_arguments}) =
+    (Comp_Modifiers {compilation = compilation, function_name_prefix = function_name_prefix,
+    compfuns = compfuns', mk_random = mk_random, modify_funT = modify_funT,
+    additional_arguments = additional_arguments, wrap_compilation = wrap_compilation,
+    transform_additional_arguments = transform_additional_arguments})
+
 end;
 
+fun unlimited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq =
+    New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
+  | unlimited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq =
+    New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns
+  
+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
+
+
 val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
   {
   compilation = Depth_Limited,
@@ -1028,7 +1046,7 @@
   {
   compilation = New_Pos_Random_DSeq,
   function_name_prefix = "new_random_dseq_",
-  compfuns = New_Pos_Random_Sequence_CompFuns.compfuns,
+  compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns,
   mk_random = (fn T => fn additional_arguments =>
   let
     val random = Const ("Quickcheck.random_class.random",
@@ -1050,7 +1068,7 @@
   {
   compilation = New_Neg_Random_DSeq,
   function_name_prefix = "new_random_dseq_neg_",
-  compfuns = New_Neg_Random_Sequence_CompFuns.compfuns,
+  compfuns = New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns,
   mk_random = (fn _ => error "no random generation"),
   modify_funT = I,
   additional_arguments = K [],
@@ -1964,8 +1982,16 @@
 
 fun compile_pred options compilation_modifiers ctxt all_vs param_vs s T (pol, mode) moded_cls =
   let
-    val compilation_modifiers = if pol then compilation_modifiers else
-      negative_comp_modifiers_of compilation_modifiers
+    val is_terminating = true (* FIXME: requires an termination analysis *)  
+    val compilation_modifiers =
+      (if pol then compilation_modifiers else
+        negative_comp_modifiers_of compilation_modifiers)
+      |> (if is_depth_limited_compilation (Comp_Mod.compilation compilation_modifiers) then
+           (if is_terminating then
+             (Comp_Mod.set_compfuns (unlimited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers)))
+           else
+             (Comp_Mod.set_compfuns (limited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers))))
+         else I)
     val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
       (all_vs @ param_vs)
     val compfuns = Comp_Mod.compfuns compilation_modifiers
@@ -3062,9 +3088,9 @@
     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 new_pos_random_dseq_comp_modifiers New_Pos_Random_Sequence_CompFuns.compfuns
+    in define_functions new_pos_random_dseq_comp_modifiers New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
       options preds (s, pos_modes)
-      #> define_functions new_neg_random_dseq_comp_modifiers New_Neg_Random_Sequence_CompFuns.compfuns
+      #> define_functions new_neg_random_dseq_comp_modifiers New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
       options preds (s, neg_modes)
     end,
   prove = prove_by_skip,
@@ -3292,7 +3318,7 @@
         Random => PredicateCompFuns.compfuns
       | DSeq => DSequence_CompFuns.compfuns
       | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
-      | New_Pos_Random_DSeq => New_Pos_Random_Sequence_CompFuns.compfuns
+      | New_Pos_Random_DSeq => New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
       | _ => PredicateCompFuns.compfuns
     val t = analyze_compr ctxt compfuns param_user_modes options t_compr;
     val T = dest_predT compfuns (fastype_of t);