# HG changeset patch # User bulwahn # Date 1322774075 -3600 # Node ID 8979b2463fc8938054e9ee7e58bf2b39912309dd # Parent b4e7b9968e60dfefa1363b9f857edb98faf20827 quickcheck random can also find potential counterexamples; moved catch_match definition; split quickcheck setup; diff -r b4e7b9968e60 -r 8979b2463fc8 src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Thu Dec 01 20:54:48 2011 +0100 +++ b/src/HOL/Quickcheck.thy Thu Dec 01 22:14:35 2011 +0100 @@ -5,13 +5,23 @@ theory Quickcheck imports Random Code_Evaluation Enum uses - "Tools/Quickcheck/quickcheck_common.ML" + ("Tools/Quickcheck/quickcheck_common.ML") ("Tools/Quickcheck/random_generators.ML") begin notation fcomp (infixl "\>" 60) notation scomp (infixl "\\" 60) +setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *} + +subsection {* Catching Match exceptions *} + +definition catch_match :: "term list option => term list option => term list option" +where + [code del]: "catch_match t1 t2 = (SOME t. t = t1 \ t = t2)" + +code_const catch_match + (Quickcheck "(_) handle Match => _") subsection {* The @{text random} class *} @@ -128,6 +138,9 @@ shows "random_aux k = rhs k" using assms by (rule code_numeral.induct) +subsection {* Deriving random generators for datatypes *} + +use "Tools/Quickcheck/quickcheck_common.ML" use "Tools/Quickcheck/random_generators.ML" setup Random_Generators.setup diff -r b4e7b9968e60 -r 8979b2463fc8 src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Thu Dec 01 20:54:48 2011 +0100 +++ b/src/HOL/Quickcheck_Exhaustive.thy Thu Dec 01 22:14:35 2011 +0100 @@ -523,13 +523,6 @@ subsection {* Defining combinators for any first-order data type *} -definition catch_match :: "term list option => term list option => term list option" -where - [code del]: "catch_match t1 t2 = (SOME t. t = t1 \ t = t2)" - -code_const catch_match - (Quickcheck "(_) handle Match => _") - definition catch_match' :: "term => term => term" where [code del]: "catch_match' t1 t2 = (SOME t. t = t1 \ t = t2)" diff -r b4e7b9968e60 -r 8979b2463fc8 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Thu Dec 01 20:54:48 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Thu Dec 01 22:14:35 2011 +0100 @@ -328,12 +328,6 @@ fun mk_unknown_term T = HOLogic.reflect_term (Const ("Quickcheck_Exhaustive.unknown", T)) -fun mk_safe_if ctxt (cond, then_t, else_t) = - @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} - $ (@{term "If :: bool => term list option => term list option => term list option"} - $ cond $ then_t $ else_t) - $ (if Config.get ctxt Quickcheck.potential then else_t else @{term "None :: term list option"}); - fun mk_safe_term t = @{term "Quickcheck_Exhaustive.catch_match' :: term => term => term"} $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t) @@ -352,7 +346,8 @@ Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T) $ lambda free t $ depth val none_t = @{term "None :: term list option"} - val mk_test_term = mk_test_term lookup mk_exhaustive_closure (mk_safe_if ctxt) none_t return ctxt + val mk_if = Quickcheck_Common.mk_safe_if ctxt + val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt in lambda depth (mk_test_term t) end fun mk_full_generator_expr ctxt (t, eval_terms) = @@ -378,7 +373,8 @@ $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) $ lambda free (lambda term_var t)) $ depth val none_t = @{term "None :: term list option"} - val mk_test_term = mk_test_term lookup mk_exhaustive_closure (mk_safe_if ctxt) none_t return ctxt + val mk_if = Quickcheck_Common.mk_safe_if ctxt + val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt in lambda depth (mk_test_term t) end fun mk_parametric_generator_expr mk_generator_expr = diff -r b4e7b9968e60 -r 8979b2463fc8 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Dec 01 20:54:48 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Dec 01 22:14:35 2011 +0100 @@ -13,6 +13,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 mk_safe_if : Proof.context -> (term * term * term) -> term val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list type compile_generator = Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option @@ -265,6 +266,14 @@ correct_inst_goals end +(* compilation of testing functions *) + +fun mk_safe_if ctxt (cond, then_t, else_t) = + @{term "Quickcheck.catch_match :: term list option => term list option => term list option"} + $ (@{term "If :: bool => term list option => term list option => term list option"} + $ cond $ then_t $ else_t) + $ (if Config.get ctxt Quickcheck.potential then else_t else @{term "None :: term list option"}); + fun collect_results f [] results = results | collect_results f (t :: ts) results = let diff -r b4e7b9968e60 -r 8979b2463fc8 src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Thu Dec 01 20:54:48 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Thu Dec 01 22:14:35 2011 +0100 @@ -297,8 +297,8 @@ (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts; val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds); val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds); - val check = @{term "If :: bool => term list option => term list option => term list option"} - $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms); + val check = Quickcheck_Common.mk_safe_if ctxt (result, @{term "None :: term list option"}, + @{term "Some :: term list => term list option"} $ terms) val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"}; fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"}); @@ -446,7 +446,6 @@ val setup = Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype)) - #> Code_Target.extend_target (target, (Code_Runtime.target, K I)) #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals))); end;