f64.bend
bend-kit-f64@0.1.0.0 · 1,122 lines · 210 definitions
1
2import Base
3
4
5
6
7
8type W2 is Data:
9 W2{hi: U32, lo: U32}
10
11type W4 is Data:
12 W4{a: U32, b: U32, c: U32, d: U32}
13
14type Limb is Data:
15 Limb{s: U32, c: U32}
16
17type Step is Data:
18 Step{rem: W2, q: W4}
19
20type Cls is Data:
21 Fin{}
22 Inf{}
23 Nan{}
24
25type Parts is Data:
26 Parts{kind: Cls, sign: U32, exp: U32, sig: W2}
27
28type Norm is Data:
29 Norm{sign: U32, exp: U32, w: W4, sticky: Bool}
30
31type F64 is Data:
32 F64{hi: U32, lo: U32}
33
34def u01(b: Bool) -> U32:
35 match b:
36 case True{}:
37 1
38 case False{}:
39 0
40
41def 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
50def clz(+x: U32) -> U32:
51 clz.go(32n, U32.is_zero((x .&. 2147483648 : U32)), 0, x)
52
53def F64.nan() -> F64:
54 F64{2146959360, 0}
55
56def F64.inf.pos(pos: Bool) -> F64:
57 match pos:
58 case True{}:
59 F64{2146435072, 0}
60 case False{}:
61 F64{4293918720, 0}
62
63def F64.inf.sign(sign: U32) -> F64:
64 F64.inf.pos(U32.is_zero(sign))
65
66def F64.zero.sign(sign: U32) -> F64:
67 F64{(sign << 31n : U32), 0}
68
69def F64.pack(sign: U32, exp: U32, sh: U32, sl: U32) -> F64:
70 F64{((sign << 31n) .|. (exp << 20n) .|. (sh .&. 1048575) : U32), sl}
71
72def F64.hi(a: F64) -> U32:
73 match a:
74 case F64{hi, lo}:
75 hi
76
77def F64.lo(a: F64) -> U32:
78 match a:
79 case F64{hi, lo}:
80 lo
81
82def 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
87def 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
94def 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
99def 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
106def 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
113def 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
118def 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
121def 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
126def 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
131def 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
138def 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
145def W2.shl(w: W2, +k: U32) -> W2:
146 W2.shl.big(U32.is_ge(k, 32), k, w)
147
148def 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
155def W2.msb(w: W2) -> U32:
156 match w:
157 case W2{+hi, lo}:
158 W2.msb.hi(U32.is_zero(hi), hi, lo)
159
160def 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
167def W2.inc.of(hi: U32, +lo: U32) -> W2:
168 W2.inc.carry(U32.is_zero(lo), hi, lo)
169
170def W2.inc(w: W2) -> W2:
171 match w:
172 case W2{hi, lo}:
173 W2.inc.of(hi, (lo + 1 : U32))
174
175def 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
180def 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
185def W4.set0(w: W4) -> W4:
186 match w:
187 case W4{a, b, c, d}:
188 W4{a, b, c, (d .|. 1 : U32)}
189
190def 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
194def Limb.add(+x: U32, y: U32, c: U32) -> Limb:
195 Limb.add.s(x, c, (x + y : U32))
196
197def 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
200def Limb.sub(+x: U32, +y: U32, br: U32) -> Limb:
201 Limb.sub.s(x, y, br, (x - y : U32))
202
203def 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
208def 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
213def 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
218def 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
223def 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
228def 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
233def 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
238def 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
243def 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
248def 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
253def W4.one() -> W4:
254 W4{0, 0, 0, 1}
255
256def 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
261def 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
266def 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
271def 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
274def 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
279def 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
286def W4.shr.bits(+k: U32, w: W4, lost: Bool) -> W4 & Bool:
287 W4.shr.bits.z(U32.is_zero(k), k, w, lost)
288
289def W4.shr.pair(bits: U32, r: W4 & Bool) -> W4 & Bool:
290 (w, lost) = r
291 W4.shr.bits(bits, w, lost)
292
293def 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
306def 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
313def W4.shr(w: W4, +n: U32) -> W4 & Bool:
314 W4.shr.wide(U32.is_ge(n, 128), n, w)
315
316def W4.slide1(w: W4) -> W4:
317 match w:
318 case W4{a, b, c, d}:
319 W4{b, c, d, 0}
320
321def W4.slide2(w: W4) -> W4:
322 match w:
323 case W4{a, b, c, d}:
324 W4{c, d, 0, 0}
325
326def W4.slide3(w: W4) -> W4:
327 match w:
328 case W4{a, b, c, d}:
329 W4{d, 0, 0, 0}
330
331def 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
336def 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
343def W4.shl.bits(+k: U32, w: W4) -> W4:
344 W4.shl.bits.z(U32.is_zero(k), k, w)
345
346def 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
359def 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
366def W4.shl(w: W4, +n: U32) -> W4:
367 W4.shl.wide(U32.is_ge(n, 128), n, w)
368
369def 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
376def 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
383def 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
390def 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
397def 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
402def 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
406def 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
413def 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
418def 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
421def 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
426def 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
431def 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
436def 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
441def 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
446def 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
449def 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
456def 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
459def 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
466def div.rem(+rem: W2, q: W4, +mb: W2) -> Step:
467 div.ge(W2.ge(rem, mb), rem, q, mb)
468
469def 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
474def div.finish(st: Step) -> W4 & Bool:
475 match st:
476 case Step{rem, q}:
477 (q, W2.nz(rem))
478
479def 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
487def div.q(ma: W2, mb: W2) -> W4 & Bool:
488 div.go(169n, Step{W2{0, 0}, W4{0, 0, 0, 0}}, mb, ma)
489
490def 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
497def 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
504def 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
511def 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
518def 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
521def 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
528def 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
533def 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
536def 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
543def 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
546def 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
552def 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
556def 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
559def 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
562def 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
569def 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
576def 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
579def 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
582def 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
585def 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
592def 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)
598def 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
605def 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
612def 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
617def 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
621def under.shr(sign: U32, w: W4, sticky: Bool, sh: U32) -> F64:
622 under.pair(sign, sticky, W4.shr(w, sh))
623
624def 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
631def under(sign: U32, +exp: U32, w: W4, sticky: Bool) -> F64:
632 under.low(U32.is_lt(exp, 4097), exp, sign, w, sticky)
633
634def 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
641def 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
648def 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
655def 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
662def 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
665def 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
672def add.borrow(sign: U32, exp: U32, +total: W4) -> F64:
673 add.cancel(W4.nz(total), sign, exp, total, True{})
674
675def 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
682def 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
689def 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
693def 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))
697def 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
705def 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
708def 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
719def 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
728def 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
735def 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
744def 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
753def 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
758def 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
765def 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
772def 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
779def 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
782def 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
787def F64.neg(a: F64) -> F64:
788 match a:
789 case F64{hi, lo}:
790 F64{(hi .^. 2147483648 : U32), lo}
791
792def F64.sub(a: F64, b: F64) -> F64:
793 F64.add(a, F64.neg(b))
794
795def 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
800def 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
809def Cls.inf(k: Cls) -> Bool:
810 match k:
811 case Inf{}:
812 True{}
813 case Fin{}:
814 False{}
815 case Nan{}:
816 False{}
817
818def Cls.fin(k: Cls) -> Bool:
819 match k:
820 case Fin{}:
821 True{}
822 case Inf{}:
823 False{}
824 case Nan{}:
825 False{}
826
827def Cls.nan(k: Cls) -> Bool:
828 match k:
829 case Nan{}:
830 True{}
831 case Fin{}:
832 False{}
833 case Inf{}:
834 False{}
835
836def 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
843def 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
850def 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
857def 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
862def 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
867def div.norm(k: U32, mb: W2) -> W2:
868 W2.shl(mb, k)
869
870def div.sig.q(sign: U32, exp: U32, r: W4 & Bool) -> F64:
871 (q, sticky) = r
872 under(sign, exp, q, sticky)
873
874def 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
877def 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
880def 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
887def 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
894def 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
901def 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
908def 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
915def 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
918def 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
925def 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
932def 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
937def 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
942def 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
945def F64.zero.bits(h: U32, l: U32) -> Bool:
946 Bool.and(U32.is_zero((h .&. 2147483647 : U32)), U32.is_zero(l))
947
948def F64.is_nan(a: F64) -> Bool:
949 match a:
950 case F64{hi, lo}:
951 F64.nan.bits(hi, lo)
952
953def 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
958def F64.is_zero(a: F64) -> Bool:
959 match a:
960 case F64{hi, lo}:
961 F64.zero.bits(hi, lo)
962
963def 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
968def 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
971def 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
978def 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
985def 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
992def 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
999def 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
1004def 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
1011def 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
1018def 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
1021def 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
1028def 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
1035def 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
1042def 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
1049def 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
1056def 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
1063def 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
1070def 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
1075def F64.is_ne(a: F64, b: F64) -> Bool:
1076 Bool.not(F64.is_eq(a, b))
1077
1078def F64.is_le(+a: F64, +b: F64) -> Bool:
1079 Bool.or(F64.is_lt(a, b), F64.is_eq(a, b))
1080
1081def F64.is_gt(a: F64, b: F64) -> Bool:
1082 F64.is_lt(b, a)
1083
1084def F64.is_ge(+a: F64, +b: F64) -> Bool:
1085 Bool.or(F64.is_lt(b, a), F64.is_eq(a, b))
1086
1087def F64.abs(a: F64) -> F64:
1088 match a:
1089 case F64{hi, lo}:
1090 F64{(hi .&. 2147483647 : U32), lo}
1091
1092def 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
1095def 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
1102def F64.from.clz(+z: U32, n: U32) -> F64:
1103 F64.from.small(U32.is_lt(z, 11), z, n)
1104
1105def 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
1112def F64.from_u32(+n: U32) -> F64:
1113 F64.from.z(U32.is_zero(n), n)
1114
1115def F64.one() -> F64:
1116 F64{1072693248, 0}
1117
1118def F64.zero() -> F64:
1119 F64{0, 0}
1120
1121def F64.inf() -> F64:
1122 F64{2146435072, 0}