--- a/src/HOL/Library/Dlist.thy Tue Feb 21 13:10:13 2012 +0100
+++ b/src/HOL/Library/Dlist.thy Tue Feb 21 13:15:25 2012 +0100
@@ -182,7 +182,7 @@
subsection {* Quickcheck generators *}
-quickcheck_generator dlist constructors: empty, insert
+quickcheck_generator dlist predicate: distinct constructors: empty, insert
hide_const (open) member fold foldr empty insert remove map filter null member length fold
--- a/src/HOL/Library/RBT.thy Tue Feb 21 13:10:13 2012 +0100
+++ b/src/HOL/Library/RBT.thy Tue Feb 21 13:15:25 2012 +0100
@@ -171,6 +171,6 @@
subsection {* Quickcheck generators *}
-quickcheck_generator rbt constructors: empty, insert
+quickcheck_generator rbt predicate: is_rbt constructors: empty, insert
end
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Tue Feb 21 13:10:13 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Tue Feb 21 13:15:25 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,19 +28,20 @@
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
+ val opt_pred = Option.map (prep_term ctxt) opt_pred_raw
val constrs = map (prep_term ctxt) constrs_raw
- val _ = check_constrs ctxt tyco constrs
+ 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 _ =
+ fun the_descr _ _ =
let
val descr = [(0, (tyco, map Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))]
in
@@ -53,7 +54,9 @@
in
thy
|> ensure_sort (@{sort full_exhaustive}, Exhaustive_Generators.instantiate_full_exhaustive_datatype)
+ |> ensure_sort (@{sort exhaustive}, Exhaustive_Generators.instantiate_exhaustive_datatype)
|> ensure_sort (@{sort random}, Random_Generators.instantiate_random_datatype)
+ |> (case opt_pred of NONE => I | SOME t => Context.theory_map (Quickcheck_Common.register_predicate (t, tyco)))
end
val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
@@ -62,7 +65,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
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Feb 21 13:10:13 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Tue Feb 21 13:15:25 2012 +0100
@@ -23,6 +23,9 @@
val instantiate_full_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
(string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+ val instantiate_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
+ (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+
end;
structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Feb 21 13:10:13 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Feb 21 13:15:25 2012 +0100
@@ -14,6 +14,7 @@
-> (string * sort -> string * sort) option
val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
-> (typ option * (term * term list)) list list
+ val register_predicate : term * string -> Context.generic -> Context.generic
val mk_safe_if : term -> term -> term * term * (bool -> term) -> bool -> term
val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
type result = (bool * term list) option * Quickcheck.report option
@@ -96,9 +97,11 @@
val _ = Quickcheck.verbose_message ctxt
("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
val _ = current_size := k
- val ((result, report), timing) =
+ val ((result, report), time) =
cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1])
- val _ = Quickcheck.add_timing timing current_result
+ val _ = if Config.get ctxt Quickcheck.timing then
+ Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
+ val _ = Quickcheck.add_timing time current_result
val _ = Quickcheck.add_report k report current_result
in
case result of
@@ -277,6 +280,37 @@
subst_bounds (map Free (rev vs'), body)
end
+
+structure Subtype_Predicates = Generic_Data
+(
+ type T = (term * string) list
+ val empty = []
+ val extend = I
+ val merge = AList.merge (op =) (K true)
+)
+
+val register_predicate = Subtype_Predicates.map o AList.update (op =)
+
+fun subtype_preprocess ctxt (T, (t, ts)) =
+ let
+ val preds = Subtype_Predicates.get (Context.Proof ctxt)
+ fun matches (p $ x) = AList.defined Term.could_unify preds p
+ fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p)
+ fun subst_of (tyco, v as Free (x, repT)) =
+ let
+ val [(info, _)] = Typedef.get_info ctxt tyco
+ val repT' = Logic.varifyT_global (#rep_type info)
+ val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty
+ val absT = Envir.subst_type substT (Logic.varifyT_global (#abs_type info))
+ in (v, Const (#Rep_name info, absT --> repT) $ Free (x, absT)) end
+ val (prems, concl) = strip_imp t
+ val subst = map subst_of (map_filter get_match prems)
+ val t' = Term.subst_free subst
+ (fold_rev (curry HOLogic.mk_imp) (filter_out matches prems) concl)
+ in
+ (T, (t', ts))
+ end
+
(* instantiation of type variables with concrete types *)
fun instantiate_goals lthy insts goals =
@@ -333,6 +367,7 @@
fun generator_test_goal_terms generator ctxt catch_code_errors insts goals =
let
+ val use_subtype = Config.get ctxt Quickcheck.use_subtype
fun add_eval_term t ts = if is_Free t then ts else ts @ [t]
fun add_equation_eval_terms (t, eval_terms) =
case try HOLogic.dest_eq (snd (strip_imp t)) of
@@ -343,6 +378,7 @@
[(NONE, t)] => test_term generator ctxt catch_code_errors t
| ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts)
val goals' = instantiate_goals ctxt insts goals
+ |> (if use_subtype then map (map (subtype_preprocess ctxt)) else I)
|> map (map (apsnd add_equation_eval_terms))
in
if Config.get ctxt Quickcheck.finite_types then
--- a/src/Tools/quickcheck.ML Tue Feb 21 13:10:13 2012 +0100
+++ b/src/Tools/quickcheck.ML Tue Feb 21 13:15:25 2012 +0100
@@ -19,13 +19,14 @@
val depth : int Config.T
val no_assms : bool Config.T
val report : bool Config.T
+ val timeout : real Config.T
val timing : bool Config.T
val genuine_only : bool Config.T
val abort_potential : bool Config.T
val quiet : bool Config.T
val verbose : bool Config.T
- val timeout : real Config.T
- val allow_function_inversion : bool Config.T;
+ val use_subtype : bool Config.T
+ val allow_function_inversion : bool Config.T
val finite_types : bool Config.T
val finite_type_size : int Config.T
val set_active_testers: string list -> Context.generic -> Context.generic
@@ -177,11 +178,16 @@
val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
+val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
+
val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false)
+
val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false)
-val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
+
+val use_subtype = Attrib.setup_config_bool @{binding quickcheck_use_subtype} (K false)
+
val allow_function_inversion =
Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false)
val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true)
@@ -438,6 +444,7 @@
| parse_test_param ("abort_potential", [arg]) = apsnd (Config.put_generic abort_potential (read_bool arg))
| parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
| parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
+ | parse_test_param ("use_subtype", [arg]) = apsnd (Config.put_generic use_subtype (read_bool arg))
| parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
| parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
| parse_test_param ("allow_function_inversion", [arg]) =