src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Fri Oct 23 20:48:14 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sat Oct 24 23:57:42 2009 +0200
@@ -3,18 +3,19 @@
 A quickcheck generator based on the predicate compiler
 *)
 
-signature PRED_COMPILE_QUICKCHECK =
+signature PREDICATE_COMPILE_QUICKCHECK =
 sig
   val quickcheck : Proof.context -> term -> int -> term list option
   val test_ref :
     ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref
 end;
 
-structure Pred_Compile_Quickcheck : PRED_COMPILE_QUICKCHECK =
+structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
 struct
 
 val test_ref =
   Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option)
+
 val target = "Quickcheck"
 
 fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
@@ -63,21 +64,21 @@
     val _ = tracing (Display.string_of_thm ctxt' intro)
     val thy'' = thy'
       |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
-      |> Predicate_Compile.preprocess full_constname
-      |> Predicate_Compile_Core.add_equations [full_constname]
-      |> Predicate_Compile_Core.add_sizelim_equations [full_constname]
-      |> Predicate_Compile_Core.add_quickcheck_equations [full_constname]
-    val sizelim_modes = Predicate_Compile_Core.sizelim_modes_of thy'' full_constname
+      |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname
+      (* |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname]*)
+      (*  |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
+      (* |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname] *)
+    val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname
     val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname  
     val prog =
       if member (op =) modes ([], []) then
         let
           val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], [])
-          val T = @{typ code_numeral} --> (mk_rpredT (HOLogic.mk_tupleT (map snd vs')))
-        in Const (name, T) $ Bound 0 end
-      else if member (op =) sizelim_modes ([], []) then
+          val T = [@{typ bool}, @{typ code_numeral}] ---> (mk_rpredT (HOLogic.mk_tupleT (map snd vs')))
+          in Const (name, T) $ @{term True} $ Bound 0 end
+      else if member (op =) depth_limited_modes ([], []) then
         let
-          val name = Predicate_Compile_Core.sizelim_function_name_of thy'' full_constname ([], [])
+          val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], [])
           val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs')))
         in lift_pred (Const (name, T) $ Bound 0) end
       else error "Predicate Compile Quickcheck failed"
@@ -85,7 +86,7 @@
       mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
       (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
     val _ = tracing (Syntax.string_of_term ctxt' qc_term)
-    val compile = Code_ML.eval (SOME target) ("Pred_Compile_Quickcheck.test_ref", test_ref)
+    val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
       (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc)
       thy'' qc_term []
   in