src/HOL/Tools/Quickcheck/random_generators.ML
author bulwahn
Mon Jul 18 10:34:21 2011 +0200 (2011-07-18)
changeset 43875 485d2ad43528
parent 43333 2bdec7f430d3
child 43876 b8fa7287ee4c
permissions -rw-r--r--
adding random, exhaustive and SML quickcheck as testers
     1 (*  Title:      HOL/Tools/Quickcheck/random_generators.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Random generators for various types.
     5 *)
     6 
     7 signature RANDOM_GENERATORS =
     8 sig
     9   type seed = Random_Engine.seed
    10   val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
    11     -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
    12     -> seed -> (('a -> 'b) * (unit -> term)) * seed
    13   val compile_generator_expr:
    14     Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
    15   val put_counterexample: (unit -> int -> int -> seed -> term list option * seed)
    16     -> Proof.context -> Proof.context
    17   val put_counterexample_report: (unit -> int -> int -> seed -> (term list option * (bool list * bool)) * seed)
    18     -> Proof.context -> Proof.context
    19   val setup: theory -> theory
    20 end;
    21 
    22 structure Random_Generators : RANDOM_GENERATORS =
    23 struct
    24 
    25 (** abstract syntax **)
    26 
    27 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
    28 val size = @{term "i::code_numeral"};
    29 val size_pred = @{term "(i::code_numeral) - 1"};
    30 val size' = @{term "j::code_numeral"};
    31 val seed = @{term "s::Random.seed"};
    32 
    33 
    34 (** typ "'a => 'b" **)
    35 
    36 type seed = Random_Engine.seed;
    37 
    38 fun random_fun T1 T2 eq term_of random random_split seed =
    39   let
    40     val fun_upd = Const (@{const_name fun_upd},
    41       (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
    42     val ((y, t2), seed') = random seed;
    43     val (seed'', seed''') = random_split seed';
    44 
    45     val state = Unsynchronized.ref (seed'', [], fn () => Abs ("x", T1, t2 ()));
    46     fun random_fun' x =
    47       let
    48         val (seed, fun_map, f_t) = ! state;
    49       in case AList.lookup (uncurry eq) fun_map x
    50        of SOME y => y
    51         | NONE => let
    52               val t1 = term_of x;
    53               val ((y, t2), seed') = random seed;
    54               val fun_map' = (x, y) :: fun_map;
    55               val f_t' = fn () => fun_upd $ f_t () $ t1 $ t2 ();
    56               val _ = state := (seed', fun_map', f_t');
    57             in y end
    58       end;
    59     fun term_fun' () = #3 (! state) ();
    60   in ((random_fun', term_fun'), seed''') end;
    61 
    62 
    63 (** datatypes **)
    64 
    65 (* definitional scheme for random instances on datatypes *)
    66 
    67 local
    68 
    69 fun dest_ctyp_nth k cT = nth (Thm.dest_ctyp cT) k;
    70 val eq = Thm.cprop_of @{thm random_aux_rec} |> Thm.dest_arg |> Thm.dest_arg |> Thm.dest_arg;
    71 val lhs = eq |> Thm.dest_arg1;
    72 val pt_random_aux = lhs |> Thm.dest_fun;
    73 val ct_k = lhs |> Thm.dest_arg;
    74 val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun;
    75 val aT = pt_random_aux |> Thm.ctyp_of_term |> dest_ctyp_nth 1;
    76 
    77 val rew_thms = map mk_meta_eq [@{thm code_numeral_zero_minus_one},
    78   @{thm Suc_code_numeral_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}];
    79 val rew_ts = map (Logic.dest_equals o Thm.prop_of) rew_thms;
    80 val rew_ss = HOL_ss addsimps rew_thms;
    81 
    82 in
    83 
    84 fun random_aux_primrec eq lthy =
    85   let
    86     val thy = Proof_Context.theory_of lthy;
    87     val ((t_random_aux as Free (random_aux, T)) $ (t_k as Free (v, _)), proto_t_rhs) =
    88       (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
    89     val Type (_, [_, iT]) = T;
    90     val icT = Thm.ctyp_of thy iT;
    91     val cert = Thm.cterm_of thy;
    92     val inst = Thm.instantiate_cterm ([(aT, icT)], []);
    93     fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
    94     val t_rhs = lambda t_k proto_t_rhs;
    95     val eqs0 = [subst_v @{term "0::code_numeral"} eq,
    96       subst_v (@{term "Suc_code_numeral"} $ t_k) eq];
    97     val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
    98     val ((_, (_, eqs2)), lthy') = Primrec.add_primrec_simple
    99       [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;
   100     val cT_random_aux = inst pt_random_aux;
   101     val cT_rhs = inst pt_rhs;
   102     val rule = @{thm random_aux_rec}
   103       |> Drule.instantiate_normalize ([(aT, icT)],
   104            [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
   105     val tac = ALLGOALS (rtac rule)
   106       THEN ALLGOALS (simp_tac rew_ss)
   107       THEN (ALLGOALS (Proof_Context.fact_tac eqs2))
   108     val simp = Skip_Proof.prove lthy' [v] [] eq (K tac);
   109   in (simp, lthy') end;
   110 
   111 end;
   112 
   113 fun random_aux_primrec_multi auxname [eq] lthy =
   114       lthy
   115       |> random_aux_primrec eq
   116       |>> (fn simp => [simp])
   117   | random_aux_primrec_multi auxname (eqs as _ :: _ :: _) lthy =
   118       let
   119         val thy = Proof_Context.theory_of lthy;
   120         val (lhss, rhss) = map_split (HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs;
   121         val (vs, (arg as Free (v, _)) :: _) = map_split (fn (t1 $ t2) => (t1, t2)) lhss;
   122         val Ts = map fastype_of lhss;
   123         val tupleT = foldr1 HOLogic.mk_prodT Ts;
   124         val aux_lhs = Free ("mutual_" ^ auxname, fastype_of arg --> tupleT) $ arg;
   125         val aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   126           (aux_lhs, foldr1 HOLogic.mk_prod rhss);
   127         fun mk_proj t [T] = [t]
   128           | mk_proj t (Ts as T :: (Ts' as _ :: _)) =
   129               Const (@{const_name fst}, foldr1 HOLogic.mk_prodT Ts --> T) $ t
   130                 :: mk_proj (Const (@{const_name snd},
   131                   foldr1 HOLogic.mk_prodT Ts --> foldr1 HOLogic.mk_prodT Ts') $ t) Ts';
   132         val projs = mk_proj (aux_lhs) Ts;
   133         val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs;
   134         val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) =>
   135           ((Binding.conceal (Binding.name name), NoSyn),
   136             (apfst Binding.conceal Attrib.empty_binding, rhs))) vs proj_eqs;
   137         val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq;
   138         fun prove_eqs aux_simp proj_defs lthy = 
   139           let
   140             val proj_simps = map (snd o snd) proj_defs;
   141             fun tac { context = ctxt, prems = _ } =
   142               ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
   143               THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
   144               THEN ALLGOALS (simp_tac (HOL_ss addsimps [@{thm fst_conv}, @{thm snd_conv}]));
   145           in (map (fn prop => Skip_Proof.prove lthy [v] [] prop tac) eqs, lthy) end;
   146       in
   147         lthy
   148         |> random_aux_primrec aux_eq'
   149         ||>> fold_map Local_Theory.define proj_defs
   150         |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs)
   151       end;
   152 
   153 fun random_aux_specification prfx name eqs lthy =
   154   let
   155     val vs = fold Term.add_free_names ((snd o strip_comb o fst o HOLogic.dest_eq
   156       o HOLogic.dest_Trueprop o hd) eqs) [];
   157     fun mk_proto_eq eq =
   158       let
   159         val (head $ t $ u, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
   160       in ((HOLogic.mk_Trueprop o HOLogic.mk_eq) (head, lambda t (lambda u rhs))) end;
   161     val proto_eqs = map mk_proto_eq eqs;
   162     fun prove_simps proto_simps lthy =
   163       let
   164         val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
   165         val tac = ALLGOALS (Proof_Context.fact_tac ext_simps);
   166       in (map (fn prop => Skip_Proof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
   167     val b = Binding.conceal (Binding.qualify true prfx
   168       (Binding.qualify true name (Binding.name "simps")));
   169   in
   170     lthy
   171     |> random_aux_primrec_multi (name ^ prfx) proto_eqs
   172     |-> (fn proto_simps => prove_simps proto_simps)
   173     |-> (fn simps => Local_Theory.note
   174       ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K)
   175           [Simplifier.simp_add, Nitpick_Simps.add]), simps))
   176     |> snd
   177   end
   178 
   179 
   180 (* constructing random instances on datatypes *)
   181 
   182 val random_auxN = "random_aux";
   183 
   184 fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
   185   let
   186     val mk_const = curry (Sign.mk_const thy);
   187     val random_auxsN = map (prefix (random_auxN ^ "_")) (names @ auxnames);
   188     val rTs = Ts @ Us;
   189     fun random_resultT T = @{typ Random.seed}
   190       --> HOLogic.mk_prodT (termifyT T,@{typ Random.seed});
   191     val pTs = map random_resultT rTs;
   192     fun sizeT T = @{typ code_numeral} --> @{typ code_numeral} --> T;
   193     val random_auxT = sizeT o random_resultT;
   194     val random_auxs = map2 (fn s => fn rT => Free (s, random_auxT rT))
   195       random_auxsN rTs;
   196     fun mk_random_call T = (NONE, (HOLogic.mk_random T size', T));
   197     fun mk_random_aux_call fTs (k, _) (tyco, Ts) =
   198       let
   199         val T = Type (tyco, Ts);
   200         fun mk_random_fun_lift [] t = t
   201           | mk_random_fun_lift (fT :: fTs) t =
   202               mk_const @{const_name random_fun_lift} [fTs ---> T, fT] $
   203                 mk_random_fun_lift fTs t;
   204         val t = mk_random_fun_lift fTs (nth random_auxs k $ size_pred $ size');
   205         val size = Option.map snd (Datatype_Aux.find_shortest_path descr k)
   206           |> the_default 0;
   207       in (SOME size, (t, fTs ---> T)) end;
   208     val tss = Datatype_Aux.interpret_construction descr vs
   209       { atyp = mk_random_call, dtyp = mk_random_aux_call };
   210     fun mk_consexpr simpleT (c, xs) =
   211       let
   212         val (ks, simple_tTs) = split_list xs;
   213         val T = termifyT simpleT;
   214         val tTs = (map o apsnd) termifyT simple_tTs;
   215         val is_rec = exists is_some ks;
   216         val k = fold (fn NONE => I | SOME k => Integer.max k) ks 0;
   217         val vs = Name.invent_names Name.context "x" (map snd simple_tTs);
   218         val tc = HOLogic.mk_return T @{typ Random.seed}
   219           (HOLogic.mk_valtermify_app c vs simpleT);
   220         val t = HOLogic.mk_ST
   221           (map2 (fn (t, _) => fn (v, T') => ((t, @{typ Random.seed}), SOME ((v, termifyT T')))) tTs vs)
   222             tc @{typ Random.seed} (SOME T, @{typ Random.seed});
   223         val tk = if is_rec
   224           then if k = 0 then size
   225             else @{term "Quickcheck.beyond :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
   226              $ HOLogic.mk_number @{typ code_numeral} k $ size
   227           else @{term "1::code_numeral"}
   228       in (is_rec, HOLogic.mk_prod (tk, t)) end;
   229     fun sort_rec xs =
   230       map_filter (fn (true, t) => SOME t | _ =>  NONE) xs
   231       @ map_filter (fn (false, t) => SOME t | _ =>  NONE) xs;
   232     val gen_exprss = tss
   233       |> (map o apfst) Type
   234       |> map (fn (T, cs) => (T, (sort_rec o map (mk_consexpr T)) cs));
   235     fun mk_select (rT, xs) =
   236       mk_const @{const_name Quickcheck.collapse} [@{typ "Random.seed"}, termifyT rT]
   237       $ (mk_const @{const_name Random.select_weight} [random_resultT rT]
   238         $ HOLogic.mk_list (HOLogic.mk_prodT (@{typ code_numeral}, random_resultT rT)) xs)
   239           $ seed;
   240     val auxs_lhss = map (fn t => t $ size $ size' $ seed) random_auxs;
   241     val auxs_rhss = map mk_select gen_exprss;
   242   in (random_auxs, auxs_lhss ~~ auxs_rhss) end;
   243 
   244 fun instantiate_random_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   245   let
   246     val _ = Datatype_Aux.message config "Creating quickcheck generators ...";
   247     val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
   248     fun mk_size_arg k = case Datatype_Aux.find_shortest_path descr k
   249      of SOME (_, l) => if l = 0 then size
   250           else @{term "max :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
   251             $ HOLogic.mk_number @{typ code_numeral} l $ size
   252       | NONE => size;
   253     val (random_auxs, auxs_eqs) = (apsnd o map) mk_prop_eq
   254       (mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us));
   255     val random_defs = map_index (fn (k, T) => mk_prop_eq
   256       (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
   257   in
   258     thy
   259     |> Class.instantiation (tycos, vs, @{sort random})
   260     |> random_aux_specification prfx random_auxN auxs_eqs
   261     |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
   262     |-> (fn random_defs' => fold_map (fn random_def =>
   263           Specification.definition (NONE, (apfst Binding.conceal
   264             Attrib.empty_binding, random_def))) random_defs')
   265     |> snd
   266     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   267   end;
   268 
   269 (** building and compiling generator expressions **)
   270 
   271 (* FIXME just one data slot (record) per program unit *)
   272 
   273 structure Counterexample = Proof_Data
   274 (
   275   type T = unit -> int -> int -> int * int -> term list option * (int * int)
   276   (* FIXME avoid user error with non-user text *)
   277   fun init _ () = error "Counterexample"
   278 );
   279 val put_counterexample = Counterexample.put;
   280 
   281 structure Counterexample_Report = Proof_Data
   282 (
   283   type T = unit -> int -> int -> seed -> (term list option * (bool list * bool)) * seed
   284   (* FIXME avoid user error with non-user text *)
   285   fun init _ () = error "Counterexample_Report"
   286 );
   287 val put_counterexample_report = Counterexample_Report.put;
   288 
   289 val target = "Quickcheck";
   290 
   291 fun mk_generator_expr ctxt (t, eval_terms) =
   292   let  
   293     val thy = Proof_Context.theory_of ctxt
   294     val prop = list_abs_free (Term.add_frees t [], t)
   295     val Ts = (map snd o fst o strip_abs) prop
   296     val bound_max = length Ts - 1;
   297     val bounds = map_index (fn (i, ty) =>
   298       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
   299     val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
   300     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
   301     val check = @{term "If :: bool => term list option => term list option => term list option"}
   302       $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms);
   303     val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"};
   304     fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
   305     fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
   306     fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
   307       liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   308     fun mk_split T = Sign.mk_const thy
   309       (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
   310     fun mk_scomp_split T t t' =
   311       mk_scomp (mk_termtyp T) @{typ "term list option"} @{typ Random.seed} t
   312         (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
   313     fun mk_bindclause (_, _, i, T) = mk_scomp_split T
   314       (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
   315   in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end;
   316 
   317 fun mk_reporting_generator_expr ctxt (t, eval_terms) =
   318   let
   319     val thy = Proof_Context.theory_of ctxt
   320     val prop = list_abs_free (Term.add_frees t [], t)
   321     val Ts = (map snd o fst o strip_abs) prop
   322     val bound_max = length Ts - 1
   323     val bounds = map_index (fn (i, ty) =>
   324       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
   325     val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
   326     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
   327     val (assms, concl) = Quickcheck_Common.strip_imp prop'
   328     val return =
   329       @{term "Pair :: term list option * (bool list * bool) => Random.seed => (term list option * (bool list * bool)) * Random.seed"};
   330     fun mk_assms_report i =
   331       HOLogic.mk_prod (@{term "None :: term list option"},
   332         HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT
   333           (replicate i @{term True} @ replicate (length assms - i) @{term False}),
   334         @{term False}))
   335     fun mk_concl_report b =
   336       HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT (replicate (length assms) @{term True}),
   337         if b then @{term True} else @{term False})
   338     val If =
   339       @{term "If :: bool => term list option * (bool list * bool) => term list option * (bool list * bool) => term list option * (bool list * bool)"}
   340     val concl_check = If $ concl $
   341       HOLogic.mk_prod (@{term "None :: term list option"}, mk_concl_report true) $
   342       HOLogic.mk_prod (@{term "Some :: term list  => term list option"} $ terms, mk_concl_report false)
   343     val check = fold_rev (fn (i, assm) => fn t => If $ assm $ t $ mk_assms_report i)
   344       (map_index I assms) concl_check
   345     fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
   346     fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
   347     fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
   348       liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   349     fun mk_split T = Sign.mk_const thy
   350       (@{const_name prod_case}, [T, @{typ "unit => term"},
   351         liftT @{typ "term list option * (bool list * bool)"} @{typ Random.seed}]);
   352     fun mk_scomp_split T t t' =
   353       mk_scomp (mk_termtyp T) @{typ "term list option * (bool list * bool)"} @{typ Random.seed} t
   354         (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
   355     fun mk_bindclause (_, _, i, T) = mk_scomp_split T
   356       (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
   357   in
   358     Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
   359   end
   360 
   361 val mk_parametric_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
   362   ((mk_generator_expr, 
   363     absdummy (@{typ code_numeral}, @{term "Pair None :: Random.seed => term list option * Random.seed"})),
   364     @{typ "code_numeral => Random.seed => term list option * Random.seed"})
   365 
   366 val mk_parametric_reporting_generator_expr = Quickcheck_Common.gen_mk_parametric_generator_expr 
   367   ((mk_reporting_generator_expr,
   368     absdummy (@{typ code_numeral},
   369       @{term "Pair (None, ([], False)) :: Random.seed => (term list option * (bool list * bool)) * Random.seed"})),
   370     @{typ "code_numeral => Random.seed => (term list option * (bool list * bool)) * Random.seed"})
   371     
   372     
   373 (* single quickcheck report *)
   374 
   375 datatype single_report = Run of bool list * bool | MatchExc
   376 
   377 fun collect_single_report single_report
   378     (Quickcheck.Report {iterations = iterations, raised_match_errors = raised_match_errors,
   379     satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
   380   case single_report
   381   of MatchExc =>
   382     Quickcheck.Report {iterations = iterations + 1, raised_match_errors = raised_match_errors + 1,
   383       satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}
   384    | Run (assms, concl) =>
   385     Quickcheck.Report {iterations = iterations + 1, raised_match_errors = raised_match_errors,
   386       satisfied_assms =
   387         map2 (fn b => fn s => if b then s + 1 else s) assms
   388          (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
   389       positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
   390 
   391 val empty_report = Quickcheck.Report { iterations = 0, raised_match_errors = 0,
   392   satisfied_assms = [], positive_concl_tests = 0 }
   393     
   394 fun compile_generator_expr ctxt ts =
   395   let
   396     val thy = Proof_Context.theory_of ctxt
   397     val iterations = Config.get ctxt Quickcheck.iterations
   398   in
   399     if Config.get ctxt Quickcheck.report then
   400       let
   401         val t' = mk_parametric_reporting_generator_expr ctxt ts;
   402         val compile = Code_Runtime.dynamic_value_strict
   403           (Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
   404           thy (SOME target) (fn proc => fn g => fn c => fn s => g c s #>> (apfst o Option.map o map) proc) t' [];
   405         fun single_tester c s = compile c s |> Random_Engine.run
   406         fun iterate_and_collect (card, size) 0 report = (NONE, report)
   407           | iterate_and_collect (card, size) j report =
   408             let
   409               val (test_result, single_report) = apsnd Run (single_tester card size) handle Match => 
   410                 (if Config.get ctxt Quickcheck.quiet then ()
   411                  else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
   412               val report = collect_single_report single_report report
   413             in
   414               case test_result of NONE => iterate_and_collect (card, size) (j - 1) report
   415                 | SOME q => (SOME q, report)
   416             end
   417       in
   418         fn [card, size] => apsnd SOME (iterate_and_collect (card, size) iterations empty_report)
   419       end
   420     else
   421       let
   422         val t' = mk_parametric_generator_expr ctxt ts;
   423         val compile = Code_Runtime.dynamic_value_strict
   424           (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
   425           thy (SOME target) (fn proc => fn g => fn c => fn s => g c s #>> (Option.map o map) proc) t' [];
   426         fun single_tester c s = compile c s |> Random_Engine.run
   427         fun iterate (card, size) 0 = NONE
   428           | iterate (card, size) j =
   429             let
   430               val result = single_tester card size handle Match => 
   431                 (if Config.get ctxt Quickcheck.quiet then ()
   432                  else warning "Exception Match raised during quickcheck"; NONE)
   433             in
   434               case result of NONE => iterate (card, size) (j - 1) | SOME q => SOME q
   435             end
   436       in
   437         fn [card, size] => (rpair NONE (iterate (card, size) iterations))
   438       end
   439   end;
   440 
   441 val test_goals = Quickcheck.generator_test_goal_terms;
   442   
   443 (** setup **)
   444 
   445 val setup =
   446   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   447     (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
   448   #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
   449   #> Context.theory_map (Quickcheck.add_generator ("random", compile_generator_expr))
   450   #> Context.theory_map (Quickcheck.add_tester ("random", test_goals));
   451 
   452 end;