# 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}