# HG changeset patch
# User bulwahn
# Date 1269243013 -3600
# Node ID aa412e08bfee25a5992d105e1a4847f4ff0cd811
# Parent  2623b23e41fc342e362f423b5e35d99dad6086c6
adding depth_limited_random compilation to predicate compiler

diff -r 2623b23e41fc -r aa412e08bfee src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 22 08:30:13 2010 +0100
@@ -478,7 +478,7 @@
 
 (* Different options for compiler *)
 
-datatype compilation = Pred | Random | Depth_Limited | DSeq | Annotated
+datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
   | Pos_Random_DSeq | Neg_Random_DSeq
 
 
@@ -493,6 +493,7 @@
     Pred => ""
   | Random => "random"
   | Depth_Limited => "depth limited"
+  | Depth_Limited_Random => "depth limited random"
   | DSeq => "dseq"
   | Annotated => "annotated"
   | Pos_Random_DSeq => "pos_random dseq"
@@ -571,7 +572,9 @@
 
 val compilation_names = [("pred", Pred),
   ("random", Random),
-  ("depth_limited", Depth_Limited), (*("annotated", Annotated),*)
+  ("depth_limited", Depth_Limited),
+  ("depth_limited_random", Depth_Limited_Random),
+  (*("annotated", Annotated),*)
   ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)]
 
 fun print_step options s =
diff -r 2623b23e41fc -r aa412e08bfee src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
@@ -2586,6 +2586,50 @@
   transform_additional_arguments = K I : (indprem -> term list -> term list)
   }
 
+val depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = Depth_Limited_Random,
+  function_name_prefix = "depth_limited_random_",
+  compfuns = PredicateCompFuns.compfuns,
+  mk_random = (fn T => fn additional_arguments =>
+  list_comb (Const(@{const_name Quickcheck.iter},
+  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
+    PredicateCompFuns.mk_predT T), tl additional_arguments)),
+  modify_funT = (fn T =>
+    let
+      val (Ts, U) = strip_type T
+      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
+        @{typ "code_numeral * code_numeral"}]
+    in (Ts @ Ts') ---> U end),
+  additional_arguments = (fn names =>
+    let
+      val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
+    in
+      [Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}),
+        Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
+    end),
+  wrap_compilation =
+  fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
+    let
+      val depth = hd (additional_arguments)
+      val (_, Ts) = split_modeT' mode (binder_types T)
+      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
+      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
+    in
+      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
+        $ mk_bot compfuns (dest_predT compfuns T')
+        $ compilation
+    end,
+  transform_additional_arguments =
+    fn prem => fn additional_arguments =>
+    let
+      val [depth, nrandom, size, seed] = additional_arguments
+      val depth' =
+        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
+          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
+    in [depth', nrandom, size, seed] end
+}
+
 (* different instantiantions of the predicate compiler *)
 
 val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
@@ -2713,6 +2757,18 @@
   use_random = true,
   qname = "random_equation"})
 
+val add_depth_limited_random_equations = gen_add_equations
+  (Steps {
+  define_functions =
+    fn options => fn preds => fn (s, modes) =>
+      define_functions depth_limited_random_comp_modifiers PredicateCompFuns.compfuns options preds
+      (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
+  comp_modifiers = depth_limited_random_comp_modifiers,
+  prove = prove_by_skip,
+  add_code_equations = K (K I),
+  use_random = true,
+  qname = "depth_limited_random_equation"})
+
 val add_dseq_equations = gen_add_equations
   (Steps {
   define_functions =
@@ -2798,6 +2854,7 @@
            | Pos_Random_DSeq => add_random_dseq_equations
            | Depth_Limited => add_depth_limited_equations
            | Random => add_random_equations
+           | Depth_Limited_Random => add_depth_limited_random_equations
            | compilation => error ("Compilation not supported")
            ) options [const]))
       end
@@ -2881,6 +2938,8 @@
             [@{term "(1, 1) :: code_numeral * code_numeral"}]
           | Annotated => []
           | Depth_Limited => [HOLogic.mk_number @{typ "code_numeral"} (hd arguments)]
+          | Depth_Limited_Random => map (HOLogic.mk_number @{typ "code_numeral"}) arguments @
+            [@{term "(1, 1) :: code_numeral * code_numeral"}]
           | DSeq => []
           | Pos_Random_DSeq => []
         val comp_modifiers =
@@ -2888,6 +2947,7 @@
             Pred => predicate_comp_modifiers
           | Random => random_comp_modifiers
           | Depth_Limited => depth_limited_comp_modifiers
+          | Depth_Limited_Random => depth_limited_random_comp_modifiers
           (*| Annotated => annotated_comp_modifiers*)
           | DSeq => dseq_comp_modifiers
           | Pos_Random_DSeq => pos_random_dseq_comp_modifiers