adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog

--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Oct 21 19:13:10 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Oct 21 19:13:11 2010 +0200
@@ -96,8 +96,8 @@
   val ioi = Fun (Input, Fun (Output, Fun (Input, Bool)))
   val oii = Fun (Output, Fun (Input, Fun (Input, Bool)))
   val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
-  val plus_nat = Predicate_Compile_Core.functional_compilation @{const_name plus} iio
-  val minus_nat = Predicate_Compile_Core.functional_compilation @{const_name "minus"} iio
+  val plus_nat = Core_Data.functional_compilation @{const_name plus} iio
+  val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
   fun subtract_nat compfuns (_ : typ) =
     let
       val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
@@ -128,21 +128,21 @@
             (single_const $ (@{term "op + :: nat => nat => nat"} $ Bound 1 $ Bound 0))))
     end
 in
-  Predicate_Compile_Core.force_modes_and_compilations @{const_name plus_eq_nat}
+  Core_Data.force_modes_and_compilations @{const_name plus_eq_nat}
     [(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)),
      (ooi, (enumerate_addups_nat, false))]
   #> Predicate_Compile_Fun.add_function_predicate_translation
        (@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"})
-  #> Predicate_Compile_Core.force_modes_and_compilations @{const_name minus_eq_nat}
+  #> Core_Data.force_modes_and_compilations @{const_name minus_eq_nat}
        [(iio, (minus_nat, false)), (oii, (enumerate_nats, false))]
   #> Predicate_Compile_Fun.add_function_predicate_translation
       (@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"})
-  #> Predicate_Compile_Core.force_modes_and_functions @{const_name plus_eq_int}
+  #> Core_Data.force_modes_and_functions @{const_name plus_eq_int}
     [(iio, (@{const_name plus}, false)), (ioi, (@{const_name subtract}, false)),
      (oii, (@{const_name subtract}, false))]
   #> Predicate_Compile_Fun.add_function_predicate_translation
        (@{term "plus :: int => int => int"}, @{term "plus_eq_int"})
-  #> Predicate_Compile_Core.force_modes_and_functions @{const_name minus_eq_int}
+  #> Core_Data.force_modes_and_functions @{const_name minus_eq_int}
     [(iio, (@{const_name minus}, false)), (oii, (@{const_name plus}, false)),
      (ioi, (@{const_name minus}, false))]
   #> Predicate_Compile_Fun.add_function_predicate_translation

--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Thu Oct 21 19:13:10 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Thu Oct 21 19:13:11 2010 +0200
@@ -13,7 +13,7 @@
   "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
 
 code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
-ML {* Predicate_Compile_Core.intros_of @{context} @{const_name specialised_nth_el'P} *}
+ML {* Core_Data.intros_of @{context} @{const_name specialised_nth_el'P} *}
 
 thm greater_than_index.equation
 
@@ -42,7 +42,7 @@
 
 thm max_of_my_SucP.equation
 
-ML {* Predicate_Compile_Core.intros_of @{context} @{const_name specialised_max_natP} *}
+ML {* Core_Data.intros_of @{context} @{const_name specialised_max_natP} *}
 
 values "{x. max_of_my_SucP x 6}"
 

--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Oct 21 19:13:10 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Oct 21 19:13:11 2010 +0200
@@ -386,9 +386,9 @@
            (fn s => member (op =) (the (AList.lookup (op =) random s))))
         val (preds, all_vs, param_vs, all_modes, clauses) =
           Predicate_Compile_Core.prepare_intrs options ctxt prednames
-            (maps (Predicate_Compile_Core.intros_of ctxt) prednames)
+            (maps (Core_Data.intros_of ctxt) prednames)
         val ((moded_clauses, random'), _) =
-          Predicate_Compile_Core.infer_modes mode_analysis_options options 
+          Mode_Inference.infer_modes mode_analysis_options options 
             (lookup_modes, lookup_neg_modes, needs_random) ctxt preds all_modes param_vs clauses
         val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
         val pos_modes' = map (apsnd (map_filter (fn (true, m) => SOME m | _ => NONE))) modes
@@ -474,7 +474,7 @@
   let 
     fun strong_conn_of gr keys =
       Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
-    val gr = Predicate_Compile_Core.intros_graph_of ctxt
+    val gr = Core_Data.intros_graph_of ctxt
     val gr' = add_edges depending_preds_of const gr
     val scc = strong_conn_of gr' [const]
     val initial_constant_table = 
@@ -917,6 +917,7 @@
   no_higher_order_predicate = [],
   inductify = false,
   detect_switches = true,
+  smart_depth_limiting = true,
   compilation = Predicate_Compile_Aux.Pred
 }
 

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:10 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Oct 21 19:13:11 2010 +0200
@@ -676,7 +676,8 @@
   ("depth_limited", Depth_Limited),
   ("depth_limited_random", Depth_Limited_Random),
   (*("annotated", Annotated),*)
-  ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq),
+  ("dseq", DSeq),
+  ("random_dseq", Pos_Random_DSeq),
   ("new_random_dseq", New_Pos_Random_DSeq),
   ("generator_dseq", Pos_Generator_DSeq)]
 

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Oct 21 19:13:10 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Oct 21 19:13:11 2010 +0200
@@ -85,6 +85,7 @@
   function_flattening = true,
   fail_safe_function_flattening = false,
   no_higher_order_predicate = [],
+  smart_depth_limiting = true,
   no_topmost_reordering = false
 }
 
@@ -108,6 +109,7 @@
   function_flattening = true,
   fail_safe_function_flattening = false,
   no_higher_order_predicate = [],
+  smart_depth_limiting = true,
   no_topmost_reordering = true
 }
 
@@ -119,14 +121,14 @@
     show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
-    no_topmost_reordering = re}) =
+    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
     show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
     show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = b,
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
-    no_topmost_reordering = re})
+    smart_depth_limiting = sm_dl, no_topmost_reordering = re})
 
 fun set_fail_safe_function_flattening b
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
@@ -135,14 +137,14 @@
     show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
