# HG changeset patch
# User bulwahn
# Date 1301986432 -7200
# Node ID 1491b7209e7664286f6843d2c686ae29dca31a8f
# Parent  3bf2eea43dac262225ed5dbd3e40b075b760852a
generalizing ensure_sort_datatype for bounded_forall instances

diff -r 3bf2eea43dac -r 1491b7209e76 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Apr 04 19:09:10 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Apr 05 08:53:52 2011 +0200
@@ -332,8 +332,8 @@
 (** setup **)
 
 val setup =
-  Datatype.interpretation
-    (Quickcheck_Common.ensure_sort_datatype (@{sort exhaustive}, instantiate_exhaustive_datatype))
+  Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+      (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
   #> setup_smart_quantifier
   #> setup_quickcheck_pretty
   #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
diff -r 3bf2eea43dac -r 1491b7209e76 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Apr 04 19:09:10 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Apr 05 08:53:52 2011 +0200
@@ -12,11 +12,12 @@
   val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
     -> (string * sort -> string * sort) option
   val ensure_sort_datatype:
-    sort * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string ->
-      string list * string list -> typ list * typ list -> theory -> theory)
+    ((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list
+      -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory)
     -> Datatype.config -> string list -> theory -> theory
   val gen_mk_parametric_generator_expr :
-   (((Proof.context -> term * term list -> term) * term) * typ) -> Proof.context -> (term * term list) list -> term
+   (((Proof.context -> term * term list -> term) * term) * typ)
+     -> Proof.context -> (term * term list) list -> term
   val post_process_term : term -> term
 end;
 
@@ -86,25 +87,20 @@
   in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
   end handle Sorts.CLASS_ERROR _ => NONE;
 
-fun ensure_sort_datatype (sort, instantiate_datatype) config raw_tycos thy =
+fun ensure_sort_datatype (((sort_vs, aux_sort), sort), instantiate_datatype) config raw_tycos thy =
   let
     val algebra = Sign.classes_of thy;
-    val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
-      Datatype.the_descr thy raw_tycos;
-    val typerep_vs = (map o apsnd)
-      (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
-    val sort_insts = (map (rpair sort) o flat o maps snd o maps snd)
-      (Datatype_Aux.interpret_construction descr typerep_vs
-        { atyp = single, dtyp = (K o K o K) [] });
-    val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
-      (Datatype_Aux.interpret_construction descr typerep_vs
-        { atyp = K [], dtyp = K o K });
-    val has_inst = exists (fn tyco =>
-      can (Sorts.mg_domain algebra tyco) sort) tycos;
+    val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = Datatype.the_descr thy raw_tycos
+    val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
+    fun insts_of sort constr  = (map (rpair sort) o flat o maps snd o maps snd)
+      (Datatype_Aux.interpret_construction descr vs constr)
+    val insts = insts_of sort  { atyp = single, dtyp = (K o K o K) [] }
+      @ insts_of aux_sort { atyp = K [], dtyp = K o K }
+    val has_inst = exists (fn tyco => can (Sorts.mg_domain algebra tyco) sort) tycos;
   in if has_inst then thy
-    else case perhaps_constrain thy (sort_insts @ term_of_insts) typerep_vs
+    else case perhaps_constrain thy insts vs
      of SOME constrain => instantiate_datatype config descr
-          (map constrain typerep_vs) tycos prfx (names, auxnames)
+          (map constrain vs) tycos prfx (names, auxnames)
             ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
       | NONE => thy
   end;
diff -r 3bf2eea43dac -r 1491b7209e76 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Apr 04 19:09:10 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Apr 05 08:53:52 2011 +0200
@@ -442,7 +442,8 @@
 (** setup **)
 
 val setup =
-  Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype (@{sort random}, instantiate_random_datatype))
+  Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+    (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
   #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
   #> Context.theory_map
     (Quickcheck.add_generator ("random", compile_generator_expr));