author | bulwahn |
Fri, 10 Dec 2010 11:42:04 +0100 | |
changeset 41104 | 013adf7ebd96 |
parent 41085 | a549ff1d4070 |
child 41105 | a76ee71c3313 |
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 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
3 |
header {* Another simple counterexample generator *} |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
4 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
5 |
theory Smallcheck |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
6 |
imports Quickcheck |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
7 |
uses ("Tools/smallvalue_generators.ML") |
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 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
10 |
|
40620 | 11 |
subsection {* small value generator type classes *} |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
12 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
13 |
class small = term_of + |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
14 |
fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option" |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
15 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
16 |
instantiation unit :: small |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
17 |
begin |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
18 |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
19 |
definition "small f d = f ()" |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
20 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
21 |
instance .. |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
22 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
23 |
end |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
24 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
25 |
instantiation int :: small |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
26 |
begin |
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 |
function small' :: "(int => term list option) => int => int => term list option" |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
29 |
where "small' f d i = (if d < i then None else (case f i of Some t => Some t | None => small' f d (i + 1)))" |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
30 |
by pat_completeness auto |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
31 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
32 |
termination |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
33 |
by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
34 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
35 |
definition "small f d = small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))" |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
36 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
37 |
instance .. |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
38 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
39 |
end |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
40 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
41 |
instantiation prod :: (small, small) small |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
42 |
begin |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
43 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
44 |
definition |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
45 |
"small f d = small (%x. small (%y. f (x, y)) d) d" |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
46 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
47 |
instance .. |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
48 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
49 |
end |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
50 |
|
40899
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
51 |
subsection {* full small value generator type classes *} |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
52 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
53 |
class full_small = term_of + |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
54 |
fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option" |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
55 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
56 |
instantiation unit :: full_small |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
57 |
begin |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
58 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
59 |
definition "full_small f d = f (Code_Evaluation.valtermify ())" |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
60 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
61 |
instance .. |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
62 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
63 |
end |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
64 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
65 |
instantiation int :: full_small |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
66 |
begin |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
67 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
68 |
function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option" |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
69 |
where "full_small' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_small' f d (i + 1)))" |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
70 |
by pat_completeness auto |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
71 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
72 |
termination |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
73 |
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
|
74 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
75 |
definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))" |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
76 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
77 |
instance .. |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
78 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
79 |
end |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
80 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
81 |
instantiation prod :: (full_small, full_small) full_small |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
82 |
begin |
40899
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
83 |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
84 |
definition |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
85 |
"full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y), |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
86 |
%u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d" |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
87 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
88 |
instance .. |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
89 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
90 |
end |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
91 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
92 |
instantiation "fun" :: ("{equal, full_small}", full_small) full_small |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
93 |
begin |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
94 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
95 |
fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option" |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
96 |
where |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
97 |
"full_small_fun' f i d = (if i > 1 then |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
98 |
full_small (%(a, at). full_small (%(b, bt). |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
99 |
full_small_fun' (%(g, gt). f (g(a := b), |
40899
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
100 |
(%_. let T1 = (Typerep.typerep (TYPE('a))); |
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
101 |
T2 = (Typerep.typerep (TYPE('b))) |
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
102 |
in |
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
103 |
Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App |
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
104 |
(Code_Evaluation.Const (STR ''Fun.fun_upd'') |
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
105 |
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], |
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
106 |
Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) |
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
107 |
(gt ())) (at ())) (bt ())))) (i - 1) d) d) d |
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
108 |
else (if i > 0 then |
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
109 |
full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))" |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
110 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
111 |
definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option" |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
112 |
where |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
113 |
"full_small_fun f d = full_small_fun' f d d" |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
114 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
115 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
116 |
instance .. |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
117 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
118 |
end |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
119 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
120 |
subsubsection {* A smarter enumeration scheme for functions over finite datatypes *} |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
121 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
122 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
123 |
class check_all = enum + term_of + |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
124 |
fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option" |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
125 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
126 |
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
|
127 |
where |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
128 |
"check_all_n_lists f n = |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
129 |
(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
|
130 |
|
41104 | 131 |
instantiation "fun" :: ("{equal, check_all}", check_all) check_all |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
132 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
133 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
134 |
definition mk_map_term :: "'a list \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> unit \<Rightarrow> term" |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
135 |
where |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
136 |
"mk_map_term domm rng T2 = |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
137 |
(%_. let T1 = (Typerep.typerep (TYPE('a))); |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
138 |
T2 = T2 (); |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
139 |
update_term = (%g (a, b). |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
140 |
Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
141 |
(Code_Evaluation.Const (STR ''Fun.fun_upd'') |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
142 |
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
143 |
Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) g) (Code_Evaluation.term_of a)) b) |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
144 |
in |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
145 |
List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip domm (rng ())))" |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
146 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
147 |
definition |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
148 |
"check_all f = check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip (Enum.enum\<Colon>'a list) ys), mk_map_term (Enum.enum::'a list) yst (%_. Typerep.typerep (TYPE('b))))) (Code_Numeral.of_nat (length (Enum.enum :: 'a list)))" |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
149 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
150 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
151 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
152 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
153 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
154 |
instantiation bool :: check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
155 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
156 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
157 |
definition |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
158 |
"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
|
159 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
160 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
161 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
162 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
163 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
164 |
instantiation prod :: (check_all, check_all) check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
165 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
166 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
167 |
definition |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
168 |
"check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))))" |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
169 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
170 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
171 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
172 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
173 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
174 |
instantiation Enum.finite_1 :: check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
175 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
176 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
177 |
definition |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
178 |
"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
|
179 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
180 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
181 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
182 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
183 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
184 |
instantiation Enum.finite_2 :: check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
185 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
186 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
187 |
definition |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
188 |
"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
|
189 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
190 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
191 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
192 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
193 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
194 |
instantiation Enum.finite_3 :: check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
195 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
196 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
197 |
definition |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
198 |
"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
|
199 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
200 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
201 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
202 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
203 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
204 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
205 |
|
40620 | 206 |
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
|
207 |
|
40899
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
208 |
definition orelse :: "'a option => 'a option => 'a option" |
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
209 |
where |
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
210 |
[code_unfold]: "orelse x y = (case x of Some x' => Some x' | None => y)" |
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
211 |
|
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
212 |
|
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
213 |
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
|
214 |
where |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
215 |
[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
|
216 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
217 |
code_const catch_match |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
218 |
(SML "(_) handle Match => _") |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
219 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
220 |
use "Tools/smallvalue_generators.ML" |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
221 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
222 |
setup {* Smallvalue_Generators.setup *} |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
223 |
|
40915
a4c956d1f91f
declaring quickcheck testers as default after their setup
bulwahn
parents:
40914
diff
changeset
|
224 |
declare [[quickcheck_tester = exhaustive]] |
a4c956d1f91f
declaring quickcheck testers as default after their setup
bulwahn
parents:
40914
diff
changeset
|
225 |
|
40899
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
226 |
hide_fact orelse_def catch_match_def |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
227 |
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
|
228 |
|
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
229 |
end |