adding a smarter enumeration scheme for finite functions
authorbulwahn
Wed Dec 08 18:07:03 2010 +0100 (2010-12-08)
changeset 41085a549ff1d4070
parent 41084 a434f89a9962
child 41086 b4cccce25d9a
adding a smarter enumeration scheme for finite functions
src/HOL/Enum.thy
src/HOL/Smallcheck.thy
src/HOL/Tools/smallvalue_generators.ML
     1.1 --- a/src/HOL/Enum.thy	Wed Dec 08 16:47:57 2010 +0100
     1.2 +++ b/src/HOL/Enum.thy	Wed Dec 08 18:07:03 2010 +0100
     1.3 @@ -545,7 +545,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -hide_const a\<^isub>1
     1.8 +hide_const (open) a\<^isub>1
     1.9  
    1.10  datatype finite_2 = a\<^isub>1 | a\<^isub>2
    1.11  
    1.12 @@ -598,7 +598,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -hide_const a\<^isub>1 a\<^isub>2
    1.17 +hide_const (open) a\<^isub>1 a\<^isub>2
    1.18  
    1.19  
    1.20  datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
    1.21 @@ -651,7 +651,7 @@
    1.22  
    1.23  end
    1.24  
    1.25 -hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3
    1.26 +hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3
    1.27  
    1.28  
    1.29  datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
    1.30 @@ -687,7 +687,7 @@
    1.31  
    1.32  end
    1.33  
    1.34 -hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
    1.35 +hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
    1.36  
    1.37  
    1.38  datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
    1.39 @@ -724,10 +724,10 @@
    1.40  
    1.41  end
    1.42  
    1.43 -hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
    1.44 +hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
    1.45  
    1.46  
    1.47 -hide_type finite_1 finite_2 finite_3 finite_4 finite_5
    1.48 +hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
    1.49  hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product
    1.50  
    1.51  end
     2.1 --- a/src/HOL/Smallcheck.thy	Wed Dec 08 16:47:57 2010 +0100
     2.2 +++ b/src/HOL/Smallcheck.thy	Wed Dec 08 18:07:03 2010 +0100
     2.3 @@ -117,6 +117,92 @@
     2.4  
     2.5  end
     2.6  
     2.7 +subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
     2.8 +
     2.9 +
    2.10 +class check_all = enum + term_of +
    2.11 +fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
    2.12 +
    2.13 +fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    2.14 +where
    2.15 +  "check_all_n_lists f n =
    2.16 +     (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
    2.17 +
    2.18 +instantiation "fun" :: ("{equal, enum, check_all}", "{enum, term_of, check_all}") check_all
    2.19 +begin
    2.20 +
    2.21 +definition mk_map_term :: "'a list \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> unit \<Rightarrow> term"
    2.22 +where
    2.23 +  "mk_map_term domm rng T2 =
    2.24 +     (%_. let T1 = (Typerep.typerep (TYPE('a)));
    2.25 +              T2 = T2 ();
    2.26 +              update_term = (%g (a, b).
    2.27 +                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
    2.28 +                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
    2.29 +                   (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
    2.30 +                      Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) g) (Code_Evaluation.term_of a)) b)
    2.31 +          in
    2.32 +             List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip domm (rng ())))"
    2.33 +
    2.34 +definition
    2.35 +  "check_all f = check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip (Enum.enum\<Colon>'a list) ys), mk_map_term (Enum.enum::'a list) yst (%_. Typerep.typerep (TYPE('b))))) (Code_Numeral.of_nat (length (Enum.enum :: 'a list)))"
    2.36 +
    2.37 +instance ..
    2.38 +
    2.39 +end
    2.40 +
    2.41 +instantiation bool :: check_all
    2.42 +begin
    2.43 +
    2.44 +definition
    2.45 +  "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
    2.46 +
    2.47 +instance ..
    2.48 +
    2.49 +end
    2.50 +
    2.51 +instantiation prod :: (check_all, check_all) check_all
    2.52 +begin
    2.53 +
    2.54 +definition
    2.55 +  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))))"
    2.56 +
    2.57 +instance ..
    2.58 +
    2.59 +end
    2.60 +
    2.61 +instantiation Enum.finite_1 :: check_all
    2.62 +begin
    2.63 +
    2.64 +definition
    2.65 +  "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
    2.66 +
    2.67 +instance ..
    2.68 +
    2.69 +end
    2.70 +
    2.71 +instantiation Enum.finite_2 :: check_all
    2.72 +begin
    2.73 +
    2.74 +definition
    2.75 +  "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
    2.76 +
    2.77 +instance ..
    2.78 +
    2.79 +end
    2.80 +
    2.81 +instantiation Enum.finite_3 :: check_all
    2.82 +begin
    2.83 +
    2.84 +definition
    2.85 +  "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3)))"
    2.86 +
    2.87 +instance ..
    2.88 +
    2.89 +end
    2.90 +
    2.91 +
    2.92 +
    2.93  subsection {* Defining combinators for any first-order data type *}
    2.94  
    2.95  definition orelse :: "'a option => 'a option => 'a option"
    2.96 @@ -138,6 +224,6 @@
    2.97  declare [[quickcheck_tester = exhaustive]]
    2.98  
    2.99  hide_fact orelse_def catch_match_def
   2.100 -hide_const (open) orelse catch_match
   2.101 +hide_const (open) orelse catch_match mk_map_term check_all_n_lists
   2.102  
   2.103  end
   2.104 \ No newline at end of file
     3.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 08 16:47:57 2010 +0100
     3.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 08 18:07:03 2010 +0100
     3.3 @@ -81,7 +81,10 @@
     3.4  
     3.5  fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
     3.6    --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
     3.7 - 
     3.8 +
     3.9 +fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    3.10 +  --> @{typ "Code_Evaluation.term list option"}
    3.11 +
    3.12  fun mk_equations thy descr vs tycos smalls (Ts, Us) =
    3.13    let
    3.14      fun mk_small_call T =
    3.15 @@ -217,6 +220,7 @@
    3.16  
    3.17  fun mk_smart_generator_expr ctxt t =
    3.18    let
    3.19 +    val thy = ProofContext.theory_of ctxt
    3.20      val ((vnames, Ts), t') = apfst split_list (strip_abs t)
    3.21      val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt
    3.22      val (names, ctxt'') = Variable.variant_fixes vnames ctxt'
    3.23 @@ -229,9 +233,14 @@
    3.24      val (assms, concl) = strip_imp (subst_bounds (rev frees, t'))
    3.25      val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
    3.26      fun mk_small_closure (free as Free (_, T), term_var) t =
    3.27 -      Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
    3.28 -        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
    3.29 -          $ lambda free (lambda term_var t)) $ depth
    3.30 +      if Sign.of_sort thy (T, @{sort enum}) then
    3.31 +        Const (@{const_name "Smallcheck.check_all_class.check_all"}, check_allT T)
    3.32 +          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
    3.33 +            $ lambda free (lambda term_var t))
    3.34 +      else
    3.35 +        Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
    3.36 +          $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
    3.37 +            $ lambda free (lambda term_var t)) $ depth
    3.38      fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
    3.39      val none_t = @{term "None :: term list option"}
    3.40      fun mk_safe_if (cond, then_t, else_t) =