1	# IEEE 754 binary64 add, sub, mul, and div. Source: https://github.com/paymog/bend-kit/tree/main/f64
2	import Base
3	
4	# ponytail: two U32 halves, not Int.U64. Word(64n) is 64 bools and blows the C word limit. Replace these limbs with Base F64 when bendlang/bend#1120 lands.
5	# A NaN operand becomes one quiet NaN. Payloads are not kept. Rounding is ties to even.
6	# exp below is the IEEE biased exponent plus 4096, so a U32 never goes negative.
7	
8	type W2 is Data:
9	  W2{hi: U32, lo: U32}
10	
11	type W4 is Data:
12	  W4{a: U32, b: U32, c: U32, d: U32}
13	
14	type Limb is Data:
15	  Limb{s: U32, c: U32}
16	
17	type Step is Data:
18	  Step{rem: W2, q: W4}
19	
20	type Cls is Data:
21	  Fin{}
22	  Inf{}
23	  Nan{}
24	
25	type Parts is Data:
26	  Parts{kind: Cls, sign: U32, exp: U32, sig: W2}
27	
28	type Norm is Data:
29	  Norm{sign: U32, exp: U32, w: W4, sticky: Bool}
30	
31	type F64 is Data:
32	  F64{hi: U32, lo: U32}
33	
34	def u01(b: Bool) -> U32:
35	  match b:
36	    case True{}:
37	      1
38	    case False{}:
39	      0
40	
41	def clz.go(k: Nat, z: Bool, n: U32, +x: U32) -> U32:
42	  match k z:
43	    case 0n _:
44	      n
45	    case 1n+p False{}:
46	      n
47	    case 1n+p True{}:
48	      clz.go(p, U32.is_zero(((x << 1n) .&. 2147483648 : U32)), (n + 1 : U32), (x << 1n : U32))
49	
50	def clz(+x: U32) -> U32:
51	  clz.go(32n, U32.is_zero((x .&. 2147483648 : U32)), 0, x)
52	
53	def F64.nan() -> F64:
54	  F64{2146959360, 0}
55	
56	def F64.inf.pos(pos: Bool) -> F64:
57	  match pos:
58	    case True{}:
59	      F64{2146435072, 0}
60	    case False{}:
61	      F64{4293918720, 0}
62	
63	def F64.inf.sign(sign: U32) -> F64:
64	  F64.inf.pos(U32.is_zero(sign))
65	
66	def F64.zero.sign(sign: U32) -> F64:
67	  F64{(sign << 31n : U32), 0}
68	
69	def F64.pack(sign: U32, exp: U32, sh: U32, sl: U32) -> F64:
70	  F64{((sign << 31n) .|. (exp << 20n) .|. (sh .&. 1048575) : U32), sl}
71	
72	def F64.hi(a: F64) -> U32:
73	  match a:
74	    case F64{hi, lo}:
75	      hi
76	
77	def F64.lo(a: F64) -> U32:
78	  match a:
79	    case F64{hi, lo}:
80	      lo
81	
82	def W2.nz(w: W2) -> Bool:
83	  match w:
84	    case W2{hi, lo}:
85	      Bool.not(Bool.and(U32.is_zero(hi), U32.is_zero(lo)))
86	
87	def W2.bit.at(low: Bool, n: U32, hi: U32, lo: U32) -> U32:
88	  match low:
89	    case True{}:
90	      ((lo >> U32.to_nat(n)) .&. 1 : U32)
91	    case False{}:
92	      ((hi >> U32.to_nat((n - 32 : U32))) .&. 1 : U32)
93	
94	def W2.bit(w: W2, +n: U32) -> U32:
95	  match w:
96	    case W2{hi, lo}:
97	      W2.bit.at(U32.is_lt(n, 32), n, hi, lo)
98	
99	def W2.ge.eq(eq: Bool, al: U32, bl: U32) -> Bool:
100	  match eq:
101	    case False{}:
102	      False{}
103	    case True{}:
104	      U32.is_ge(al, bl)
105	
106	def W2.ge.hi(gt: Bool, eq: Bool, al: U32, bl: U32) -> Bool:
107	  match gt:
108	    case True{}:
109	      True{}
110	    case False{}:
111	      W2.ge.eq(eq, al, bl)
112	
113	def W2.ge(a: W2, b: W2) -> Bool:
114	  match a b:
115	    case W2{+ah, al} W2{+bh, bl}:
116	      W2.ge.hi(U32.is_gt(ah, bh), U32.is_eq(ah, bh), al, bl)
117	
118	def W2.sub.of(ah: U32, bh: U32, al: U32, bl: U32, lo: U32) -> W2:
119	  W2{(ah - bh - u01(U32.is_lt(al, bl)) : U32), lo}
120	
121	def W2.sub(a: W2, b: W2) -> W2:
122	  match a b:
123	    case W2{ah, +al} W2{bh, +bl}:
124	      W2.sub.of(ah, bh, al, bl, (al - bl : U32))
125	
126	def W2.shl1(w: W2, bit: U32) -> W2:
127	  match w:
128	    case W2{hi, +lo}:
129	      W2{((hi << 1n) .|. (lo >> 31n) : U32), ((lo << 1n) .|. bit : U32)}
130	
131	def W2.shl.small(z: Bool, +k: U32, hi: U32, +lo: U32) -> W2:
132	  match z:
133	    case True{}:
134	      W2{hi, lo}
135	    case False{}:
136	      W2{((hi << U32.to_nat(k)) .|. (lo >> U32.to_nat((32 - k : U32))) : U32), (lo << U32.to_nat(k) : U32)}
137	
138	def W2.shl.big(big: Bool, +k: U32, w: W2) -> W2:
139	  match big w:
140	    case True{} W2{hi, lo}:
141	      W2{(lo << U32.to_nat((k - 32 : U32)) : U32), 0}
142	    case False{} W2{hi, lo}:
143	      W2.shl.small(U32.is_zero(k), k, hi, lo)
144	
145	def W2.shl(w: W2, +k: U32) -> W2:
146	  W2.shl.big(U32.is_ge(k, 32), k, w)
147	
148	def W2.msb.hi(z: Bool, hi: U32, lo: U32) -> U32:
149	  match z:
150	    case False{}:
151	      (63 - clz(hi) : U32)
152	    case True{}:
153	      (31 - clz(lo) : U32)
154	
155	def W2.msb(w: W2) -> U32:
156	  match w:
157	    case W2{+hi, lo}:
158	      W2.msb.hi(U32.is_zero(hi), hi, lo)
159	
160	def W2.inc.carry(z: Bool, hi: U32, lo: U32) -> W2:
161	  match z:
162	    case False{}:
163	      W2{hi, lo}
164	    case True{}:
165	      W2{(hi + 1 : U32), lo}
166	
167	def W2.inc.of(hi: U32, +lo: U32) -> W2:
168	  W2.inc.carry(U32.is_zero(lo), hi, lo)
169	
170	def W2.inc(w: W2) -> W2:
171	  match w:
172	    case W2{hi, lo}:
173	      W2.inc.of(hi, (lo + 1 : U32))
174	
175	def W4.nz(w: W4) -> Bool:
176	  match w:
177	    case W4{a, b, c, d}:
178	      Bool.not(Bool.and(Bool.and(U32.is_zero(a), U32.is_zero(b)), Bool.and(U32.is_zero(c), U32.is_zero(d))))
179	
180	def W4.shl1(w: W4) -> W4:
181	  match w:
182	    case W4{a, +b, +c, +d}:
183	      W4{((a << 1n) .|. (b >> 31n) : U32), ((b << 1n) .|. (c >> 31n) : U32), ((c << 1n) .|. (d >> 31n) : U32), (d << 1n : U32)}
184	
185	def W4.set0(w: W4) -> W4:
186	  match w:
187	    case W4{a, b, c, d}:
188	      W4{a, b, c, (d .|. 1 : U32)}
189	
190	def Limb.add.s(+x: U32, c: U32, +s1: U32) -> Limb:
191	  +s2 = (s1 + c : U32)
192	  Limb{s2, u01(Bool.or(U32.is_lt(s1, x), U32.is_lt(s2, s1)))}
193	
194	def Limb.add(+x: U32, y: U32, c: U32) -> Limb:
195	  Limb.add.s(x, c, (x + y : U32))
196	
197	def Limb.sub.s(x: U32, y: U32, +br: U32, +s1: U32) -> Limb:
198	  Limb{(s1 - br : U32), u01(Bool.or(U32.is_lt(x, y), U32.is_lt(s1, br)))}
199	
200	def Limb.sub(+x: U32, +y: U32, br: U32) -> Limb:
201	  Limb.sub.s(x, y, br, (x - y : U32))
202	
203	def W4.add.a(d: U32, c: U32, b: U32, limb: Limb) -> W4:
204	  match limb:
205	    case Limb{a, ca}:
206	      W4{a, b, c, d}
207	
208	def W4.add.b(xa: U32, ya: U32, d: U32, c: U32, limb: Limb) -> W4:
209	  match limb:
210	    case Limb{b, cb}:
211	      W4.add.a(d, c, b, Limb.add(xa, ya, cb))
212	
213	def W4.add.c(xa: U32, xb: U32, ya: U32, yb: U32, d: U32, limb: Limb) -> W4:
214	  match limb:
215	    case Limb{c, cc}:
216	      W4.add.b(xa, ya, d, c, Limb.add(xb, yb, cc))
217	
218	def W4.add.d(xa: U32, xb: U32, xc: U32, ya: U32, yb: U32, yc: U32, limb: Limb) -> W4:
219	  match limb:
220	    case Limb{d, cd}:
221	      W4.add.c(xa, xb, ya, yb, d, Limb.add(xc, yc, cd))
222	
223	def W4.add(x: W4, y: W4) -> W4:
224	  match x y:
225	    case W4{xa, xb, xc, xd} W4{ya, yb, yc, yd}:
226	      W4.add.d(xa, xb, xc, ya, yb, yc, Limb.add(xd, yd, 0))
227	
228	def W4.sub.a(d: U32, c: U32, b: U32, limb: Limb) -> W4:
229	  match limb:
230	    case Limb{a, ba}:
231	      W4{a, b, c, d}
232	
233	def W4.sub.b(xa: U32, ya: U32, d: U32, c: U32, limb: Limb) -> W4:
234	  match limb:
235	    case Limb{b, bb}:
236	      W4.sub.a(d, c, b, Limb.sub(xa, ya, bb))
237	
238	def W4.sub.c(xa: U32, xb: U32, ya: U32, yb: U32, d: U32, limb: Limb) -> W4:
239	  match limb:
240	    case Limb{c, bc}:
241	      W4.sub.b(xa, ya, d, c, Limb.sub(xb, yb, bc))
242	
243	def W4.sub.d(xa: U32, xb: U32, xc: U32, ya: U32, yb: U32, yc: U32, limb: Limb) -> W4:
244	  match limb:
245	    case Limb{d, bd}:
246	      W4.sub.c(xa, xb, ya, yb, d, Limb.sub(xc, yc, bd))
247	
248	def W4.sub(x: W4, y: W4) -> W4:
249	  match x y:
250	    case W4{xa, xb, xc, xd} W4{ya, yb, yc, yd}:
251	      W4.sub.d(xa, xb, xc, ya, yb, yc, Limb.sub(xd, yd, 0))
252	
253	def W4.one() -> W4:
254	  W4{0, 0, 0, 1}
255	
256	def W4.drop1(w: W4) -> W4 & Bool:
257	  match w:
258	    case W4{a, b, c, d}:
259	      (W4{0, a, b, c}, Bool.not(U32.is_zero(d)))
260	
261	def W4.drop2(w: W4) -> W4 & Bool:
262	  match w:
263	    case W4{a, b, c, d}:
264	      (W4{0, 0, a, b}, Bool.not(Bool.and(U32.is_zero(c), U32.is_zero(d))))
265	
266	def W4.drop3(w: W4) -> W4 & Bool:
267	  match w:
268	    case W4{a, b, c, d}:
269	      (W4{0, 0, 0, a}, Bool.not(Bool.and(U32.is_zero(b), Bool.and(U32.is_zero(c), U32.is_zero(d)))))
270	
271	def W4.shr.bits.out(+k: Nat, +j: Nat, +a: U32, +b: U32, +c: U32, d: U32, lost: Bool, low: U32) -> W4 & Bool:
272	  (W4{(a >> k : U32), ((b >> k) .|. (a << j) : U32), ((c >> k) .|. (b << j) : U32), ((d >> k) .|. (c << j) : U32)}, Bool.or(lost, Bool.not(U32.is_zero(low))))
273	
274	def W4.shr.bits.go(+k: Nat, j: Nat, w: W4, lost: Bool) -> W4 & Bool:
275	  match w:
276	    case W4{+a, +b, +c, +d}:
277	      W4.shr.bits.out(k, j, a, b, c, d, lost, (d .&. ((1 << k) - 1 : U32) : U32))
278	
279	def W4.shr.bits.z(z: Bool, +k: U32, w: W4, lost: Bool) -> W4 & Bool:
280	  match z:
281	    case True{}:
282	      (w, lost)
283	    case False{}:
284	      W4.shr.bits.go(U32.to_nat(k), U32.to_nat((32 - k : U32)), w, lost)
285	
286	def W4.shr.bits(+k: U32, w: W4, lost: Bool) -> W4 & Bool:
287	  W4.shr.bits.z(U32.is_zero(k), k, w, lost)
288	
289	def W4.shr.pair(bits: U32, r: W4 & Bool) -> W4 & Bool:
290	  (w, lost) = r
291	  W4.shr.bits(bits, w, lost)
292	
293	def W4.shr.limbs(k: Nat, bits: U32, w: W4) -> W4 & Bool:
294	  match k:
295	    case 0n:
296	      W4.shr.bits(bits, w, False{})
297	    case 1n:
298	      W4.shr.pair(bits, W4.drop1(w))
299	    case 2n:
300	      W4.shr.pair(bits, W4.drop2(w))
301	    case 3n:
302	      W4.shr.pair(bits, W4.drop3(w))
303	    case 4n+p:
304	      (W4{0, 0, 0, 0}, W4.nz(w))
305	
306	def W4.shr.wide(wide: Bool, +n: U32, w: W4) -> W4 & Bool:
307	  match wide:
308	    case True{}:
309	      (W4{0, 0, 0, 0}, W4.nz(w))
310	    case False{}:
311	      W4.shr.limbs(U32.to_nat((n >> 5n : U32)), (n .&. 31 : U32), w)
312	
313	def W4.shr(w: W4, +n: U32) -> W4 & Bool:
314	  W4.shr.wide(U32.is_ge(n, 128), n, w)
315	
316	def W4.slide1(w: W4) -> W4:
317	  match w:
318	    case W4{a, b, c, d}:
319	      W4{b, c, d, 0}
320	
321	def W4.slide2(w: W4) -> W4:
322	  match w:
323	    case W4{a, b, c, d}:
324	      W4{c, d, 0, 0}
325	
326	def W4.slide3(w: W4) -> W4:
327	  match w:
328	    case W4{a, b, c, d}:
329	      W4{d, 0, 0, 0}
330	
331	def W4.shl.bits.go(+k: Nat, +j: Nat, w: W4) -> W4:
332	  match w:
333	    case W4{+a, +b, +c, +d}:
334	      W4{((a << k) .|. (b >> j) : U32), ((b << k) .|. (c >> j) : U32), ((c << k) .|. (d >> j) : U32), (d << k : U32)}
335	
336	def W4.shl.bits.z(z: Bool, +k: U32, w: W4) -> W4:
337	  match z:
338	    case True{}:
339	      w
340	    case False{}:
341	      W4.shl.bits.go(U32.to_nat(k), U32.to_nat((32 - k : U32)), w)
342	
343	def W4.shl.bits(+k: U32, w: W4) -> W4:
344	  W4.shl.bits.z(U32.is_zero(k), k, w)
345	
346	def W4.shl.limbs(k: Nat, bits: U32, w: W4) -> W4:
347	  match k:
348	    case 0n:
349	      W4.shl.bits(bits, w)
350	    case 1n:
351	      W4.shl.bits(bits, W4.slide1(w))
352	    case 2n:
353	      W4.shl.bits(bits, W4.slide2(w))
354	    case 3n:
355	      W4.shl.bits(bits, W4.slide3(w))
356	    case 4n+p:
357	      W4{0, 0, 0, 0}
358	
359	def W4.shl.wide(wide: Bool, +n: U32, w: W4) -> W4:
360	  match wide:
361	    case True{}:
362	      W4{0, 0, 0, 0}
363	    case False{}:
364	      W4.shl.limbs(U32.to_nat((n >> 5n : U32)), (n .&. 31 : U32), w)
365	
366	def W4.shl(w: W4, +n: U32) -> W4:
367	  W4.shl.wide(U32.is_ge(n, 128), n, w)
368	
369	def W4.msb.d(z: Bool, d: U32) -> Maybe<&2, U32>:
370	  match z:
371	    case True{}:
372	      None{}
373	    case False{}:
374	      Some{(31 - clz(d) : U32)}
375	
376	def W4.msb.c(z: Bool, c: U32, +d: U32) -> Maybe<&2, U32>:
377	  match z:
378	    case False{}:
379	      Some{(63 - clz(c) : U32)}
380	    case True{}:
381	      W4.msb.d(U32.is_zero(d), d)
382	
383	def W4.msb.b(z: Bool, b: U32, +c: U32, d: U32) -> Maybe<&2, U32>:
384	  match z:
385	    case False{}:
386	      Some{(95 - clz(b) : U32)}
387	    case True{}:
388	      W4.msb.c(U32.is_zero(c), c, d)
389	
390	def W4.msb.a(z: Bool, a: U32, +b: U32, c: U32, d: U32) -> Maybe<&2, U32>:
391	  match z:
392	    case False{}:
393	      Some{(127 - clz(a) : U32)}
394	    case True{}:
395	      W4.msb.b(U32.is_zero(b), b, c, d)
396	
397	def W4.msb(w: W4) -> Maybe<&2, U32>:
398	  match w:
399	    case W4{+a, b, c, d}:
400	      W4.msb.a(U32.is_zero(a), a, b, c, d)
401	
402	def mul32.of(+p00: U32, +p01: U32, +p10: U32, +p11: U32) -> W2:
403	  +mid = ((p00 >> 16n) + (p01 .&. 65535) + (p10 .&. 65535) : U32)
404	  W2{(p11 + (p01 >> 16n) + (p10 >> 16n) + (mid >> 16n) : U32), ((p00 .&. 65535) .|. (mid << 16n) : U32)}
405	
406	def mul32(+x: U32, +y: U32) -> W2:
407	  +x0 = (x .&. 65535 : U32)
408	  +x1 = (x >> 16n : U32)
409	  +y0 = (y .&. 65535 : U32)
410	  +y1 = (y >> 16n : U32)
411	  mul32.of((x0 * y0 : U32), (x0 * y1 : U32), (x1 * y0 : U32), (x1 * y1 : U32))
412	
413	def mul.sum6(d: U32, c: U32, h11: U32, b12: U32, limb: Limb) -> W4:
414	  match limb:
415	    case Limb{b, b3}:
416	      W4{(h11 + (b12 + b3 : U32) : U32), b, c, d}
417	
418	def mul.sum5(d: U32, c: U32, h11: U32, +b: U32, b12: U32, carry: U32) -> W4:
419	  mul.sum6(d, c, h11, b12, Limb.add(b, carry, 0))
420	
421	def mul.sum4(d: U32, c: U32, h11: U32, b1: U32, carry: U32, limb: Limb) -> W4:
422	  match limb:
423	    case Limb{+b, b2}:
424	      mul.sum5(d, c, h11, b, (b1 + b2 : U32), carry)
425	
426	def mul.sum3(d: U32, c: U32, h10: U32, h11: U32, carry: U32, limb: Limb) -> W4:
427	  match limb:
428	    case Limb{b, b1}:
429	      mul.sum4(d, c, h11, b1, carry, Limb.add(b, h10, 0))
430	
431	def mul.sum2(d: U32, c1: U32, h01: U32, h10: U32, h11: U32, l11: U32, limb: Limb) -> W4:
432	  match limb:
433	    case Limb{c, c2}:
434	      mul.sum3(d, c, h10, h11, (c1 + c2 : U32), Limb.add(l11, h01, 0))
435	
436	def mul.sum1(d: U32, h01: U32, l10: U32, h10: U32, h11: U32, l11: U32, limb: Limb) -> W4:
437	  match limb:
438	    case Limb{c, c1}:
439	      mul.sum2(d, c1, h01, h10, h11, l11, Limb.add(c, l10, 0))
440	
441	def mul.acc(p00: W2, p01: W2, p10: W2, p11: W2) -> W4:
442	  match p00 p01 p10 p11:
443	    case W2{h00, l00} W2{h01, l01} W2{h10, l10} W2{h11, l11}:
444	      mul.sum1(l00, h01, l10, h10, h11, l11, Limb.add(h00, l01, 0))
445	
446	def mul.wide(+xh: U32, +xl: U32, +yh: U32, +yl: U32) -> W4:
447	  mul.acc(mul32(xl, yl), mul32(xl, yh), mul32(xh, yl), mul32(xh, yh))
448	
449	def div.bit.small(small: Bool, idx: U32, ma: W2) -> U32:
450	  match small:
451	    case True{}:
452	      0
453	    case False{}:
454	      W2.bit(ma, (idx - 116 : U32))
455	
456	def div.bit(+p: Nat, ma: W2) -> U32:
457	  div.bit.small(U32.is_lt(U32.from_nat(p), 116), U32.from_nat(p), ma)
458	
459	def div.ge(ge: Bool, rem: W2, q: W4, mb: W2) -> Step:
460	  match ge:
461	    case True{}:
462	      Step{W2.sub(rem, mb), W4.set0(q)}
463	    case False{}:
464	      Step{rem, q}
465	
466	def div.rem(+rem: W2, q: W4, +mb: W2) -> Step:
467	  div.ge(W2.ge(rem, mb), rem, q, mb)
468	
469	def div.advance(p: Nat, st: Step, mb: W2, ma: W2) -> Step:
470	  match st:
471	    case Step{rem, q}:
472	      div.rem(W2.shl1(rem, div.bit(p, ma)), W4.shl1(q), mb)
473	
474	def div.finish(st: Step) -> W4 & Bool:
475	  match st:
476	    case Step{rem, q}:
477	      (q, W2.nz(rem))
478	
479	def div.go(k: Nat, st: Step, +mb: W2, +ma: W2) -> W4 & Bool:
480	  match k:
481	    case 0n:
482	      div.finish(st)
483	    case 1n+p:
484	      +q = p
485	      div.go(q, div.advance(q, st, mb, ma), mb, ma)
486	
487	def div.q(ma: W2, mb: W2) -> W4 & Bool:
488	  div.go(169n, Step{W2{0, 0}, W4{0, 0, 0, 0}}, mb, ma)
489	
490	def round.sub(sub: Bool, sign: U32, exp: U32, sh: U32, sl: U32) -> F64:
491	  match sub:
492	    case True{}:
493	      F64.pack(sign, 0, sh, sl)
494	    case False{}:
495	      F64.pack(sign, exp, sh, sl)
496	
497	def round.zero.lo(zl: Bool, sign: U32, exp: U32, +sh: U32, sl: U32) -> F64:
498	  match zl:
499	    case True{}:
500	      F64.zero.sign(sign)
501	    case False{}:
502	      round.sub(U32.is_lt(sh, 1048576), sign, (exp - 4096 : U32), sh, sl)
503	
504	def round.zero(zh: Bool, zl: Bool, sign: U32, exp: U32, +sh: U32, sl: U32) -> F64:
505	  match zh:
506	    case False{}:
507	      round.sub(U32.is_lt(sh, 1048576), sign, (exp - 4096 : U32), sh, sl)
508	    case True{}:
509	      round.zero.lo(zl, sign, exp, sh, sl)
510	
511	def round.inf(big: Bool, sign: U32, exp: U32, +sh: U32, +sl: U32) -> F64:
512	  match big:
513	    case True{}:
514	      F64.inf.sign(sign)
515	    case False{}:
516	      round.zero(U32.is_zero(sh), U32.is_zero(sl), sign, exp, sh, sl)
517	
518	def round.pack(sign: U32, +exp: U32, sh: U32, sl: U32) -> F64:
519	  round.inf(U32.is_ge((exp - 4096 : U32), 2047), sign, exp, sh, sl)
520	
521	def round.ov(ov: Bool, sign: U32, exp: U32, sh: U32, sl: U32) -> F64:
522	  match ov:
523	    case True{}:
524	      round.pack(sign, (exp + 1 : U32), 1048576, 0)
525	    case False{}:
526	      round.pack(sign, exp, sh, sl)
527	
528	def round.inc(sign: U32, exp: U32, w: W2) -> F64:
529	  match w:
530	    case W2{+sh, sl}:
531	      round.ov(U32.is_ge(sh, 2097152), sign, exp, sh, sl)
532	
533	def round.should(+c: U32, d: U32, sl: U32, sticky: Bool) -> Bool:
534	  Bool.and(U32.is_ge(c, 2147483648), Bool.or(Bool.or(sticky, Bool.not(U32.is_zero((c .&. 2147483647 : U32)))), Bool.or(Bool.not(U32.is_zero(d)), U32.is_eq((sl .&. 1 : U32), 1))))
535	
536	def round.up(up: Bool, sign: U32, exp: U32, sh: U32, sl: U32) -> F64:
537	  match up:
538	    case False{}:
539	      round.pack(sign, exp, sh, sl)
540	    case True{}:
541	      round.inc(sign, exp, W2.inc(W2{sh, sl}))
542	
543	def round.sig(sign: U32, exp: U32, sh: U32, +sl: U32, c: U32, d: U32, sticky: Bool) -> F64:
544	  round.up(round.should(c, d, sl, sticky), sign, exp, sh, sl)
545	
546	def round.go(sign: U32, exp: U32, w: W4, sticky: Bool) -> F64:
547	  match w:
548	    case W4{a, b, c, d}:
549	      round.sig(sign, exp, (a .&. 2097151 : U32), b, c, d, sticky)
550	
551	
552	def norm.right.pair(sign: U32, exp: U32, sticky: Bool, r: W4 & Bool) -> F64:
553	  (w, lost) = r
554	  round.go(sign, exp, w, Bool.or(sticky, lost))
555	
556	def norm.right.sh(+sh: U32, sign: U32, exp: U32, w: W4, sticky: Bool) -> F64:
557	  norm.right.pair(sign, (exp + sh : U32), sticky, W4.shr(w, sh))
558	
559	def norm.right(top: U32, sign: U32, exp: U32, w: W4, sticky: Bool) -> F64:
560	  norm.right.sh((top - 116 : U32), sign, exp, w, sticky)
561	
562	def norm.left.room0(z: Bool, room: U32, sign: U32, w: W4, sticky: Bool) -> F64:
563	  match z:
564	    case True{}:
565	      round.go(sign, 4097, w, sticky)
566	    case False{}:
567	      round.go(sign, 4097, W4.shl(w, room), sticky)
568	
569	def norm.left.fit(fit: Bool, +need: U32, +room: U32, sign: U32, exp: U32, w: W4, sticky: Bool) -> F64:
570	  match fit:
571	    case True{}:
572	      round.go(sign, (exp - need : U32), W4.shl(w, need), sticky)
573	    case False{}:
574	      norm.left.room0(U32.is_zero(room), room, sign, w, sticky)
575	
576	def norm.left.room(+need: U32, +room: U32, sign: U32, exp: U32, w: W4, sticky: Bool) -> F64:
577	  norm.left.fit(U32.is_le(need, room), need, room, sign, exp, w, sticky)
578	
579	def norm.left.need(need: U32, sign: U32, +exp: U32, w: W4, sticky: Bool) -> F64:
580	  norm.left.room(need, (exp - 4097 : U32), sign, exp, w, sticky)
581	
582	def norm.left(top: U32, sign: U32, exp: U32, w: W4, sticky: Bool) -> F64:
583	  norm.left.need((116 - top : U32), sign, exp, w, sticky)
584	
585	def norm.lo(lo: Bool, top: U32, sign: U32, exp: U32, w: W4, sticky: Bool) -> F64:
586	  match lo:
587	    case True{}:
588	      norm.left(top, sign, exp, w, sticky)
589	    case False{}:
590	      round.go(sign, exp, w, sticky)
591	
592	def norm.hi(hi: Bool, +top: U32, sign: U32, exp: U32, w: W4, sticky: Bool) -> F64:
593	  match hi:
594	    case True{}:
595	      norm.right(top, sign, exp, w, sticky)
596	    case False{}:
597	      norm.lo(U32.is_lt(top, 116), top, sign, exp, w, sticky)
598	def norm.top(m: Maybe<&2, U32>, sign: U32, exp: U32, w: W4, sticky: Bool) -> F64:
599	  match m:
600	    case None{}:
601	      F64.zero.sign(sign)
602	    case Some{+top}:
603	      norm.hi(U32.is_gt(top, 116), top, sign, exp, w, sticky)
604	
605	def norm.z(nz: Bool, sign: U32, exp: U32, +w: W4, sticky: Bool) -> F64:
606	  match nz:
607	    case False{}:
608	      F64.zero.sign(sign)
609	    case True{}:
610	      norm.top(W4.msb(w), sign, exp, w, sticky)
611	
612	def norm.go(st: Norm) -> F64:
613	  match st:
614	    case Norm{sign, exp, +w, sticky}:
615	      norm.z(W4.nz(w), sign, exp, w, sticky)
616	
617	def under.pair(sign: U32, sticky: Bool, r: W4 & Bool) -> F64:
618	  (w, lost) = r
619	  norm.go(Norm{sign, 4097, w, Bool.or(sticky, lost)})
620	
621	def under.shr(sign: U32, w: W4, sticky: Bool, sh: U32) -> F64:
622	  under.pair(sign, sticky, W4.shr(w, sh))
623	
624	def under.low(low: Bool, exp: U32, sign: U32, w: W4, sticky: Bool) -> F64:
625	  match low:
626	    case False{}:
627	      norm.go(Norm{sign, exp, w, sticky})
628	    case True{}:
629	      under.shr(sign, w, sticky, (4097 - exp : U32))
630	
631	def under(sign: U32, +exp: U32, w: W4, sticky: Bool) -> F64:
632	  under.low(U32.is_lt(exp, 4097), exp, sign, w, sticky)
633	
634	def mag.eq(eq: Bool, al: U32, bl: U32) -> Bool:
635	  match eq:
636	    case False{}:
637	      False{}
638	    case True{}:
639	      U32.is_lt(al, bl)
640	
641	def mag.hi(lt: Bool, eq: Bool, al: U32, bl: U32) -> Bool:
642	  match lt:
643	    case True{}:
644	      True{}
645	    case False{}:
646	      mag.eq(eq, al, bl)
647	
648	def mag.same(eq: Bool, ma: W2, mb: W2) -> Bool:
649	  match eq ma mb:
650	    case False{} W2{ah, al} W2{bh, bl}:
651	      False{}
652	    case True{} W2{+ah, al} W2{+bh, bl}:
653	      mag.hi(U32.is_lt(ah, bh), U32.is_eq(ah, bh), al, bl)
654	
655	def mag.exp(lt: Bool, eq: Bool, ma: W2, mb: W2) -> Bool:
656	  match lt:
657	    case True{}:
658	      True{}
659	    case False{}:
660	      mag.same(eq, ma, mb)
661	
662	def mag.lt(+ea: U32, ma: W2, +eb: U32, mb: W2) -> Bool:
663	  mag.exp(U32.is_lt(ea, eb), U32.is_eq(ea, eb), ma, mb)
664	
665	def add.cancel(nz: Bool, sign: U32, exp: U32, total: W4, sticky: Bool) -> F64:
666	  match nz:
667	    case False{}:
668	      F64{0, 0}
669	    case True{}:
670	      norm.go(Norm{sign, exp, total, sticky})
671	
672	def add.borrow(sign: U32, exp: U32, +total: W4) -> F64:
673	  add.cancel(W4.nz(total), sign, exp, total, True{})
674	
675	def add.sub.lost(lost: Bool, sign: U32, exp: U32, +total: W4) -> F64:
676	  match lost:
677	    case False{}:
678	      add.cancel(W4.nz(total), sign, exp, total, False{})
679	    case True{}:
680	      add.borrow(sign, exp, W4.sub(total, W4.one()))
681	
682	def add.sign(same: Bool, sign: U32, exp: U32, +aa: W4, +trunc: W4, lost: Bool) -> F64:
683	  match same:
684	    case True{}:
685	      norm.go(Norm{sign, exp, W4.add(aa, trunc), lost})
686	    case False{}:
687	      add.sub.lost(lost, sign, exp, W4.sub(aa, trunc))
688	
689	def add.pair(same: Bool, sign: U32, exp: U32, aa: W4, r: W4 & Bool) -> F64:
690	  (trunc, lost) = r
691	  add.sign(same, sign, exp, aa, trunc, lost)
692	
693	def add.de(same: Bool, sa: U32, ea: U32, ma: W2, de: U32, mb: W2) -> F64:
694	  match ma mb:
695	    case W2{ah, al} W2{bh, bl}:
696	      add.pair(same, sa, ea, W4{ah, al, 0, 0}, W4.shr(W4{bh, bl, 0, 0}, de))
697	def add.ord(swap: Bool, +sa: U32, +ea: U32, +ma: W2, +sb: U32, +eb: U32, +mb: W2) -> F64:
698	  match swap:
699	    case True{}:
700	      add.de(U32.is_eq(sb, sa), sb, eb, mb, (eb - ea : U32), ma)
701	    case False{}:
702	      add.de(U32.is_eq(sa, sb), sa, ea, ma, (ea - eb : U32), mb)
703	
704	
705	def add.fin(+sa: U32, +ea: U32, +ma: W2, +sb: U32, +eb: U32, +mb: W2) -> F64:
706	  add.ord(mag.lt(ea, ma, eb, mb), sa, ea, ma, sb, eb, mb)
707	
708	def add.fin.z(na: Bool, nb: Bool, a: F64, b: F64, +sa: U32, ea: U32, ma: W2, sb: U32, eb: U32, mb: W2) -> F64:
709	  match na nb:
710	    case False{} False{}:
711	      F64.zero.sign(u01(Bool.and(U32.is_eq(sa, sb), U32.is_eq(sa, 1))))
712	    case False{} True{}:
713	      b
714	    case True{} False{}:
715	      a
716	    case True{} True{}:
717	      add.fin(sa, ea, ma, sb, eb, mb)
718	
719	def add.kb(kb: Cls, a: F64, b: F64, sa: U32, ea: U32, +ma: W2, sb: U32, eb: U32, +mb: W2) -> F64:
720	  match kb:
721	    case Nan{}:
722	      F64.nan()
723	    case Inf{}:
724	      F64.inf.sign(sb)
725	    case Fin{}:
726	      add.fin.z(W2.nz(ma), W2.nz(mb), a, b, sa, ea, ma, sb, eb, mb)
727	
728	def add.inf.both(same: Bool, sa: U32) -> F64:
729	  match same:
730	    case True{}:
731	      F64.inf.sign(sa)
732	    case False{}:
733	      F64.nan()
734	
735	def add.inf.a(kb: Cls, +sa: U32, sb: U32) -> F64:
736	  match kb:
737	    case Nan{}:
738	      F64.nan()
739	    case Inf{}:
740	      add.inf.both(U32.is_eq(sa, sb), sa)
741	    case Fin{}:
742	      F64.inf.sign(sa)
743	
744	def add.ka(ka: Cls, kb: Cls, a: F64, b: F64, sa: U32, ea: U32, ma: W2, sb: U32, eb: U32, mb: W2) -> F64:
745	  match ka:
746	    case Nan{}:
747	      F64.nan()
748	    case Inf{}:
749	      add.inf.a(kb, sa, sb)
750	    case Fin{}:
751	      add.kb(kb, a, b, sa, ea, ma, sb, eb, mb)
752	
753	def add.both(a: F64, b: F64, pa: Parts, pb: Parts) -> F64:
754	  match pa pb:
755	    case Parts{ka, sa, ea, ma} Parts{kb, sb, eb, mb}:
756	      add.ka(ka, kb, a, b, sa, ea, ma, sb, eb, mb)
757	
758	def unpack.sub(sub: Bool, exp: U32, +h: U32, l: U32) -> Parts:
759	  match sub:
760	    case True{}:
761	      Parts{Fin{}, (h >> 31n : U32), 4097, W2{(h .&. 1048575 : U32), l}}
762	    case False{}:
763	      Parts{Fin{}, (h >> 31n : U32), (exp + 4096 : U32), W2{((h .&. 1048575) .|. 1048576 : U32), l}}
764	
765	def unpack.nan(z: Bool, h: U32) -> Parts:
766	  match z:
767	    case True{}:
768	      Parts{Inf{}, (h >> 31n : U32), 0, W2{0, 0}}
769	    case False{}:
770	      Parts{Nan{}, 0, 0, W2{0, 0}}
771	
772	def unpack.special(naninf: Bool, sub: Bool, exp: U32, +h: U32, l: U32) -> Parts:
773	  match naninf:
774	    case True{}:
775	      unpack.nan(Bool.and(U32.is_zero((h .&. 1048575 : U32)), U32.is_zero(l)), h)
776	    case False{}:
777	      unpack.sub(sub, exp, h, l)
778	
779	def unpack(+h: U32, l: U32) -> Parts:
780	  unpack.special(U32.is_eq(((h >> 20n) .&. 2047 : U32), 2047), U32.is_zero(((h >> 20n) .&. 2047 : U32)), ((h >> 20n) .&. 2047 : U32), h, l)
781	
782	def F64.add(a: F64, b: F64) -> F64:
783	  match a b:
784	    case F64{+ah, +al} F64{+bh, +bl}:
785	      add.both(F64{ah, al}, F64{bh, bl}, unpack(ah, al), unpack(bh, bl))
786	
787	def F64.neg(a: F64) -> F64:
788	  match a:
789	    case F64{hi, lo}:
790	      F64{(hi .^. 2147483648 : U32), lo}
791	
792	def F64.sub(a: F64, b: F64) -> F64:
793	  F64.add(a, F64.neg(b))
794	
795	def mul.sig(sa: U32, ea: U32, ma: W2, sb: U32, eb: U32, mb: W2) -> F64:
796	  match ma mb:
797	    case W2{ah, al} W2{bh, bl}:
798	      under((sa .^. sb : U32), (ea + eb - 5119 : U32), W4.shl(mul.wide(ah, al, bh, bl), 12), False{})
799	
800	def mul.z(az: Bool, bz: Bool, sign: U32, sa: U32, ea: U32, ma: W2, sb: U32, eb: U32, mb: W2) -> F64:
801	  match az bz:
802	    case True{} _:
803	      F64.zero.sign(sign)
804	    case False{} True{}:
805	      F64.zero.sign(sign)
806	    case False{} False{}:
807	      mul.sig(sa, ea, ma, sb, eb, mb)
808	
809	def Cls.inf(k: Cls) -> Bool:
810	  match k:
811	    case Inf{}:
812	      True{}
813	    case Fin{}:
814	      False{}
815	    case Nan{}:
816	      False{}
817	
818	def Cls.fin(k: Cls) -> Bool:
819	  match k:
820	    case Fin{}:
821	      True{}
822	    case Inf{}:
823	      False{}
824	    case Nan{}:
825	      False{}
826	
827	def Cls.nan(k: Cls) -> Bool:
828	  match k:
829	    case Nan{}:
830	      True{}
831	    case Fin{}:
832	      False{}
833	    case Inf{}:
834	      False{}
835	
836	def mul.inf.z(z: Bool, sign: U32) -> F64:
837	  match z:
838	    case True{}:
839	      F64.nan()
840	    case False{}:
841	      F64.inf.sign(sign)
842	
843	def mul.inf(inf: Bool, az: Bool, bz: Bool, sign: U32, sa: U32, ea: U32, ma: W2, sb: U32, eb: U32, mb: W2) -> F64:
844	  match inf:
845	    case True{}:
846	      mul.inf.z(Bool.or(az, bz), sign)
847	    case False{}:
848	      mul.z(az, bz, sign, sa, ea, ma, sb, eb, mb)
849	
850	def mul.nan(nan: Bool, +ca: Cls, +cb: Cls, +sa: U32, ea: U32, +ma: W2, +sb: U32, eb: U32, +mb: W2) -> F64:
851	  match nan:
852	    case True{}:
853	      F64.nan()
854	    case False{}:
855	      mul.inf(Bool.or(Cls.inf(ca), Cls.inf(cb)), Bool.and(Cls.fin(ca), Bool.not(W2.nz(ma))), Bool.and(Cls.fin(cb), Bool.not(W2.nz(mb))), (sa .^. sb : U32), sa, ea, ma, sb, eb, mb)
856	
857	def mul.parts(pa: Parts, pb: Parts) -> F64:
858	  match pa pb:
859	    case Parts{+ka, sa, ea, ma} Parts{+kb, sb, eb, mb}:
860	      mul.nan(Bool.or(Cls.nan(ka), Cls.nan(kb)), ka, kb, sa, ea, ma, sb, eb, mb)
861	
862	def F64.mul(a: F64, b: F64) -> F64:
863	  match a b:
864	    case F64{ah, al} F64{bh, bl}:
865	      mul.parts(unpack(ah, al), unpack(bh, bl))
866	
867	def div.norm(k: U32, mb: W2) -> W2:
868	  W2.shl(mb, k)
869	
870	def div.sig.q(sign: U32, exp: U32, r: W4 & Bool) -> F64:
871	  (q, sticky) = r
872	  under(sign, exp, q, sticky)
873	
874	def div.sig(sign: U32, ea: U32, ma: W2, eb: U32, mb: W2, +k: U32) -> F64:
875	  div.sig.q(sign, (ea + 5119 + k - eb : U32), div.q(ma, div.norm(k, mb)))
876	
877	def div.k(sign: U32, ea: U32, ma: W2, eb: U32, +mb: W2) -> F64:
878	  div.sig(sign, ea, ma, eb, mb, (52 - W2.msb(mb) : U32))
879	
880	def div.by0(na: Bool, sign: U32) -> F64:
881	  match na:
882	    case False{}:
883	      F64.nan()
884	    case True{}:
885	      F64.inf.sign(sign)
886	
887	def div.num0(na: Bool, sign: U32, ea: U32, ma: W2, eb: U32, mb: W2) -> F64:
888	  match na:
889	    case False{}:
890	      F64.zero.sign(sign)
891	    case True{}:
892	      div.k(sign, ea, ma, eb, mb)
893	
894	def div.fin.z(nb: Bool, na: Bool, sign: U32, ea: U32, ma: W2, eb: U32, mb: W2) -> F64:
895	  match nb:
896	    case False{}:
897	      div.by0(na, sign)
898	    case True{}:
899	      div.num0(na, sign, ea, ma, eb, mb)
900	
901	def div.fin.a(ia: Bool, nb: Bool, na: Bool, sign: U32, ea: U32, ma: W2, eb: U32, mb: W2) -> F64:
902	  match ia:
903	    case True{}:
904	      F64.inf.sign(sign)
905	    case False{}:
906	      div.fin.z(nb, na, sign, ea, ma, eb, mb)
907	
908	def div.fin.b(ib: Bool, ia: Bool, nb: Bool, na: Bool, sign: U32, ea: U32, ma: W2, eb: U32, mb: W2) -> F64:
909	  match ib:
910	    case True{}:
911	      F64.zero.sign(sign)
912	    case False{}:
913	      div.fin.a(ia, nb, na, sign, ea, ma, eb, mb)
914	
915	def div.fin(+ca: Cls, +cb: Cls, sign: U32, ea: U32, +ma: W2, eb: U32, +mb: W2) -> F64:
916	  div.fin.b(Cls.inf(cb), Cls.inf(ca), W2.nz(mb), W2.nz(ma), sign, ea, ma, eb, mb)
917	
918	def div.both(both: Bool, ca: Cls, cb: Cls, sign: U32, ea: U32, ma: W2, eb: U32, mb: W2) -> F64:
919	  match both:
920	    case True{}:
921	      F64.nan()
922	    case False{}:
923	      div.fin(ca, cb, sign, ea, ma, eb, mb)
924	
925	def div.nan(nan: Bool, both: Bool, ca: Cls, cb: Cls, sign: U32, ea: U32, ma: W2, eb: U32, mb: W2) -> F64:
926	  match nan:
927	    case True{}:
928	      F64.nan()
929	    case False{}:
930	      div.both(both, ca, cb, sign, ea, ma, eb, mb)
931	
932	def div.parts(pa: Parts, pb: Parts) -> F64:
933	  match pa pb:
934	    case Parts{+ka, +sa, ea, ma} Parts{+kb, +sb, eb, mb}:
935	      div.nan(Bool.or(Cls.nan(ka), Cls.nan(kb)), Bool.and(Cls.inf(ka), Cls.inf(kb)), ka, kb, (sa .^. sb : U32), ea, ma, eb, mb)
936	
937	def F64.div(a: F64, b: F64) -> F64:
938	  match a b:
939	    case F64{ah, al} F64{bh, bl}:
940	      div.parts(unpack(ah, al), unpack(bh, bl))
941	
942	def F64.nan.bits(+h: U32, l: U32) -> Bool:
943	  Bool.and(U32.is_eq(((h >> 20n) .&. 2047 : U32), 2047), Bool.not(Bool.and(U32.is_zero((h .&. 1048575 : U32)), U32.is_zero(l))))
944	
945	def F64.zero.bits(h: U32, l: U32) -> Bool:
946	  Bool.and(U32.is_zero((h .&. 2147483647 : U32)), U32.is_zero(l))
947	
948	def F64.is_nan(a: F64) -> Bool:
949	  match a:
950	    case F64{hi, lo}:
951	      F64.nan.bits(hi, lo)
952	
953	def F64.is_inf(a: F64) -> Bool:
954	  match a:
955	    case F64{+hi, lo}:
956	      Bool.and(U32.is_eq(((hi >> 20n) .&. 2047 : U32), 2047), F64.zero.bits((hi .&. 2147483647 : U32), lo))
957	
958	def F64.is_zero(a: F64) -> Bool:
959	  match a:
960	    case F64{hi, lo}:
961	      F64.zero.bits(hi, lo)
962	
963	def F64.is_subnormal(a: F64) -> Bool:
964	  match a:
965	    case F64{+hi, lo}:
966	      Bool.and(U32.is_zero(((hi >> 20n) .&. 2047 : U32)), Bool.not(F64.zero.bits(hi, lo)))
967	
968	def F64.eq.bits(ah: U32, al: U32, bh: U32, bl: U32) -> Bool:
969	  Bool.and(U32.is_eq(ah, bh), U32.is_eq(al, bl))
970	
971	def F64.eq.zb(zb: Bool, ah: U32, al: U32, bh: U32, bl: U32) -> Bool:
972	  match zb:
973	    case True{}:
974	      False{}
975	    case False{}:
976	      F64.eq.bits(ah, al, bh, bl)
977	
978	def F64.eq.zero(za: Bool, zb: Bool, ah: U32, al: U32, bh: U32, bl: U32) -> Bool:
979	  match za:
980	    case True{}:
981	      zb
982	    case False{}:
983	      F64.eq.zb(zb, ah, al, bh, bl)
984	
985	def F64.eq.nb(nb: Bool, +ah: U32, +al: U32, +bh: U32, +bl: U32) -> Bool:
986	  match nb:
987	    case True{}:
988	      False{}
989	    case False{}:
990	      F64.eq.zero(F64.zero.bits(ah, al), F64.zero.bits(bh, bl), ah, al, bh, bl)
991	
992	def F64.eq.nan(na: Bool, nb: Bool, ah: U32, al: U32, bh: U32, bl: U32) -> Bool:
993	  match na:
994	    case True{}:
995	      False{}
996	    case False{}:
997	      F64.eq.nb(nb, ah, al, bh, bl)
998	
999	def F64.is_eq(a: F64, b: F64) -> Bool:
1000	  match a b:
1001	    case F64{+ah, +al} F64{+bh, +bl}:
1002	      F64.eq.nan(F64.nan.bits(ah, al), F64.nan.bits(bh, bl), ah, al, bh, bl)
1003	
1004	def F64.lt.eq(eq: Bool, al: U32, bl: U32) -> Bool:
1005	  match eq:
1006	    case False{}:
1007	      False{}
1008	    case True{}:
1009	      U32.is_lt(al, bl)
1010	
1011	def F64.lt.hi(lt: Bool, eq: Bool, al: U32, bl: U32) -> Bool:
1012	  match lt:
1013	    case True{}:
1014	      True{}
1015	    case False{}:
1016	      F64.lt.eq(eq, al, bl)
1017	
1018	def F64.lt.mag(+ah: U32, al: U32, +bh: U32, bl: U32) -> Bool:
1019	  F64.lt.hi(U32.is_lt(ah, bh), U32.is_eq(ah, bh), al, bl)
1020	
1021	def F64.lt.neg(nb: Bool, ah: U32, al: U32, bh: U32, bl: U32) -> Bool:
1022	  match nb:
1023	    case False{}:
1024	      True{}
1025	    case True{}:
1026	      F64.lt.mag(bh, bl, ah, al)
1027	
1028	def F64.lt.pos(nb: Bool, ah: U32, al: U32, bh: U32, bl: U32) -> Bool:
1029	  match nb:
1030	    case True{}:
1031	      False{}
1032	    case False{}:
1033	      F64.lt.mag(ah, al, bh, bl)
1034	
1035	def F64.lt.sign(na: Bool, nb: Bool, ah: U32, al: U32, bh: U32, bl: U32) -> Bool:
1036	  match na:
1037	    case True{}:
1038	      F64.lt.neg(nb, ah, al, bh, bl)
1039	    case False{}:
1040	      F64.lt.pos(nb, ah, al, bh, bl)
1041	
1042	def F64.lt.zb(zb: Bool, +ah: U32, al: U32, +bh: U32, bl: U32) -> Bool:
1043	  match zb:
1044	    case True{}:
1045	      False{}
1046	    case False{}:
1047	      F64.lt.sign(U32.is_ge(ah, 2147483648), U32.is_ge(bh, 2147483648), ah, al, bh, bl)
1048	
1049	def F64.lt.zero(za: Bool, zb: Bool, +ah: U32, al: U32, +bh: U32, bl: U32) -> Bool:
1050	  match za:
1051	    case True{}:
1052	      F64.lt.zb(zb, ah, al, bh, bl)
1053	    case False{}:
1054	      F64.lt.sign(U32.is_ge(ah, 2147483648), U32.is_ge(bh, 2147483648), ah, al, bh, bl)
1055	
1056	def F64.lt.nb(nb: Bool, +ah: U32, +al: U32, +bh: U32, +bl: U32) -> Bool:
1057	  match nb:
1058	    case True{}:
1059	      False{}
1060	    case False{}:
1061	      F64.lt.zero(F64.zero.bits(ah, al), F64.zero.bits(bh, bl), ah, al, bh, bl)
1062	
1063	def F64.lt.nan(na: Bool, nb: Bool, ah: U32, al: U32, bh: U32, bl: U32) -> Bool:
1064	  match na:
1065	    case True{}:
1066	      False{}
1067	    case False{}:
1068	      F64.lt.nb(nb, ah, al, bh, bl)
1069	
1070	def F64.is_lt(a: F64, b: F64) -> Bool:
1071	  match a b:
1072	    case F64{+ah, +al} F64{+bh, +bl}:
1073	      F64.lt.nan(F64.nan.bits(ah, al), F64.nan.bits(bh, bl), ah, al, bh, bl)
1074	
1075	def F64.is_ne(a: F64, b: F64) -> Bool:
1076	  Bool.not(F64.is_eq(a, b))
1077	
1078	def F64.is_le(+a: F64, +b: F64) -> Bool:
1079	  Bool.or(F64.is_lt(a, b), F64.is_eq(a, b))
1080	
1081	def F64.is_gt(a: F64, b: F64) -> Bool:
1082	  F64.is_lt(b, a)
1083	
1084	def F64.is_ge(+a: F64, +b: F64) -> Bool:
1085	  Bool.or(F64.is_lt(b, a), F64.is_eq(a, b))
1086	
1087	def F64.abs(a: F64) -> F64:
1088	  match a:
1089	    case F64{hi, lo}:
1090	      F64{(hi .&. 2147483647 : U32), lo}
1091	
1092	def F64.from.lo(+z: U32, +n: U32, hi_sh: U32, lo_sh: U32) -> F64:
1093	  F64.pack(0, (1054 - z : U32), (n >> U32.to_nat(hi_sh) : U32), (n << U32.to_nat(lo_sh) : U32))
1094	
1095	def F64.from.small(small: Bool, +z: U32, +n: U32) -> F64:
1096	  match small:
1097	    case True{}:
1098	      F64.from.lo(z, n, (11 - z : U32), (21 + z : U32))
1099	    case False{}:
1100	      F64.pack(0, (1054 - z : U32), (n << U32.to_nat((z - 11 : U32)) : U32), 0)
1101	
1102	def F64.from.clz(+z: U32, n: U32) -> F64:
1103	  F64.from.small(U32.is_lt(z, 11), z, n)
1104	
1105	def F64.from.z(z: Bool, +n: U32) -> F64:
1106	  match z:
1107	    case True{}:
1108	      F64{0, 0}
1109	    case False{}:
1110	      F64.from.clz(clz(n), n)
1111	
1112	def F64.from_u32(+n: U32) -> F64:
1113	  F64.from.z(U32.is_zero(n), n)
1114	
1115	def F64.one() -> F64:
1116	  F64{1072693248, 0}
1117	
1118	def F64.zero() -> F64:
1119	  F64{0, 0}
1120	
1121	def F64.inf() -> F64:
1122	  F64{2146435072, 0}