# HG changeset patch
# User bulwahn
# Date 1256630636 -3600
# Node ID b350516cb1f96473f607309b4afbdcfed0d5ce03
# Parent  75b01355e5d4142a8ca4234e9e479c44911eddff
adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex

diff -r 75b01355e5d4 -r b350516cb1f9 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Oct 27 09:03:56 2009 +0100
+++ b/src/HOL/IsaMakefile	Tue Oct 27 09:03:56 2009 +0100
@@ -953,7 +953,7 @@
   ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy	\
   ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
   ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy		\
-  ex/Predicate_Compile_ex.thy			\
+  ex/Predicate_Compile_ex.thy ex/Predicate_Compile_Quickcheck.thy			\
   ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
   ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
   ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
diff -r 75b01355e5d4 -r b350516cb1f9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 27 09:03:56 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 27 09:03:56 2009 +0100
@@ -53,10 +53,9 @@
   };
   val pred_compfuns : compilation_funs
   val randompred_compfuns : compilation_funs
-    (*  val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
+  val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
-  *)
 end;
 
 structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
diff -r 75b01355e5d4 -r b350516cb1f9 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Oct 27 09:03:56 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Oct 27 09:03:56 2009 +0100
@@ -20,10 +20,9 @@
 
 fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
 val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns)
-val mk_rpredT = #mk_predT (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
-val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
-val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
-val lift_pred = #lift_pred (dest_compfuns Predicate_Compile_Core.rpred_compfuns)
+val mk_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
+val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
+val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
 
 fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
   | mk_split_lambda [x] t = lambda x t
@@ -65,22 +64,22 @@
     val thy'' = thy'
       |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
       |> 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_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] *)
+      |> 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 bool}, @{typ code_numeral}] ---> (mk_rpredT (HOLogic.mk_tupleT (map snd vs')))
+          val T = [@{typ bool}, @{typ code_numeral}] ---> (mk_randompredT (HOLogic.mk_tupleT (map snd vs')))
           in Const (name, T) $ @{term True} $ Bound 0 end
-      else if member (op =) depth_limited_modes ([], []) then
+      (*else if member (op =) depth_limited_modes ([], []) then
         let
           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
+        in lift_pred (Const (name, T) $ Bound 0) end*)
       else error "Predicate Compile Quickcheck failed"
     val qc_term = Abs ("size", @{typ code_numeral}, mk_bind (prog,
       mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}