1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
|
(** Java driver *)
printer "java"
module mach.java.lang.Integer
syntax type integer "int"
syntax literal integer "%c"
syntax val min_integer "Integer.MIN_VALUE" prec 0
syntax val max_integer "Integer.MAX_VALUE" prec 0
syntax val (+) "%1 + %2" prec 4 4 3
syntax val (-) "%1 - %2" prec 4 4 3
syntax val (-_) "-%1" prec 2 1
syntax val ( * ) "%1 * %2" prec 3 3 2
syntax val (/) "%1 / %2" prec 3 3 2
syntax val (%) "%1 % %2" prec 3 3 2
syntax val (=) "%1 == %2" prec 7 7 6
syntax val (<=) "%1 <= %2" prec 6 6 5
syntax val (<) "%1 < %2" prec 6 6 5
syntax val (>=) "%1 >= %2" prec 6 6 5
syntax val (>) "%1 > %2" prec 6 6 5
syntax val to_int "(%1).intValue()"
remove module
end
module mach.java.lang.Long
syntax type long "long"
syntax literal long "%c"
syntax val min_long "Long.MIN_VALUE" prec 0
syntax val max_long "Long.MAX_VALUE" prec 0
syntax val (+) "%1 + %2" prec 4 4 3
syntax val (-) "%1 - %2" prec 4 4 3
syntax val (-_) "-%1" prec 2 1
syntax val ( * ) "%1 * %2" prec 3 3 2
syntax val (/) "%1 / %2" prec 3 3 2
syntax val (%) "%1 % %2" prec 3 3 2
syntax val (=) "%1 == %2" prec 7 7 6
syntax val (<=) "%1 <= %2" prec 6 6 5
syntax val (<) "%1 < %2" prec 6 6 5
syntax val (>=) "%1 >= %2" prec 6 6 5
syntax val (>) "%1 > %2" prec 6 6 5
syntax val of_integer "Long.valueOf(%1)" prec 15 15
syntax val int_value "Integer.valueOf((int)%1)" prec 15 15
remove module
end
module mach.java.lang.Short
syntax type short "short"
syntax literal short "%c"
syntax val min_short "Short.MIN_VALUE" prec 0
syntax val max_short "Short.MAX_VALUE" prec 0
syntax val (+) "%1 + %2" prec 4 4 3
syntax val (-) "%1 - %2" prec 4 4 3
syntax val (-_) "-%1" prec 2 1
syntax val ( * ) "%1 * %2" prec 3 3 2
syntax val (/) "%1 / %2" prec 3 3 2
syntax val (%) "%1 % %2" prec 3 3 2
syntax val (=) "%1 == %2" prec 7 7 6
syntax val (<=) "%1 <= %2" prec 6 6 5
syntax val (<) "%1 < %2" prec 6 6 5
syntax val (>=) "%1 >= %2" prec 6 6 5
syntax val (>) "%1 > %2" prec 6 6 5
remove module
end
module string.String
syntax type string "String"
syntax literal string "%c"
end
module mach.java.lang.String
syntax val equals "%1.equals (%2)" prec 15 14 14
syntax val concat "%1.concat (%2)" prec 15 14 14
syntax val of_integer "String.valueOf(%1)" prec 15
syntax val of_long "String.valueOf(%1)" prec 15
syntax val format_1 "String.format(%1, %2)" prec 15 14
syntax val format_2 "String.format(%1, %2, %3)" prec 15 14 14
syntax val format_3 "String.format(%1, %2, %3, %4)" prec 15 14 14 14
syntax val format_4 "String.format(%1, %2, %3, %4, %5)" prec 15 14 14 14 14
remove module
end
module mach.java.lang.System
syntax val out "System.out" prec 0
syntax val err "System.err" prec 0
remove module
end
module mach.java.io.PrintStream
prelude export "import java.io.PrintStream;"
syntax type print_stream "PrintStream"
syntax val print "%1.print(%2)" prec 15 14
syntax val println "%1.println(%2)" prec 15 14
remove module
end
module mach.java.util.NoSuchElementException
prelude export "import java.util.NoSuchElementException;"
syntax exception E "NoSuchElementException"
remove module
end
module mach.java.lang.IndexOutOfBoundsException
syntax exception E "IndexOutOfBoundsException"
remove module
end
module mach.java.lang.IllegalArgumentException
syntax exception E "IllegalArgumentException"
remove module
end
module mach.java.lang.ArithmeticException
syntax exception E "ArithmeticException"
remove module
end
module mach.java.util.Set
prelude export "import java.util.Set;"
prelude export "import java.util.HashSet;"
syntax type set "Set<%1>"
syntax val empty "new HashSet<> ()" prec 15
syntax val size "%1.size ()" prec 15
syntax val contains "%1.contains (%2)" prec 15
syntax val equals "%1.equals (%2)" prec 15
syntax val add "%1.add (%2)" prec 15 14 14
remove module
end
module mach.java.util.Map
prelude export "import java.util.Map;"
prelude export "import java.util.HashMap;"
syntax type map "Map<%1,%2>"
syntax val empty "new HashMap<> ()" prec 15
syntax val size "%1.size ()" prec 15
syntax val containsKey "%1.containsKey (%2)" prec 15
syntax val put "%1.put (%2, %3)" prec 15 14 14
syntax val get "%1.get (%2)" prec 15 14 14
remove module
end
module mach.java.util.List
prelude export "import java.util.List;"
prelude export "import java.util.ArrayList;"
syntax type list "List<%1>"
syntax val empty "new ArrayList<> ()" prec 15
syntax val size "%1.size()" prec 15
syntax val add "%1.add(%2)" prec 15 14 14
syntax val get "%1.get(%2)" prec 15 14 14
syntax val insert "%1.add(%2, %3)" prec 15 14 14 14
syntax val set "%1.set(%2, %3)" prec 15 14 14 14
(* List.copyOf needs JDKs >= 10 *)
syntax val copy_of "List.copyOf(%1)" prec 15 14
remove module
end
module mach.java.util.UnmodifiableList
prelude export "import java.util.List;"
syntax type ulist "List<%1>"
syntax val size "%1.size ()" prec 15
syntax val get "%1.get (%2)" prec 15 14 14
remove module
end
module mach.java.util.Queue
prelude export "import java.util.Queue;"
prelude export "import java.util.ArrayDeque;"
syntax type queue "Queue<%1>"
syntax val empty "new ArrayDeque()" prec 15
syntax val size "%1.size()" prec 15 14
syntax val poll "%1.poll()" prec 15 14
syntax val peek "%1.peek()" prec 15 14
syntax val add "%1.add(%2)" prec 15 14 14
syntax val is_empty "%1.isEmpty()" prec 15 14
syntax val equals "%1.equals(%2)" prec 15 14 14
remove module
end
module mach.java.util.Optional
prelude export "import java.util.Optional;"
syntax type optional "Optional<%1>"
syntax val empty "Optional.ofNullable(null)" prec 15
syntax val build "Optional.of(%1)" prec 15
syntax val is_present "%1.isPresent()" prec 15 14
syntax val is_empty "%1.isEmpty()" prec 15 14
syntax val get "%1.get()" prec 15 14
syntax val get_safe "%1.get()" prec 15 14
remove module
end
module pqueue.PqueueNoDup
remove module
end
module set.Set
remove module
end
module ref.Ref
syntax type ref "%1"
syntax val ref "%1"
syntax val (!) "%1" prec 2 1
syntax val (:=) "%1 = %2" prec 15 14
remove module
end
module ref.Refint
syntax val incr "%1 = %1+1" prec 15 14
syntax val decr "%1 = %1+1" prec 15 14
syntax val (+=) "%1 = %1+%2" prec 15 14
syntax val (-=) "%1 = %1-%2" prec 15 14
syntax val ( *=) "%1 = %1+%2" prec 15 14
remove module
end
module mach.java.lang.Array
prelude export "import java.util.Arrays;\n"
syntax type array "%1 []"
syntax val length "%1.length"
syntax val ([]) "%1[%2]" prec 1 1 15
syntax val ([]<-) "%1[%2] = %3" prec 1 1 15 14
(* syntax val equals "Objects.deepEquals(%1, %2)" prec 1 1 15 14 *)
(* syntax val hash_code "Arrays.deepHashCode(%1)" prec 1 1 15 14 *)
syntax val equals "%1.equals(%2)" prec 1 1 15 14
syntax val hash_code "%1.hashCode()" prec 1 1 15
remove module
end
module mach.java.util.Random
prelude export "import java.util.Random;\n"
syntax type random "Random"
syntax val create "new Random()"
syntax val create_init "new Random(%1)"
syntax val set_seed "%1.setSeed(%2)" prec 1 1 15 14
syntax val next_boolean "%1.nextBoolean()" prec 1 1 15
syntax val next_int "%1.nextInt()" prec 1 1 15
syntax val next_bounded_int "%1.nextInt(%2)" prec 1 1 15 14
remove module
end
(* remove some modules from the standard library *)
module bool.Bool
syntax type bool "boolean"
remove module
end
module map.Map
remove module
end
module map.Const
remove module
end
module number.Divisibility
remove module
end
module int.Int
remove module
end
module int.Abs
remove module
end
module int.ComputerDivision
remove module
end
module int.EuclideanDivision
remove module
end
module int.MinMax
remove module
end
module int.Power
remove module
end
module int.Sum
remove module
end
module real.Real
remove module
end
module real.ExpLog
remove module
end
module real.RealInfix
remove module
end
module real.Square
remove module
end
module mach.int.Unsigned
remove module
end
module seq.Seq
remove module
end
module seq.FreeMonoid
remove module
end
module int.NumOf
remove module
end
module set.Fset
remove module
end
module fmap.Fmap
remove module
end
module pigeon.Pigeonhole
remove module
end
module option.Option
remove module
end
|
