# HG changeset patch # User haftmann # Date 1246891791 -7200 # Node ID 7300186d745af4479422ba48b79885b74d887d39 # Parent 3f933687fae98831a1dd61c2ab4f49c9848a0f5c tuned code diff -r 3f933687fae9 -r 7300186d745a src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Mon Jul 06 14:19:13 2009 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Mon Jul 06 16:49:51 2009 +0200 @@ -5,7 +5,6 @@ signature QUICKCHECK_GENERATORS = sig - val compile_generator_expr: theory -> term -> int -> term list option type seed = Random_Engine.seed val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term) -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed) @@ -16,6 +15,7 @@ -> string list -> string list * string list -> typ list * typ list -> term list * (term * term) list val ensure_random_datatype: Datatype.config -> string list -> theory -> theory + val compile_generator_expr: theory -> term -> int -> term list option val eval_ref: (unit -> int -> seed -> term list option * seed) option ref val setup: theory -> theory end; @@ -23,42 +23,13 @@ structure Quickcheck_Generators : QUICKCHECK_GENERATORS = struct -(** building and compiling generator expressions **) - -val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE; - -val target = "Quickcheck"; +(** abstract syntax **) -fun mk_generator_expr thy prop tys = - let - val bound_max = length tys - 1; - val bounds = map_index (fn (i, ty) => - (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys; - val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds); - val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds); - val check = @{term "If :: bool => term list option => term list option => term list option"} - $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option "} $ terms); - val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"}; - fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); - fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit => term"}); - fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp}, - liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; - fun mk_split ty = Sign.mk_const thy - (@{const_name split}, [ty, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]); - fun mk_scomp_split ty t t' = - mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t - (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit => term"}, t'))); - fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty - (Sign.mk_const thy (@{const_name Quickcheck.random}, [ty]) $ Bound i); - in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end; - -fun compile_generator_expr thy t = - let - val tys = (map snd o fst o strip_abs) t; - val t' = mk_generator_expr thy t tys; - val f = Code_ML.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref) - (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' []; - in f #> Random_Engine.run end; +fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}) +val size = @{term "i::code_numeral"}; +val size1 = @{term "(i::code_numeral) - 1"}; +val size' = @{term "j::code_numeral"}; +val seed = @{term "s::Random.seed"}; (** typ "'a => 'b" **) @@ -91,25 +62,22 @@ (** type copies **) -fun mk_random_typecopy tyco vs constr typ thy = +fun mk_random_typecopy tyco vs constr T' thy = let val Ts = map TFree vs; val T = Type (tyco, Ts); - fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}) - val Ttm = mk_termifyT T; - val typtm = mk_termifyT typ; + val Tm = termifyT T; + val Tm' = termifyT T'; fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts)); - fun mk_random T = mk_const @{const_name Quickcheck.random} [T]; - val size = @{term "j::code_numeral"}; val v = "x"; - val t_v = Free (v, typtm); + val t_v = Free (v, Tm'); val t_constr = mk_const constr Ts; - val lhs = mk_random T $ size; - val rhs = HOLogic.mk_ST [(((mk_random typ) $ size, @{typ Random.seed}), SOME (v, typtm))] - (HOLogic.mk_return Ttm @{typ Random.seed} - (mk_const "Code_Eval.valapp" [typ, T] + val lhs = HOLogic.mk_random T size; + val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))] + (HOLogic.mk_return Tm @{typ Random.seed} + (mk_const "Code_Eval.valapp" [T', T] $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v)) - @{typ Random.seed} (SOME Ttm, @{typ Random.seed}); + @{typ Random.seed} (SOME Tm, @{typ Random.seed}); val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); in thy @@ -122,16 +90,16 @@ fun ensure_random_typecopy tyco thy = let - val SOME { vs = raw_vs, constr, typ = raw_typ, ... } = + val SOME { vs = raw_vs, constr, typ = raw_T, ... } = Typecopy.get_info thy tyco; val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)); - val typ = map_atyps (fn TFree (v, sort) => - TFree (v, constrain sort @{sort random})) raw_typ; - val vs' = Term.add_tfreesT typ []; + val T = map_atyps (fn TFree (v, sort) => + TFree (v, constrain sort @{sort random})) raw_T; + val vs' = Term.add_tfreesT T []; val vs = map (fn (v, sort) => (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs; - val do_inst = Sign.of_sort thy (typ, @{sort random}); - in if do_inst then mk_random_typecopy tyco vs constr typ thy else thy end; + val can_inst = Sign.of_sort thy (T, @{sort random}); + in if can_inst then mk_random_typecopy tyco vs constr T thy else thy end; (** datatypes **) @@ -258,12 +226,7 @@ fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) = let val mk_const = curry (Sign.mk_const thy); - val i = @{term "i\code_numeral"}; - val i1 = @{term "(i\code_numeral) - 1"}; - val j = @{term "j\code_numeral"}; - val seed = @{term "s\Random.seed"}; val random_auxsN = map (prefix (random_auxN ^ "_")) (names @ auxnames); - fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \ term"}); val rTs = Ts @ Us; fun random_resultT T = @{typ Random.seed} --> HOLogic.mk_prodT (termifyT T,@{typ Random.seed}); @@ -272,7 +235,7 @@ val random_auxT = sizeT o random_resultT; val random_auxs = map2 (fn s => fn rT => Free (s, random_auxT rT)) random_auxsN rTs; - fun mk_random_call T = (NONE, (HOLogic.mk_random T j, T)); + fun mk_random_call T = (NONE, (HOLogic.mk_random T size', T)); fun mk_random_aux_call fTs (k, _) (tyco, Ts) = let val T = Type (tyco, Ts); @@ -280,7 +243,7 @@ | mk_random_fun_lift (fT :: fTs) t = mk_const @{const_name random_fun_lift} [fTs ---> T, fT] $ mk_random_fun_lift fTs t; - val t = mk_random_fun_lift fTs (nth random_auxs k $ i1 $ j); + val t = mk_random_fun_lift fTs (nth random_auxs k $ size1 $ size'); val size = Option.map snd (DatatypeCodegen.find_shortest_path descr k) |> the_default 0; in (SOME size, (t, fTs ---> T)) end; @@ -300,9 +263,9 @@ val t = HOLogic.mk_ST (map (fn (t, _) => (t, @{typ Random.seed})) tTs ~~ map SOME vs') tc @{typ Random.seed} (SOME T, @{typ Random.seed}); val tk = if is_rec - then if k = 0 then i + then if k = 0 then size else @{term "Quickcheck.beyond :: code_numeral \ code_numeral \ code_numeral"} - $ HOLogic.mk_number @{typ code_numeral} k $ i + $ HOLogic.mk_number @{typ code_numeral} k $ size else @{term "1::code_numeral"} in (is_rec, HOLogic.mk_prod (tk, t)) end; fun sort_rec xs = @@ -316,24 +279,23 @@ $ (mk_const @{const_name Random.select_weight} [random_resultT rT] $ HOLogic.mk_list (HOLogic.mk_prodT (@{typ code_numeral}, random_resultT rT)) xs) $ seed; - val auxs_lhss = map (fn t => t $ i $ j $ seed) random_auxs; + val auxs_lhss = map (fn t => t $ size $ size' $ seed) random_auxs; val auxs_rhss = map mk_select gen_exprss; in (random_auxs, auxs_lhss ~~ auxs_rhss) end; fun mk_random_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = let val _ = DatatypeAux.message config "Creating quickcheck generators ..."; - val i = @{term "i\code_numeral"}; val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; fun mk_size_arg k = case DatatypeCodegen.find_shortest_path descr k - of SOME (_, l) => if l = 0 then i + of SOME (_, l) => if l = 0 then size else @{term "max :: code_numeral \ code_numeral \ code_numeral"} - $ HOLogic.mk_number @{typ code_numeral} l $ i - | NONE => i; + $ HOLogic.mk_number @{typ code_numeral} l $ size + | NONE => size; val (random_auxs, auxs_eqs) = (apsnd o map) mk_prop_eq (mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us)); val random_defs = map_index (fn (k, T) => mk_prop_eq - (HOLogic.mk_random T i, nth random_auxs k $ mk_size_arg k $ i)) Ts; + (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts; in thy |> TheoryTarget.instantiation (tycos, vs, @{sort random}) @@ -381,11 +343,49 @@ end; +(** building and compiling generator expressions **) + +val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE; + +val target = "Quickcheck"; + +fun mk_generator_expr thy prop Ts = + let + val bound_max = length Ts - 1; + val bounds = map_index (fn (i, ty) => + (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts; + val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds); + val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds); + val check = @{term "If :: bool => term list option => term list option => term list option"} + $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option "} $ terms); + val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"}; + fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); + fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"}); + fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp}, + liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; + fun mk_split T = Sign.mk_const thy + (@{const_name split}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]); + fun mk_scomp_split T t t' = + mk_scomp (mk_termtyp T) @{typ "term list option"} @{typ Random.seed} t + (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t'))); + fun mk_bindclause (_, _, i, T) = mk_scomp_split T + (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i); + in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end; + +fun compile_generator_expr thy t = + let + val Ts = (map snd o fst o strip_abs) t; + val t' = mk_generator_expr thy t Ts; + val compile = Code_ML.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref) + (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' []; + in compile #> Random_Engine.run end; + + (** setup **) -val setup = Code_Target.extend_target (target, (Code_ML.target_Eval, K I)) - #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of) - #> Typecopy.interpretation ensure_random_typecopy - #> Datatype.interpretation ensure_random_datatype; +val setup = Typecopy.interpretation ensure_random_typecopy + #> Datatype.interpretation ensure_random_datatype + #> Code_Target.extend_target (target, (Code_ML.target_Eval, K I)) + #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of); end;