# HG changeset patch
# User bulwahn
# Date 1329819948 -3600
# Node ID daa915508f63375c10106fe1d9b33e2738c9a4d0
# Parent  092f4eca98485add0d670d01abbde4ca76dd1bf3
adding parsing of an optional predicate with quickcheck_generator command

diff -r 092f4eca9848 -r daa915508f63 src/HOL/Tools/Quickcheck/abstract_generators.ML
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Tue Feb 21 11:08:05 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Tue Feb 21 11:25:48 2012 +0100
@@ -6,7 +6,7 @@
 
 signature ABSTRACT_GENERATORS =
 sig
-  val quickcheck_generator : string -> term list -> theory -> theory
+  val quickcheck_generator : string -> term option -> term list -> theory -> theory
 end;
 
 structure Abstract_Generators : ABSTRACT_GENERATORS =
@@ -28,7 +28,7 @@
     map check_type constrs
   end
   
-fun gen_quickcheck_generator prep_tyco prep_term tyco_raw constrs_raw thy =
+fun gen_quickcheck_generator prep_tyco prep_term tyco_raw opt_pred_raw constrs_raw thy =
   let
     val ctxt = Proof_Context.init_global thy
     val tyco = prep_tyco ctxt tyco_raw
@@ -40,7 +40,7 @@
         (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 _ =
+    fun the_descr _ _ =
       let
         val descr = [(0, (tyco, map Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))]
       in
@@ -62,7 +62,10 @@
   (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)))
+    Keyword.thy_decl ((Parse.type_const --
+      Scan.option (Args.$$$ "predicate" |-- Parse.$$$ ":" |-- Parse.term)) --
+      (Args.$$$ "constructors" |-- Parse.$$$ ":" |-- Parse.list1 Parse.term)
+      >> (fn ((tyco, opt_pred), constrs) =>
+        Toplevel.theory (quickcheck_generator_cmd tyco opt_pred constrs)))
 
 end;
\ No newline at end of file