25 fun gen_set' aG i j = frequency |
25 fun gen_set' aG i j = frequency |
26 [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] () |
26 [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] () |
27 and gen_set aG i = gen_set' aG i i; |
27 and gen_set aG i = gen_set' aG i i; |
28 *} |
28 *} |
29 |
29 |
|
30 code_syntax_tyco set |
|
31 ml ("_ list") |
|
32 haskell (atom "[_]") |
|
33 |
|
34 code_syntax_const "{}" |
|
35 ml (atom "[]") |
|
36 haskell (atom "[]") |
|
37 |
30 consts_code |
38 consts_code |
31 "{}" ("[]") |
39 "{}" ("[]") |
32 "insert" ("(_ ins _)") |
40 "insert" ("(_ ins _)") |
33 "op Un" ("(_ union _)") |
41 "op Un" ("(_ union _)") |
34 "op Int" ("(_ inter _)") |
42 "op Int" ("(_ inter _)") |
52 "Ball" ("\<module>Ball") |
60 "Ball" ("\<module>Ball") |
53 attach {* |
61 attach {* |
54 fun Ball S P = Library.forall P S; |
62 fun Ball S P = Library.forall P S; |
55 *} |
63 *} |
56 |
64 |
|
65 code_generate "op mem" |
|
66 |
|
67 code_primconst "insert" |
|
68 depending_on ("List.const.member") |
|
69 ml {* |
|
70 fun insert x xs = |
|
71 if List.member x xs then xs |
|
72 else x::xs; |
|
73 *} |
|
74 haskell {* |
|
75 insert x xs = |
|
76 if elem x xs then xs else x:xs |
|
77 *} |
|
78 |
|
79 code_primconst "op Un" |
|
80 depending_on ("List.const.insert") |
|
81 ml {* |
|
82 fun union xs [] = xs |
|
83 | union [] ys = ys |
|
84 | union (x::xs) ys = union xs (insert x ys); |
|
85 *} |
|
86 haskell {* |
|
87 union xs [] = xs |
|
88 union [] ys = ys |
|
89 union (x:xs) ys = union xs (insert x ys) |
|
90 *} |
|
91 |
|
92 code_primconst "op Int" |
|
93 depending_on ("List.const.member") |
|
94 ml {* |
|
95 fun inter [] ys = [] |
|
96 | inter (x::xs) ys = |
|
97 if List.member x ys |
|
98 then x :: inter xs ys |
|
99 else inter xs ys; |
|
100 *} |
|
101 haskell {* |
|
102 inter [] ys = [] |
|
103 inter (x:xs) ys = |
|
104 if elem x ys |
|
105 then x : inter xs ys |
|
106 else inter xs ys |
|
107 *} |
|
108 |
|
109 code_primconst "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
|
110 ml {* |
|
111 fun op_minus ys [] = ys |
|
112 | op_minus ys (x::xs) = |
|
113 let |
|
114 fun minus [] x = [] |
|
115 | minus (y::ys) x = if x = y then ys else y :: minus ys x |
|
116 in |
|
117 op_minus (minus ys x) xs |
|
118 end; |
|
119 *} |
|
120 haskell {* |
|
121 op_minus ys [] = ys |
|
122 op_minus ys (x:xs) = op_minus (minus ys x) xs where |
|
123 minus [] x = [] |
|
124 minus (y:ys) x = if x = y then ys else y : minus ys x |
|
125 *} |
|
126 |
|
127 code_primconst "image" |
|
128 depending_on ("List.const.insert") |
|
129 ml {* |
|
130 fun image f = |
|
131 let |
|
132 fun img xs [] = xs |
|
133 | img xs (y::ys) = img (insert (f y) xs) ys; |
|
134 in img [] end;; |
|
135 *} |
|
136 haskell {* |
|
137 image f = img [] where |
|
138 img xs [] = xs |
|
139 img xs (y:ys) = img (insert (f y) xs) ys; |
|
140 *} |
|
141 |
|
142 code_primconst "UNION" |
|
143 depending_on ("List.const.union") |
|
144 ml {* |
|
145 fun UNION [] f = [] |
|
146 | UNION (x::xs) f = union (f x) (UNION xs); |
|
147 *} |
|
148 haskell {* |
|
149 UNION [] f = [] |
|
150 UNION (x:xs) f = union (f x) (UNION xs); |
|
151 *} |
|
152 |
|
153 code_primconst "INTER" |
|
154 depending_on ("List.const.inter") |
|
155 ml {* |
|
156 fun INTER [] f = [] |
|
157 | INTER (x::xs) f = inter (f x) (INTER xs); |
|
158 *} |
|
159 haskell {* |
|
160 INTER [] f = [] |
|
161 INTER (x:xs) f = inter (f x) (INTER xs); |
|
162 *} |
|
163 |
|
164 code_primconst "Ball" |
|
165 ml {* |
|
166 fun Ball [] f = true |
|
167 | Ball (x::xs) f = f x andalso Ball f xs; |
|
168 *} |
|
169 haskell {* |
|
170 Ball = all . flip |
|
171 *} |
|
172 |
|
173 code_primconst "Bex" |
|
174 ml {* |
|
175 fun Bex [] f = false |
|
176 | Bex (x::xs) f = f x orelse Bex f xs; |
|
177 *} |
|
178 haskell {* |
|
179 Ball = any . flip |
|
180 *} |
|
181 |
57 end |
182 end |