src/HOL/Tools/Quickcheck/exhaustive_generators.ML
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42316 12635bb655fd
parent 42315 95dfa082065a
child 42325 104472645443
permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
     1 (*  Title:      HOL/Tools/Quickcheck/exhaustive_generators.ML
     2     Author:     Lukas Bulwahn, TU Muenchen
     3 
     4 Exhaustive generators for various types.
     5 *)
     6 
     7 signature EXHAUSTIVE_GENERATORS =
     8 sig
     9   val compile_generator_expr:
    10     Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
    11   val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
    12   val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list
    13   val put_counterexample: (unit -> int -> int -> term list option)
    14     -> Proof.context -> Proof.context
    15   val put_counterexample_batch: (unit -> (int -> term list option) list)
    16     -> Proof.context -> Proof.context
    17   val put_validator_batch: (unit -> (int -> bool) list) -> Proof.context -> Proof.context
    18   exception Counterexample of term list
    19   val smart_quantifier : bool Config.T
    20   val quickcheck_pretty : bool Config.T
    21   val setup: theory -> theory
    22 end;
    23 
    24 structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
    25 struct
    26 
    27 (* basics *)
    28 
    29 (** dynamic options **)
    30 
    31 val (smart_quantifier, setup_smart_quantifier) =
    32   Attrib.config_bool "quickcheck_smart_quantifier" (K true)
    33 
    34 val (fast, setup_fast) =
    35   Attrib.config_bool "quickcheck_fast" (K false)
    36   
    37 val (full_support, setup_full_support) =
    38   Attrib.config_bool "quickcheck_full_support" (K true)
    39 
    40 val (quickcheck_pretty, setup_quickcheck_pretty) =
    41   Attrib.config_bool "quickcheck_pretty" (K true)
    42  
    43 (** general term functions **)
    44 
    45 fun mk_measure f =
    46   let
    47     val Type ("fun", [T, @{typ nat}]) = fastype_of f 
    48   in
    49     Const (@{const_name Wellfounded.measure},
    50       (T --> @{typ nat}) --> HOLogic.mk_prodT (T, T) --> @{typ bool})
    51     $ f
    52   end
    53 
    54 fun mk_sumcases rT f (Type (@{type_name Sum_Type.sum}, [TL, TR])) =
    55   let
    56     val lt = mk_sumcases rT f TL
    57     val rt = mk_sumcases rT f TR
    58   in
    59     SumTree.mk_sumcase TL TR rT lt rt
    60   end
    61   | mk_sumcases _ f T = f T
    62 
    63 (** abstract syntax **)
    64 
    65 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
    66 
    67 val size = @{term "i :: code_numeral"}
    68 val size_pred = @{term "(i :: code_numeral) - 1"}
    69 val size_ge_zero = @{term "(i :: code_numeral) > 0"}
    70 
    71 fun mk_none_continuation (x, y) =
    72   let
    73     val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
    74   in
    75     Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y
    76   end
    77 
    78 fun mk_unit_let (x, y) =
    79   Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ (absdummy (@{typ unit}, y))
    80   
    81 (* handling inductive datatypes *)
    82 
    83 (** constructing generator instances **)
    84 
    85 exception FUNCTION_TYPE;
    86 
    87 exception Counterexample of term list
    88 
    89 val exhaustiveN = "exhaustive";
    90 val full_exhaustiveN = "full_exhaustive";
    91 val fast_exhaustiveN = "fast_exhaustive";
    92 val bounded_forallN = "bounded_forall";
    93 
    94 fun fast_exhaustiveT T = (T --> @{typ unit})
    95   --> @{typ code_numeral} --> @{typ unit}
    96 
    97 fun exhaustiveT T = (T --> @{typ "Code_Evaluation.term list option"})
    98   --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
    99 
   100 fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
   101 
   102 fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
   103   --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
   104 
   105 fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
   106   --> @{typ "Code_Evaluation.term list option"}
   107 
   108 fun mk_equation_terms generics (descr, vs, Ts) =
   109   let
   110     val (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, exhaustives) = generics
   111     val rhss =
   112       Datatype_Aux.interpret_construction descr vs
   113         { atyp = mk_call, dtyp = mk_aux_call }
   114       |> (map o apfst) Type
   115       |> map (fn (T, cs) => map (mk_consexpr T) cs)
   116       |> map mk_rhs
   117     val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives Ts
   118   in
   119     map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
   120   end
   121 
   122 fun gen_mk_call c T =  (T, fn t => c T $ absdummy (T, t) $ size_pred)
   123 
   124 fun gen_mk_aux_call functerms fTs (k, _) (tyco, Ts) =
   125   let
   126     val T = Type (tyco, Ts)
   127     val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   128   in
   129    (T, fn t => nth functerms k $ absdummy (T, t) $ size_pred)
   130   end
   131 
   132 fun gen_mk_consexpr test_function functerms simpleT (c, xs) =
   133   let
   134     val (Ts, fns) = split_list xs
   135     val constr = Const (c, Ts ---> simpleT)
   136     val bounds = map Bound (((length xs) - 1) downto 0)
   137     val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
   138     val start_term = test_function simpleT $ list_comb (constr, bounds)
   139   in fold_rev (fn f => fn t => f t) fns start_term end
   140       
   141 fun mk_fast_equations functerms =
   142   let
   143     fun test_function T = Free ("f", T --> @{typ "unit"})
   144     val mk_call = gen_mk_call (fn T =>
   145       Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"},
   146         fast_exhaustiveT T))
   147     val mk_aux_call = gen_mk_aux_call functerms
   148     val mk_consexpr = gen_mk_consexpr test_function functerms
   149     fun mk_rhs exprs = @{term "If :: bool => unit => unit => unit"}
   150         $ size_ge_zero $ (foldr1 mk_unit_let exprs) $ @{term "()"}
   151   in
   152     mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   153   end
   154 
   155 fun mk_equations functerms =
   156   let
   157     fun test_function T = Free ("f", T --> @{typ "term list option"})
   158     val mk_call = gen_mk_call (fn T =>
   159       Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T))
   160     val mk_aux_call = gen_mk_aux_call functerms
   161     val mk_consexpr = gen_mk_consexpr test_function functerms
   162     fun mk_rhs exprs =
   163       @{term "If :: bool => term list option => term list option => term list option"}
   164           $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
   165   in
   166     mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   167   end
   168 
   169 fun mk_bounded_forall_equations functerms =
   170   let
   171     fun test_function T = Free ("P", T --> @{typ bool})
   172     val mk_call = gen_mk_call (fn T =>
   173       Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"},
   174         bounded_forallT T))
   175     val mk_aux_call = gen_mk_aux_call functerms
   176     val mk_consexpr = gen_mk_consexpr test_function functerms
   177     fun mk_rhs exprs =
   178       @{term "If :: bool => bool => bool => bool"} $ size_ge_zero $
   179         (foldr1 HOLogic.mk_conj exprs) $ @{term "True"}
   180   in
   181     mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   182   end
   183   
   184 fun mk_full_equations functerms =
   185   let
   186     fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
   187     fun mk_call T =
   188       let
   189         val full_exhaustive =
   190           Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
   191             full_exhaustiveT T)
   192       in
   193         (T, (fn t => full_exhaustive $
   194           (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   195           $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
   196       end
   197     fun mk_aux_call fTs (k, _) (tyco, Ts) =
   198       let
   199         val T = Type (tyco, Ts)
   200         val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   201       in
   202         (T, (fn t => nth functerms k $
   203           (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   204             $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
   205       end
   206     fun mk_consexpr simpleT (c, xs) =
   207       let
   208         val (Ts, fns) = split_list xs
   209         val constr = Const (c, Ts ---> simpleT)
   210         val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
   211         val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
   212         val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
   213         val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
   214         val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
   215           bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
   216         val start_term = test_function simpleT $ 
   217         (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
   218           $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
   219       in fold_rev (fn f => fn t => f t) fns start_term end
   220     fun mk_rhs exprs =
   221         @{term "If :: bool => term list option => term list option => term list option"}
   222             $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
   223   in
   224     mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   225   end
   226   
   227 (** foundational definition with the function package **)
   228 
   229 val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
   230 
   231 fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
   232     Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
   233 
   234 fun mk_termination_measure T =
   235   let
   236     val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
   237   in
   238     mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
   239   end
   240 
   241 fun termination_tac ctxt = 
   242   Function_Relation.relation_tac ctxt mk_termination_measure 1
   243   THEN rtac @{thm wf_measure} 1
   244   THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
   245     (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
   246      @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
   247 
   248 (** instantiating generator classes **)
   249   
   250 val contains_recursive_type_under_function_types =
   251   exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
   252     (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false))))
   253     
   254 fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames)
   255     config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   256   if not (contains_recursive_type_under_function_types descr) then
   257     let
   258       val _ = Datatype_Aux.message config ("Creating " ^ name ^ "...")
   259       val fullnames = map (prefix (constprfx ^ "_")) (names @ auxnames)
   260     in
   261       thy
   262       |> Class.instantiation (tycos, vs, sort)
   263       |> Quickcheck_Common.define_functions
   264           (fn functerms => mk_equations functerms (descr, vs, Ts @ Us), NONE)
   265           prfx argnames fullnames (map mk_T (Ts @ Us))
   266       |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   267     end
   268   else
   269     (Datatype_Aux.message config
   270       ("Creation of " ^ name ^ " failed because the datatype is recursive under a function type");
   271     thy)
   272 
   273 val instantiate_bounded_forall_datatype = instantiate_datatype
   274  ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall},
   275    mk_bounded_forall_equations, bounded_forallT, ["P", "i"]);
   276 
   277 val instantiate_fast_exhaustive_datatype = instantiate_datatype 
   278  ("fast exhaustive generators", fast_exhaustiveN, @{sort fast_exhaustive},
   279    mk_fast_equations, fast_exhaustiveT, ["f", "i"])
   280 
   281 val instantiate_exhaustive_datatype = instantiate_datatype  
   282   ("exhaustive generators", exhaustiveN, @{sort full_exhaustive}, mk_equations, exhaustiveT, ["f", "i"])
   283 
   284 val instantiate_full_exhaustive_datatype = instantiate_datatype
   285   ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive},
   286   mk_full_equations, full_exhaustiveT, ["f", "i"])
   287   
   288 (* building and compiling generator expressions *)
   289 
   290 fun mk_fast_generator_expr ctxt (t, eval_terms) =
   291   let
   292     val thy = ProofContext.theory_of ctxt
   293     val ctxt' = Variable.auto_fixes t ctxt
   294     val names = Term.add_free_names t []
   295     val frees = map Free (Term.add_frees t [])
   296     val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
   297     val depth = Free (depth_name, @{typ code_numeral})
   298     val return = @{term "throw_Counterexample :: term list => unit"} $
   299       (HOLogic.mk_list @{typ "term"}
   300         (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
   301     fun mk_exhaustive_closure (free as Free (_, T)) t =
   302       Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"}, fast_exhaustiveT T)
   303         $ lambda free t $ depth
   304     val none_t = @{term "()"}
   305     fun mk_safe_if (cond, then_t, else_t) =
   306       @{term "If :: bool => unit => unit => unit"} $ cond $ then_t $ else_t
   307     fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
   308     fun mk_naive_test_term t =
   309       fold_rev mk_exhaustive_closure frees (mk_safe_if (t, none_t, return)) 
   310     fun mk_smart_test_term' concl bound_vars assms =
   311       let
   312         fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
   313         val (vars, check) =
   314           case assms of [] => (vars_of concl, (concl, none_t, return))
   315             | assm :: assms => (vars_of assm, (assm,
   316                 mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
   317       in
   318         fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
   319       end
   320     fun mk_smart_test_term t =
   321       let
   322         val (assms, concl) = Quickcheck_Common.strip_imp t
   323       in
   324         mk_smart_test_term' concl [] assms
   325       end
   326     val mk_test_term =
   327       if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
   328   in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end
   329 
   330 fun mk_generator_expr ctxt (t, eval_terms) =
   331   let
   332     val thy = ProofContext.theory_of ctxt
   333     val ctxt' = Variable.auto_fixes t ctxt
   334     val names = Term.add_free_names t []
   335     val frees = map Free (Term.add_frees t [])
   336     val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
   337     val depth = Free (depth_name, @{typ code_numeral})
   338     val return = @{term "Some :: term list => term list option"} $
   339       (HOLogic.mk_list @{typ "term"}
   340         (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
   341     fun mk_exhaustive_closure (free as Free (_, T)) t =
   342       Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
   343         $ lambda free t $ depth
   344     val none_t = @{term "None :: term list option"}
   345     fun mk_safe_if (cond, then_t, else_t) =
   346       @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
   347         (@{term "If :: bool => term list option => term list option => term list option"}
   348         $ cond $ then_t $ else_t) $ none_t;
   349     fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
   350     fun mk_naive_test_term t =
   351       fold_rev mk_exhaustive_closure frees (mk_safe_if (t, none_t, return)) 
   352     fun mk_smart_test_term' concl bound_vars assms =
   353       let
   354         fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
   355         val (vars, check) =
   356           case assms of [] => (vars_of concl, (concl, none_t, return))
   357             | assm :: assms => (vars_of assm, (assm,
   358                 mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
   359       in
   360         fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
   361       end
   362     fun mk_smart_test_term t =
   363       let
   364         val (assms, concl) = Quickcheck_Common.strip_imp t
   365       in
   366         mk_smart_test_term' concl [] assms
   367       end
   368     val mk_test_term =
   369       if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
   370   in lambda depth (mk_test_term t) end
   371 
   372 fun mk_full_generator_expr ctxt (t, eval_terms) =
   373   let
   374     val thy = ProofContext.theory_of ctxt
   375     val ctxt' = Variable.auto_fixes t ctxt
   376     val names = Term.add_free_names t []
   377     val frees = map Free (Term.add_frees t [])
   378     val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
   379     val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") names) ctxt''
   380     val depth = Free (depth_name, @{typ code_numeral})
   381     val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
   382     val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
   383     val appendC = @{term "List.append :: term list => term list => term list"}  
   384     val return = @{term "Some :: term list => term list option"} $ (appendC $ terms $
   385       (HOLogic.mk_list @{typ "term"} (map (fn t => HOLogic.mk_term_of (fastype_of t) t) eval_terms)))
   386     fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
   387       if Sign.of_sort thy (T, @{sort enum}) then
   388         Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
   389           $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   390             $ lambda free (lambda term_var t))
   391       else
   392         Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
   393           $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
   394             $ lambda free (lambda term_var t)) $ depth
   395     val none_t = @{term "None :: term list option"}
   396     fun mk_safe_if (cond, then_t, else_t) =
   397       @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
   398         (@{term "If :: bool => term list option => term list option => term list option"}
   399         $ cond $ then_t $ else_t) $ none_t;
   400     fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
   401     fun mk_naive_test_term t =
   402       fold_rev mk_exhaustive_closure (frees ~~ term_vars) (mk_safe_if (t, none_t, return)) 
   403     fun mk_smart_test_term' concl bound_vars assms =
   404       let
   405         fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
   406         val (vars, check) =
   407           case assms of [] => (vars_of concl, (concl, none_t, return))
   408             | assm :: assms => (vars_of assm, (assm,
   409                 mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
   410       in
   411         fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
   412       end
   413     fun mk_smart_test_term t =
   414       let
   415         val (assms, concl) = Quickcheck_Common.strip_imp t
   416       in
   417         mk_smart_test_term' concl [] assms
   418       end
   419     val mk_test_term =
   420       if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
   421   in lambda depth (mk_test_term t) end
   422 
   423 fun mk_parametric_generator_expr mk_generator_expr =
   424   Quickcheck_Common.gen_mk_parametric_generator_expr 
   425     ((mk_generator_expr, absdummy (@{typ "code_numeral"}, @{term "None :: term list option"})),
   426       @{typ "code_numeral => term list option"})
   427 
   428 fun mk_validator_expr ctxt t =
   429   let
   430     fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
   431     val thy = ProofContext.theory_of ctxt
   432     val ctxt' = Variable.auto_fixes t ctxt
   433     val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
   434     val depth = Free (depth_name, @{typ code_numeral})
   435     fun mk_bounded_forall (s, T) t =
   436       Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)
   437         $ lambda (Free (s, T)) t $ depth
   438     fun mk_implies (cond, then_t) =
   439       @{term "If :: bool => bool => bool => bool"} $ cond $ then_t $ @{term True}
   440     fun mk_naive_test_term t = fold_rev mk_bounded_forall (Term.add_frees t []) t 
   441     fun mk_smart_test_term' concl bound_frees assms =
   442       let
   443         fun vars_of t = subtract (op =) bound_frees (Term.add_frees t [])
   444         val (vars, check) =
   445           case assms of [] => (vars_of concl, concl)
   446             | assm :: assms => (vars_of assm, mk_implies (assm,
   447                 mk_smart_test_term' concl (union (op =) (vars_of assm) bound_frees) assms))
   448       in
   449         fold_rev mk_bounded_forall vars check
   450       end
   451     fun mk_smart_test_term t =
   452       let
   453         val (assms, concl) = Quickcheck_Common.strip_imp t
   454       in
   455         mk_smart_test_term' concl [] assms
   456       end
   457     val mk_test_term =
   458       if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term 
   459   in lambda depth (mk_test_term t) end
   460 
   461 
   462 (** generator compiliation **)
   463 
   464 structure Counterexample = Proof_Data
   465 (
   466   type T = unit -> int -> int -> term list option
   467   (* FIXME avoid user error with non-user text *)
   468   fun init _ () = error "Counterexample"
   469 );
   470 val put_counterexample = Counterexample.put;
   471 
   472 structure Counterexample_Batch = Proof_Data
   473 (
   474   type T = unit -> (int -> term list option) list
   475   (* FIXME avoid user error with non-user text *)
   476   fun init _ () = error "Counterexample"
   477 );
   478 val put_counterexample_batch = Counterexample_Batch.put;
   479 
   480 structure Validator_Batch = Proof_Data
   481 (
   482   type T = unit -> (int -> bool) list
   483   (* FIXME avoid user error with non-user text *)
   484   fun init _ () = error "Counterexample"
   485 );
   486 val put_validator_batch = Validator_Batch.put;
   487 
   488 
   489 val target = "Quickcheck";
   490   
   491 fun compile_generator_expr ctxt ts =
   492   let
   493     val thy = ProofContext.theory_of ctxt
   494     val mk_generator_expr = 
   495       if Config.get ctxt fast then mk_fast_generator_expr
   496       else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr
   497     val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts;
   498     val compile = Code_Runtime.dynamic_value_strict
   499       (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
   500       thy (SOME target) (fn proc => fn g =>
   501         fn card => fn size => g card size |> (Option.map o map) proc) t' []
   502   in
   503     fn [card, size] => rpair NONE (compile card size |> 
   504       (if Config.get ctxt quickcheck_pretty then
   505         Option.map (map Quickcheck_Common.post_process_term) else I))
   506   end;
   507  
   508 fun compile_generator_exprs ctxt ts =
   509   let
   510     val thy = ProofContext.theory_of ctxt
   511     val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts;
   512     val compiles = Code_Runtime.dynamic_value_strict
   513       (Counterexample_Batch.get, put_counterexample_batch,
   514         "Exhaustive_Generators.put_counterexample_batch")
   515       thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
   516       (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') []
   517   in
   518     map (fn compile => fn size => compile size
   519       |> Option.map (map Quickcheck_Common.post_process_term)) compiles
   520   end;
   521 
   522 fun compile_validator_exprs ctxt ts =
   523   let
   524     val thy = ProofContext.theory_of ctxt
   525     val ts' = map (mk_validator_expr ctxt) ts
   526   in
   527     Code_Runtime.dynamic_value_strict
   528       (Validator_Batch.get, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
   529       thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
   530   end;
   531 
   532 (* setup *)
   533 
   534 val setup =
   535   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   536       (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
   537 (* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   538       (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
   539   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   540       (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
   541   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   542       (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
   543   #> setup_smart_quantifier
   544   #> setup_full_support
   545   #> setup_fast
   546   #> setup_quickcheck_pretty
   547   #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
   548   #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
   549   #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));
   550 
   551 end;