--- a/src/HOL/Quickcheck_Exhaustive.thy Thu Apr 14 15:33:23 2016 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Thu Apr 14 15:33:51 2016 +0200
@@ -1,4 +1,6 @@
-(* Author: Lukas Bulwahn, TU Muenchen *)
+(* Title: HOL/Quickcheck_Exhaustive.thy
+ Author: Lukas Bulwahn, TU Muenchen
+*)
section \<open>A simple counterexample generator performing exhaustive testing\<close>
@@ -7,32 +9,34 @@
keywords "quickcheck_generator" :: thy_decl
begin
-subsection \<open>basic operations for exhaustive generators\<close>
+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)"
+definition orelse :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" (infixr "orelse" 55)
+ where [code_unfold]: "x orelse y = (case x of Some x' \<Rightarrow> Some x' | None \<Rightarrow> y)"
-subsection \<open>exhaustive generator type classes\<close>
+
+subsection \<open>Exhaustive generator type classes\<close>
class exhaustive = term_of +
- fixes exhaustive :: "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
-
+ fixes exhaustive :: "('a \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
+
class full_exhaustive = term_of +
- fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
+ fixes full_exhaustive ::
+ "('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
instantiation natural :: full_exhaustive
begin
-function full_exhaustive_natural' :: "(natural * (unit => term) => (bool * term list) option) => natural => natural => (bool * term list) option"
+function full_exhaustive_natural' ::
+ "(natural \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
+ natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
where "full_exhaustive_natural' f d i =
(if d < i then None
- else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))"
+ else (f (i, \<lambda>_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))"
by pat_completeness auto
termination
- by (relation "measure (%(_, d, i). nat_of_natural (d + 1 - i))")
- (auto simp add: less_natural_def)
+ by (relation "measure (\<lambda>(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def)
definition "full_exhaustive f d = full_exhaustive_natural' f d 0"
@@ -43,15 +47,15 @@
instantiation natural :: exhaustive
begin
-function exhaustive_natural' :: "(natural => (bool * term list) option) => natural => natural => (bool * term list) option"
+function exhaustive_natural' ::
+ "(natural \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
where "exhaustive_natural' f d i =
(if d < i then None
- else (f i orelse exhaustive_natural' f d (i + 1)))"
+ else (f i orelse exhaustive_natural' f d (i + 1)))"
by pat_completeness auto
termination
- by (relation "measure (%(_, d, i). nat_of_natural (d + 1 - i))")
- (auto simp add: less_natural_def)
+ by (relation "measure (\<lambda>(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def)
definition "exhaustive f d = exhaustive_natural' f d 0"
@@ -62,12 +66,14 @@
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)))"
+function exhaustive_integer' ::
+ "(integer \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> integer \<Rightarrow> integer \<Rightarrow> (bool \<times> 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
-termination
- by (relation "measure (%(_, d, i). nat_of_integer (d + 1 - i))")
+termination
+ by (relation "measure (\<lambda>(_, d, i). nat_of_integer (d + 1 - i))")
(auto simp add: less_integer_def nat_of_integer_def)
definition "exhaustive f d = exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
@@ -79,15 +85,23 @@
instantiation integer :: full_exhaustive
begin
-function full_exhaustive_integer' :: "(integer * (unit => term) => (bool * term list) option) => integer => integer => (bool * term list) option"
- where "full_exhaustive_integer' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive_integer' f d (i + 1)))"
+function full_exhaustive_integer' ::
+ "(integer \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
+ 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
-termination
- by (relation "measure (%(_, d, i). nat_of_integer (d + 1 - i))")
+termination
+ by (relation "measure (\<lambda>(_, d, i). nat_of_integer (d + 1 - i))")
(auto simp add: less_integer_def nat_of_integer_def)
-definition "full_exhaustive f d = full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
+definition "full_exhaustive f d =
+ full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
instance ..
@@ -96,7 +110,7 @@
instantiation nat :: exhaustive
begin
-definition "exhaustive f d = exhaustive (%x. f (nat_of_natural x)) d"
+definition "exhaustive f d = exhaustive (\<lambda>x. f (nat_of_natural x)) d"
instance ..
@@ -105,7 +119,8 @@
instantiation nat :: full_exhaustive
begin
-definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (nat_of_natural x, %_. Code_Evaluation.term_of (nat_of_natural x))) d"
+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 ..
@@ -114,15 +129,18 @@
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)))"
+function exhaustive_int' ::
+ "(int \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> (bool \<times> 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
+termination
+ by (relation "measure (\<lambda>(_, 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)))"
+definition "exhaustive f d =
+ exhaustive_int' f (int_of_integer (integer_of_natural d))
+ (- (int_of_integer (integer_of_natural d)))"
instance ..
@@ -131,15 +149,23 @@
instantiation int :: full_exhaustive
begin
-function full_exhaustive_int' :: "(int * (unit => term) => (bool * term list) option) => int => int => (bool * term list) option"
- where "full_exhaustive_int' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive_int' f d (i + 1)))"
+function full_exhaustive_int' ::
+ "(int \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
+ 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
+termination
+ by (relation "measure (\<lambda>(_, 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)))"
+definition "full_exhaustive f d =
+ full_exhaustive_int' f (int_of_integer (integer_of_natural d))
+ (- (int_of_integer (integer_of_natural d)))"
instance ..
@@ -148,20 +174,21 @@
instantiation prod :: (exhaustive, exhaustive) exhaustive
begin
-definition
- "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
+definition "exhaustive f d = exhaustive (\<lambda>x. exhaustive (\<lambda>y. f ((x, y))) d) d"
instance ..
end
-definition (in term_syntax) [code_unfold]: "valtermify_pair x y = Code_Evaluation.valtermify (Pair :: 'a :: typerep => 'b :: typerep => 'a * 'b) {\<cdot>} x {\<cdot>} y"
+definition (in term_syntax)
+ [code_unfold]: "valtermify_pair x y =
+ Code_Evaluation.valtermify (Pair :: 'a::typerep \<Rightarrow> 'b::typerep \<Rightarrow> 'a \<times> 'b) {\<cdot>} x {\<cdot>} y"
instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
begin
-definition
- "full_exhaustive f d = full_exhaustive (%x. full_exhaustive (%y. f (valtermify_pair x y)) d) d"
+definition "full_exhaustive f d =
+ full_exhaustive (\<lambda>x. full_exhaustive (\<lambda>y. f (valtermify_pair x y)) d) d"
instance ..
@@ -172,7 +199,12 @@
fun exhaustive_set
where
- "exhaustive_set f i = (if i = 0 then None else (f {} orelse exhaustive_set (%A. f A orelse exhaustive (%x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1)))"
+ "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 ..
@@ -181,49 +213,70 @@
instantiation set :: (full_exhaustive) full_exhaustive
begin
-fun full_exhaustive_set
+fun full_exhaustive_set
where
- "full_exhaustive_set f i = (if i = 0 then None else (f valterm_emptyset orelse full_exhaustive_set (%A. f A orelse Quickcheck_Exhaustive.full_exhaustive (%x. if fst x \<in> fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1)))"
+ "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
+instantiation "fun" :: ("{equal,exhaustive}", exhaustive) exhaustive
begin
-fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => natural => natural => (bool * term list) option"
+fun exhaustive_fun' ::
+ "(('a \<Rightarrow> 'b) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
where
- "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
- orelse (if i > 1 then
- exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
- f (g(a := b))) d) d) (i - 1) d else None)"
+ "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 exhaustive_fun ::
+ "(('a \<Rightarrow> 'b) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
+ where "exhaustive_fun f d = exhaustive_fun' f d d"
instance ..
end
-definition [code_unfold]: "valtermify_absdummy = (%(v, t). (%_::'a. v, %u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))"
+definition [code_unfold]:
+ "valtermify_absdummy =
+ (\<lambda>(v, t).
+ (\<lambda>_::'a. v,
+ \<lambda>u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))"
-definition (in term_syntax) [code_unfold]: "valtermify_fun_upd g a b = Code_Evaluation.valtermify (fun_upd :: ('a :: typerep => 'b :: typerep) => 'a => 'b => 'a => 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b"
+definition (in term_syntax)
+ [code_unfold]: "valtermify_fun_upd g a b =
+ Code_Evaluation.valtermify
+ (fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b"
-instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
+instantiation "fun" :: ("{equal,full_exhaustive}", full_exhaustive) full_exhaustive
begin
-fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => natural => natural => (bool * term list) option"
+fun full_exhaustive_fun' ::
+ "(('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
+ natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
where
- "full_exhaustive_fun' f i d = (full_exhaustive (%v. f (valtermify_absdummy v)) d)
- orelse (if i > 1 then
- full_exhaustive_fun' (%g. full_exhaustive (%a. full_exhaustive (%b.
- f (valtermify_fun_upd g a b)) d) d) (i - 1) d else None)"
+ "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 => (bool * term list) option"
-where
- "full_exhaustive_fun f d = full_exhaustive_fun' f d d"
+definition full_exhaustive_fun ::
+ "(('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
+ natural \<Rightarrow> (bool \<times> term list) option"
+ where "full_exhaustive_fun f d = full_exhaustive_fun' f d d"
instance ..
@@ -232,75 +285,110 @@
subsubsection \<open>A smarter enumeration scheme for functions over finite datatypes\<close>
class check_all = enum + term_of +
- fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> (bool * term list) option) \<Rightarrow> (bool * term list) option"
+ fixes check_all :: "('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool * term list) option"
fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
-
-fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
+
+fun check_all_n_lists :: "('a::check_all list \<times> (unit \<Rightarrow> term list) \<Rightarrow>
+ (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool * 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)))"
+ (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)))"
-definition (in term_syntax) [code_unfold]: "termify_fun_upd g a b = (Code_Evaluation.termify (fun_upd :: ('a :: typerep => 'b :: typerep) => 'a => 'b => 'a => 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)"
+definition (in term_syntax)
+ [code_unfold]: "termify_fun_upd g a b =
+ (Code_Evaluation.termify
+ (fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)"
-definition mk_map_term :: " (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term"
-where
- "mk_map_term T1 T2 domm rng =
- (%_. let T1 = T1 ();
- 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) a) b)
- in
- List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
+definition mk_map_term ::
+ "(unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow>
+ (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term"
+ where "mk_map_term T1 T2 domm rng =
+ (\<lambda>_.
+ let
+ T1 = T1 ();
+ T2 = T2 ();
+ update_term =
+ (\<lambda>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) a) b)
+ in
+ List.foldl update_term
+ (Code_Evaluation.Abs (STR ''x'') T1
+ (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
-instantiation "fun" :: ("{equal, check_all}", check_all) check_all
+instantiation "fun" :: ("{equal,check_all}", check_all) check_all
begin
definition
"check_all f =
(let
- mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a)));
+ mk_term =
+ mk_map_term
+ (\<lambda>_. Typerep.typerep (TYPE('a)))
+ (\<lambda>_. Typerep.typerep (TYPE('b)))
+ (enum_term_of (TYPE('a)));
enum = (Enum.enum :: 'a list)
- in check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst)) (natural_of_nat (length enum)))"
+ in
+ check_all_n_lists
+ (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst))
+ (natural_of_nat (length enum)))"
-definition enum_term_of_fun :: "('a => 'b) itself => unit => term list"
-where
- "enum_term_of_fun = (%_ _. let
- enum_term_of_a = enum_term_of (TYPE('a));
- mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
- in map (%ys. mk_term (%_. ys) ()) (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
-
+definition enum_term_of_fun :: "('a \<Rightarrow> 'b) itself \<Rightarrow> unit \<Rightarrow> term list"
+ where "enum_term_of_fun =
+ (\<lambda>_ _.
+ let
+ enum_term_of_a = enum_term_of (TYPE('a));
+ mk_term =
+ mk_map_term
+ (\<lambda>_. Typerep.typerep (TYPE('a)))
+ (\<lambda>_. Typerep.typerep (TYPE('b)))
+ enum_term_of_a
+ in
+ map (\<lambda>ys. mk_term (\<lambda>_. ys) ())
+ (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
+
instance ..
end
-fun (in term_syntax) check_all_subsets :: "(('a :: typerep) set * (unit => term) => (bool * term list) option) => ('a * (unit => term)) list => (bool * term list) option"
+fun (in term_syntax) check_all_subsets ::
+ "(('a::typerep) set \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
+ ('a \<times> (unit \<Rightarrow> term)) list \<Rightarrow> (bool \<times> term list) option"
where
"check_all_subsets f [] = f valterm_emptyset"
-| "check_all_subsets f (x # xs) = check_all_subsets (%s. case f s of Some ts => Some ts | None => f (valtermify_insert x s)) xs"
+| "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 (in term_syntax) [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a :: typerep) set)"
-definition (in term_syntax) [code_unfold]: "termify_insert x s = Code_Evaluation.termify (insert :: ('a::typerep) => 'a set => 'a set) <\<cdot>> x <\<cdot>> s"
+definition (in term_syntax)
+ [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a::typerep) set)"
-definition (in term_syntax) setify :: "('a::typerep) itself => term list => term"
+definition (in term_syntax)
+ [code_unfold]: "termify_insert x s =
+ Code_Evaluation.termify (insert :: ('a::typerep) \<Rightarrow> 'a set \<Rightarrow> 'a set) <\<cdot>> x <\<cdot>> s"
+
+definition (in term_syntax) setify :: "('a::typerep) itself \<Rightarrow> term list \<Rightarrow> term"
where
- "setify T ts = foldr (termify_insert T) ts (term_emptyset T)"
+ "setify T ts = foldr (termify_insert T) ts (term_emptyset T)"
instantiation set :: (check_all) check_all
begin
definition
"check_all_set f =
- check_all_subsets f (zip (Enum.enum :: 'a list) (map (%a. %u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))"
+ 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))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
+definition enum_term_of_set :: "'a set itself \<Rightarrow> unit \<Rightarrow> term list"
+ where "enum_term_of_set _ _ =
+ map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
instance ..
@@ -309,12 +397,10 @@
instantiation unit :: check_all
begin
-definition
- "check_all f = f (Code_Evaluation.valtermify ())"
+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 ()])"
+definition enum_term_of_unit :: "unit itself \<Rightarrow> unit \<Rightarrow> term list"
+ where "enum_term_of_unit = (\<lambda>_ _. [Code_Evaluation.term_of ()])"
instance ..
@@ -325,55 +411,66 @@
begin
definition
- "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
+ "check_all f =
+ (case f (Code_Evaluation.valtermify False) of
+ Some x' \<Rightarrow> 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))"
+definition enum_term_of_bool :: "bool itself \<Rightarrow> unit \<Rightarrow> term list"
+ where "enum_term_of_bool = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
instance ..
end
-definition (in term_syntax) [code_unfold]: "termify_pair x y = Code_Evaluation.termify (Pair :: 'a :: typerep => 'b :: typerep => 'a * 'b) <\<cdot>> x <\<cdot>> y"
+definition (in term_syntax) [code_unfold]:
+ "termify_pair x y =
+ Code_Evaluation.termify (Pair :: 'a::typerep \<Rightarrow> 'b :: typerep \<Rightarrow> 'a * 'b) <\<cdot>> x <\<cdot>> y"
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 = check_all (\<lambda>x. check_all (\<lambda>y. f (valtermify_pair x y)))"
-definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
-where
- "enum_term_of_prod = (%_ _. map (%(x, y). termify_pair TYPE('a) TYPE('b) x y)
- (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
+definition enum_term_of_prod :: "('a * 'b) itself \<Rightarrow> unit \<Rightarrow> term list"
+ where "enum_term_of_prod =
+ (\<lambda>_ _.
+ map (\<lambda>(x, y). termify_pair TYPE('a) TYPE('b) x y)
+ (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
instance ..
end
-definition (in term_syntax) [code_unfold]: "valtermify_Inl x = Code_Evaluation.valtermify (Inl :: 'a :: typerep => 'a + 'b :: typerep) {\<cdot>} x"
-definition (in term_syntax) [code_unfold]: "valtermify_Inr x = Code_Evaluation.valtermify (Inr :: 'b :: typerep => 'a ::typerep + 'b) {\<cdot>} x"
+definition (in term_syntax)
+ [code_unfold]: "valtermify_Inl x =
+ Code_Evaluation.valtermify (Inl :: 'a::typerep \<Rightarrow> 'a + 'b :: typerep) {\<cdot>} x"
+
+definition (in term_syntax)
+ [code_unfold]: "valtermify_Inr x =
+ Code_Evaluation.valtermify (Inr :: 'b::typerep \<Rightarrow> 'a::typerep + 'b) {\<cdot>} x"
instantiation sum :: (check_all, check_all) check_all
begin
definition
- "check_all f = check_all (%a. f (valtermify_Inl a)) orelse check_all (%b. f (valtermify_Inr b))"
+ "check_all f = check_all (\<lambda>a. f (valtermify_Inl a)) orelse check_all (\<lambda>b. f (valtermify_Inr b))"
-definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"
-where
- "enum_term_of_sum = (%_ _.
- let
- T1 = (Typerep.typerep (TYPE('a)));
- T2 = (Typerep.typerep (TYPE('b)))
- in
- map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'')
- (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
- (enum_term_of (TYPE('a)) ()) @
- map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'')
- (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
- (enum_term_of (TYPE('b)) ()))"
+definition enum_term_of_sum :: "('a + 'b) itself \<Rightarrow> unit \<Rightarrow> term list"
+ where "enum_term_of_sum =
+ (\<lambda>_ _.
+ let
+ T1 = Typerep.typerep (TYPE('a));
+ T2 = Typerep.typerep (TYPE('b))
+ in
+ map
+ (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'')
+ (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
+ (enum_term_of (TYPE('a)) ()) @
+ map
+ (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'')
+ (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
+ (enum_term_of (TYPE('b)) ()))"
instance ..
@@ -383,13 +480,13 @@
begin
definition
- "check_all f = check_all (%(x, t1). check_all (%(y, t2).
- f (Char x y, %_. Code_Evaluation.App
+ "check_all f = check_all (\<lambda>(x, t1). check_all (\<lambda>(y, t2).
+ f (Char x y, \<lambda>_. Code_Evaluation.App
(Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
-definition enum_term_of_char :: "char itself => unit => term list"
+definition enum_term_of_char :: "char itself \<Rightarrow> unit \<Rightarrow> term list"
where
- "enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
+ "enum_term_of_char = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
instance ..
@@ -399,14 +496,29 @@
begin
definition
- "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
- (Code_Evaluation.Const (STR ''Option.option.Some'')
- (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
+ "check_all f =
+ f (Code_Evaluation.valtermify (None :: 'a option)) orelse
+ check_all
+ (\<lambda>(x, t).
+ f
+ (Some x,
+ \<lambda>_. Code_Evaluation.App
+ (Code_Evaluation.Const (STR ''Option.option.Some'')
+ (Typerep.Typerep (STR ''fun'')
+ [Typerep.typerep TYPE('a),
+ Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
-definition enum_term_of_option :: "'a option itself => unit => term list"
-where
- "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'')
- (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))"
+definition enum_term_of_option :: "'a option itself \<Rightarrow> unit \<Rightarrow> term list"
+ where "enum_term_of_option =
+ (\<lambda> _ _.
+ Code_Evaluation.term_of (None :: 'a option) #
+ (map
+ (Code_Evaluation.App
+ (Code_Evaluation.Const (STR ''Option.option.Some'')
+ (Typerep.Typerep (STR ''fun'')
+ [Typerep.typerep TYPE('a),
+ Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])))
+ (enum_term_of (TYPE('a)) ())))"
instance ..
@@ -416,12 +528,10 @@
instantiation Enum.finite_1 :: check_all
begin
-definition
- "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)"
+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])"
+definition enum_term_of_finite_1 :: "Enum.finite_1 itself \<Rightarrow> unit \<Rightarrow> term list"
+ where "enum_term_of_finite_1 = (\<lambda>_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])"
instance ..
@@ -431,12 +541,13 @@
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))"
+ "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 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
+definition enum_term_of_finite_2 :: "Enum.finite_2 itself \<Rightarrow> unit \<Rightarrow> term list"
+ where "enum_term_of_finite_2 =
+ (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
instance ..
@@ -446,13 +557,14 @@
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))"
+ "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 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
+definition enum_term_of_finite_3 :: "Enum.finite_3 itself \<Rightarrow> unit \<Rightarrow> term list"
+ where "enum_term_of_finite_3 =
+ (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
instance ..
@@ -462,14 +574,15 @@
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))"
+ "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 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
+definition enum_term_of_finite_4 :: "Enum.finite_4 itself \<Rightarrow> unit \<Rightarrow> term list"
+ where "enum_term_of_finite_4 =
+ (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
instance ..
@@ -480,69 +593,61 @@
class bounded_forall =
fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> natural \<Rightarrow> bool"
+
subsection \<open>Fast exhaustive combinators\<close>
class fast_exhaustive = term_of +
fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> natural \<Rightarrow> unit"
-axiomatization throw_Counterexample :: "term list => unit"
-axiomatization catch_Counterexample :: "unit => term list option"
+axiomatization throw_Counterexample :: "term list \<Rightarrow> unit"
+axiomatization catch_Counterexample :: "unit \<Rightarrow> term list option"
code_printing
constant throw_Counterexample \<rightharpoonup>
(Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)"
| constant catch_Counterexample \<rightharpoonup>
- (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)"
+ (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts \<Rightarrow> SOME ts)"
+
subsection \<open>Continuation passing style functions as plus monad\<close>
-
-type_synonym 'a cps = "('a => term list option) => term list option"
+
+type_synonym 'a cps = "('a \<Rightarrow> term list option) \<Rightarrow> term list option"
definition cps_empty :: "'a cps"
-where
- "cps_empty = (%cont. None)"
+ where "cps_empty = (\<lambda>cont. None)"
-definition cps_single :: "'a => 'a cps"
-where
- "cps_single v = (%cont. cont v)"
+definition cps_single :: "'a \<Rightarrow> 'a cps"
+ where "cps_single v = (\<lambda>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_bind :: "'a cps \<Rightarrow> ('a \<Rightarrow> 'b cps) \<Rightarrow> 'b cps"
+ where "cps_bind m f = (\<lambda>cont. m (\<lambda>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_plus :: "'a cps \<Rightarrow> 'a cps \<Rightarrow> 'a cps"
+ where "cps_plus a b = (\<lambda>c. case a c of None \<Rightarrow> b c | Some x \<Rightarrow> Some x)"
+
+definition cps_if :: "bool \<Rightarrow> unit cps"
+ where "cps_if b = (if b then cps_single () else cps_empty)"
-definition cps_if :: "bool => unit cps"
-where
- "cps_if b = (if b then cps_single () else cps_empty)"
+definition cps_not :: "unit cps \<Rightarrow> unit cps"
+ where "cps_not n = (\<lambda>c. case n (\<lambda>u. Some []) of None \<Rightarrow> c () | Some _ \<Rightarrow> None)"
-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"
+type_synonym 'a pos_bound_cps =
+ "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
definition pos_bound_cps_empty :: "'a pos_bound_cps"
-where
- "pos_bound_cps_empty = (%cont i. None)"
+ where "pos_bound_cps_empty = (\<lambda>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_single :: "'a \<Rightarrow> 'a pos_bound_cps"
+ where "pos_bound_cps_single v = (\<lambda>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_bind :: "'a pos_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b pos_bound_cps) \<Rightarrow> 'b pos_bound_cps"
+ where "pos_bound_cps_bind m f = (\<lambda>cont i. if i = 0 then None else (m (\<lambda>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_plus :: "'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps"
+ where "pos_bound_cps_plus a b = (\<lambda>c i. case a c i of None \<Rightarrow> b c i | Some x \<Rightarrow> 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)"
+definition pos_bound_cps_if :: "bool \<Rightarrow> 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
@@ -550,35 +655,44 @@
datatype (plugins only: code extraction) (dead 'a) three_valued =
Unknown_value | Value 'a | No_value
-type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
+type_synonym 'a neg_bound_cps =
+ "('a unknown \<Rightarrow> term list three_valued) \<Rightarrow> natural \<Rightarrow> term list three_valued"
definition neg_bound_cps_empty :: "'a neg_bound_cps"
-where
- "neg_bound_cps_empty = (%cont i. No_value)"
+ where "neg_bound_cps_empty = (\<lambda>cont i. No_value)"
+
+definition neg_bound_cps_single :: "'a \<Rightarrow> 'a neg_bound_cps"
+ where "neg_bound_cps_single v = (\<lambda>cont i. cont (Known v))"
-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 = (%cont i. if i = 0 then cont Unknown else m (%a. case a of Unknown => cont Unknown | Known a' => f a' cont i) (i - 1))"
+definition neg_bound_cps_bind :: "'a neg_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b neg_bound_cps) \<Rightarrow> '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 = (%c i. case a c i of No_value => b c i | Value x => Value x | Unknown_value => (case b c i of No_value => Unknown_value | Value x => Value x | Unknown_value => 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_plus :: "'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps \<Rightarrow> '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_not :: "unit pos_bound_cps => unit neg_bound_cps"
-where
- "neg_bound_cps_not n = (%c i. case n (%u. Some (True, [])) i of None => c (Known ()) | Some _ => No_value)"
+definition neg_bound_cps_if :: "bool \<Rightarrow> unit neg_bound_cps"
+ where "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
-definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps"
-where
- "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
+definition neg_bound_cps_not :: "unit pos_bound_cps \<Rightarrow> 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 \<Rightarrow> 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>
@@ -590,6 +704,7 @@
declare [[quickcheck_batch_tester = exhaustive]]
+
subsection \<open>Defining generators for abstract types\<close>
ML_file "Tools/Quickcheck/abstract_generators.ML"
@@ -615,10 +730,11 @@
end *)
hide_fact (open) orelse_def
-no_notation orelse (infixr "orelse" 55)
+no_notation orelse (infixr "orelse" 55)
-hide_const valtermify_absdummy valtermify_fun_upd valterm_emptyset valtermify_insert valtermify_pair
- valtermify_Inl valtermify_Inr
+hide_const valtermify_absdummy valtermify_fun_upd
+ valterm_emptyset valtermify_insert
+ valtermify_pair valtermify_Inl valtermify_Inr
termify_fun_upd term_emptyset termify_insert termify_pair setify
hide_const (open)
@@ -631,9 +747,12 @@
orelse unknown mk_map_term check_all_n_lists check_all_subsets
hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
+
hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
- pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
- neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
+ pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind
+ pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
+ neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind
+ neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
Unknown Known Unknown_value Value No_value
end
--- a/src/HOL/Quickcheck_Random.thy Thu Apr 14 15:33:23 2016 +0200
+++ b/src/HOL/Quickcheck_Random.thy Thu Apr 14 15:33:51 2016 +0200
@@ -1,4 +1,6 @@
-(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)
+(* Title: HOL/Quickcheck_Random.thy
+ Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen
+*)
section \<open>A simple counterexample generator performing random testing\<close>
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Thu Apr 14 15:33:23 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Thu Apr 14 15:33:51 2016 +0200
@@ -7,7 +7,7 @@
signature ABSTRACT_GENERATORS =
sig
val quickcheck_generator : string -> term option -> term list -> theory -> theory
-end;
+end
structure Abstract_Generators : ABSTRACT_GENERATORS =
struct
@@ -15,19 +15,17 @@
fun check_constrs ctxt tyco constrs =
let
fun check_type c =
- case try (dest_Type o body_type o fastype_of) c of
+ (case try (dest_Type o body_type o fastype_of) c of
NONE => error (Syntax.string_of_term ctxt c ^ " has mismatching result type.")
| SOME (tyco', vs) => if not (tyco' = tyco) then
error (Syntax.string_of_term ctxt c ^ " has mismatching result type. " ^
"Expected type constructor " ^ quote tyco ^ ", but found " ^ quote tyco' ^ ".")
else
- case try (map dest_TFree) vs of
+ (case try (map dest_TFree) vs of
NONE => error (Syntax.string_of_term ctxt c ^ " has mismatching result type.")
- | SOME _ => ()
- in
- map check_type constrs
- end
-
+ | SOME _ => ()))
+ in map check_type constrs end
+
fun gen_quickcheck_generator prep_tyco prep_term tyco_raw opt_pred_raw constrs_raw thy =
let
val ctxt = Proof_Context.init_global thy
@@ -36,36 +34,36 @@
val constrs = map (prep_term ctxt) constrs_raw
val _ = check_constrs ctxt tyco constrs
val vs = map dest_TFree (snd (dest_Type (body_type (fastype_of (hd constrs)))))
- val name = Long_Name.base_name tyco
+ val name = Long_Name.base_name tyco
fun mk_dconstrs (Const (s, T)) =
- (s, map (Old_Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T))
- | mk_dconstrs t = error (Syntax.string_of_term ctxt t ^
- " is not a valid constructor for quickcheck_generator, which expects a constant.")
+ (s, map (Old_Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T))
+ | mk_dconstrs t =
+ error (Syntax.string_of_term ctxt t ^
+ " is not a valid constructor for quickcheck_generator, which expects a constant.")
fun the_descr _ _ =
- let
- val descr = [(0, (tyco, map Old_Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))]
- in
- (descr, vs, [tyco], name, ([name], []), ([Type (tyco, map TFree vs)], []))
- end
+ let val descr = [(0, (tyco, map Old_Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))]
+ in (descr, vs, [tyco], name, ([name], []), ([Type (tyco, map TFree vs)], [])) end
fun ensure_sort (sort, instantiate) =
- Quickcheck_Common.ensure_sort (((@{sort typerep}, @{sort term_of}), sort),
- (the_descr, instantiate))
- Old_Datatype_Aux.default_config [tyco]
+ Quickcheck_Common.ensure_sort
+ (((@{sort typerep}, @{sort term_of}), sort), (the_descr, instantiate))
+ Old_Datatype_Aux.default_config [tyco]
in
thy
- |> ensure_sort (@{sort full_exhaustive}, Exhaustive_Generators.instantiate_full_exhaustive_datatype)
+ |> ensure_sort
+ (@{sort full_exhaustive}, Exhaustive_Generators.instantiate_full_exhaustive_datatype)
|> ensure_sort (@{sort exhaustive}, Exhaustive_Generators.instantiate_exhaustive_datatype)
|> ensure_sort (@{sort random}, Random_Generators.instantiate_random_datatype)
- |> (case opt_pred of NONE => I | SOME t => Context.theory_map (Quickcheck_Common.register_predicate (t, tyco)))
+ |> (case opt_pred of NONE => I
+ | SOME t => Context.theory_map (Quickcheck_Common.register_predicate (t, tyco)))
end
val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
-
+
val quickcheck_generator_cmd =
gen_quickcheck_generator
((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = true})
Syntax.read_term
-
+
val _ =
Outer_Syntax.command @{command_keyword quickcheck_generator}
"define quickcheck generators for abstract types"
@@ -75,4 +73,4 @@
>> (fn ((tyco, opt_pred), constrs) =>
Toplevel.theory (quickcheck_generator_cmd tyco opt_pred constrs)))
-end;
+end
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Thu Apr 14 15:33:23 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Thu Apr 14 15:33:51 2016 +0200
@@ -6,28 +6,30 @@
signature EXHAUSTIVE_GENERATORS =
sig
- val compile_generator_expr:
- Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
+ val compile_generator_expr: Proof.context -> (term * term list) list -> bool -> int list ->
+ (bool * term list) option * Quickcheck.report option
val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list
- val put_counterexample: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option)
- -> Proof.context -> Proof.context
- val put_counterexample_batch: (unit -> (Code_Numeral.natural -> term list option) list)
- -> Proof.context -> Proof.context
- val put_validator_batch: (unit -> (Code_Numeral.natural -> bool) list) -> Proof.context -> Proof.context
+ val put_counterexample:
+ (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) ->
+ Proof.context -> Proof.context
+ val put_counterexample_batch: (unit -> (Code_Numeral.natural -> term list option) list) ->
+ Proof.context -> Proof.context
+ val put_validator_batch: (unit -> (Code_Numeral.natural -> bool) list) ->
+ Proof.context -> Proof.context
exception Counterexample of term list
val smart_quantifier : bool Config.T
val optimise_equality : bool Config.T
val quickcheck_pretty : bool Config.T
val setup_exhaustive_datatype_interpretation : theory -> theory
val setup_bounded_forall_datatype_interpretation : theory -> theory
-
val instantiate_full_exhaustive_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
- (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+ (string * sort) list -> string list -> string -> string list * string list ->
+ typ list * typ list -> theory -> theory
val instantiate_exhaustive_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
- (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
-
-end;
+ (string * sort) list -> string list -> string -> string list * string list ->
+ typ list * typ list -> theory -> theory
+end
structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
struct
@@ -43,44 +45,40 @@
val bounded_forall = Attrib.setup_config_bool @{binding quickcheck_bounded_forall} (K false)
val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true)
val quickcheck_pretty = Attrib.setup_config_bool @{binding quickcheck_pretty} (K true)
-
+
(** abstract syntax **)
-fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
+fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> Code_Evaluation.term"})
val size = @{term "i :: natural"}
val size_pred = @{term "(i :: natural) - 1"}
val size_ge_zero = @{term "(i :: natural) > 0"}
fun mk_none_continuation (x, y) =
- let
- val (T as Type(@{type_name "option"}, _)) = fastype_of x
- in
- Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y
- end
+ let val (T as Type (@{type_name option}, _)) = fastype_of x
+ in Const (@{const_name Quickcheck_Exhaustive.orelse}, T --> T --> T) $ x $ y end
fun mk_if (b, t, e) =
- let
- val T = fastype_of t
- in Const (@{const_name "HOL.If"}, @{typ bool} --> T --> T --> T) $ b $ t $ e end
+ let val T = fastype_of t
+ in Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e end
+
(* handling inductive datatypes *)
(** constructing generator instances **)
-exception FUNCTION_TYPE;
+exception FUNCTION_TYPE
exception Counterexample of term list
-val resultT = @{typ "(bool * term list) option"};
+val resultT = @{typ "(bool * term list) option"}
-val exhaustiveN = "exhaustive";
-val full_exhaustiveN = "full_exhaustive";
-val bounded_forallN = "bounded_forall";
+val exhaustiveN = "exhaustive"
+val full_exhaustiveN = "full_exhaustive"
+val bounded_forallN = "bounded_forall"
-fun fast_exhaustiveT T = (T --> @{typ unit})
- --> @{typ natural} --> @{typ unit}
+fun fast_exhaustiveT T = (T --> @{typ unit}) --> @{typ natural} --> @{typ unit}
fun exhaustiveT T = (T --> resultT) --> @{typ natural} --> resultT
@@ -100,9 +98,7 @@
|> map (fn (T, cs) => map (mk_consexpr T) cs)
|> map mk_rhs
val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives Ts
- in
- map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
- end
+ in map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) end
fun gen_mk_call c T = (T, fn t => c T $ absdummy T t $ size_pred)
@@ -110,9 +106,7 @@
let
val T = Type (tyco, Ts)
val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
- in
- (T, fn t => nth functerms k $ absdummy T t $ size_pred)
- end
+ in (T, fn t => nth functerms k $ absdummy T t $ size_pred) end
fun gen_mk_consexpr test_function simpleT (c, xs) =
let
@@ -126,49 +120,51 @@
let
fun test_function T = Free ("f", T --> resultT)
val mk_call = gen_mk_call (fn T =>
- Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T))
+ Const (@{const_name Quickcheck_Exhaustive.exhaustive_class.exhaustive}, exhaustiveT T))
val mk_aux_call = gen_mk_aux_call functerms
val mk_consexpr = gen_mk_consexpr test_function
fun mk_rhs exprs =
- mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name "None"}, resultT))
- in
- mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
- end
+ mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT))
+ in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end
fun mk_bounded_forall_equations functerms =
let
fun test_function T = Free ("P", T --> @{typ bool})
val mk_call = gen_mk_call (fn T =>
- Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"},
+ Const (@{const_name Quickcheck_Exhaustive.bounded_forall_class.bounded_forall},
bounded_forallT T))
val mk_aux_call = gen_mk_aux_call functerms
val mk_consexpr = gen_mk_consexpr test_function
- fun mk_rhs exprs =
- mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term "True"})
- in
- mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
- end
-
+ fun mk_rhs exprs = mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term True})
+ in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end
+
fun mk_full_equations functerms =
let
fun test_function T = Free ("f", termifyT T --> resultT)
- fun case_prod_const T = HOLogic.case_prod_const (T, @{typ "unit => Code_Evaluation.term"}, resultT)
+ fun case_prod_const T =
+ HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> Code_Evaluation.term"}, resultT)
fun mk_call T =
let
val full_exhaustive =
- Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
+ Const (@{const_name Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive},
full_exhaustiveT T)
- in
- (T, fn t => full_exhaustive $
- (case_prod_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
+ in
+ (T,
+ fn t =>
+ full_exhaustive $
+ (case_prod_const T $ absdummy T (absdummy @{typ "unit \<Rightarrow> Code_Evaluation.term"} t)) $
+ size_pred)
end
fun mk_aux_call fTs (k, _) (tyco, Ts) =
let
val T = Type (tyco, Ts)
val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
in
- (T, fn t => nth functerms k $
- (case_prod_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
+ (T,
+ fn t =>
+ nth functerms k $
+ (case_prod_const T $ absdummy T (absdummy @{typ "unit \<Rightarrow> Code_Evaluation.term"} t)) $
+ size_pred)
end
fun mk_consexpr simpleT (c, xs) =
let
@@ -176,29 +172,30 @@
val constr = Const (c, Ts ---> simpleT)
val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
val Eval_App =
- Const (@{const_name Code_Evaluation.App}, HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
+ Const (@{const_name Code_Evaluation.App},
+ HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
val Eval_Const =
- Const (@{const_name Code_Evaluation.Const}, HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
- val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
- bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
- val start_term = test_function simpleT $
- (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
- $ (list_comb (constr, bounds)) $ absdummy @{typ unit} term)
+ Const (@{const_name Code_Evaluation.Const},
+ HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
+ val term =
+ fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
+ bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
+ val start_term =
+ test_function simpleT $
+ (HOLogic.pair_const simpleT @{typ "unit \<Rightarrow> Code_Evaluation.term"} $
+ (list_comb (constr, bounds)) $ absdummy @{typ unit} term)
in fold_rev (fn f => fn t => f t) fns start_term end
fun mk_rhs exprs =
- mk_if (size_ge_zero, foldr1 mk_none_continuation exprs,
- Const (@{const_name "None"}, resultT))
- in
- mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
- end
-
+ mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT))
+ in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end
+
(** instantiating generator classes **)
-
+
fun contains_recursive_type_under_function_types xs =
exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
(case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true | _ => false)))) xs
-
+
fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames)
config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
if not (contains_recursive_type_under_function_types descr) then
@@ -218,106 +215,111 @@
("Creation of " ^ name ^ " failed because the datatype is recursive under a function type");
thy)
-val instantiate_bounded_forall_datatype = instantiate_datatype
- ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall},
- mk_bounded_forall_equations, bounded_forallT, ["P", "i"]);
+val instantiate_bounded_forall_datatype =
+ instantiate_datatype
+ ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall},
+ mk_bounded_forall_equations, bounded_forallT, ["P", "i"])
-val instantiate_exhaustive_datatype = instantiate_datatype
- ("exhaustive generators", exhaustiveN, @{sort exhaustive},
- mk_equations, exhaustiveT, ["f", "i"])
+val instantiate_exhaustive_datatype =
+ instantiate_datatype
+ ("exhaustive generators", exhaustiveN, @{sort exhaustive},
+ mk_equations, exhaustiveT, ["f", "i"])
-val instantiate_full_exhaustive_datatype = instantiate_datatype
- ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive},
- mk_full_equations, full_exhaustiveT, ["f", "i"])
+val instantiate_full_exhaustive_datatype =
+ instantiate_datatype
+ ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive},
+ mk_full_equations, full_exhaustiveT, ["f", "i"])
+
(* building and compiling generator expressions *)
fun mk_let_expr (x, t, e) genuine =
- let
- val (T1, T2) = (fastype_of x, fastype_of (e genuine))
- in
- Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine)
- end
+ let val (T1, T2) = (fastype_of x, fastype_of (e genuine))
+ in Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine) end
fun mk_safe_let_expr genuine_only none safe (x, t, e) genuine =
let
val (T1, T2) = (fastype_of x, fastype_of (e genuine))
- val if_t = Const (@{const_name "If"}, @{typ bool} --> T2 --> T2 --> T2)
+ val if_t = Const (@{const_name If}, @{typ bool} --> T2 --> T2 --> T2)
in
- Const (@{const_name "Quickcheck_Random.catch_match"}, T2 --> T2 --> T2) $
+ Const (@{const_name Quickcheck_Random.catch_match}, T2 --> T2 --> T2) $
(Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine)) $
(if_t $ genuine_only $ none $ safe false)
end
fun mk_test_term lookup mk_closure mk_if mk_let none_t return ctxt =
let
- val cnstrs = flat (maps
- (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
- (Symtab.dest (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt)
- Quickcheck_Common.compat_prefs)))
- fun is_constrt (Const (s, T), ts) = (case (AList.lookup (op =) cnstrs s, body_type T) of
- (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname'
- | _ => false)
+ val cnstrs =
+ flat (maps
+ (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
+ (Symtab.dest
+ (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt) Quickcheck_Common.compat_prefs)))
+ fun is_constrt (Const (s, T), ts) =
+ (case (AList.lookup (op =) cnstrs s, body_type T) of
+ (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname'
+ | _ => false)
| is_constrt _ = false
fun mk_naive_test_term t =
- fold_rev mk_closure (map lookup (Term.add_free_names t []))
- (mk_if (t, none_t, return) true)
+ fold_rev mk_closure (map lookup (Term.add_free_names t [])) (mk_if (t, none_t, return) true)
fun mk_test (vars, check) = fold_rev mk_closure (map lookup vars) check
fun mk_smart_test_term' concl bound_vars assms genuine =
let
fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
fun mk_equality_term (lhs, f as Free (x, _)) c (assm, assms) =
- if member (op =) (Term.add_free_names lhs bound_vars) x then
- c (assm, assms)
- else
- (let
- val rec_call = mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms
- fun safe genuine =
- the_default I (Option.map mk_closure (try lookup x)) (rec_call genuine)
- in
- mk_test (remove (op =) x (vars_of assm),
- mk_let safe f (try lookup x) lhs
- (mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine)
-
- end)
+ if member (op =) (Term.add_free_names lhs bound_vars) x then
+ c (assm, assms)
+ else
+ let
+ val rec_call = mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms
+ fun safe genuine =
+ the_default I (Option.map mk_closure (try lookup x)) (rec_call genuine)
+ in
+ mk_test (remove (op =) x (vars_of assm),
+ mk_let safe f (try lookup x) lhs
+ (mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine)
+
+ end
| mk_equality_term (lhs, t) c (assm, assms) =
- if is_constrt (strip_comb t) then
- let
- val (constr, args) = strip_comb t
- val T = fastype_of t
- val vars = map Free (Variable.variant_frees ctxt (concl :: assms)
- (map (fn t => ("x", fastype_of t)) args))
- val varnames = map (fst o dest_Free) vars
- val dummy_var = Free (singleton
- (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T))
- val new_assms = map HOLogic.mk_eq (vars ~~ args)
- val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars)
- val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine
- in
- mk_test (vars_of lhs,
- Case_Translation.make_case ctxt Case_Translation.Quiet Name.context lhs
- [(list_comb (constr, vars), cont_t), (dummy_var, none_t)])
- end
- else c (assm, assms)
+ if is_constrt (strip_comb t) then
+ let
+ val (constr, args) = strip_comb t
+ val T = fastype_of t
+ val vars =
+ map Free
+ (Variable.variant_frees ctxt (concl :: assms)
+ (map (fn t => ("x", fastype_of t)) args))
+ val varnames = map (fst o dest_Free) vars
+ val dummy_var =
+ Free (singleton
+ (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T))
+ val new_assms = map HOLogic.mk_eq (vars ~~ args)
+ val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars)
+ val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine
+ in
+ mk_test (vars_of lhs,
+ Case_Translation.make_case ctxt Case_Translation.Quiet Name.context lhs
+ [(list_comb (constr, vars), cont_t), (dummy_var, none_t)])
+ end
+ else c (assm, assms)
fun default (assm, assms) =
- mk_test (vars_of assm,
- mk_if (HOLogic.mk_not assm, none_t,
- mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine)
+ mk_test
+ (vars_of assm,
+ mk_if (HOLogic.mk_not assm, none_t,
+ mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine)
in
- case assms of [] => mk_test (vars_of concl, mk_if (concl, none_t, return) genuine)
- | assm :: assms =>
+ (case assms of
+ [] => mk_test (vars_of concl, mk_if (concl, none_t, return) genuine)
+ | assm :: assms =>
if Config.get ctxt optimise_equality then
(case try HOLogic.dest_eq assm of
SOME (lhs, rhs) =>
mk_equality_term (lhs, rhs) (mk_equality_term (rhs, lhs) default) (assm, assms)
| NONE => default (assm, assms))
- else default (assm, assms)
+ else default (assm, assms))
end
val mk_smart_test_term =
Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms true)
- in
- if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term
- end
+ in if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term end
fun mk_fast_generator_expr ctxt (t, eval_terms) =
let
@@ -327,26 +329,31 @@
fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt'
val depth = Free (depth_name, @{typ natural})
- fun return _ = @{term "throw_Counterexample :: term list => unit"} $
- (HOLogic.mk_list @{typ "term"}
- (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
+ fun return _ =
+ @{term "throw_Counterexample :: term list \<Rightarrow> unit"} $
+ (HOLogic.mk_list @{typ term}
+ (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
fun mk_exhaustive_closure (free as Free (_, T)) t =
- Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"},
- fast_exhaustiveT T)
- $ lambda free t $ depth
+ Const (@{const_name Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive},
+ fast_exhaustiveT T) $ lambda free t $ depth
val none_t = @{term "()"}
fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
- val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt
+ val mk_test_term =
+ mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt
in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end
-fun mk_unknown_term T = HOLogic.reflect_term (Const (@{const_name Quickcheck_Exhaustive.unknown}, T))
+fun mk_unknown_term T =
+ HOLogic.reflect_term (Const (@{const_name Quickcheck_Exhaustive.unknown}, T))
-fun mk_safe_term t = @{term "Quickcheck_Random.catch_match :: term => term => term"}
- $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)
+fun mk_safe_term t =
+ @{term "Quickcheck_Random.catch_match :: term \<Rightarrow> term \<Rightarrow> term"} $
+ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)
-fun mk_return t genuine = @{term "Some :: bool * term list => (bool * term list) option"} $
- (HOLogic.pair_const @{typ bool} @{typ "term list"} $ Quickcheck_Common.reflect_bool genuine $ t)
+fun mk_return t genuine =
+ @{term "Some :: bool \<times> term list \<Rightarrow> (bool \<times> term list) option"} $
+ (HOLogic.pair_const @{typ bool} @{typ "term list"} $
+ Quickcheck_Common.reflect_bool genuine $ t)
fun mk_generator_expr ctxt (t, eval_terms) =
let
@@ -357,15 +364,17 @@
val ([depth_name, genuine_only_name], _) =
Variable.variant_fixes ["depth", "genuine_only"] ctxt'
val depth = Free (depth_name, @{typ natural})
- val genuine_only = Free (genuine_only_name, @{typ bool})
- val return = mk_return (HOLogic.mk_list @{typ "term"}
+ val genuine_only = Free (genuine_only_name, @{typ bool})
+ val return =
+ mk_return (HOLogic.mk_list @{typ term}
(map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms))
fun mk_exhaustive_closure (free as Free (_, T)) t =
- Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
- $ lambda free t $ depth
- val none_t = Const (@{const_name "None"}, resultT)
+ Const (@{const_name Quickcheck_Exhaustive.exhaustive_class.exhaustive}, exhaustiveT T) $
+ lambda free t $ depth
+ val none_t = Const (@{const_name None}, resultT)
val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
- fun mk_let safe def v_opt t e = mk_safe_let_expr genuine_only none_t safe (the_default def v_opt, t, e)
+ fun mk_let safe def v_opt t e =
+ mk_safe_let_expr genuine_only none_t safe (the_default def v_opt, t, e)
val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt
in lambda genuine_only (lambda depth (mk_test_term t)) end
@@ -379,33 +388,36 @@
Variable.variant_fixes ["depth", "genuine_only"] ctxt'
val (term_names, _) = Variable.variant_fixes (map (prefix "t_") names) ctxt''
val depth = Free (depth_name, @{typ natural})
- val genuine_only = Free (genuine_only_name, @{typ bool})
- val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
+ val genuine_only = Free (genuine_only_name, @{typ bool})
+ val term_vars = map (fn n => Free (n, @{typ "unit \<Rightarrow> term"})) term_names
fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
- val return = mk_return (HOLogic.mk_list @{typ term}
+ val return =
+ mk_return
+ (HOLogic.mk_list @{typ term}
(map (fn v => v $ @{term "()"}) term_vars @ map mk_safe_term eval_terms))
fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
if Sign.of_sort thy (T, @{sort check_all}) then
- Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
- $ (HOLogic.case_prod_const (T, @{typ "unit => term"}, resultT)
- $ lambda free (lambda term_var t))
+ Const (@{const_name Quickcheck_Exhaustive.check_all_class.check_all}, check_allT T) $
+ (HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) $
+ lambda free (lambda term_var t))
else
- Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
- $ (HOLogic.case_prod_const (T, @{typ "unit => term"}, resultT)
- $ lambda free (lambda term_var t)) $ depth
- val none_t = Const (@{const_name "None"}, resultT)
+ Const (@{const_name Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive},
+ full_exhaustiveT T) $
+ (HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) $
+ lambda free (lambda term_var t)) $ depth
+ val none_t = Const (@{const_name None}, resultT)
val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
fun mk_let safe _ (SOME (v, term_var)) t e =
- mk_safe_let_expr genuine_only none_t safe (v, t,
- e #> subst_free [(term_var, absdummy @{typ unit} (mk_safe_term t))])
+ mk_safe_let_expr genuine_only none_t safe (v, t,
+ e #> subst_free [(term_var, absdummy @{typ unit} (mk_safe_term t))])
| mk_let safe v NONE t e = mk_safe_let_expr genuine_only none_t safe (v, t, e)
val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt
in lambda genuine_only (lambda depth (mk_test_term t)) end
fun mk_parametric_generator_expr mk_generator_expr =
- Quickcheck_Common.gen_mk_parametric_generator_expr
+ Quickcheck_Common.gen_mk_parametric_generator_expr
((mk_generator_expr,
- absdummy @{typ bool} (absdummy @{typ natural} (Const (@{const_name "None"}, resultT)))),
+ absdummy @{typ bool} (absdummy @{typ natural} (Const (@{const_name None}, resultT)))),
@{typ bool} --> @{typ natural} --> resultT)
fun mk_validator_expr ctxt t =
@@ -418,115 +430,117 @@
val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt'
val depth = Free (depth_name, @{typ natural})
fun mk_bounded_forall (Free (s, T)) t =
- Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)
- $ lambda (Free (s, T)) t $ depth
+ Const (@{const_name Quickcheck_Exhaustive.bounded_forall_class.bounded_forall},
+ bounded_forallT T) $ lambda (Free (s, T)) t $ depth
fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
val mk_test_term =
mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) ctxt
in lambda depth (mk_test_term t) end
-
-fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) =
+fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) =
let
val frees = Term.add_free_names t []
- val dummy_term = @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'')
- (Typerep.Typerep (STR ''dummy'') [])"}
- val return = @{term "Some :: term list => term list option"} $
- (HOLogic.mk_list @{typ "term"}
- (replicate (length frees + length eval_terms) dummy_term))
+ val dummy_term =
+ @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (Typerep.Typerep (STR ''dummy'') [])"}
+ val return =
+ @{term "Some :: term list => term list option"} $
+ (HOLogic.mk_list @{typ term} (replicate (length frees + length eval_terms) dummy_term))
val wrap = absdummy @{typ bool}
- (@{term "If :: bool => term list option => term list option => term list option"} $
+ (@{term "If :: bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"} $
Bound 0 $ @{term "None :: term list option"} $ return)
in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end
-
+
(** generator compiliation **)
structure Data = Proof_Data
(
type T =
- (unit -> Code_Numeral.natural -> bool ->
- Code_Numeral.natural -> (bool * term list) option) *
+ (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) *
(unit -> (Code_Numeral.natural -> term list option) list) *
- (unit -> (Code_Numeral.natural -> bool) list);
+ (unit -> (Code_Numeral.natural -> bool) list)
val empty: T =
(fn () => raise Fail "counterexample",
fn () => raise Fail "counterexample_batch",
- fn () => raise Fail "validator_batch");
- fun init _ = empty;
-);
+ fn () => raise Fail "validator_batch")
+ fun init _ = empty
+)
-val get_counterexample = #1 o Data.get;
-val get_counterexample_batch = #2 o Data.get;
-val get_validator_batch = #3 o Data.get;
+val get_counterexample = #1 o Data.get
+val get_counterexample_batch = #2 o Data.get
+val get_validator_batch = #3 o Data.get
-val put_counterexample = Data.map o @{apply 3(1)} o K;
-val put_counterexample_batch = Data.map o @{apply 3(2)} o K;
-val put_validator_batch = Data.map o @{apply 3(3)} o K;
+val put_counterexample = Data.map o @{apply 3(1)} o K
+val put_counterexample_batch = Data.map o @{apply 3(2)} o K
+val put_validator_batch = Data.map o @{apply 3(3)} o K
-val target = "Quickcheck";
+val target = "Quickcheck"
fun compile_generator_expr_raw ctxt ts =
let
- val mk_generator_expr =
+ val mk_generator_expr =
if Config.get ctxt fast then mk_fast_generator_expr
else if Config.get ctxt bounded_forall then mk_bounded_forall_generator_expr
else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr
- val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts;
- val compile = Code_Runtime.dynamic_value_strict
- (get_counterexample, put_counterexample, "Exhaustive_Generators.put_counterexample")
- ctxt (SOME target) (fn proc => fn g =>
- fn card => fn genuine_only => fn size => g card genuine_only size
+ val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts
+ val compile =
+ Code_Runtime.dynamic_value_strict
+ (get_counterexample, put_counterexample, "Exhaustive_Generators.put_counterexample")
+ ctxt (SOME target)
+ (fn proc => fn g => fn card => fn genuine_only => fn size =>
+ g card genuine_only size
|> (Option.map o apsnd o map) proc) t' []
in
- fn genuine_only => fn [card, size] => rpair NONE (compile card genuine_only size |>
- (if Config.get ctxt quickcheck_pretty then
- Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I))
- end;
+ fn genuine_only => fn [card, size] =>
+ rpair NONE (compile card genuine_only size
+ |> (if Config.get ctxt quickcheck_pretty then
+ Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I))
+ end
fun compile_generator_expr ctxt ts =
- let
- val compiled = compile_generator_expr_raw ctxt ts;
- in fn genuine_only => fn [card, size] =>
- compiled genuine_only [Code_Numeral.natural_of_integer card, Code_Numeral.natural_of_integer size]
- end;
+ let val compiled = compile_generator_expr_raw ctxt ts in
+ fn genuine_only => fn [card, size] =>
+ compiled genuine_only
+ [Code_Numeral.natural_of_integer card, Code_Numeral.natural_of_integer size]
+ end
fun compile_generator_exprs_raw ctxt ts =
let
- val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts;
- val compiles = Code_Runtime.dynamic_value_strict
- (get_counterexample_batch, put_counterexample_batch,
- "Exhaustive_Generators.put_counterexample_batch")
- ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
- (HOLogic.mk_list @{typ "natural => term list option"} ts') []
+ val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts
+ val compiles =
+ Code_Runtime.dynamic_value_strict
+ (get_counterexample_batch, put_counterexample_batch,
+ "Exhaustive_Generators.put_counterexample_batch")
+ ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
+ (HOLogic.mk_list @{typ "natural => term list option"} ts') []
in
- map (fn compile => fn size => compile size
- |> (Option.map o map) Quickcheck_Common.post_process_term) compiles
- end;
+ map (fn compile => fn size =>
+ compile size |> (Option.map o map) Quickcheck_Common.post_process_term) compiles
+ end
fun compile_generator_exprs ctxt ts =
compile_generator_exprs_raw ctxt ts
- |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size));
+ |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size))
fun compile_validator_exprs_raw ctxt ts =
- let
- val ts' = map (mk_validator_expr ctxt) ts
- in
+ let val ts' = map (mk_validator_expr ctxt) ts in
Code_Runtime.dynamic_value_strict
(get_validator_batch, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
- ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural => bool"} ts') []
- end;
+ ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural \<Rightarrow> bool"} ts') []
+ end
fun compile_validator_exprs ctxt ts =
compile_validator_exprs_raw ctxt ts
- |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size));
+ |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size))
fun size_matters_for thy Ts = not (forall (fn T => Sign.of_sort thy (T, @{sort check_all})) Ts)
val test_goals =
- Quickcheck_Common.generator_test_goal_terms ("exhaustive", (size_matters_for, compile_generator_expr));
-
+ Quickcheck_Common.generator_test_goal_terms
+ ("exhaustive", (size_matters_for, compile_generator_expr))
+
+
(* setup *)
val setup_exhaustive_datatype_interpretation =
@@ -540,7 +554,7 @@
(fn thy => BNF_LFP_Compat.the_descr thy Quickcheck_Common.compat_prefs,
instantiate_bounded_forall_datatype)))
-val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
+val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true)
val _ =
Theory.setup
@@ -548,6 +562,6 @@
(@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
#> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
#> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
- #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)));
+ #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)))
-end;
+end
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Apr 14 15:33:23 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Apr 14 15:33:51 2016 +0200
@@ -15,8 +15,9 @@
| Existential_Counterexample of (term * counterexample) list
| Empty_Assignment
val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context
- val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context
-end;
+ val put_existential_counterexample : (unit -> counterexample option) ->
+ Proof.context -> Proof.context
+end
structure Narrowing_Generators : NARROWING_GENERATORS =
struct
@@ -28,26 +29,29 @@
val overlord = Attrib.setup_config_bool @{binding quickcheck_narrowing_overlord} (K false)
val ghc_options = Attrib.setup_config_string @{binding quickcheck_narrowing_ghc_options} (K "")
+
(* partial_term_of instances *)
fun mk_partial_term_of (x, T) =
Const (@{const_name Quickcheck_Narrowing.partial_term_of_class.partial_term_of},
- Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term})
- $ Logic.mk_type T $ x
+ Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) $ Logic.mk_type T $ x
+
(** formal definition **)
fun add_partial_term_of tyco raw_vs thy =
let
- val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
- val ty = Type (tyco, map TFree vs);
- val lhs = Const (@{const_name partial_term_of},
- Term.itselfT ty --> @{typ narrowing_term} --> @{typ Code_Evaluation.term})
- $ Free ("x", Term.itselfT ty) $ Free ("t", @{typ narrowing_term});
- val rhs = @{term "undefined :: Code_Evaluation.term"};
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
- fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
- o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
+ val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs
+ val ty = Type (tyco, map TFree vs)
+ val lhs =
+ Const (@{const_name partial_term_of},
+ Term.itselfT ty --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) $
+ Free ("x", Term.itselfT ty) $ Free ("t", @{typ narrowing_term})
+ val rhs = @{term "undefined :: Code_Evaluation.term"}
+ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
+ fun triv_name_of t =
+ (fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^
+ "_triv"
in
thy
|> Class.instantiation ([tyco], vs, @{sort partial_term_of})
@@ -55,13 +59,13 @@
|-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
- end;
+ end
fun ensure_partial_term_of (tyco, (raw_vs, _)) thy =
let
val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of})
- andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep};
- in if need_inst then add_partial_term_of tyco raw_vs thy else thy end;
+ andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep}
+ in if need_inst then add_partial_term_of tyco raw_vs thy else thy end
(** code equations for datatypes **)
@@ -69,15 +73,17 @@
fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
let
val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys))
- val narrowing_term = @{term Quickcheck_Narrowing.Narrowing_constructor} $ HOLogic.mk_number @{typ integer} i
- $ HOLogic.mk_list @{typ narrowing_term} (rev frees)
- val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
+ val narrowing_term =
+ @{term Quickcheck_Narrowing.Narrowing_constructor} $ HOLogic.mk_number @{typ integer} i $
+ HOLogic.mk_list @{typ narrowing_term} (rev frees)
+ val rhs =
+ fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
(map mk_partial_term_of (frees ~~ tys))
(@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty))
val insts =
map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
[Free ("ty", Term.itselfT ty), narrowing_term, rhs]
- val cty = Thm.global_ctyp_of thy ty;
+ val cty = Thm.global_ctyp_of thy ty
in
@{thm partial_term_of_anything}
|> Thm.instantiate' [SOME cty] insts
@@ -86,44 +92,42 @@
fun add_partial_term_of_code tyco raw_vs raw_cs thy =
let
- val algebra = Sign.classes_of thy;
- val vs = map (fn (v, sort) =>
- (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
- val ty = Type (tyco, map TFree vs);
- val cs = (map o apsnd o apsnd o map o map_atyps)
- (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
- val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco);
+ val algebra = Sign.classes_of thy
+ val vs = map (fn (v, sort) => (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs
+ val ty = Type (tyco, map TFree vs)
+ val cs =
+ (map o apsnd o apsnd o map o map_atyps)
+ (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs
+ val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco)
val var_insts =
map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
[Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"},
- @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
+ @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty]
val var_eq =
@{thm partial_term_of_anything}
|> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts
|> Thm.varifyT_global
- val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs;
- in
+ val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs
+ in
thy
|> Code.del_eqns const
|> fold Code.add_eqn eqs
- end;
+ end
fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy =
- let
- val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of};
- in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end;
+ let val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of}
+ in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end
(* narrowing generators *)
(** narrowing specific names and types **)
-exception FUNCTION_TYPE;
+exception FUNCTION_TYPE
-val narrowingN = "narrowing";
+val narrowingN = "narrowing"
-fun narrowingT T =
- @{typ integer} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T])
+fun narrowingT T = @{typ integer} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T])
fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T --> narrowingT T) $ Const (c, T)
@@ -136,11 +140,9 @@
end
fun mk_sum (t, u) =
- let
- val T = fastype_of t
- in
- Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u
- end
+ let val T = fastype_of t
+ in Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u end
+
(** deriving narrowing instances **)
@@ -156,8 +158,7 @@
(T, nth narrowings k)
end
fun mk_consexpr simpleT (c, xs) =
- let
- val Ts = map fst xs
+ let val Ts = map fst xs
in snd (fold mk_apply xs (Ts ---> simpleT, mk_cons c (Ts ---> simpleT))) end
fun mk_rhs exprs = foldr1 mk_sum exprs
val rhss =
@@ -168,9 +169,7 @@
|> map mk_rhs
val lhss = narrowings
val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
- in
- eqs
- end
+ in eqs end
fun contains_recursive_type_under_function_types xs =
exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
@@ -178,8 +177,8 @@
fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
let
- val _ = Old_Datatype_Aux.message config "Creating narrowing generators ...";
- val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames);
+ val _ = Old_Datatype_Aux.message config "Creating narrowing generators ..."
+ val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames)
in
if not (contains_recursive_type_under_function_types descr) then
thy
@@ -188,14 +187,15 @@
(fn narrowings => mk_equations descr vs narrowings, NONE)
prfx [] narrowingsN (map narrowingT (Ts @ Us))
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
- else
- thy
- end;
+ else thy
+ end
+
(* testing framework *)
val target = "Haskell_Quickcheck"
+
(** invocation of Haskell interpreter **)
val narrowing_engine =
@@ -213,14 +213,15 @@
let
val path =
Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
- val _ = Isabelle_System.mkdirs path;
- in Exn.release (Exn.capture f path) end;
+ val _ = Isabelle_System.mkdirs path
+ in Exn.release (Exn.capture f path) end
fun elapsed_time description e =
let val ({elapsed, ...}, result) = Timing.timing e ()
in (result, (description, Time.toMilliseconds elapsed)) end
-fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) =
+fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size))
+ ctxt cookie (code_modules, _) =
let
val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
fun message s = if quiet then () else writeln s
@@ -235,26 +236,33 @@
let
fun mk_code_file name = Path.append in_path (Path.basic (name ^ ".hs"))
val generatedN = Code_Target.generatedN
- val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file;
+ val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file
val code = the (AList.lookup (op =) code_modules generatedN)
val code_file = mk_code_file generatedN
val narrowing_engine_file = mk_code_file "Narrowing_Engine"
val main_file = mk_code_file "Main"
- val main = "module Main where {\n\n" ^
+ val main =
+ "module Main where {\n\n" ^
"import System.IO;\n" ^
"import System.Environment;\n" ^
"import Narrowing_Engine;\n" ^
"import " ^ generatedN ^ " ;\n\n" ^
"main = getArgs >>= \\[potential, size] -> " ^
- "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^ ".value ())\n\n" ^
- "}\n"
- val _ = map (uncurry File.write) (includes @
- [(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine),
- (code_file, code), (main_file, main)])
- val executable = File.bash_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
- val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
- ghc_options ^ " " ^
- (space_implode " " (map File.bash_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
+ "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^
+ ".value ())\n\n}\n"
+ val _ =
+ map (uncurry File.write)
+ (includes @
+ [(narrowing_engine_file,
+ if contains_existentials then pnf_narrowing_engine else narrowing_engine),
+ (code_file, code), (main_file, main)])
+ val executable =
+ File.bash_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
+ val cmd =
+ "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^
+ (space_implode " "
+ (map File.bash_path
+ (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
" -o " ^ executable ^ ";"
val (_, compilation_time) =
elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
@@ -262,52 +270,49 @@
fun haskell_string_of_bool v = if v then "True" else "False"
val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
fun with_size genuine_only k =
- if k > size then
- (NONE, !current_result)
+ if k > size then (NONE, !current_result)
else
let
val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
val _ = current_size := k
- val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
- (fn () => Isabelle_System.bash_output
- (executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k))
+ val ((response, _), timing) =
+ elapsed_time ("execution of size " ^ string_of_int k)
+ (fn () => Isabelle_System.bash_output
+ (executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k))
val _ = Quickcheck.add_timing timing current_result
in
- if response = "NONE\n" then
- with_size genuine_only (k + 1)
+ if response = "NONE\n" then with_size genuine_only (k + 1)
else
let
val output_value = the_default "NONE"
(try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
val ml_code =
"\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^ put_ml
- ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))";
+ ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))"
val ctxt' = ctxt
|> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
- |> Context.proof_map (exec false ml_code);
+ |> Context.proof_map (exec false ml_code)
val counterexample = get ctxt' ()
in
if is_genuine counterexample then
(counterexample, !current_result)
else
let
- val cex = Option.map (rpair []) (counterexample_of counterexample);
- val _ = message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
- val _ = message "Quickcheck continues to find a genuine counterexample...";
+ val cex = Option.map (rpair []) (counterexample_of counterexample)
+ val _ = message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex))
+ val _ = message "Quickcheck continues to find a genuine counterexample..."
in with_size true (k + 1) end
end
end
in with_size genuine_only 0 end
- in
- with_tmp_dir tmp_prefix run
- end;
+ in with_tmp_dir tmp_prefix run end
fun dynamic_value_strict opts cookie ctxt postproc t =
let
fun evaluator program _ vs_ty_t deps =
Exn.interruptible_capture (value opts ctxt cookie)
- (Code_Target.evaluator ctxt target program deps true vs_ty_t);
- in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end;
+ (Code_Target.evaluator ctxt target program deps true vs_ty_t)
+ in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
(** counterexample generator **)
@@ -317,7 +322,7 @@
| Existential_Counterexample of (term * counterexample) list
| Empty_Assignment
-fun map_counterexample f Empty_Assignment = Empty_Assignment
+fun map_counterexample _ Empty_Assignment = Empty_Assignment
| map_counterexample f (Universal_Counterexample (t, c)) =
Universal_Counterexample (f t, map_counterexample f c)
| map_counterexample f (Existential_Counterexample cs) =
@@ -327,18 +332,18 @@
(
type T =
(unit -> (bool * term list) option) *
- (unit -> counterexample option);
+ (unit -> counterexample option)
val empty: T =
(fn () => raise Fail "counterexample",
- fn () => raise Fail "existential_counterexample");
- fun init _ = empty;
-);
+ fn () => raise Fail "existential_counterexample")
+ fun init _ = empty
+)
val get_counterexample = #1 o Data.get;
val get_existential_counterexample = #2 o Data.get;
-val put_counterexample = Data.map o @{apply 2(1)} o K;
-val put_existential_counterexample = Data.map o @{apply 2(2)} o K;
+val put_counterexample = Data.map o @{apply 2(1)} o K
+val put_existential_counterexample = Data.map o @{apply 2(2)} o K
fun finitize_functions (xTs, t) =
let
@@ -350,27 +355,27 @@
Const (@{const_name "Quickcheck_Narrowing.eval_cfun"},
Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT)
fun eval_function (Type (@{type_name fun}, [dT, rT])) =
- let
- val (rt', rT') = eval_function rT
- in
- case dT of
- Type (@{type_name fun}, _) =>
- (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
- Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
- | _ =>
- (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
- Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
- end
+ let
+ val (rt', rT') = eval_function rT
+ in
+ (case dT of
+ Type (@{type_name fun}, _) =>
+ (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
+ Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
+ | _ =>
+ (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
+ Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT'])))
+ end
| eval_function (T as Type (@{type_name prod}, [fT, sT])) =
- let
- val (ft', fT') = eval_function fT
- val (st', sT') = eval_function sT
- val T' = Type (@{type_name prod}, [fT', sT'])
- val map_const = Const (@{const_name map_prod}, (fT' --> fT) --> (sT' --> sT) --> T' --> T)
- fun apply_dummy T t = absdummy T (t (Bound 0))
- in
- (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T')
- end
+ let
+ val (ft', fT') = eval_function fT
+ val (st', sT') = eval_function sT
+ val T' = Type (@{type_name prod}, [fT', sT'])
+ val map_const = Const (@{const_name map_prod}, (fT' --> fT) --> (sT' --> sT) --> T' --> T)
+ fun apply_dummy T t = absdummy T (t (Bound 0))
+ in
+ (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T')
+ end
| eval_function T = (I, T)
val (tt, boundTs') = split_list (map eval_function boundTs)
val t' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) boundTs), t)
@@ -381,63 +386,63 @@
fun dest_ffun (Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT])) = (dT, rT)
fun eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Constant"}, T) $ value) =
- absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value)
+ absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value)
| eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Update"}, T) $ a $ b $ f) =
- let
- val (T1, T2) = dest_ffun (body_type T)
- in
- Quickcheck_Common.mk_fun_upd T1 T2
- (eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f)
- end
+ let
+ val (T1, T2) = dest_ffun (body_type T)
+ in
+ Quickcheck_Common.mk_fun_upd T1 T2
+ (eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f)
+ end
| eval_finite_functions t = t
+
(** tester **)
val rewrs =
- map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
- (@{thms all_simps} @ @{thms ex_simps})
- @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
- [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all},
- @{thm meta_eq_to_obj_eq [OF Ex1_def]}]
+ map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
+ (@{thms all_simps} @ @{thms ex_simps}) @
+ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
+ [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all},
+ @{thm meta_eq_to_obj_eq [OF Ex1_def]}]
fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t
fun strip_quantifiers (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
- apfst (cons (@{const_name Ex}, (x, T))) (strip_quantifiers t)
+ apfst (cons (@{const_name Ex}, (x, T))) (strip_quantifiers t)
| strip_quantifiers (Const (@{const_name All}, _) $ Abs (x, T, t)) =
- apfst (cons (@{const_name All}, (x, T))) (strip_quantifiers t)
+ apfst (cons (@{const_name All}, (x, T))) (strip_quantifiers t)
| strip_quantifiers t = ([], t)
-fun contains_existentials t = exists (fn (Q, _) => Q = @{const_name Ex}) (fst (strip_quantifiers t))
+fun contains_existentials t =
+ exists (fn (Q, _) => Q = @{const_name Ex}) (fst (strip_quantifiers t))
fun mk_property qs t =
let
fun enclose (@{const_name Ex}, (x, T)) t =
- Const (@{const_name Quickcheck_Narrowing.exists}, (T --> @{typ property}) --> @{typ property})
- $ Abs (x, T, t)
+ Const (@{const_name Quickcheck_Narrowing.exists},
+ (T --> @{typ property}) --> @{typ property}) $ Abs (x, T, t)
| enclose (@{const_name All}, (x, T)) t =
- Const (@{const_name Quickcheck_Narrowing.all}, (T --> @{typ property}) --> @{typ property})
- $ Abs (x, T, t)
- in
- fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ t)
- end
+ Const (@{const_name Quickcheck_Narrowing.all},
+ (T --> @{typ property}) --> @{typ property}) $ Abs (x, T, t)
+ in fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ t) end
fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
- Case_Translation.make_case ctxt Case_Translation.Quiet Name.context (Free (x, T)) (map (fn (t, c) =>
- (t, mk_case_term ctxt (p - 1) qs' c)) cs)
+ Case_Translation.make_case ctxt Case_Translation.Quiet Name.context (Free (x, T)) (map (fn (t, c) =>
+ (t, mk_case_term ctxt (p - 1) qs' c)) cs)
| mk_case_term ctxt p ((@{const_name All}, _) :: qs') (Universal_Counterexample (t, c)) =
- if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
+ if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
-val post_process = (perhaps (try Quickcheck_Common.post_process_term)) o eval_finite_functions
+val post_process =
+ perhaps (try Quickcheck_Common.post_process_term) o eval_finite_functions
fun mk_terms ctxt qs result =
let
- val
- ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs)
- in
- map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps
- |> map (apsnd post_process)
- end
+ val ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs)
+ in
+ map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps
+ |> map (apsnd post_process)
+ end
fun test_term ctxt catch_code_errors (t, _) =
let
@@ -453,8 +458,8 @@
if Config.get ctxt allow_existentials andalso contains_existentials pnf_t then
let
fun wrap f (qs, t) =
- let val (qs1, qs2) = split_list qs in
- apfst (map2 pair qs1) (f (qs2, t)) end
+ let val (qs1, qs2) = split_list qs
+ in apfst (map2 pair qs1) (f (qs2, t)) end
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
val act = if catch_code_errors then try else (fn f => SOME o f)
@@ -465,14 +470,14 @@
"Narrowing_Generators.put_existential_counterexample"))
ctxt (apfst o Option.map o map_counterexample)
in
- case act execute (mk_property qs prop_t) of
+ (case act execute (mk_property qs prop_t) of
SOME (counterexample, result) => Quickcheck.Result
{counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
evaluation_terms = Option.map (K []) counterexample,
timings = #timings (dest_result result), reports = #reports (dest_result result)}
| NONE =>
(Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing";
- Quickcheck.empty_result)
+ Quickcheck.empty_result))
end
else
let
@@ -481,10 +486,12 @@
fun wrap f t = uncurry (fold_rev Term.abs) (f (strip_abs t))
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
fun ensure_testable t =
- Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
+ Const (@{const_name Quickcheck_Narrowing.ensure_testable},
+ fastype_of t --> fastype_of t) $ t
fun is_genuine (SOME (true, _)) = true
| is_genuine _ = false
- val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
+ val counterexample_of =
+ Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
val act = if catch_code_errors then try else (fn f => SOME o f)
val execute =
dynamic_value_strict (false, opts)
@@ -493,7 +500,7 @@
"Narrowing_Generators.put_counterexample"))
ctxt (apfst o Option.map o apsnd o map)
in
- case act execute (ensure_testable (finitize t')) of
+ (case act execute (ensure_testable (finitize t')) of
SOME (counterexample, result) =>
Quickcheck.Result
{counterexample = counterexample_of counterexample,
@@ -502,14 +509,14 @@
reports = #reports (dest_result result)}
| NONE =>
(Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing";
- Quickcheck.empty_result)
+ Quickcheck.empty_result))
end
- end;
+ end
fun test_goals ctxt catch_code_errors insts goals =
- if (not (getenv "ISABELLE_GHC" = "")) then
+ if not (getenv "ISABELLE_GHC" = "") then
let
- val _ = Quickcheck.message ctxt "Testing conjecture with Quickcheck-narrowing...";
+ val _ = Quickcheck.message ctxt "Testing conjecture with Quickcheck-narrowing..."
val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
in
Quickcheck_Common.collect_results (test_term ctxt catch_code_errors)
@@ -522,9 +529,10 @@
^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false.");
[Quickcheck.empty_result])
+
(* setup *)
-val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false);
+val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false)
val _ =
Theory.setup
@@ -532,6 +540,6 @@
#> Code.datatype_interpretation ensure_partial_term_of_code
#> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
(@{sort narrowing}, instantiate_narrowing_datatype)
- #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals))));
+ #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals))))
-end;
+end
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Apr 14 15:33:23 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Apr 14 15:33:51 2016 +0200
@@ -10,37 +10,39 @@
val strip_imp : term -> (term list * term)
val reflect_bool : bool -> term
val define_functions : ((term list -> term list) * (Proof.context -> tactic) option)
- -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context
+ -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context
val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
-> (string * sort -> string * sort) option
val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
-> (typ option * (term * term list)) list list
val register_predicate : term * string -> Context.generic -> Context.generic
val mk_safe_if : term -> term -> term * term * (bool -> term) -> bool -> term
- val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
+ val collect_results : ('a -> Quickcheck.result) -> 'a list ->
+ Quickcheck.result list -> Quickcheck.result list
type result = (bool * term list) option * Quickcheck.report option
- type generator = string * ((theory -> typ list -> bool) *
+ type generator = string * ((theory -> typ list -> bool) *
(Proof.context -> (term * term list) list -> bool -> int list -> result))
val generator_test_goal_terms :
generator -> Proof.context -> bool -> (string * typ) list
-> (term * term list) list -> Quickcheck.result list
- type instantiation = Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list
- -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+ type instantiation =
+ Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list ->
+ string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
val ensure_sort :
(((sort * sort) * sort) *
((theory -> string list -> Old_Datatype_Aux.descr * (string * sort) list * string list
- * string * (string list * string list) * (typ list * typ list)) * instantiation))
- -> Old_Datatype_Aux.config -> string list -> theory -> theory
- val ensure_common_sort_datatype :
- (sort * instantiation) -> Old_Datatype_Aux.config -> string list -> theory -> theory
+ * string * (string list * string list) * (typ list * typ list)) * instantiation)) ->
+ Old_Datatype_Aux.config -> string list -> theory -> theory
+ val ensure_common_sort_datatype : (sort * instantiation) -> Old_Datatype_Aux.config ->
+ string list -> theory -> theory
val datatype_interpretation : string -> sort * instantiation -> theory -> theory
val gen_mk_parametric_generator_expr :
- (((Proof.context -> term * term list -> term) * term) * typ)
- -> Proof.context -> (term * term list) list -> term
+ (((Proof.context -> term * term list -> term) * term) * typ) ->
+ Proof.context -> (term * term list) list -> term
val mk_fun_upd : typ -> typ -> term * term -> term -> term
val post_process_term : term -> term
val test_term : generator -> Proof.context -> bool -> term * term list -> Quickcheck.result
-end;
+end
structure Quickcheck_Common : QUICKCHECK_COMMON =
struct
@@ -51,27 +53,32 @@
val define_foundationally = false
+
(* HOLogic's term functions *)
-fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
+fun strip_imp (Const(@{const_name HOL.implies}, _) $ A $ B) = apfst (cons A) (strip_imp B)
| strip_imp A = ([], A)
-fun reflect_bool b = if b then @{term "True"} else @{term "False"}
+fun reflect_bool b = if b then @{term True} else @{term False}
-fun mk_undefined T = Const(@{const_name undefined}, T)
+fun mk_undefined T = Const (@{const_name undefined}, T)
+
(* testing functions: testing with increasing sizes (and cardinalities) *)
type result = (bool * term list) option * Quickcheck.report option
-type generator = string * ((theory -> typ list -> bool) *
- (Proof.context -> (term * term list) list -> bool -> int list -> result))
+type generator =
+ string * ((theory -> typ list -> bool) *
+ (Proof.context -> (term * term list) list -> bool -> int list -> result))
fun check_test_term t =
let
- val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
- error "Term to be tested contains type variables";
- val _ = null (Term.add_vars t []) orelse
- error "Term to be tested contains schematic variables";
+ val _ =
+ (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
+ error "Term to be tested contains type variables"
+ val _ =
+ null (Term.add_vars t []) orelse
+ error "Term to be tested contains schematic variables"
in () end
fun cpu_time description e =
@@ -85,55 +92,59 @@
val _ = check_test_term t
val names = Term.add_free_names t []
val current_size = Unsynchronized.ref 0
- val current_result = Unsynchronized.ref Quickcheck.empty_result
- val act = if catch_code_errors then try else (fn f => SOME o f)
- val (test_fun, comp_time) = cpu_time "quickcheck compilation"
- (fn () => act (compile ctxt) [(t, eval_terms)]);
+ val current_result = Unsynchronized.ref Quickcheck.empty_result
+ val act = if catch_code_errors then try else (fn f => SOME o f)
+ val (test_fun, comp_time) =
+ cpu_time "quickcheck compilation" (fn () => act (compile ctxt) [(t, eval_terms)])
val _ = Quickcheck.add_timing comp_time current_result
fun with_size test_fun genuine_only k =
- if k > Config.get ctxt Quickcheck.size then
- NONE
+ if k > Config.get ctxt Quickcheck.size then NONE
else
let
- val _ = Quickcheck.verbose_message ctxt
- ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
+ val _ =
+ Quickcheck.verbose_message ctxt
+ ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
val _ = current_size := k
val ((result, report), time) =
cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1])
- val _ = if Config.get ctxt Quickcheck.timing then
- Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
+ val _ =
+ if Config.get ctxt Quickcheck.timing then
+ Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms")
+ else ()
val _ = Quickcheck.add_timing time current_result
val _ = Quickcheck.add_report k report current_result
in
- case result of
+ (case result of
NONE => with_size test_fun genuine_only (k + 1)
| SOME (true, ts) => SOME (true, ts)
| SOME (false, ts) =>
- if abort_potential then SOME (false, ts)
- else
- let
- val (ts1, ts2) = chop (length names) ts
- val (eval_terms', _) = chop (length ts2) eval_terms
- val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
- in
- (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
- Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
- with_size test_fun true k)
- end
- end;
+ if abort_potential then SOME (false, ts)
+ else
+ let
+ val (ts1, ts2) = chop (length names) ts
+ val (eval_terms', _) = chop (length ts2) eval_terms
+ val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
+ in
+ Quickcheck.message ctxt
+ (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+ Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
+ with_size test_fun true k
+ end)
+ end
in
case test_fun of
- NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
- !current_result)
+ NONE =>
+ (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
+ !current_result)
| SOME test_fun =>
- let
- val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...");
- val (response, exec_time) =
- cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1)
- val _ = Quickcheck.add_response names eval_terms response current_result
- val _ = Quickcheck.add_timing exec_time current_result
- in !current_result end
- end;
+ let
+ val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...")
+ val (response, exec_time) =
+ cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1)
+ val _ = Quickcheck.add_response names eval_terms response current_result
+ val _ = Quickcheck.add_timing exec_time current_result
+ in !current_result end
+ end
fun test_term_with_cardinality (name, (size_matters_for, compile)) ctxt catch_code_errors ts =
let
@@ -145,105 +156,104 @@
val names = Term.add_free_names (hd ts') []
val Ts = map snd (Term.add_frees (hd ts') [])
val current_result = Unsynchronized.ref Quickcheck.empty_result
- fun test_card_size test_fun genuine_only (card, size) =
- (* FIXME: why decrement size by one? *)
+ fun test_card_size test_fun genuine_only (card, size) = (* FIXME: why decrement size by one? *)
let
val _ =
Quickcheck.verbose_message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
(if size = 0 then "" else "data size: " ^ string_of_int size ^ " and ") ^
- "cardinality: " ^ string_of_int card)
+ "cardinality: " ^ string_of_int card)
val (ts, timing) =
cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
(fn () => fst (test_fun genuine_only [card, size + 1]))
val _ = Quickcheck.add_timing timing current_result
- in
- Option.map (pair (card, size)) ts
- end
+ in Option.map (pair (card, size)) ts end
val enumeration_card_size =
if size_matters_for thy Ts then
map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size))
|> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
- else
- map (rpair 0) (1 upto (length ts))
+ else map (rpair 0) (1 upto (length ts))
val act = if catch_code_errors then try else (fn f => SOME o f)
val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => act (compile ctxt) ts)
val _ = Quickcheck.add_timing comp_time current_result
in
- case test_fun of
- NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
- !current_result)
+ (case test_fun of
+ NONE =>
+ (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
+ !current_result)
| SOME test_fun =>
- let
- val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...");
- fun test genuine_only enum = case get_first (test_card_size test_fun genuine_only) enum of
- SOME ((card, _), (true, ts)) =>
- Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (true, ts)) current_result
- | SOME ((card, size), (false, ts)) =>
- if abort_potential then
- Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (false, ts)) current_result
- else
- let
- val (ts1, ts2) = chop (length names) ts
- val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1))
- val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
- in
- (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
- Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
- test true (snd (take_prefix (fn x => not (x = (card, size))) enum)))
- end
- | NONE => ()
- in (test genuine_only enumeration_card_size; !current_result) end
+ let
+ val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...")
+ fun test genuine_only enum =
+ (case get_first (test_card_size test_fun genuine_only) enum of
+ SOME ((card, _), (true, ts)) =>
+ Quickcheck.add_response names (nth eval_terms (card - 1))
+ (SOME (true, ts)) current_result
+ | SOME ((card, size), (false, ts)) =>
+ if abort_potential then
+ Quickcheck.add_response names (nth eval_terms (card - 1))
+ (SOME (false, ts)) current_result
+ else
+ let
+ val (ts1, ts2) = chop (length names) ts
+ val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1))
+ val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
+ in
+ Quickcheck.message ctxt
+ (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+ Quickcheck.message ctxt
+ "Quickcheck continues to find a genuine counterexample...";
+ test true (snd (take_prefix (fn x => not (x = (card, size))) enum))
+ end
+ | NONE => ())
+ in (test genuine_only enumeration_card_size; !current_result) end)
end
fun get_finite_types ctxt =
fst (chop (Config.get ctxt Quickcheck.finite_type_size)
- [@{typ "Enum.finite_1"}, @{typ "Enum.finite_2"}, @{typ "Enum.finite_3"},
- @{typ "Enum.finite_4"}, @{typ "Enum.finite_5"}])
+ [@{typ Enum.finite_1}, @{typ Enum.finite_2}, @{typ Enum.finite_3},
+ @{typ Enum.finite_4}, @{typ Enum.finite_5}])
exception WELLSORTED of string
fun monomorphic_term thy insts default_T =
let
fun subst (T as TFree (v, S)) =
- let
- val T' = AList.lookup (op =) insts v
- |> the_default default_T
- in if Sign.of_sort thy (T', S) then T'
- else raise (WELLSORTED ("For instantiation with default_type " ^
- Syntax.string_of_typ_global thy default_T ^
- ":\n" ^ Syntax.string_of_typ_global thy T' ^
- " to be substituted for variable " ^
- Syntax.string_of_typ_global thy T ^ " does not have sort " ^
- Syntax.string_of_sort_global thy S))
- end
- | subst T = T;
- in (map_types o map_atyps) subst end;
+ let val T' = AList.lookup (op =) insts v |> the_default default_T in
+ if Sign.of_sort thy (T', S) then T'
+ else raise (WELLSORTED ("For instantiation with default_type " ^
+ Syntax.string_of_typ_global thy default_T ^
+ ":\n" ^ Syntax.string_of_typ_global thy T' ^
+ " to be substituted for variable " ^
+ Syntax.string_of_typ_global thy T ^ " does not have sort " ^
+ Syntax.string_of_sort_global thy S))
+ end
+ | subst T = T
+ in (map_types o map_atyps) subst end
datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
+
(* minimalistic preprocessing *)
-fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) =
- let
- val (a', t') = strip_all t
- in ((a, T) :: a', t') end
- | strip_all t = ([], t);
+fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) =
+ let val (a', t') = strip_all t
+ in ((a, T) :: a', t') end
+ | strip_all t = ([], t)
fun preprocess ctxt t =
let
val thy = Proof_Context.theory_of ctxt
val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
- val rewrs = map (swap o dest) @{thms all_simps} @
- (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff},
- @{thm bot_fun_def}, @{thm less_bool_def}])
+ val rewrs =
+ map (swap o dest) @{thms all_simps} @
+ (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff},
+ @{thm bot_fun_def}, @{thm less_bool_def}])
val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t)
val (vs, body) = strip_all t'
val vs' = Variable.variant_frees ctxt [t'] vs
- in
- subst_bounds (map Free (rev vs'), body)
- end
+ in subst_bounds (map Free (rev vs'), body) end
-
+
structure Subtype_Predicates = Generic_Data
(
type T = (term * string) list
@@ -257,31 +267,31 @@
fun subtype_preprocess ctxt (T, (t, ts)) =
let
val preds = Subtype_Predicates.get (Context.Proof ctxt)
- fun matches (p $ _) = AList.defined Term.could_unify preds p
+ fun matches (p $ _) = AList.defined Term.could_unify preds p
fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p)
fun subst_of (tyco, v as Free (x, repT)) =
let
val [(info, _)] = Typedef.get_info ctxt tyco
val repT' = Logic.varifyT_global (#rep_type info)
- val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty
+ val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty
val absT = Envir.subst_type substT (Logic.varifyT_global (#abs_type info))
in (v, Const (#Rep_name info, absT --> repT) $ Free (x, absT)) end
val (prems, concl) = strip_imp t
val subst = map subst_of (map_filter get_match prems)
val t' = Term.subst_free subst
(fold_rev (curry HOLogic.mk_imp) (filter_out matches prems) concl)
- in
- (T, (t', ts))
- end
+ in (T, (t', ts)) end
+
(* instantiation of type variables with concrete types *)
-
+
fun instantiate_goals lthy insts goals =
let
fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
val thy = Proof_Context.theory_of lthy
val default_insts =
- if Config.get lthy Quickcheck.finite_types then get_finite_types else Quickcheck.default_type
+ if Config.get lthy Quickcheck.finite_types
+ then get_finite_types else Quickcheck.default_type
val inst_goals =
map (fn (check_goal, eval_terms) =>
if not (null (Term.add_tfree_names check_goal [])) then
@@ -289,67 +299,61 @@
(pair (SOME T) o Term o apfst (preprocess lthy))
(map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts lthy)
- else
- [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals
+ else [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals
val error_msg =
cat_lines
(maps (map_filter (fn (_, Term _) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
fun is_wellsorted_term (T, Term t) = SOME (T, t)
| is_wellsorted_term (_, Wellsorted_Error _) = NONE
val correct_inst_goals =
- case map (map_filter is_wellsorted_term) inst_goals of
+ (case map (map_filter is_wellsorted_term) inst_goals of
[[]] => error error_msg
- | xs => xs
+ | xs => xs)
val _ = if Config.get lthy Quickcheck.quiet then () else warning error_msg
- in
- correct_inst_goals
- end
+ in correct_inst_goals end
+
(* compilation of testing functions *)
fun mk_safe_if genuine_only none (cond, then_t, else_t) genuine =
let
val T = fastype_of then_t
- val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
+ val if_t = Const (@{const_name If}, @{typ bool} --> T --> T --> T)
in
- Const (@{const_name "Quickcheck_Random.catch_match"}, T --> T --> T) $
+ Const (@{const_name "Quickcheck_Random.catch_match"}, T --> T --> T) $
(if_t $ cond $ then_t $ else_t genuine) $
(if_t $ genuine_only $ none $ else_t false)
end
fun collect_results f [] results = results
| collect_results f (t :: ts) results =
- let
- val result = f t
- in
- if Quickcheck.found_counterexample result then
- (result :: results)
- else
- collect_results f ts (result :: results)
- end
+ let val result = f t in
+ if Quickcheck.found_counterexample result then result :: results
+ else collect_results f ts (result :: results)
+ end
fun generator_test_goal_terms generator ctxt catch_code_errors insts goals =
let
val use_subtype = Config.get ctxt Quickcheck.use_subtype
fun add_eval_term t ts = if is_Free t then ts else ts @ [t]
fun add_equation_eval_terms (t, eval_terms) =
- case try HOLogic.dest_eq (snd (strip_imp t)) of
+ (case try HOLogic.dest_eq (snd (strip_imp t)) of
SOME (lhs, rhs) => (t, add_eval_term lhs (add_eval_term rhs eval_terms))
- | NONE => (t, eval_terms)
+ | NONE => (t, eval_terms))
fun test_term' goal =
- case goal of
+ (case goal of
[(NONE, t)] => test_term generator ctxt catch_code_errors t
- | ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts)
- val goals' = instantiate_goals ctxt insts goals
+ | ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts))
+ val goals' =
+ instantiate_goals ctxt insts goals
|> (if use_subtype then map (map (subtype_preprocess ctxt)) else I)
|> map (map (apsnd add_equation_eval_terms))
in
if Config.get ctxt Quickcheck.finite_types then
collect_results test_term' goals' []
- else
- collect_results (test_term generator ctxt catch_code_errors)
- (maps (map snd) goals') []
- end;
+ else collect_results (test_term generator ctxt catch_code_errors) (maps (map snd) goals') []
+ end
+
(* defining functions *)
@@ -388,38 +392,42 @@
(names ~~ eqs) lthy
end)
+
(** ensuring sort constraints **)
-type instantiation = Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list
- -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+type instantiation =
+ Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list ->
+ string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
fun perhaps_constrain thy insts raw_vs =
let
- fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy)
- (Logic.varifyT_global T, sort);
+ fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) (Logic.varifyT_global T, sort)
val vtab = Vartab.empty
|> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
- |> fold meet insts;
- in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
- end handle Sorts.CLASS_ERROR _ => NONE;
+ |> fold meet insts
+ in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0))) end
+ handle Sorts.CLASS_ERROR _ => NONE
fun ensure_sort (((sort_vs, aux_sort), sort), (the_descr, instantiate)) config raw_tycos thy =
let
- val algebra = Sign.classes_of thy;
+ val algebra = Sign.classes_of thy
val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = the_descr thy raw_tycos
val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd)
(Old_Datatype_Aux.interpret_construction descr vs constr)
val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] }
@ insts_of aux_sort { atyp = K [], dtyp = K o K }
- val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos;
- in if has_inst then thy
- else case perhaps_constrain thy insts vs
- of SOME constrain => instantiate config descr
- (map constrain vs) tycos prfx (names, auxnames)
- ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
- | NONE => thy
- end;
+ val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos
+ in
+ if has_inst then thy
+ else
+ (case perhaps_constrain thy insts vs of
+ SOME constrain =>
+ instantiate config descr
+ (map constrain vs) tycos prfx (names, auxnames)
+ ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
+ | NONE => thy)
+ end
fun ensure_common_sort_datatype (sort, instantiate) =
ensure_sort (((@{sort typerep}, @{sort term_of}), sort),
@@ -427,86 +435,89 @@
fun datatype_interpretation name =
BNF_LFP_Compat.interpretation name compat_prefs o ensure_common_sort_datatype
-
+
+
(** generic parametric compilation **)
fun gen_mk_parametric_generator_expr ((mk_generator_expr, out_of_bounds), T) ctxt ts =
let
- val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
- fun mk_if (index, (t, eval_terms)) else_t = if_t $
- (HOLogic.eq_const @{typ natural} $ Bound 0 $ HOLogic.mk_number @{typ natural} index) $
+ val if_t = Const (@{const_name If}, @{typ bool} --> T --> T --> T)
+ fun mk_if (index, (t, eval_terms)) else_t =
+ if_t $ (HOLogic.eq_const @{typ natural} $ Bound 0 $ HOLogic.mk_number @{typ natural} index) $
(mk_generator_expr ctxt (t, eval_terms)) $ else_t
- in
- absdummy @{typ natural} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
- end
+ in absdummy @{typ natural} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds) end
+
(** post-processing of function terms **)
fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
| dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
-fun mk_fun_upd T1 T2 (t1, t2) t =
+fun mk_fun_upd T1 T2 (t1, t2) t =
Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
fun dest_fun_upds t =
- case try dest_fun_upd t of
+ (case try dest_fun_upd t of
NONE =>
(case t of
- Abs (_, _, _) => ([], t)
+ Abs (_, _, _) => ([], t)
| _ => raise TERM ("dest_fun_upds", [t]))
- | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)
+ | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0))
fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
| make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
| make_set T1 ((t1, @{const True}) :: tps) =
- Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
- $ t1 $ (make_set T1 tps)
+ Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool}) $
+ t1 $ (make_set T1 tps)
| make_set T1 ((_, t) :: _) = raise TERM ("make_set", [t])
fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool})
- | make_coset T tps =
+ | make_coset T tps =
let
val U = T --> @{typ bool}
fun invert @{const False} = @{const True}
| invert @{const True} = @{const False}
in
- Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U)
- $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
+ Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U) $
+ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
end
fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
| make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
| make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
-
+
fun post_process_term t =
let
fun map_Abs f t =
- case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t])
- fun process_args t = case strip_comb t of
- (c as Const (_, _), ts) => list_comb (c, map post_process_term ts)
+ (case t of
+ Abs (x, T, t') => Abs (x, T, f t')
+ | _ => raise TERM ("map_Abs", [t]))
+ fun process_args t =
+ (case strip_comb t of
+ (c as Const (_, _), ts) => list_comb (c, map post_process_term ts))
in
- case fastype_of t of
+ (case fastype_of t of
Type (@{type_name fun}, [T1, T2]) =>
(case try dest_fun_upds t of
SOME (tps, t) =>
- (map (apply2 post_process_term) tps, map_Abs post_process_term t)
- |> (case T2 of
- @{typ bool} =>
- (case t of
- Abs(_, _, @{const False}) => fst #> rev #> make_set T1
- | Abs(_, _, @{const True}) => fst #> rev #> make_coset T1
- | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
- | _ => raise TERM ("post_process_term", [t]))
- | Type (@{type_name option}, _) =>
- (case t of
- Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2
- | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
- | _ => make_fun_upds T1 T2)
- | _ => make_fun_upds T1 T2)
+ (map (apply2 post_process_term) tps, map_Abs post_process_term t) |>
+ (case T2 of
+ @{typ bool} =>
+ (case t of
+ Abs(_, _, @{const False}) => fst #> rev #> make_set T1
+ | Abs(_, _, @{const True}) => fst #> rev #> make_coset T1
+ | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
+ | _ => raise TERM ("post_process_term", [t]))
+ | Type (@{type_name option}, _) =>
+ (case t of
+ Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2
+ | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
+ | _ => make_fun_upds T1 T2)
+ | _ => make_fun_upds T1 T2)
| NONE => process_args t)
- | _ => process_args t
+ | _ => process_args t)
end
-end;
+end
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Thu Apr 14 15:33:23 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Thu Apr 14 15:33:51 2016 +0200
@@ -7,17 +7,19 @@
signature RANDOM_GENERATORS =
sig
type seed = Random_Engine.seed
- val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
- -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
- -> seed -> (('a -> 'b) * (unit -> term)) * seed
- val compile_generator_expr:
- Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
- val put_counterexample: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> (bool * term list) option * seed)
- -> Proof.context -> Proof.context
- val put_counterexample_report: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> ((bool * term list) option * (bool list * bool)) * seed)
- -> Proof.context -> Proof.context
+ val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term) ->
+ (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed) ->
+ seed -> (('a -> 'b) * (unit -> term)) * seed
+ val compile_generator_expr: Proof.context -> (term * term list) list -> bool -> int list ->
+ (bool * term list) option * Quickcheck.report option
+ val put_counterexample: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural ->
+ seed -> (bool * term list) option * seed) -> Proof.context -> Proof.context
+ val put_counterexample_report: (unit -> Code_Numeral.natural -> bool ->
+ Code_Numeral.natural -> seed -> ((bool * term list) option * (bool list * bool)) * seed) ->
+ Proof.context -> Proof.context
val instantiate_random_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
- (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+ (string * sort) list -> string list -> string -> string list * string list ->
+ typ list * typ list -> theory -> theory
end;
structure Random_Generators : RANDOM_GENERATORS =
@@ -25,22 +27,22 @@
(** abstract syntax **)
-fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
+fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"})
val size = @{term "i::natural"};
val size_pred = @{term "(i::natural) - 1"};
val size' = @{term "j::natural"};
val seed = @{term "s::Random.seed"};
-val resultT = @{typ "(bool * term list) option"};
+val resultT = @{typ "(bool \<times> term list) option"};
-(** typ "'a => 'b" **)
+
+(** typ "'a \<Rightarrow> 'b" **)
type seed = Random_Engine.seed;
fun random_fun T1 T2 eq term_of random random_split seed =
let
- val fun_upd = Const (@{const_name fun_upd},
- (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
+ val fun_upd = Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
val ((_, t2), seed') = random seed;
val (seed'', seed''') = random_split seed';
@@ -474,6 +476,7 @@
val test_goals =
Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));
+
(** setup **)