author | haftmann |
Mon, 02 Oct 2006 23:00:58 +0200 | |
changeset 20840 | 5e92606245b6 |
parent 20597 | 65fe827aa595 |
child 20934 | 2b872c161747 |
permissions | -rw-r--r-- |
17632 | 1 |
(* Title: HOL/Library/ExecutableSet.thy |
2 |
ID: $Id$ |
|
3 |
Author: Stefan Berghofer, TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* Implementation of finite sets by lists *} |
|
7 |
||
8 |
theory ExecutableSet |
|
9 |
imports Main |
|
10 |
begin |
|
11 |
||
20597 | 12 |
section {* Definitional equality rewrites *} |
13 |
||
14 |
instance set :: (eq) eq .. |
|
19791 | 15 |
|
16 |
lemma [code target: Set]: |
|
17 |
"(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)" |
|
17632 | 18 |
by blast |
19 |
||
20597 | 20 |
lemma [code func]: |
21 |
"OperationalEquality.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)" |
|
22 |
unfolding eq_def by blast |
|
23 |
||
17632 | 24 |
declare bex_triv_one_point1 [symmetric, standard, code] |
25 |
||
20597 | 26 |
|
19791 | 27 |
section {* HOL definitions *} |
28 |
||
29 |
subsection {* Basic definitions *} |
|
30 |
||
31 |
definition |
|
32 |
flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" |
|
33 |
"flip f a b = f b a" |
|
20597 | 34 |
member :: "'a list \<Rightarrow> 'a\<Colon>eq \<Rightarrow> bool" |
19791 | 35 |
"member xs x = (x \<in> set xs)" |
20597 | 36 |
insertl :: "'a\<Colon>eq\<Rightarrow> 'a list \<Rightarrow> 'a list" |
19791 | 37 |
"insertl x xs = (if member xs x then xs else x#xs)" |
38 |
||
39 |
lemma |
|
40 |
[code target: List]: "member [] y = False" |
|
41 |
and [code target: List]: "member (x#xs) y = (y = x \<or> member xs y)" |
|
42 |
unfolding member_def by (induct xs) simp_all |
|
43 |
||
44 |
consts |
|
45 |
drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
46 |
||
47 |
primrec |
|
48 |
"drop_first f [] = []" |
|
49 |
"drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)" |
|
50 |
declare drop_first.simps [code del] |
|
51 |
declare drop_first.simps [code target: List] |
|
52 |
||
53 |
declare remove1.simps [code del] |
|
20597 | 54 |
ML {* reset CodegenData.strict_functyp *} |
19791 | 55 |
lemma [code target: List]: |
56 |
"remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)" |
|
57 |
proof (cases "member xs x") |
|
58 |
case False thus ?thesis unfolding member_def by (induct xs) auto |
|
59 |
next |
|
60 |
case True |
|
61 |
have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all |
|
62 |
with True show ?thesis by simp |
|
63 |
qed |
|
20597 | 64 |
ML {* set CodegenData.strict_functyp *} |
19791 | 65 |
|
66 |
lemma member_nil [simp]: |
|
67 |
"member [] = (\<lambda>x. False)" |
|
68 |
proof |
|
69 |
fix x |
|
70 |
show "member [] x = False" unfolding member_def by simp |
|
71 |
qed |
|
72 |
||
73 |
lemma member_insertl [simp]: |
|
74 |
"x \<in> set (insertl x xs)" |
|
75 |
unfolding insertl_def member_def mem_iff by simp |
|
76 |
||
77 |
lemma insertl_member [simp]: |
|
78 |
fixes xs x |
|
79 |
assumes member: "member xs x" |
|
80 |
shows "insertl x xs = xs" |
|
81 |
using member unfolding insertl_def by simp |
|
82 |
||
83 |
lemma insertl_not_member [simp]: |
|
84 |
fixes xs x |
|
85 |
assumes member: "\<not> (member xs x)" |
|
86 |
shows "insertl x xs = x # xs" |
|
87 |
using member unfolding insertl_def by simp |
|
88 |
||
89 |
lemma foldr_remove1_empty [simp]: |
|
90 |
"foldr remove1 xs [] = []" |
|
91 |
by (induct xs) simp_all |
|
92 |
||
93 |
||
94 |
subsection {* Derived definitions *} |
|
95 |
||
20597 | 96 |
function unionl :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
97 |
where |
19791 | 98 |
"unionl [] ys = ys" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
99 |
| "unionl xs ys = foldr insertl xs ys" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
100 |
by pat_completeness auto |
19791 | 101 |
termination unionl by (auto_term "{}") |
102 |
lemmas unionl_def = unionl.simps(2) |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
103 |
declare unionl.simps[code] |
19791 | 104 |
|
20597 | 105 |
function intersect :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
106 |
where |
19791 | 107 |
"intersect [] ys = []" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
108 |
| "intersect xs [] = []" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
109 |
| "intersect xs ys = filter (member xs) ys" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
110 |
by pat_completeness auto |
19791 | 111 |
termination intersect by (auto_term "{}") |
112 |
lemmas intersect_def = intersect.simps(3) |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
113 |
declare intersect.simps[code] |
19791 | 114 |
|
20597 | 115 |
function subtract :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
116 |
where |
19791 | 117 |
"subtract [] ys = ys" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
118 |
| "subtract xs [] = []" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
119 |
| "subtract xs ys = foldr remove1 xs ys" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
120 |
by pat_completeness auto |
19791 | 121 |
termination subtract by (auto_term "{}") |
122 |
lemmas subtract_def = subtract.simps(3) |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
123 |
declare subtract.simps[code] |
19791 | 124 |
|
20597 | 125 |
function map_distinct :: "('a \<Rightarrow> 'b\<Colon>eq) \<Rightarrow> 'a list \<Rightarrow> 'b list" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
126 |
where |
19791 | 127 |
"map_distinct f [] = []" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
128 |
| "map_distinct f xs = foldr (insertl o f) xs []" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
129 |
by pat_completeness auto |
19791 | 130 |
termination map_distinct by (auto_term "{}") |
131 |
lemmas map_distinct_def = map_distinct.simps(2) |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
132 |
declare map_distinct.simps[code] |
19791 | 133 |
|
20597 | 134 |
function unions :: "'a\<Colon>eq list list \<Rightarrow> 'a list" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
135 |
where |
19791 | 136 |
"unions [] = []" |
137 |
"unions xs = foldr unionl xs []" |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
138 |
by pat_completeness auto |
19791 | 139 |
termination unions by (auto_term "{}") |
140 |
lemmas unions_def = unions.simps(2) |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
141 |
declare unions.simps[code] |
19791 | 142 |
|
20597 | 143 |
consts intersects :: "'a\<Colon>eq list list \<Rightarrow> 'a list" |
19791 | 144 |
primrec |
145 |
"intersects (x#xs) = foldr intersect xs x" |
|
146 |
||
147 |
definition |
|
20597 | 148 |
map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b\<Colon>eq list) \<Rightarrow> 'b list" |
19791 | 149 |
"map_union xs f = unions (map f xs)" |
20597 | 150 |
map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b\<Colon>eq list) \<Rightarrow> 'b list" |
19791 | 151 |
"map_inter xs f = intersects (map f xs)" |
152 |
||
153 |
||
154 |
section {* Isomorphism proofs *} |
|
155 |
||
156 |
lemma iso_member: |
|
157 |
"member xs x = (x \<in> set xs)" |
|
158 |
unfolding member_def mem_iff .. |
|
159 |
||
160 |
lemma iso_insert: |
|
161 |
"set (insertl x xs) = insert x (set xs)" |
|
162 |
unfolding insertl_def iso_member by (simp add: Set.insert_absorb) |
|
163 |
||
164 |
lemma iso_remove1: |
|
165 |
assumes distnct: "distinct xs" |
|
166 |
shows "set (remove1 x xs) = set xs - {x}" |
|
167 |
using distnct set_remove1_eq by auto |
|
168 |
||
169 |
lemma iso_union: |
|
170 |
"set (unionl xs ys) = set xs \<union> set ys" |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
171 |
unfolding unionl_def |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20503
diff
changeset
|
172 |
by (induct xs arbitrary: ys) (simp_all add: iso_insert) |
19791 | 173 |
|
174 |
lemma iso_intersect: |
|
175 |
"set (intersect xs ys) = set xs \<inter> set ys" |
|
176 |
unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto |
|
177 |
||
178 |
lemma iso_subtract: |
|
179 |
fixes ys |
|
180 |
assumes distnct: "distinct ys" |
|
181 |
shows "set (subtract xs ys) = set ys - set xs" |
|
182 |
and "distinct (subtract xs ys)" |
|
20503 | 183 |
unfolding subtract_def using distnct by (induct xs arbitrary: ys) (simp_all, auto) |
19791 | 184 |
|
185 |
corollary iso_subtract': |
|
186 |
fixes xs ys |
|
187 |
assumes distnct: "distinct xs" |
|
188 |
shows "set ((flip subtract) xs ys) = set xs - set ys" |
|
189 |
proof - |
|
190 |
from distnct iso_subtract have "set (subtract ys xs) = set xs - set ys" by auto |
|
191 |
thus ?thesis unfolding flip_def by auto |
|
192 |
qed |
|
193 |
||
194 |
lemma iso_map_distinct: |
|
195 |
"set (map_distinct f xs) = image f (set xs)" |
|
196 |
unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert) |
|
197 |
||
198 |
lemma iso_unions: |
|
199 |
"set (unions xss) = \<Union> set (map set xss)" |
|
200 |
unfolding unions_def proof (induct xss) |
|
201 |
case Nil show ?case by simp |
|
202 |
next |
|
203 |
case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert) |
|
204 |
qed |
|
205 |
||
206 |
lemma iso_intersects: |
|
207 |
"set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))" |
|
208 |
by (induct xss) (simp_all add: Int_def iso_member, auto) |
|
209 |
||
210 |
lemma iso_UNION: |
|
211 |
"set (map_union xs f) = UNION (set xs) (set o f)" |
|
212 |
unfolding map_union_def iso_unions by simp |
|
213 |
||
214 |
lemma iso_INTER: |
|
215 |
"set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)" |
|
216 |
unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto) |
|
217 |
||
218 |
definition |
|
219 |
Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
220 |
"Blall = flip list_all" |
|
221 |
Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
222 |
"Blex = flip list_ex" |
|
223 |
||
224 |
lemma iso_Ball: |
|
225 |
"Blall xs f = Ball (set xs) f" |
|
226 |
unfolding Blall_def flip_def by (induct xs) simp_all |
|
227 |
||
228 |
lemma iso_Bex: |
|
229 |
"Blex xs f = Bex (set xs) f" |
|
230 |
unfolding Blex_def flip_def by (induct xs) simp_all |
|
231 |
||
232 |
||
233 |
section {* code generator setup *} |
|
234 |
||
235 |
subsection {* type serializations *} |
|
236 |
||
17632 | 237 |
types_code |
238 |
set ("_ list") |
|
239 |
attach (term_of) {* |
|
240 |
fun term_of_set f T [] = Const ("{}", Type ("set", [T])) |
|
241 |
| term_of_set f T (x :: xs) = Const ("insert", |
|
242 |
T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs; |
|
243 |
*} |
|
244 |
attach (test) {* |
|
245 |
fun gen_set' aG i j = frequency |
|
246 |
[(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] () |
|
247 |
and gen_set aG i = gen_set' aG i i; |
|
248 |
*} |
|
249 |
||
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
250 |
code_type set |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
251 |
(SML "_ list") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
252 |
(Haskell target_atom "[_]") |
18702 | 253 |
|
19791 | 254 |
|
255 |
subsection {* const serializations *} |
|
18702 | 256 |
|
17632 | 257 |
consts_code |
258 |
"{}" ("[]") |
|
19791 | 259 |
"insert" ("{*insertl*}") |
260 |
"op Un" ("{*unionl*}") |
|
261 |
"op Int" ("{*intersect*}") |
|
262 |
"HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
|
263 |
("{*flip subtract*}") |
|
264 |
"image" ("{*map_distinct*}") |
|
265 |
"Union" ("{*unions*}") |
|
266 |
"Inter" ("{*intersects*}") |
|
267 |
"UNION" ("{*map_union*}") |
|
268 |
"INTER" ("{*map_inter*}") |
|
269 |
"Ball" ("{*Blall*}") |
|
270 |
"Bex" ("{*Blex*}") |
|
17632 | 271 |
|
20380 | 272 |
code_constname |
19791 | 273 |
"ExecutableSet.member" "List.member" |
274 |
"ExecutableSet.insertl" "List.insertl" |
|
275 |
"ExecutableSet.drop_first" "List.drop_first" |
|
18963 | 276 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
277 |
code_const "{}" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
278 |
(SML target_atom "[]") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
279 |
(Haskell target_atom "[]") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
280 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
281 |
code_const insert |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
282 |
(SML "{*insertl*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
283 |
(Haskell "{*insertl*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
284 |
|
20840 | 285 |
code_const insert |
286 |
(SML "{*insertl*}") |
|
287 |
(Haskell "{*insertl*}") |
|
288 |
||
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
289 |
code_const "op \<union>" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
290 |
(SML "{*unionl*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
291 |
(Haskell "{*unionl*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
292 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
293 |
code_const "op \<inter>" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
294 |
(SML "{*intersect*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
295 |
(Haskell "{*intersect*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
296 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
297 |
code_const "op - :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
298 |
(SML "{*flip subtract*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
299 |
(Haskell "{*flip subtract*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
300 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
301 |
code_const image |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
302 |
(SML "{*map_distinct*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
303 |
(Haskell "{*map_distinct*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
304 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
305 |
code_const "Union" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
306 |
(SML "{*unions*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
307 |
(Haskell "{*unions*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
308 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
309 |
code_const "Inter" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
310 |
(SML "{*intersects*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
311 |
(Haskell "{*intersects*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
312 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
313 |
code_const UNION |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
314 |
(SML "{*map_union*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
315 |
(Haskell "{*map_union*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
316 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
317 |
code_const INTER |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
318 |
(SML "{*map_inter*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
319 |
(Haskell "{*map_inter*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
320 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
321 |
code_const Ball |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
322 |
(SML "{*Blall*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
323 |
(Haskell "{*Blall*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
324 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
325 |
code_const Bex |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
326 |
(SML "{*Blex*}") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20380
diff
changeset
|
327 |
(Haskell "{*Blex*}") |
18702 | 328 |
|
20597 | 329 |
code_gen (SML -) (SML _) |
330 |
||
17632 | 331 |
end |