# HG changeset patch # User bulwahn # Date 1291828023 -3600 # Node ID a549ff1d40706ea56ac3fbc879d6c79df58d5133 # Parent a434f89a9962347a31ca0f38454f99fd608de5fc adding a smarter enumeration scheme for finite functions diff -r a434f89a9962 -r a549ff1d4070 src/HOL/Enum.thy --- a/src/HOL/Enum.thy Wed Dec 08 16:47:57 2010 +0100 +++ b/src/HOL/Enum.thy Wed Dec 08 18:07:03 2010 +0100 @@ -545,7 +545,7 @@ end -hide_const a\<^isub>1 +hide_const (open) a\<^isub>1 datatype finite_2 = a\<^isub>1 | a\<^isub>2 @@ -598,7 +598,7 @@ end -hide_const a\<^isub>1 a\<^isub>2 +hide_const (open) a\<^isub>1 a\<^isub>2 datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 @@ -651,7 +651,7 @@ end -hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 +hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 @@ -687,7 +687,7 @@ end -hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 +hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5 @@ -724,10 +724,10 @@ end -hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5 +hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5 -hide_type finite_1 finite_2 finite_3 finite_4 finite_5 +hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5 hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product end diff -r a434f89a9962 -r a549ff1d4070 src/HOL/Smallcheck.thy --- a/src/HOL/Smallcheck.thy Wed Dec 08 16:47:57 2010 +0100 +++ b/src/HOL/Smallcheck.thy Wed Dec 08 18:07:03 2010 +0100 @@ -117,6 +117,92 @@ end +subsubsection {* A smarter enumeration scheme for functions over finite datatypes *} + + +class check_all = enum + term_of + +fixes check_all :: "('a * (unit \ term) \ term list option) \ term list option" + +fun check_all_n_lists :: "(('a :: check_all) list * (unit \ term list) \ term list option) \ code_numeral \ term list option" +where + "check_all_n_lists f n = + (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))" + +instantiation "fun" :: ("{equal, enum, check_all}", "{enum, term_of, check_all}") check_all +begin + +definition mk_map_term :: "'a list \ (unit \ term list) \ (unit \ typerep) \ unit \ term" +where + "mk_map_term domm rng T2 = + (%_. let T1 = (Typerep.typerep (TYPE('a))); + T2 = T2 (); + update_term = (%g (a, b). + Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App + (Code_Evaluation.Const (STR ''Fun.fun_upd'') + (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], + Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) g) (Code_Evaluation.term_of a)) b) + in + List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip domm (rng ())))" + +definition + "check_all f = check_all_n_lists (\(ys, yst). f (the o map_of (zip (Enum.enum\'a list) ys), mk_map_term (Enum.enum::'a list) yst (%_. Typerep.typerep (TYPE('b))))) (Code_Numeral.of_nat (length (Enum.enum :: 'a list)))" + +instance .. + +end + +instantiation bool :: check_all +begin + +definition + "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \ Some x' | None \ f (Code_Evaluation.valtermify True))" + +instance .. + +end + +instantiation prod :: (check_all, check_all) check_all +begin + +definition + "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 ()))))" + +instance .. + +end + +instantiation Enum.finite_1 :: check_all +begin + +definition + "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)" + +instance .. + +end + +instantiation Enum.finite_2 :: check_all +begin + +definition + "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1) of Some x' \ Some x' | None \ f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))" + +instance .. + +end + +instantiation Enum.finite_3 :: check_all +begin + +definition + "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1) of Some x' \ Some x' | None \ (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2) of Some x' \ Some x' | None \ f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3)))" + +instance .. + +end + + + subsection {* Defining combinators for any first-order data type *} definition orelse :: "'a option => 'a option => 'a option" @@ -138,6 +224,6 @@ declare [[quickcheck_tester = exhaustive]] hide_fact orelse_def catch_match_def -hide_const (open) orelse catch_match +hide_const (open) orelse catch_match mk_map_term check_all_n_lists end \ No newline at end of file diff -r a434f89a9962 -r a549ff1d4070 src/HOL/Tools/smallvalue_generators.ML --- a/src/HOL/Tools/smallvalue_generators.ML Wed Dec 08 16:47:57 2010 +0100 +++ b/src/HOL/Tools/smallvalue_generators.ML Wed Dec 08 18:07:03 2010 +0100 @@ -81,7 +81,10 @@ fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"}) --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"} - + +fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"}) + --> @{typ "Code_Evaluation.term list option"} + fun mk_equations thy descr vs tycos smalls (Ts, Us) = let fun mk_small_call T = @@ -217,6 +220,7 @@ fun mk_smart_generator_expr ctxt t = let + val thy = ProofContext.theory_of ctxt val ((vnames, Ts), t') = apfst split_list (strip_abs t) val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt val (names, ctxt'') = Variable.variant_fixes vnames ctxt' @@ -229,9 +233,14 @@ val (assms, concl) = strip_imp (subst_bounds (rev frees, t')) val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars) fun mk_small_closure (free as Free (_, T), term_var) t = - Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T) - $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) - $ lambda free (lambda term_var t)) $ depth + if Sign.of_sort thy (T, @{sort enum}) then + Const (@{const_name "Smallcheck.check_all_class.check_all"}, check_allT T) + $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) + $ lambda free (lambda term_var t)) + else + Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T) + $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) + $ lambda free (lambda term_var t)) $ depth fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v) val none_t = @{term "None :: term list option"} fun mk_safe_if (cond, then_t, else_t) =