# HG changeset patch
# User blanchet
# Date 1410177788 -7200
# Node ID a2afad27a0b1ef0f3826a1c080f8c8921b8d7ee8
# Parent  61b852f90161b4643ba599a772a64461a5ef4fc5
wildcards in plugins

diff -r 61b852f90161 -r a2afad27a0b1 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 08 14:03:02 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 08 14:03:08 2014 +0200
@@ -507,7 +507,8 @@
 
 \item
 The @{text "plugins"} option indicates which plugins should be enabled
-(@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
+(@{text only}) or disabled (@{text del}). Wildcards (``@{text *}'') are allowed
+(e.g., @{text "quickcheck_*"}). By default, all plugins are enabled.
 
 \item
 The @{text "discs_sels"} option indicates that discriminators and selectors
@@ -539,7 +540,7 @@
 The optional names preceding the type variables allow to override the default
 names of the set functions (@{text set\<^sub>1_t}, \ldots, @{text set\<^sub>m_t}). Type
 arguments can be marked as dead by entering @{text dead} in front of the
-type variable (e.g., ``@{text "(dead 'a)"}''); otherwise, they are live or dead
+type variable (e.g., @{text "(dead 'a)"}); otherwise, they are live or dead
 (and a set function is generated or not) depending on where they occur in the
 right-hand sides of the definition. Declaring a type argument as dead can speed
 up the type definition but will prevent any later (co)recursion through that
@@ -2652,7 +2653,7 @@
 parenthesized mixfix notation \cite{isabelle-isar-ref}.
 
 Type arguments are live by default; they can be marked as dead by entering
-@{text dead} in front of the type variable (e.g., ``@{text "(dead 'a)"}'')
+@{text dead} in front of the type variable (e.g., @{text "(dead 'a)"})
 instead of an identifier for the corresponding set function. Witnesses can be
 specified by their types. Otherwise, the syntax of @{command bnf_axiomatization}
 is identical to the left-hand side of a @{command datatype_new} or
@@ -2843,9 +2844,9 @@
 
 text {*
 The integration of (co)datatypes with Quickcheck is accomplished by a number of
-plugins that instantiate specific type classes: @{text random},
-@{text exhaustive}, @{text bounded_forall}, @{text full_exhaustive}, and
-@{text narrowing}.
+plugins that instantiate specific type classes: @{text quickcheck_random},
+@{text quickcheck_exhaustive}, @{text quickcheck_bounded_forall},
+@{text quickcheck_full_exhaustive}, and @{text quickcheck_narrowing}.
 *}
 
 
diff -r 61b852f90161 -r a2afad27a0b1 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 08 14:03:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 08 14:03:08 2014 +0200
@@ -35,7 +35,7 @@
     (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory ->
     (term list * thm list) * theory
   val add_primrec_simple: ((binding * typ) * mixfix) list -> term list ->
-    local_theory -> (string list * (term list * (int list * thm list))) * local_theory
+    local_theory -> (string list * (term list * thm list)) * local_theory
 end;
 
 structure BNF_LFP_Compat : BNF_LFP_COMPAT =
@@ -516,7 +516,7 @@
 val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec;
 val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global;
 val add_primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.add_primrec_overloaded;
-val add_primrec_simple = apfst (apsnd (apsnd (apsnd flat o apfst flat))) ooo
+val add_primrec_simple = apfst (apsnd (apsnd (flat o snd))) ooo
   BNF_LFP_Rec_Sugar.add_primrec_simple;
 
 val _ =
diff -r 61b852f90161 -r a2afad27a0b1 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Sep 08 14:03:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Sep 08 14:03:08 2014 +0200
@@ -529,7 +529,11 @@
            error ("primrec error:\n  " ^ str ^ "\nin\n  " ^
              space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns));
 
-val add_primrec_simple = add_primrec_simple' [];
+fun add_primrec_simple fixes ts lthy =
+  add_primrec_simple' [] fixes ts lthy
+  handle OLD_PRIMREC () =>
+    Old_Primrec.add_primrec_simple fixes ts lthy
+    |>> apsnd (apsnd (pair [] o single)) o apfst single;
 
 fun gen_primrec old_primrec prep_spec opts
     (raw_fixes : (binding * 'a option * mixfix) list) raw_specs lthy =
diff -r 61b852f90161 -r a2afad27a0b1 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Sep 08 14:03:02 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Sep 08 14:03:08 2014 +0200
@@ -92,7 +92,19 @@
 structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
 struct
 
-fun map_prod f g (x, y) = (f x, g y)
+fun match_entire_string pat s =
+  let
+    fun match [] [] = true
+      | match [] _ = false
+      | match (ps as #"*" :: ps') cs =
+        match ps' cs orelse (not (null cs) andalso match ps (tl cs))
+      | match _ [] = false
+      | match (p :: ps) (c :: cs) = p = c andalso match ps cs;
+  in
+    match (String.explode pat) (String.explode s)
+  end;
+
+fun map_prod f g (x, y) = (f x, g y);
 
 fun map3 _ [] [] [] = []
   | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
@@ -272,7 +284,8 @@
 val parse_plugins =
   Parse.reserved "plugins" |--
     ((Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --| @{keyword ":"}
-     -- Scan.repeat Parse.short_ident) >> (fn (modif, ss) => modif o member (op =) ss);
+     -- Scan.repeat (Parse.short_ident || Parse.string))
+  >> (fn (modif, pats) => modif o member (uncurry match_entire_string o swap) pats);
 
 fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
 
@@ -291,7 +304,6 @@
   let val (butlast, last) = split_last xs;
   in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end;
 
-(*not eta-converted because of monotype restriction*)
 fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
 fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;