separate module for quickcheck generators
authorhaftmann
Tue May 26 17:29:32 2009 +0200 (2009-05-26)
changeset 312604d273d043d59
parent 31256 cf75908fd3c3
child 31261 900ebbc35e30
separate module for quickcheck generators
src/HOL/IsaMakefile
src/HOL/Quickcheck.thy
src/HOL/Tools/quickcheck_generators.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue May 26 13:40:50 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue May 26 17:29:32 2009 +0200
     1.3 @@ -244,6 +244,7 @@
     1.4    Tools/numeral_simprocs.ML \
     1.5    Tools/numeral_syntax.ML \
     1.6    Tools/polyhash.ML \
     1.7 +  Tools/quickcheck_generators.ML \
     1.8    Tools/Qelim/cooper_data.ML \
     1.9    Tools/Qelim/cooper.ML \
    1.10    Tools/Qelim/generated_cooper.ML \
     2.1 --- a/src/HOL/Quickcheck.thy	Tue May 26 13:40:50 2009 +0200
     2.2 +++ b/src/HOL/Quickcheck.thy	Tue May 26 17:29:32 2009 +0200
     2.3 @@ -4,6 +4,7 @@
     2.4  
     2.5  theory Quickcheck
     2.6  imports Random Code_Eval
     2.7 +uses ("Tools/quickcheck_generators.ML")
     2.8  begin
     2.9  
    2.10  notation fcomp (infixl "o>" 60)
    2.11 @@ -16,59 +17,7 @@
    2.12    fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    2.13  
    2.14  
    2.15 -subsection {* Quickcheck generator *}
    2.16 -
    2.17 -ML {*
    2.18 -structure Quickcheck =
    2.19 -struct
    2.20 -
    2.21 -open Quickcheck;
    2.22 -
    2.23 -val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
    2.24 -
    2.25 -val target = "Quickcheck";
    2.26 -
    2.27 -fun mk_generator_expr thy prop tys =
    2.28 -  let
    2.29 -    val bound_max = length tys - 1;
    2.30 -    val bounds = map_index (fn (i, ty) =>
    2.31 -      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
    2.32 -    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
    2.33 -    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
    2.34 -    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
    2.35 -      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
    2.36 -    val return = @{term "Pair \<Colon> term list option \<Rightarrow> Random.seed \<Rightarrow> term list option \<times> Random.seed"};
    2.37 -    fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    2.38 -    fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
    2.39 -    fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
    2.40 -      liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    2.41 -    fun mk_split ty = Sign.mk_const thy
    2.42 -      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
    2.43 -    fun mk_scomp_split ty t t' =
    2.44 -      mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t
    2.45 -        (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
    2.46 -    fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
    2.47 -      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
    2.48 -  in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
    2.49 -
    2.50 -fun compile_generator_expr thy t =
    2.51 -  let
    2.52 -    val tys = (map snd o fst o strip_abs) t;
    2.53 -    val t' = mk_generator_expr thy t tys;
    2.54 -    val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
    2.55 -      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
    2.56 -  in f #> Random_Engine.run end;
    2.57 -
    2.58 -end
    2.59 -*}
    2.60 -
    2.61 -setup {*
    2.62 -  Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I))
    2.63 -  #> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
    2.64 -*}
    2.65 -
    2.66 -
    2.67 -subsection {* Fundamental types*}
    2.68 +subsection {* Fundamental and numeric types*}
    2.69  
    2.70  instantiation bool :: random
    2.71  begin
    2.72 @@ -91,66 +40,6 @@
    2.73  
    2.74  end
    2.75  
    2.76 -text {* Type @{typ "'a \<Rightarrow> 'b"} *}
    2.77 -
    2.78 -ML {*
    2.79 -structure Random_Engine =
    2.80 -struct
    2.81 -
    2.82 -open Random_Engine;
    2.83 -
    2.84 -fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
    2.85 -    (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed)
    2.86 -    (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
    2.87 -    (seed : Random_Engine.seed) =
    2.88 -  let
    2.89 -    val (seed', seed'') = random_split seed;
    2.90 -    val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
    2.91 -    val fun_upd = Const (@{const_name fun_upd},
    2.92 -      (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
    2.93 -    fun random_fun' x =
    2.94 -      let
    2.95 -        val (seed, fun_map, f_t) = ! state;
    2.96 -      in case AList.lookup (uncurry eq) fun_map x
    2.97 -       of SOME y => y
    2.98 -        | NONE => let
    2.99 -              val t1 = term_of x;
   2.100 -              val ((y, t2), seed') = random seed;
   2.101 -              val fun_map' = (x, y) :: fun_map;
   2.102 -              val f_t' = fun_upd $ f_t $ t1 $ t2 ();
   2.103 -              val _ = state := (seed', fun_map', f_t');
   2.104 -            in y end
   2.105 -      end;
   2.106 -    fun term_fun' () = #3 (! state);
   2.107 -  in ((random_fun', term_fun'), seed'') end;
   2.108 -
   2.109 -end
   2.110 -*}
   2.111 -
   2.112 -axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
   2.113 -  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
   2.114 -  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   2.115 -
   2.116 -code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun")
   2.117 -  -- {* With enough criminal energy this can be abused to derive @{prop False};
   2.118 -  for this reason we use a distinguished target @{text Quickcheck}
   2.119 -  not spoiling the regular trusted code generation *}
   2.120 -
   2.121 -instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
   2.122 -begin
   2.123 -
   2.124 -definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   2.125 -  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
   2.126 -
   2.127 -instance ..
   2.128 -
   2.129 -end
   2.130 -
   2.131 -code_reserved Quickcheck Random_Engine
   2.132 -
   2.133 -
   2.134 -subsection {* Numeric types *}
   2.135 -
   2.136  instantiation nat :: random
   2.137  begin
   2.138  
   2.139 @@ -175,119 +64,40 @@
   2.140  
   2.141  end
   2.142  
   2.143 -subsection {* Type copies *}
   2.144 +
   2.145 +subsection {* Complex generators *}
   2.146 +
   2.147 +definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
   2.148 +  "collapse f = (f o\<rightarrow> id)"
   2.149  
   2.150 -setup {*
   2.151 -let
   2.152 +definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
   2.153 +  "beyond k l = (if l > k then l else 0)"
   2.154 +
   2.155 +use "Tools/quickcheck_generators.ML"
   2.156 +setup {* Quickcheck_Generators.setup *}
   2.157 +
   2.158 +code_reserved Quickcheck Quickcheck_Generators
   2.159 +
   2.160 +text {* Type @{typ "'a \<Rightarrow> 'b"} *}
   2.161  
   2.162 -fun mk_random_typecopy tyco vs constr typ thy =
   2.163 -  let
   2.164 -    val Ts = map TFree vs;  
   2.165 -    val T = Type (tyco, Ts);
   2.166 -    fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"})
   2.167 -    val Ttm = mk_termifyT T;
   2.168 -    val typtm = mk_termifyT typ;
   2.169 -    fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
   2.170 -    fun mk_random T = mk_const @{const_name random} [T];
   2.171 -    val size = @{term "k\<Colon>code_numeral"};
   2.172 -    val v = "x";
   2.173 -    val t_v = Free (v, typtm);
   2.174 -    val t_constr = mk_const constr Ts;
   2.175 -    val lhs = mk_random T $ size;
   2.176 -    val rhs = HOLogic.mk_ST [(((mk_random typ) $ size, @{typ Random.seed}), SOME (v, typtm))]
   2.177 -      (HOLogic.mk_return Ttm @{typ Random.seed}
   2.178 -      (mk_const "Code_Eval.valapp" [typ, T]
   2.179 -        $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
   2.180 -      @{typ Random.seed} (SOME Ttm, @{typ Random.seed});
   2.181 -    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   2.182 -  in   
   2.183 -    thy
   2.184 -    |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
   2.185 -    |> `(fn lthy => Syntax.check_term lthy eq)
   2.186 -    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
   2.187 -    |> snd
   2.188 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   2.189 -  end;
   2.190 +axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
   2.191 +  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
   2.192 +  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   2.193  
   2.194 -fun ensure_random_typecopy tyco thy =
   2.195 -  let
   2.196 -    val SOME { vs = raw_vs, constr, typ = raw_typ, ... } =
   2.197 -      TypecopyPackage.get_info thy tyco;
   2.198 -    val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
   2.199 -    val typ = map_atyps (fn TFree (v, sort) =>
   2.200 -      TFree (v, constrain sort @{sort random})) raw_typ;
   2.201 -    val vs' = Term.add_tfreesT typ [];
   2.202 -    val vs = map (fn (v, sort) =>
   2.203 -      (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
   2.204 -    val do_inst = Sign.of_sort thy (typ, @{sort random});
   2.205 -  in if do_inst then mk_random_typecopy tyco vs constr typ thy else thy end;
   2.206 +code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun")
   2.207 +  -- {* With enough criminal energy this can be abused to derive @{prop False};
   2.208 +  for this reason we use a distinguished target @{text Quickcheck}
   2.209 +  not spoiling the regular trusted code generation *}
   2.210  
   2.211 -in
   2.212 +instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
   2.213 +begin
   2.214  
   2.215 -TypecopyPackage.interpretation ensure_random_typecopy
   2.216 +definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   2.217 +  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
   2.218 +
   2.219 +instance ..
   2.220  
   2.221  end
   2.222 -*}
   2.223 -
   2.224 -
   2.225 -subsection {* Type copies *}
   2.226 -
   2.227 -setup {*
   2.228 -let
   2.229 -
   2.230 -fun mk_random_typecopy tyco vs constr typ thy =
   2.231 -  let
   2.232 -    val Ts = map TFree vs;
   2.233 -    val T = Type (tyco, Ts);
   2.234 -    fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"})
   2.235 -    val Ttm = mk_termifyT T;
   2.236 -    val typtm = mk_termifyT typ;
   2.237 -    fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
   2.238 -    fun mk_random T = mk_const @{const_name random} [T];
   2.239 -    val size = @{term "k\<Colon>code_numeral"};
   2.240 -    val v = "x";
   2.241 -    val t_v = Free (v, typtm);
   2.242 -    val t_constr = mk_const constr Ts;
   2.243 -    val lhs = mk_random T $ size;
   2.244 -    val rhs = HOLogic.mk_ST [(((mk_random typ) $ size, @{typ Random.seed}), SOME (v, typtm))]
   2.245 -      (HOLogic.mk_return Ttm @{typ Random.seed}
   2.246 -      (mk_const "Code_Eval.valapp" [typ, T]
   2.247 -        $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
   2.248 -      @{typ Random.seed} (SOME Ttm, @{typ Random.seed});
   2.249 -    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   2.250 -  in
   2.251 -    thy
   2.252 -    |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
   2.253 -    |> `(fn lthy => Syntax.check_term lthy eq)
   2.254 -    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
   2.255 -    |> snd
   2.256 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   2.257 -  end;
   2.258 -
   2.259 -fun ensure_random_typecopy tyco thy =
   2.260 -  let
   2.261 -    val SOME { vs = raw_vs, constr, typ = raw_typ, ... } =
   2.262 -      TypecopyPackage.get_info thy tyco;
   2.263 -    val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
   2.264 -    val typ = map_atyps (fn TFree (v, sort) =>
   2.265 -      TFree (v, constrain sort @{sort random})) raw_typ;
   2.266 -    val vs' = Term.add_tfreesT typ [];
   2.267 -    val vs = map (fn (v, sort) =>
   2.268 -      (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
   2.269 -    val do_inst = Sign.of_sort thy (typ, @{sort random});
   2.270 -  in if do_inst then mk_random_typecopy tyco vs constr typ thy else thy end;
   2.271 -
   2.272 -in
   2.273 -
   2.274 -TypecopyPackage.interpretation ensure_random_typecopy
   2.275 -
   2.276 -end
   2.277 -*}
   2.278 -
   2.279 -
   2.280 -subsection {* Datatypes *}
   2.281 -
   2.282 -text {* under construction *}
   2.283  
   2.284  
   2.285  no_notation fcomp (infixl "o>" 60)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Tue May 26 17:29:32 2009 +0200
     3.3 @@ -0,0 +1,145 @@
     3.4 +(* Author: Florian Haftmann, TU Muenchen
     3.5 +
     3.6 +Quickcheck generators for various types.
     3.7 +*)
     3.8 +
     3.9 +signature QUICKCHECK_GENERATORS =
    3.10 +sig
    3.11 +  val compile_generator_expr: theory -> term -> int -> term list option
    3.12 +  type seed = Random_Engine.seed
    3.13 +  val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
    3.14 +    -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
    3.15 +    -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
    3.16 +  val ensure_random_typecopy: string -> theory -> theory
    3.17 +  val eval_ref: (unit -> int -> int * int -> term list option * (int * int)) option ref
    3.18 +  val setup: theory -> theory
    3.19 +end;
    3.20 +
    3.21 +structure Quickcheck_Generators : QUICKCHECK_GENERATORS =
    3.22 +struct
    3.23 +
    3.24 +(** building and compiling generator expressions **)
    3.25 +
    3.26 +val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
    3.27 +
    3.28 +val target = "Quickcheck";
    3.29 +
    3.30 +fun mk_generator_expr thy prop tys =
    3.31 +  let
    3.32 +    val bound_max = length tys - 1;
    3.33 +    val bounds = map_index (fn (i, ty) =>
    3.34 +      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
    3.35 +    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
    3.36 +    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
    3.37 +    val check = @{term "If :: bool => term list option => term list option => term list option"}
    3.38 +      $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option "} $ terms);
    3.39 +    val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"};
    3.40 +    fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    3.41 +    fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit => term"});
    3.42 +    fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
    3.43 +      liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    3.44 +    fun mk_split ty = Sign.mk_const thy
    3.45 +      (@{const_name split}, [ty, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
    3.46 +    fun mk_scomp_split ty t t' =
    3.47 +      mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t
    3.48 +        (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit => term"}, t')));
    3.49 +    fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
    3.50 +      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
    3.51 +  in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
    3.52 +
    3.53 +fun compile_generator_expr thy t =
    3.54 +  let
    3.55 +    val tys = (map snd o fst o strip_abs) t;
    3.56 +    val t' = mk_generator_expr thy t tys;
    3.57 +    val f = Code_ML.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
    3.58 +      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
    3.59 +  in f #> Random_Engine.run end;
    3.60 +
    3.61 +
    3.62 +(** typ "'a => 'b" **)
    3.63 +
    3.64 +type seed = Random_Engine.seed;
    3.65 +
    3.66 +fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
    3.67 +    (random : seed -> ('b * (unit -> term)) * seed)
    3.68 +    (random_split : seed -> seed * seed)
    3.69 +    (seed : seed) =
    3.70 +  let
    3.71 +    val (seed', seed'') = random_split seed;
    3.72 +    val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
    3.73 +    val fun_upd = Const (@{const_name fun_upd},
    3.74 +      (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
    3.75 +    fun random_fun' x =
    3.76 +      let
    3.77 +        val (seed, fun_map, f_t) = ! state;
    3.78 +      in case AList.lookup (uncurry eq) fun_map x
    3.79 +       of SOME y => y
    3.80 +        | NONE => let
    3.81 +              val t1 = term_of x;
    3.82 +              val ((y, t2), seed') = random seed;
    3.83 +              val fun_map' = (x, y) :: fun_map;
    3.84 +              val f_t' = fun_upd $ f_t $ t1 $ t2 ();
    3.85 +              val _ = state := (seed', fun_map', f_t');
    3.86 +            in y end
    3.87 +      end;
    3.88 +    fun term_fun' () = #3 (! state);
    3.89 +  in ((random_fun', term_fun'), seed'') end;
    3.90 +
    3.91 +
    3.92 +(** type copies **)
    3.93 +
    3.94 +fun mk_random_typecopy tyco vs constr typ thy =
    3.95 +  let
    3.96 +    val Ts = map TFree vs;  
    3.97 +    val T = Type (tyco, Ts);
    3.98 +    fun mk_termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
    3.99 +    val Ttm = mk_termifyT T;
   3.100 +    val typtm = mk_termifyT typ;
   3.101 +    fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
   3.102 +    fun mk_random T = mk_const @{const_name random} [T];
   3.103 +    val size = @{term "j::code_numeral"};
   3.104 +    val v = "x";
   3.105 +    val t_v = Free (v, typtm);
   3.106 +    val t_constr = mk_const constr Ts;
   3.107 +    val lhs = mk_random T $ size;
   3.108 +    val rhs = HOLogic.mk_ST [(((mk_random typ) $ size, @{typ Random.seed}), SOME (v, typtm))]
   3.109 +      (HOLogic.mk_return Ttm @{typ Random.seed}
   3.110 +      (mk_const "Code_Eval.valapp" [typ, T]
   3.111 +        $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
   3.112 +      @{typ Random.seed} (SOME Ttm, @{typ Random.seed});
   3.113 +    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   3.114 +  in   
   3.115 +    thy
   3.116 +    |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
   3.117 +    |> `(fn lthy => Syntax.check_term lthy eq)
   3.118 +    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
   3.119 +    |> snd
   3.120 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   3.121 +  end;
   3.122 +
   3.123 +fun ensure_random_typecopy tyco thy =
   3.124 +  let
   3.125 +    val SOME { vs = raw_vs, constr, typ = raw_typ, ... } =
   3.126 +      TypecopyPackage.get_info thy tyco;
   3.127 +    val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
   3.128 +    val typ = map_atyps (fn TFree (v, sort) =>
   3.129 +      TFree (v, constrain sort @{sort random})) raw_typ;
   3.130 +    val vs' = Term.add_tfreesT typ [];
   3.131 +    val vs = map (fn (v, sort) =>
   3.132 +      (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
   3.133 +    val do_inst = Sign.of_sort thy (typ, @{sort random});
   3.134 +  in if do_inst then mk_random_typecopy tyco vs constr typ thy else thy end;
   3.135 +
   3.136 +
   3.137 +(** datatypes **)
   3.138 +
   3.139 +(* still under construction *)
   3.140 +
   3.141 +
   3.142 +(** setup **)
   3.143 +
   3.144 +val setup = Code_Target.extend_target (target, (Code_ML.target_Eval, K I))
   3.145 +  #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of)
   3.146 +  #> TypecopyPackage.interpretation ensure_random_typecopy;
   3.147 +
   3.148 +end;