# HG changeset patch # User bulwahn # Date 1269876638 -7200 # Node ID 3ee4c29ead7f6dbaa32bf17062ad54244a0d3bb8 # Parent 64bbbd858c393a8c0de84f5c79ac8724a417954a adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck diff -r 64bbbd858c39 -r 3ee4c29ead7f src/HOL/Lazy_Sequence.thy --- a/src/HOL/Lazy_Sequence.thy Mon Mar 29 17:30:36 2010 +0200 +++ b/src/HOL/Lazy_Sequence.thy Mon Mar 29 17:30:38 2010 +0200 @@ -131,6 +131,7 @@ datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence) + val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence end; structure Lazy_Sequence : LAZY_SEQUENCE = @@ -142,6 +143,8 @@ val yieldn = @{code yieldn} +val map = @{code map} + end; *} diff -r 64bbbd858c39 -r 3ee4c29ead7f src/HOL/Random.thy --- a/src/HOL/Random.thy Mon Mar 29 17:30:36 2010 +0200 +++ b/src/HOL/Random.thy Mon Mar 29 17:30:38 2010 +0200 @@ -1,3 +1,4 @@ + (* Author: Florian Haftmann, TU Muenchen *) header {* A HOL random engine *} @@ -154,6 +155,14 @@ in +fun next_seed () = + let + val (seed1, seed') = @{code split_seed} (! seed) + val _ = seed := seed' + in + seed1 + end + fun run f = let val (x, seed') = f (! seed); diff -r 64bbbd858c39 -r 3ee4c29ead7f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 29 17:30:36 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 29 17:30:38 2010 +0200 @@ -39,6 +39,9 @@ val dseq_eval_ref : (unit -> term DSequence.dseq) option Unsynchronized.ref val random_dseq_eval_ref : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) option Unsynchronized.ref + val new_random_dseq_eval_ref : + (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) + option Unsynchronized.ref val code_pred_intro_attrib : attribute (* used by Quickcheck_Generator *) @@ -58,8 +61,10 @@ val pred_compfuns : compilation_funs val randompred_compfuns : compilation_funs + val new_randompred_compfuns : compilation_funs val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory val add_random_dseq_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory + val add_new_random_dseq_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory val mk_tracing : string -> term -> term end; @@ -1020,6 +1025,7 @@ (* for external use with interactive mode *) val pred_compfuns = PredicateCompFuns.compfuns val randompred_compfuns = Random_Sequence_CompFuns.compfuns; +val new_randompred_compfuns = New_Pos_Random_Sequence_CompFuns.compfuns (* compilation modifiers *) @@ -1892,7 +1898,7 @@ | (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]" | (t, Context m) => Syntax.string_of_term ctxt t ^ "[" ^ string_of_mode m ^ "]") -fun compile_expr compilation_modifiers ctxt pol (t, deriv) additional_arguments = +fun compile_expr compilation_modifiers ctxt (t, deriv) additional_arguments = let val compfuns = Comp_Mod.compfuns compilation_modifiers fun expr_of (t, deriv) = @@ -1926,7 +1932,7 @@ end fun compile_clause compilation_modifiers ctxt all_vs param_vs additional_arguments - (pol, mode) inp (ts, moded_ps) = + mode inp (ts, moded_ps) = let val compfuns = Comp_Mod.compfuns compilation_modifiers val iss = ho_arg_modes_of mode @@ -1959,8 +1965,7 @@ Prem t => let val u = - compile_expr compilation_modifiers ctxt - pol (t, deriv) additional_arguments' + compile_expr compilation_modifiers ctxt (t, deriv) additional_arguments' val (_, out_ts''') = split_mode mode (snd (strip_comb t)) val rest = compile_prems out_ts''' vs' names'' ps in @@ -1971,8 +1976,7 @@ val neg_compilation_modifiers = negative_comp_modifiers_of compilation_modifiers val u = mk_not compfuns - (compile_expr neg_compilation_modifiers ctxt - (not pol) (t, deriv) additional_arguments') + (compile_expr neg_compilation_modifiers ctxt (t, deriv) additional_arguments') val (_, out_ts''') = split_mode mode (snd (strip_comb t)) val rest = compile_prems out_ts''' vs' names'' ps in @@ -2005,6 +2009,8 @@ fun compile_pred compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls = let val ctxt = ProofContext.init thy + val compilation_modifiers = if pol then compilation_modifiers else + negative_comp_modifiers_of compilation_modifiers val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers (all_vs @ param_vs) val compfuns = Comp_Mod.compfuns compilation_modifiers @@ -2029,7 +2035,7 @@ (fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts val cl_ts = map (compile_clause compilation_modifiers - ctxt all_vs param_vs additional_arguments (pol, mode) (HOLogic.mk_tuple in_ts')) moded_cls; + ctxt all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts')) moded_cls; val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments (if null cl_ts then @@ -3127,6 +3133,8 @@ val dseq_eval_ref = Unsynchronized.ref (NONE : (unit -> term DSequence.dseq) option); val random_dseq_eval_ref = Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) option); +val new_random_dseq_eval_ref = + Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) option) (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*) fun analyze_compr thy compfuns param_user_modes (compilation, arguments) t_compr = @@ -3196,6 +3204,7 @@ [@{term "(1, 1) :: code_numeral * code_numeral"}] | DSeq => [] | Pos_Random_DSeq => [] + | New_Pos_Random_DSeq => [] val comp_modifiers = case compilation of Pred => predicate_comp_modifiers @@ -3205,8 +3214,9 @@ (*| Annotated => annotated_comp_modifiers*) | DSeq => dseq_comp_modifiers | Pos_Random_DSeq => pos_random_dseq_comp_modifiers + | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers val t_pred = compile_expr comp_modifiers (ProofContext.init thy) - true (body, deriv) additional_arguments; + (body, deriv) additional_arguments; val T_pred = dest_predT compfuns (fastype_of t_pred) val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple in @@ -3223,7 +3233,9 @@ Random => PredicateCompFuns.compfuns | DSeq => DSequence_CompFuns.compfuns | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns + | New_Pos_Random_DSeq => New_Pos_Random_Sequence_CompFuns.compfuns | _ => PredicateCompFuns.compfuns + val t = analyze_compr thy compfuns param_user_modes options t_compr; val T = dest_predT compfuns (fastype_of t); val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t; @@ -3249,6 +3261,18 @@ fst (DSequence.yieldn k (Code_Eval.eval NONE ("Predicate_Compile_Core.dseq_eval_ref", dseq_eval_ref) DSequence.map thy t' []) (the_single arguments) true) + | New_Pos_Random_DSeq => + let + val [nrandom, size, depth] = arguments + val seed = Random_Engine.next_seed () + in + fst (Lazy_Sequence.yieldn k + (Code_Eval.eval NONE + ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref) + (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth + |> Lazy_Sequence.map proc) + thy t' [] nrandom size seed depth)) + end | _ => fst (Predicate.yieldn k (Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref)