theory Quickcheck_Exhaustive imports Quickcheck_Random
keywords "quickcheck_generator" :: thy_decl begin
subsection \<open>Basic operations for exhaustive generators\<close>
definition orelse :: "'a option \ 'a option \ 'a option" (infixr \orelse\ 55) where [code_unfold]: "x orelse y = (case x of Some x' \ Some x' | None \ y)"
subsection \<open>Exhaustive generator type classes\<close>
class exhaustive = term_of + fixes exhaustive :: "('a \ (bool \ term list) option) \ natural \ (bool \ term list) option"
class full_exhaustive = term_of + fixes full_exhaustive :: "('a \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option"
instantiation natural :: full_exhaustive begin
function full_exhaustive_natural' :: "(natural \ (unit \ term) \ (bool \ term list) option) \
natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" where"full_exhaustive_natural' f d i =
(if d < i then None
else (f (i, \<lambda>_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))" by pat_completeness auto
definition"full_exhaustive f d = full_exhaustive_natural' f d 0"
instance ..
end
instantiation natural :: exhaustive begin
function exhaustive_natural' :: "(natural \ (bool \ term list) option) \ natural \ natural \ (bool \ term list) option" where"exhaustive_natural' f d i =
(if d < i then None
else (f i orelse exhaustive_natural' f d (i + 1)))" by pat_completeness auto
definition"exhaustive f d = exhaustive_natural' f d 0"
instance ..
end
instantiation integer :: exhaustive begin
function exhaustive_integer' :: "(integer \ (bool \ term list) option) \ integer \ integer \ (bool \ term list) option" where"exhaustive_integer' f d i =
(if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))" by pat_completeness auto
definition"exhaustive f d = exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
instance ..
end
instantiation integer :: full_exhaustive begin
function full_exhaustive_integer' :: "(integer \ (unit \ term) \ (bool \ term list) option) \
integer \<Rightarrow> integer \<Rightarrow> (bool \<times> term list) option" where"full_exhaustive_integer' f d i =
(if d < i then None
else
(case f (i, \<lambda>_. Code_Evaluation.term_of i) of
Some t \<Rightarrow> Some t
| None \<Rightarrow> full_exhaustive_integer' f d (i + 1)))" by pat_completeness auto
definition"full_exhaustive f d =
full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
instance ..
end
instantiation nat :: exhaustive begin
definition"exhaustive f d = exhaustive (\x. f (nat_of_natural x)) d"
instance ..
end
instantiation nat :: full_exhaustive begin
definition"full_exhaustive f d =
full_exhaustive (\<lambda>(x, xt). f (nat_of_natural x, \<lambda>_. Code_Evaluation.term_of (nat_of_natural x))) d"
instance ..
end
instantiation int :: exhaustive begin
function exhaustive_int' :: "(int \ (bool \ term list) option) \ int \ int \ (bool \ term list) option" where"exhaustive_int' f d i =
(if d < i then None else (f i orelse exhaustive_int' f d (i + 1)))" by pat_completeness auto
termination by (relation "measure (\(_, d, i). nat (d + 1 - i))") auto
definition"exhaustive f d =
exhaustive_int' f (int_of_integer (integer_of_natural d))
(- (int_of_integer (integer_of_natural d)))"
instance ..
end
instantiation int :: full_exhaustive begin
function full_exhaustive_int' :: "(int \ (unit \ term) \ (bool \ term list) option) \
int \<Rightarrow> int \<Rightarrow> (bool \<times> term list) option" where"full_exhaustive_int' f d i =
(if d < i then None
else
(case f (i, \<lambda>_. Code_Evaluation.term_of i) of
Some t \<Rightarrow> Some t
| None \<Rightarrow> full_exhaustive_int' f d (i + 1)))" by pat_completeness auto
termination by (relation "measure (\(_, d, i). nat (d + 1 - i))") auto
definition"full_exhaustive f d =
full_exhaustive_int' f (int_of_integer (integer_of_natural d))
(- (int_of_integer (integer_of_natural d)))"
instance ..
end
instantiation prod :: (exhaustive, exhaustive) exhaustive begin
definition"exhaustive f d = exhaustive (\x. exhaustive (\y. f ((x, y))) d) d"
instance ..
end
context includes term_syntax begin
definition
[code_unfold]: "valtermify_pair x y =
Code_Evaluation.valtermify (Pair :: 'a::typerep \ 'b::typerep \ 'a \ 'b) {\} x {\} y"
end
instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive begin
definition"full_exhaustive f d =
full_exhaustive (\<lambda>x. full_exhaustive (\<lambda>y. f (valtermify_pair x y)) d) d"
instance ..
end
instantiation set :: (exhaustive) exhaustive begin
fun exhaustive_set where "exhaustive_set f i =
(if i = 0 then None
else
f {} orelse
exhaustive_set
(\<lambda>A. f A orelse exhaustive (\<lambda>x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1))"
instance ..
end
instantiation set :: (full_exhaustive) full_exhaustive begin
fun full_exhaustive_set where "full_exhaustive_set f i =
(if i = 0 then None
else
f valterm_emptyset orelse
full_exhaustive_set
(\<lambda>A. f A orelse Quickcheck_Exhaustive.full_exhaustive
(\<lambda>x. if fst x \<in> fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1))"
instance ..
end
instantiation"fun" :: ("{equal,exhaustive}", exhaustive) exhaustive begin
fun exhaustive_fun' :: "(('a \ 'b) \ (bool \ term list) option) \ natural \ natural \ (bool \ term list) option" where "exhaustive_fun' f i d =
(exhaustive (\<lambda>b. f (\<lambda>_. b)) d) orelse
(if i > 1 then
exhaustive_fun'
(\<lambda>g. exhaustive (\<lambda>a. exhaustive (\<lambda>b. f (g(a := b))) d) d) (i - 1) d else None)"
definition exhaustive_fun :: "(('a \ 'b) \ (bool \ term list) option) \ natural \ (bool \ term list) option" where"exhaustive_fun f d = exhaustive_fun' f d d"
definition
[code_unfold]: "valtermify_fun_upd g a b =
Code_Evaluation.valtermify
(fun_upd :: ('a::typerep \ 'b::typerep) \ 'a \ 'b \ 'a \ 'b) {\} g {\} a {\} b"
end
instantiation"fun" :: ("{equal,full_exhaustive}", full_exhaustive) full_exhaustive begin
fun full_exhaustive_fun' :: "(('a \ 'b) \ (unit \ term) \ (bool \ term list) option) \
natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" where "full_exhaustive_fun' f i d =
full_exhaustive (\<lambda>v. f (valtermify_absdummy v)) d orelse
(if i > 1 then
full_exhaustive_fun'
(\<lambda>g. full_exhaustive
(\<lambda>a. full_exhaustive (\<lambda>b. f (valtermify_fun_upd g a b)) d) d) (i - 1) d
else None)"
definition full_exhaustive_fun :: "(('a \ 'b) \ (unit \ term) \ (bool \ term list) option) \
natural \<Rightarrow> (bool \<times> term list) option" where"full_exhaustive_fun f d = full_exhaustive_fun' f d d"
instance ..
end
subsubsection \<open>A smarter enumeration scheme for functions over finite datatypes\<close>
class check_all = enum + term_of + fixes check_all :: "('a \ (unit \ term) \ (bool \ term list) option) \ (bool * term list) option" fixes enum_term_of :: "'a itself \ unit \ term list"
fun check_all_n_lists :: "('a::check_all list \ (unit \ term list) \
(bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option" where "check_all_n_lists f n =
(if n = 0 then f ([], (\<lambda>_. []))
else check_all (\<lambda>(x, xt).
check_all_n_lists (\<lambda>(xs, xst). f ((x # xs), (\<lambda>_. (xt () # xst ())))) (n - 1)))"
context includes term_syntax begin
definition
[code_unfold]: "termify_fun_upd g a b =
(Code_Evaluation.termify
(fun_upd :: ('a::typerep \ 'b::typerep) \ 'a \ 'b \ 'a \ 'b) <\> g <\> a <\> b)"
fun check_all_subsets :: "(('a::typerep) set \ (unit \ term) \ (bool \ term list) option) \
('a \ (unit \ term)) list \ (bool \ term list) option" where "check_all_subsets f [] = f valterm_emptyset"
| "check_all_subsets f (x # xs) =
check_all_subsets (\<lambda>s. case f s of Some ts \<Rightarrow> Some ts | None \<Rightarrow> f (valtermify_insert x s)) xs"
definition
[code_unfold]: "termify_insert x s =
Code_Evaluation.termify (insert :: ('a::typerep) \ 'a set \ 'a set) <\> x <\> s"
definition setify :: "('a::typerep) itself \ term list \ term" where "setify T ts = foldr (termify_insert T) ts (term_emptyset T)"
end
instantiation set :: (check_all) check_all begin
definition "check_all_set f =
check_all_subsets f
(zip (Enum.enum :: 'a list)
(map (\<lambda>a. \<lambda>u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))"
definition enum_term_of_set :: "'a set itself \ unit \ term list" where"enum_term_of_set _ _ =
map (setify (TYPE('a))) (subseqs (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
instance ..
end
instantiation unit :: check_all begin
definition"check_all f = f (Code_Evaluation.valtermify ())"
definition enum_term_of_unit :: "unit itself \ unit \ term list" where"enum_term_of_unit = (\_ _. [Code_Evaluation.term_of ()])"
instance ..
end
instantiation bool :: check_all begin
definition "check_all f =
(case f (Code_Evaluation.valtermify False) of
Some x' \ Some x'
| None \<Rightarrow> f (Code_Evaluation.valtermify True))"
definition enum_term_of_bool :: "bool itself \ unit \ term list" where"enum_term_of_bool = (\_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
instance ..
end
context includes term_syntax begin
definition [code_unfold]: "termify_pair x y =
Code_Evaluation.termify (Pair :: 'a::typerep \ 'b :: typerep \ 'a * 'b) <\> x <\> y"
end
instantiation prod :: (check_all, check_all) check_all begin
definition"check_all f = check_all (\x. check_all (\y. f (valtermify_pair x y)))"
definition"check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)"
definition enum_term_of_finite_1 :: "Enum.finite_1 itself \ unit \ term list" where"enum_term_of_finite_1 = (\_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])"
instance ..
end
instantiation Enum.finite_2 :: check_all begin
definition "check_all f =
(f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1) orelse
f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))"
definition enum_term_of_finite_2 :: "Enum.finite_2 itself \ unit \ term list" where"enum_term_of_finite_2 =
(\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
instance ..
end
instantiation Enum.finite_3 :: check_all begin
definition "check_all f =
(f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1) orelse
f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2) orelse
f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))"
definition enum_term_of_finite_3 :: "Enum.finite_3 itself \ unit \ term list" where"enum_term_of_finite_3 =
(\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
instance ..
end
instantiation Enum.finite_4 :: check_all begin
definition "check_all f =
f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1) orelse
f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2) orelse
f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3) orelse
f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4)"
definition enum_term_of_finite_4 :: "Enum.finite_4 itself \ unit \ term list" where"enum_term_of_finite_4 =
(\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
definition cps_single :: "'a \ 'a cps" where"cps_single v = (\cont. cont v)"
definition cps_bind :: "'a cps \ ('a \ 'b cps) \ 'b cps" where"cps_bind m f = (\cont. m (\a. (f a) cont))"
definition cps_plus :: "'a cps \ 'a cps \ 'a cps" where"cps_plus a b = (\c. case a c of None \ b c | Some x \ Some x)"
definition cps_if :: "bool \ unit cps" where"cps_if b = (if b then cps_single () else cps_empty)"
definition cps_not :: "unit cps \ unit cps" where"cps_not n = (\c. case n (\u. Some []) of None \ c () | Some _ \ None)"
type_synonym'a pos_bound_cps = "('a \ (bool * term list) option) \ natural \ (bool * term list) option"
definition pos_bound_cps_empty :: "'a pos_bound_cps" where"pos_bound_cps_empty = (\cont i. None)"
definition pos_bound_cps_single :: "'a \ 'a pos_bound_cps" where"pos_bound_cps_single v = (\cont i. cont v)"
definition pos_bound_cps_bind :: "'a pos_bound_cps \ ('a \ 'b pos_bound_cps) \ 'b pos_bound_cps" where"pos_bound_cps_bind m f = (\cont i. if i = 0 then None else (m (\a. (f a) cont i) (i - 1)))"
definition pos_bound_cps_plus :: "'a pos_bound_cps \ 'a pos_bound_cps \ 'a pos_bound_cps" where"pos_bound_cps_plus a b = (\c i. case a c i of None \ b c i | Some x \ Some x)"
definition pos_bound_cps_if :: "bool \ unit pos_bound_cps" where"pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
datatype (plugins only: code extraction) (dead 'a) unknown =
Unknown | Known 'a
type_synonym'a neg_bound_cps = "('a unknown \ term list three_valued) \ natural \ term list three_valued"
definition neg_bound_cps_empty :: "'a neg_bound_cps" where"neg_bound_cps_empty = (\cont i. No_value)"
definition neg_bound_cps_single :: "'a \ 'a neg_bound_cps" where"neg_bound_cps_single v = (\cont i. cont (Known v))"
definition neg_bound_cps_bind :: "'a neg_bound_cps \ ('a \ 'b neg_bound_cps) \ 'b neg_bound_cps" where"neg_bound_cps_bind m f =
(\<lambda>cont i. if i = 0 then cont Unknown
else m (\<lambda>a. case a of Unknown \<Rightarrow> cont Unknown | Known a' \<Rightarrow> f a' cont i) (i - 1))"
definition neg_bound_cps_plus :: "'a neg_bound_cps \ 'a neg_bound_cps \ 'a neg_bound_cps" where"neg_bound_cps_plus a b =
(\<lambda>c i. case a c i of
No_value \<Rightarrow> b c i
| Value x \<Rightarrow> Value x
| Unknown_value \<Rightarrow>
(case b c i of
No_value \<Rightarrow> Unknown_value
| Value x \<Rightarrow> Value x
| Unknown_value \<Rightarrow> Unknown_value))"
definition neg_bound_cps_if :: "bool \ unit neg_bound_cps" where"neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
definition neg_bound_cps_not :: "unit pos_bound_cps \ unit neg_bound_cps" where"neg_bound_cps_not n =
(\<lambda>c i. case n (\<lambda>u. Some (True, [])) i of None \<Rightarrow> c (Known ()) | Some _ \<Rightarrow> No_value)"
definition pos_bound_cps_not :: "unit neg_bound_cps \ unit pos_bound_cps" where"pos_bound_cps_not n =
(\<lambda>c i. case n (\<lambda>u. Value []) i of No_value \<Rightarrow> c () | Value _ \<Rightarrow> None | Unknown_value \<Rightarrow> None)"
subsection \<open>Defining generators for any first-order data type\<close>
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
