src/HOL/Smallcheck.thy
author bulwahn
Fri Dec 10 11:42:05 2010 +0100 (2010-12-10)
changeset 41105 a76ee71c3313
parent 41104 013adf7ebd96
child 41177 810a885decee
permissions -rw-r--r--
adding check_all instances for a few more finite types in smallcheck
     1 (* Author: Lukas Bulwahn, TU Muenchen *)
     2 
     3 header {* Another simple counterexample generator *}
     4 
     5 theory Smallcheck
     6 imports Quickcheck
     7 uses ("Tools/smallvalue_generators.ML")
     8 begin
     9 
    10 subsection {* basic operations for generators *}
    11 
    12 definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55)
    13 where
    14   [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)"
    15 
    16 subsection {* small value generator type classes *}
    17 
    18 class small = term_of +
    19 fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    20 
    21 instantiation unit :: small
    22 begin
    23 
    24 definition "small f d = f ()"
    25 
    26 instance ..
    27 
    28 end
    29 
    30 instantiation int :: small
    31 begin
    32 
    33 function small' :: "(int => term list option) => int => int => term list option"
    34 where "small' f d i = (if d < i then None else (case f i of Some t => Some t | None => small' f d (i + 1)))"
    35 by pat_completeness auto
    36 
    37 termination 
    38   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    39 
    40 definition "small f d = small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    41 
    42 instance ..
    43 
    44 end
    45 
    46 instantiation prod :: (small, small) small
    47 begin
    48 
    49 definition
    50   "small f d = small (%x. small (%y. f (x, y)) d) d"
    51 
    52 instance ..
    53 
    54 end
    55 
    56 subsection {* full small value generator type classes *}
    57 
    58 class full_small = term_of +
    59 fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    60 
    61 instantiation unit :: full_small
    62 begin
    63 
    64 definition "full_small f d = f (Code_Evaluation.valtermify ())"
    65 
    66 instance ..
    67 
    68 end
    69 
    70 instantiation int :: full_small
    71 begin
    72 
    73 function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option"
    74   where "full_small' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_small' f d (i + 1)))"
    75 by pat_completeness auto
    76 
    77 termination 
    78   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    79 
    80 definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    81 
    82 instance ..
    83 
    84 end
    85 
    86 instantiation prod :: (full_small, full_small) full_small
    87 begin
    88 
    89 definition
    90   "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
    91     %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
    92 
    93 instance ..
    94 
    95 end
    96 
    97 instantiation "fun" :: ("{equal, full_small}", full_small) full_small
    98 begin
    99 
   100 fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
   101 where
   102   "full_small_fun' f i d = (if i > 1 then
   103     full_small (%(a, at). full_small (%(b, bt).
   104       full_small_fun' (%(g, gt). f (g(a := b),
   105         (%_. let T1 = (Typerep.typerep (TYPE('a)));
   106                  T2 = (Typerep.typerep (TYPE('b)))
   107              in
   108                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   109                  (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   110                     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
   111                        Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   112                (gt ())) (at ())) (bt ())))) (i - 1) d) d) d
   113   else (if i > 0 then
   114     full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
   115 
   116 definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
   117 where
   118   "full_small_fun f d = full_small_fun' f d d" 
   119 
   120 
   121 instance ..
   122 
   123 end
   124 
   125 subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
   126 
   127 
   128 class check_all = enum + term_of +
   129 fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
   130 
   131 fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
   132 where
   133   "check_all_n_lists f n =
   134      (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
   135 
   136 instantiation "fun" :: ("{equal, check_all}", check_all) check_all
   137 begin
   138 
   139 definition mk_map_term :: "'a list \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> unit \<Rightarrow> term"
   140 where
   141   "mk_map_term domm rng T2 =
   142      (%_. let T1 = (Typerep.typerep (TYPE('a)));
   143               T2 = T2 ();
   144               update_term = (%g (a, b).
   145                 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   146                  (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   147                    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
   148                       Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) g) (Code_Evaluation.term_of a)) b)
   149           in
   150              List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip domm (rng ())))"
   151 
   152 definition
   153   "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)))"
   154 
   155 instance ..
   156 
   157 end
   158 
   159 
   160 instantiation unit :: check_all
   161 begin
   162 
   163 definition
   164   "check_all f = f (Code_Evaluation.valtermify ())"
   165 
   166 instance ..
   167 
   168 end
   169 
   170 
   171 instantiation bool :: check_all
   172 begin
   173 
   174 definition
   175   "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
   176 
   177 instance ..
   178 
   179 end
   180 
   181 
   182 instantiation prod :: (check_all, check_all) check_all
   183 begin
   184 
   185 definition
   186   "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 ()))))"
   187 
   188 instance ..
   189 
   190 end
   191 
   192 
   193 instantiation sum :: (check_all, check_all) check_all
   194 begin
   195 
   196 definition
   197   "check_all f = (case check_all (%(a, t). f (Inl a, %_. Code_Evaluation.App (Code_Evaluation.term_of (Inl :: 'a => 'a + 'b)) (t ()))) of Some x' => Some x'
   198              | None => check_all (%(b, t). f (Inr b, %_. Code_Evaluation.App (Code_Evaluation.term_of (Inr :: 'b => 'a + 'b)) (t ()))))"
   199 
   200 instance ..
   201 
   202 end
   203 
   204 instantiation nibble :: check_all
   205 begin
   206 
   207 definition
   208   "check_all f =
   209     f (Code_Evaluation.valtermify Nibble0) orelse
   210     f (Code_Evaluation.valtermify Nibble1) orelse
   211     f (Code_Evaluation.valtermify Nibble2) orelse
   212     f (Code_Evaluation.valtermify Nibble3) orelse
   213     f (Code_Evaluation.valtermify Nibble4) orelse
   214     f (Code_Evaluation.valtermify Nibble5) orelse
   215     f (Code_Evaluation.valtermify Nibble6) orelse
   216     f (Code_Evaluation.valtermify Nibble7) orelse
   217     f (Code_Evaluation.valtermify Nibble8) orelse
   218     f (Code_Evaluation.valtermify Nibble9) orelse
   219     f (Code_Evaluation.valtermify NibbleA) orelse
   220     f (Code_Evaluation.valtermify NibbleB) orelse
   221     f (Code_Evaluation.valtermify NibbleC) orelse
   222     f (Code_Evaluation.valtermify NibbleD) orelse
   223     f (Code_Evaluation.valtermify NibbleE) orelse
   224     f (Code_Evaluation.valtermify NibbleF)"
   225 
   226 instance ..
   227 
   228 end
   229 
   230 
   231 instantiation char :: check_all
   232 begin
   233 
   234 definition
   235   "check_all f = check_all (%(x, t1). check_all (%(y, t2). f (Char x y, %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
   236 
   237 instance ..
   238 
   239 end
   240 
   241 
   242 instantiation option :: (check_all) check_all
   243 begin
   244 
   245 definition
   246   "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App (Code_Evaluation.term_of (Some :: 'a => 'a option)) (t ())))"
   247 
   248 instance ..
   249 
   250 end
   251 
   252 
   253 instantiation Enum.finite_1 :: check_all
   254 begin
   255 
   256 definition
   257   "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
   258 
   259 instance ..
   260 
   261 end
   262 
   263 instantiation Enum.finite_2 :: check_all
   264 begin
   265 
   266 definition
   267   "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))"
   268 
   269 instance ..
   270 
   271 end
   272 
   273 instantiation Enum.finite_3 :: check_all
   274 begin
   275 
   276 definition
   277   "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)))"
   278 
   279 instance ..
   280 
   281 end
   282 
   283 
   284 
   285 subsection {* Defining combinators for any first-order data type *}
   286 
   287 definition catch_match :: "term list option => term list option => term list option"
   288 where
   289   [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
   290 
   291 code_const catch_match 
   292   (SML "(_) handle Match => _")
   293 
   294 use "Tools/smallvalue_generators.ML"
   295 
   296 setup {* Smallvalue_Generators.setup *}
   297 
   298 declare [[quickcheck_tester = exhaustive]]
   299 
   300 hide_fact orelse_def catch_match_def
   301 no_notation orelse (infixr "orelse" 55)
   302 hide_const (open) orelse catch_match mk_map_term check_all_n_lists
   303 
   304 end