--- a/src/HOL/IsaMakefile Tue May 26 11:02:59 2009 -0700
+++ b/src/HOL/IsaMakefile Wed May 27 07:28:29 2009 +0200
@@ -244,6 +244,7 @@
Tools/numeral_simprocs.ML \
Tools/numeral_syntax.ML \
Tools/polyhash.ML \
+ Tools/quickcheck_generators.ML \
Tools/Qelim/cooper_data.ML \
Tools/Qelim/cooper.ML \
Tools/Qelim/generated_cooper.ML \
--- a/src/HOL/Quickcheck.thy Tue May 26 11:02:59 2009 -0700
+++ b/src/HOL/Quickcheck.thy Wed May 27 07:28:29 2009 +0200
@@ -4,6 +4,7 @@
theory Quickcheck
imports Random Code_Eval
+uses ("Tools/quickcheck_generators.ML")
begin
notation fcomp (infixl "o>" 60)
@@ -16,59 +17,7 @@
fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-subsection {* Quickcheck generator *}
-
-ML {*
-structure Quickcheck =
-struct
-
-open Quickcheck;
-
-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 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 \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
- $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
- val return = @{term "Pair \<Colon> term list option \<Rightarrow> Random.seed \<Rightarrow> term list option \<times> Random.seed"};
- fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
- fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> 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 \<Rightarrow> 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 \<Rightarrow> term"}, t')));
- fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
- (Sign.mk_const thy (@{const_name 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.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;
-
-end
-*}
-
-setup {*
- Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I))
- #> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
-*}
-
-
-subsection {* Fundamental types*}
+subsection {* Fundamental and numeric types*}
instantiation bool :: random
begin
@@ -91,66 +40,6 @@
end
-text {* Type @{typ "'a \<Rightarrow> 'b"} *}
-
-ML {*
-structure Random_Engine =
-struct
-
-open Random_Engine;
-
-fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
- (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed)
- (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
- (seed : Random_Engine.seed) =
- let
- val (seed', seed'') = random_split seed;
- val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
- val fun_upd = Const (@{const_name fun_upd},
- (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
- fun random_fun' x =
- let
- val (seed, fun_map, f_t) = ! state;
- in case AList.lookup (uncurry eq) fun_map x
- of SOME y => y
- | NONE => let
- val t1 = term_of x;
- val ((y, t2), seed') = random seed;
- val fun_map' = (x, y) :: fun_map;
- val f_t' = fun_upd $ f_t $ t1 $ t2 ();
- val _ = state := (seed', fun_map', f_t');
- in y end
- end;
- fun term_fun' () = #3 (! state);
- in ((random_fun', term_fun'), seed'') end;
-
-end
-*}
-
-axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
- \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
- \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-
-code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun")
- -- {* With enough criminal energy this can be abused to derive @{prop False};
- for this reason we use a distinguished target @{text Quickcheck}
- not spoiling the regular trusted code generation *}
-
-instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
-begin
-
-definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
- "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
-
-instance ..
-
-end
-
-code_reserved Quickcheck Random_Engine
-
-
-subsection {* Numeric types *}
-
instantiation nat :: random
begin
@@ -175,119 +64,40 @@
end
-subsection {* Type copies *}
+
+subsection {* Complex generators *}
+
+definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+ "collapse f = (f o\<rightarrow> id)"
-setup {*
-let
+definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
+ "beyond k l = (if l > k then l else 0)"
+
+use "Tools/quickcheck_generators.ML"
+setup {* Quickcheck_Generators.setup *}
+
+code_reserved Quickcheck Quickcheck_Generators
+
+text {* Type @{typ "'a \<Rightarrow> 'b"} *}
-fun mk_random_typecopy tyco vs constr typ thy =
- let
- val Ts = map TFree vs;
- val T = Type (tyco, Ts);
- fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"})
- val Ttm = mk_termifyT T;
- val typtm = mk_termifyT typ;
- fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
- fun mk_random T = mk_const @{const_name random} [T];
- val size = @{term "k\<Colon>code_numeral"};
- val v = "x";
- val t_v = Free (v, typtm);
- 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]
- $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
- @{typ Random.seed} (SOME Ttm, @{typ Random.seed});
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
- in
- thy
- |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
- |> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
- |> snd
- |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end;
+axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
+ \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
+ \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-fun ensure_random_typecopy tyco thy =
- let
- val SOME { vs = raw_vs, constr, typ = raw_typ, ... } =
- TypecopyPackage.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 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;
+code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun")
+ -- {* With enough criminal energy this can be abused to derive @{prop False};
+ for this reason we use a distinguished target @{text Quickcheck}
+ not spoiling the regular trusted code generation *}
-in
+instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
+begin
-TypecopyPackage.interpretation ensure_random_typecopy
+definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+ "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
+
+instance ..
end
-*}
-
-
-subsection {* Type copies *}
-
-setup {*
-let
-
-fun mk_random_typecopy tyco vs constr typ thy =
- let
- val Ts = map TFree vs;
- val T = Type (tyco, Ts);
- fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"})
- val Ttm = mk_termifyT T;
- val typtm = mk_termifyT typ;
- fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
- fun mk_random T = mk_const @{const_name random} [T];
- val size = @{term "k\<Colon>code_numeral"};
- val v = "x";
- val t_v = Free (v, typtm);
- 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]
- $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
- @{typ Random.seed} (SOME Ttm, @{typ Random.seed});
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
- in
- thy
- |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
- |> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
- |> snd
- |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end;
-
-fun ensure_random_typecopy tyco thy =
- let
- val SOME { vs = raw_vs, constr, typ = raw_typ, ... } =
- TypecopyPackage.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 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;
-
-in
-
-TypecopyPackage.interpretation ensure_random_typecopy
-
-end
-*}
-
-
-subsection {* Datatypes *}
-
-text {* under construction *}
no_notation fcomp (infixl "o>" 60)
--- a/src/HOL/Random.thy Tue May 26 11:02:59 2009 -0700
+++ b/src/HOL/Random.thy Wed May 27 07:28:29 2009 +0200
@@ -119,7 +119,7 @@
qed
lemma select_weigth_drop_zero:
- "Random.select_weight (filter (\<lambda>(k, _). k > 0) xs) = Random.select_weight xs"
+ "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
proof -
have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
by (induct xs) auto
@@ -128,9 +128,9 @@
lemma select_weigth_select:
assumes "xs \<noteq> []"
- shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
+ shows "select_weight (map (Pair 1) xs) = select xs"
proof -
- have less: "\<And>s. fst (Random.range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
+ have less: "\<And>s. fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
using assms by (intro range) simp
moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)"
by (induct xs) simp_all
--- a/src/HOL/Tools/primrec_package.ML Tue May 26 11:02:59 2009 -0700
+++ b/src/HOL/Tools/primrec_package.ML Wed May 27 07:28:29 2009 +0200
@@ -16,6 +16,8 @@
val add_primrec_overloaded: (string * (string * typ) * bool) list ->
(binding * typ option * mixfix) list ->
(Attrib.binding * term) list -> theory -> thm list * theory
+ val add_primrec_simple: ((binding * typ) * mixfix) list -> (binding * term) list ->
+ local_theory -> (string * thm list list) * local_theory
end;
structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -211,22 +213,12 @@
else find_dts dt_info tnames' tnames);
-(* primrec definition *)
+(* distill primitive definition(s) from primrec specification *)
-local
-
-fun prove_spec ctxt names rec_rewrites defs eqs =
+fun distill lthy fixes eqs =
let
- val rewrites = map mk_meta_eq rec_rewrites @ map (snd o snd) defs;
- fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
- val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
- in map (fn (a, t) => (a, [Goal.prove ctxt [] [] t tac])) eqs end;
-
-fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
- let
- val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
- orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes) o snd) spec [];
+ orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) eqs [];
val tnames = distinct (op =) (map (#1 o snd) eqns);
val dts = find_dts (DatatypePackage.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
val main_fns = map (fn (tname, {index, ...}) =>
@@ -236,31 +228,59 @@
("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
else snd (hd dts);
val (fnames, fnss) = fold_rev (process_fun descr eqns) main_fns ([], []);
- val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
- val names1 = map snd fnames;
- val names2 = map fst eqns;
- val _ = if gen_eq_set (op =) (names1, names2) then ()
- else primrec_error ("functions " ^ commas_quote names2 ^
+ val (fs, raw_defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
+ val defs = map (make_def lthy fixes fs) raw_defs;
+ val names = map snd fnames;
+ val names_eqns = map fst eqns;
+ val _ = if gen_eq_set (op =) (names, names_eqns) then ()
+ else primrec_error ("functions " ^ commas_quote names_eqns ^
"\nare not mutually recursive");
- val prefix = space_implode "_" (map (Long_Name.base_name o #1) defs);
- val qualify = Binding.qualify false prefix;
- val spec' = (map o apfst)
- (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
- val simp_atts = map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add];
+ val rec_rewrites' = map mk_meta_eq rec_rewrites;
+ val prefix = space_implode "_" (map (Long_Name.base_name o #1) raw_defs);
+ fun prove lthy defs =
+ let
+ val rewrites = rec_rewrites' @ map (snd o snd) defs;
+ fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
+ val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
+ in map (fn eq => [Goal.prove lthy [] [] eq tac]) eqs end;
+ in ((prefix, (fs, defs)), prove) end
+ handle PrimrecError (msg, some_eqn) =>
+ error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
+ of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn)
+ | NONE => ""));
+
+
+(* primrec definition *)
+
+fun add_primrec_simple fixes spec lthy =
+ let
+ val ((prefix, (fs, defs)), prove) = distill lthy fixes (map snd spec);
+ in
+ lthy
+ |> fold_map (LocalTheory.define Thm.definitionK) defs
+ |-> (fn defs => `(fn lthy => (prefix, prove lthy defs)))
+ end;
+
+local
+
+fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
+ let
+ val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
+ fun attr_bindings prefix = map (fn ((b, attrs), _) =>
+ (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec;
+ fun simp_attr_binding prefix = (Binding.qualify false prefix (Binding.name "simps"),
+ map (Attrib.internal o K)
+ [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]);
in
lthy
|> set_group ? LocalTheory.set_group (serial_string ())
- |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
- |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
- |-> (fn simps => fold_map (LocalTheory.note Thm.generatedK) simps)
- |-> (fn simps' => LocalTheory.note Thm.generatedK
- ((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps'))
+ |> add_primrec_simple fixes spec
+ |-> (fn (prefix, simps) => fold_map (LocalTheory.note Thm.generatedK)
+ (attr_bindings prefix ~~ simps)
+ #-> (fn simps' => LocalTheory.note Thm.generatedK
+ (simp_attr_binding prefix, maps snd simps')))
|>> snd
- end handle PrimrecError (msg, some_eqn) =>
- error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
- of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn)
- | NONE => ""));
+ end;
in
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/quickcheck_generators.ML Wed May 27 07:28:29 2009 +0200
@@ -0,0 +1,145 @@
+(* Author: Florian Haftmann, TU Muenchen
+
+Quickcheck generators for various types.
+*)
+
+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)
+ -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
+ val ensure_random_typecopy: string -> theory -> theory
+ val eval_ref: (unit -> int -> int * int -> term list option * (int * int)) option ref
+ val setup: theory -> theory
+end;
+
+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";
+
+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 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;
+
+
+(** typ "'a => 'b" **)
+
+type seed = Random_Engine.seed;
+
+fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
+ (random : seed -> ('b * (unit -> term)) * seed)
+ (random_split : seed -> seed * seed)
+ (seed : seed) =
+ let
+ val (seed', seed'') = random_split seed;
+ val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
+ val fun_upd = Const (@{const_name fun_upd},
+ (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
+ fun random_fun' x =
+ let
+ val (seed, fun_map, f_t) = ! state;
+ in case AList.lookup (uncurry eq) fun_map x
+ of SOME y => y
+ | NONE => let
+ val t1 = term_of x;
+ val ((y, t2), seed') = random seed;
+ val fun_map' = (x, y) :: fun_map;
+ val f_t' = fun_upd $ f_t $ t1 $ t2 ();
+ val _ = state := (seed', fun_map', f_t');
+ in y end
+ end;
+ fun term_fun' () = #3 (! state);
+ in ((random_fun', term_fun'), seed'') end;
+
+
+(** type copies **)
+
+fun mk_random_typecopy tyco vs constr typ 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;
+ fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
+ fun mk_random T = mk_const @{const_name random} [T];
+ val size = @{term "j::code_numeral"};
+ val v = "x";
+ val t_v = Free (v, typtm);
+ 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]
+ $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
+ @{typ Random.seed} (SOME Ttm, @{typ Random.seed});
+ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+ in
+ thy
+ |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
+ |> `(fn lthy => Syntax.check_term lthy eq)
+ |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
+ |> snd
+ |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+ end;
+
+fun ensure_random_typecopy tyco thy =
+ let
+ val SOME { vs = raw_vs, constr, typ = raw_typ, ... } =
+ TypecopyPackage.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 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;
+
+
+(** datatypes **)
+
+(* still under construction *)
+
+
+(** 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)
+ #> TypecopyPackage.interpretation ensure_random_typecopy;
+
+end;