-    no_topmost_reordering = re}) =
+    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
     show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
     show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
     fail_safe_function_flattening = b, no_higher_order_predicate = no_ho,
-    no_topmost_reordering = re})
+    smart_depth_limiting = sm_dl, no_topmost_reordering = re})
 
 fun set_no_higher_order_predicate ss
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
@@ -151,13 +153,14 @@
     show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
-    no_topmost_reordering = re}) =
+    smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
     show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
     show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
-    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss, no_topmost_reordering = re})
+    fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss,
+    smart_depth_limiting = sm_dl, no_topmost_reordering = re})
 
 
 fun get_options () = 
@@ -173,9 +176,12 @@
 val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns
 val mk_bind = Predicate_Compile_Aux.mk_bind RandomPredCompFuns.compfuns
 
-val mk_new_randompredT = Predicate_Compile_Aux.mk_predT New_Pos_Random_Sequence_CompFuns.compfuns
-val mk_new_return = Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.compfuns
-val mk_new_bind = Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.compfuns
+val mk_new_randompredT =
+  Predicate_Compile_Aux.mk_predT New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
+val mk_new_return =
+  Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
+val mk_new_bind =
+  Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
 
 val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple
 
@@ -207,13 +213,12 @@
     val _ = Output.tracing ("Preprocessing time: " ^ string_of_int (snd preproc_time))
     val _ = Output.tracing ("Core compilation time: " ^ string_of_int (snd core_comp_time))
     val ctxt4 = ProofContext.init_global thy4
-    val modes = Predicate_Compile_Core.modes_of compilation ctxt4 full_constname
+    val modes = Core_Data.modes_of compilation ctxt4 full_constname
     val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
     val prog =
       if member eq_mode modes output_mode then
         let
-          val name = Predicate_Compile_Core.function_name_of compilation ctxt4
-            full_constname output_mode
+          val name = Core_Data.function_name_of compilation ctxt4 full_constname output_mode
           val T = 
             case compilation of
               Pos_Random_DSeq => mk_randompredT (HOLogic.mk_tupleT (map snd vs'))