renaming smallvalue_generators.ML to exhaustive_generators.ML
authorbulwahn
Fri Mar 11 15:21:13 2011 +0100 (2011-03-11)
changeset 41917caa650526f98
parent 41916 80060d5f864a
child 41918 d2ab869f8b0b
renaming smallvalue_generators.ML to exhaustive_generators.ML
src/HOL/Tools/exhaustive_generators.ML
src/HOL/Tools/smallvalue_generators.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/exhaustive_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     1.3 @@ -0,0 +1,412 @@
     1.4 +(*  Title:      HOL/Tools/smallvalue_generators.ML
     1.5 +    Author:     Lukas Bulwahn, TU Muenchen
     1.6 +
     1.7 +Generators for small values for various types.
     1.8 +*)
     1.9 +
    1.10 +signature SMALLVALUE_GENERATORS =
    1.11 +sig
    1.12 +  val compile_generator_expr:
    1.13 +    Proof.context -> term -> int -> term list option * Quickcheck.report option
    1.14 +  val compile_generator_exprs:
    1.15 +    Proof.context -> term list -> (int -> term list option) list
    1.16 +  val put_counterexample: (unit -> int -> term list option)
    1.17 +    -> Proof.context -> Proof.context
    1.18 +  val put_counterexample_batch: (unit -> (int -> term list option) list)
    1.19 +    -> Proof.context -> Proof.context
    1.20 +  val smart_quantifier : bool Config.T;
    1.21 +  val quickcheck_pretty : bool Config.T;
    1.22 +  val setup: theory -> theory
    1.23 +end;
    1.24 +
    1.25 +structure Smallvalue_Generators : SMALLVALUE_GENERATORS =
    1.26 +struct
    1.27 +
    1.28 +(* static options *)
    1.29 +
    1.30 +val define_foundationally = false
    1.31 +
    1.32 +(* dynamic options *)
    1.33 +
    1.34 +val (smart_quantifier, setup_smart_quantifier) =
    1.35 +  Attrib.config_bool "quickcheck_smart_quantifier" (K true)
    1.36 +
    1.37 +val (quickcheck_pretty, setup_quickcheck_pretty) =
    1.38 +  Attrib.config_bool "quickcheck_pretty" (K true)
    1.39 + 
    1.40 +(** general term functions **)
    1.41 +
    1.42 +fun mk_measure f =
    1.43 +  let
    1.44 +    val Type ("fun", [T, @{typ nat}]) = fastype_of f 
    1.45 +  in
    1.46 +    Const (@{const_name Wellfounded.measure},
    1.47 +      (T --> @{typ nat}) --> HOLogic.mk_prodT (T, T) --> @{typ bool})
    1.48 +    $ f
    1.49 +  end
    1.50 +
    1.51 +fun mk_sumcases rT f (Type (@{type_name Sum_Type.sum}, [TL, TR])) =
    1.52 +  let
    1.53 +    val lt = mk_sumcases rT f TL
    1.54 +    val rt = mk_sumcases rT f TR
    1.55 +  in
    1.56 +    SumTree.mk_sumcase TL TR rT lt rt
    1.57 +  end
    1.58 +  | mk_sumcases _ f T = f T
    1.59 +
    1.60 +fun mk_undefined T = Const(@{const_name undefined}, T)
    1.61 +  
    1.62 +
    1.63 +(** abstract syntax **)
    1.64 +
    1.65 +fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
    1.66 +
    1.67 +val size = @{term "i :: code_numeral"}
    1.68 +val size_pred = @{term "(i :: code_numeral) - 1"}
    1.69 +val size_ge_zero = @{term "(i :: code_numeral) > 0"}
    1.70 +fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
    1.71 +
    1.72 +fun mk_none_continuation (x, y) =
    1.73 +  let
    1.74 +    val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
    1.75 +  in
    1.76 +    Const (@{const_name "Smallcheck.orelse"}, T --> T --> T)
    1.77 +      $ x $ y
    1.78 +  end
    1.79 +
    1.80 +(** datatypes **)
    1.81 +
    1.82 +(* constructing smallvalue generator instances on datatypes *)
    1.83 +
    1.84 +exception FUNCTION_TYPE;
    1.85 +
    1.86 +val smallN = "small";
    1.87 +
    1.88 +fun smallT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ code_numeral}
    1.89 +  --> @{typ "Code_Evaluation.term list option"}
    1.90 +
    1.91 +val full_smallN = "full_small";
    1.92 +
    1.93 +fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    1.94 +  --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
    1.95 +
    1.96 +fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    1.97 +  --> @{typ "Code_Evaluation.term list option"}
    1.98 +
    1.99 +fun mk_equations thy descr vs tycos smalls (Ts, Us) =
   1.100 +  let
   1.101 +    fun mk_small_call T =
   1.102 +      let
   1.103 +        val small = Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)        
   1.104 +      in
   1.105 +        (T, (fn t => small $
   1.106 +          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   1.107 +          $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
   1.108 +      end
   1.109 +    fun mk_small_aux_call fTs (k, _) (tyco, Ts) =
   1.110 +      let
   1.111 +        val T = Type (tyco, Ts)
   1.112 +        val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   1.113 +        val small = nth smalls k
   1.114 +      in
   1.115 +       (T, (fn t => small $
   1.116 +          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   1.117 +            $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))  
   1.118 +      end
   1.119 +    fun mk_consexpr simpleT (c, xs) =
   1.120 +      let
   1.121 +        val (Ts, fns) = split_list xs
   1.122 +        val constr = Const (c, Ts ---> simpleT)
   1.123 +        val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
   1.124 +        val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
   1.125 +        val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
   1.126 +        val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
   1.127 +        val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
   1.128 +          bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
   1.129 +        val start_term = test_function simpleT $ 
   1.130 +        (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
   1.131 +          $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
   1.132 +      in fold_rev (fn f => fn t => f t) fns start_term end
   1.133 +    fun mk_rhs exprs =
   1.134 +        @{term "If :: bool => term list option => term list option => term list option"}
   1.135 +            $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
   1.136 +    val rhss =
   1.137 +      Datatype_Aux.interpret_construction descr vs
   1.138 +        { atyp = mk_small_call, dtyp = mk_small_aux_call }
   1.139 +      |> (map o apfst) Type
   1.140 +      |> map (fn (T, cs) => map (mk_consexpr T) cs)
   1.141 +      |> map mk_rhs
   1.142 +    val lhss = map2 (fn t => fn T => t $ test_function T $ size) smalls (Ts @ Us);
   1.143 +    val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
   1.144 +  in
   1.145 +    eqs
   1.146 +  end
   1.147 +
   1.148 +(* foundational definition with the function package *)
   1.149 +
   1.150 +val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
   1.151 +
   1.152 +fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
   1.153 +    Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
   1.154 +
   1.155 +fun mk_termination_measure T =
   1.156 +  let
   1.157 +    val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
   1.158 +  in
   1.159 +    mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
   1.160 +  end
   1.161 +
   1.162 +fun termination_tac ctxt = 
   1.163 +  Function_Relation.relation_tac ctxt mk_termination_measure 1
   1.164 +  THEN rtac @{thm wf_measure} 1
   1.165 +  THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
   1.166 +    (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
   1.167 +     @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
   1.168 +
   1.169 +fun pat_completeness_auto ctxt =
   1.170 +  Pat_Completeness.pat_completeness_tac ctxt 1
   1.171 +  THEN auto_tac (clasimpset_of ctxt)    
   1.172 +
   1.173 +
   1.174 +(* creating the instances *)
   1.175 +
   1.176 +fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   1.177 +  let
   1.178 +    val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
   1.179 +    val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
   1.180 +  in
   1.181 +    thy
   1.182 +    |> Class.instantiation (tycos, vs, @{sort full_small})
   1.183 +    |> (if define_foundationally then
   1.184 +      let
   1.185 +        val smalls = map2 (fn name => fn T => Free (name, full_smallT T)) smallsN (Ts @ Us)
   1.186 +        val eqs = mk_equations thy descr vs tycos smalls (Ts, Us)
   1.187 +      in
   1.188 +        Function.add_function
   1.189 +          (map (fn (name, T) =>
   1.190 +              Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T)))
   1.191 +                (smallsN ~~ (Ts @ Us)))
   1.192 +            (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs)
   1.193 +          Function_Common.default_config pat_completeness_auto
   1.194 +        #> snd
   1.195 +        #> Local_Theory.restore
   1.196 +        #> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
   1.197 +        #> snd
   1.198 +      end
   1.199 +    else
   1.200 +      fold_map (fn (name, T) => Local_Theory.define
   1.201 +          ((Binding.conceal (Binding.name name), NoSyn),
   1.202 +            (apfst Binding.conceal Attrib.empty_binding, mk_undefined (full_smallT T)))
   1.203 +        #> apfst fst) (smallsN ~~ (Ts @ Us))
   1.204 +      #> (fn (smalls, lthy) =>
   1.205 +        let
   1.206 +          val eqs_t = mk_equations thy descr vs tycos smalls (Ts, Us)
   1.207 +          val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
   1.208 +            (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
   1.209 +        in
   1.210 +          fold (fn (name, eq) => Local_Theory.note
   1.211 +          ((Binding.conceal (Binding.qualify true prfx
   1.212 +             (Binding.qualify true name (Binding.name "simps"))),
   1.213 +             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
   1.214 +               [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (smallsN ~~ eqs) lthy
   1.215 +        end))
   1.216 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   1.217 +  end handle FUNCTION_TYPE =>
   1.218 +    (Datatype_Aux.message config
   1.219 +      "Creation of smallvalue generators failed because the datatype contains a function type";
   1.220 +    thy)
   1.221 +
   1.222 +(** building and compiling generator expressions **)
   1.223 +
   1.224 +structure Counterexample = Proof_Data
   1.225 +(
   1.226 +  type T = unit -> int -> term list option
   1.227 +  (* FIXME avoid user error with non-user text *)
   1.228 +  fun init _ () = error "Counterexample"
   1.229 +);
   1.230 +val put_counterexample = Counterexample.put;
   1.231 +
   1.232 +structure Counterexample_Batch = Proof_Data
   1.233 +(
   1.234 +  type T = unit -> (int -> term list option) list
   1.235 +  (* FIXME avoid user error with non-user text *)
   1.236 +  fun init _ () = error "Counterexample"
   1.237 +);
   1.238 +val put_counterexample_batch = Counterexample_Batch.put;
   1.239 +
   1.240 +val target = "Quickcheck";
   1.241 +
   1.242 +fun mk_smart_generator_expr ctxt t =
   1.243 +  let
   1.244 +    val thy = ProofContext.theory_of ctxt
   1.245 +    val ((vnames, Ts), t') = apfst split_list (strip_abs t)
   1.246 +    val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt
   1.247 +    val (names, ctxt'') = Variable.variant_fixes vnames ctxt'
   1.248 +    val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") vnames) ctxt''
   1.249 +    val depth = Free (depth_name, @{typ code_numeral})
   1.250 +    val frees = map2 (curry Free) names Ts
   1.251 +    val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names 
   1.252 +    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
   1.253 +      | strip_imp A = ([], A)
   1.254 +    val (assms, concl) = strip_imp (subst_bounds (rev frees, t'))
   1.255 +    val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
   1.256 +    fun mk_small_closure (free as Free (_, T), term_var) t =
   1.257 +      if Sign.of_sort thy (T, @{sort enum}) then
   1.258 +        Const (@{const_name "Smallcheck.check_all_class.check_all"}, check_allT T)
   1.259 +          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   1.260 +            $ lambda free (lambda term_var t))
   1.261 +      else
   1.262 +        Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
   1.263 +          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   1.264 +            $ lambda free (lambda term_var t)) $ depth
   1.265 +    fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
   1.266 +    val none_t = @{term "None :: term list option"}
   1.267 +    fun mk_safe_if (cond, then_t, else_t) =
   1.268 +      @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
   1.269 +        (@{term "If :: bool => term list option => term list option => term list option"}
   1.270 +        $ cond $ then_t $ else_t) $ none_t;
   1.271 +    fun mk_test_term bound_vars assms =
   1.272 +      let
   1.273 +        fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
   1.274 +        val (vars, check) =
   1.275 +          case assms of [] =>
   1.276 +            (vars_of concl, (concl, none_t, @{term "Some :: term list => term list option"} $ terms))
   1.277 +          | assm :: assms =>
   1.278 +            (vars_of assm, (assm, mk_test_term (union (op =) (vars_of assm) bound_vars) assms, none_t))
   1.279 +      in
   1.280 +        fold_rev mk_small_closure (map lookup vars) (mk_safe_if check)
   1.281 +      end
   1.282 +  in lambda depth (mk_test_term [] assms) end
   1.283 +
   1.284 +fun mk_generator_expr ctxt t =
   1.285 +  let
   1.286 +    val Ts = (map snd o fst o strip_abs) t;
   1.287 +    val thy = ProofContext.theory_of ctxt
   1.288 +    val bound_max = length Ts - 1;
   1.289 +    val bounds = map_index (fn (i, ty) =>
   1.290 +      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
   1.291 +    val result = list_comb (t, map (fn (i, _, _, _) => Bound i) bounds);
   1.292 +    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
   1.293 +    val check =
   1.294 +      @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
   1.295 +        (@{term "If :: bool => term list option => term list option => term list option"}
   1.296 +        $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms))
   1.297 +      $ @{term "None :: term list option"};
   1.298 +    fun mk_small_closure (_, _, i, T) t =
   1.299 +      Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
   1.300 +        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   1.301 +        $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
   1.302 +  in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
   1.303 +
   1.304 +(** post-processing of function terms **)
   1.305 +
   1.306 +fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
   1.307 +  | dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
   1.308 +
   1.309 +fun mk_fun_upd T1 T2 (t1, t2) t = 
   1.310 +  Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
   1.311 +
   1.312 +fun dest_fun_upds t =
   1.313 +  case try dest_fun_upd t of
   1.314 +    NONE =>
   1.315 +      (case t of
   1.316 +        Abs (_, _, _) => ([], t) 
   1.317 +      | _ => raise TERM ("dest_fun_upds", [t]))
   1.318 +  | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)
   1.319 +
   1.320 +fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
   1.321 +
   1.322 +fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
   1.323 +  | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
   1.324 +  | make_set T1 ((t1, @{const True}) :: tps) =
   1.325 +    Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
   1.326 +      $ t1 $ (make_set T1 tps)
   1.327 +  | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
   1.328 +
   1.329 +fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool})
   1.330 +  | make_coset T tps = 
   1.331 +    let
   1.332 +      val U = T --> @{typ bool}
   1.333 +      fun invert @{const False} = @{const True}
   1.334 +        | invert @{const True} = @{const False}
   1.335 +    in
   1.336 +      Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U)
   1.337 +        $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
   1.338 +    end
   1.339 +
   1.340 +fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
   1.341 +  | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
   1.342 +  | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
   1.343 +  
   1.344 +fun post_process_term t =
   1.345 +  let
   1.346 +    fun map_Abs f t =
   1.347 +      case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
   1.348 +    fun process_args t = case strip_comb t of
   1.349 +      (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
   1.350 +  in
   1.351 +    case fastype_of t of
   1.352 +      Type (@{type_name fun}, [T1, T2]) =>
   1.353 +        (case try dest_fun_upds t of
   1.354 +          SOME (tps, t) =>
   1.355 +            (map (pairself post_process_term) tps, map_Abs post_process_term t)
   1.356 +            |> (case T2 of
   1.357 +              @{typ bool} => 
   1.358 +                (case t of
   1.359 +                   Abs(_, _, @{const True}) => fst #> rev #> make_set T1
   1.360 +                 | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1
   1.361 +                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
   1.362 +                 | _ => raise TERM ("post_process_term", [t]))
   1.363 +            | Type (@{type_name option}, _) =>
   1.364 +                (case t of
   1.365 +                  Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2
   1.366 +                | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
   1.367 +                | _ => make_fun_upds T1 T2) 
   1.368 +            | _ => make_fun_upds T1 T2)
   1.369 +        | NONE => process_args t)
   1.370 +    | _ => process_args t
   1.371 +  end
   1.372 +
   1.373 +(** generator compiliation **)
   1.374 +
   1.375 +fun compile_generator_expr ctxt t =
   1.376 +  let
   1.377 +    val thy = ProofContext.theory_of ctxt
   1.378 +    val t' =
   1.379 +      (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
   1.380 +        ctxt t;
   1.381 +    val compile = Code_Runtime.dynamic_value_strict
   1.382 +      (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
   1.383 +      thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
   1.384 +  in
   1.385 +    fn size => rpair NONE (compile size |> 
   1.386 +      (if Config.get ctxt quickcheck_pretty then Option.map (map post_process_term) else I))
   1.387 +  end;
   1.388 +
   1.389 +fun compile_generator_exprs ctxt ts =
   1.390 +  let
   1.391 +    val thy = ProofContext.theory_of ctxt
   1.392 +    val mk_generator_expr =
   1.393 +      if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr
   1.394 +    val ts' = map (mk_generator_expr ctxt) ts;
   1.395 +    val compiles = Code_Runtime.dynamic_value_strict
   1.396 +      (Counterexample_Batch.get, put_counterexample_batch,
   1.397 +        "Smallvalue_Generators.put_counterexample_batch")
   1.398 +      thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
   1.399 +      (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') [];
   1.400 +  in
   1.401 +    map (fn compile => fn size => compile size |> Option.map (map post_process_term)) compiles
   1.402 +  end;
   1.403 +  
   1.404 +  
   1.405 +(** setup **)
   1.406 +
   1.407 +val setup =
   1.408 +  Datatype.interpretation
   1.409 +    (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
   1.410 +  #> setup_smart_quantifier
   1.411 +  #> setup_quickcheck_pretty
   1.412 +  #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
   1.413 +  #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs));
   1.414 +
   1.415 +end;
     2.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,412 +0,0 @@
     2.4 -(*  Title:      HOL/Tools/smallvalue_generators.ML
     2.5 -    Author:     Lukas Bulwahn, TU Muenchen
     2.6 -
     2.7 -Generators for small values for various types.
     2.8 -*)
     2.9 -
    2.10 -signature SMALLVALUE_GENERATORS =
    2.11 -sig
    2.12 -  val compile_generator_expr:
    2.13 -    Proof.context -> term -> int -> term list option * Quickcheck.report option
    2.14 -  val compile_generator_exprs:
    2.15 -    Proof.context -> term list -> (int -> term list option) list
    2.16 -  val put_counterexample: (unit -> int -> term list option)
    2.17 -    -> Proof.context -> Proof.context
    2.18 -  val put_counterexample_batch: (unit -> (int -> term list option) list)
    2.19 -    -> Proof.context -> Proof.context
    2.20 -  val smart_quantifier : bool Config.T;
    2.21 -  val quickcheck_pretty : bool Config.T;
    2.22 -  val setup: theory -> theory
    2.23 -end;
    2.24 -
    2.25 -structure Smallvalue_Generators : SMALLVALUE_GENERATORS =
    2.26 -struct
    2.27 -
    2.28 -(* static options *)
    2.29 -
    2.30 -val define_foundationally = false
    2.31 -
    2.32 -(* dynamic options *)
    2.33 -
    2.34 -val (smart_quantifier, setup_smart_quantifier) =
    2.35 -  Attrib.config_bool "quickcheck_smart_quantifier" (K true)
    2.36 -
    2.37 -val (quickcheck_pretty, setup_quickcheck_pretty) =
    2.38 -  Attrib.config_bool "quickcheck_pretty" (K true)
    2.39 - 
    2.40 -(** general term functions **)
    2.41 -
    2.42 -fun mk_measure f =
    2.43 -  let
    2.44 -    val Type ("fun", [T, @{typ nat}]) = fastype_of f 
    2.45 -  in
    2.46 -    Const (@{const_name Wellfounded.measure},
    2.47 -      (T --> @{typ nat}) --> HOLogic.mk_prodT (T, T) --> @{typ bool})
    2.48 -    $ f
    2.49 -  end
    2.50 -
    2.51 -fun mk_sumcases rT f (Type (@{type_name Sum_Type.sum}, [TL, TR])) =
    2.52 -  let
    2.53 -    val lt = mk_sumcases rT f TL
    2.54 -    val rt = mk_sumcases rT f TR
    2.55 -  in
    2.56 -    SumTree.mk_sumcase TL TR rT lt rt
    2.57 -  end
    2.58 -  | mk_sumcases _ f T = f T
    2.59 -
    2.60 -fun mk_undefined T = Const(@{const_name undefined}, T)
    2.61 -  
    2.62 -
    2.63 -(** abstract syntax **)
    2.64 -
    2.65 -fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
    2.66 -
    2.67 -val size = @{term "i :: code_numeral"}
    2.68 -val size_pred = @{term "(i :: code_numeral) - 1"}
    2.69 -val size_ge_zero = @{term "(i :: code_numeral) > 0"}
    2.70 -fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
    2.71 -
    2.72 -fun mk_none_continuation (x, y) =
    2.73 -  let
    2.74 -    val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
    2.75 -  in
    2.76 -    Const (@{const_name "Smallcheck.orelse"}, T --> T --> T)
    2.77 -      $ x $ y
    2.78 -  end
    2.79 -
    2.80 -(** datatypes **)
    2.81 -
    2.82 -(* constructing smallvalue generator instances on datatypes *)
    2.83 -
    2.84 -exception FUNCTION_TYPE;
    2.85 -
    2.86 -val smallN = "small";
    2.87 -
    2.88 -fun smallT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ code_numeral}
    2.89 -  --> @{typ "Code_Evaluation.term list option"}
    2.90 -
    2.91 -val full_smallN = "full_small";
    2.92 -
    2.93 -fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    2.94 -  --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
    2.95 -
    2.96 -fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    2.97 -  --> @{typ "Code_Evaluation.term list option"}
    2.98 -
    2.99 -fun mk_equations thy descr vs tycos smalls (Ts, Us) =
   2.100 -  let
   2.101 -    fun mk_small_call T =
   2.102 -      let
   2.103 -        val small = Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)        
   2.104 -      in
   2.105 -        (T, (fn t => small $
   2.106 -          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   2.107 -          $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
   2.108 -      end
   2.109 -    fun mk_small_aux_call fTs (k, _) (tyco, Ts) =
   2.110 -      let
   2.111 -        val T = Type (tyco, Ts)
   2.112 -        val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   2.113 -        val small = nth smalls k
   2.114 -      in
   2.115 -       (T, (fn t => small $
   2.116 -          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   2.117 -            $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))  
   2.118 -      end
   2.119 -    fun mk_consexpr simpleT (c, xs) =
   2.120 -      let
   2.121 -        val (Ts, fns) = split_list xs
   2.122 -        val constr = Const (c, Ts ---> simpleT)
   2.123 -        val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
   2.124 -        val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
   2.125 -        val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
   2.126 -        val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
   2.127 -        val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
   2.128 -          bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
   2.129 -        val start_term = test_function simpleT $ 
   2.130 -        (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
   2.131 -          $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
   2.132 -      in fold_rev (fn f => fn t => f t) fns start_term end
   2.133 -    fun mk_rhs exprs =
   2.134 -        @{term "If :: bool => term list option => term list option => term list option"}
   2.135 -            $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
   2.136 -    val rhss =
   2.137 -      Datatype_Aux.interpret_construction descr vs
   2.138 -        { atyp = mk_small_call, dtyp = mk_small_aux_call }
   2.139 -      |> (map o apfst) Type
   2.140 -      |> map (fn (T, cs) => map (mk_consexpr T) cs)
   2.141 -      |> map mk_rhs
   2.142 -    val lhss = map2 (fn t => fn T => t $ test_function T $ size) smalls (Ts @ Us);
   2.143 -    val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
   2.144 -  in
   2.145 -    eqs
   2.146 -  end
   2.147 -
   2.148 -(* foundational definition with the function package *)
   2.149 -
   2.150 -val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
   2.151 -
   2.152 -fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
   2.153 -    Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
   2.154 -
   2.155 -fun mk_termination_measure T =
   2.156 -  let
   2.157 -    val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
   2.158 -  in
   2.159 -    mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
   2.160 -  end
   2.161 -
   2.162 -fun termination_tac ctxt = 
   2.163 -  Function_Relation.relation_tac ctxt mk_termination_measure 1
   2.164 -  THEN rtac @{thm wf_measure} 1
   2.165 -  THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
   2.166 -    (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
   2.167 -     @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
   2.168 -
   2.169 -fun pat_completeness_auto ctxt =
   2.170 -  Pat_Completeness.pat_completeness_tac ctxt 1
   2.171 -  THEN auto_tac (clasimpset_of ctxt)    
   2.172 -
   2.173 -
   2.174 -(* creating the instances *)
   2.175 -
   2.176 -fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   2.177 -  let
   2.178 -    val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
   2.179 -    val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
   2.180 -  in
   2.181 -    thy
   2.182 -    |> Class.instantiation (tycos, vs, @{sort full_small})
   2.183 -    |> (if define_foundationally then
   2.184 -      let
   2.185 -        val smalls = map2 (fn name => fn T => Free (name, full_smallT T)) smallsN (Ts @ Us)
   2.186 -        val eqs = mk_equations thy descr vs tycos smalls (Ts, Us)
   2.187 -      in
   2.188 -        Function.add_function
   2.189 -          (map (fn (name, T) =>
   2.190 -              Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T)))
   2.191 -                (smallsN ~~ (Ts @ Us)))
   2.192 -            (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs)
   2.193 -          Function_Common.default_config pat_completeness_auto
   2.194 -        #> snd
   2.195 -        #> Local_Theory.restore
   2.196 -        #> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
   2.197 -        #> snd
   2.198 -      end
   2.199 -    else
   2.200 -      fold_map (fn (name, T) => Local_Theory.define
   2.201 -          ((Binding.conceal (Binding.name name), NoSyn),
   2.202 -            (apfst Binding.conceal Attrib.empty_binding, mk_undefined (full_smallT T)))
   2.203 -        #> apfst fst) (smallsN ~~ (Ts @ Us))
   2.204 -      #> (fn (smalls, lthy) =>
   2.205 -        let
   2.206 -          val eqs_t = mk_equations thy descr vs tycos smalls (Ts, Us)
   2.207 -          val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
   2.208 -            (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
   2.209 -        in
   2.210 -          fold (fn (name, eq) => Local_Theory.note
   2.211 -          ((Binding.conceal (Binding.qualify true prfx
   2.212 -             (Binding.qualify true name (Binding.name "simps"))),
   2.213 -             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
   2.214 -               [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (smallsN ~~ eqs) lthy
   2.215 -        end))
   2.216 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   2.217 -  end handle FUNCTION_TYPE =>
   2.218 -    (Datatype_Aux.message config
   2.219 -      "Creation of smallvalue generators failed because the datatype contains a function type";
   2.220 -    thy)
   2.221 -
   2.222 -(** building and compiling generator expressions **)
   2.223 -
   2.224 -structure Counterexample = Proof_Data
   2.225 -(
   2.226 -  type T = unit -> int -> term list option
   2.227 -  (* FIXME avoid user error with non-user text *)
   2.228 -  fun init _ () = error "Counterexample"
   2.229 -);
   2.230 -val put_counterexample = Counterexample.put;
   2.231 -
   2.232 -structure Counterexample_Batch = Proof_Data
   2.233 -(
   2.234 -  type T = unit -> (int -> term list option) list
   2.235 -  (* FIXME avoid user error with non-user text *)
   2.236 -  fun init _ () = error "Counterexample"
   2.237 -);
   2.238 -val put_counterexample_batch = Counterexample_Batch.put;
   2.239 -
   2.240 -val target = "Quickcheck";
   2.241 -
   2.242 -fun mk_smart_generator_expr ctxt t =
   2.243 -  let
   2.244 -    val thy = ProofContext.theory_of ctxt
   2.245 -    val ((vnames, Ts), t') = apfst split_list (strip_abs t)
   2.246 -    val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt
   2.247 -    val (names, ctxt'') = Variable.variant_fixes vnames ctxt'
   2.248 -    val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") vnames) ctxt''
   2.249 -    val depth = Free (depth_name, @{typ code_numeral})
   2.250 -    val frees = map2 (curry Free) names Ts
   2.251 -    val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names 
   2.252 -    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
   2.253 -      | strip_imp A = ([], A)
   2.254 -    val (assms, concl) = strip_imp (subst_bounds (rev frees, t'))
   2.255 -    val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
   2.256 -    fun mk_small_closure (free as Free (_, T), term_var) t =
   2.257 -      if Sign.of_sort thy (T, @{sort enum}) then
   2.258 -        Const (@{const_name "Smallcheck.check_all_class.check_all"}, check_allT T)
   2.259 -          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   2.260 -            $ lambda free (lambda term_var t))
   2.261 -      else
   2.262 -        Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
   2.263 -          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   2.264 -            $ lambda free (lambda term_var t)) $ depth
   2.265 -    fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
   2.266 -    val none_t = @{term "None :: term list option"}
   2.267 -    fun mk_safe_if (cond, then_t, else_t) =
   2.268 -      @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
   2.269 -        (@{term "If :: bool => term list option => term list option => term list option"}
   2.270 -        $ cond $ then_t $ else_t) $ none_t;
   2.271 -    fun mk_test_term bound_vars assms =
   2.272 -      let
   2.273 -        fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
   2.274 -        val (vars, check) =
   2.275 -          case assms of [] =>
   2.276 -            (vars_of concl, (concl, none_t, @{term "Some :: term list => term list option"} $ terms))
   2.277 -          | assm :: assms =>
   2.278 -            (vars_of assm, (assm, mk_test_term (union (op =) (vars_of assm) bound_vars) assms, none_t))
   2.279 -      in
   2.280 -        fold_rev mk_small_closure (map lookup vars) (mk_safe_if check)
   2.281 -      end
   2.282 -  in lambda depth (mk_test_term [] assms) end
   2.283 -
   2.284 -fun mk_generator_expr ctxt t =
   2.285 -  let
   2.286 -    val Ts = (map snd o fst o strip_abs) t;
   2.287 -    val thy = ProofContext.theory_of ctxt
   2.288 -    val bound_max = length Ts - 1;
   2.289 -    val bounds = map_index (fn (i, ty) =>
   2.290 -      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
   2.291 -    val result = list_comb (t, map (fn (i, _, _, _) => Bound i) bounds);
   2.292 -    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
   2.293 -    val check =
   2.294 -      @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
   2.295 -        (@{term "If :: bool => term list option => term list option => term list option"}
   2.296 -        $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms))
   2.297 -      $ @{term "None :: term list option"};
   2.298 -    fun mk_small_closure (_, _, i, T) t =
   2.299 -      Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
   2.300 -        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   2.301 -        $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
   2.302 -  in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
   2.303 -
   2.304 -(** post-processing of function terms **)
   2.305 -
   2.306 -fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
   2.307 -  | dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
   2.308 -
   2.309 -fun mk_fun_upd T1 T2 (t1, t2) t = 
   2.310 -  Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
   2.311 -
   2.312 -fun dest_fun_upds t =
   2.313 -  case try dest_fun_upd t of
   2.314 -    NONE =>
   2.315 -      (case t of
   2.316 -        Abs (_, _, _) => ([], t) 
   2.317 -      | _ => raise TERM ("dest_fun_upds", [t]))
   2.318 -  | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)
   2.319 -
   2.320 -fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
   2.321 -
   2.322 -fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
   2.323 -  | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
   2.324 -  | make_set T1 ((t1, @{const True}) :: tps) =
   2.325 -    Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
   2.326 -      $ t1 $ (make_set T1 tps)
   2.327 -  | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
   2.328 -
   2.329 -fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool})
   2.330 -  | make_coset T tps = 
   2.331 -    let
   2.332 -      val U = T --> @{typ bool}
   2.333 -      fun invert @{const False} = @{const True}
   2.334 -        | invert @{const True} = @{const False}
   2.335 -    in
   2.336 -      Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U)
   2.337 -        $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
   2.338 -    end
   2.339 -
   2.340 -fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
   2.341 -  | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
   2.342 -  | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
   2.343 -  
   2.344 -fun post_process_term t =
   2.345 -  let
   2.346 -    fun map_Abs f t =
   2.347 -      case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
   2.348 -    fun process_args t = case strip_comb t of
   2.349 -      (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
   2.350 -  in
   2.351 -    case fastype_of t of
   2.352 -      Type (@{type_name fun}, [T1, T2]) =>
   2.353 -        (case try dest_fun_upds t of
   2.354 -          SOME (tps, t) =>
   2.355 -            (map (pairself post_process_term) tps, map_Abs post_process_term t)
   2.356 -            |> (case T2 of
   2.357 -              @{typ bool} => 
   2.358 -                (case t of
   2.359 -                   Abs(_, _, @{const True}) => fst #> rev #> make_set T1
   2.360 -                 | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1
   2.361 -                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
   2.362 -                 | _ => raise TERM ("post_process_term", [t]))
   2.363 -            | Type (@{type_name option}, _) =>
   2.364 -                (case t of
   2.365 -                  Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2
   2.366 -                | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
   2.367 -                | _ => make_fun_upds T1 T2) 
   2.368 -            | _ => make_fun_upds T1 T2)
   2.369 -        | NONE => process_args t)
   2.370 -    | _ => process_args t
   2.371 -  end
   2.372 -
   2.373 -(** generator compiliation **)
   2.374 -
   2.375 -fun compile_generator_expr ctxt t =
   2.376 -  let
   2.377 -    val thy = ProofContext.theory_of ctxt
   2.378 -    val t' =
   2.379 -      (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
   2.380 -        ctxt t;
   2.381 -    val compile = Code_Runtime.dynamic_value_strict
   2.382 -      (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
   2.383 -      thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
   2.384 -  in
   2.385 -    fn size => rpair NONE (compile size |> 
   2.386 -      (if Config.get ctxt quickcheck_pretty then Option.map (map post_process_term) else I))
   2.387 -  end;
   2.388 -
   2.389 -fun compile_generator_exprs ctxt ts =
   2.390 -  let
   2.391 -    val thy = ProofContext.theory_of ctxt
   2.392 -    val mk_generator_expr =
   2.393 -      if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr
   2.394 -    val ts' = map (mk_generator_expr ctxt) ts;
   2.395 -    val compiles = Code_Runtime.dynamic_value_strict
   2.396 -      (Counterexample_Batch.get, put_counterexample_batch,
   2.397 -        "Smallvalue_Generators.put_counterexample_batch")
   2.398 -      thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
   2.399 -      (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') [];
   2.400 -  in
   2.401 -    map (fn compile => fn size => compile size |> Option.map (map post_process_term)) compiles
   2.402 -  end;
   2.403 -  
   2.404 -  
   2.405 -(** setup **)
   2.406 -
   2.407 -val setup =
   2.408 -  Datatype.interpretation
   2.409 -    (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
   2.410 -  #> setup_smart_quantifier
   2.411 -  #> setup_quickcheck_pretty
   2.412 -  #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
   2.413 -  #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs));
   2.414 -
   2.415 -end;