int.bend
bend-kit-int@0.2.0.0 · 1,624 lines · 326 definitions
1
2import Base
3
4
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
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
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
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
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
275def Radix.digit.if(lo: Bool, d: U32) -> Char:
276 match lo:
277 case True{}:
278 Chr{U32.add(48, d)}
279 case False{}:
280 Chr{U32.add(87, d)}
281
282def Radix.digit(+d: U32) -> Char:
283 Radix.digit.if(U32.is_lt(d, 10), d)
284
285def Radix.in(+c: U32, lo: U32, hi: U32) -> Bool:
286 Bool.and(U32.is_ge(c, lo), U32.is_le(c, hi))
287
288def Radix.value.lower(ok: Bool, c: U32) -> U32:
289 match ok:
290 case True{}:
291 U32.sub(c, 87)
292 case False{}:
293 36
294
295def Radix.value.upper(ok: Bool, +c: U32) -> U32:
296 match ok:
297 case True{}:
298 U32.sub(c, 55)
299 case False{}:
300 Radix.value.lower(Radix.in(c, 97, 122), c)
301
302def Radix.value.if(ok: Bool, +c: U32) -> U32:
303 match ok:
304 case True{}:
305 U32.sub(c, 48)
306 case False{}:
307 Radix.value.upper(Radix.in(c, 65, 90), c)
308
309
310def Radix.value(+c: U32) -> U32:
311 Radix.value.if(Radix.in(c, 48, 57), c)
312
313def Radix.clamp(r: U32) -> U32:
314 U32.clamp(r, 2, 36)
315
316def Radix.ok(+r: U32) -> Bool:
317 Radix.in(r, 2, 36)
318
319def Radix.sign.if(neg: Bool, pos: Bool, c: Char, t: String) -> Bool & String:
320 match neg:
321 case True{}:
322 (True{}, t)
323 case False{}:
324 match pos:
325 case True{}:
326 (False{}, t)
327 case False{}:
328 (False{}, SCon{c, t})
329
330
331def Radix.sign(s: String) -> Bool & String:
332 match s:
333 case SNil{}:
334 (False{}, SNil{})
335 case SCon{Chr{x}, t}:
336 +c = {x : U32}
337 Radix.sign.if(U32.is_eq(c, 45), U32.is_eq(c, 43), Chr{c}, t)
338
339
340def Int.show.go(f: Nat, +n: Nat, +b: Word(n), acc: String, z: Bool,
341 qr: Word(n) & Word(n)) -> String:
342 match f:
343 case 0n:
344 acc
345 case 1n+g:
346 match z:
347 case True{}:
348 acc
349 case False{}:
350 (q, r) = qr
351 +q2 = {q : Word(n)}
352 Int.show.go(g, n, b,
353 SCon{Radix.digit(U32.from_nat(Word.to_nat(n, r))), acc},
354 Int.is_zero(n, q2), Int.udivmod.go(n, q2, n, b))
355
356def Int.show.u(+n: Nat, +b: Word(n), w: Word(n)) -> String:
357 Int.show.go(n, n, b, SNil{}, False{}, Int.udivmod.go(n, w, n, b))
358
359def Int.show.if(neg: Bool, +n: Nat, +b: Word(n), w: Word(n)) -> String:
360 match neg:
361 case True{}:
362 SCon{Chr{45}, Int.show.u(n, b, Int.neg(n, w))}
363 case False{}:
364 Int.show.u(n, b, w)
365
366def Int.show(+n: Nat, s: Bool, r: U32, +w: Word(n)) -> String:
367 match s:
368 case True{}:
369 Int.show.if(Int.msb(n, w), n, Int.bits(n, U32.to_nat(Radix.clamp(r))), w)
370 case False{}:
371 Int.show.u(n, Int.bits(n, U32.to_nat(Radix.clamp(r))), w)
372
373def Int.read.add(+n: Nat, d: Word(n), o: Bool & Word(n)) -> Maybe<&2, Word(n)>:
374 (ov, m) = o
375 match ov:
376 case True{}:
377 None{}
378 case False{}:
379 Int.checked(n, Int.add_ov(n, False{}, m, d))
380
381def Int.read.dig(ok: Bool, +n: Nat, +b: Word(n), acc: Word(n), d: U32) ->
382 Maybe<&2, Word(n)>:
383 match ok:
384 case True{}:
385 Int.read.add(n, Int.bits(n, U32.to_nat(d)), Int.mul_ov(n, False{}, acc, b))
386 case False{}:
387 None{}
388
389def Int.read.step(+n: Nat, +b: Word(n), +r: U32, st: Maybe<&2, Word(n)>,
390 x: U32) -> Maybe<&2, Word(n)>:
391 match st:
392 case None{}:
393 None{}
394 case Some{acc}:
395 +d = {Radix.value(x) : U32}
396 Int.read.dig(U32.is_lt(d, r), n, b, acc, d)
397
398def Int.read.go(s: String, +n: Nat, +b: Word(n), +r: U32,
399 st: Maybe<&2, Word(n)>) -> Maybe<&2, Word(n)>:
400 match s:
401 case SNil{}:
402 st
403 case SCon{Chr{x}, t}:
404 Int.read.go(t, n, b, r, Int.read.step(n, b, r, st, x))
405
406def Int.read.u(+n: Nat, +b: Word(n), +r: U32, s: String) -> Maybe<&2, Word(n)>:
407 match s:
408 case SNil{}:
409 None{}
410 case SCon{h, t}:
411 Int.read.go(SCon{h, t}, n, b, r, Some{Word.zero(n)})
412
413def Int.read.fit(bad: Bool, -n: Nat, w: Word(n)) -> Maybe<&2, Word(n)>:
414 match bad:
415 case True{}:
416 None{}
417 case False{}:
418 Some{w}
419
420def Int.read.pos(+n: Nat, m: Maybe<&2, Word(n)>) -> Maybe<&2, Word(n)>:
421 match m:
422 case None{}:
423 None{}
424 case Some{w}:
425 +v = {w : Word(n)}
426 Int.read.fit(Int.msb(n, v), n, v)
427
428def Int.read.neg(+n: Nat, m: Maybe<&2, Word(n)>) -> Maybe<&2, Word(n)>:
429 match m:
430 case None{}:
431 None{}
432 case Some{w}:
433 +v = {w : Word(n)}
434 Int.read.fit(Cmp.is_gt(Word.cmp(n, v, Int.min(n, True{}))), n,
435 Int.neg(n, v))
436
437def Int.read.sign(s: Bool, neg: Bool, +n: Nat, +b: Word(n), +r: U32,
438 t: String) -> Maybe<&2, Word(n)>:
439 match s:
440 case True{}:
441 match neg:
442 case True{}:
443 Int.read.neg(n, Int.read.u(n, b, r, t))
444 case False{}:
445 Int.read.pos(n, Int.read.u(n, b, r, t))
446 case False{}:
447 match neg:
448 case True{}:
449 None{}
450 case False{}:
451 Int.read.u(n, b, r, t)
452
453def Int.read.split(s: Bool, +n: Nat, +r: U32, p: Bool & String) ->
454 Maybe<&2, Word(n)>:
455 (neg, t) = p
456 Int.read.sign(s, neg, n, Int.bits(n, U32.to_nat(r)), r, t)
457
458def Int.read.if(ok: Bool, +n: Nat, s: Bool, +r: U32, str: String) ->
459 Maybe<&2, Word(n)>:
460 match ok:
461 case True{}:
462 Int.read.split(s, n, r, Radix.sign(str))
463 case False{}:
464 None{}
465
466def Int.read(+n: Nat, s: Bool, +r: U32, str: String) -> Maybe<&2, Word(n)>:
467 Int.read.if(Radix.ok(r), n, s, r, str)
468
469def Int.to_nat.s(neg: Bool, n: Nat, w: Word(n)) -> Maybe<&2, Nat>:
470 match neg:
471 case True{}:
472 None{}
473 case False{}:
474 Some{Word.to_nat(n, w)}
475
476
477def Int.to_nat(+n: Nat, +w: Word(n)) -> Maybe<&2, Nat>:
478 Int.to_nat.s(Int.msb(n, w), n, w)
479
480def Int.sext(m: Nat, +n: Nat, +w: Word(n)) -> Word(m):
481 Int.ext(m, n, Int.msb(n, w), w)
482
483
484def Nar.opt(ov: Bool, r: U32) -> Maybe<&2, U32>:
485 match ov:
486 case True{}:
487 None{}
488 case False{}:
489 Some{r}
490
491def Nar.over(+m: U32, +r: U32) -> Maybe<&2, U32>:
492 Nar.opt(U32.is_gt(r, m), r)
493
494def Nar.checked_sub(+a: U32, +b: U32) -> Maybe<&2, U32>:
495 Nar.opt(U32.is_lt(a, b), U32.sub(a, b))
496
497def Nar.checked_div(a: U32, +b: U32) -> Maybe<&2, U32>:
498 Nar.opt(U32.is_zero(b), U32.div(a, b))
499
500def Nar.checked_mod(a: U32, +b: U32) -> Maybe<&2, U32>:
501 Nar.opt(U32.is_zero(b), U32.mod(a, b))
502
503def Nar.sat_sub(lt: Bool, a: U32, b: U32) -> U32:
504 match lt:
505 case True{}:
506 0
507 case False{}:
508 U32.sub(a, b)
509
510def Nar.saturating_sub(+a: U32, +b: U32) -> U32:
511 Nar.sat_sub(U32.is_lt(a, b), a, b)
512
513
514def Nar.show.go(f: Nat, +r: U32, acc: String, z: Bool, +x: U32) -> String:
515 match f:
516 case 0n:
517 acc
518 case 1n+g:
519 match z:
520 case True{}:
521 acc
522 case False{}:
523 +q = {U32.div(x, r) : U32}
524 Nar.show.go(g, r, SCon{Radix.digit(U32.mod(x, r)), acc},
525 U32.is_zero(q), q)
526
527def Nar.show(r: U32, x: U32) -> String:
528 Nar.show.go(32n, Radix.clamp(r), SNil{}, False{}, x)
529
530def Nar.read.dig(ok: Bool, +r: U32, acc: U32, d: U32) -> Maybe<&2, U32>:
531 match ok:
532 case True{}:
533 Some{U32.add(U32.mul(acc, r), d)}
534 case False{}:
535 None{}
536
537
538def Nar.read.step(+r: U32, +m: U32, st: Maybe<&2, U32>, x: U32) ->
539 Maybe<&2, U32>:
540 match st:
541 case None{}:
542 None{}
543 case Some{acc}:
544 +a = {acc : U32}
545 +d = {Radix.value(x) : U32}
546 Nar.read.dig(Bool.and(U32.is_lt(d, r),
547 U32.is_le(a, U32.div(U32.sub(m, d), r))), r, a, d)
548
549def Nar.read.go(s: String, +r: U32, +m: U32, st: Maybe<&2, U32>) ->
550 Maybe<&2, U32>:
551 match s:
552 case SNil{}:
553 st
554 case SCon{Chr{x}, t}:
555 Nar.read.go(t, r, m, Nar.read.step(r, m, st, x))
556
557
558def Nar.read.u(+r: U32, +m: U32, s: String) -> Maybe<&2, U32>:
559 match s:
560 case SNil{}:
561 None{}
562 case SCon{h, t}:
563 Nar.read.go(SCon{h, t}, r, m, Some{0})
564
565def Nar.read.split(+r: U32, +m: U32, p: Bool & String) -> Maybe<&2, U32>:
566 (neg, t) = p
567 match neg:
568 case True{}:
569 None{}
570 case False{}:
571 Nar.read.u(r, m, t)
572
573def Nar.read.if(ok: Bool, +r: U32, +m: U32, s: String) -> Maybe<&2, U32>:
574 match ok:
575 case True{}:
576 Nar.read.split(r, m, Radix.sign(s))
577 case False{}:
578 None{}
579
580def Nar.read(+r: U32, +m: U32, s: String) -> Maybe<&2, U32>:
581 Nar.read.if(Radix.ok(r), r, m, s)
582
583
584def S32.MIN() -> U32:
585 2147483648
586
587def S32.is_neg(x: U32) -> Bool:
588 U32.is_ge(x, S32.MIN())
589
590def S32.neg(x: U32) -> U32:
591 U32.sub(0, x)
592
593def S32.neg_if(c: Bool, x: U32) -> U32:
594 match c:
595 case True{}:
596 S32.neg(x)
597 case False{}:
598 x
599
600def S32.abs(+x: U32) -> U32:
601 S32.neg_if(S32.is_neg(x), x)
602
603def S32.cmp(a: U32, b: U32) -> Cmp:
604 U32.cmp(U32.xor(a, S32.MIN()), U32.xor(b, S32.MIN()))
605
606
607def S32.divmod.if(z: Bool, +a: U32, +b: U32) -> U32 & U32:
608 match z:
609 case True{}:
610 (0, a)
611 case False{}:
612 (S32.neg_if(Bool.xor(S32.is_neg(a), S32.is_neg(b)),
613 U32.div(S32.abs(a), S32.abs(b))),
614 S32.neg_if(S32.is_neg(a), U32.mod(S32.abs(a), S32.abs(b))))
615
616def S32.fst(p: U32 & U32) -> U32:
617 (q, r) = p
618 q
619
620def S32.snd(p: U32 & U32) -> U32:
621 (q, r) = p
622 r
623
624def S32.div(a: U32, +b: U32) -> U32:
625 S32.fst(S32.divmod.if(U32.is_zero(b), a, b))
626
627def S32.mod(a: U32, +b: U32) -> U32:
628 S32.snd(S32.divmod.if(U32.is_zero(b), a, b))
629
630
631def S32.min_neg1(a: U32, b: U32) -> Bool:
632 Bool.and(U32.is_eq(a, S32.MIN()), U32.is_eq(b, 4294967295))
633
634def S32.div_ov(+a: U32, +b: U32) -> Bool:
635 Bool.or(U32.is_zero(b), S32.min_neg1(a, b))
636
637def S32.add_ov.go(a: U32, b: U32, +r: U32) -> Bool & U32:
638 (S32.is_neg(U32.and(U32.xor(a, r), U32.xor(b, r))), r)
639
640def S32.add_ov(+a: U32, +b: U32) -> Bool & U32:
641 S32.add_ov.go(a, b, U32.add(a, b))
642
643def S32.sub_ov.go(+a: U32, b: U32, +r: U32) -> Bool & U32:
644 (S32.is_neg(U32.and(U32.xor(a, b), U32.xor(a, r))), r)
645
646def S32.sub_ov(+a: U32, +b: U32) -> Bool & U32:
647 S32.sub_ov.go(a, b, U32.sub(a, b))
648
649def S32.mul_ov.go(+a: U32, +b: U32, +r: U32) -> Bool & U32:
650 (Bool.or(Bool.and(Bool.not(U32.is_zero(b)),
651 Bool.not(U32.is_eq(S32.div(r, b), a))), S32.min_neg1(a, b)), r)
652
653def S32.mul_ov(+a: U32, +b: U32) -> Bool & U32:
654 S32.mul_ov.go(a, b, U32.mul(a, b))
655
656def S32.checked(o: Bool & U32) -> Maybe<&2, U32>:
657 (ov, r) = o
658 Nar.opt(ov, r)
659
660def S32.checked_div(+a: U32, +b: U32) -> Maybe<&2, U32>:
661 Nar.opt(S32.div_ov(a, b), S32.div(a, b))
662
663def S32.checked_mod(+a: U32, +b: U32) -> Maybe<&2, U32>:
664 Nar.opt(S32.div_ov(a, b), S32.mod(a, b))
665
666def S32.sat(low: Bool) -> U32:
667 match low:
668 case True{}:
669 S32.MIN()
670 case False{}:
671 2147483647
672
673def S32.saturate(low: Bool, o: Bool & U32) -> U32:
674 (ov, r) = o
675 match ov:
676 case True{}:
677 S32.sat(low)
678 case False{}:
679 r
680
681
682def S32.shr.if(neg: Bool, x: U32, k: Nat) -> U32:
683 match neg:
684 case True{}:
685 U32.not(U32.shrn(U32.not(x), k))
686 case False{}:
687 U32.shrn(x, k)
688
689def S32.show.if(neg: Bool, r: U32, x: U32) -> String:
690 match neg:
691 case True{}:
692 SCon{Chr{45}, Nar.show(r, S32.neg(x))}
693 case False{}:
694 Nar.show(r, x)
695
696def S32.read.neg(m: Maybe<&2, U32>) -> Maybe<&2, U32>:
697 match m:
698 case None{}:
699 None{}
700 case Some{x}:
701 Some{S32.neg(x)}
702
703def S32.read.split(+r: U32, p: Bool & String) -> Maybe<&2, U32>:
704 (neg, t) = p
705 match neg:
706 case True{}:
707 S32.read.neg(Nar.read.u(r, S32.MIN(), t))
708 case False{}:
709 Nar.read.u(r, 2147483647, t)
710
711def S32.read.if(ok: Bool, +r: U32, s: String) -> Maybe<&2, U32>:
712 match ok:
713 case True{}:
714 S32.read.split(r, Radix.sign(s))
715 case False{}:
716 None{}
717
718def S32.read(+r: U32, s: String) -> Maybe<&2, U32>:
719 S32.read.if(Radix.ok(r), r, s)
720
721def S32.to_nat.if(neg: Bool, x: U32) -> Maybe<&2, Nat>:
722 match neg:
723 case True{}:
724 None{}
725 case False{}:
726 Some{U32.to_nat(x)}
727
728
729def U32.show_radix(r: U32, x: U32) -> String:
730 Nar.show(r, x)
731
732def U32.read_radix(+r: U32, s: String) -> Maybe<&2, U32>:
733 Nar.read(r, 4294967295, s)
734
735type U8 is Data:
736 U8{data: U32}
737
738def U8.some(m: Maybe<&2, U32>) -> Maybe<&2, U8>:
739 match m:
740 case None{}:
741 None{}
742 case Some{x}:
743 Some{U8{x}}
744
745def U8.MIN() -> U8:
746 U8{0}
747
748def U8.MAX() -> U8:
749 U8{255}
750
751def U8.add(a: U8, b: U8) -> U8:
752 match a b:
753 case U8{x} U8{y}:
754 U8{U32.and(U32.add(x, y), 255)}
755
756def U8.sub(a: U8, b: U8) -> U8:
757 match a b:
758 case U8{x} U8{y}:
759 U8{U32.and(U32.sub(x, y), 255)}
760
761def U8.mul(a: U8, b: U8) -> U8:
762 match a b:
763 case U8{x} U8{y}:
764 U8{U32.and(U32.mul(x, y), 255)}
765
766def U8.and(a: U8, b: U8) -> U8:
767 match a b:
768 case U8{x} U8{y}:
769 U8{U32.and(x, y)}
770
771def U8.or(a: U8, b: U8) -> U8:
772 match a b:
773 case U8{x} U8{y}:
774 U8{U32.or(x, y)}
775
776def U8.xor(a: U8, b: U8) -> U8:
777 match a b:
778 case U8{x} U8{y}:
779 U8{U32.xor(x, y)}
780
781def U8.div(a: U8, b: U8) -> U8:
782 match a b:
783 case U8{x} U8{y}:
784 U8{U32.div(x, y)}
785
786def U8.mod(a: U8, b: U8) -> U8:
787 match a b:
788 case U8{x} U8{y}:
789 U8{U32.mod(x, y)}
790
791def U8.checked_add(a: U8, b: U8) -> Maybe<&2, U8>:
792 match a b:
793 case U8{x} U8{y}:
794 U8.some(Nar.over(255, U32.add(x, y)))
795
796def U8.checked_sub(a: U8, b: U8) -> Maybe<&2, U8>:
797 match a b:
798 case U8{x} U8{y}:
799 U8.some(Nar.checked_sub(x, y))
800
801def U8.checked_mul(a: U8, b: U8) -> Maybe<&2, U8>:
802 match a b:
803 case U8{x} U8{y}:
804 U8.some(Nar.over(255, U32.mul(x, y)))
805
806def U8.checked_div(a: U8, b: U8) -> Maybe<&2, U8>:
807 match a b:
808 case U8{x} U8{y}:
809 U8.some(Nar.checked_div(x, y))
810
811def U8.checked_mod(a: U8, b: U8) -> Maybe<&2, U8>:
812 match a b:
813 case U8{x} U8{y}:
814 U8.some(Nar.checked_mod(x, y))
815
816def U8.saturating_add(a: U8, b: U8) -> U8:
817 match a b:
818 case U8{x} U8{y}:
819 U8{U32.min(U32.add(x, y), 255)}
820
821def U8.saturating_sub(a: U8, b: U8) -> U8:
822 match a b:
823 case U8{x} U8{y}:
824 U8{Nar.saturating_sub(x, y)}
825
826def U8.saturating_mul(a: U8, b: U8) -> U8:
827 match a b:
828 case U8{x} U8{y}:
829 U8{U32.min(U32.mul(x, y), 255)}
830
831def U8.cmp(a: U8, b: U8) -> Cmp:
832 match a b:
833 case U8{x} U8{y}:
834 U32.cmp(x, y)
835
836def U8.is_eq(a: U8, b: U8) -> Bool:
837 Cmp.is_eq(U8.cmp(a, b))
838
839def U8.is_lt(a: U8, b: U8) -> Bool:
840 Cmp.is_lt(U8.cmp(a, b))
841
842def U8.is_le(a: U8, b: U8) -> Bool:
843 Cmp.is_le(U8.cmp(a, b))
844
845def U8.is_gt(a: U8, b: U8) -> Bool:
846 Cmp.is_gt(U8.cmp(a, b))
847
848def U8.is_ge(a: U8, b: U8) -> Bool:
849 Cmp.is_ge(U8.cmp(a, b))
850
851def U8.is_ne(a: U8, b: U8) -> Bool:
852 Bool.not(Cmp.is_eq(U8.cmp(a, b)))
853
854def U8.is_zero(a: U8) -> Bool:
855 match a:
856 case U8{x}:
857 U32.is_zero(x)
858
859def U8.not(a: U8) -> U8:
860 match a:
861 case U8{x}:
862 U8{U32.xor(x, 255)}
863
864def U8.shl(a: U8, k: Nat) -> U8:
865 match a:
866 case U8{x}:
867 U8{U32.and(U32.shln(x, k), 255)}
868
869def U8.shr(a: U8, k: Nat) -> U8:
870 match a:
871 case U8{x}:
872 U8{U32.shrn(x, k)}
873
874def U8.show_radix(r: U32, a: U8) -> String:
875 match a:
876 case U8{x}:
877 Nar.show(r, x)
878
879def U8.show(a: U8) -> String:
880 U8.show_radix(10, a)
881
882def U8.read_radix(r: U32, s: String) -> Maybe<&2, U8>:
883 U8.some(Nar.read(r, 255, s))
884
885def U8.read(s: String) -> Maybe<&2, U8>:
886 U8.read_radix(10, s)
887
888def U8.to_u32(a: U8) -> U32:
889 match a:
890 case U8{x}:
891 x
892
893def U8.from_u32(a: U32) -> U8:
894 U8{U32.and(a, 255)}
895
896def U8.to_nat(a: U8) -> Nat:
897 match a:
898 case U8{x}:
899 U32.to_nat(x)
900
901def U8.from_nat(k: Nat) -> U8:
902 U8{U32.and(U32.from_nat(k), 255)}
903
904type U16 is Data:
905 U16{data: U32}
906
907def U16.some(m: Maybe<&2, U32>) -> Maybe<&2, U16>:
908 match m:
909 case None{}:
910 None{}
911 case Some{x}:
912 Some{U16{x}}
913
914def U16.MIN() -> U16:
915 U16{0}
916
917def U16.MAX() -> U16:
918 U16{65535}
919
920def U16.add(a: U16, b: U16) -> U16:
921 match a b:
922 case U16{x} U16{y}:
923 U16{U32.and(U32.add(x, y), 65535)}
924
925def U16.sub(a: U16, b: U16) -> U16:
926 match a b:
927 case U16{x} U16{y}:
928 U16{U32.and(U32.sub(x, y), 65535)}
929
930def U16.mul(a: U16, b: U16) -> U16:
931 match a b:
932 case U16{x} U16{y}:
933 U16{U32.and(U32.mul(x, y), 65535)}
934
935def U16.and(a: U16, b: U16) -> U16:
936 match a b:
937 case U16{x} U16{y}:
938 U16{U32.and(x, y)}
939
940def U16.or(a: U16, b: U16) -> U16:
941 match a b:
942 case U16{x} U16{y}:
943 U16{U32.or(x, y)}
944
945def U16.xor(a: U16, b: U16) -> U16:
946 match a b:
947 case U16{x} U16{y}:
948 U16{U32.xor(x, y)}
949
950def U16.div(a: U16, b: U16) -> U16:
951 match a b:
952 case U16{x} U16{y}:
953 U16{U32.div(x, y)}
954
955def U16.mod(a: U16, b: U16) -> U16:
956 match a b:
957 case U16{x} U16{y}:
958 U16{U32.mod(x, y)}
959
960def U16.checked_add(a: U16, b: U16) -> Maybe<&2, U16>:
961 match a b:
962 case U16{x} U16{y}:
963 U16.some(Nar.over(65535, U32.add(x, y)))
964
965def U16.checked_sub(a: U16, b: U16) -> Maybe<&2, U16>:
966 match a b:
967 case U16{x} U16{y}:
968 U16.some(Nar.checked_sub(x, y))
969
970def U16.checked_mul(a: U16, b: U16) -> Maybe<&2, U16>:
971 match a b:
972 case U16{x} U16{y}:
973 U16.some(Nar.over(65535, U32.mul(x, y)))
974
975def U16.checked_div(a: U16, b: U16) -> Maybe<&2, U16>:
976 match a b:
977 case U16{x} U16{y}:
978 U16.some(Nar.checked_div(x, y))
979
980def U16.checked_mod(a: U16, b: U16) -> Maybe<&2, U16>:
981 match a b:
982 case U16{x} U16{y}:
983 U16.some(Nar.checked_mod(x, y))
984
985def U16.saturating_add(a: U16, b: U16) -> U16:
986 match a b:
987 case U16{x} U16{y}:
988 U16{U32.min(U32.add(x, y), 65535)}
989
990def U16.saturating_sub(a: U16, b: U16) -> U16:
991 match a b:
992 case U16{x} U16{y}:
993 U16{Nar.saturating_sub(x, y)}
994
995def U16.saturating_mul(a: U16, b: U16) -> U16:
996 match a b:
997 case U16{x} U16{y}:
998 U16{U32.min(U32.mul(x, y), 65535)}
999
1000def U16.cmp(a: U16, b: U16) -> Cmp:
1001 match a b:
1002 case U16{x} U16{y}:
1003 U32.cmp(x, y)
1004
1005def U16.is_eq(a: U16, b: U16) -> Bool:
1006 Cmp.is_eq(U16.cmp(a, b))
1007
1008def U16.is_lt(a: U16, b: U16) -> Bool:
1009 Cmp.is_lt(U16.cmp(a, b))
1010
1011def U16.is_le(a: U16, b: U16) -> Bool:
1012 Cmp.is_le(U16.cmp(a, b))
1013
1014def U16.is_gt(a: U16, b: U16) -> Bool:
1015 Cmp.is_gt(U16.cmp(a, b))
1016
1017def U16.is_ge(a: U16, b: U16) -> Bool:
1018 Cmp.is_ge(U16.cmp(a, b))
1019
1020def U16.is_ne(a: U16, b: U16) -> Bool:
1021 Bool.not(Cmp.is_eq(U16.cmp(a, b)))
1022
1023def U16.is_zero(a: U16) -> Bool:
1024 match a:
1025 case U16{x}:
1026 U32.is_zero(x)
1027
1028def U16.not(a: U16) -> U16:
1029 match a:
1030 case U16{x}:
1031 U16{U32.xor(x, 65535)}
1032
1033def U16.shl(a: U16, k: Nat) -> U16:
1034 match a:
1035 case U16{x}:
1036 U16{U32.and(U32.shln(x, k), 65535)}
1037
1038def U16.shr(a: U16, k: Nat) -> U16:
1039 match a:
1040 case U16{x}:
1041 U16{U32.shrn(x, k)}
1042
1043def U16.show_radix(r: U32, a: U16) -> String:
1044 match a:
1045 case U16{x}:
1046 Nar.show(r, x)
1047
1048def U16.show(a: U16) -> String:
1049 U16.show_radix(10, a)
1050
1051def U16.read_radix(r: U32, s: String) -> Maybe<&2, U16>:
1052 U16.some(Nar.read(r, 65535, s))
1053
1054def U16.read(s: String) -> Maybe<&2, U16>:
1055 U16.read_radix(10, s)
1056
1057def U16.to_u32(a: U16) -> U32:
1058 match a:
1059 case U16{x}:
1060 x
1061
1062def U16.from_u32(a: U32) -> U16:
1063 U16{U32.and(a, 65535)}
1064
1065def U16.to_nat(a: U16) -> Nat:
1066 match a:
1067 case U16{x}:
1068 U32.to_nat(x)
1069
1070def U16.from_nat(k: Nat) -> U16:
1071 U16{U32.and(U32.from_nat(k), 65535)}
1072
1073
1074
1075type U64 is Data:
1076 U64{data: Word(64n)}
1077
1078def U64.some(m: Maybe<&2, Word(64n)>) -> Maybe<&2, U64>:
1079 match m:
1080 case None{}:
1081 None{}
1082 case Some{x}:
1083 Some{U64{x}}
1084
1085def U64.MIN() -> U64:
1086 U64{Int.min(64n, False{})}
1087
1088def U64.MAX() -> U64:
1089 U64{Int.max(64n, False{})}
1090
1091def U64.add(a: U64, b: U64) -> U64:
1092 match a b:
1093 case U64{x} U64{y}:
1094 U64{Word.add(64n, x, y)}
1095
1096def U64.sub(a: U64, b: U64) -> U64:
1097 match a b:
1098 case U64{x} U64{y}:
1099 U64{Word.sub(64n, x, y)}
1100
1101def U64.mul(a: U64, b: U64) -> U64:
1102 match a b:
1103 case U64{x} U64{y}:
1104 U64{Word.mul(64n, x, y)}
1105
1106def U64.and(a: U64, b: U64) -> U64:
1107 match a b:
1108 case U64{x} U64{y}:
1109 U64{Word.and(64n, x, y)}
1110
1111def U64.or(a: U64, b: U64) -> U64:
1112 match a b:
1113 case U64{x} U64{y}:
1114 U64{Word.or(64n, x, y)}
1115
1116def U64.xor(a: U64, b: U64) -> U64:
1117 match a b:
1118 case U64{x} U64{y}:
1119 U64{Word.xor(64n, x, y)}
1120
1121def U64.div(a: U64, b: U64) -> U64:
1122 match a b:
1123 case U64{x} U64{y}:
1124 U64{Int.div(64n, False{}, x, y)}
1125
1126def U64.mod(a: U64, b: U64) -> U64:
1127 match a b:
1128 case U64{x} U64{y}:
1129 U64{Int.mod(64n, False{}, x, y)}
1130
1131def U64.checked_add(a: U64, b: U64) -> Maybe<&2, U64>:
1132 match a b:
1133 case U64{x} U64{y}:
1134 U64.some(Int.checked(64n, Int.add_ov(64n, False{}, x, y)))
1135
1136def U64.checked_sub(a: U64, b: U64) -> Maybe<&2, U64>:
1137 match a b:
1138 case U64{x} U64{y}:
1139 U64.some(Int.checked(64n, Int.sub_ov(64n, False{}, x, y)))
1140
1141def U64.checked_mul(a: U64, b: U64) -> Maybe<&2, U64>:
1142 match a b:
1143 case U64{x} U64{y}:
1144 U64.some(Int.checked(64n, Int.mul_ov(64n, False{}, x, y)))
1145
1146def U64.checked_div(a: U64, b: U64) -> Maybe<&2, U64>:
1147 match a b:
1148 case U64{x} U64{y}:
1149 U64.some(Int.checked_div(64n, False{}, x, y))
1150
1151def U64.checked_mod(a: U64, b: U64) -> Maybe<&2, U64>:
1152 match a b:
1153 case U64{x} U64{y}:
1154 U64.some(Int.checked_mod(64n, False{}, x, y))
1155
1156def U64.saturating_add(a: U64, b: U64) -> U64:
1157 match a b:
1158 case U64{x} U64{y}:
1159 U64{Int.saturating_add(64n, False{}, x, y)}
1160
1161def U64.saturating_sub(a: U64, b: U64) -> U64:
1162 match a b:
1163 case U64{x} U64{y}:
1164 U64{Int.saturating_sub(64n, False{}, x, y)}
1165
1166def U64.saturating_mul(a: U64, b: U64) -> U64:
1167 match a b:
1168 case U64{x} U64{y}:
1169 U64{Int.saturating_mul(64n, False{}, x, y)}
1170
1171def U64.cmp(a: U64, b: U64) -> Cmp:
1172 match a b:
1173 case U64{x} U64{y}:
1174 Int.cmp(64n, False{}, x, y)
1175
1176def U64.is_eq(a: U64, b: U64) -> Bool:
1177 Cmp.is_eq(U64.cmp(a, b))
1178
1179def U64.is_lt(a: U64, b: U64) -> Bool:
1180 Cmp.is_lt(U64.cmp(a, b))
1181
1182def U64.is_le(a: U64, b: U64) -> Bool:
1183 Cmp.is_le(U64.cmp(a, b))
1184
1185def U64.is_gt(a: U64, b: U64) -> Bool:
1186 Cmp.is_gt(U64.cmp(a, b))
1187
1188def U64.is_ge(a: U64, b: U64) -> Bool:
1189 Cmp.is_ge(U64.cmp(a, b))
1190
1191def U64.is_ne(a: U64, b: U64) -> Bool:
1192 Bool.not(Cmp.is_eq(U64.cmp(a, b)))
1193
1194def U64.is_zero(a: U64) -> Bool:
1195 match a:
1196 case U64{x}:
1197 Int.is_zero(64n, x)
1198
1199def U64.not(a: U64) -> U64:
1200 match a:
1201 case U64{x}:
1202 U64{Word.not(64n, x)}
1203
1204def U64.shl(a: U64, k: Nat) -> U64:
1205 match a:
1206 case U64{x}:
1207 U64{Int.shl(64n, k, x)}
1208
1209def U64.shr(a: U64, k: Nat) -> U64:
1210 match a:
1211 case U64{x}:
1212 U64{Int.shr(64n, False{}, k, x)}
1213
1214def U64.show_radix(r: U32, a: U64) -> String:
1215 match a:
1216 case U64{x}:
1217 Int.show(64n, False{}, r, x)
1218
1219def U64.show(a: U64) -> String:
1220 U64.show_radix(10, a)
1221
1222def U64.read_radix(r: U32, s: String) -> Maybe<&2, U64>:
1223 U64.some(Int.read(64n, False{}, r, s))
1224
1225def U64.read(s: String) -> Maybe<&2, U64>:
1226 U64.read_radix(10, s)
1227
1228def U64.to_u32(a: U64) -> U32:
1229 match a:
1230 case U64{x}:
1231 U32{Int.ext(32n, 64n, False{}, x)}
1232
1233def U64.from_u32(a: U32) -> U64:
1234 match a:
1235 case U32{x}:
1236 U64{Int.ext(64n, 32n, False{}, x)}
1237
1238
1239def U64.to_nat(a: U64) -> Nat:
1240 match a:
1241 case U64{x}:
1242 Word.to_nat(64n, x)
1243
1244def U64.from_nat(k: Nat) -> U64:
1245 U64{Int.bits(64n, k)}
1246
1247type I32 is Data:
1248 I32{data: U32}
1249
1250def I32.some(m: Maybe<&2, U32>) -> Maybe<&2, I32>:
1251 match m:
1252 case None{}:
1253 None{}
1254 case Some{x}:
1255 Some{I32{x}}
1256
1257def I32.MIN() -> I32:
1258 I32{S32.MIN()}
1259
1260def I32.MAX() -> I32:
1261 I32{2147483647}
1262
1263def I32.add(a: I32, b: I32) -> I32:
1264 match a b:
1265 case I32{x} I32{y}:
1266 I32{U32.add(x, y)}
1267
1268def I32.sub(a: I32, b: I32) -> I32:
1269 match a b:
1270 case I32{x} I32{y}:
1271 I32{U32.sub(x, y)}
1272
1273def I32.mul(a: I32, b: I32) -> I32:
1274 match a b:
1275 case I32{x} I32{y}:
1276 I32{U32.mul(x, y)}
1277
1278def I32.and(a: I32, b: I32) -> I32:
1279 match a b:
1280 case I32{x} I32{y}:
1281 I32{U32.and(x, y)}
1282
1283def I32.or(a: I32, b: I32) -> I32:
1284 match a b:
1285 case I32{x} I32{y}:
1286 I32{U32.or(x, y)}
1287
1288def I32.xor(a: I32, b: I32) -> I32:
1289 match a b:
1290 case I32{x} I32{y}:
1291 I32{U32.xor(x, y)}
1292
1293def I32.div(a: I32, b: I32) -> I32:
1294 match a b:
1295 case I32{x} I32{y}:
1296 I32{S32.div(x, y)}
1297
1298def I32.mod(a: I32, b: I32) -> I32:
1299 match a b:
1300 case I32{x} I32{y}:
1301 I32{S32.mod(x, y)}
1302
1303def I32.checked_add(a: I32, b: I32) -> Maybe<&2, I32>:
1304 match a b:
1305 case I32{x} I32{y}:
1306 I32.some(S32.checked(S32.add_ov(x, y)))
1307
1308def I32.checked_sub(a: I32, b: I32) -> Maybe<&2, I32>:
1309 match a b:
1310 case I32{x} I32{y}:
1311 I32.some(S32.checked(S32.sub_ov(x, y)))
1312
1313def I32.checked_mul(a: I32, b: I32) -> Maybe<&2, I32>:
1314 match a b:
1315 case I32{x} I32{y}:
1316 I32.some(S32.checked(S32.mul_ov(x, y)))
1317
1318def I32.checked_div(a: I32, b: I32) -> Maybe<&2, I32>:
1319 match a b:
1320 case I32{x} I32{y}:
1321 I32.some(S32.checked_div(x, y))
1322
1323def I32.checked_mod(a: I32, b: I32) -> Maybe<&2, I32>:
1324 match a b:
1325 case I32{x} I32{y}:
1326 I32.some(S32.checked_mod(x, y))
1327
1328def I32.cmp(a: I32, b: I32) -> Cmp:
1329 match a b:
1330 case I32{x} I32{y}:
1331 S32.cmp(x, y)
1332
1333def I32.saturating_add(a: I32, b: I32) -> I32:
1334 match a b:
1335 case I32{x} I32{y}:
1336 +v = {x : U32}
1337 I32{S32.saturate(S32.is_neg(v), S32.add_ov(v, y))}
1338
1339def I32.saturating_sub(a: I32, b: I32) -> I32:
1340 match a b:
1341 case I32{x} I32{y}:
1342 +v = {x : U32}
1343 I32{S32.saturate(S32.is_neg(v), S32.sub_ov(v, y))}
1344
1345def I32.saturating_mul(a: I32, b: I32) -> I32:
1346 match a b:
1347 case I32{x} I32{y}:
1348 +v = {x : U32}
1349 +w = {y : U32}
1350 I32{S32.saturate(Bool.xor(S32.is_neg(v), S32.is_neg(w)), S32.mul_ov(v, w))}
1351
1352def I32.is_eq(a: I32, b: I32) -> Bool:
1353 Cmp.is_eq(I32.cmp(a, b))
1354
1355def I32.is_lt(a: I32, b: I32) -> Bool:
1356 Cmp.is_lt(I32.cmp(a, b))
1357
1358def I32.is_le(a: I32, b: I32) -> Bool:
1359 Cmp.is_le(I32.cmp(a, b))
1360
1361def I32.is_gt(a: I32, b: I32) -> Bool:
1362 Cmp.is_gt(I32.cmp(a, b))
1363
1364def I32.is_ge(a: I32, b: I32) -> Bool:
1365 Cmp.is_ge(I32.cmp(a, b))
1366
1367def I32.is_ne(a: I32, b: I32) -> Bool:
1368 Bool.not(Cmp.is_eq(I32.cmp(a, b)))
1369
1370def I32.is_zero(a: I32) -> Bool:
1371 match a:
1372 case I32{x}:
1373 U32.is_zero(x)
1374
1375def I32.not(a: I32) -> I32:
1376 match a:
1377 case I32{x}:
1378 I32{U32.not(x)}
1379
1380def I32.shl(a: I32, k: Nat) -> I32:
1381 match a:
1382 case I32{x}:
1383 I32{U32.shln(x, k)}
1384
1385def I32.shr(a: I32, k: Nat) -> I32:
1386 match a:
1387 case I32{x}:
1388 +v = {x : U32}
1389 I32{S32.shr.if(S32.is_neg(v), v, k)}
1390
1391def I32.neg(a: I32) -> I32:
1392 match a:
1393 case I32{x}:
1394 I32{S32.neg(x)}
1395
1396def I32.abs(a: I32) -> I32:
1397 match a:
1398 case I32{x}:
1399 I32{S32.abs(x)}
1400
1401def I32.is_neg(a: I32) -> Bool:
1402 match a:
1403 case I32{x}:
1404 S32.is_neg(x)
1405
1406def I32.show_radix(r: U32, a: I32) -> String:
1407 match a:
1408 case I32{x}:
1409 +v = {x : U32}
1410 S32.show.if(S32.is_neg(v), r, v)
1411
1412def I32.show(a: I32) -> String:
1413 I32.show_radix(10, a)
1414
1415def I32.read_radix(r: U32, s: String) -> Maybe<&2, I32>:
1416 I32.some(S32.read(r, s))
1417
1418def I32.read(s: String) -> Maybe<&2, I32>:
1419 I32.read_radix(10, s)
1420
1421def I32.to_u32(a: I32) -> U32:
1422 match a:
1423 case I32{x}:
1424 x
1425
1426def I32.from_u32(a: U32) -> I32:
1427 I32{a}
1428
1429def I32.to_nat(a: I32) -> Maybe<&2, Nat>:
1430 match a:
1431 case I32{x}:
1432 +v = {x : U32}
1433 S32.to_nat.if(S32.is_neg(v), v)
1434
1435def I32.from_nat(k: Nat) -> I32:
1436 I32{U32.from_nat(k)}
1437
1438
1439
1440type I64 is Data:
1441 I64{data: Word(64n)}
1442
1443def I64.some(m: Maybe<&2, Word(64n)>) -> Maybe<&2, I64>:
1444 match m:
1445 case None{}:
1446 None{}
1447 case Some{x}:
1448 Some{I64{x}}
1449
1450def I64.MIN() -> I64:
1451 I64{Int.min(64n, True{})}
1452
1453def I64.MAX() -> I64:
1454 I64{Int.max(64n, True{})}
1455
1456def I64.add(a: I64, b: I64) -> I64:
1457 match a b:
1458 case I64{x} I64{y}:
1459 I64{Word.add(64n, x, y)}
1460
1461def I64.sub(a: I64, b: I64) -> I64:
1462 match a b:
1463 case I64{x} I64{y}:
1464 I64{Word.sub(64n, x, y)}
1465
1466def I64.mul(a: I64, b: I64) -> I64:
1467 match a b:
1468 case I64{x} I64{y}:
1469 I64{Word.mul(64n, x, y)}
1470
1471def I64.and(a: I64, b: I64) -> I64:
1472 match a b:
1473 case I64{x} I64{y}:
1474 I64{Word.and(64n, x, y)}
1475
1476def I64.or(a: I64, b: I64) -> I64:
1477 match a b:
1478 case I64{x} I64{y}:
1479 I64{Word.or(64n, x, y)}
1480
1481def I64.xor(a: I64, b: I64) -> I64:
1482 match a b:
1483 case I64{x} I64{y}:
1484 I64{Word.xor(64n, x, y)}
1485
1486def I64.div(a: I64, b: I64) -> I64:
1487 match a b:
1488 case I64{x} I64{y}:
1489 I64{Int.div(64n, True{}, x, y)}
1490
1491def I64.mod(a: I64, b: I64) -> I64:
1492 match a b:
1493 case I64{x} I64{y}:
1494 I64{Int.mod(64n, True{}, x, y)}
1495
1496def I64.checked_add(a: I64, b: I64) -> Maybe<&2, I64>:
1497 match a b:
1498 case I64{x} I64{y}:
1499 I64.some(Int.checked(64n, Int.add_ov(64n, True{}, x, y)))
1500
1501def I64.checked_sub(a: I64, b: I64) -> Maybe<&2, I64>:
1502 match a b:
1503 case I64{x} I64{y}:
1504 I64.some(Int.checked(64n, Int.sub_ov(64n, True{}, x, y)))
1505
1506def I64.checked_mul(a: I64, b: I64) -> Maybe<&2, I64>:
1507 match a b:
1508 case I64{x} I64{y}:
1509 I64.some(Int.checked(64n, Int.mul_ov(64n, True{}, x, y)))
1510
1511def I64.checked_div(a: I64, b: I64) -> Maybe<&2, I64>:
1512 match a b:
1513 case I64{x} I64{y}:
1514 I64.some(Int.checked_div(64n, True{}, x, y))
1515
1516def I64.checked_mod(a: I64, b: I64) -> Maybe<&2, I64>:
1517 match a b:
1518 case I64{x} I64{y}:
1519 I64.some(Int.checked_mod(64n, True{}, x, y))
1520
1521def I64.saturating_add(a: I64, b: I64) -> I64:
1522 match a b:
1523 case I64{x} I64{y}:
1524 I64{Int.saturating_add(64n, True{}, x, y)}
1525
1526def I64.saturating_sub(a: I64, b: I64) -> I64:
1527 match a b:
1528 case I64{x} I64{y}:
1529 I64{Int.saturating_sub(64n, True{}, x, y)}
1530
1531def I64.saturating_mul(a: I64, b: I64) -> I64:
1532 match a b:
1533 case I64{x} I64{y}:
1534 I64{Int.saturating_mul(64n, True{}, x, y)}
1535
1536def I64.cmp(a: I64, b: I64) -> Cmp:
1537 match a b:
1538 case I64{x} I64{y}:
1539 Int.cmp(64n, True{}, x, y)
1540
1541def I64.is_eq(a: I64, b: I64) -> Bool:
1542 Cmp.is_eq(I64.cmp(a, b))
1543
1544def I64.is_lt(a: I64, b: I64) -> Bool:
1545 Cmp.is_lt(I64.cmp(a, b))
1546
1547def I64.is_le(a: I64, b: I64) -> Bool:
1548 Cmp.is_le(I64.cmp(a, b))
1549
1550def I64.is_gt(a: I64, b: I64) -> Bool:
1551 Cmp.is_gt(I64.cmp(a, b))
1552
1553def I64.is_ge(a: I64, b: I64) -> Bool:
1554 Cmp.is_ge(I64.cmp(a, b))
1555
1556def I64.is_ne(a: I64, b: I64) -> Bool:
1557 Bool.not(Cmp.is_eq(I64.cmp(a, b)))
1558
1559def I64.is_zero(a: I64) -> Bool:
1560 match a:
1561 case I64{x}:
1562 Int.is_zero(64n, x)
1563
1564def I64.not(a: I64) -> I64:
1565 match a:
1566 case I64{x}:
1567 I64{Word.not(64n, x)}
1568
1569def I64.shl(a: I64, k: Nat) -> I64:
1570 match a:
1571 case I64{x}:
1572 I64{Int.shl(64n, k, x)}
1573
1574def I64.shr(a: I64, k: Nat) -> I64:
1575 match a:
1576 case I64{x}:
1577 I64{Int.shr(64n, True{}, k, x)}
1578
1579def I64.neg(a: I64) -> I64:
1580 match a:
1581 case I64{x}:
1582 I64{Int.neg(64n, x)}
1583
1584def I64.abs(a: I64) -> I64:
1585 match a:
1586 case I64{x}:
1587 I64{Int.abs(64n, x)}
1588
1589def I64.is_neg(a: I64) -> Bool:
1590 match a:
1591 case I64{x}:
1592 Int.msb(64n, x)
1593
1594def I64.show_radix(r: U32, a: I64) -> String:
1595 match a:
1596 case I64{x}:
1597 Int.show(64n, True{}, r, x)
1598
1599def I64.show(a: I64) -> String:
1600 I64.show_radix(10, a)
1601
1602def I64.read_radix(r: U32, s: String) -> Maybe<&2, I64>:
1603 I64.some(Int.read(64n, True{}, r, s))
1604
1605def I64.read(s: String) -> Maybe<&2, I64>:
1606 I64.read_radix(10, s)
1607
1608def I64.to_u32(a: I64) -> U32:
1609 match a:
1610 case I64{x}:
1611 U32{Int.sext(32n, 64n, x)}
1612
1613def I64.from_u32(a: U32) -> I64:
1614 match a:
1615 case U32{x}:
1616 I64{Int.ext(64n, 32n, False{}, x)}
1617
1618def I64.to_nat(a: I64) -> Maybe<&2, Nat>:
1619 match a:
1620 case I64{x}:
1621 Int.to_nat(64n, x)
1622
1623def I64.from_nat(k: Nat) -> I64:
1624 I64{Int.bits(64n, k)}