1	# Fixed-width integers U8, U16, U64, I32 and I64: wrapping, checked and saturating arithmetic.
2	import Base
3	
4	# The Int.* core serves only U64 and I64. When Base ships a native U64 (bendlang/bend#1027), delete it.
5	def 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.
14	def Int.bits(n: Nat, k: Nat) -> Word(n):
15	  Int.bits.go(n, Nat.divmod(k, 2n))
16	
17	def 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	
26	def Int.msb(n: Nat, w: Word(n)) -> Bool:
27	  Int.msb.go(n, False{}, w)
28	
29	def 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	
36	def 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	
45	def 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	
58	def Int.ones(+n: Nat) -> Word(n):
59	  Word.not(n, Word.zero(n))
60	
61	def 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	
68	def 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	
75	def Int.is_eq(+n: Nat, a: Word(n), b: Word(n)) -> Bool:
76	  Cmp.is_eq(Word.cmp(n, a, b))
77	
78	def Int.is_zero(+n: Nat, w: Word(n)) -> Bool:
79	  Int.is_eq(n, w, Word.zero(n))
80	
81	def 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	
89	def Int.neg(+n: Nat, w: Word(n)) -> Word(n):
90	  Word.sub(n, Word.zero(n), w)
91	
92	def 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	
99	def Int.abs(+n: Nat, +w: Word(n)) -> Word(n):
100	  Int.neg_if(n, Int.msb(n, w), w)
101	
102	def 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	
110	def 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	
116	def 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	
121	def 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	
129	def 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.
135	def 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	
148	def 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	
152	def Int.fst(-n: Nat, p: Word(n) & Word(n)) -> Word(n):
153	  (q, r) = p
154	  q
155	
156	def Int.snd(-n: Nat, p: Word(n) & Word(n)) -> Word(n):
157	  (q, r) = p
158	  r
159	
160	def 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	
163	def 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.
167	def 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	
175	def 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	
178	def 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	
186	def 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	
189	def 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	
197	def 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	
200	def 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	
206	def 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	
209	def 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	
217	def 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	
221	def 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	
225	def 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	
232	def 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	
240	def 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	
243	def 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	
247	def 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	
252	def 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.
260	def 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	
267	def 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.
275	def 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	
291	def 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	
294	def 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	
301	def 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	
308	def 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	
316	def 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	
325	def 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	
334	def 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	
342	def 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	
349	def 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	
356	def 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	
364	def 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	
373	def 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	
380	def 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	
392	def 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.
400	def Int.to_nat(+n: Nat, +w: Word(n)) -> Maybe<&2, Nat>:
401	  Int.to_nat.s(Int.msb(n, w), n, w)
402	
403	def 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.
407	def Nar.opt(ov: Bool, r: U32) -> Maybe<&2, U32>:
408	  match ov:
409	    case True{}:
410	      None{}
411	    case False{}:
412	      Some{r}
413	
414	def Nar.over(+m: U32, +r: U32) -> Maybe<&2, U32>:
415	  Nar.opt(U32.is_gt(r, m), r)
416	
417	def Nar.checked_sub(+a: U32, +b: U32) -> Maybe<&2, U32>:
418	  Nar.opt(U32.is_lt(a, b), U32.sub(a, b))
419	
420	def Nar.checked_div(a: U32, +b: U32) -> Maybe<&2, U32>:
421	  Nar.opt(U32.is_zero(b), U32.div(a, b))
422	
423	def Nar.checked_mod(a: U32, +b: U32) -> Maybe<&2, U32>:
424	  Nar.opt(U32.is_zero(b), U32.mod(a, b))
425	
426	def 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	
433	def Nar.saturating_sub(+a: U32, +b: U32) -> U32:
434	  Nar.sat_sub(U32.is_lt(a, b), a, b)
435	
436	def 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.
445	def S32.MIN() -> U32:
446	  2147483648
447	
448	def S32.is_neg(x: U32) -> Bool:
449	  U32.is_ge(x, S32.MIN())
450	
451	def S32.neg(x: U32) -> U32:
452	  U32.sub(0, x)
453	
454	def S32.neg_if(c: Bool, x: U32) -> U32:
455	  match c:
456	    case True{}:
457	      S32.neg(x)
458	    case False{}:
459	      x
460	
461	def S32.abs(+x: U32) -> U32:
462	  S32.neg_if(S32.is_neg(x), x)
463	
464	def 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.
468	def 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	
477	def S32.fst(p: U32 & U32) -> U32:
478	  (q, r) = p
479	  q
480	
481	def S32.snd(p: U32 & U32) -> U32:
482	  (q, r) = p
483	  r
484	
485	def S32.div(a: U32, +b: U32) -> U32:
486	  S32.fst(S32.divmod.if(U32.is_zero(b), a, b))
487	
488	def 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.
492	def S32.min_neg1(a: U32, b: U32) -> Bool:
493	  Bool.and(U32.is_eq(a, S32.MIN()), U32.is_eq(b, 4294967295))
494	
495	def S32.div_ov(+a: U32, +b: U32) -> Bool:
496	  Bool.or(U32.is_zero(b), S32.min_neg1(a, b))
497	
498	def 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	
501	def S32.add_ov(+a: U32, +b: U32) -> Bool & U32:
502	  S32.add_ov.go(a, b, U32.add(a, b))
503	
504	def 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	
507	def S32.sub_ov(+a: U32, +b: U32) -> Bool & U32:
508	  S32.sub_ov.go(a, b, U32.sub(a, b))
509	
510	def 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	
514	def S32.mul_ov(+a: U32, +b: U32) -> Bool & U32:
515	  S32.mul_ov.go(a, b, U32.mul(a, b))
516	
517	def S32.checked(o: Bool & U32) -> Maybe<&2, U32>:
518	  (ov, r) = o
519	  Nar.opt(ov, r)
520	
521	def S32.checked_div(+a: U32, +b: U32) -> Maybe<&2, U32>:
522	  Nar.opt(S32.div_ov(a, b), S32.div(a, b))
523	
524	def S32.checked_mod(+a: U32, +b: U32) -> Maybe<&2, U32>:
525	  Nar.opt(S32.div_ov(a, b), S32.mod(a, b))
526	
527	def S32.sat(low: Bool) -> U32:
528	  match low:
529	    case True{}:
530	      S32.MIN()
531	    case False{}:
532	      2147483647
533	
534	def 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.
543	def 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	
550	def 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	
557	def 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	
565	def 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	
573	def 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	
580	def 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	
588	def 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	
595	type U8 is Data:
596	  U8{data: U32}
597	
598	def 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	
605	def U8.MIN() -> U8:
606	  U8{0}
607	
608	def U8.MAX() -> U8:
609	  U8{255}
610	
611	def 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	
616	def 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	
621	def 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	
626	def U8.and(a: U8, b: U8) -> U8:
627	  match a b:
628	    case U8{x} U8{y}:
629	      U8{U32.and(x, y)}
630	
631	def U8.or(a: U8, b: U8) -> U8:
632	  match a b:
633	    case U8{x} U8{y}:
634	      U8{U32.or(x, y)}
635	
636	def U8.xor(a: U8, b: U8) -> U8:
637	  match a b:
638	    case U8{x} U8{y}:
639	      U8{U32.xor(x, y)}
640	
641	def U8.div(a: U8, b: U8) -> U8:
642	  match a b:
643	    case U8{x} U8{y}:
644	      U8{U32.div(x, y)}
645	
646	def U8.mod(a: U8, b: U8) -> U8:
647	  match a b:
648	    case U8{x} U8{y}:
649	      U8{U32.mod(x, y)}
650	
651	def 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	
656	def 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	
661	def 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	
666	def 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	
671	def 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	
676	def 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	
681	def 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	
686	def 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	
691	def U8.cmp(a: U8, b: U8) -> Cmp:
692	  match a b:
693	    case U8{x} U8{y}:
694	      U32.cmp(x, y)
695	
696	def U8.is_eq(a: U8, b: U8) -> Bool:
697	  Cmp.is_eq(U8.cmp(a, b))
698	
699	def U8.is_lt(a: U8, b: U8) -> Bool:
700	  Cmp.is_lt(U8.cmp(a, b))
701	
702	def U8.is_le(a: U8, b: U8) -> Bool:
703	  Cmp.is_le(U8.cmp(a, b))
704	
705	def U8.is_gt(a: U8, b: U8) -> Bool:
706	  Cmp.is_gt(U8.cmp(a, b))
707	
708	def U8.is_ge(a: U8, b: U8) -> Bool:
709	  Cmp.is_ge(U8.cmp(a, b))
710	
711	def U8.is_ne(a: U8, b: U8) -> Bool:
712	  Bool.not(Cmp.is_eq(U8.cmp(a, b)))
713	
714	def U8.is_zero(a: U8) -> Bool:
715	  match a:
716	    case U8{x}:
717	      U32.is_zero(x)
718	
719	def U8.not(a: U8) -> U8:
720	  match a:
721	    case U8{x}:
722	      U8{U32.xor(x, 255)}
723	
724	def U8.shl(a: U8, k: Nat) -> U8:
725	  match a:
726	    case U8{x}:
727	      U8{U32.and(U32.shln(x, k), 255)}
728	
729	def U8.shr(a: U8, k: Nat) -> U8:
730	  match a:
731	    case U8{x}:
732	      U8{U32.shrn(x, k)}
733	
734	def U8.show(a: U8) -> String:
735	  match a:
736	    case U8{x}:
737	      U32.show(x)
738	
739	def U8.read(s: String) -> Maybe<&2, U8>:
740	  U8.some(Nar.read(255, U32.read(s)))
741	
742	def U8.to_u32(a: U8) -> U32:
743	  match a:
744	    case U8{x}:
745	      x
746	
747	def U8.from_u32(a: U32) -> U8:
748	  U8{U32.and(a, 255)}
749	
750	def U8.to_nat(a: U8) -> Nat:
751	  match a:
752	    case U8{x}:
753	      U32.to_nat(x)
754	
755	def U8.from_nat(k: Nat) -> U8:
756	  U8{U32.and(U32.from_nat(k), 255)}
757	
758	type U16 is Data:
759	  U16{data: U32}
760	
761	def 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	
768	def U16.MIN() -> U16:
769	  U16{0}
770	
771	def U16.MAX() -> U16:
772	  U16{65535}
773	
774	def 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	
779	def 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	
784	def 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	
789	def U16.and(a: U16, b: U16) -> U16:
790	  match a b:
791	    case U16{x} U16{y}:
792	      U16{U32.and(x, y)}
793	
794	def U16.or(a: U16, b: U16) -> U16:
795	  match a b:
796	    case U16{x} U16{y}:
797	      U16{U32.or(x, y)}
798	
799	def U16.xor(a: U16, b: U16) -> U16:
800	  match a b:
801	    case U16{x} U16{y}:
802	      U16{U32.xor(x, y)}
803	
804	def U16.div(a: U16, b: U16) -> U16:
805	  match a b:
806	    case U16{x} U16{y}:
807	      U16{U32.div(x, y)}
808	
809	def U16.mod(a: U16, b: U16) -> U16:
810	  match a b:
811	    case U16{x} U16{y}:
812	      U16{U32.mod(x, y)}
813	
814	def 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	
819	def 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	
824	def 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	
829	def 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	
834	def 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	
839	def 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	
844	def 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	
849	def 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	
854	def U16.cmp(a: U16, b: U16) -> Cmp:
855	  match a b:
856	    case U16{x} U16{y}:
857	      U32.cmp(x, y)
858	
859	def U16.is_eq(a: U16, b: U16) -> Bool:
860	  Cmp.is_eq(U16.cmp(a, b))
861	
862	def U16.is_lt(a: U16, b: U16) -> Bool:
863	  Cmp.is_lt(U16.cmp(a, b))
864	
865	def U16.is_le(a: U16, b: U16) -> Bool:
866	  Cmp.is_le(U16.cmp(a, b))
867	
868	def U16.is_gt(a: U16, b: U16) -> Bool:
869	  Cmp.is_gt(U16.cmp(a, b))
870	
871	def U16.is_ge(a: U16, b: U16) -> Bool:
872	  Cmp.is_ge(U16.cmp(a, b))
873	
874	def U16.is_ne(a: U16, b: U16) -> Bool:
875	  Bool.not(Cmp.is_eq(U16.cmp(a, b)))
876	
877	def U16.is_zero(a: U16) -> Bool:
878	  match a:
879	    case U16{x}:
880	      U32.is_zero(x)
881	
882	def U16.not(a: U16) -> U16:
883	  match a:
884	    case U16{x}:
885	      U16{U32.xor(x, 65535)}
886	
887	def U16.shl(a: U16, k: Nat) -> U16:
888	  match a:
889	    case U16{x}:
890	      U16{U32.and(U32.shln(x, k), 65535)}
891	
892	def U16.shr(a: U16, k: Nat) -> U16:
893	  match a:
894	    case U16{x}:
895	      U16{U32.shrn(x, k)}
896	
897	def U16.show(a: U16) -> String:
898	  match a:
899	    case U16{x}:
900	      U32.show(x)
901	
902	def U16.read(s: String) -> Maybe<&2, U16>:
903	  U16.some(Nar.read(65535, U32.read(s)))
904	
905	def U16.to_u32(a: U16) -> U32:
906	  match a:
907	    case U16{x}:
908	      x
909	
910	def U16.from_u32(a: U32) -> U16:
911	  U16{U32.and(a, 65535)}
912	
913	def U16.to_nat(a: U16) -> Nat:
914	  match a:
915	    case U16{x}:
916	      U32.to_nat(x)
917	
918	def 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.
923	type U64 is Data:
924	  U64{data: Word(64n)}
925	
926	def 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	
933	def U64.MIN() -> U64:
934	  U64{Int.min(64n, False{})}
935	
936	def U64.MAX() -> U64:
937	  U64{Int.max(64n, False{})}
938	
939	def 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	
944	def 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	
949	def 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	
954	def 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	
959	def 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	
964	def 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	
969	def 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	
974	def 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	
979	def 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	
984	def 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	
989	def 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	
994	def 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	
999	def 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	
1004	def 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	
1009	def 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	
1014	def 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	
1019	def 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	
1024	def U64.is_eq(a: U64, b: U64) -> Bool:
1025	  Cmp.is_eq(U64.cmp(a, b))
1026	
1027	def U64.is_lt(a: U64, b: U64) -> Bool:
1028	  Cmp.is_lt(U64.cmp(a, b))
1029	
1030	def U64.is_le(a: U64, b: U64) -> Bool:
1031	  Cmp.is_le(U64.cmp(a, b))
1032	
1033	def U64.is_gt(a: U64, b: U64) -> Bool:
1034	  Cmp.is_gt(U64.cmp(a, b))
1035	
1036	def U64.is_ge(a: U64, b: U64) -> Bool:
1037	  Cmp.is_ge(U64.cmp(a, b))
1038	
1039	def U64.is_ne(a: U64, b: U64) -> Bool:
1040	  Bool.not(Cmp.is_eq(U64.cmp(a, b)))
1041	
1042	def U64.is_zero(a: U64) -> Bool:
1043	  match a:
1044	    case U64{x}:
1045	      Int.is_zero(64n, x)
1046	
1047	def U64.not(a: U64) -> U64:
1048	  match a:
1049	    case U64{x}:
1050	      U64{Word.not(64n, x)}
1051	
1052	def U64.shl(a: U64, k: Nat) -> U64:
1053	  match a:
1054	    case U64{x}:
1055	      U64{Int.shl(64n, k, x)}
1056	
1057	def U64.shr(a: U64, k: Nat) -> U64:
1058	  match a:
1059	    case U64{x}:
1060	      U64{Int.shr(64n, False{}, k, x)}
1061	
1062	def U64.show(a: U64) -> String:
1063	  match a:
1064	    case U64{x}:
1065	      Int.show(64n, False{}, x)
1066	
1067	def U64.read(s: String) -> Maybe<&2, U64>:
1068	  U64.some(Int.read(64n, False{}, s))
1069	
1070	def U64.to_u32(a: U64) -> U32:
1071	  match a:
1072	    case U64{x}:
1073	      U32{Int.ext(32n, 64n, False{}, x)}
1074	
1075	def 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.
1081	def U64.to_nat(a: U64) -> Nat:
1082	  match a:
1083	    case U64{x}:
1084	      Word.to_nat(64n, x)
1085	
1086	def U64.from_nat(k: Nat) -> U64:
1087	  U64{Int.bits(64n, k)}
1088	
1089	type I32 is Data:
1090	  I32{data: U32}
1091	
1092	def 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	
1099	def I32.MIN() -> I32:
1100	  I32{S32.MIN()}
1101	
1102	def I32.MAX() -> I32:
1103	  I32{2147483647}
1104	
1105	def I32.add(a: I32, b: I32) -> I32:
1106	  match a b:
1107	    case I32{x} I32{y}:
1108	      I32{U32.add(x, y)}
1109	
1110	def I32.sub(a: I32, b: I32) -> I32:
1111	  match a b:
1112	    case I32{x} I32{y}:
1113	      I32{U32.sub(x, y)}
1114	
1115	def I32.mul(a: I32, b: I32) -> I32:
1116	  match a b:
1117	    case I32{x} I32{y}:
1118	      I32{U32.mul(x, y)}
1119	
1120	def I32.and(a: I32, b: I32) -> I32:
1121	  match a b:
1122	    case I32{x} I32{y}:
1123	      I32{U32.and(x, y)}
1124	
1125	def I32.or(a: I32, b: I32) -> I32:
1126	  match a b:
1127	    case I32{x} I32{y}:
1128	      I32{U32.or(x, y)}
1129	
1130	def I32.xor(a: I32, b: I32) -> I32:
1131	  match a b:
1132	    case I32{x} I32{y}:
1133	      I32{U32.xor(x, y)}
1134	
1135	def I32.div(a: I32, b: I32) -> I32:
1136	  match a b:
1137	    case I32{x} I32{y}:
1138	      I32{S32.div(x, y)}
1139	
1140	def I32.mod(a: I32, b: I32) -> I32:
1141	  match a b:
1142	    case I32{x} I32{y}:
1143	      I32{S32.mod(x, y)}
1144	
1145	def 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	
1150	def 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	
1155	def 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	
1160	def 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	
1165	def 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	
1170	def I32.cmp(a: I32, b: I32) -> Cmp:
1171	  match a b:
1172	    case I32{x} I32{y}:
1173	      S32.cmp(x, y)
1174	
1175	def 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	
1181	def 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	
1187	def 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	
1194	def I32.is_eq(a: I32, b: I32) -> Bool:
1195	  Cmp.is_eq(I32.cmp(a, b))
1196	
1197	def I32.is_lt(a: I32, b: I32) -> Bool:
1198	  Cmp.is_lt(I32.cmp(a, b))
1199	
1200	def I32.is_le(a: I32, b: I32) -> Bool:
1201	  Cmp.is_le(I32.cmp(a, b))
1202	
1203	def I32.is_gt(a: I32, b: I32) -> Bool:
1204	  Cmp.is_gt(I32.cmp(a, b))
1205	
1206	def I32.is_ge(a: I32, b: I32) -> Bool:
1207	  Cmp.is_ge(I32.cmp(a, b))
1208	
1209	def I32.is_ne(a: I32, b: I32) -> Bool:
1210	  Bool.not(Cmp.is_eq(I32.cmp(a, b)))
1211	
1212	def I32.is_zero(a: I32) -> Bool:
1213	  match a:
1214	    case I32{x}:
1215	      U32.is_zero(x)
1216	
1217	def I32.not(a: I32) -> I32:
1218	  match a:
1219	    case I32{x}:
1220	      I32{U32.not(x)}
1221	
1222	def I32.shl(a: I32, k: Nat) -> I32:
1223	  match a:
1224	    case I32{x}:
1225	      I32{U32.shln(x, k)}
1226	
1227	def 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	
1233	def I32.neg(a: I32) -> I32:
1234	  match a:
1235	    case I32{x}:
1236	      I32{S32.neg(x)}
1237	
1238	def I32.abs(a: I32) -> I32:
1239	  match a:
1240	    case I32{x}:
1241	      I32{S32.abs(x)}
1242	
1243	def I32.is_neg(a: I32) -> Bool:
1244	  match a:
1245	    case I32{x}:
1246	      S32.is_neg(x)
1247	
1248	def 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	
1254	def I32.read(s: String) -> Maybe<&2, I32>:
1255	  I32.some(S32.read(s))
1256	
1257	def I32.to_u32(a: I32) -> U32:
1258	  match a:
1259	    case I32{x}:
1260	      x
1261	
1262	def I32.from_u32(a: U32) -> I32:
1263	  I32{a}
1264	
1265	def 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	
1271	def 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.
1276	type I64 is Data:
1277	  I64{data: Word(64n)}
1278	
1279	def 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	
1286	def I64.MIN() -> I64:
1287	  I64{Int.min(64n, True{})}
1288	
1289	def I64.MAX() -> I64:
1290	  I64{Int.max(64n, True{})}
1291	
1292	def 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	
1297	def 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	
1302	def 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	
1307	def 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	
1312	def 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	
1317	def 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	
1322	def 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	
1327	def 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	
1332	def 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	
1337	def 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	
1342	def 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	
1347	def 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	
1352	def 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	
1357	def 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	
1362	def 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	
1367	def 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	
1372	def 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	
1377	def I64.is_eq(a: I64, b: I64) -> Bool:
1378	  Cmp.is_eq(I64.cmp(a, b))
1379	
1380	def I64.is_lt(a: I64, b: I64) -> Bool:
1381	  Cmp.is_lt(I64.cmp(a, b))
1382	
1383	def I64.is_le(a: I64, b: I64) -> Bool:
1384	  Cmp.is_le(I64.cmp(a, b))
1385	
1386	def I64.is_gt(a: I64, b: I64) -> Bool:
1387	  Cmp.is_gt(I64.cmp(a, b))
1388	
1389	def I64.is_ge(a: I64, b: I64) -> Bool:
1390	  Cmp.is_ge(I64.cmp(a, b))
1391	
1392	def I64.is_ne(a: I64, b: I64) -> Bool:
1393	  Bool.not(Cmp.is_eq(I64.cmp(a, b)))
1394	
1395	def I64.is_zero(a: I64) -> Bool:
1396	  match a:
1397	    case I64{x}:
1398	      Int.is_zero(64n, x)
1399	
1400	def I64.not(a: I64) -> I64:
1401	  match a:
1402	    case I64{x}:
1403	      I64{Word.not(64n, x)}
1404	
1405	def I64.shl(a: I64, k: Nat) -> I64:
1406	  match a:
1407	    case I64{x}:
1408	      I64{Int.shl(64n, k, x)}
1409	
1410	def I64.shr(a: I64, k: Nat) -> I64:
1411	  match a:
1412	    case I64{x}:
1413	      I64{Int.shr(64n, True{}, k, x)}
1414	
1415	def I64.neg(a: I64) -> I64:
1416	  match a:
1417	    case I64{x}:
1418	      I64{Int.neg(64n, x)}
1419	
1420	def I64.abs(a: I64) -> I64:
1421	  match a:
1422	    case I64{x}:
1423	      I64{Int.abs(64n, x)}
1424	
1425	def I64.is_neg(a: I64) -> Bool:
1426	  match a:
1427	    case I64{x}:
1428	      Int.msb(64n, x)
1429	
1430	def I64.show(a: I64) -> String:
1431	  match a:
1432	    case I64{x}:
1433	      Int.show(64n, True{}, x)
1434	
1435	def I64.read(s: String) -> Maybe<&2, I64>:
1436	  I64.some(Int.read(64n, True{}, s))
1437	
1438	def I64.to_u32(a: I64) -> U32:
1439	  match a:
1440	    case I64{x}:
1441	      U32{Int.sext(32n, 64n, x)}
1442	
1443	def I64.from_u32(a: U32) -> I64:
1444	  match a:
1445	    case U32{x}:
1446	      I64{Int.ext(64n, 32n, False{}, x)}
1447	
1448	def I64.to_nat(a: I64) -> Maybe<&2, Nat>:
1449	  match a:
1450	    case I64{x}:
1451	      Int.to_nat(64n, x)
1452	
1453	def I64.from_nat(k: Nat) -> I64:
1454	  I64{Int.bits(64n, k)}