author | bulwahn |
Fri, 01 Apr 2011 13:49:36 +0200 | |
changeset 42194 | bd416284a432 |
parent 42117 | 306713ec55c3 |
child 42195 | 1e7b62c93f5d |
permissions | -rw-r--r-- |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
1 |
(* Author: Lukas Bulwahn, TU Muenchen *) |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
2 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
3 |
header {* A simple counterexample generator performing exhaustive testing *} |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
4 |
|
41918 | 5 |
theory Quickcheck_Exhaustive |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
6 |
imports Quickcheck |
41920
d4fb7a418152
moving exhaustive_generators.ML to Quickcheck directory
bulwahn
parents:
41918
diff
changeset
|
7 |
uses ("Tools/Quickcheck/exhaustive_generators.ML") |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
8 |
begin |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
9 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
10 |
subsection {* basic operations for exhaustive generators *} |
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
11 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
12 |
definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55) |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
13 |
where |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
14 |
[code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)" |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
15 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
16 |
subsection {* exhaustive generator type classes *} |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
17 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
18 |
class exhaustive = term_of + |
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
19 |
fixes exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option" |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
20 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
21 |
instantiation unit :: exhaustive |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
22 |
begin |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
23 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
24 |
definition "exhaustive f d = f (Code_Evaluation.valtermify ())" |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
25 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
26 |
instance .. |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
27 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
28 |
end |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
29 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
30 |
instantiation code_numeral :: exhaustive |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
31 |
begin |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
32 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
33 |
function exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option" |
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
34 |
where "exhaustive_code_numeral' f d i = |
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
35 |
(if d < i then None |
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
36 |
else (f (i, %_. Code_Evaluation.term_of i)) orelse (exhaustive_code_numeral' f d (i + 1)))" |
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
37 |
by pat_completeness auto |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
38 |
|
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
39 |
termination |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
40 |
by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
41 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
42 |
definition "exhaustive f d = exhaustive_code_numeral' f d 0" |
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
43 |
|
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
44 |
instance .. |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
45 |
|
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
46 |
end |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
47 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
48 |
instantiation nat :: exhaustive |
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
49 |
begin |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
50 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
51 |
definition "exhaustive f d = exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d" |
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
52 |
|
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
53 |
instance .. |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
54 |
|
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
55 |
end |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
56 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
57 |
instantiation int :: exhaustive |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
58 |
begin |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
59 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
60 |
function exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option" |
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
61 |
where "exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => exhaustive' f d (i + 1)))" |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
62 |
by pat_completeness auto |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
63 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
64 |
termination |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
65 |
by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
66 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
67 |
definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))" |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
68 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
69 |
instance .. |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
70 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
71 |
end |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
72 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
73 |
instantiation prod :: (exhaustive, exhaustive) exhaustive |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
74 |
begin |
40899
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
75 |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
76 |
definition |
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
77 |
"exhaustive f d = exhaustive (%(x, t1). exhaustive (%(y, t2). f ((x, y), |
41719
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
78 |
%u. let T1 = (Typerep.typerep (TYPE('a))); |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
79 |
T2 = (Typerep.typerep (TYPE('b))) |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
80 |
in Code_Evaluation.App (Code_Evaluation.App ( |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
81 |
Code_Evaluation.Const (STR ''Product_Type.Pair'') |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
82 |
(Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
83 |
(t1 ())) (t2 ()))) d) d" |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
84 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
85 |
instance .. |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
86 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
87 |
end |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
88 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
89 |
instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
90 |
begin |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
91 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
92 |
fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option" |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
93 |
where |
42117
306713ec55c3
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents:
41920
diff
changeset
|
94 |
"exhaustive_fun' f i d = (exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d) |
306713ec55c3
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents:
41920
diff
changeset
|
95 |
orelse (if i > 1 then |
306713ec55c3
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents:
41920
diff
changeset
|
96 |
exhaustive_fun' (%(g, gt). exhaustive (%(a, at). exhaustive (%(b, bt). |
306713ec55c3
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents:
41920
diff
changeset
|
97 |
f (g(a := b), |
306713ec55c3
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents:
41920
diff
changeset
|
98 |
(%_. let A = (Typerep.typerep (TYPE('a))); |
306713ec55c3
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents:
41920
diff
changeset
|
99 |
B = (Typerep.typerep (TYPE('b))); |
306713ec55c3
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents:
41920
diff
changeset
|
100 |
fun = (%T U. Typerep.Typerep (STR ''fun'') [T, U]) |
306713ec55c3
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents:
41920
diff
changeset
|
101 |
in |
306713ec55c3
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents:
41920
diff
changeset
|
102 |
Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App |
306713ec55c3
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents:
41920
diff
changeset
|
103 |
(Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B))))) |
306713ec55c3
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents:
41920
diff
changeset
|
104 |
(gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)" |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
105 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
106 |
definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option" |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
107 |
where |
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
108 |
"exhaustive_fun f d = exhaustive_fun' f d d" |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
109 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
110 |
instance .. |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
111 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
112 |
end |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
113 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
114 |
subsubsection {* A smarter enumeration scheme for functions over finite datatypes *} |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
115 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
116 |
class check_all = enum + term_of + |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
117 |
fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
118 |
fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
119 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
120 |
fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option" |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
121 |
where |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
122 |
"check_all_n_lists f n = |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
123 |
(if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))" |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
124 |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
125 |
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" |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
126 |
where |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
127 |
"mk_map_term T1 T2 domm rng = |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
128 |
(%_. let T1 = T1 (); |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
129 |
T2 = T2 (); |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
130 |
update_term = (%g (a, b). |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
131 |
Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
132 |
(Code_Evaluation.Const (STR ''Fun.fun_upd'') |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
133 |
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
134 |
Typerep.Typerep (STR ''fun'') [T1, |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
135 |
Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
136 |
g) a) b) |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
137 |
in |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
138 |
List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
139 |
|
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
140 |
instantiation "fun" :: ("{equal, check_all}", check_all) check_all |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
141 |
begin |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
142 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
143 |
definition |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
144 |
"check_all f = |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
145 |
(let |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
146 |
mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a))); |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
147 |
enum = (Enum.enum :: 'a list) |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
148 |
in check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst)) (Code_Numeral.of_nat (length enum)))" |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
149 |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
150 |
definition enum_term_of_fun :: "('a => 'b) itself => unit => term list" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
151 |
where |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
152 |
"enum_term_of_fun = (%_ _. let |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
153 |
enum_term_of_a = enum_term_of (TYPE('a)); |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
154 |
mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
155 |
in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
156 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
157 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
158 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
159 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
160 |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
161 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
162 |
instantiation unit :: check_all |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
163 |
begin |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
164 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
165 |
definition |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
166 |
"check_all f = f (Code_Evaluation.valtermify ())" |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
167 |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
168 |
definition enum_term_of_unit :: "unit itself => unit => term list" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
169 |
where |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
170 |
"enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
171 |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
172 |
instance .. |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
173 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
174 |
end |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
175 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
176 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
177 |
instantiation bool :: check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
178 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
179 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
180 |
definition |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
181 |
"check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))" |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
182 |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
183 |
definition enum_term_of_bool :: "bool itself => unit => term list" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
184 |
where |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
185 |
"enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
186 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
187 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
188 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
189 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
190 |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
191 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
192 |
instantiation prod :: (check_all, check_all) check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
193 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
194 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
195 |
definition |
41719
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
196 |
"check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
197 |
%u. let T1 = (Typerep.typerep (TYPE('a))); |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
198 |
T2 = (Typerep.typerep (TYPE('b))) |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
199 |
in Code_Evaluation.App (Code_Evaluation.App ( |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
200 |
Code_Evaluation.Const (STR ''Product_Type.Pair'') |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
201 |
(Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
202 |
(t1 ())) (t2 ()))))" |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
203 |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
204 |
definition enum_term_of_prod :: "('a * 'b) itself => unit => term list" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
205 |
where |
41719
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
206 |
"enum_term_of_prod = (%_ _. map (%(x, y). |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
207 |
let T1 = (Typerep.typerep (TYPE('a))); |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
208 |
T2 = (Typerep.typerep (TYPE('b))) |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
209 |
in Code_Evaluation.App (Code_Evaluation.App ( |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
210 |
Code_Evaluation.Const (STR ''Product_Type.Pair'') |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
211 |
(Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y) |
91c2510e19c5
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents:
41231
diff
changeset
|
212 |
(Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ()))) " |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
213 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
214 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
215 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
216 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
217 |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
218 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
219 |
instantiation sum :: (check_all, check_all) check_all |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
220 |
begin |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
221 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
222 |
definition |
41722
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
223 |
"check_all f = (case check_all (%(a, t). f (Inl a, %_. |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
224 |
let T1 = (Typerep.typerep (TYPE('a))); |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
225 |
T2 = (Typerep.typerep (TYPE('b))) |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
226 |
in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
227 |
(Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))) of Some x' => Some x' |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
228 |
| None => check_all (%(b, t). f (Inr b, %_. let |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
229 |
T1 = (Typerep.typerep (TYPE('a))); |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
230 |
T2 = (Typerep.typerep (TYPE('b))) |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
231 |
in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
232 |
(Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))))" |
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
233 |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
234 |
definition enum_term_of_sum :: "('a + 'b) itself => unit => term list" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
235 |
where |
41722
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
236 |
"enum_term_of_sum = (%_ _. |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
237 |
let |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
238 |
T1 = (Typerep.typerep (TYPE('a))); |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
239 |
T2 = (Typerep.typerep (TYPE('b))) |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
240 |
in |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
241 |
map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
242 |
(Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]]))) |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
243 |
(enum_term_of (TYPE('a)) ()) @ |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
244 |
map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
245 |
(Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]]))) |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
246 |
(enum_term_of (TYPE('b)) ()))" |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
247 |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
248 |
instance .. |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
249 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
250 |
end |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
251 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
252 |
instantiation nibble :: check_all |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
253 |
begin |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
254 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
255 |
definition |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
256 |
"check_all f = |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
257 |
f (Code_Evaluation.valtermify Nibble0) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
258 |
f (Code_Evaluation.valtermify Nibble1) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
259 |
f (Code_Evaluation.valtermify Nibble2) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
260 |
f (Code_Evaluation.valtermify Nibble3) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
261 |
f (Code_Evaluation.valtermify Nibble4) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
262 |
f (Code_Evaluation.valtermify Nibble5) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
263 |
f (Code_Evaluation.valtermify Nibble6) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
264 |
f (Code_Evaluation.valtermify Nibble7) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
265 |
f (Code_Evaluation.valtermify Nibble8) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
266 |
f (Code_Evaluation.valtermify Nibble9) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
267 |
f (Code_Evaluation.valtermify NibbleA) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
268 |
f (Code_Evaluation.valtermify NibbleB) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
269 |
f (Code_Evaluation.valtermify NibbleC) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
270 |
f (Code_Evaluation.valtermify NibbleD) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
271 |
f (Code_Evaluation.valtermify NibbleE) orelse |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
272 |
f (Code_Evaluation.valtermify NibbleF)" |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
273 |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
274 |
definition enum_term_of_nibble :: "nibble itself => unit => term list" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
275 |
where |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
276 |
"enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
277 |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
278 |
instance .. |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
279 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
280 |
end |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
281 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
282 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
283 |
instantiation char :: check_all |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
284 |
begin |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
285 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
286 |
definition |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
287 |
"check_all f = check_all (%(x, t1). check_all (%(y, t2). f (Char x y, %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))" |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
288 |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
289 |
definition enum_term_of_char :: "char itself => unit => term list" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
290 |
where |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
291 |
"enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
292 |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
293 |
instance .. |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
294 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
295 |
end |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
296 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
297 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
298 |
instantiation option :: (check_all) check_all |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
299 |
begin |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
300 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
301 |
definition |
41178
f4d3acf0c4cc
adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition
bulwahn
parents:
41177
diff
changeset
|
302 |
"check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App |
f4d3acf0c4cc
adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition
bulwahn
parents:
41177
diff
changeset
|
303 |
(Code_Evaluation.Const (STR ''Option.option.Some'') |
f4d3acf0c4cc
adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition
bulwahn
parents:
41177
diff
changeset
|
304 |
(Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))" |
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
305 |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
306 |
definition enum_term_of_option :: "'a option itself => unit => term list" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
307 |
where |
41722
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
308 |
"enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'') |
9575694d2da5
improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents:
41719
diff
changeset
|
309 |
(Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))" |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
310 |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
311 |
instance .. |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
312 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
313 |
end |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
314 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
315 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
316 |
instantiation Enum.finite_1 :: check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
317 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
318 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
319 |
definition |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
320 |
"check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)" |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
321 |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
322 |
definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
323 |
where |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
324 |
"enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
325 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
326 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
327 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
328 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
329 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
330 |
instantiation Enum.finite_2 :: check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
331 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
332 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
333 |
definition |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
334 |
"check_all f = (case f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))" |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
335 |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
336 |
definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
337 |
where |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
338 |
"enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
339 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
340 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
341 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
342 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
343 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
344 |
instantiation Enum.finite_3 :: check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
345 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
346 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
347 |
definition |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
348 |
"check_all f = (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3)))" |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
349 |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
350 |
definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
351 |
where |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
352 |
"enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))" |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
353 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
354 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
355 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
356 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
357 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
358 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
359 |
|
40620 | 360 |
subsection {* Defining combinators for any first-order data type *} |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
361 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
362 |
definition catch_match :: "term list option => term list option => term list option" |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
363 |
where |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
364 |
[code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)" |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
365 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
366 |
code_const catch_match |
41920
d4fb7a418152
moving exhaustive_generators.ML to Quickcheck directory
bulwahn
parents:
41918
diff
changeset
|
367 |
(Quickcheck "(_) handle Match => _") |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
368 |
|
41920
d4fb7a418152
moving exhaustive_generators.ML to Quickcheck directory
bulwahn
parents:
41918
diff
changeset
|
369 |
use "Tools/Quickcheck/exhaustive_generators.ML" |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
370 |
|
41918 | 371 |
setup {* Exhaustive_Generators.setup *} |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
372 |
|
40915
a4c956d1f91f
declaring quickcheck testers as default after their setup
bulwahn
parents:
40914
diff
changeset
|
373 |
declare [[quickcheck_tester = exhaustive]] |
a4c956d1f91f
declaring quickcheck testers as default after their setup
bulwahn
parents:
40914
diff
changeset
|
374 |
|
40899
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
375 |
hide_fact orelse_def catch_match_def |
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
376 |
no_notation orelse (infixr "orelse" 55) |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
377 |
hide_const (open) orelse catch_match mk_map_term check_all_n_lists |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
378 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
379 |
end |