quickcheck random can also find potential counterexamples;
authorbulwahn
Thu Dec 01 22:14:35 2011 +0100 (2011-12-01)
changeset 457188979b2463fc8
parent 45717 b4e7b9968e60
child 45719 39c52a820f6e
quickcheck random can also find potential counterexamples;
moved catch_match definition;
split quickcheck setup;
src/HOL/Quickcheck.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/Quickcheck/random_generators.ML
     1.1 --- a/src/HOL/Quickcheck.thy	Thu Dec 01 20:54:48 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck.thy	Thu Dec 01 22:14:35 2011 +0100
     1.3 @@ -5,13 +5,23 @@
     1.4  theory Quickcheck
     1.5  imports Random Code_Evaluation Enum
     1.6  uses
     1.7 -  "Tools/Quickcheck/quickcheck_common.ML"
     1.8 +  ("Tools/Quickcheck/quickcheck_common.ML")
     1.9    ("Tools/Quickcheck/random_generators.ML")
    1.10  begin
    1.11  
    1.12  notation fcomp (infixl "\<circ>>" 60)
    1.13  notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.14  
    1.15 +setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
    1.16 +
    1.17 +subsection {* Catching Match exceptions *}
    1.18 +
    1.19 +definition catch_match :: "term list option => term list option => term list option"
    1.20 +where
    1.21 +  [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
    1.22 +
    1.23 +code_const catch_match 
    1.24 +  (Quickcheck "(_) handle Match => _")
    1.25  
    1.26  subsection {* The @{text random} class *}
    1.27  
    1.28 @@ -128,6 +138,9 @@
    1.29    shows "random_aux k = rhs k"
    1.30    using assms by (rule code_numeral.induct)
    1.31  
    1.32 +subsection {* Deriving random generators for datatypes *}
    1.33 +
    1.34 +use "Tools/Quickcheck/quickcheck_common.ML" 
    1.35  use "Tools/Quickcheck/random_generators.ML"
    1.36  setup Random_Generators.setup
    1.37  
     2.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 20:54:48 2011 +0100
     2.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:14:35 2011 +0100
     2.3 @@ -523,13 +523,6 @@
     2.4  
     2.5  subsection {* Defining combinators for any first-order data type *}
     2.6  
     2.7 -definition catch_match :: "term list option => term list option => term list option"
     2.8 -where
     2.9 -  [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
    2.10 -
    2.11 -code_const catch_match 
    2.12 -  (Quickcheck "(_) handle Match => _")
    2.13 -
    2.14  definition catch_match' :: "term => term => term"
    2.15  where
    2.16    [code del]: "catch_match' t1 t2 = (SOME t. t = t1 \<or> t = t2)"
     3.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 20:54:48 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 22:14:35 2011 +0100
     3.3 @@ -328,12 +328,6 @@
     3.4  
     3.5  fun mk_unknown_term T = HOLogic.reflect_term (Const ("Quickcheck_Exhaustive.unknown", T))
     3.6  
     3.7 -fun mk_safe_if ctxt (cond, then_t, else_t) =
     3.8 -  @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"}
     3.9 -    $ (@{term "If :: bool => term list option => term list option => term list option"}
    3.10 -      $ cond $ then_t $ else_t)
    3.11 -    $ (if Config.get ctxt Quickcheck.potential then else_t else @{term "None :: term list option"});  
    3.12 -
    3.13  fun mk_safe_term t = @{term "Quickcheck_Exhaustive.catch_match' :: term => term => term"}
    3.14        $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)    
    3.15  
    3.16 @@ -352,7 +346,8 @@
    3.17        Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
    3.18          $ lambda free t $ depth
    3.19      val none_t = @{term "None :: term list option"}
    3.20 -    val mk_test_term = mk_test_term lookup mk_exhaustive_closure (mk_safe_if ctxt) none_t return ctxt
    3.21 +    val mk_if = Quickcheck_Common.mk_safe_if ctxt
    3.22 +    val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
    3.23    in lambda depth (mk_test_term t) end
    3.24  
    3.25  fun mk_full_generator_expr ctxt (t, eval_terms) =
    3.26 @@ -378,7 +373,8 @@
    3.27            $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
    3.28              $ lambda free (lambda term_var t)) $ depth
    3.29      val none_t = @{term "None :: term list option"}
    3.30 -    val mk_test_term = mk_test_term lookup mk_exhaustive_closure (mk_safe_if ctxt) none_t return ctxt
    3.31 +    val mk_if = Quickcheck_Common.mk_safe_if ctxt
    3.32 +    val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if none_t return ctxt
    3.33    in lambda depth (mk_test_term t) end
    3.34  
    3.35  fun mk_parametric_generator_expr mk_generator_expr =
     4.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 20:54:48 2011 +0100
     4.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
     4.3 @@ -13,6 +13,7 @@
     4.4      -> (string * sort -> string * sort) option
     4.5    val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
     4.6      -> (typ option * (term * term list)) list list
     4.7 +  val mk_safe_if : Proof.context -> (term * term * term) -> term
     4.8    val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
     4.9    type compile_generator =
    4.10      Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
    4.11 @@ -265,6 +266,14 @@
    4.12      correct_inst_goals
    4.13    end
    4.14  
    4.15 +(* compilation of testing functions *)
    4.16 +
    4.17 +fun mk_safe_if ctxt (cond, then_t, else_t) =
    4.18 +  @{term "Quickcheck.catch_match :: term list option => term list option => term list option"}
    4.19 +    $ (@{term "If :: bool => term list option => term list option => term list option"}
    4.20 +      $ cond $ then_t $ else_t)
    4.21 +    $ (if Config.get ctxt Quickcheck.potential then else_t else @{term "None :: term list option"});  
    4.22 +
    4.23  fun collect_results f [] results = results
    4.24    | collect_results f (t :: ts) results =
    4.25      let
     5.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 20:54:48 2011 +0100
     5.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 22:14:35 2011 +0100
     5.3 @@ -297,8 +297,8 @@
     5.4        (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
     5.5      val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
     5.6      val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
     5.7 -    val check = @{term "If :: bool => term list option => term list option => term list option"}
     5.8 -      $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms);
     5.9 +    val check = Quickcheck_Common.mk_safe_if ctxt (result, @{term "None :: term list option"},
    5.10 +      @{term "Some :: term list => term list option"} $ terms)
    5.11      val return = @{term "Pair :: term list option => Random.seed => term list option * Random.seed"};
    5.12      fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    5.13      fun mk_termtyp T = HOLogic.mk_prodT (T, @{typ "unit => term"});
    5.14 @@ -446,7 +446,6 @@
    5.15  val setup =
    5.16    Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    5.17      (((@{sort typerep}, @{sort term_of}), @{sort random}), instantiate_random_datatype))
    5.18 -  #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
    5.19    #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
    5.20  
    5.21  end;