# HG changeset patch # User haftmann # Date 1243402109 -7200 # Node ID 4dbe0b4c313bc468e3c0d8f9be3d88beb552536a # Parent c1b981b71dba2dc391eaacb66df05a1cfe4cac2a# Parent 580510315ddaf449e6592f32e322a0a8ef1ab4b7 merged diff -r c1b981b71dba -r 4dbe0b4c313b src/HOL/IsaMakefile --- 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 \ diff -r c1b981b71dba -r 4dbe0b4c313b src/HOL/Quickcheck.thy --- 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 \ Random.seed \ ('a \ (unit \ term)) \ 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 \ 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.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 \ '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 \ typerep \ ('a \ 'a \ bool) \ ('a \ term) - \ (Random.seed \ ('b \ (unit \ term)) \ Random.seed) \ (Random.seed \ Random.seed \ Random.seed) - \ Random.seed \ (('a \ 'b) \ (unit \ term)) \ 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 \ Random.seed \ (('a \ 'b) \ (unit \ term)) \ 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 \ ('a \ 'b \ 'a) \ 'a) \ 'a \ 'b \ 'a" where + "collapse f = (f o\ id)" -setup {* -let +definition beyond :: "code_numeral \ code_numeral \ 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 \ '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 \ 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\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 \ typerep \ ('a \ 'a \ bool) \ ('a \ term) + \ (Random.seed \ ('b \ (unit \ term)) \ Random.seed) \ (Random.seed \ Random.seed \ Random.seed) + \ Random.seed \ (('a \ 'b) \ (unit \ term)) \ 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 \ Random.seed \ (('a \ 'b) \ (unit \ term)) \ 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 \ 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\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) diff -r c1b981b71dba -r 4dbe0b4c313b src/HOL/Random.thy --- 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 (\(k, _). k > 0) xs) = Random.select_weight xs" + "select_weight (filter (\(k, _). k > 0) xs) = select_weight xs" proof - have "listsum (map fst [(k, _)\xs . 0 < k]) = listsum (map fst xs)" by (induct xs) auto @@ -128,9 +128,9 @@ lemma select_weigth_select: assumes "xs \ []" - shows "Random.select_weight (map (Pair 1) xs) = Random.select xs" + shows "select_weight (map (Pair 1) xs) = select xs" proof - - have less: "\s. fst (Random.range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" + have less: "\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 diff -r c1b981b71dba -r 4dbe0b4c313b src/HOL/Tools/primrec_package.ML --- 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 diff -r c1b981b71dba -r 4dbe0b4c313b src/HOL/Tools/quickcheck_generators.ML --- /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;