# HG changeset patch # User bulwahn # Date 1256892915 -3600 # Node ID fd3e861f8d3135c4cd4e6bca2b428bca3023ada4 # Parent 37ec56ac3fd43b578fea01d413f7b6712bbc48aa renamed rpred to random diff -r 37ec56ac3fd4 -r fd3e861f8d31 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Oct 30 01:32:06 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Oct 30 09:55:15 2009 +0100 @@ -122,7 +122,7 @@ show_compilation = chk "show_compilation", skip_proof = chk "skip_proof", inductify = chk "inductify", - rpred = chk "rpred", + random = chk "random", depth_limited = chk "depth_limited" } end @@ -151,7 +151,7 @@ val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes", - "show_mode_inference", "show_compilation", "skip_proof", "inductify", "rpred", "depth_limited"] + "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited"] local structure P = OuterParse in diff -r 37ec56ac3fd4 -r fd3e861f8d31 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Oct 30 01:32:06 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Oct 30 09:55:15 2009 +0100 @@ -169,7 +169,7 @@ skip_proof : bool, inductify : bool, - rpred : bool, + random : bool, depth_limited : bool }; @@ -183,7 +183,7 @@ fun skip_proof (Options opt) = #skip_proof opt fun is_inductify (Options opt) = #inductify opt -fun is_rpred (Options opt) = #rpred opt +fun is_random (Options opt) = #random opt fun is_depth_limited (Options opt) = #depth_limited opt val default_options = Options { @@ -197,7 +197,7 @@ skip_proof = false, inductify = false, - rpred = false, + random = false, depth_limited = false } diff -r 37ec56ac3fd4 -r fd3e861f8d31 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Oct 30 01:32:06 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Oct 30 09:55:15 2009 +0100 @@ -254,7 +254,7 @@ val depth_limited_modes_of = (map fst) o #depth_limited_functions oo the_pred_data -val rpred_modes_of = (map fst) o #generators oo the_pred_data +val random_modes_of = (map fst) o #generators oo the_pred_data fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy) @@ -302,8 +302,6 @@ val depth_limited_function_name_of = #name ooo the_depth_limited_function_data -(*val generator_modes_of = (map fst) o #generators oo the_pred_data*) - (* diagnostic display functions *) fun print_modes options modes = @@ -1586,7 +1584,7 @@ (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs)) end -fun rpred_create_definitions preds (name, modes) thy = +fun random_create_definitions preds (name, modes) thy = let val T = AList.lookup (op =) preds name |> the fun create_definition mode thy = @@ -2260,7 +2258,7 @@ in [polarity', depth'] end } -val rpred_comp_modifiers = Comp_Mod.Comp_Modifiers +val random_comp_modifiers = Comp_Mod.Comp_Modifiers {const_name_of = generator_name_of, funT_of = K generator_funT_of : (compilation_funs -> mode -> typ -> typ), additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})], @@ -2287,11 +2285,11 @@ val add_quickcheck_equations = gen_add_equations (Steps {infer_modes = infer_modes_with_generator, - create_definitions = rpred_create_definitions, - compile_preds = compile_preds rpred_comp_modifiers RandomPredCompFuns.compfuns, + create_definitions = random_create_definitions, + compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns, prove = prove_by_skip, - are_not_defined = fn thy => forall (null o rpred_modes_of thy), - qname = "rpred_equation"}) + are_not_defined = fn thy => forall (null o random_modes_of thy), + qname = "random_equation"}) (** user interface **) @@ -2345,7 +2343,7 @@ (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms) in goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #> - (if is_rpred options then + (if is_random options then (add_equations options [const] #> add_quickcheck_equations options [const]) else if is_depth_limited options then @@ -2395,7 +2393,7 @@ | SOME d => [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} d] val comp_modifiers = case depth_limit of NONE => - (if random then rpred_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers + (if random then random_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers val mk_fun_of = if random then mk_generator_of else if (is_some depth_limit) then mk_depth_limited_fun_of else mk_fun_of val t_pred = compile_expr comp_modifiers compfuns thy diff -r 37ec56ac3fd4 -r fd3e861f8d31 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Oct 30 01:32:06 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Oct 30 09:55:15 2009 +0100 @@ -144,8 +144,6 @@ val abs_args = filter is_Abs args fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) = let - val _ = tracing ("Introduce new constant for " ^ - Syntax.string_of_term_global thy abs_arg) val vars = map Var (Term.add_vars abs_arg []) val abs_arg' = Logic.unvarify abs_arg val frees = map Free (Term.add_frees abs_arg' []) @@ -156,7 +154,6 @@ val const = Const (full_constname, constT) val lhs = list_comb (const, frees) val def = Logic.mk_equals (lhs, abs_arg') - val _ = tracing (Syntax.string_of_term_global thy def) val ([definition], thy') = thy |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])] diff -r 37ec56ac3fd4 -r fd3e861f8d31 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Oct 30 01:32:06 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Oct 30 09:55:15 2009 +0100 @@ -32,7 +32,7 @@ skip_proof = false, inductify = false, - rpred = false, + random = false, depth_limited = false } diff -r 37ec56ac3fd4 -r fd3e861f8d31 src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy --- a/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Fri Oct 30 01:32:06 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Fri Oct 30 09:55:15 2009 +0100 @@ -32,10 +32,10 @@ | "w \ S\<^isub>2 \ b # w \ B\<^isub>2" | "\v \ B\<^isub>2; v \ B\<^isub>2\ \ a # v @ w \ B\<^isub>2" -code_pred [inductify, rpred] S\<^isub>2 . -thm S\<^isub>2.rpred_equation -thm A\<^isub>2.rpred_equation -thm B\<^isub>2.rpred_equation +code_pred [inductify, random] S\<^isub>2 . +thm S\<^isub>2.random_equation +thm A\<^isub>2.random_equation +thm B\<^isub>2.random_equation values [random] 10 "{x. S\<^isub>2 x}" diff -r 37ec56ac3fd4 -r fd3e861f8d31 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Fri Oct 30 01:32:06 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Fri Oct 30 09:55:15 2009 +0100 @@ -1,5 +1,5 @@ theory Predicate_Compile_ex -imports "../Main" Predicate_Compile_Alternative_Defs +imports Main Predicate_Compile_Alternative_Defs begin subsection {* Basic predicates *} @@ -8,7 +8,7 @@ code_pred (mode : []) False' . code_pred [depth_limited] False' . -code_pred [rpred] False' . +code_pred [random] False' . inductive EmptySet :: "'a \ bool" @@ -67,7 +67,7 @@ "zerozero (0, 0)" code_pred (mode: [i], [(i, o)], [(o, i)], [o]) zerozero . -code_pred [rpred] zerozero . +code_pred [random] zerozero . subsection {* Alternative Rules *} @@ -188,14 +188,14 @@ code_pred (mode: [], [1]) even . code_pred [depth_limited] even . -code_pred [rpred] even . +code_pred [random] even . thm odd.equation thm even.equation thm odd.depth_limited_equation thm even.depth_limited_equation -thm even.rpred_equation -thm odd.rpred_equation +thm even.random_equation +thm odd.random_equation values "{x. even 2}" values "{x. odd 2}" @@ -211,7 +211,7 @@ code_pred (mode: [1]) [inductify] odd' . code_pred [inductify, depth_limited] odd' . -code_pred [inductify, rpred] odd' . +code_pred [inductify, random] odd' . thm odd'.depth_limited_equation values [depth_limit = 2] "{x. odd' 7}" @@ -231,11 +231,11 @@ code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append . code_pred [depth_limited] append . -code_pred [rpred] append . +code_pred [random] append . thm append.equation thm append.depth_limited_equation -thm append.rpred_equation +thm append.random_equation values "{(ys, xs). append xs ys [0, Suc 0, 2]}" values "{zs. append [0, Suc 0, 2] [17, 8] zs}" @@ -279,7 +279,7 @@ | "tupled_append (xs, ys, zs) \ tupled_append (x # xs, ys, x # zs)" code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append . -code_pred [rpred] tupled_append . +code_pred [random] tupled_append . thm tupled_append.equation (* TODO: values with tupled modes @@ -332,7 +332,7 @@ code_pred (mode: [1] ==> [1], [1] ==> [1, 2]) filter1 . code_pred [depth_limited] filter1 . -code_pred [rpred] filter1 . +code_pred [random] filter1 . thm filter1.equation @@ -344,9 +344,9 @@ code_pred (mode: [1, 2, 3], [1, 2]) filter2 . code_pred [depth_limited] filter2 . -code_pred [rpred] filter2 . +code_pred [random] filter2 . thm filter2.equation -thm filter2.rpred_equation +thm filter2.random_equation inductive filter3 for P @@ -363,7 +363,7 @@ code_pred (mode: [1, 2], [1, 2, 3]) filter4 . code_pred [depth_limited] filter4 . -code_pred [rpred] filter4 . +code_pred [random] filter4 . subsection {* reverse predicate *} @@ -394,7 +394,7 @@ code_pred (mode: [1] ==> [1], [1] ==> [2, 3], [1] ==> [1, 2], [1] ==> [1, 3], [1] ==> [1, 2, 3]) partition . code_pred [depth_limited] partition . -code_pred [rpred] partition . +code_pred [random] partition . values 10 "{(ys, zs). partition is_even [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" @@ -425,18 +425,18 @@ qed code_pred [depth_limited] tranclp . -code_pred [rpred] tranclp . +code_pred [random] tranclp . thm tranclp.equation -thm tranclp.rpred_equation +thm tranclp.random_equation inductive succ :: "nat \ nat \ bool" where "succ 0 1" | "succ m n \ succ (Suc m) (Suc n)" code_pred succ . -code_pred [rpred] succ . +code_pred [random] succ . thm succ.equation -thm succ.rpred_equation +thm succ.random_equation values 10 "{(m, n). succ n m}" values "{m. succ 0 m}" @@ -549,9 +549,9 @@ subsection {* Lexicographic order *} code_pred [inductify] lexord . -code_pred [inductify, rpred] lexord . +code_pred [inductify, random] lexord . thm lexord.equation -thm lexord.rpred_equation +thm lexord.random_equation inductive less_than_nat :: "nat * nat => bool" where @@ -561,16 +561,16 @@ code_pred less_than_nat . code_pred [depth_limited] less_than_nat . -code_pred [rpred] less_than_nat . +code_pred [random] less_than_nat . inductive test_lexord :: "nat list * nat list => bool" where "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)" -code_pred [rpred] test_lexord . +code_pred [random] test_lexord . code_pred [depth_limited] test_lexord . thm test_lexord.depth_limited_equation -thm test_lexord.rpred_equation +thm test_lexord.random_equation values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}" values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}" @@ -580,15 +580,15 @@ code_pred [inductify] lexn . thm lexn.equation -code_pred [rpred] lexn . +code_pred [random] lexn . -thm lexn.rpred_equation +thm lexn.random_equation -code_pred [inductify, show_steps] lenlex . +code_pred [inductify] lenlex . thm lenlex.equation -code_pred [inductify, rpred] lenlex . -thm lenlex.rpred_equation +code_pred [inductify, random] lenlex . +thm lenlex.random_equation code_pred [inductify] lists . thm lists.equation @@ -609,8 +609,8 @@ code_pred [inductify] avl . thm avl.equation -code_pred [rpred] avl . -thm avl.rpred_equation +code_pred [random] avl . +thm avl.random_equation fun set_of where @@ -667,9 +667,9 @@ subsection {* Inverting list functions *} code_pred [inductify] length . -code_pred [inductify, rpred] length . +code_pred [inductify, random] length . thm size_listP.equation -thm size_listP.rpred_equation +thm size_listP.random_equation values [random] 20 "{xs. size_listP (xs::nat list) (5::nat)}" @@ -693,7 +693,7 @@ code_pred [inductify] foldr . code_pred [inductify] foldl . code_pred [inductify] filter . -code_pred [inductify, rpred] filter . +code_pred [inductify, random] filter . subsection {* Context Free Grammar *} @@ -708,9 +708,9 @@ | "\v \ B\<^isub>1; v \ B\<^isub>1\ \ a # v @ w \ B\<^isub>1" code_pred [inductify] S\<^isub>1p . -code_pred [inductify, rpred] S\<^isub>1p . +code_pred [inductify, random] S\<^isub>1p . thm S\<^isub>1p.equation -thm S\<^isub>1p.rpred_equation +thm S\<^isub>1p.random_equation values [random] 5 "{x. S\<^isub>1p x}" @@ -722,10 +722,10 @@ | "w \ S\<^isub>2 \ b # w \ B\<^isub>2" | "\v \ B\<^isub>2; v \ B\<^isub>2\ \ a # v @ w \ B\<^isub>2" -code_pred [inductify, rpred] S\<^isub>2 . -thm S\<^isub>2.rpred_equation -thm A\<^isub>2.rpred_equation -thm B\<^isub>2.rpred_equation +code_pred [inductify, random] S\<^isub>2 . +thm S\<^isub>2.random_equation +thm A\<^isub>2.random_equation +thm B\<^isub>2.random_equation values [random] 10 "{x. S\<^isub>2 x}"