src/HOL/Quickcheck_Narrowing.thy
author haftmann
Fri Feb 15 08:31:31 2013 +0100 (2013-02-15)
changeset 51143 0a2371e7ced3
parent 50046 0051dc4f301f
child 52435 6646bb548c6b
permissions -rw-r--r--
two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one
     1 (* Author: Lukas Bulwahn, TU Muenchen *)
     2 
     3 header {* Counterexample generator performing narrowing-based testing *}
     4 
     5 theory Quickcheck_Narrowing
     6 imports Quickcheck_Exhaustive
     7 keywords "find_unused_assms" :: diag
     8 begin
     9 
    10 subsection {* Counterexample generator *}
    11 
    12 subsubsection {* Code generation setup *}
    13 
    14 setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *}
    15 
    16 code_type typerep
    17   (Haskell_Quickcheck "Typerep")
    18 
    19 code_const Typerep.Typerep
    20   (Haskell_Quickcheck "Typerep")
    21 
    22 code_type integer
    23   (Haskell_Quickcheck "Prelude.Int")
    24 
    25 code_reserved Haskell_Quickcheck Typerep
    26 
    27 
    28 subsubsection {* Narrowing's deep representation of types and terms *}
    29 
    30 datatype narrowing_type = Narrowing_sum_of_products "narrowing_type list list"
    31 datatype narrowing_term = Narrowing_variable "integer list" narrowing_type | Narrowing_constructor integer "narrowing_term list"
    32 datatype 'a narrowing_cons = Narrowing_cons narrowing_type "(narrowing_term list => 'a) list"
    33 
    34 primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
    35 where
    36   "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (%c. f o c) cs)"
    37 
    38 subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *}
    39 
    40 class partial_term_of = typerep +
    41   fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term"
    42 
    43 lemma partial_term_of_anything: "partial_term_of x nt \<equiv> t"
    44   by (rule eq_reflection) (cases "partial_term_of x nt", cases t, simp)
    45  
    46 subsubsection {* Auxilary functions for Narrowing *}
    47 
    48 consts nth :: "'a list => integer => 'a"
    49 
    50 code_const nth (Haskell_Quickcheck infixl 9  "!!")
    51 
    52 consts error :: "char list => 'a"
    53 
    54 code_const error (Haskell_Quickcheck "error")
    55 
    56 consts toEnum :: "integer => char"
    57 
    58 code_const toEnum (Haskell_Quickcheck "Prelude.toEnum")
    59 
    60 consts marker :: "char"
    61 
    62 code_const marker (Haskell_Quickcheck "''\\0'")
    63 
    64 subsubsection {* Narrowing's basic operations *}
    65 
    66 type_synonym 'a narrowing = "integer => 'a narrowing_cons"
    67 
    68 definition empty :: "'a narrowing"
    69 where
    70   "empty d = Narrowing_cons (Narrowing_sum_of_products []) []"
    71   
    72 definition cons :: "'a => 'a narrowing"
    73 where
    74   "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(%_. a)])"
    75 
    76 fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
    77 where
    78   "conv cs (Narrowing_variable p _) = error (marker # map toEnum p)"
    79 | "conv cs (Narrowing_constructor i xs) = (nth cs i) xs"
    80 
    81 fun non_empty :: "narrowing_type => bool"
    82 where
    83   "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))"
    84 
    85 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
    86 where
    87   "apply f a d =
    88      (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs =>
    89        case a (d - 1) of Narrowing_cons ta cas =>
    90        let
    91          shallow = (d > 0 \<and> non_empty ta);
    92          cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
    93        in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p <- ps]) cs)"
    94 
    95 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
    96 where
    97   "sum a b d =
    98     (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca => 
    99       case b d of Narrowing_cons (Narrowing_sum_of_products ssb) cb =>
   100       Narrowing_cons (Narrowing_sum_of_products (ssa @ ssb)) (ca @ cb))"
   101 
   102 lemma [fundef_cong]:
   103   assumes "a d = a' d" "b d = b' d" "d = d'"
   104   shows "sum a b d = sum a' b' d'"
   105 using assms unfolding sum_def by (auto split: narrowing_cons.split narrowing_type.split)
   106 
   107 lemma [fundef_cong]:
   108   assumes "f d = f' d" "(\<And>d'. 0 \<le> d' \<and> d' < d \<Longrightarrow> a d' = a' d')"
   109   assumes "d = d'"
   110   shows "apply f a d = apply f' a' d'"
   111 proof -
   112   note assms
   113   moreover have "0 < d' \<Longrightarrow> 0 \<le> d' - 1"
   114     by (simp add: less_integer_def less_eq_integer_def)
   115   ultimately show ?thesis
   116     by (auto simp add: apply_def Let_def
   117       split: narrowing_cons.split narrowing_type.split)
   118 qed
   119 
   120 subsubsection {* Narrowing generator type class *}
   121 
   122 class narrowing =
   123   fixes narrowing :: "integer => 'a narrowing_cons"
   124 
   125 datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
   126 
   127 (* FIXME: hard-wired maximal depth of 100 here *)
   128 definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
   129 where
   130   "exists f = (case narrowing (100 :: integer) of Narrowing_cons ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   131 
   132 definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property"
   133 where
   134   "all f = (case narrowing (100 :: integer) of Narrowing_cons ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   135 
   136 subsubsection {* class @{text is_testable} *}
   137 
   138 text {* The class @{text is_testable} ensures that all necessary type instances are generated. *}
   139 
   140 class is_testable
   141 
   142 instance bool :: is_testable ..
   143 
   144 instance "fun" :: ("{term_of, narrowing, partial_term_of}", is_testable) is_testable ..
   145 
   146 definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"
   147 where
   148   "ensure_testable f = f"
   149 
   150 
   151 subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
   152 
   153 datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
   154 
   155 primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
   156 where
   157   "eval_ffun (Constant c) x = c"
   158 | "eval_ffun (Update x' y f) x = (if x = x' then y else eval_ffun f x)"
   159 
   160 hide_type (open) ffun
   161 hide_const (open) Constant Update eval_ffun
   162 
   163 datatype 'b cfun = Constant 'b
   164 
   165 primrec eval_cfun :: "'b cfun => 'a => 'b"
   166 where
   167   "eval_cfun (Constant c) y = c"
   168 
   169 hide_type (open) cfun
   170 hide_const (open) Constant eval_cfun Abs_cfun Rep_cfun
   171 
   172 subsubsection {* Setting up the counterexample generator *}
   173 
   174 ML_file "Tools/Quickcheck/narrowing_generators.ML"
   175 
   176 setup {* Narrowing_Generators.setup *}
   177 
   178 definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
   179 where
   180   "narrowing_dummy_partial_term_of = partial_term_of"
   181 
   182 definition narrowing_dummy_narrowing :: "integer => ('a :: narrowing) narrowing_cons"
   183 where
   184   "narrowing_dummy_narrowing = narrowing"
   185 
   186 lemma [code]:
   187   "ensure_testable f =
   188     (let
   189       x = narrowing_dummy_narrowing :: integer => bool narrowing_cons;
   190       y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term;
   191       z = (conv :: _ => _ => unit)  in f)"
   192 unfolding Let_def ensure_testable_def ..
   193 
   194 subsection {* Narrowing for sets *}
   195 
   196 instantiation set :: (narrowing) narrowing
   197 begin
   198 
   199 definition "narrowing_set = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons set) narrowing"
   200 
   201 instance ..
   202 
   203 end
   204   
   205 subsection {* Narrowing for integers *}
   206 
   207 
   208 definition drawn_from :: "'a list \<Rightarrow> 'a narrowing_cons"
   209 where
   210   "drawn_from xs =
   211     Narrowing_cons (Narrowing_sum_of_products (map (\<lambda>_. []) xs)) (map (\<lambda>x _. x) xs)"
   212 
   213 function around_zero :: "int \<Rightarrow> int list"
   214 where
   215   "around_zero i = (if i < 0 then [] else (if i = 0 then [0] else around_zero (i - 1) @ [i, -i]))"
   216   by pat_completeness auto
   217 termination by (relation "measure nat") auto
   218 
   219 declare around_zero.simps [simp del]
   220 
   221 lemma length_around_zero:
   222   assumes "i >= 0" 
   223   shows "length (around_zero i) = 2 * nat i + 1"
   224 proof (induct rule: int_ge_induct [OF assms])
   225   case 1
   226   from 1 show ?case by (simp add: around_zero.simps)
   227 next
   228   case (2 i)
   229   from 2 show ?case
   230     by (simp add: around_zero.simps [of "i + 1"])
   231 qed
   232 
   233 instantiation int :: narrowing
   234 begin
   235 
   236 definition
   237   "narrowing_int d = (let (u :: _ \<Rightarrow> _ \<Rightarrow> unit) = conv; i = int_of_integer d
   238     in drawn_from (around_zero i))"
   239 
   240 instance ..
   241 
   242 end
   243 
   244 lemma [code, code del]: "partial_term_of (ty :: int itself) t \<equiv> undefined"
   245   by (rule partial_term_of_anything)+
   246 
   247 lemma [code]:
   248   "partial_term_of (ty :: int itself) (Narrowing_variable p t) \<equiv>
   249     Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
   250   "partial_term_of (ty :: int itself) (Narrowing_constructor i []) \<equiv>
   251     (if i mod 2 = 0
   252      then Code_Evaluation.term_of (- (int_of_integer i) div 2)
   253      else Code_Evaluation.term_of ((int_of_integer i + 1) div 2))"
   254   by (rule partial_term_of_anything)+
   255 
   256 instantiation integer :: narrowing
   257 begin
   258 
   259 definition
   260   "narrowing_integer d = (let (u :: _ \<Rightarrow> _ \<Rightarrow> unit) = conv; i = int_of_integer d
   261     in drawn_from (map integer_of_int (around_zero i)))"
   262 
   263 instance ..
   264 
   265 end
   266 
   267 lemma [code, code del]: "partial_term_of (ty :: integer itself) t \<equiv> undefined"
   268   by (rule partial_term_of_anything)+
   269 
   270 lemma [code]:
   271   "partial_term_of (ty :: integer itself) (Narrowing_variable p t) \<equiv>
   272     Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Code_Numeral.integer'') [])"
   273   "partial_term_of (ty :: integer itself) (Narrowing_constructor i []) \<equiv>
   274     (if i mod 2 = 0
   275      then Code_Evaluation.term_of (- i div 2)
   276      else Code_Evaluation.term_of ((i + 1) div 2))"
   277   by (rule partial_term_of_anything)+
   278 
   279 
   280 subsection {* The @{text find_unused_assms} command *}
   281 
   282 ML_file "Tools/Quickcheck/find_unused_assms.ML"
   283 
   284 subsection {* Closing up *}
   285 
   286 hide_type narrowing_type narrowing_term narrowing_cons property
   287 hide_const map_cons nth error toEnum marker empty Narrowing_cons conv non_empty ensure_testable all exists drawn_from around_zero
   288 hide_const (open) Narrowing_variable Narrowing_constructor "apply" sum cons
   289 hide_fact empty_def cons_def conv.simps non_empty.simps apply_def sum_def ensure_testable_def all_def exists_def
   290 
   291 end
   292