quickcheck generators for abstract types; tuned

--- a/src/HOL/Quickcheck_Exhaustive.thy	Tue Dec 20 17:22:31 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Tue Dec 20 17:39:56 2011 +0100
@@ -4,7 +4,9 @@
 
 theory Quickcheck_Exhaustive
 imports Quickcheck
-uses ("Tools/Quickcheck/exhaustive_generators.ML")
+uses
+  ("Tools/Quickcheck/exhaustive_generators.ML")
+  ("Tools/Quickcheck/abstract_generators.ML")
 begin
 
 subsection {* basic operations for exhaustive generators *}
@@ -521,7 +523,7 @@
 where
   "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
 
-subsection {* Defining combinators for any first-order data type *}
+subsection {* Defining generators for any first-order data type *}
 
 axiomatization unknown :: 'a
 
@@ -533,6 +535,10 @@
 
 declare [[quickcheck_batch_tester = exhaustive]]
 
+subsection {* Defining generators for abstract types *}
+
+use "Tools/Quickcheck/abstract_generators.ML"
+
 hide_fact orelse_def
 no_notation orelse (infixr "orelse" 55)
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Tue Dec 20 17:39:56 2011 +0100
@@ -0,0 +1,64 @@
+(*  Title:      HOL/Tools/Quickcheck/abstract_generators.ML
+    Author:     Lukas Bulwahn, TU Muenchen
+
+Quickcheck generators for abstract types.
+*)
+
+signature ABSTRACT_GENERATORS =
+sig
+  val quickcheck_generator : string -> term list -> theory -> theory
+end;
+
+structure Abstract_Generators : ABSTRACT_GENERATORS =
+struct
+
+fun check_constrs ctxt tyco constrs =
+  let
+    fun check_type c =
+      case try (dest_Type o body_type o fastype_of) c of
+        NONE => error (Syntax.string_of_term ctxt c ^ " has mismatching result type.")
+      | SOME (tyco', vs) => if not (tyco' = tyco) then
+            error (Syntax.string_of_term ctxt c ^ " has mismatching result type. " ^
+              "Expected type constructor " ^ quote tyco ^ ", but found " ^ quote tyco' ^ ".")
+          else
+            case try (map dest_TFree) vs of
+              NONE => error (Syntax.string_of_term ctxt c ^ " has mismatching result type.")
+            | SOME _ => ()
+  in
+    map check_type constrs
+  end
+  
+fun gen_quickcheck_generator prep_tyco prep_term tyco_raw constrs_raw thy =
+  let
+    val ctxt = Proof_Context.init_global thy
+    val tyco = prep_tyco ctxt tyco_raw
+    val constrs = map (prep_term ctxt) constrs_raw
+    val _ = check_constrs ctxt tyco constrs 
+    val vs = map dest_TFree (snd (dest_Type (body_type (fastype_of (hd constrs)))))
+    val name = Long_Name.base_name tyco 
+    fun mk_dconstrs (Const (s, T)) =
+        (s, map (Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T))
+      | mk_dconstrs t = error (Syntax.string_of_term ctxt t ^
+          " is not a valid constructor for quickcheck_generator, which expects a constant.")
+    fun the_descr thy _ =
+      let
+        val descr = [(0, (tyco, map Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))]
+      in
+        (descr, vs, [tyco], name, ([name], []), ([Type (tyco, map TFree vs)], []))
+      end
+  in
+    Quickcheck_Common.ensure_sort (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}),
+        (the_descr, Exhaustive_Generators.instantiate_full_exhaustive_datatype))
+      Datatype_Aux.default_config [tyco] thy
+  end
+
+val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
+  
+val quickcheck_generator_cmd = gen_quickcheck_generator
+  (fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term
+  
+val _ = Outer_Syntax.command "quickcheck_generator" "define quickcheck generators for abstract types"
+    Keyword.thy_decl (Parse.type_const -- (Args.$$$ "constructors" |-- Parse.$$$ ":" |-- Parse.list1 Parse.term)
+      >> (fn (tyco, constrs) => Toplevel.theory (quickcheck_generator_cmd tyco constrs)))
+
+end;
\ No newline at end of file