moving exhaustive_generators.ML to Quickcheck directory
authorbulwahn
Fri Mar 11 15:21:13 2011 +0100 (2011-03-11)
changeset 41920d4fb7a418152
parent 41919 e180c2a9873b
child 41921 ee84fc7a61f1
moving exhaustive_generators.ML to Quickcheck directory
src/HOL/IsaMakefile
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Rat.thy
src/HOL/RealDef.thy
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/exhaustive_generators.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Mar 11 15:21:13 2011 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Mar 11 15:21:13 2011 +0100
     1.3 @@ -299,7 +299,6 @@
     1.4    Tools/ATP/atp_systems.ML \
     1.5    Tools/choice_specification.ML \
     1.6    Tools/code_evaluation.ML \
     1.7 -  Tools/exhaustive_generators.ML \
     1.8    Tools/groebner.ML \
     1.9    Tools/int_arith.ML \
    1.10    Tools/list_code.ML \
    1.11 @@ -338,6 +337,7 @@
    1.12    Tools/Qelim/cooper.ML \
    1.13    Tools/Qelim/cooper_procedure.ML \
    1.14    Tools/Qelim/qelim.ML \
    1.15 +  Tools/Quickcheck/exhaustive_generators.ML \
    1.16    Tools/Quotient/quotient_def.ML \
    1.17    Tools/Quotient/quotient_info.ML \
    1.18    Tools/Quotient/quotient_tacs.ML \
     2.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 15:21:13 2011 +0100
     2.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 15:21:13 2011 +0100
     2.3 @@ -4,7 +4,7 @@
     2.4  
     2.5  theory Quickcheck_Exhaustive
     2.6  imports Quickcheck
     2.7 -uses ("Tools/exhaustive_generators.ML")
     2.8 +uses ("Tools/Quickcheck/exhaustive_generators.ML")
     2.9  begin
    2.10  
    2.11  subsection {* basic operations for exhaustive generators *}
    2.12 @@ -366,9 +366,9 @@
    2.13    [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
    2.14  
    2.15  code_const catch_match 
    2.16 -  (SML "(_) handle Match => _")
    2.17 +  (Quickcheck "(_) handle Match => _")
    2.18  
    2.19 -use "Tools/exhaustive_generators.ML"
    2.20 +use "Tools/Quickcheck/exhaustive_generators.ML"
    2.21  
    2.22  setup {* Exhaustive_Generators.setup *}
    2.23  
     3.1 --- a/src/HOL/Rat.thy	Fri Mar 11 15:21:13 2011 +0100
     3.2 +++ b/src/HOL/Rat.thy	Fri Mar 11 15:21:13 2011 +0100
     3.3 @@ -1132,11 +1132,11 @@
     3.4  no_notation fcomp (infixl "\<circ>>" 60)
     3.5  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
     3.6  
     3.7 -instantiation rat :: full_small
     3.8 +instantiation rat :: exhaustive
     3.9  begin
    3.10  
    3.11  definition
    3.12 -  "full_small f d = full_small (%(k, kt). full_small (%(l, lt).
    3.13 +  "exhaustive f d = exhaustive (%(k, kt). exhaustive (%(l, lt).
    3.14       f (valterm_fract (Code_Numeral.int_of k, %_. Code_Evaluation.term_of (Code_Numeral.int_of k)) (Code_Numeral.int_of l, %_. Code_Evaluation.term_of (Code_Numeral.int_of l)))) d) d"
    3.15  
    3.16  instance ..
     4.1 --- a/src/HOL/RealDef.thy	Fri Mar 11 15:21:13 2011 +0100
     4.2 +++ b/src/HOL/RealDef.thy	Fri Mar 11 15:21:13 2011 +0100
     4.3 @@ -1768,11 +1768,11 @@
     4.4  no_notation fcomp (infixl "\<circ>>" 60)
     4.5  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
     4.6  
     4.7 -instantiation real :: full_small
     4.8 +instantiation real :: exhaustive
     4.9  begin
    4.10  
    4.11  definition
    4.12 -  "full_small f d = full_small (%r. f (valterm_ratreal r)) d"
    4.13 +  "exhaustive f d = exhaustive (%r. f (valterm_ratreal r)) d"
    4.14  
    4.15  instance ..
    4.16  
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     5.3 @@ -0,0 +1,405 @@
     5.4 +(*  Title:      HOL/Tools/exhaustive_generators.ML
     5.5 +    Author:     Lukas Bulwahn, TU Muenchen
     5.6 +
     5.7 +Exhaustive generators for various types.
     5.8 +*)
     5.9 +
    5.10 +signature EXHAUSTIVE_GENERATORS =
    5.11 +sig
    5.12 +  val compile_generator_expr:
    5.13 +    Proof.context -> term -> int -> term list option * Quickcheck.report option
    5.14 +  val compile_generator_exprs:
    5.15 +    Proof.context -> term list -> (int -> term list option) list
    5.16 +  val put_counterexample: (unit -> int -> term list option)
    5.17 +    -> Proof.context -> Proof.context
    5.18 +  val put_counterexample_batch: (unit -> (int -> term list option) list)
    5.19 +    -> Proof.context -> Proof.context
    5.20 +  val smart_quantifier : bool Config.T;
    5.21 +  val quickcheck_pretty : bool Config.T;
    5.22 +  val setup: theory -> theory
    5.23 +end;
    5.24 +
    5.25 +structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
    5.26 +struct
    5.27 +
    5.28 +(* static options *)
    5.29 +
    5.30 +val define_foundationally = false
    5.31 +
    5.32 +(* dynamic options *)
    5.33 +
    5.34 +val (smart_quantifier, setup_smart_quantifier) =
    5.35 +  Attrib.config_bool "quickcheck_smart_quantifier" (K true)
    5.36 +
    5.37 +val (quickcheck_pretty, setup_quickcheck_pretty) =
    5.38 +  Attrib.config_bool "quickcheck_pretty" (K true)
    5.39 + 
    5.40 +(** general term functions **)
    5.41 +
    5.42 +fun mk_measure f =
    5.43 +  let
    5.44 +    val Type ("fun", [T, @{typ nat}]) = fastype_of f 
    5.45 +  in
    5.46 +    Const (@{const_name Wellfounded.measure},
    5.47 +      (T --> @{typ nat}) --> HOLogic.mk_prodT (T, T) --> @{typ bool})
    5.48 +    $ f
    5.49 +  end
    5.50 +
    5.51 +fun mk_sumcases rT f (Type (@{type_name Sum_Type.sum}, [TL, TR])) =
    5.52 +  let
    5.53 +    val lt = mk_sumcases rT f TL
    5.54 +    val rt = mk_sumcases rT f TR
    5.55 +  in
    5.56 +    SumTree.mk_sumcase TL TR rT lt rt
    5.57 +  end
    5.58 +  | mk_sumcases _ f T = f T
    5.59 +
    5.60 +fun mk_undefined T = Const(@{const_name undefined}, T)
    5.61 +  
    5.62 +
    5.63 +(** abstract syntax **)
    5.64 +
    5.65 +fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
    5.66 +
    5.67 +val size = @{term "i :: code_numeral"}
    5.68 +val size_pred = @{term "(i :: code_numeral) - 1"}
    5.69 +val size_ge_zero = @{term "(i :: code_numeral) > 0"}
    5.70 +fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
    5.71 +
    5.72 +fun mk_none_continuation (x, y) =
    5.73 +  let
    5.74 +    val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
    5.75 +  in
    5.76 +    Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T)
    5.77 +      $ x $ y
    5.78 +  end
    5.79 +
    5.80 +(** datatypes **)
    5.81 +
    5.82 +(* constructing exhaustive generator instances on datatypes *)
    5.83 +
    5.84 +exception FUNCTION_TYPE;
    5.85 +val exhaustiveN = "exhaustive";
    5.86 +
    5.87 +fun exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    5.88 +  --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
    5.89 +
    5.90 +fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    5.91 +  --> @{typ "Code_Evaluation.term list option"}
    5.92 +
    5.93 +fun mk_equations thy descr vs tycos exhaustives (Ts, Us) =
    5.94 +  let
    5.95 +    fun mk_call T =
    5.96 +      let
    5.97 +        val exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)        
    5.98 +      in
    5.99 +        (T, (fn t => exhaustive $
   5.100 +          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   5.101 +          $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
   5.102 +      end
   5.103 +    fun mk_aux_call fTs (k, _) (tyco, Ts) =
   5.104 +      let
   5.105 +        val T = Type (tyco, Ts)
   5.106 +        val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   5.107 +      in
   5.108 +       (T, (fn t => nth exhaustives k $
   5.109 +          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   5.110 +            $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
   5.111 +      end
   5.112 +    fun mk_consexpr simpleT (c, xs) =
   5.113 +      let
   5.114 +        val (Ts, fns) = split_list xs
   5.115 +        val constr = Const (c, Ts ---> simpleT)
   5.116 +        val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
   5.117 +        val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
   5.118 +        val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
   5.119 +        val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
   5.120 +        val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
   5.121 +          bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
   5.122 +        val start_term = test_function simpleT $ 
   5.123 +        (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
   5.124 +          $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
   5.125 +      in fold_rev (fn f => fn t => f t) fns start_term end
   5.126 +    fun mk_rhs exprs =
   5.127 +        @{term "If :: bool => term list option => term list option => term list option"}
   5.128 +            $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
   5.129 +    val rhss =
   5.130 +      Datatype_Aux.interpret_construction descr vs
   5.131 +        { atyp = mk_call, dtyp = mk_aux_call }
   5.132 +      |> (map o apfst) Type
   5.133 +      |> map (fn (T, cs) => map (mk_consexpr T) cs)
   5.134 +      |> map mk_rhs
   5.135 +    val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives (Ts @ Us);
   5.136 +    val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
   5.137 +  in
   5.138 +    eqs
   5.139 +  end
   5.140 +
   5.141 +(* foundational definition with the function package *)
   5.142 +
   5.143 +val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
   5.144 +
   5.145 +fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
   5.146 +    Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
   5.147 +
   5.148 +fun mk_termination_measure T =
   5.149 +  let
   5.150 +    val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
   5.151 +  in
   5.152 +    mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
   5.153 +  end
   5.154 +
   5.155 +fun termination_tac ctxt = 
   5.156 +  Function_Relation.relation_tac ctxt mk_termination_measure 1
   5.157 +  THEN rtac @{thm wf_measure} 1
   5.158 +  THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
   5.159 +    (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
   5.160 +     @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
   5.161 +
   5.162 +fun pat_completeness_auto ctxt =
   5.163 +  Pat_Completeness.pat_completeness_tac ctxt 1
   5.164 +  THEN auto_tac (clasimpset_of ctxt)    
   5.165 +
   5.166 +
   5.167 +(* creating the instances *)
   5.168 +
   5.169 +fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   5.170 +  let
   5.171 +    val _ = Datatype_Aux.message config "Creating exhaustive generators ...";
   5.172 +    val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames);
   5.173 +  in
   5.174 +    thy
   5.175 +    |> Class.instantiation (tycos, vs, @{sort exhaustive})
   5.176 +    |> (if define_foundationally then
   5.177 +      let
   5.178 +        val exhaustives = map2 (fn name => fn T => Free (name, exhaustiveT T)) exhaustivesN (Ts @ Us)
   5.179 +        val eqs = mk_equations thy descr vs tycos exhaustives (Ts, Us)
   5.180 +      in
   5.181 +        Function.add_function
   5.182 +          (map (fn (name, T) =>
   5.183 +              Syntax.no_syn (Binding.conceal (Binding.name name), SOME (exhaustiveT T)))
   5.184 +                (exhaustivesN ~~ (Ts @ Us)))
   5.185 +            (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs)
   5.186 +          Function_Common.default_config pat_completeness_auto
   5.187 +        #> snd
   5.188 +        #> Local_Theory.restore
   5.189 +        #> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
   5.190 +        #> snd
   5.191 +      end
   5.192 +    else
   5.193 +      fold_map (fn (name, T) => Local_Theory.define
   5.194 +          ((Binding.conceal (Binding.name name), NoSyn),
   5.195 +            (apfst Binding.conceal Attrib.empty_binding, mk_undefined (exhaustiveT T)))
   5.196 +        #> apfst fst) (exhaustivesN ~~ (Ts @ Us))
   5.197 +      #> (fn (exhaustives, lthy) =>
   5.198 +        let
   5.199 +          val eqs_t = mk_equations thy descr vs tycos exhaustives (Ts, Us)
   5.200 +          val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
   5.201 +            (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
   5.202 +        in
   5.203 +          fold (fn (name, eq) => Local_Theory.note
   5.204 +          ((Binding.conceal (Binding.qualify true prfx
   5.205 +             (Binding.qualify true name (Binding.name "simps"))),
   5.206 +             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
   5.207 +               [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (exhaustivesN ~~ eqs) lthy
   5.208 +        end))
   5.209 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   5.210 +  end handle FUNCTION_TYPE =>
   5.211 +    (Datatype_Aux.message config
   5.212 +      "Creation of exhaustivevalue generators failed because the datatype contains a function type";
   5.213 +    thy)
   5.214 +
   5.215 +(** building and compiling generator expressions **)
   5.216 +
   5.217 +structure Counterexample = Proof_Data
   5.218 +(
   5.219 +  type T = unit -> int -> term list option
   5.220 +  (* FIXME avoid user error with non-user text *)
   5.221 +  fun init _ () = error "Counterexample"
   5.222 +);
   5.223 +val put_counterexample = Counterexample.put;
   5.224 +
   5.225 +structure Counterexample_Batch = Proof_Data
   5.226 +(
   5.227 +  type T = unit -> (int -> term list option) list
   5.228 +  (* FIXME avoid user error with non-user text *)
   5.229 +  fun init _ () = error "Counterexample"
   5.230 +);
   5.231 +val put_counterexample_batch = Counterexample_Batch.put;
   5.232 +
   5.233 +val target = "Quickcheck";
   5.234 +
   5.235 +fun mk_smart_generator_expr ctxt t =
   5.236 +  let
   5.237 +    val thy = ProofContext.theory_of ctxt
   5.238 +    val ((vnames, Ts), t') = apfst split_list (strip_abs t)
   5.239 +    val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt
   5.240 +    val (names, ctxt'') = Variable.variant_fixes vnames ctxt'
   5.241 +    val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") vnames) ctxt''
   5.242 +    val depth = Free (depth_name, @{typ code_numeral})
   5.243 +    val frees = map2 (curry Free) names Ts
   5.244 +    val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names 
   5.245 +    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
   5.246 +      | strip_imp A = ([], A)
   5.247 +    val (assms, concl) = strip_imp (subst_bounds (rev frees, t'))
   5.248 +    val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
   5.249 +    fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
   5.250 +      if Sign.of_sort thy (T, @{sort enum}) then
   5.251 +        Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
   5.252 +          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   5.253 +            $ lambda free (lambda term_var t))
   5.254 +      else
   5.255 +        Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
   5.256 +          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   5.257 +            $ lambda free (lambda term_var t)) $ depth
   5.258 +    fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
   5.259 +    val none_t = @{term "None :: term list option"}
   5.260 +    fun mk_safe_if (cond, then_t, else_t) =
   5.261 +      @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
   5.262 +        (@{term "If :: bool => term list option => term list option => term list option"}
   5.263 +        $ cond $ then_t $ else_t) $ none_t;
   5.264 +    fun mk_test_term bound_vars assms =
   5.265 +      let
   5.266 +        fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
   5.267 +        val (vars, check) =
   5.268 +          case assms of [] =>
   5.269 +            (vars_of concl, (concl, none_t, @{term "Some :: term list => term list option"} $ terms))
   5.270 +          | assm :: assms =>
   5.271 +            (vars_of assm, (assm, mk_test_term (union (op =) (vars_of assm) bound_vars) assms, none_t))
   5.272 +      in
   5.273 +        fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
   5.274 +      end
   5.275 +  in lambda depth (mk_test_term [] assms) end
   5.276 +
   5.277 +fun mk_generator_expr ctxt t =
   5.278 +  let
   5.279 +    val Ts = (map snd o fst o strip_abs) t;
   5.280 +    val thy = ProofContext.theory_of ctxt
   5.281 +    val bound_max = length Ts - 1;
   5.282 +    val bounds = map_index (fn (i, ty) =>
   5.283 +      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
   5.284 +    val result = list_comb (t, map (fn (i, _, _, _) => Bound i) bounds);
   5.285 +    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
   5.286 +    val check =
   5.287 +      @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
   5.288 +        (@{term "If :: bool => term list option => term list option => term list option"}
   5.289 +        $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms))
   5.290 +      $ @{term "None :: term list option"};
   5.291 +    fun mk_exhaustive_closure (_, _, i, T) t =
   5.292 +      Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
   5.293 +        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   5.294 +        $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
   5.295 +  in Abs ("d", @{typ code_numeral}, fold_rev mk_exhaustive_closure bounds check) end
   5.296 +
   5.297 +(** post-processing of function terms **)
   5.298 +
   5.299 +fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
   5.300 +  | dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
   5.301 +
   5.302 +fun mk_fun_upd T1 T2 (t1, t2) t = 
   5.303 +  Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
   5.304 +
   5.305 +fun dest_fun_upds t =
   5.306 +  case try dest_fun_upd t of
   5.307 +    NONE =>
   5.308 +      (case t of
   5.309 +        Abs (_, _, _) => ([], t) 
   5.310 +      | _ => raise TERM ("dest_fun_upds", [t]))
   5.311 +  | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)
   5.312 +
   5.313 +fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
   5.314 +
   5.315 +fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
   5.316 +  | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
   5.317 +  | make_set T1 ((t1, @{const True}) :: tps) =
   5.318 +    Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
   5.319 +      $ t1 $ (make_set T1 tps)
   5.320 +  | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
   5.321 +
   5.322 +fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool})
   5.323 +  | make_coset T tps = 
   5.324 +    let
   5.325 +      val U = T --> @{typ bool}
   5.326 +      fun invert @{const False} = @{const True}
   5.327 +        | invert @{const True} = @{const False}
   5.328 +    in
   5.329 +      Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U)
   5.330 +        $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
   5.331 +    end
   5.332 +
   5.333 +fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
   5.334 +  | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
   5.335 +  | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
   5.336 +  
   5.337 +fun post_process_term t =
   5.338 +  let
   5.339 +    fun map_Abs f t =
   5.340 +      case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
   5.341 +    fun process_args t = case strip_comb t of
   5.342 +      (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
   5.343 +  in
   5.344 +    case fastype_of t of
   5.345 +      Type (@{type_name fun}, [T1, T2]) =>
   5.346 +        (case try dest_fun_upds t of
   5.347 +          SOME (tps, t) =>
   5.348 +            (map (pairself post_process_term) tps, map_Abs post_process_term t)
   5.349 +            |> (case T2 of
   5.350 +              @{typ bool} => 
   5.351 +                (case t of
   5.352 +                   Abs(_, _, @{const True}) => fst #> rev #> make_set T1
   5.353 +                 | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1
   5.354 +                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
   5.355 +                 | _ => raise TERM ("post_process_term", [t]))
   5.356 +            | Type (@{type_name option}, _) =>
   5.357 +                (case t of
   5.358 +                  Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2
   5.359 +                | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
   5.360 +                | _ => make_fun_upds T1 T2) 
   5.361 +            | _ => make_fun_upds T1 T2)
   5.362 +        | NONE => process_args t)
   5.363 +    | _ => process_args t
   5.364 +  end
   5.365 +
   5.366 +(** generator compiliation **)
   5.367 +
   5.368 +fun compile_generator_expr ctxt t =
   5.369 +  let
   5.370 +    val thy = ProofContext.theory_of ctxt
   5.371 +    val t' =
   5.372 +      (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
   5.373 +        ctxt t;
   5.374 +    val compile = Code_Runtime.dynamic_value_strict
   5.375 +      (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
   5.376 +      thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
   5.377 +  in
   5.378 +    fn size => rpair NONE (compile size |> 
   5.379 +      (if Config.get ctxt quickcheck_pretty then Option.map (map post_process_term) else I))
   5.380 +  end;
   5.381 +
   5.382 +fun compile_generator_exprs ctxt ts =
   5.383 +  let
   5.384 +    val thy = ProofContext.theory_of ctxt
   5.385 +    val mk_generator_expr =
   5.386 +      if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr
   5.387 +    val ts' = map (mk_generator_expr ctxt) ts;
   5.388 +    val compiles = Code_Runtime.dynamic_value_strict
   5.389 +      (Counterexample_Batch.get, put_counterexample_batch,
   5.390 +        "Exhaustive_Generators.put_counterexample_batch")
   5.391 +      thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
   5.392 +      (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') [];
   5.393 +  in
   5.394 +    map (fn compile => fn size => compile size |> Option.map (map post_process_term)) compiles
   5.395 +  end;
   5.396 +  
   5.397 +  
   5.398 +(** setup **)
   5.399 +
   5.400 +val setup =
   5.401 +  Datatype.interpretation
   5.402 +    (Quickcheck_Generators.ensure_sort_datatype (@{sort exhaustive}, instantiate_exhaustive_datatype))
   5.403 +  #> setup_smart_quantifier
   5.404 +  #> setup_quickcheck_pretty
   5.405 +  #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
   5.406 +  #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs));
   5.407 +
   5.408 +end;
     6.1 --- a/src/HOL/Tools/exhaustive_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,405 +0,0 @@
     6.4 -(*  Title:      HOL/Tools/exhaustive_generators.ML
     6.5 -    Author:     Lukas Bulwahn, TU Muenchen
     6.6 -
     6.7 -Exhaustive generators for various types.
     6.8 -*)
     6.9 -
    6.10 -signature EXHAUSTIVE_GENERATORS =
    6.11 -sig
    6.12 -  val compile_generator_expr:
    6.13 -    Proof.context -> term -> int -> term list option * Quickcheck.report option
    6.14 -  val compile_generator_exprs:
    6.15 -    Proof.context -> term list -> (int -> term list option) list
    6.16 -  val put_counterexample: (unit -> int -> term list option)
    6.17 -    -> Proof.context -> Proof.context
    6.18 -  val put_counterexample_batch: (unit -> (int -> term list option) list)
    6.19 -    -> Proof.context -> Proof.context
    6.20 -  val smart_quantifier : bool Config.T;
    6.21 -  val quickcheck_pretty : bool Config.T;
    6.22 -  val setup: theory -> theory
    6.23 -end;
    6.24 -
    6.25 -structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
    6.26 -struct
    6.27 -
    6.28 -(* static options *)
    6.29 -
    6.30 -val define_foundationally = false
    6.31 -
    6.32 -(* dynamic options *)
    6.33 -
    6.34 -val (smart_quantifier, setup_smart_quantifier) =
    6.35 -  Attrib.config_bool "quickcheck_smart_quantifier" (K true)
    6.36 -
    6.37 -val (quickcheck_pretty, setup_quickcheck_pretty) =
    6.38 -  Attrib.config_bool "quickcheck_pretty" (K true)
    6.39 - 
    6.40 -(** general term functions **)
    6.41 -
    6.42 -fun mk_measure f =
    6.43 -  let
    6.44 -    val Type ("fun", [T, @{typ nat}]) = fastype_of f 
    6.45 -  in
    6.46 -    Const (@{const_name Wellfounded.measure},
    6.47 -      (T --> @{typ nat}) --> HOLogic.mk_prodT (T, T) --> @{typ bool})
    6.48 -    $ f
    6.49 -  end
    6.50 -
    6.51 -fun mk_sumcases rT f (Type (@{type_name Sum_Type.sum}, [TL, TR])) =
    6.52 -  let
    6.53 -    val lt = mk_sumcases rT f TL
    6.54 -    val rt = mk_sumcases rT f TR
    6.55 -  in
    6.56 -    SumTree.mk_sumcase TL TR rT lt rt
    6.57 -  end
    6.58 -  | mk_sumcases _ f T = f T
    6.59 -
    6.60 -fun mk_undefined T = Const(@{const_name undefined}, T)
    6.61 -  
    6.62 -
    6.63 -(** abstract syntax **)
    6.64 -
    6.65 -fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
    6.66 -
    6.67 -val size = @{term "i :: code_numeral"}
    6.68 -val size_pred = @{term "(i :: code_numeral) - 1"}
    6.69 -val size_ge_zero = @{term "(i :: code_numeral) > 0"}
    6.70 -fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
    6.71 -
    6.72 -fun mk_none_continuation (x, y) =
    6.73 -  let
    6.74 -    val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
    6.75 -  in
    6.76 -    Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T)
    6.77 -      $ x $ y
    6.78 -  end
    6.79 -
    6.80 -(** datatypes **)
    6.81 -
    6.82 -(* constructing exhaustive generator instances on datatypes *)
    6.83 -
    6.84 -exception FUNCTION_TYPE;
    6.85 -val exhaustiveN = "exhaustive";
    6.86 -
    6.87 -fun exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    6.88 -  --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
    6.89 -
    6.90 -fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    6.91 -  --> @{typ "Code_Evaluation.term list option"}
    6.92 -
    6.93 -fun mk_equations thy descr vs tycos exhaustives (Ts, Us) =
    6.94 -  let
    6.95 -    fun mk_call T =
    6.96 -      let
    6.97 -        val exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)        
    6.98 -      in
    6.99 -        (T, (fn t => exhaustive $
   6.100 -          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   6.101 -          $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
   6.102 -      end
   6.103 -    fun mk_aux_call fTs (k, _) (tyco, Ts) =
   6.104 -      let
   6.105 -        val T = Type (tyco, Ts)
   6.106 -        val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   6.107 -      in
   6.108 -       (T, (fn t => nth exhaustives k $
   6.109 -          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   6.110 -            $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
   6.111 -      end
   6.112 -    fun mk_consexpr simpleT (c, xs) =
   6.113 -      let
   6.114 -        val (Ts, fns) = split_list xs
   6.115 -        val constr = Const (c, Ts ---> simpleT)
   6.116 -        val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
   6.117 -        val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
   6.118 -        val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
   6.119 -        val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
   6.120 -        val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
   6.121 -          bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
   6.122 -        val start_term = test_function simpleT $ 
   6.123 -        (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
   6.124 -          $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
   6.125 -      in fold_rev (fn f => fn t => f t) fns start_term end
   6.126 -    fun mk_rhs exprs =
   6.127 -        @{term "If :: bool => term list option => term list option => term list option"}
   6.128 -            $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
   6.129 -    val rhss =
   6.130 -      Datatype_Aux.interpret_construction descr vs
   6.131 -        { atyp = mk_call, dtyp = mk_aux_call }
   6.132 -      |> (map o apfst) Type
   6.133 -      |> map (fn (T, cs) => map (mk_consexpr T) cs)
   6.134 -      |> map mk_rhs
   6.135 -    val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives (Ts @ Us);
   6.136 -    val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
   6.137 -  in
   6.138 -    eqs
   6.139 -  end
   6.140 -
   6.141 -(* foundational definition with the function package *)
   6.142 -
   6.143 -val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
   6.144 -
   6.145 -fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
   6.146 -    Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
   6.147 -
   6.148 -fun mk_termination_measure T =
   6.149 -  let
   6.150 -    val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
   6.151 -  in
   6.152 -    mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
   6.153 -  end
   6.154 -
   6.155 -fun termination_tac ctxt = 
   6.156 -  Function_Relation.relation_tac ctxt mk_termination_measure 1
   6.157 -  THEN rtac @{thm wf_measure} 1
   6.158 -  THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
   6.159 -    (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
   6.160 -     @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
   6.161 -
   6.162 -fun pat_completeness_auto ctxt =
   6.163 -  Pat_Completeness.pat_completeness_tac ctxt 1
   6.164 -  THEN auto_tac (clasimpset_of ctxt)    
   6.165 -
   6.166 -
   6.167 -(* creating the instances *)
   6.168 -
   6.169 -fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   6.170 -  let
   6.171 -    val _ = Datatype_Aux.message config "Creating exhaustive generators ...";
   6.172 -    val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames);
   6.173 -  in
   6.174 -    thy
   6.175 -    |> Class.instantiation (tycos, vs, @{sort exhaustive})
   6.176 -    |> (if define_foundationally then
   6.177 -      let
   6.178 -        val exhaustives = map2 (fn name => fn T => Free (name, exhaustiveT T)) exhaustivesN (Ts @ Us)
   6.179 -        val eqs = mk_equations thy descr vs tycos exhaustives (Ts, Us)
   6.180 -      in
   6.181 -        Function.add_function
   6.182 -          (map (fn (name, T) =>
   6.183 -              Syntax.no_syn (Binding.conceal (Binding.name name), SOME (exhaustiveT T)))
   6.184 -                (exhaustivesN ~~ (Ts @ Us)))
   6.185 -            (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs)
   6.186 -          Function_Common.default_config pat_completeness_auto
   6.187 -        #> snd
   6.188 -        #> Local_Theory.restore
   6.189 -        #> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
   6.190 -        #> snd
   6.191 -      end
   6.192 -    else
   6.193 -      fold_map (fn (name, T) => Local_Theory.define
   6.194 -          ((Binding.conceal (Binding.name name), NoSyn),
   6.195 -            (apfst Binding.conceal Attrib.empty_binding, mk_undefined (exhaustiveT T)))
   6.196 -        #> apfst fst) (exhaustivesN ~~ (Ts @ Us))
   6.197 -      #> (fn (exhaustives, lthy) =>
   6.198 -        let
   6.199 -          val eqs_t = mk_equations thy descr vs tycos exhaustives (Ts, Us)
   6.200 -          val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
   6.201 -            (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
   6.202 -        in
   6.203 -          fold (fn (name, eq) => Local_Theory.note
   6.204 -          ((Binding.conceal (Binding.qualify true prfx
   6.205 -             (Binding.qualify true name (Binding.name "simps"))),
   6.206 -             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
   6.207 -               [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (exhaustivesN ~~ eqs) lthy
   6.208 -        end))
   6.209 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   6.210 -  end handle FUNCTION_TYPE =>
   6.211 -    (Datatype_Aux.message config
   6.212 -      "Creation of exhaustivevalue generators failed because the datatype contains a function type";
   6.213 -    thy)
   6.214 -
   6.215 -(** building and compiling generator expressions **)
   6.216 -
   6.217 -structure Counterexample = Proof_Data
   6.218 -(
   6.219 -  type T = unit -> int -> term list option
   6.220 -  (* FIXME avoid user error with non-user text *)
   6.221 -  fun init _ () = error "Counterexample"
   6.222 -);
   6.223 -val put_counterexample = Counterexample.put;
   6.224 -
   6.225 -structure Counterexample_Batch = Proof_Data
   6.226 -(
   6.227 -  type T = unit -> (int -> term list option) list
   6.228 -  (* FIXME avoid user error with non-user text *)
   6.229 -  fun init _ () = error "Counterexample"
   6.230 -);
   6.231 -val put_counterexample_batch = Counterexample_Batch.put;
   6.232 -
   6.233 -val target = "Quickcheck";
   6.234 -
   6.235 -fun mk_smart_generator_expr ctxt t =
   6.236 -  let
   6.237 -    val thy = ProofContext.theory_of ctxt
   6.238 -    val ((vnames, Ts), t') = apfst split_list (strip_abs t)
   6.239 -    val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt
   6.240 -    val (names, ctxt'') = Variable.variant_fixes vnames ctxt'
   6.241 -    val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") vnames) ctxt''
   6.242 -    val depth = Free (depth_name, @{typ code_numeral})
   6.243 -    val frees = map2 (curry Free) names Ts
   6.244 -    val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names 
   6.245 -    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
   6.246 -      | strip_imp A = ([], A)
   6.247 -    val (assms, concl) = strip_imp (subst_bounds (rev frees, t'))
   6.248 -    val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
   6.249 -    fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
   6.250 -      if Sign.of_sort thy (T, @{sort enum}) then
   6.251 -        Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
   6.252 -          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   6.253 -            $ lambda free (lambda term_var t))
   6.254 -      else
   6.255 -        Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
   6.256 -          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   6.257 -            $ lambda free (lambda term_var t)) $ depth
   6.258 -    fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
   6.259 -    val none_t = @{term "None :: term list option"}
   6.260 -    fun mk_safe_if (cond, then_t, else_t) =
   6.261 -      @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
   6.262 -        (@{term "If :: bool => term list option => term list option => term list option"}
   6.263 -        $ cond $ then_t $ else_t) $ none_t;
   6.264 -    fun mk_test_term bound_vars assms =
   6.265 -      let
   6.266 -        fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
   6.267 -        val (vars, check) =
   6.268 -          case assms of [] =>
   6.269 -            (vars_of concl, (concl, none_t, @{term "Some :: term list => term list option"} $ terms))
   6.270 -          | assm :: assms =>
   6.271 -            (vars_of assm, (assm, mk_test_term (union (op =) (vars_of assm) bound_vars) assms, none_t))
   6.272 -      in
   6.273 -        fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
   6.274 -      end
   6.275 -  in lambda depth (mk_test_term [] assms) end
   6.276 -
   6.277 -fun mk_generator_expr ctxt t =
   6.278 -  let
   6.279 -    val Ts = (map snd o fst o strip_abs) t;
   6.280 -    val thy = ProofContext.theory_of ctxt
   6.281 -    val bound_max = length Ts - 1;
   6.282 -    val bounds = map_index (fn (i, ty) =>
   6.283 -      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
   6.284 -    val result = list_comb (t, map (fn (i, _, _, _) => Bound i) bounds);
   6.285 -    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
   6.286 -    val check =
   6.287 -      @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
   6.288 -        (@{term "If :: bool => term list option => term list option => term list option"}
   6.289 -        $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms))
   6.290 -      $ @{term "None :: term list option"};
   6.291 -    fun mk_exhaustive_closure (_, _, i, T) t =
   6.292 -      Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
   6.293 -        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   6.294 -        $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
   6.295 -  in Abs ("d", @{typ code_numeral}, fold_rev mk_exhaustive_closure bounds check) end
   6.296 -
   6.297 -(** post-processing of function terms **)
   6.298 -
   6.299 -fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
   6.300 -  | dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
   6.301 -
   6.302 -fun mk_fun_upd T1 T2 (t1, t2) t = 
   6.303 -  Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
   6.304 -
   6.305 -fun dest_fun_upds t =
   6.306 -  case try dest_fun_upd t of
   6.307 -    NONE =>
   6.308 -      (case t of
   6.309 -        Abs (_, _, _) => ([], t) 
   6.310 -      | _ => raise TERM ("dest_fun_upds", [t]))
   6.311 -  | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)
   6.312 -
   6.313 -fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
   6.314 -
   6.315 -fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
   6.316 -  | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
   6.317 -  | make_set T1 ((t1, @{const True}) :: tps) =
   6.318 -    Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
   6.319 -      $ t1 $ (make_set T1 tps)
   6.320 -  | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
   6.321 -
   6.322 -fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool})
   6.323 -  | make_coset T tps = 
   6.324 -    let
   6.325 -      val U = T --> @{typ bool}
   6.326 -      fun invert @{const False} = @{const True}
   6.327 -        | invert @{const True} = @{const False}
   6.328 -    in
   6.329 -      Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U)
   6.330 -        $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
   6.331 -    end
   6.332 -
   6.333 -fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
   6.334 -  | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
   6.335 -  | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
   6.336 -  
   6.337 -fun post_process_term t =
   6.338 -  let
   6.339 -    fun map_Abs f t =
   6.340 -      case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
   6.341 -    fun process_args t = case strip_comb t of
   6.342 -      (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
   6.343 -  in
   6.344 -    case fastype_of t of
   6.345 -      Type (@{type_name fun}, [T1, T2]) =>
   6.346 -        (case try dest_fun_upds t of
   6.347 -          SOME (tps, t) =>
   6.348 -            (map (pairself post_process_term) tps, map_Abs post_process_term t)
   6.349 -            |> (case T2 of
   6.350 -              @{typ bool} => 
   6.351 -                (case t of
   6.352 -                   Abs(_, _, @{const True}) => fst #> rev #> make_set T1
   6.353 -                 | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1
   6.354 -                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
   6.355 -                 | _ => raise TERM ("post_process_term", [t]))
   6.356 -            | Type (@{type_name option}, _) =>
   6.357 -                (case t of
   6.358 -                  Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2
   6.359 -                | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
   6.360 -                | _ => make_fun_upds T1 T2) 
   6.361 -            | _ => make_fun_upds T1 T2)
   6.362 -        | NONE => process_args t)
   6.363 -    | _ => process_args t
   6.364 -  end
   6.365 -
   6.366 -(** generator compiliation **)
   6.367 -
   6.368 -fun compile_generator_expr ctxt t =
   6.369 -  let
   6.370 -    val thy = ProofContext.theory_of ctxt
   6.371 -    val t' =
   6.372 -      (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
   6.373 -        ctxt t;
   6.374 -    val compile = Code_Runtime.dynamic_value_strict
   6.375 -      (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
   6.376 -      thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
   6.377 -  in
   6.378 -    fn size => rpair NONE (compile size |> 
   6.379 -      (if Config.get ctxt quickcheck_pretty then Option.map (map post_process_term) else I))
   6.380 -  end;
   6.381 -
   6.382 -fun compile_generator_exprs ctxt ts =
   6.383 -  let
   6.384 -    val thy = ProofContext.theory_of ctxt
   6.385 -    val mk_generator_expr =
   6.386 -      if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr
   6.387 -    val ts' = map (mk_generator_expr ctxt) ts;
   6.388 -    val compiles = Code_Runtime.dynamic_value_strict
   6.389 -      (Counterexample_Batch.get, put_counterexample_batch,
   6.390 -        "Exhaustive_Generators.put_counterexample_batch")
   6.391 -      thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
   6.392 -      (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') [];
   6.393 -  in
   6.394 -    map (fn compile => fn size => compile size |> Option.map (map post_process_term)) compiles
   6.395 -  end;
   6.396 -  
   6.397 -  
   6.398 -(** setup **)
   6.399 -
   6.400 -val setup =
   6.401 -  Datatype.interpretation
   6.402 -    (Quickcheck_Generators.ensure_sort_datatype (@{sort exhaustive}, instantiate_exhaustive_datatype))
   6.403 -  #> setup_smart_quantifier
   6.404 -  #> setup_quickcheck_pretty
   6.405 -  #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
   6.406 -  #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs));
   6.407 -
   6.408 -end;