41905

1 
(* Author: Lukas Bulwahn, TU Muenchen *)


2 


3 
header {* Counterexample generator based on LazySmallCheck *}


4 


5 
theory LSC


6 
imports Main "~~/src/HOL/Library/Code_Char"


7 
uses ("~~/src/HOL/Tools/LSC/lazysmallcheck.ML")


8 
begin


9 


10 
subsection {* Counterexample generator *}


11 


12 
subsubsection {* LSC's deep representation of types of terms *}


13 


14 
datatype type = SumOfProd "type list list"


15 


16 
datatype "term" = Var "code_numeral list" type  Ctr code_numeral "term list"


17 


18 
datatype 'a cons = C type "(term list => 'a) list"


19 


20 
subsubsection {* auxilary functions for LSC *}


21 


22 
definition nth :: "'a list => code_numeral => 'a"


23 
where


24 
"nth xs i = List.nth xs (Code_Numeral.nat_of i)"


25 


26 
lemma [code]:


27 
"nth (x # xs) i = (if i = 0 then x else nth xs (i  1))"


28 
unfolding nth_def by (cases i) simp


29 


30 
definition error :: "char list => 'a"


31 
where


32 
"error = undefined"


33 


34 
code_const error ("Haskell" "error")


35 


36 
definition toEnum' :: "code_numeral => char"


37 
where


38 
"toEnum' = undefined"


39 


40 
code_const toEnum' ("Haskell" "(toEnum . fromInteger)")


41 


42 
subsubsection {* LSC's basic operations *}


43 


44 
type_synonym 'a series = "code_numeral => 'a cons"


45 


46 
definition empty :: "'a series"


47 
where


48 
"empty d = C (SumOfProd []) []"


49 


50 
definition cons :: "'a => 'a series"


51 
where


52 
"cons a d = (C (SumOfProd [[]]) [(%_. a)])"


53 


54 
fun conv :: "(term list => 'a) list => term => 'a"


55 
where


56 
"conv cs (Var p _) = error (Char Nibble0 Nibble0 # map toEnum' p)"


57 
 "conv cs (Ctr i xs) = (nth cs i) xs"


58 


59 
fun nonEmpty :: "type => bool"


60 
where


61 
"nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"


62 


63 
definition "apply" :: "('a => 'b) series => 'a series => 'b series"


64 
where


65 
"apply f a d =


66 
(case f d of C (SumOfProd ps) cfs =>


67 
case a (d  1) of C ta cas =>


68 
let


69 
shallow = (d > 0 \<and> nonEmpty ta);


70 
cs = [(%xs'. (case xs' of [] => undefined  x # xs => cf xs (conv cas x))). shallow, cf < cfs]


71 
in C (SumOfProd [ta # p. shallow, p < ps]) cs)"


72 


73 
definition sum :: "'a series => 'a series => 'a series"


74 
where


75 
"sum a b d =


76 
(case a d of C (SumOfProd ssa) ca =>


77 
case b d of C (SumOfProd ssb) cb =>


78 
C (SumOfProd (ssa @ ssb)) (ca @ cb))"


79 


80 
definition cons0 :: "'a => 'a series"


81 
where


82 
"cons0 f = cons f"


83 


84 


85 
subsubsection {* LSC's type class for enumeration *}


86 


87 
class serial =


88 
fixes series :: "code_numeral => 'a cons"


89 


90 
definition cons1 :: "('a::serial => 'b) => 'b series"


91 
where


92 
"cons1 f = apply (cons f) series"


93 


94 
definition cons2 :: "('a :: serial => 'b :: serial => 'c) => 'c series"


95 
where


96 
"cons2 f = apply (apply (cons f) series) series"


97 


98 
instantiation unit :: serial


99 
begin


100 


101 
definition


102 
"series = cons0 ()"


103 


104 
instance ..


105 


106 
end


107 


108 
instantiation bool :: serial


109 
begin


110 


111 
definition


112 
"series = sum (cons0 True) (cons0 False)"


113 


114 
instance ..


115 


116 
end


117 


118 
instantiation option :: (serial) serial


119 
begin


120 


121 
definition


122 
"series = sum (cons0 None) (cons1 Some)"


123 


124 
instance ..


125 


126 
end


127 


128 
instantiation sum :: (serial, serial) serial


129 
begin


130 


131 
definition


132 
"series = sum (cons1 Inl) (cons1 Inr)"


133 


134 
instance ..


135 


136 
end


137 


138 
instantiation list :: (serial) serial


139 
begin


140 


141 
function series_list :: "'a list series"


142 
where


143 
"series_list d = sum (cons []) (apply (apply (cons Cons) series) series_list) d"


144 
by pat_completeness auto


145 


146 
termination sorry


147 


148 
instance ..


149 


150 
end


151 


152 
instantiation nat :: serial


153 
begin


154 


155 
function series_nat :: "nat series"


156 
where


157 
"series_nat d = sum (cons 0) (apply (cons Suc) series_nat) d"


158 
by pat_completeness auto


159 


160 
termination sorry


161 


162 
instance ..


163 


164 
end


165 


166 
instantiation Enum.finite_1 :: serial


167 
begin


168 


169 
definition series_finite_1 :: "Enum.finite_1 series"


170 
where


171 
"series_finite_1 = cons (Enum.finite_1.a\<^isub>1 :: Enum.finite_1)"


172 


173 
instance ..


174 


175 
end


176 


177 
instantiation Enum.finite_2 :: serial


178 
begin


179 


180 
definition series_finite_2 :: "Enum.finite_2 series"


181 
where


182 
"series_finite_2 = sum (cons (Enum.finite_2.a\<^isub>1 :: Enum.finite_2)) (cons (Enum.finite_2.a\<^isub>2 :: Enum.finite_2))"


183 


184 
instance ..


185 


186 
end


187 


188 
instantiation Enum.finite_3 :: serial


189 
begin


190 


191 
definition series_finite_3 :: "Enum.finite_3 series"


192 
where


193 
"series_finite_3 = sum (cons (Enum.finite_3.a\<^isub>1 :: Enum.finite_3)) (sum (cons (Enum.finite_3.a\<^isub>2 :: Enum.finite_3)) (cons (Enum.finite_3.a\<^isub>3 :: Enum.finite_3)))"


194 


195 
instance ..


196 


197 
end


198 


199 
subsubsection {* class is_testable *}


200 


201 
text {* The class is_testable ensures that all necessary type instances are generated. *}


202 


203 
class is_testable


204 


205 
instance bool :: is_testable ..


206 


207 
instance "fun" :: ("{term_of, serial}", is_testable) is_testable ..


208 


209 
definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"


210 
where


211 
"ensure_testable f = f"


212 


213 
subsubsection {* Setting up the counterexample generator *}


214 


215 
use "Tools/LSC/lazysmallcheck.ML"


216 


217 
setup {* Lazysmallcheck.setup *}


218 


219 
end 