int.bend
bend-kit-int@0.1.0.0 · 1,454 lines · 0 definitions
1# Fixed-width integers U8, U16, U64, I32 and I64: wrapping, checked and saturating arithmetic.
2import Base
3
4# The Int.* core serves only U64 and I64. When Base ships a native U64 (bendlang/bend#1027), delete it.
5def Int.bits.go(n: Nat, qr: Nat & Nat) -> Word(n):
6 match n:
7 case 0n:
8 WNil{}
9 case 1n+p:
10 (q, r) = qr
11 WCon{Nat.is_eq(r, 1n), Int.bits.go(p, Nat.divmod(q, 2n))}
12
13# The low n bits of k: k mod 2^n.
14def Int.bits(n: Nat, k: Nat) -> Word(n):
15 Int.bits.go(n, Nat.divmod(k, 2n))
16
17def Int.msb.go(n: Nat, b: Bool, w: Word(n)) -> Bool:
18 match n:
19 case 0n:
20 b
21 case 1n+p:
22 match w:
23 case WCon{h, t}:
24 Int.msb.go(p, h, t)
25
26def Int.msb(n: Nat, w: Word(n)) -> Bool:
27 Int.msb.go(n, False{}, w)
28
29def Int.put_msb.bit(p: Nat, v: Bool, b: Bool) -> Bool:
30 match p:
31 case 0n:
32 v
33 case 1n+q:
34 b
35
36def Int.put_msb(+n: Nat, +v: Bool, w: Word(n)) -> Word(n):
37 match n:
38 case 0n:
39 WNil{}
40 case 1n+p:
41 match w:
42 case WCon{b, t}:
43 WCon{Int.put_msb.bit(p, v, b), Int.put_msb(p, v, t)}
44
45def Int.ext(m: Nat, n: Nat, +fill: Bool, w: Word(n)) -> Word(m):
46 match m:
47 case 0n:
48 WNil{}
49 case 1n+p:
50 match n:
51 case 0n:
52 WCon{fill, Int.ext(p, 0n, fill, WNil{})}
53 case 1n+q:
54 match w:
55 case WCon{b, t}:
56 WCon{b, Int.ext(p, q, fill, t)}
57
58def Int.ones(+n: Nat) -> Word(n):
59 Word.not(n, Word.zero(n))
60
61def Int.min(+n: Nat, s: Bool) -> Word(n):
62 match s:
63 case True{}:
64 Int.put_msb(n, True{}, Word.zero(n))
65 case False{}:
66 Word.zero(n)
67
68def Int.max(+n: Nat, s: Bool) -> Word(n):
69 match s:
70 case True{}:
71 Int.put_msb(n, False{}, Int.ones(n))
72 case False{}:
73 Int.ones(n)
74
75def Int.is_eq(+n: Nat, a: Word(n), b: Word(n)) -> Bool:
76 Cmp.is_eq(Word.cmp(n, a, b))
77
78def Int.is_zero(+n: Nat, w: Word(n)) -> Bool:
79 Int.is_eq(n, w, Word.zero(n))
80
81def Int.cmp(+n: Nat, s: Bool, a: Word(n), b: Word(n)) -> Cmp:
82 match s:
83 case True{}:
84 Word.cmp(n, Word.xor(n, a, Int.min(n, True{})),
85 Word.xor(n, b, Int.min(n, True{})))
86 case False{}:
87 Word.cmp(n, a, b)
88
89def Int.neg(+n: Nat, w: Word(n)) -> Word(n):
90 Word.sub(n, Word.zero(n), w)
91
92def Int.neg_if(+n: Nat, c: Bool, w: Word(n)) -> Word(n):
93 match c:
94 case True{}:
95 Int.neg(n, w)
96 case False{}:
97 w
98
99def Int.abs(+n: Nat, +w: Word(n)) -> Word(n):
100 Int.neg_if(n, Int.msb(n, w), w)
101
102def Int.udivmod.fin(-p: Nat, q: Word(p), +n: Nat, s: Word(n), b: Word(n),
103 g: Bool) -> Word(1n+p) & Word(n):
104 match g:
105 case True{}:
106 (WCon{True{}, q}, Word.sub(n, s, b))
107 case False{}:
108 (WCon{False{}, q}, s)
109
110def Int.udivmod.shl(-p: Nat, q: Word(p), +n: Nat, +b: Word(n),
111 ts: Bool & Word(n)) -> Word(1n+p) & Word(n):
112 (t, s) = ts
113 +s2 = {s : Word(n)}
114 Int.udivmod.fin(p, q, n, s2, b, Bool.or(t, Cmp.is_ge(Word.cmp(n, s2, b))))
115
116def Int.udivmod.rec(-p: Nat, a0: Bool, +n: Nat, +b: Word(n),
117 qr: Word(p) & Word(n)) -> Word(1n+p) & Word(n):
118 (q, r) = qr
119 Int.udivmod.shl(p, q, n, b, Word.shl.out(n, a0, r))
120
121def Int.udivmod.go(m: Nat, a: Word(m), +n: Nat, +b: Word(n)) ->
122 Word(m) & Word(n):
123 match m a:
124 case 0n WNil{}:
125 (WNil{}, Word.zero(n))
126 case 1n+p WCon{a0, hi}:
127 Int.udivmod.rec(p, a0, n, b, Int.udivmod.go(p, hi, n, b))
128
129def Int.sdivmod.fix(+n: Nat, +na: Bool, nb: Bool, qr: Word(n) & Word(n)) ->
130 Word(n) & Word(n):
131 (q, r) = qr
132 (Int.neg_if(n, Bool.xor(na, nb), q), Int.neg_if(n, na, r))
133
134# x / 0 is 0 and x % 0 is x, as in Base's U32. MIN / -1 wraps to MIN.
135def Int.divmod.if(z: Bool, s: Bool, +n: Nat, +a: Word(n), +b: Word(n)) ->
136 Word(n) & Word(n):
137 match z:
138 case True{}:
139 (Word.zero(n), a)
140 case False{}:
141 match s:
142 case True{}:
143 Int.sdivmod.fix(n, Int.msb(n, a), Int.msb(n, b),
144 Int.udivmod.go(n, Int.abs(n, a), n, Int.abs(n, b)))
145 case False{}:
146 Int.udivmod.go(n, a, n, b)
147
148def Int.divmod(+n: Nat, s: Bool, a: Word(n), +b: Word(n)) ->
149 Word(n) & Word(n):
150 Int.divmod.if(Int.is_zero(n, b), s, n, a, b)
151
152def Int.fst(-n: Nat, p: Word(n) & Word(n)) -> Word(n):
153 (q, r) = p
154 q
155
156def Int.snd(-n: Nat, p: Word(n) & Word(n)) -> Word(n):
157 (q, r) = p
158 r
159
160def Int.div(+n: Nat, s: Bool, a: Word(n), b: Word(n)) -> Word(n):
161 Int.fst(n, Int.divmod(n, s, a, b))
162
163def Int.mod(+n: Nat, s: Bool, a: Word(n), b: Word(n)) -> Word(n):
164 Int.snd(n, Int.divmod(n, s, a, b))
165
166# True for signed MIN and -1, the one quotient that overflows.
167def Int.min_neg1(+n: Nat, s: Bool, a: Word(n), b: Word(n)) -> Bool:
168 match s:
169 case True{}:
170 Bool.and(Int.is_eq(n, a, Int.min(n, True{})),
171 Int.is_eq(n, b, Int.ones(n)))
172 case False{}:
173 False{}
174
175def Int.div_ov(+n: Nat, s: Bool, a: Word(n), +b: Word(n)) -> Bool:
176 Bool.or(Int.is_zero(n, b), Int.min_neg1(n, s, a, b))
177
178def Int.add_ov.go(+n: Nat, s: Bool, a: Word(n), b: Word(n), +r: Word(n)) ->
179 Bool & Word(n):
180 match s:
181 case True{}:
182 (Int.msb(n, Word.and(n, Word.xor(n, a, r), Word.xor(n, b, r))), r)
183 case False{}:
184 (Cmp.is_lt(Word.cmp(n, r, a)), r)
185
186def Int.add_ov(+n: Nat, s: Bool, +a: Word(n), +b: Word(n)) -> Bool & Word(n):
187 Int.add_ov.go(n, s, a, b, Word.add(n, a, b))
188
189def Int.sub_ov.go(+n: Nat, s: Bool, +a: Word(n), b: Word(n), +r: Word(n)) ->
190 Bool & Word(n):
191 match s:
192 case True{}:
193 (Int.msb(n, Word.and(n, Word.xor(n, a, b), Word.xor(n, a, r))), r)
194 case False{}:
195 (Cmp.is_lt(Word.cmp(n, a, b)), r)
196
197def Int.sub_ov(+n: Nat, s: Bool, +a: Word(n), +b: Word(n)) -> Bool & Word(n):
198 Int.sub_ov.go(n, s, a, b, Word.sub(n, a, b))
199
200def Int.mul_ov.go(+n: Nat, +s: Bool, +a: Word(n), +b: Word(n), +r: Word(n)) ->
201 Bool & Word(n):
202 (Bool.or(Bool.and(Bool.not(Int.is_zero(n, b)),
203 Bool.not(Int.is_eq(n, Int.div(n, s, r, b), a))),
204 Int.min_neg1(n, s, a, b)), r)
205
206def Int.mul_ov(+n: Nat, s: Bool, +a: Word(n), +b: Word(n)) -> Bool & Word(n):
207 Int.mul_ov.go(n, s, a, b, Word.mul(n, a, b))
208
209def Int.checked(-n: Nat, o: Bool & Word(n)) -> Maybe<&2, Word(n)>:
210 (ov, r) = o
211 match ov:
212 case True{}:
213 None{}
214 case False{}:
215 Some{r}
216
217def Int.checked_div(+n: Nat, +s: Bool, +a: Word(n), +b: Word(n)) ->
218 Maybe<&2, Word(n)>:
219 Int.checked(n, (Int.div_ov(n, s, a, b), Int.div(n, s, a, b)))
220
221def Int.checked_mod(+n: Nat, +s: Bool, +a: Word(n), +b: Word(n)) ->
222 Maybe<&2, Word(n)>:
223 Int.checked(n, (Int.div_ov(n, s, a, b), Int.mod(n, s, a, b)))
224
225def Int.sat(low: Bool, +n: Nat, s: Bool) -> Word(n):
226 match low:
227 case True{}:
228 Int.min(n, s)
229 case False{}:
230 Int.max(n, s)
231
232def Int.saturate(+n: Nat, s: Bool, low: Bool, o: Bool & Word(n)) -> Word(n):
233 (ov, r) = o
234 match ov:
235 case True{}:
236 Int.sat(low, n, s)
237 case False{}:
238 r
239
240def Int.saturating_add(+n: Nat, +s: Bool, +a: Word(n), b: Word(n)) -> Word(n):
241 Int.saturate(n, s, Bool.and(s, Int.msb(n, a)), Int.add_ov(n, s, a, b))
242
243def Int.saturating_sub(+n: Nat, +s: Bool, +a: Word(n), b: Word(n)) -> Word(n):
244 Int.saturate(n, s, Bool.or(Bool.not(s), Int.msb(n, a)),
245 Int.sub_ov(n, s, a, b))
246
247def Int.saturating_mul(+n: Nat, +s: Bool, +a: Word(n), +b: Word(n)) ->
248 Word(n):
249 Int.saturate(n, s, Bool.and(s, Bool.xor(Int.msb(n, a), Int.msb(n, b))),
250 Int.mul_ov(n, s, a, b))
251
252def Int.shl(+n: Nat, k: Nat, w: Word(n)) -> Word(n):
253 match k:
254 case 0n:
255 w
256 case 1n+j:
257 Int.shl(n, j, Word.shl(n, w))
258
259# Signed shifts right are arithmetic: the sign bit fills in from the top.
260def Int.shr1(+n: Nat, s: Bool, +w: Word(n)) -> Word(n):
261 match s:
262 case True{}:
263 Int.put_msb(n, Int.msb(n, w), Word.shr(n, w))
264 case False{}:
265 Word.shr(n, w)
266
267def Int.shr(+n: Nat, +s: Bool, k: Nat, w: Word(n)) -> Word(n):
268 match k:
269 case 0n:
270 w
271 case 1n+j:
272 Int.shr(n, s, j, Int.shr1(n, s, w))
273
274# z is set once the value left to print is zero; fuel n bounds the digits.
275def Int.show.go(f: Nat, +n: Nat, acc: String, z: Bool,
276 qr: Word(n) & Word(n)) -> String:
277 match f:
278 case 0n:
279 acc
280 case 1n+g:
281 match z:
282 case True{}:
283 acc
284 case False{}:
285 (q, r) = qr
286 +q2 = {q : Word(n)}
287 Int.show.go(g, n,
288 SCon{Chr{U32.add(48, U32.from_nat(Word.to_nat(n, r)))}, acc},
289 Int.is_zero(n, q2), Int.udivmod.go(n, q2, n, Int.bits(n, 10n)))
290
291def Int.show.u(+n: Nat, w: Word(n)) -> String:
292 Int.show.go(n, n, SNil{}, False{}, Int.udivmod.go(n, w, n, Int.bits(n, 10n)))
293
294def Int.show.if(neg: Bool, +n: Nat, w: Word(n)) -> String:
295 match neg:
296 case True{}:
297 SCon{Chr{45}, Int.show.u(n, Int.neg(n, w))}
298 case False{}:
299 Int.show.u(n, w)
300
301def Int.show(+n: Nat, s: Bool, +w: Word(n)) -> String:
302 match s:
303 case True{}:
304 Int.show.if(Int.msb(n, w), n, w)
305 case False{}:
306 Int.show.u(n, w)
307
308def Int.read.add(+n: Nat, d: Word(n), o: Bool & Word(n)) -> Maybe<&2, Word(n)>:
309 (ov, m) = o
310 match ov:
311 case True{}:
312 None{}
313 case False{}:
314 Int.checked(n, Int.add_ov(n, False{}, m, d))
315
316def Int.read.dig(ok: Bool, +n: Nat, acc: Word(n), x: U32) ->
317 Maybe<&2, Word(n)>:
318 match ok:
319 case True{}:
320 Int.read.add(n, Int.bits(n, U32.to_nat(U32.sub(x, 48))),
321 Int.mul_ov(n, False{}, acc, Int.bits(n, 10n)))
322 case False{}:
323 None{}
324
325def Int.read.step(+n: Nat, st: Maybe<&2, Word(n)>, x: U32) ->
326 Maybe<&2, Word(n)>:
327 match st:
328 case None{}:
329 None{}
330 case Some{acc}:
331 +c = {x : U32}
332 Int.read.dig(Bool.and(U32.is_ge(c, 48), U32.is_le(c, 57)), n, acc, c)
333
334def Int.read.go(s: String, +n: Nat, st: Maybe<&2, Word(n)>) ->
335 Maybe<&2, Word(n)>:
336 match s:
337 case SNil{}:
338 st
339 case SCon{Chr{x}, t}:
340 Int.read.go(t, n, Int.read.step(n, st, x))
341
342def Int.read.u(+n: Nat, s: String) -> Maybe<&2, Word(n)>:
343 match s:
344 case SNil{}:
345 None{}
346 case SCon{h, t}:
347 Int.read.go(SCon{h, t}, n, Some{Word.zero(n)})
348
349def Int.read.fit(bad: Bool, -n: Nat, w: Word(n)) -> Maybe<&2, Word(n)>:
350 match bad:
351 case True{}:
352 None{}
353 case False{}:
354 Some{w}
355
356def Int.read.pos(+n: Nat, m: Maybe<&2, Word(n)>) -> Maybe<&2, Word(n)>:
357 match m:
358 case None{}:
359 None{}
360 case Some{w}:
361 +v = {w : Word(n)}
362 Int.read.fit(Int.msb(n, v), n, v)
363
364def Int.read.neg(+n: Nat, m: Maybe<&2, Word(n)>) -> Maybe<&2, Word(n)>:
365 match m:
366 case None{}:
367 None{}
368 case Some{w}:
369 +v = {w : Word(n)}
370 Int.read.fit(Cmp.is_gt(Word.cmp(n, v, Int.min(n, True{}))), n,
371 Int.neg(n, v))
372
373def Int.read.sign(neg: Bool, +n: Nat, t: String, c: U32) -> Maybe<&2, Word(n)>:
374 match neg:
375 case True{}:
376 Int.read.neg(n, Int.read.u(n, t))
377 case False{}:
378 Int.read.pos(n, Int.read.u(n, SCon{Chr{c}, t}))
379
380def Int.read(+n: Nat, s: Bool, str: String) -> Maybe<&2, Word(n)>:
381 match s:
382 case False{}:
383 Int.read.u(n, str)
384 case True{}:
385 match str:
386 case SNil{}:
387 None{}
388 case SCon{Chr{x}, t}:
389 +c = {x : U32}
390 Int.read.sign(U32.is_eq(c, 45), n, t, c)
391
392def Int.to_nat.s(neg: Bool, n: Nat, w: Word(n)) -> Maybe<&2, Nat>:
393 match neg:
394 case True{}:
395 None{}
396 case False{}:
397 Some{Word.to_nat(n, w)}
398
399# Signed values below zero have no Nat.
400def Int.to_nat(+n: Nat, +w: Word(n)) -> Maybe<&2, Nat>:
401 Int.to_nat.s(Int.msb(n, w), n, w)
402
403def Int.sext(m: Nat, +n: Nat, +w: Word(n)) -> Word(m):
404 Int.ext(m, n, Int.msb(n, w), w)
405
406# U8 and U16 hold their value in a U32 below 2^w, and m is 2^w - 1.
407def Nar.opt(ov: Bool, r: U32) -> Maybe<&2, U32>:
408 match ov:
409 case True{}:
410 None{}
411 case False{}:
412 Some{r}
413
414def Nar.over(+m: U32, +r: U32) -> Maybe<&2, U32>:
415 Nar.opt(U32.is_gt(r, m), r)
416
417def Nar.checked_sub(+a: U32, +b: U32) -> Maybe<&2, U32>:
418 Nar.opt(U32.is_lt(a, b), U32.sub(a, b))
419
420def Nar.checked_div(a: U32, +b: U32) -> Maybe<&2, U32>:
421 Nar.opt(U32.is_zero(b), U32.div(a, b))
422
423def Nar.checked_mod(a: U32, +b: U32) -> Maybe<&2, U32>:
424 Nar.opt(U32.is_zero(b), U32.mod(a, b))
425
426def Nar.sat_sub(lt: Bool, a: U32, b: U32) -> U32:
427 match lt:
428 case True{}:
429 0
430 case False{}:
431 U32.sub(a, b)
432
433def Nar.saturating_sub(+a: U32, +b: U32) -> U32:
434 Nar.sat_sub(U32.is_lt(a, b), a, b)
435
436def Nar.read(+m: U32, r: Maybe<&2, U32>) -> Maybe<&2, U32>:
437 match r:
438 case None{}:
439 None{}
440 case Some{x}:
441 +v = {x : U32}
442 Nar.over(m, v)
443
444# I32 holds its two's-complement bits in a U32.
445def S32.MIN() -> U32:
446 2147483648
447
448def S32.is_neg(x: U32) -> Bool:
449 U32.is_ge(x, S32.MIN())
450
451def S32.neg(x: U32) -> U32:
452 U32.sub(0, x)
453
454def S32.neg_if(c: Bool, x: U32) -> U32:
455 match c:
456 case True{}:
457 S32.neg(x)
458 case False{}:
459 x
460
461def S32.abs(+x: U32) -> U32:
462 S32.neg_if(S32.is_neg(x), x)
463
464def S32.cmp(a: U32, b: U32) -> Cmp:
465 U32.cmp(U32.xor(a, S32.MIN()), U32.xor(b, S32.MIN()))
466
467# x / 0 is 0 and x % 0 is x, as in Base's U32. MIN / -1 wraps to MIN.
468def S32.divmod.if(z: Bool, +a: U32, +b: U32) -> U32 & U32:
469 match z:
470 case True{}:
471 (0, a)
472 case False{}:
473 (S32.neg_if(Bool.xor(S32.is_neg(a), S32.is_neg(b)),
474 U32.div(S32.abs(a), S32.abs(b))),
475 S32.neg_if(S32.is_neg(a), U32.mod(S32.abs(a), S32.abs(b))))
476
477def S32.fst(p: U32 & U32) -> U32:
478 (q, r) = p
479 q
480
481def S32.snd(p: U32 & U32) -> U32:
482 (q, r) = p
483 r
484
485def S32.div(a: U32, +b: U32) -> U32:
486 S32.fst(S32.divmod.if(U32.is_zero(b), a, b))
487
488def S32.mod(a: U32, +b: U32) -> U32:
489 S32.snd(S32.divmod.if(U32.is_zero(b), a, b))
490
491# True for MIN and -1, the one quotient that overflows.
492def S32.min_neg1(a: U32, b: U32) -> Bool:
493 Bool.and(U32.is_eq(a, S32.MIN()), U32.is_eq(b, 4294967295))
494
495def S32.div_ov(+a: U32, +b: U32) -> Bool:
496 Bool.or(U32.is_zero(b), S32.min_neg1(a, b))
497
498def S32.add_ov.go(a: U32, b: U32, +r: U32) -> Bool & U32:
499 (S32.is_neg(U32.and(U32.xor(a, r), U32.xor(b, r))), r)
500
501def S32.add_ov(+a: U32, +b: U32) -> Bool & U32:
502 S32.add_ov.go(a, b, U32.add(a, b))
503
504def S32.sub_ov.go(+a: U32, b: U32, +r: U32) -> Bool & U32:
505 (S32.is_neg(U32.and(U32.xor(a, b), U32.xor(a, r))), r)
506
507def S32.sub_ov(+a: U32, +b: U32) -> Bool & U32:
508 S32.sub_ov.go(a, b, U32.sub(a, b))
509
510def S32.mul_ov.go(+a: U32, +b: U32, +r: U32) -> Bool & U32:
511 (Bool.or(Bool.and(Bool.not(U32.is_zero(b)),
512 Bool.not(U32.is_eq(S32.div(r, b), a))), S32.min_neg1(a, b)), r)
513
514def S32.mul_ov(+a: U32, +b: U32) -> Bool & U32:
515 S32.mul_ov.go(a, b, U32.mul(a, b))
516
517def S32.checked(o: Bool & U32) -> Maybe<&2, U32>:
518 (ov, r) = o
519 Nar.opt(ov, r)
520
521def S32.checked_div(+a: U32, +b: U32) -> Maybe<&2, U32>:
522 Nar.opt(S32.div_ov(a, b), S32.div(a, b))
523
524def S32.checked_mod(+a: U32, +b: U32) -> Maybe<&2, U32>:
525 Nar.opt(S32.div_ov(a, b), S32.mod(a, b))
526
527def S32.sat(low: Bool) -> U32:
528 match low:
529 case True{}:
530 S32.MIN()
531 case False{}:
532 2147483647
533
534def S32.saturate(low: Bool, o: Bool & U32) -> U32:
535 (ov, r) = o
536 match ov:
537 case True{}:
538 S32.sat(low)
539 case False{}:
540 r
541
542# Shifts right are arithmetic: the sign bit fills in from the top.
543def S32.shr.if(neg: Bool, x: U32, k: Nat) -> U32:
544 match neg:
545 case True{}:
546 U32.not(U32.shrn(U32.not(x), k))
547 case False{}:
548 U32.shrn(x, k)
549
550def S32.show.if(neg: Bool, x: U32) -> String:
551 match neg:
552 case True{}:
553 SCon{Chr{45}, U32.show(S32.neg(x))}
554 case False{}:
555 U32.show(x)
556
557def S32.read.neg(r: Maybe<&2, U32>) -> Maybe<&2, U32>:
558 match r:
559 case None{}:
560 None{}
561 case Some{x}:
562 +v = {x : U32}
563 Nar.opt(U32.is_gt(v, S32.MIN()), S32.neg(v))
564
565def S32.read.pos(r: Maybe<&2, U32>) -> Maybe<&2, U32>:
566 match r:
567 case None{}:
568 None{}
569 case Some{x}:
570 +v = {x : U32}
571 Nar.opt(S32.is_neg(v), v)
572
573def S32.read.sign(neg: Bool, t: String, c: U32) -> Maybe<&2, U32>:
574 match neg:
575 case True{}:
576 S32.read.neg(U32.read(t))
577 case False{}:
578 S32.read.pos(U32.read(SCon{Chr{c}, t}))
579
580def S32.read(s: String) -> Maybe<&2, U32>:
581 match s:
582 case SNil{}:
583 None{}
584 case SCon{Chr{x}, t}:
585 +c = {x : U32}
586 S32.read.sign(U32.is_eq(c, 45), t, c)
587
588def S32.to_nat.if(neg: Bool, x: U32) -> Maybe<&2, Nat>:
589 match neg:
590 case True{}:
591 None{}
592 case False{}:
593 Some{U32.to_nat(x)}
594
595type U8 is Data:
596 U8{data: U32}
597
598def U8.some(m: Maybe<&2, U32>) -> Maybe<&2, U8>:
599 match m:
600 case None{}:
601 None{}
602 case Some{x}:
603 Some{U8{x}}
604
605def U8.MIN() -> U8:
606 U8{0}
607
608def U8.MAX() -> U8:
609 U8{255}
610
611def U8.add(a: U8, b: U8) -> U8:
612 match a b:
613 case U8{x} U8{y}:
614 U8{U32.and(U32.add(x, y), 255)}
615
616def U8.sub(a: U8, b: U8) -> U8:
617 match a b:
618 case U8{x} U8{y}:
619 U8{U32.and(U32.sub(x, y), 255)}
620
621def U8.mul(a: U8, b: U8) -> U8:
622 match a b:
623 case U8{x} U8{y}:
624 U8{U32.and(U32.mul(x, y), 255)}
625
626def U8.and(a: U8, b: U8) -> U8:
627 match a b:
628 case U8{x} U8{y}:
629 U8{U32.and(x, y)}
630
631def U8.or(a: U8, b: U8) -> U8:
632 match a b:
633 case U8{x} U8{y}:
634 U8{U32.or(x, y)}
635
636def U8.xor(a: U8, b: U8) -> U8:
637 match a b:
638 case U8{x} U8{y}:
639 U8{U32.xor(x, y)}
640
641def U8.div(a: U8, b: U8) -> U8:
642 match a b:
643 case U8{x} U8{y}:
644 U8{U32.div(x, y)}
645
646def U8.mod(a: U8, b: U8) -> U8:
647 match a b:
648 case U8{x} U8{y}:
649 U8{U32.mod(x, y)}
650
651def U8.checked_add(a: U8, b: U8) -> Maybe<&2, U8>:
652 match a b:
653 case U8{x} U8{y}:
654 U8.some(Nar.over(255, U32.add(x, y)))
655
656def U8.checked_sub(a: U8, b: U8) -> Maybe<&2, U8>:
657 match a b:
658 case U8{x} U8{y}:
659 U8.some(Nar.checked_sub(x, y))
660
661def U8.checked_mul(a: U8, b: U8) -> Maybe<&2, U8>:
662 match a b:
663 case U8{x} U8{y}:
664 U8.some(Nar.over(255, U32.mul(x, y)))
665
666def U8.checked_div(a: U8, b: U8) -> Maybe<&2, U8>:
667 match a b:
668 case U8{x} U8{y}:
669 U8.some(Nar.checked_div(x, y))
670
671def U8.checked_mod(a: U8, b: U8) -> Maybe<&2, U8>:
672 match a b:
673 case U8{x} U8{y}:
674 U8.some(Nar.checked_mod(x, y))
675
676def U8.saturating_add(a: U8, b: U8) -> U8:
677 match a b:
678 case U8{x} U8{y}:
679 U8{U32.min(U32.add(x, y), 255)}
680
681def U8.saturating_sub(a: U8, b: U8) -> U8:
682 match a b:
683 case U8{x} U8{y}:
684 U8{Nar.saturating_sub(x, y)}
685
686def U8.saturating_mul(a: U8, b: U8) -> U8:
687 match a b:
688 case U8{x} U8{y}:
689 U8{U32.min(U32.mul(x, y), 255)}
690
691def U8.cmp(a: U8, b: U8) -> Cmp:
692 match a b:
693 case U8{x} U8{y}:
694 U32.cmp(x, y)
695
696def U8.is_eq(a: U8, b: U8) -> Bool:
697 Cmp.is_eq(U8.cmp(a, b))
698
699def U8.is_lt(a: U8, b: U8) -> Bool:
700 Cmp.is_lt(U8.cmp(a, b))
701
702def U8.is_le(a: U8, b: U8) -> Bool:
703 Cmp.is_le(U8.cmp(a, b))
704
705def U8.is_gt(a: U8, b: U8) -> Bool:
706 Cmp.is_gt(U8.cmp(a, b))
707
708def U8.is_ge(a: U8, b: U8) -> Bool:
709 Cmp.is_ge(U8.cmp(a, b))
710
711def U8.is_ne(a: U8, b: U8) -> Bool:
712 Bool.not(Cmp.is_eq(U8.cmp(a, b)))
713
714def U8.is_zero(a: U8) -> Bool:
715 match a:
716 case U8{x}:
717 U32.is_zero(x)
718
719def U8.not(a: U8) -> U8:
720 match a:
721 case U8{x}:
722 U8{U32.xor(x, 255)}
723
724def U8.shl(a: U8, k: Nat) -> U8:
725 match a:
726 case U8{x}:
727 U8{U32.and(U32.shln(x, k), 255)}
728
729def U8.shr(a: U8, k: Nat) -> U8:
730 match a:
731 case U8{x}:
732 U8{U32.shrn(x, k)}
733
734def U8.show(a: U8) -> String:
735 match a:
736 case U8{x}:
737 U32.show(x)
738
739def U8.read(s: String) -> Maybe<&2, U8>:
740 U8.some(Nar.read(255, U32.read(s)))
741
742def U8.to_u32(a: U8) -> U32:
743 match a:
744 case U8{x}:
745 x
746
747def U8.from_u32(a: U32) -> U8:
748 U8{U32.and(a, 255)}
749
750def U8.to_nat(a: U8) -> Nat:
751 match a:
752 case U8{x}:
753 U32.to_nat(x)
754
755def U8.from_nat(k: Nat) -> U8:
756 U8{U32.and(U32.from_nat(k), 255)}
757
758type U16 is Data:
759 U16{data: U32}
760
761def U16.some(m: Maybe<&2, U32>) -> Maybe<&2, U16>:
762 match m:
763 case None{}:
764 None{}
765 case Some{x}:
766 Some{U16{x}}
767
768def U16.MIN() -> U16:
769 U16{0}
770
771def U16.MAX() -> U16:
772 U16{65535}
773
774def U16.add(a: U16, b: U16) -> U16:
775 match a b:
776 case U16{x} U16{y}:
777 U16{U32.and(U32.add(x, y), 65535)}
778
779def U16.sub(a: U16, b: U16) -> U16:
780 match a b:
781 case U16{x} U16{y}:
782 U16{U32.and(U32.sub(x, y), 65535)}
783
784def U16.mul(a: U16, b: U16) -> U16:
785 match a b:
786 case U16{x} U16{y}:
787 U16{U32.and(U32.mul(x, y), 65535)}
788
789def U16.and(a: U16, b: U16) -> U16:
790 match a b:
791 case U16{x} U16{y}:
792 U16{U32.and(x, y)}
793
794def U16.or(a: U16, b: U16) -> U16:
795 match a b:
796 case U16{x} U16{y}:
797 U16{U32.or(x, y)}
798
799def U16.xor(a: U16, b: U16) -> U16:
800 match a b:
801 case U16{x} U16{y}:
802 U16{U32.xor(x, y)}
803
804def U16.div(a: U16, b: U16) -> U16:
805 match a b:
806 case U16{x} U16{y}:
807 U16{U32.div(x, y)}
808
809def U16.mod(a: U16, b: U16) -> U16:
810 match a b:
811 case U16{x} U16{y}:
812 U16{U32.mod(x, y)}
813
814def U16.checked_add(a: U16, b: U16) -> Maybe<&2, U16>:
815 match a b:
816 case U16{x} U16{y}:
817 U16.some(Nar.over(65535, U32.add(x, y)))
818
819def U16.checked_sub(a: U16, b: U16) -> Maybe<&2, U16>:
820 match a b:
821 case U16{x} U16{y}:
822 U16.some(Nar.checked_sub(x, y))
823
824def U16.checked_mul(a: U16, b: U16) -> Maybe<&2, U16>:
825 match a b:
826 case U16{x} U16{y}:
827 U16.some(Nar.over(65535, U32.mul(x, y)))
828
829def U16.checked_div(a: U16, b: U16) -> Maybe<&2, U16>:
830 match a b:
831 case U16{x} U16{y}:
832 U16.some(Nar.checked_div(x, y))
833
834def U16.checked_mod(a: U16, b: U16) -> Maybe<&2, U16>:
835 match a b:
836 case U16{x} U16{y}:
837 U16.some(Nar.checked_mod(x, y))
838
839def U16.saturating_add(a: U16, b: U16) -> U16:
840 match a b:
841 case U16{x} U16{y}:
842 U16{U32.min(U32.add(x, y), 65535)}
843
844def U16.saturating_sub(a: U16, b: U16) -> U16:
845 match a b:
846 case U16{x} U16{y}:
847 U16{Nar.saturating_sub(x, y)}
848
849def U16.saturating_mul(a: U16, b: U16) -> U16:
850 match a b:
851 case U16{x} U16{y}:
852 U16{U32.min(U32.mul(x, y), 65535)}
853
854def U16.cmp(a: U16, b: U16) -> Cmp:
855 match a b:
856 case U16{x} U16{y}:
857 U32.cmp(x, y)
858
859def U16.is_eq(a: U16, b: U16) -> Bool:
860 Cmp.is_eq(U16.cmp(a, b))
861
862def U16.is_lt(a: U16, b: U16) -> Bool:
863 Cmp.is_lt(U16.cmp(a, b))
864
865def U16.is_le(a: U16, b: U16) -> Bool:
866 Cmp.is_le(U16.cmp(a, b))
867
868def U16.is_gt(a: U16, b: U16) -> Bool:
869 Cmp.is_gt(U16.cmp(a, b))
870
871def U16.is_ge(a: U16, b: U16) -> Bool:
872 Cmp.is_ge(U16.cmp(a, b))
873
874def U16.is_ne(a: U16, b: U16) -> Bool:
875 Bool.not(Cmp.is_eq(U16.cmp(a, b)))
876
877def U16.is_zero(a: U16) -> Bool:
878 match a:
879 case U16{x}:
880 U32.is_zero(x)
881
882def U16.not(a: U16) -> U16:
883 match a:
884 case U16{x}:
885 U16{U32.xor(x, 65535)}
886
887def U16.shl(a: U16, k: Nat) -> U16:
888 match a:
889 case U16{x}:
890 U16{U32.and(U32.shln(x, k), 65535)}
891
892def U16.shr(a: U16, k: Nat) -> U16:
893 match a:
894 case U16{x}:
895 U16{U32.shrn(x, k)}
896
897def U16.show(a: U16) -> String:
898 match a:
899 case U16{x}:
900 U32.show(x)
901
902def U16.read(s: String) -> Maybe<&2, U16>:
903 U16.some(Nar.read(65535, U32.read(s)))
904
905def U16.to_u32(a: U16) -> U32:
906 match a:
907 case U16{x}:
908 x
909
910def U16.from_u32(a: U32) -> U16:
911 U16{U32.and(a, 65535)}
912
913def U16.to_nat(a: U16) -> Nat:
914 match a:
915 case U16{x}:
916 U32.to_nat(x)
917
918def U16.from_nat(k: Nat) -> U16:
919 U16{U32.and(U32.from_nat(k), 65535)}
920
921# ponytail: Word(64n) costs about 68 us per op. When Base ships a native U64
922# (bendlang/bend#1027), store Base's U64 here, as U8 and U16 store Base's U32.
923type U64 is Data:
924 U64{data: Word(64n)}
925
926def U64.some(m: Maybe<&2, Word(64n)>) -> Maybe<&2, U64>:
927 match m:
928 case None{}:
929 None{}
930 case Some{x}:
931 Some{U64{x}}
932
933def U64.MIN() -> U64:
934 U64{Int.min(64n, False{})}
935
936def U64.MAX() -> U64:
937 U64{Int.max(64n, False{})}
938
939def U64.add(a: U64, b: U64) -> U64:
940 match a b:
941 case U64{x} U64{y}:
942 U64{Word.add(64n, x, y)}
943
944def U64.sub(a: U64, b: U64) -> U64:
945 match a b:
946 case U64{x} U64{y}:
947 U64{Word.sub(64n, x, y)}
948
949def U64.mul(a: U64, b: U64) -> U64:
950 match a b:
951 case U64{x} U64{y}:
952 U64{Word.mul(64n, x, y)}
953
954def U64.and(a: U64, b: U64) -> U64:
955 match a b:
956 case U64{x} U64{y}:
957 U64{Word.and(64n, x, y)}
958
959def U64.or(a: U64, b: U64) -> U64:
960 match a b:
961 case U64{x} U64{y}:
962 U64{Word.or(64n, x, y)}
963
964def U64.xor(a: U64, b: U64) -> U64:
965 match a b:
966 case U64{x} U64{y}:
967 U64{Word.xor(64n, x, y)}
968
969def U64.div(a: U64, b: U64) -> U64:
970 match a b:
971 case U64{x} U64{y}:
972 U64{Int.div(64n, False{}, x, y)}
973
974def U64.mod(a: U64, b: U64) -> U64:
975 match a b:
976 case U64{x} U64{y}:
977 U64{Int.mod(64n, False{}, x, y)}
978
979def U64.checked_add(a: U64, b: U64) -> Maybe<&2, U64>:
980 match a b:
981 case U64{x} U64{y}:
982 U64.some(Int.checked(64n, Int.add_ov(64n, False{}, x, y)))
983
984def U64.checked_sub(a: U64, b: U64) -> Maybe<&2, U64>:
985 match a b:
986 case U64{x} U64{y}:
987 U64.some(Int.checked(64n, Int.sub_ov(64n, False{}, x, y)))
988
989def U64.checked_mul(a: U64, b: U64) -> Maybe<&2, U64>:
990 match a b:
991 case U64{x} U64{y}:
992 U64.some(Int.checked(64n, Int.mul_ov(64n, False{}, x, y)))
993
994def U64.checked_div(a: U64, b: U64) -> Maybe<&2, U64>:
995 match a b:
996 case U64{x} U64{y}:
997 U64.some(Int.checked_div(64n, False{}, x, y))
998
999def U64.checked_mod(a: U64, b: U64) -> Maybe<&2, U64>:
1000 match a b:
1001 case U64{x} U64{y}:
1002 U64.some(Int.checked_mod(64n, False{}, x, y))
1003
1004def U64.saturating_add(a: U64, b: U64) -> U64:
1005 match a b:
1006 case U64{x} U64{y}:
1007 U64{Int.saturating_add(64n, False{}, x, y)}
1008
1009def U64.saturating_sub(a: U64, b: U64) -> U64:
1010 match a b:
1011 case U64{x} U64{y}:
1012 U64{Int.saturating_sub(64n, False{}, x, y)}
1013
1014def U64.saturating_mul(a: U64, b: U64) -> U64:
1015 match a b:
1016 case U64{x} U64{y}:
1017 U64{Int.saturating_mul(64n, False{}, x, y)}
1018
1019def U64.cmp(a: U64, b: U64) -> Cmp:
1020 match a b:
1021 case U64{x} U64{y}:
1022 Int.cmp(64n, False{}, x, y)
1023
1024def U64.is_eq(a: U64, b: U64) -> Bool:
1025 Cmp.is_eq(U64.cmp(a, b))
1026
1027def U64.is_lt(a: U64, b: U64) -> Bool:
1028 Cmp.is_lt(U64.cmp(a, b))
1029
1030def U64.is_le(a: U64, b: U64) -> Bool:
1031 Cmp.is_le(U64.cmp(a, b))
1032
1033def U64.is_gt(a: U64, b: U64) -> Bool:
1034 Cmp.is_gt(U64.cmp(a, b))
1035
1036def U64.is_ge(a: U64, b: U64) -> Bool:
1037 Cmp.is_ge(U64.cmp(a, b))
1038
1039def U64.is_ne(a: U64, b: U64) -> Bool:
1040 Bool.not(Cmp.is_eq(U64.cmp(a, b)))
1041
1042def U64.is_zero(a: U64) -> Bool:
1043 match a:
1044 case U64{x}:
1045 Int.is_zero(64n, x)
1046
1047def U64.not(a: U64) -> U64:
1048 match a:
1049 case U64{x}:
1050 U64{Word.not(64n, x)}
1051
1052def U64.shl(a: U64, k: Nat) -> U64:
1053 match a:
1054 case U64{x}:
1055 U64{Int.shl(64n, k, x)}
1056
1057def U64.shr(a: U64, k: Nat) -> U64:
1058 match a:
1059 case U64{x}:
1060 U64{Int.shr(64n, False{}, k, x)}
1061
1062def U64.show(a: U64) -> String:
1063 match a:
1064 case U64{x}:
1065 Int.show(64n, False{}, x)
1066
1067def U64.read(s: String) -> Maybe<&2, U64>:
1068 U64.some(Int.read(64n, False{}, s))
1069
1070def U64.to_u32(a: U64) -> U32:
1071 match a:
1072 case U64{x}:
1073 U32{Int.ext(32n, 64n, False{}, x)}
1074
1075def U64.from_u32(a: U32) -> U64:
1076 match a:
1077 case U32{x}:
1078 U64{Int.ext(64n, 32n, False{}, x)}
1079
1080# A native build stops on a Nat past 2^48 - 1, so large U64 values have no native Nat.
1081def U64.to_nat(a: U64) -> Nat:
1082 match a:
1083 case U64{x}:
1084 Word.to_nat(64n, x)
1085
1086def U64.from_nat(k: Nat) -> U64:
1087 U64{Int.bits(64n, k)}
1088
1089type I32 is Data:
1090 I32{data: U32}
1091
1092def I32.some(m: Maybe<&2, U32>) -> Maybe<&2, I32>:
1093 match m:
1094 case None{}:
1095 None{}
1096 case Some{x}:
1097 Some{I32{x}}
1098
1099def I32.MIN() -> I32:
1100 I32{S32.MIN()}
1101
1102def I32.MAX() -> I32:
1103 I32{2147483647}
1104
1105def I32.add(a: I32, b: I32) -> I32:
1106 match a b:
1107 case I32{x} I32{y}:
1108 I32{U32.add(x, y)}
1109
1110def I32.sub(a: I32, b: I32) -> I32:
1111 match a b:
1112 case I32{x} I32{y}:
1113 I32{U32.sub(x, y)}
1114
1115def I32.mul(a: I32, b: I32) -> I32:
1116 match a b:
1117 case I32{x} I32{y}:
1118 I32{U32.mul(x, y)}
1119
1120def I32.and(a: I32, b: I32) -> I32:
1121 match a b:
1122 case I32{x} I32{y}:
1123 I32{U32.and(x, y)}
1124
1125def I32.or(a: I32, b: I32) -> I32:
1126 match a b:
1127 case I32{x} I32{y}:
1128 I32{U32.or(x, y)}
1129
1130def I32.xor(a: I32, b: I32) -> I32:
1131 match a b:
1132 case I32{x} I32{y}:
1133 I32{U32.xor(x, y)}
1134
1135def I32.div(a: I32, b: I32) -> I32:
1136 match a b:
1137 case I32{x} I32{y}:
1138 I32{S32.div(x, y)}
1139
1140def I32.mod(a: I32, b: I32) -> I32:
1141 match a b:
1142 case I32{x} I32{y}:
1143 I32{S32.mod(x, y)}
1144
1145def I32.checked_add(a: I32, b: I32) -> Maybe<&2, I32>:
1146 match a b:
1147 case I32{x} I32{y}:
1148 I32.some(S32.checked(S32.add_ov(x, y)))
1149
1150def I32.checked_sub(a: I32, b: I32) -> Maybe<&2, I32>:
1151 match a b:
1152 case I32{x} I32{y}:
1153 I32.some(S32.checked(S32.sub_ov(x, y)))
1154
1155def I32.checked_mul(a: I32, b: I32) -> Maybe<&2, I32>:
1156 match a b:
1157 case I32{x} I32{y}:
1158 I32.some(S32.checked(S32.mul_ov(x, y)))
1159
1160def I32.checked_div(a: I32, b: I32) -> Maybe<&2, I32>:
1161 match a b:
1162 case I32{x} I32{y}:
1163 I32.some(S32.checked_div(x, y))
1164
1165def I32.checked_mod(a: I32, b: I32) -> Maybe<&2, I32>:
1166 match a b:
1167 case I32{x} I32{y}:
1168 I32.some(S32.checked_mod(x, y))
1169
1170def I32.cmp(a: I32, b: I32) -> Cmp:
1171 match a b:
1172 case I32{x} I32{y}:
1173 S32.cmp(x, y)
1174
1175def I32.saturating_add(a: I32, b: I32) -> I32:
1176 match a b:
1177 case I32{x} I32{y}:
1178 +v = {x : U32}
1179 I32{S32.saturate(S32.is_neg(v), S32.add_ov(v, y))}
1180
1181def I32.saturating_sub(a: I32, b: I32) -> I32:
1182 match a b:
1183 case I32{x} I32{y}:
1184 +v = {x : U32}
1185 I32{S32.saturate(S32.is_neg(v), S32.sub_ov(v, y))}
1186
1187def I32.saturating_mul(a: I32, b: I32) -> I32:
1188 match a b:
1189 case I32{x} I32{y}:
1190 +v = {x : U32}
1191 +w = {y : U32}
1192 I32{S32.saturate(Bool.xor(S32.is_neg(v), S32.is_neg(w)), S32.mul_ov(v, w))}
1193
1194def I32.is_eq(a: I32, b: I32) -> Bool:
1195 Cmp.is_eq(I32.cmp(a, b))
1196
1197def I32.is_lt(a: I32, b: I32) -> Bool:
1198 Cmp.is_lt(I32.cmp(a, b))
1199
1200def I32.is_le(a: I32, b: I32) -> Bool:
1201 Cmp.is_le(I32.cmp(a, b))
1202
1203def I32.is_gt(a: I32, b: I32) -> Bool:
1204 Cmp.is_gt(I32.cmp(a, b))
1205
1206def I32.is_ge(a: I32, b: I32) -> Bool:
1207 Cmp.is_ge(I32.cmp(a, b))
1208
1209def I32.is_ne(a: I32, b: I32) -> Bool:
1210 Bool.not(Cmp.is_eq(I32.cmp(a, b)))
1211
1212def I32.is_zero(a: I32) -> Bool:
1213 match a:
1214 case I32{x}:
1215 U32.is_zero(x)
1216
1217def I32.not(a: I32) -> I32:
1218 match a:
1219 case I32{x}:
1220 I32{U32.not(x)}
1221
1222def I32.shl(a: I32, k: Nat) -> I32:
1223 match a:
1224 case I32{x}:
1225 I32{U32.shln(x, k)}
1226
1227def I32.shr(a: I32, k: Nat) -> I32:
1228 match a:
1229 case I32{x}:
1230 +v = {x : U32}
1231 I32{S32.shr.if(S32.is_neg(v), v, k)}
1232
1233def I32.neg(a: I32) -> I32:
1234 match a:
1235 case I32{x}:
1236 I32{S32.neg(x)}
1237
1238def I32.abs(a: I32) -> I32:
1239 match a:
1240 case I32{x}:
1241 I32{S32.abs(x)}
1242
1243def I32.is_neg(a: I32) -> Bool:
1244 match a:
1245 case I32{x}:
1246 S32.is_neg(x)
1247
1248def I32.show(a: I32) -> String:
1249 match a:
1250 case I32{x}:
1251 +v = {x : U32}
1252 S32.show.if(S32.is_neg(v), v)
1253
1254def I32.read(s: String) -> Maybe<&2, I32>:
1255 I32.some(S32.read(s))
1256
1257def I32.to_u32(a: I32) -> U32:
1258 match a:
1259 case I32{x}:
1260 x
1261
1262def I32.from_u32(a: U32) -> I32:
1263 I32{a}
1264
1265def I32.to_nat(a: I32) -> Maybe<&2, Nat>:
1266 match a:
1267 case I32{x}:
1268 +v = {x : U32}
1269 S32.to_nat.if(S32.is_neg(v), v)
1270
1271def I32.from_nat(k: Nat) -> I32:
1272 I32{U32.from_nat(k)}
1273
1274# ponytail: Word(64n) costs about 68 us per op. When Base ships a native U64
1275# (bendlang/bend#1027), store its bits in Base's U64, as I32 does with Base's U32.
1276type I64 is Data:
1277 I64{data: Word(64n)}
1278
1279def I64.some(m: Maybe<&2, Word(64n)>) -> Maybe<&2, I64>:
1280 match m:
1281 case None{}:
1282 None{}
1283 case Some{x}:
1284 Some{I64{x}}
1285
1286def I64.MIN() -> I64:
1287 I64{Int.min(64n, True{})}
1288
1289def I64.MAX() -> I64:
1290 I64{Int.max(64n, True{})}
1291
1292def I64.add(a: I64, b: I64) -> I64:
1293 match a b:
1294 case I64{x} I64{y}:
1295 I64{Word.add(64n, x, y)}
1296
1297def I64.sub(a: I64, b: I64) -> I64:
1298 match a b:
1299 case I64{x} I64{y}:
1300 I64{Word.sub(64n, x, y)}
1301
1302def I64.mul(a: I64, b: I64) -> I64:
1303 match a b:
1304 case I64{x} I64{y}:
1305 I64{Word.mul(64n, x, y)}
1306
1307def I64.and(a: I64, b: I64) -> I64:
1308 match a b:
1309 case I64{x} I64{y}:
1310 I64{Word.and(64n, x, y)}
1311
1312def I64.or(a: I64, b: I64) -> I64:
1313 match a b:
1314 case I64{x} I64{y}:
1315 I64{Word.or(64n, x, y)}
1316
1317def I64.xor(a: I64, b: I64) -> I64:
1318 match a b:
1319 case I64{x} I64{y}:
1320 I64{Word.xor(64n, x, y)}
1321
1322def I64.div(a: I64, b: I64) -> I64:
1323 match a b:
1324 case I64{x} I64{y}:
1325 I64{Int.div(64n, True{}, x, y)}
1326
1327def I64.mod(a: I64, b: I64) -> I64:
1328 match a b:
1329 case I64{x} I64{y}:
1330 I64{Int.mod(64n, True{}, x, y)}
1331
1332def I64.checked_add(a: I64, b: I64) -> Maybe<&2, I64>:
1333 match a b:
1334 case I64{x} I64{y}:
1335 I64.some(Int.checked(64n, Int.add_ov(64n, True{}, x, y)))
1336
1337def I64.checked_sub(a: I64, b: I64) -> Maybe<&2, I64>:
1338 match a b:
1339 case I64{x} I64{y}:
1340 I64.some(Int.checked(64n, Int.sub_ov(64n, True{}, x, y)))
1341
1342def I64.checked_mul(a: I64, b: I64) -> Maybe<&2, I64>:
1343 match a b:
1344 case I64{x} I64{y}:
1345 I64.some(Int.checked(64n, Int.mul_ov(64n, True{}, x, y)))
1346
1347def I64.checked_div(a: I64, b: I64) -> Maybe<&2, I64>:
1348 match a b:
1349 case I64{x} I64{y}:
1350 I64.some(Int.checked_div(64n, True{}, x, y))
1351
1352def I64.checked_mod(a: I64, b: I64) -> Maybe<&2, I64>:
1353 match a b:
1354 case I64{x} I64{y}:
1355 I64.some(Int.checked_mod(64n, True{}, x, y))
1356
1357def I64.saturating_add(a: I64, b: I64) -> I64:
1358 match a b:
1359 case I64{x} I64{y}:
1360 I64{Int.saturating_add(64n, True{}, x, y)}
1361
1362def I64.saturating_sub(a: I64, b: I64) -> I64:
1363 match a b:
1364 case I64{x} I64{y}:
1365 I64{Int.saturating_sub(64n, True{}, x, y)}
1366
1367def I64.saturating_mul(a: I64, b: I64) -> I64:
1368 match a b:
1369 case I64{x} I64{y}:
1370 I64{Int.saturating_mul(64n, True{}, x, y)}
1371
1372def I64.cmp(a: I64, b: I64) -> Cmp:
1373 match a b:
1374 case I64{x} I64{y}:
1375 Int.cmp(64n, True{}, x, y)
1376
1377def I64.is_eq(a: I64, b: I64) -> Bool:
1378 Cmp.is_eq(I64.cmp(a, b))
1379
1380def I64.is_lt(a: I64, b: I64) -> Bool:
1381 Cmp.is_lt(I64.cmp(a, b))
1382
1383def I64.is_le(a: I64, b: I64) -> Bool:
1384 Cmp.is_le(I64.cmp(a, b))
1385
1386def I64.is_gt(a: I64, b: I64) -> Bool:
1387 Cmp.is_gt(I64.cmp(a, b))
1388
1389def I64.is_ge(a: I64, b: I64) -> Bool:
1390 Cmp.is_ge(I64.cmp(a, b))
1391
1392def I64.is_ne(a: I64, b: I64) -> Bool:
1393 Bool.not(Cmp.is_eq(I64.cmp(a, b)))
1394
1395def I64.is_zero(a: I64) -> Bool:
1396 match a:
1397 case I64{x}:
1398 Int.is_zero(64n, x)
1399
1400def I64.not(a: I64) -> I64:
1401 match a:
1402 case I64{x}:
1403 I64{Word.not(64n, x)}
1404
1405def I64.shl(a: I64, k: Nat) -> I64:
1406 match a:
1407 case I64{x}:
1408 I64{Int.shl(64n, k, x)}
1409
1410def I64.shr(a: I64, k: Nat) -> I64:
1411 match a:
1412 case I64{x}:
1413 I64{Int.shr(64n, True{}, k, x)}
1414
1415def I64.neg(a: I64) -> I64:
1416 match a:
1417 case I64{x}:
1418 I64{Int.neg(64n, x)}
1419
1420def I64.abs(a: I64) -> I64:
1421 match a:
1422 case I64{x}:
1423 I64{Int.abs(64n, x)}
1424
1425def I64.is_neg(a: I64) -> Bool:
1426 match a:
1427 case I64{x}:
1428 Int.msb(64n, x)
1429
1430def I64.show(a: I64) -> String:
1431 match a:
1432 case I64{x}:
1433 Int.show(64n, True{}, x)
1434
1435def I64.read(s: String) -> Maybe<&2, I64>:
1436 I64.some(Int.read(64n, True{}, s))
1437
1438def I64.to_u32(a: I64) -> U32:
1439 match a:
1440 case I64{x}:
1441 U32{Int.sext(32n, 64n, x)}
1442
1443def I64.from_u32(a: U32) -> I64:
1444 match a:
1445 case U32{x}:
1446 I64{Int.ext(64n, 32n, False{}, x)}
1447
1448def I64.to_nat(a: I64) -> Maybe<&2, Nat>:
1449 match a:
1450 case I64{x}:
1451 Int.to_nat(64n, x)
1452
1453def I64.from_nat(k: Nat) -> I64:
1454 I64{Int.bits(64n, k)}