author | wenzelm |
Fri, 17 Nov 2006 02:20:03 +0100 | |
changeset 21404 | eb85850d3eb7 |
parent 21319 | cf814e36f788 |
child 21460 | cda5cd8bfd16 |
permissions | -rw-r--r-- |
20436 | 1 |
(* ID: $Id$ |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Collection classes as examples for code generation *} |
|
6 |
||
7 |
theory CodeCollections |
|
20597 | 8 |
imports Main |
20436 | 9 |
begin |
10 |
||
11 |
section {* Collection classes as examples for code generation *} |
|
12 |
||
13 |
class ordered = eq + |
|
14 |
constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
15 |
fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^loc><<=" 65) |
|
16 |
fixes lt :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^loc><<" 65) |
|
17 |
assumes order_refl: "x \<^loc><<= x" |
|
18 |
assumes order_trans: "x \<^loc><<= y ==> y \<^loc><<= z ==> x \<^loc><<= z" |
|
19 |
assumes order_antisym: "x \<^loc><<= y ==> y \<^loc><<= x ==> x = y" |
|
20 |
||
21 |
declare order_refl [simp, intro] |
|
22 |
||
23 |
defs |
|
24 |
lt_def: "x << y == (x <<= y \<and> x \<noteq> y)" |
|
25 |
||
26 |
lemma lt_intro [intro]: |
|
27 |
assumes "x <<= y" and "x \<noteq> y" |
|
28 |
shows "x << y" |
|
29 |
unfolding lt_def .. |
|
30 |
||
31 |
lemma lt_elim [elim]: |
|
32 |
assumes "(x::'a::ordered) << y" |
|
33 |
and Q: "!!x y::'a::ordered. x <<= y \<Longrightarrow> x \<noteq> y \<Longrightarrow> P" |
|
34 |
shows P |
|
35 |
proof - |
|
36 |
from prems have R1: "x <<= y" and R2: "x \<noteq> y" by (simp_all add: lt_def) |
|
37 |
show P by (rule Q [OF R1 R2]) |
|
38 |
qed |
|
39 |
||
40 |
lemma lt_trans: |
|
41 |
assumes "x << y" and "y << z" |
|
42 |
shows "x << z" |
|
43 |
proof |
|
44 |
from prems lt_def have prems': "x <<= y" "y <<= z" by auto |
|
45 |
show "x <<= z" by (rule order_trans, auto intro: prems') |
|
46 |
next |
|
47 |
show "x \<noteq> z" |
|
48 |
proof |
|
49 |
from prems lt_def have prems': "x <<= y" "y <<= z" "x \<noteq> y" by auto |
|
50 |
assume "x = z" |
|
51 |
with prems' have "x <<= y" and "y <<= x" by auto |
|
52 |
with order_antisym have "x = y" . |
|
53 |
with prems' show False by auto |
|
54 |
qed |
|
55 |
qed |
|
56 |
||
57 |
definition (in ordered) |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
58 |
min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where |
20436 | 59 |
"min x y = (if x \<^loc><<= y then x else y)" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
60 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
61 |
definition (in ordered) |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
62 |
max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where |
20436 | 63 |
"max x y = (if x \<^loc><<= y then y else x)" |
64 |
||
65 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
66 |
min :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a" where |
20436 | 67 |
"min x y = (if x <<= y then x else y)" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
68 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
69 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
70 |
max :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a" where |
20436 | 71 |
"max x y = (if x <<= y then y else x)" |
72 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
73 |
fun abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
74 |
where |
20436 | 75 |
"abs_sorted cmp [] = True" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
76 |
| "abs_sorted cmp [x] = True" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
77 |
| "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
78 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
79 |
thm abs_sorted.simps |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
80 |
|
20436 | 81 |
abbreviation (in ordered) |
82 |
"sorted \<equiv> abs_sorted le" |
|
83 |
||
84 |
abbreviation |
|
85 |
"sorted \<equiv> abs_sorted le" |
|
86 |
||
87 |
lemma (in ordered) sorted_weakening: |
|
88 |
assumes "sorted (x # xs)" |
|
89 |
shows "sorted xs" |
|
90 |
using prems proof (induct xs) |
|
91 |
case Nil show ?case by simp |
|
92 |
next |
|
93 |
case (Cons x' xs) |
|
94 |
from this(5) have "sorted (x # x' # xs)" . |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
95 |
then show "sorted (x' # xs)" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
96 |
by auto |
20436 | 97 |
qed |
98 |
||
99 |
instance bool :: ordered |
|
100 |
"p <<= q == (p --> q)" |
|
101 |
by default (unfold ordered_bool_def, blast+) |
|
102 |
||
103 |
instance nat :: ordered |
|
104 |
"m <<= n == m <= n" |
|
105 |
by default (simp_all add: ordered_nat_def) |
|
106 |
||
107 |
instance int :: ordered |
|
108 |
"k <<= l == k <= l" |
|
109 |
by default (simp_all add: ordered_int_def) |
|
110 |
||
111 |
instance unit :: ordered |
|
112 |
"u <<= v == True" |
|
113 |
by default (simp_all add: ordered_unit_def) |
|
114 |
||
115 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
116 |
fun le_option' :: "'a::ordered option \<Rightarrow> 'a option \<Rightarrow> bool" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
117 |
where |
20436 | 118 |
"le_option' None y = True" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
119 |
| "le_option' (Some x) None = False" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
120 |
| "le_option' (Some x) (Some y) = x <<= y" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
121 |
|
20597 | 122 |
instance option :: (ordered) ordered |
20436 | 123 |
"x <<= y == le_option' x y" |
124 |
proof (default, unfold ordered_option_def) |
|
125 |
fix x |
|
126 |
show "le_option' x x" by (cases x) simp_all |
|
127 |
next |
|
128 |
fix x y z |
|
129 |
assume "le_option' x y" "le_option' y z" |
|
130 |
then show "le_option' x z" |
|
131 |
by (cases x, simp_all, cases y, simp_all, cases z, simp_all) |
|
132 |
(erule order_trans, assumption) |
|
133 |
next |
|
134 |
fix x y |
|
135 |
assume "le_option' x y" "le_option' y x" |
|
136 |
then show "x = y" |
|
137 |
by (cases x, simp_all, cases y, simp_all, cases y, simp_all) |
|
138 |
(erule order_antisym, assumption) |
|
139 |
qed |
|
140 |
||
141 |
lemma [simp, code]: |
|
142 |
"None <<= y = True" |
|
143 |
"Some x <<= None = False" |
|
144 |
"Some v <<= Some w = v <<= w" |
|
145 |
unfolding ordered_option_def le_option'.simps by rule+ |
|
146 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
147 |
fun le_pair' :: "'a::ordered \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
148 |
where |
20436 | 149 |
"le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)" |
150 |
||
20597 | 151 |
instance * :: (ordered, ordered) ordered |
20436 | 152 |
"x <<= y == le_pair' x y" |
153 |
apply (default, unfold "ordered_*_def", unfold split_paired_all) |
|
154 |
apply simp_all |
|
155 |
apply (auto intro: lt_trans order_trans)[1] |
|
156 |
unfolding lt_def apply (auto intro: order_antisym)[1] |
|
157 |
done |
|
158 |
||
159 |
lemma [simp, code]: |
|
160 |
"(x1, y1) <<= (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)" |
|
161 |
unfolding "ordered_*_def" le_pair'.simps .. |
|
162 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
163 |
(* |
20436 | 164 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
165 |
fun le_list' :: "'a::ordered list \<Rightarrow> 'a list \<Rightarrow> bool" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
166 |
where |
20436 | 167 |
"le_list' [] ys = True" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
168 |
| "le_list' (x#xs) [] = False" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
169 |
| "le_list' (x#xs) (y#ys) = (x << y \<or> x = y \<and> le_list' xs ys)" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
170 |
|
20436 | 171 |
instance (ordered) list :: ordered |
172 |
"xs <<= ys == le_list' xs ys" |
|
173 |
proof (default, unfold "ordered_list_def") |
|
174 |
fix xs |
|
175 |
show "le_list' xs xs" by (induct xs) simp_all |
|
176 |
next |
|
177 |
fix xs ys zs |
|
178 |
assume "le_list' xs ys" and "le_list' ys zs" |
|
179 |
then show "le_list' xs zs" |
|
180 |
apply (induct xs zs rule: le_list'.induct) |
|
181 |
apply simp_all |
|
182 |
apply (cases ys) apply simp_all |
|
183 |
||
184 |
apply (induct ys) apply simp_all |
|
185 |
apply (induct ys) |
|
186 |
apply simp_all |
|
187 |
apply (induct zs) |
|
188 |
apply simp_all |
|
189 |
next |
|
190 |
fix xs ys |
|
191 |
assume "le_list' xs ys" and "le_list' ys xs" |
|
192 |
show "xs = ys" sorry |
|
193 |
qed |
|
194 |
||
195 |
lemma [simp, code]: |
|
196 |
"[] <<= ys = True" |
|
197 |
"(x#xs) <<= [] = False" |
|
198 |
"(x#xs) <<= (y#ys) = (x << y \<or> x = y \<and> xs <<= ys)" |
|
199 |
unfolding "ordered_list_def" le_list'.simps by rule+*) |
|
200 |
||
201 |
class infimum = ordered + |
|
202 |
fixes inf |
|
203 |
assumes inf: "inf \<^loc><<= x" |
|
204 |
||
205 |
lemma (in infimum) |
|
206 |
assumes prem: "a \<^loc><<= inf" |
|
207 |
shows no_smaller: "a = inf" |
|
208 |
using prem inf by (rule order_antisym) |
|
209 |
||
210 |
||
211 |
ML {* set quick_and_dirty *} |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
212 |
function abs_max_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
213 |
where |
20436 | 214 |
"abs_max_of cmp inff [] = inff" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
215 |
| "abs_max_of cmp inff [x] = x" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
216 |
| "abs_max_of cmp inff (x#xs) = |
20436 | 217 |
ordered.max cmp x (abs_max_of cmp inff xs)" |
218 |
apply pat_completeness sorry |
|
219 |
||
220 |
abbreviation (in infimum) |
|
221 |
"max_of xs \<equiv> abs_max_of le inf" |
|
222 |
||
223 |
abbreviation |
|
224 |
"max_of xs \<equiv> abs_max_of le inf" |
|
225 |
||
226 |
instance bool :: infimum |
|
227 |
"inf == False" |
|
228 |
by default (simp add: infimum_bool_def) |
|
229 |
||
230 |
instance nat :: infimum |
|
231 |
"inf == 0" |
|
232 |
by default (simp add: infimum_nat_def) |
|
233 |
||
234 |
instance unit :: infimum |
|
235 |
"inf == ()" |
|
236 |
by default (simp add: infimum_unit_def) |
|
237 |
||
20597 | 238 |
instance option :: (ordered) infimum |
20436 | 239 |
"inf == None" |
240 |
by default (simp add: infimum_option_def) |
|
241 |
||
20597 | 242 |
instance * :: (infimum, infimum) infimum |
20436 | 243 |
"inf == (inf, inf)" |
244 |
by default (unfold "infimum_*_def", unfold split_paired_all, auto intro: inf) |
|
245 |
||
246 |
class enum = ordered + |
|
247 |
fixes enum :: "'a list" |
|
248 |
assumes member_enum: "x \<in> set enum" |
|
249 |
and ordered_enum: "abs_sorted le enum" |
|
250 |
||
251 |
(* |
|
252 |
FIXME: |
|
253 |
- abbreviations must be propagated before locale introduction |
|
254 |
- then also now shadowing may occur |
|
255 |
*) |
|
256 |
(*abbreviation (in enum) |
|
257 |
"local.sorted \<equiv> abs_sorted le"*) |
|
258 |
||
259 |
instance bool :: enum |
|
260 |
(* FIXME: better name handling of definitions *) |
|
261 |
"_1": "enum == [False, True]" |
|
262 |
by default (simp_all add: enum_bool_def) |
|
263 |
||
264 |
instance unit :: enum |
|
265 |
"_2": "enum == [()]" |
|
266 |
by default (simp_all add: enum_unit_def) |
|
267 |
||
268 |
(*consts |
|
269 |
product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list" |
|
270 |
||
271 |
primrec |
|
272 |
"product [] ys = []" |
|
273 |
"product (x#xs) ys = map (Pair x) ys @ product xs ys" |
|
274 |
||
275 |
lemma product_all: |
|
276 |
assumes "x \<in> set xs" "y \<in> set ys" |
|
277 |
shows "(x, y) \<in> set (product xs ys)" |
|
278 |
using prems proof (induct xs) |
|
279 |
case Nil |
|
280 |
then have False by auto |
|
281 |
then show ?case .. |
|
282 |
next |
|
283 |
case (Cons z xs) |
|
284 |
then show ?case |
|
285 |
proof (cases "x = z") |
|
286 |
case True |
|
287 |
with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp |
|
288 |
with True show ?thesis by simp |
|
289 |
next |
|
290 |
case False |
|
291 |
with Cons have "x \<in> set xs" by auto |
|
292 |
with Cons have "(x, y) \<in> set (product xs ys)" by auto |
|
293 |
then show "(x, y) \<in> set (product (z#xs) ys)" by auto |
|
294 |
qed |
|
295 |
qed |
|
296 |
||
297 |
lemma product_sorted: |
|
298 |
assumes "sorted xs" "sorted ys" |
|
299 |
shows "sorted (product xs ys)" |
|
300 |
using prems proof (induct xs) |
|
301 |
case Nil |
|
302 |
then show ?case by simp |
|
303 |
next |
|
304 |
case (Cons x xs) |
|
305 |
from Cons ordered.sorted_weakening have "sorted xs" by auto |
|
306 |
with Cons have "sorted (product xs ys)" by auto |
|
307 |
then show ?case apply simp |
|
308 |
proof - |
|
309 |
assume |
|
310 |
apply simp |
|
311 |
||
312 |
proof (cases "x = z") |
|
313 |
case True |
|
314 |
with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp |
|
315 |
with True show ?thesis by simp |
|
316 |
next |
|
317 |
case False |
|
318 |
with Cons have "x \<in> set xs" by auto |
|
319 |
with Cons have "(x, y) \<in> set (product xs ys)" by auto |
|
320 |
then show "(x, y) \<in> set (product (z#xs) ys)" by auto |
|
321 |
qed |
|
322 |
qed |
|
323 |
||
324 |
instance (enum, enum) * :: enum |
|
325 |
"_3": "enum == product enum enum" |
|
326 |
apply default |
|
327 |
apply (simp_all add: "enum_*_def") |
|
328 |
apply (unfold split_paired_all) |
|
329 |
apply (rule product_all) |
|
330 |
apply (rule member_enum)+ |
|
331 |
sorry*) |
|
332 |
||
20597 | 333 |
instance option :: (enum) enum |
20436 | 334 |
"_4": "enum == None # map Some enum" |
335 |
proof (default, unfold enum_option_def) |
|
336 |
fix x :: "'a::enum option" |
|
337 |
show "x \<in> set (None # map Some enum)" |
|
338 |
proof (cases x) |
|
339 |
case None then show ?thesis by auto |
|
340 |
next |
|
341 |
case (Some x) then show ?thesis by (auto intro: member_enum) |
|
342 |
qed |
|
343 |
next |
|
344 |
show "sorted (None # map Some (enum :: ('a::enum) list))" |
|
345 |
sorry |
|
346 |
(*proof (cases "enum :: 'a list") |
|
347 |
case Nil then show ?thesis by simp |
|
348 |
next |
|
349 |
case (Cons x xs) |
|
350 |
then have "sorted (None # map Some (x # xs))" sorry |
|
351 |
then show ?thesis apply simp |
|
352 |
apply simp_all |
|
353 |
apply auto*) |
|
354 |
qed |
|
355 |
||
356 |
ML {* reset quick_and_dirty *} |
|
357 |
||
358 |
consts |
|
359 |
get_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option" |
|
360 |
||
361 |
primrec |
|
362 |
"get_first p [] = None" |
|
363 |
"get_first p (x#xs) = (if p x then Some x else get_first p xs)" |
|
364 |
||
365 |
consts |
|
366 |
get_index :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat option" |
|
367 |
||
368 |
primrec |
|
369 |
"get_index p n [] = None" |
|
370 |
"get_index p n (x#xs) = (if p x then Some n else get_index p (Suc n) xs)" |
|
371 |
||
372 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
373 |
between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option" where |
20436 | 374 |
"between x y = get_first (\<lambda>z. x << z & z << y) enum" |
375 |
||
376 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
377 |
index :: "'a::enum \<Rightarrow> nat" where |
20436 | 378 |
"index x = the (get_index (\<lambda>y. y = x) 0 enum)" |
379 |
||
380 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
381 |
add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a" where |
20436 | 382 |
"add x y = |
383 |
(let |
|
384 |
enm = enum |
|
385 |
in enm ! ((index x + index y) mod length enm))" |
|
386 |
||
387 |
consts |
|
388 |
sum :: "'a::{enum, infimum} list \<Rightarrow> 'a" |
|
389 |
||
390 |
primrec |
|
391 |
"sum [] = inf" |
|
392 |
"sum (x#xs) = add x (sum xs)" |
|
393 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
394 |
definition "test1 = sum [None, Some True, None, Some False]" |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21319
diff
changeset
|
395 |
definition "test2 = (inf :: nat \<times> unit)" |
20436 | 396 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
397 |
code_gen "op <<=" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
398 |
code_gen "op <<" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
399 |
code_gen inf |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
400 |
code_gen between |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
401 |
code_gen index |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
402 |
code_gen test1 |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
403 |
code_gen test2 |
20436 | 404 |
|
21125 | 405 |
code_gen (SML *) |
21080 | 406 |
code_gen (Haskell -) |
20436 | 407 |
|
408 |
end |