# 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;