# HG changeset patch # User bulwahn # Date 1269243013 -3600 # Node ID 2623b23e41fc342e362f423b5e35d99dad6086c6 # Parent 99818df5b8f5c7f3c2c19825868628d11fb95d1a a new simpler random compilation for the predicate compiler diff -r 99818df5b8f5 -r 2623b23e41fc src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Quickcheck.thy Mon Mar 22 08:30:13 2010 +0100 @@ -145,6 +145,23 @@ subsection {* The Random-Predicate Monad *} +fun iter' :: + "'a itself => code_numeral => code_numeral => code_numeral * code_numeral => ('a::random) Predicate.pred" +where + "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else + let ((x, _), seed') = random sz seed + in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))" + +definition iter :: "code_numeral => code_numeral => code_numeral * code_numeral => ('a::random) Predicate.pred" +where + "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed" + +lemma [code]: + "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else + let ((x, _), seed') = random sz seed + in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))" +unfolding iter_def iter'.simps[of _ nrandom] .. + types 'a randompred = "Random.seed \ ('a Predicate.pred \ Random.seed)" definition empty :: "'a randompred" @@ -182,9 +199,9 @@ definition map :: "('a \ 'b) \ ('a randompred \ 'b randompred)" where "map f P = bind P (single o f)" -hide (open) fact empty_def single_def bind_def union_def if_randompred_def not_randompred_def Random_def map_def +hide (open) fact iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def not_randompred_def Random_def map_def hide (open) type randompred hide (open) const random collapse beyond random_fun_aux random_fun_lift - empty single bind union if_randompred not_randompred Random map + iter' iter empty single bind union if_randompred not_randompred Random map end diff -r 99818df5b8f5 -r 2623b23e41fc 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 @@ -570,7 +570,7 @@ "no_topmost_reordering"] val compilation_names = [("pred", Pred), - (*("random", Random),*) + ("random", Random), ("depth_limited", Depth_Limited), (*("annotated", Annotated),*) ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)] diff -r 99818df5b8f5 -r 2623b23e41fc 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 @@ -868,19 +868,6 @@ end; - - -fun mk_random T = - let - val random = Const ("Quickcheck.random_class.random", - @{typ code_numeral} --> @{typ Random.seed} --> - HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) - in - Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} --> - HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> - Random_Sequence_CompFuns.mk_random_dseqT T) $ random - end; - (* for external use with interactive mode *) val pred_compfuns = PredicateCompFuns.compfuns val randompred_compfuns = Random_Sequence_CompFuns.compfuns; @@ -1447,6 +1434,7 @@ compilation : compilation, function_name_prefix : string, compfuns : compilation_funs, + mk_random : typ -> term list -> term, modify_funT : typ -> typ, additional_arguments : string list -> term list, wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term, @@ -1459,6 +1447,7 @@ val function_name_prefix = #function_name_prefix o dest_comp_modifiers val compfuns = #compfuns o dest_comp_modifiers +val mk_random = #mk_random o dest_comp_modifiers val funT_of' = funT_of o compfuns val modify_funT = #modify_funT o dest_comp_modifiers fun funT_of comp mode = modify_funT comp o funT_of' comp mode @@ -1612,8 +1601,7 @@ end | Generator (v, T) => let - val u = mk_random T - + val u = Comp_Mod.mk_random compilation_modifiers T additional_arguments val rest = compile_prems [Free (v, T)] vs' names'' ps; in (u, rest) @@ -2543,9 +2531,10 @@ compilation = Depth_Limited, function_name_prefix = "depth_limited_", compfuns = PredicateCompFuns.compfuns, + mk_random = (fn _ => error "no random generation"), additional_arguments = fn names => let - val [depth_name] = Name.variant_list names ["depth"] + val depth_name = Name.variant names "depth" in [Free (depth_name, @{typ code_numeral})] end, modify_funT = (fn T => let val (Ts, U) = strip_type T val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end), @@ -2570,20 +2559,33 @@ $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"}) in [depth'] end } -(* + val random_comp_modifiers = Comp_Mod.Comp_Modifiers { compilation = Random, - function_name_of = function_name_of Random, - set_function_name = set_function_name Random, function_name_prefix = "random_", - funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ), - additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})], + 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), additional_arguments)), + modify_funT = (fn T => + let + val (Ts, U) = strip_type T + val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}] + in (Ts @ Ts') ---> U end), + additional_arguments = (fn names => + let + val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"] + in + [Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}), + Free (seed, @{typ "code_numeral * code_numeral"})] + end), wrap_compilation = K (K (K (K (K I)))) : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), transform_additional_arguments = K I : (indprem -> term list -> term list) } -*) + (* different instantiantions of the predicate compiler *) val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers @@ -2591,7 +2593,8 @@ compilation = Pred, function_name_prefix = "", compfuns = PredicateCompFuns.compfuns, - modify_funT = I, + mk_random = (fn _ => error "no random generation"), + modify_funT = I, additional_arguments = K [], wrap_compilation = K (K (K (K (K I)))) : (compilation_funs -> string -> typ -> mode -> term list -> term -> term), @@ -2615,6 +2618,7 @@ compilation = Annotated, function_name_prefix = "annotated_", compfuns = PredicateCompFuns.compfuns, + mk_random = (fn _ => error "no random generation"), modify_funT = I, additional_arguments = K [], wrap_compilation = @@ -2629,6 +2633,7 @@ compilation = DSeq, function_name_prefix = "dseq_", compfuns = DSequence_CompFuns.compfuns, + mk_random = (fn _ => error "no random generation"), modify_funT = I, additional_arguments = K [], wrap_compilation = K (K (K (K (K I)))) @@ -2641,6 +2646,17 @@ compilation = Pos_Random_DSeq, function_name_prefix = "random_dseq_", compfuns = Random_Sequence_CompFuns.compfuns, + mk_random = (fn T => fn additional_arguments => + let + val random = Const ("Quickcheck.random_class.random", + @{typ code_numeral} --> @{typ Random.seed} --> + HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) + in + Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} --> + HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> + Random_Sequence_CompFuns.mk_random_dseqT T) $ random + end), + modify_funT = I, additional_arguments = K [], wrap_compilation = K (K (K (K (K I)))) @@ -2653,6 +2669,7 @@ compilation = Neg_Random_DSeq, function_name_prefix = "random_dseq_neg_", compfuns = Random_Sequence_CompFuns.compfuns, + mk_random = (fn _ => error "no random generation"), modify_funT = I, additional_arguments = K [], wrap_compilation = K (K (K (K (K I)))) @@ -2683,16 +2700,19 @@ comp_modifiers = annotated_comp_modifiers, use_random = false, qname = "annotated_equation"}) -(* -val add_quickcheck_equations = gen_add_equations - (Steps {infer_modes = infer_modes_with_generator, - define_functions = define_functions random_comp_modifiers RandomPredCompFuns.compfuns, - compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns, + +val add_random_equations = gen_add_equations + (Steps { + define_functions = + fn options => fn preds => fn (s, modes) => + define_functions random_comp_modifiers PredicateCompFuns.compfuns options preds + (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes), + comp_modifiers = random_comp_modifiers, prove = prove_by_skip, add_code_equations = K (K I), - defined = defined_functions Random, + use_random = true, qname = "random_equation"}) -*) + val add_dseq_equations = gen_add_equations (Steps { define_functions = @@ -2777,9 +2797,8 @@ | DSeq => add_dseq_equations | Pos_Random_DSeq => add_random_dseq_equations | Depth_Limited => add_depth_limited_equations + | Random => add_random_equations | compilation => error ("Compilation not supported") - (*| Random => (fn opt => fn cs => add_equations opt cs #> add_quickcheck_equations opt cs) - | Annotated => add_annotated_equations*) ) options [const])) end in @@ -2858,7 +2877,8 @@ val additional_arguments = case compilation of Pred => [] - | Random => [@{term "5 :: code_numeral"}] + | Random => map (HOLogic.mk_number @{typ "code_numeral"}) arguments @ + [@{term "(1, 1) :: code_numeral * code_numeral"}] | Annotated => [] | Depth_Limited => [HOLogic.mk_number @{typ "code_numeral"} (hd arguments)] | DSeq => [] @@ -2885,7 +2905,7 @@ let val compfuns = case compilation of - Random => RandomPredCompFuns.compfuns + Random => PredicateCompFuns.compfuns | DSeq => DSequence_CompFuns.compfuns | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns | _ => PredicateCompFuns.compfuns @@ -2894,12 +2914,12 @@ val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t; val ts = case compilation of - Random => + (* Random => fst (Predicate.yieldn k (Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref) (fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' [] - |> Random_Engine.run)) - | Pos_Random_DSeq => + |> Random_Engine.run))*) + Pos_Random_DSeq => let val [nrandom, size, depth] = arguments in