adding a exception-safe term reification step in quickcheck; adding examples
authorbulwahn
Wed Nov 30 09:21:09 2011 +0100 (2011-11-30)
changeset 456843d6ee9c7d7ef
parent 45683 805a2acf47fd
child 45685 e2e928af750b
adding a exception-safe term reification step in quickcheck; adding examples
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/ex/Quickcheck_Examples.thy
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Wed Nov 30 09:21:07 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Wed Nov 30 09:21:09 2011 +0100
     1.3 @@ -530,6 +530,15 @@
     1.4  code_const catch_match 
     1.5    (Quickcheck "(_) handle Match => _")
     1.6  
     1.7 +definition catch_match' :: "term => term => term"
     1.8 +where
     1.9 +  [code del]: "catch_match' t1 t2 = (SOME t. t = t1 \<or> t = t2)"
    1.10 +
    1.11 +code_const catch_match'
    1.12 +  (Quickcheck "(_) handle Match => _")
    1.13 +
    1.14 +consts unknown :: "'a" ("?")
    1.15 + 
    1.16  use "Tools/Quickcheck/exhaustive_generators.ML"
    1.17  
    1.18  setup {* Exhaustive_Generators.setup *}
     2.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Nov 30 09:21:07 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Nov 30 09:21:09 2011 +0100
     2.3 @@ -349,6 +349,8 @@
     2.4      val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if none_t return ctxt
     2.5    in lambda depth (mk_test_term t) end
     2.6  
     2.7 +fun mk_unknown_term T = HOLogic.reflect_term (Const ("Quickcheck_Exhaustive.unknown", T))
     2.8 +
     2.9  fun mk_full_generator_expr ctxt (t, eval_terms) =
    2.10    let
    2.11      val thy = Proof_Context.theory_of ctxt
    2.12 @@ -361,9 +363,11 @@
    2.13      val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
    2.14      fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
    2.15      val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
    2.16 -    val appendC = @{term "List.append :: term list => term list => term list"}  
    2.17 +    fun mk_safe_term t = @{term "Quickcheck_Exhaustive.catch_match' :: term => term => term"}
    2.18 +          $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)    
    2.19 +    val appendC = @{term "List.append :: term list => term list => term list"}
    2.20      val return = @{term "Some :: term list => term list option"} $ (appendC $ terms $
    2.21 -      (HOLogic.mk_list @{typ "term"} (map (fn t => HOLogic.mk_term_of (fastype_of t) t) eval_terms)))
    2.22 +      (HOLogic.mk_list @{typ "term"} (map mk_safe_term eval_terms)))
    2.23      fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
    2.24        if Sign.of_sort thy (T, @{sort enum}) then
    2.25          Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
     3.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Wed Nov 30 09:21:07 2011 +0100
     3.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Wed Nov 30 09:21:09 2011 +0100
     3.3 @@ -407,5 +407,24 @@
     3.4  quickcheck[exhaustive, expect = counterexample]
     3.5  oops
     3.6  
     3.7 +subsection {* Examples with underspecified/partial functions *}
     3.8 +
     3.9 +lemma
    3.10 +  "xs = [] ==> hd xs \<noteq> x"
    3.11 +quickcheck[exhaustive, potential = false, expect = no_counterexample]
    3.12 +quickcheck[exhaustive, potential = true, expect = counterexample]
    3.13 +oops
    3.14 +
    3.15 +lemma
    3.16 +  "xs = [] ==> hd xs = x"
    3.17 +quickcheck[exhaustive, potential = false, expect = no_counterexample]
    3.18 +quickcheck[exhaustive, potential = true, expect = counterexample]
    3.19 +oops
    3.20 +
    3.21 +lemma "xs = [] ==> hd xs = x ==> x = y"
    3.22 +quickcheck[exhaustive, potential = false, expect = no_counterexample]
    3.23 +quickcheck[exhaustive, potential = true, expect = counterexample]
    3.24 +oops
    3.25 +
    3.26  
    3.27  end