# HG changeset patch
# User bulwahn
# Date 1324398151 -3600
# Node ID 473b744c23f2569ce39257e3a9bca8b464a380ee
# Parent  63cc69265acf95280109de53529951b8fb1e949b
generalize ensure_sort_datatype to ensure_sort  in quickcheck_common to allow generators for abstract types;
adding common datatype interpretation to quickcheck_common;

diff -r 63cc69265acf -r 473b744c23f2 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Dec 20 14:43:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Dec 20 17:22:31 2011 +0100
@@ -500,14 +500,12 @@
 (* setup *)
 
 val setup_exhaustive_datatype_interpretation =
-  Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
-      (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
+  Quickcheck_Common.datatype_interpretation (@{sort exhaustive}, instantiate_exhaustive_datatype)
 
 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
 
 val setup =
-  Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
-      (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
+  Quickcheck_Common.datatype_interpretation (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
 (* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
       (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
   #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
diff -r 63cc69265acf -r 473b744c23f2 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Dec 20 14:43:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Dec 20 17:22:31 2011 +0100
@@ -501,8 +501,7 @@
 val setup =
   Code.datatype_interpretation ensure_partial_term_of
   #> Code.datatype_interpretation ensure_partial_term_of_code
-  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
-    (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
+  #> Quickcheck_Common.datatype_interpretation (@{sort narrowing}, instantiate_narrowing_datatype)
   #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
     
 end;
diff -r 63cc69265acf -r 473b744c23f2 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Dec 20 14:43:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Dec 20 17:22:31 2011 +0100
@@ -21,10 +21,16 @@
   val generator_test_goal_terms :
     string * compile_generator -> Proof.context -> bool -> (string * typ) list
     -> (term * term list) list -> Quickcheck.result list
-  val ensure_sort_datatype:
-    ((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list
-      -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory)
+  type instantiation = Datatype.config -> Datatype.descr -> (string * sort) list
+     -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+  val ensure_sort :
+    (((sort * sort) * sort) *
+      ((theory -> string list -> Datatype_Aux.descr * (string * sort) list * string list
+        * string * (string list * string list) * (typ list * typ list)) * instantiation))
     -> Datatype.config -> string list -> theory -> theory
+  val ensure_common_sort_datatype :
+    (sort * instantiation) -> Datatype.config -> string list -> theory -> theory
+  val datatype_interpretation : (sort * instantiation) -> theory -> theory
   val gen_mk_parametric_generator_expr :
    (((Proof.context -> term * term list -> term) * term) * typ)
      -> Proof.context -> (term * term list) list -> term
@@ -379,6 +385,9 @@
 
 (** ensuring sort constraints **)
 
+type instantiation = Datatype.config -> Datatype.descr -> (string * sort) list
+  -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+
 fun perhaps_constrain thy insts raw_vs =
   let
     fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) 
@@ -389,10 +398,10 @@
   in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
   end handle Sorts.CLASS_ERROR _ => NONE;
 
-fun ensure_sort_datatype (((sort_vs, aux_sort), sort), instantiate_datatype) config raw_tycos thy =
+fun ensure_sort (((sort_vs, aux_sort), sort), (the_descr, instantiate)) 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 (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = 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)
@@ -401,11 +410,16 @@
     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 insts vs
-     of SOME constrain => instantiate_datatype config descr
+     of SOME constrain => instantiate config descr
           (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;
+
+fun ensure_common_sort_datatype (sort, instantiate) =
+  ensure_sort (((@{sort typerep}, @{sort term_of}), sort), (Datatype.the_descr, instantiate))
+
+val datatype_interpretation = Datatype.interpretation o ensure_common_sort_datatype
   
 (** generic parametric compilation **)
 
diff -r 63cc69265acf -r 473b744c23f2 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Dec 20 14:43:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Dec 20 17:22:31 2011 +0100
@@ -460,8 +460,7 @@
 val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
 
 val setup =
-  Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
-    (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
+  Quickcheck_Common.datatype_interpretation (@{sort random}, instantiate_random_datatype)
   #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
 
 end;